A simply-laced finite-type diagram has at most one branch vertex

The simply-laced lane of the finite-type Cartan-matrix classification reduces connected diagrams to paths and three-armed stars. Two branch vertices in a tree determine a double-fork subtree: the path between them, together with the two unused edges at either end, has affine type D, whose Cartan matrix is incompatible with finite type.

This file makes that reduction at the matrix level. Given two distinct degree-three vertices in the same component, TauCeti.IsFiniteType.exists_doubleFork_submatrix extracts the corresponding principal submatrix and identifies it with TauCeti.doubleForkCartanMatrix. The latter is not of finite type, contradicting inheritance of finite type by principal submatrices. Consequently a connected simply-laced finite-type diagram has a unique branch vertex whenever one exists.

The simple-lacedness hypothesis is essential at this stage: it identifies every edge on the path with the entry -1. The componentwise results impose it only on the vertices reachable from the first branch vertex, which is where the whole extracted submatrix lives. The separate multiple-edge elimination in the classification removes this hypothesis before the final assembly theorem.

Main results

• TauCeti.IsFiniteType.exists_doubleFork_submatrix: two distinct branch vertices in one simply-laced component contain an affine D principal submatrix.
• TauCeti.IsFiniteType.eq_of_reachable_of_degree_eq_three: two reachable degree-three vertices coincide.
• TauCeti.IsFiniteType.eq_of_degree_eq_three: the connected specialization.

References

This is the affine-D elimination in the “classification of finite-type Cartan matrices” target, Layer 5 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. See J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §11.4, and Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI, §4.

theorem TauCeti.IsFiniteType.exists_doubleFork_submatrix {B : Type u_1} [DecidableEq B] {A : Matrix B B ℤ} [Fintype B] (h : IsFiniteType A) {u v : B} (huv : (diagramGraph A).Reachable u v) (hsl : {w : B | (diagramGraph A).Reachable u w}.Pairwise fun (i j : B) => A i j = 0 ∨ A i j = -1) (huv_ne : u ≠ v) (hu : (diagramGraph A).degree u = 3) (hv : (diagramGraph A).degree v = 3) : ∃ (n : ℕ) (e : DoubleForkIndex n → B), Function.Injective e ∧ A.submatrix e e = doubleForkCartanMatrix n

Two distinct branch vertices in one simply-laced finite-type component contain an affine D principal submatrix. The middle Fin (n + 2) is the path between the branch vertices, and the two outer copies of Fin 2 enumerate the unused neighbours at either end.

Only the component of u is constrained: hsl asks for simple-lacedness on the vertices reachable from u, which is where every selected vertex lives, so components carrying a multiple edge do not obstruct the conclusion.

The returned map is injective, so TauCeti.IsFiniteType.submatrix applies directly. Its matrix identity is oriented to match TauCeti.doubleForkCartanMatrix, the obstruction proved in TauCeti.LinearAlgebra.RootSystem.FiniteType.AffineD.

theorem TauCeti.IsFiniteType.eq_of_reachable_of_degree_eq_three {B : Type u_1} [DecidableEq B] {A : Matrix B B ℤ} [Fintype B] (h : IsFiniteType A) {u v : B} (huv : (diagramGraph A).Reachable u v) (hsl : {w : B | (diagramGraph A).Reachable u w}.Pairwise fun (i j : B) => A i j = 0 ∨ A i j = -1) (hu : (diagramGraph A).degree u = 3) (hv : (diagramGraph A).degree v = 3) : u = v

Reachable degree-three vertices of a simply-laced finite-type diagram coincide. As in TauCeti.IsFiniteType.exists_doubleFork_submatrix, simple-lacedness is needed only on the component of u. Otherwise that theorem produces an affine D principal submatrix, contradicting TauCeti.not_isFiniteType_doubleForkCartanMatrix.

theorem TauCeti.IsFiniteType.eq_of_degree_eq_three {B : Type u_1} [DecidableEq B] {A : Matrix B B ℤ} [Fintype B] (h : IsFiniteType A) (hsl : A.IsSimplyLaced) (hconn : (diagramGraph A).Connected) {u v : B} (hu : (diagramGraph A).degree u = 3) (hv : (diagramGraph A).degree v = 3) : u = v

A connected simply-laced finite-type diagram has at most one branch vertex. This is the connected form used when extracting the D and E Dynkin diagrams from a finite-type matrix.