The sectional tree is a Dynkin tree

Proof of Proposition 4.1, Step 2: combining the preceding steps for the tree Δ of sectional paths of a finite stable translation quiver with a finite-dimensional scalar mesh category.

• Δ is a tree (isTree): it is connected through parents, and its edges are the parent edges.
• Long paths vanish in Π(Δ) (PreprojectiveNilpotent.lean), so n_i = dim P_i is finite and ∑_{j∼i} n_j < 2 n_i (PreprojectiveDimension.lean).
• Hence Δ is a star model with at most one arm, or with three arms satisfying ∑ p_i/(p_i + 1) < 2 (classify_tree).

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.eq_root_of_len {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} {p : Q.SecPath x₀} (h : p.len = 0) : p = root Q x₀

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.len_parent {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} (p : Q.SecPath x₀) (hp : p.len ≠ 0) : (p.parent hp).len + 1 = p.len

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.reachable_root {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} (p : Q.SecPath x₀) : tree.G.Reachable (root Q x₀) p

Δ is connected.

def MultiplicativeBasisDeformations.TranslationQuiver.SecPath.parentEdge {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} (p : { p : Q.SecPath x₀ // p ≠ root Q x₀ }) : ↑tree.G.edgeSet

The parent edge of a nonroot vertex.

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.parentEdge_bijective {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} : Function.Bijective parentEdge

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.isTree {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} [Finite (Q.SecPath x₀)] : tree.G.IsTree

Δ is a tree.

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.sum_outArrow {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.G.Adj] (i : D) (f : D → ℚ) : ∑ e : T.OutArrow (T.toDbl i), f e.fst = ∑ j ∈ T.G.neighborFinset i, f j

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.sectional_star_model {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x₀ : V} {k : Type u} [Field k] [Finite V] [∀ (x y : V), Subsingleton (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (hQ : Q.IsStable) (c : MeshCoefficients k Q) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) [Fintype (Q.SecPath x₀)] [DecidableEq (Q.SecPath x₀)] : ∃ (t : ℕ) (L : Fin t → ℕ) (e : Q.SecPath x₀ ≃ StarV L), (∀ (p q : Q.SecPath x₀), tree.G.Adj p q ↔ starAdj (e p) (e q)) ∧ (t ≤ 1 ∨ t = 3 ∧ ∑ i : Fin t, (↑(L i) + 1) / (↑(L i) + 2) < 2)

Proposition 4.1, Step 2: the tree of sectional paths of a finite stable translation quiver with a finite-dimensional scalar mesh category is a Dynkin tree, in the form of a star model.