Long paths vanish in Π(Δ)

Proof of Proposition 4.1, Steps 1–2 (periodic-mesh-calculations.tex): "In particular every upstairs path of length at least N is zero ... Forgetting the integer coordinate identifies the lifted mesh relations with its relations, and every path lifts. The uniform path bound makes Π(Δ) finite-dimensional."

A path of the doubled tree lifts to ℤΔ (forget is a covering), its image under π is a long path of Q, hence zero; π reflects the mesh ideal, the rescaling of Step 2 moves it to the signed mesh ideal, and forgetting heights lands in the ideal of Π(Δ).

theorem MultiplicativeBasisDeformations.TranslationQuiver.SecPath.path_mem_preproj {V : Type v} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) {x₀ : V} {k : Type u} [Field k] [Fintype (Q.SecPath x₀)] [DecidableEq (Q.SecPath x₀)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] [DecidableRel tree.orient] (c : MeshCoefficients k Q) (N : ℕ) (hN : ∀ (x y : V) (p : Quiver.Path x y), N ≤ p.length → LinearPaths.path p ∈ (RelSystem.mesh c).ideal (LinearPaths.obj x) (LinearPaths.obj y)) {v w : tree.Dbl} (P : Quiver.Path v w) (hP : N ≤ P.length) : LinearPaths.path P ∈ (tree.preproj k).ideal (LinearPaths.obj v) (LinearPaths.obj w)

Every path of length at least N vanishes in Π(Δ), if every path of length at least N vanishes in C(Q, c).