Top paths of Π(A_{2N+1})

characteristic-two-mesh-calculations.tex: for a line, "V_{d+1} = 𝒜V_d − V_{d−1} … the remaining parity interval is exactly |i − j| ≤ d ≤ min(i + j − 2, 2M − i − j), d ≡ i − j (mod 2). This proves the claimed formula and V_{M−1} is reflection." With the lower bound eq:preprojective-lower-bound, every vertex of Π(A_{2N+1}) has a nonzero path of degree 2N to its reflection, over every field.

We use the line rooted at its middle vertex, ReRoot.Lmid N (two arms of N vertices), with signed positions −N, …, N; there the recurrence matrices are U_d = V_d of DTop.V.

theorem MultiplicativeBasisDeformations.LineTop.pos_le (N : ℕ) (hN : 1 ≤ N) (v : StarV (ReRoot.Lmid N)) : -↑N ≤ ReRoot.pos v ∧ ReRoot.pos v ≤ ↑N

theorem MultiplicativeBasisDeformations.LineTop.nb_pos (N : ℕ) (hN : 1 ≤ N) (x : StarV (ReRoot.Lmid N)) (G : ℤ → ℤ) (hG : G (↑N + 1) = 0) (hG' : G (-(↑N + 1)) = 0) : ∑ z : (starTree (ReRoot.Lmid N)).Dbl, (starTree (ReRoot.Lmid N)).adjM x z * G (ReRoot.pos z) = G (ReRoot.pos x - 1) + G (ReRoot.pos x + 1)

The sum over neighbours, through positions.

theorem MultiplicativeBasisDeformations.LineTop.U_eq_V (N : ℕ) (hN : 1 ≤ N) (d : ℕ) : d ≤ 2 * N → ∀ (x y : (starTree (ReRoot.Lmid N)).Dbl), UBound.U (starTree (ReRoot.Lmid N)).adjM d x y = DTop.V N d (ReRoot.pos x) (ReRoot.pos y)

The recurrence matrices of the line are V_d.

theorem MultiplicativeBasisDeformations.LineTop.line_return (N : ℕ) (hN : 1 ≤ N) {k : Type u_1} [Field k] (v w : (starTree (ReRoot.Lmid N)).Dbl) (hw : ReRoot.pos w = -ReRoot.pos v) : ∃ (p : Quiver.Path v w), p.length = 2 * N ∧ LinearPaths.path p ∉ (starTree (ReRoot.Lmid N)).Id k v w

Top paths of Π(A_{2N+1}): every vertex has a path of degree 2N to its reflection outside the ideal, over every field.