Positive interior-residue rows for the same-strand one-off marking #
This completes the three residue classes of Lemma 4.23. Write
b = m n + r with 1 ≤ r and r+1 < n, and put c = g+m-b. The
correct firing target is
c·L + c·R + v_(alpha,r).
The paper's final displayed divisor repeats v_(0,0) twice; the second copy
must be the right endpoint. With that correction the divisor has the right
degree and its marked second difference is one.
theorem
Bananas.oneOff_firing_positive_residue
{g : ℕ}
(B : Banana g)
(alpha : Fin (g + 1))
(b m r c : ℕ)
(hLength : 1 < B.length alpha)
(hb : b = m * B.length alpha + r)
(_hrLo : 1 ≤ r)
(hrHi : r + 1 < B.length alpha)
(hbm : b ≤ g + m)
(hc : c = g + m - b)
:
linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)
(g • oneChip (rightEndpoint B) + ↑(g + 2 * m + 1 - b) • oneChip (leftEndpoint B) - ↑b • oneChip (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩))
(↑c • oneChip (leftEndpoint B) + ↑c • oneChip (rightEndpoint B) + oneChip (strandVertex B alpha ⟨r, ⋯⟩))
Corrected positive-residue firing identity for Lemma 4.23.
theorem
Bananas.rankDelta_oneOff_positive_normalForm_eq_one
{g : ℕ}
(B : Banana g)
(alpha : Fin (g + 1))
(c r : ℕ)
(hg : 2 ≤ g)
(hc : c ≤ g - 1)
(hLength : 1 < B.length alpha)
(hrLo : 1 ≤ r)
(hrHi : r + 1 < B.length alpha)
:
rankDelta
(mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B)
(strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩))
(↑c • oneChip (leftEndpoint B) + ↑c • oneChip (rightEndpoint B) + oneChip (strandVertex B alpha ⟨r, ⋯⟩)) = 1
The corrected positive-residue normal form has marked second difference one throughout its numerical range.
theorem
Bananas.transmission_oneOff_positive_residue
{g : ℕ}
(B : Banana g)
(alpha : Fin (g + 1))
(b m r : ℕ)
(tau : ℤ → ℤ)
(hg : 2 ≤ g)
(hLength : 1 < B.length alpha)
(hb : b = m * B.length alpha + r)
(hrLo : 1 ≤ r)
(hrHi : r + 1 < 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)
:
Lemma 4.23, positive interior-residue case.