The endpoint residue cases for the cross-one-off marking

This file proves the two rank-difference calculations that complement rankDelta_crossOneOff_two_interior_eq_one. Together they are the three corrected residue cases used in Lemma 4.30 of the paper.

The complementary-residue calculation is stated both in its valid range and at its unique boundary exception. At the latter boundary the second difference is zero, not one; arithmetically that boundary is exactly the paper's N = 2, b = 1 case.

theorem Bananas.isSemibreak_one_strand_chip {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (hp : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α p) : IsSemibreak B (oneChip (strandVertex B α p))

A single chip at a normalized interior position is a semibreak divisor.

theorem Bananas.rankDelta_crossOneOff_multiple_normalForm_eq_one {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (c : ℕ) (hg : 2 ≤ g) (hαβ : α ≠ β) (hpLo : 2 ≤ ↑p) (hpHi : ↑p < B.length α) (hβLength : 2 ≤ B.length β) (hc : c ≤ g - 1) : rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α ⟨1, ⋯⟩) (strandVertex B β ⟨B.length β - 1, ⋯⟩)) (↑c • oneChip (rightEndpoint B) + oneChip (strandVertex B α p)) = 1

The positive-multiple residue case of corrected Lemma 4.30. The normal form consists of a right-endpoint coefficient and one interior chip on the first marked strand.

theorem Bananas.rankDelta_crossOneOff_complement_normalForm_eq_one {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (c : ℕ) (hg : 2 ≤ g) (hαβ : α ≠ β) (hpLo : 2 ≤ ↑p) (hpHi : ↑p < B.length α) (hβLength : 2 ≤ B.length β) (hc : c < g - 1) : rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α ⟨1, ⋯⟩) (strandVertex B β ⟨B.length β - 1, ⋯⟩)) ((↑g - 1) • oneChip (leftEndpoint B) + ↑c • oneChip (rightEndpoint B) + oneChip (strandVertex B α p) + oneChip (strandVertex B β ⟨B.length β - 1, ⋯⟩)) = 1

The complementary-residue normal form has second rank difference one away from its top boundary. The strict inequality c < g - 1 is essential: the next theorem computes the omitted boundary value as zero.

theorem Bananas.rankDelta_crossOneOff_complement_boundary_eq_zero {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (hg : 2 ≤ g) (hpLo : 2 ≤ ↑p) (hpHi : ↑p < B.length α) (hβLength : 2 ≤ B.length β) : rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α ⟨1, ⋯⟩) (strandVertex B β ⟨B.length β - 1, ⋯⟩)) ((↑g - 1) • oneChip (leftEndpoint B) + (↑g - 1) • oneChip (rightEndpoint B) + oneChip (strandVertex B α p) + oneChip (strandVertex B β ⟨B.length β - 1, ⋯⟩)) = 0

At the omitted top boundary c = g - 1, the complementary-residue normal form has second rank difference zero. This is the formal obstruction behind the false N = 2, b = 1 instance in the printed Lemma 4.30(2).

theorem Bananas.crossOneOff_complement_boundary_iff_length_two {g N m b : ℕ} (hN : 2 ≤ N) (hm : 1 ≤ m) (hProduct : m * (N - 1) ≤ g) (hb : b + 1 = m * N) : m * (N - 1) = 1 ↔ N = 2 ∧ m = 1 ∧ b = 1

Under the arithmetic hypotheses of the complementary residue case, its top normal-form coefficient occurs exactly for N = 2, m = 1, and then the paper's row coordinate is b = 1.