Firing identities for the cross-one-off marking

This file formalizes the chip-firing calculation behind Lemma 4.30 of the twice-marked banana paper. Coordinates are the normalized coordinates of strandVertex. Write L,R for the two multivalent vertices, put

u = v_{α,1}, v = v_{β,N-1}, and b = mN+r.

The common identity is

gR + au - bv ~ (a-m-2)L + (g+m-b)R + v_{α,a} + v_{β,r}.

It simultaneously fixes the residue convention and the two-off-by-one error in the printed third case. The three residue-specific corollaries below are the divisor identities needed before applying the banana normal-form rank calculus.

theorem Bananas.crossOneOff_first_mark_multiple {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (a : ℕ) (ha : a ≤ B.length α) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (↑a • oneChip (strandVertex B α ⟨1, ⋯⟩)) ((↑a - 1) • oneChip (leftEndpoint B) + oneChip (strandVertex B α ⟨a, ⋯⟩))

A multiple of the first off-endpoint mark can be replaced by one chip at the corresponding coordinate and the remaining chips at the left endpoint. This is the α-strand part of Lemma 4.30.

theorem Bananas.crossOneOff_sub_first_mark_shift {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (p : ℕ) (hpLo : 1 ≤ p) (hpHi : p ≤ B.length α) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip (strandVertex B α ⟨p, ⋯⟩) - oneChip (strandVertex B α ⟨1, ⋯⟩)) (oneChip (strandVertex B α ⟨p - 1, ⋯⟩) - oneChip (leftEndpoint B))

Deleting the first off-endpoint mark from a chip farther along the same strand shifts that chip one step toward the left endpoint.

theorem Bananas.crossOneOff_sub_second_mark_shift {g : ℕ} (B : Banana g) (β : Fin (g + 1)) (q : ℕ) (hq : q < B.length β) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip (strandVertex B β ⟨q, ⋯⟩) - oneChip (strandVertex B β ⟨B.length β - 1, ⋯⟩)) (oneChip (strandVertex B β ⟨q + 1, ⋯⟩) - oneChip (rightEndpoint B))

Deleting the second off-endpoint mark from a chip earlier on the same strand shifts that chip one step toward the right endpoint.

theorem Bananas.crossOneOff_second_mark_multiple {g : ℕ} (B : Banana g) (β : Fin (g + 1)) (b m r : ℕ) (hb : b = m * B.length β + r) (hr : r ≤ B.length β) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (↑b • oneChip (strandVertex B β ⟨B.length β - 1, ⋯⟩)) ((↑m + 1) • oneChip (leftEndpoint B) + (↑b - ↑m) • oneChip (rightEndpoint B) - oneChip (strandVertex B β ⟨r, ⋯⟩))

If b = mN+r, a multiple of the second off-endpoint mark has the canonical endpoint-plus-residue representative. This is the common β-strand calculation behind all three cases of Lemma 4.30.

theorem Bananas.crossOneOff_firing_identity {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (a b m r : ℕ) (ha : a ≤ B.length α) (hb : b = m * B.length β + r) (hr : r ≤ B.length β) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (↑g • oneChip (rightEndpoint B) + ↑a • oneChip (strandVertex B α ⟨1, ⋯⟩) - ↑b • oneChip (strandVertex B β ⟨B.length β - 1, ⋯⟩)) ((↑a - ↑m - 2) • oneChip (leftEndpoint B) + (↑g + ↑m - ↑b) • oneChip (rightEndpoint B) + oneChip (strandVertex B α ⟨a, ⋯⟩) + oneChip (strandVertex B β ⟨r, ⋯⟩))

The common corrected firing identity for the cross-one-off marking.

The corrected residue cases of Lemma 4.30

theorem Bananas.crossOneOff_firing_multiple {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (b m : ℕ) (hb : b = m * B.length β) (ha : m + 1 ≤ B.length α) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (↑g • oneChip (rightEndpoint B) + ↑(m + 1) • oneChip (strandVertex B α ⟨1, ⋯⟩) - ↑b • oneChip (strandVertex B β ⟨B.length β - 1, ⋯⟩)) (oneChip (strandVertex B α ⟨m + 1, ⋯⟩) + (↑g + ↑m - ↑b) • oneChip (rightEndpoint B))

Lemma 4.30(1), at a positive multiple b = mN. The theorem is only a firing identity; the numerical hypotheses used later to identify the transmission value are deliberately kept separate.

theorem Bananas.crossOneOff_firing_complement_residue {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (b m : ℕ) (hm : 1 ≤ m) (hb : b + 1 = m * B.length β) (ha : g + m ≤ B.length α) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (↑g • oneChip (rightEndpoint B) + ↑(g + m) • oneChip (strandVertex B α ⟨1, ⋯⟩) - ↑b • oneChip (strandVertex B β ⟨B.length β - 1, ⋯⟩)) ((↑g - 1) • oneChip (leftEndpoint B) + (↑g - ↑m * (↑(B.length β) - 1)) • oneChip (rightEndpoint B) + oneChip (strandVertex B α ⟨g + m, ⋯⟩) + oneChip (strandVertex B β ⟨B.length β - 1, ⋯⟩))

Lemma 4.30(2), in the unambiguous convention b+1 = mN. The length-two, b=1 exception concerns the subsequent Δ claim, not this firing identity.

theorem Bananas.crossOneOff_firing_positive_residue {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (b m r : ℕ) (hb : b = m * B.length β + r) (_hrLo : 1 ≤ r) (hrHi : r + 1 < B.length β) (hCandidate : b ≤ g + 2 * m + 2) (ha : g + 2 * m + 2 - b ≤ B.length α) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (↑g • oneChip (rightEndpoint B) + ↑(g + 2 * m + 2 - b) • oneChip (strandVertex B α ⟨1, ⋯⟩) - ↑b • oneChip (strandVertex B β ⟨B.length β - 1, ⋯⟩)) ((↑g + ↑m - ↑b) • (oneChip (leftEndpoint B) + oneChip (rightEndpoint B)) + oneChip (strandVertex B α ⟨g + 2 * m + 2 - b, ⋯⟩) + oneChip (strandVertex B β ⟨r, ⋯⟩))

Corrected Lemma 4.30(3), using the positive remainder convention b = mN+r, 1 ≤ r ≤ N-2. The printed coefficient of L+R is one too large and its complementary coordinate belongs to the other residue convention.