Top paths of Π(A_M) for a path rooted at an end

characteristic-two-mesh-calculations.tex: for the line on 1, …, M, (V_d)_{ij} = 1 exactly when |i − j| ≤ d ≤ min(i + j − 2, 2M − i − j) and d ≡ i − j (mod 2), for 0 ≤ d ≤ M − 1; "V_{M−1} is reflection". With the lower bound eq:preprojective-lower-bound, every vertex of Π(A_M) has a nonzero path of degree M − 1 to its reflection. This is the form used for the even lines A_{r+1} retained in the odd quotients of even A.

Here the line is the one-armed star (L 0 = M − 2), and the position of a vertex is its depth plus one.

def MultiplicativeBasisDeformations.LineTop.VL (M d : ℕ) (i j : ℤ) : ℤ

The line formula on positions 1, …, M.

theorem MultiplicativeBasisDeformations.LineTop.VL_nonneg (M d : ℕ) (i j : ℤ) : 0 ≤ VL M d i j

theorem MultiplicativeBasisDeformations.LineTop.VL_rec (M d : ℕ) (hd : d + 2 ≤ M - 1) (i j : ℤ) (hi : 1 ≤ i ∧ i ≤ ↑M) (hj : 1 ≤ j ∧ j ≤ ↑M) : VL M (d + 2) i j = VL M (d + 1) (i - 1) j + VL M (d + 1) (i + 1) j - VL M d i j

theorem MultiplicativeBasisDeformations.LineTop.VL_out (M d : ℕ) (j : ℤ) (hj : 1 ≤ j ∧ j ≤ ↑M) : VL M d (↑M + 1) j = 0 ∧ VL M d 0 j = 0

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.LineTop.psn {L : Fin 1 → ℕ} (v : StarV L) : ℤ

The position of a vertex: its depth plus one.

theorem MultiplicativeBasisDeformations.LineTop.psn_le {L : Fin 1 → ℕ} (v : StarV L) : 1 ≤ psn v ∧ psn v ≤ ↑(L 0) + 2

theorem MultiplicativeBasisDeformations.LineTop.nb_psn {L : Fin 1 → ℕ} (x : StarV L) (G : ℤ → ℤ) (hG : G (↑(L 0) + 3) = 0) (hG' : G 0 = 0) : ∑ z : (starTree L).Dbl, (starTree L).adjM x z * G (psn z) = G (psn x - 1) + G (psn x + 1)

theorem MultiplicativeBasisDeformations.LineTop.U_eq_VL {L : Fin 1 → ℕ} (d : ℕ) : d ≤ L 0 + 1 → ∀ (x y : (starTree L).Dbl), UBound.U (starTree L).adjM d x y = VL (L 0 + 2) d (psn x) (psn y)

The recurrence matrices of the line rooted at an end.

theorem MultiplicativeBasisDeformations.LineTop.end_return {L : Fin 1 → ℕ} {k : Type u_1} [Field k] (v w : (starTree L).Dbl) (hw : psn w = ↑(L 0) + 3 - psn v) : ∃ (p : Quiver.Path v w), p.length = L 0 + 1 ∧ LinearPaths.path p ∉ (starTree L).Id k v w

Top paths of Π(A_M), M = L 0 + 2: every vertex has a path of degree M − 1 to its reflection outside the ideal, over every field.