Multiple-residue rows for the same-strand one-off marking

This file proves the first full residue class in Lemma 4.23. If the row index is b = m n, where n is the length of the marked strand, then the prefix firing reduces the marked twist of g • rightEndpoint to (g+m-b) • rightEndpoint. Its marked second difference is one, forcing tau(b)=m.

theorem Bananas.oneOff_firing_multiple {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (b m c : ℕ) (hLength : 1 < B.length alpha) (hb : b = m * B.length alpha) (hbm : b ≤ g + m) (hc : c = g + m - b) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (g • oneChip (rightEndpoint B) + ↑m • oneChip (leftEndpoint B) - ↑b • oneChip (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (c • oneChip (rightEndpoint B))

The multiple-residue firing identity for the one-off marking.

theorem Bananas.rankDelta_oneOff_rightEndpoint_nsmul_eq_one_all {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (c : ℕ) (hcg : c ≤ g) (hLength : 1 < B.length alpha) : rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (c • oneChip (rightEndpoint B)) = 1

The right-endpoint rank-difference theorem including coefficient zero. The positive case is rankDelta_oneOff_rightEndpoint_nsmul_eq_one; at zero all three chip-subtracted divisors have negative degree.

theorem Bananas.transmission_oneOff_multiple {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (b m : ℕ) (tau : ℤ → ℤ) (hLength : 1 < B.length alpha) (hb : b = m * B.length alpha) (hbm : b ≤ g + m) (hTau : IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) tau) : tau ↑b = ↑m

Lemma 4.23, multiple-residue case: if b=m·n, the transmission row has value m. The inequality b ≤ g+m is exactly the nonnegativity of the residual right-endpoint coefficient used in the paper.

theorem Bananas.transmission_oneOff_length {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (tau : ℤ → ℤ) (hLength : 1 < B.length alpha) (hLengthBound : B.length alpha ≤ g + 1) (hTau : IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) tau) : tau ↑(B.length alpha) = 1

The first positive multiple row, recorded without auxiliary quotient variables: if the strand length is at most g+1, then tau(n)=1.

Complement-residue rows

theorem Bananas.oneOff_firing_complement {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (b m c : ℕ) (hLength : 1 < B.length alpha) (hm : 0 < m) (hb : b + 1 = m * B.length alpha) (hbm : b + 1 ≤ g + m) (hc : c = g + m - b - 1) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (g • oneChip (rightEndpoint B) + ↑(g + m) • oneChip (leftEndpoint B) - ↑b • oneChip (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (↑g • oneChip (leftEndpoint B) + oneChip (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩) + c • oneChip (rightEndpoint B))

The corrected firing identity when b+1=m·n. The normal form is gL + v + (g+m-b-1)R; this has the same degree as the marked twist. The right-endpoint coefficient printed in the paper's intermediate display does not have that degree.

theorem Bananas.rankDelta_oneOff_complement_normalForm_eq_one {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (c : ℕ) (hg : 0 < g) (hc : c ≤ g - 1) (hLength : 1 < B.length alpha) : rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (↑g • oneChip (leftEndpoint B) + oneChip (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩) + c • oneChip (rightEndpoint B)) = 1

The marked second difference of the complement-residue normal form is one.

theorem Bananas.transmission_oneOff_complement {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (b m : ℕ) (tau : ℤ → ℤ) (hg : 0 < g) (hLength : 1 < B.length alpha) (hm : 0 < m) (hb : b + 1 = m * B.length alpha) (hbm : b + 1 ≤ g + m) (hTau : IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) tau) : tau ↑b = ↑(g + m)

Lemma 4.23, complement-residue case: if b+1=m·n, then the transmission value is g+m.