Mesh corrections on a connected stable translation quiver

Appendix A, periodic-mesh-calculations.tex: "By Proposition 5.1 we may restrict to periodic components; … a periodic component without arrows has no rows of degree at least three. Proposition 4.1 then allows us to work with the finite tree models." This file treats a finite connected stable translation quiver: by Proposition 4.1 it is covered by a star model; the types A and D are settled here, and the types E are passed in as a hypothesis (they are treated with the brick hypothesis in ECase.lean).

theorem MultiplicativeBasisDeformations.StarTrace.exists_third (a b : Fin 3) : a ≠ b → ∃ (c : Fin 3), a ≠ c ∧ b ≠ c

theorem MultiplicativeBasisDeformations.StarTrace.connected_surjective {V : Type v'} [Quiver V] [Fintype V] [DecidableEq V] [∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] [(x y : V) → DecidableEq (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype ↑Q.nonprojective] {k : Type u} [Field k] (c : MeshCoefficients k Q) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (h2 : 2 ≠ 0) (x₀ : V) (hconn : ∀ (v : V), Relation.EqvGen (TranslationQuiver.SecPath.ConnAdj hQ) x₀ v) (hE : ∀ (L : Fin 3 → ℕ) (π : (starTree L).ZVert ⥤q V), π.IsCovering → (∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) → (∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) → (∃ (a : Fin 3) (b : Fin 3) (c : Fin 3), a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ L a = 0 ∧ L b = 1 ∧ 1 ≤ L c ∧ L c ≤ 3) → ∀ (m : ℕ), 2 ≤ m → ScalarMeshCategory.MeshDerivativeSurjective c m) (m : ℕ) (hm : 2 ≤ m) : ScalarMeshCategory.MeshDerivativeSurjective c m

Mesh corrections vanish on a connected periodic quiver of type A or D; the types E are supplied by hE.