Remaining cross-one-off Delta families

This completes the rank-difference assertions in part (3) of paper Corollary 2.25.

theorem Bananas.rankDelta_crossOneOff_right_interior_family {g : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (b : ℕ) (hg : 2 ≤ g) (hab : alpha ≠ beta) (hpLo : 2 ≤ ↑p) (hpHi : ↑p < B.length alpha) (hBeta : 2 ≤ B.length beta) (hb : b < g) : rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) (↑b • oneChip (rightEndpoint B) + oneChip (strandVertex B alpha p)) = 1

Corollary 2.25(3): a right-endpoint coefficient and one sufficiently interior chip on the first marked strand have second difference one.

theorem Bananas.rankDelta_crossOneOff_two_interior_boundary_eq_zero {g : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (q : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B beta) (hg : 2 ≤ g) (hab : alpha ≠ beta) (hpLo : 2 ≤ ↑p) (hpHi : ↑p < B.length alpha) (hqLo : 1 ≤ ↑q) (hqHi : ↑q + 1 < B.length beta) : rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) ((↑g - 1) • (oneChip (leftEndpoint B) + oneChip (rightEndpoint B)) + oneChip (strandVertex B alpha p) + oneChip (strandVertex B beta q)) = 0

The two-interior family at its top coefficient. Here the first three divisors are nonspecial, while the twice-subtracted divisor remains in the banana normal-form range, and the second difference is zero.

theorem Bananas.rankDelta_crossOneOff_terminal_delta_family {g : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (b : ℕ) (hg : 2 ≤ g) (hab : alpha ≠ beta) (hpLo : 2 ≤ ↑p) (hpHi : ↑p < B.length alpha) (hBeta : 2 ≤ B.length beta) (hb : b ≤ g - 1) : rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) ((↑g - 1) • oneChip (leftEndpoint B) + ↑b • oneChip (rightEndpoint B) + oneChip (strandVertex B alpha p) + oneChip (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) = if b < g - 1 then 1 else 0

Corollary 2.25(3), the terminal-chip delta family.

theorem Bananas.rankDelta_crossOneOff_balanced_delta_family {g : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (q : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B beta) (b : ℕ) (hg : 2 ≤ g) (hab : alpha ≠ beta) (hpLo : 2 ≤ ↑p) (hpHi : ↑p < B.length alpha) (hqLo : 1 ≤ ↑q) (hqHi : ↑q + 1 < B.length beta) (hb : b ≤ g - 1) : rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) (↑b • (oneChip (leftEndpoint B) + oneChip (rightEndpoint B)) + oneChip (strandVertex B alpha p) + oneChip (strandVertex B beta q)) = if b < g - 1 then 1 else 0

Corollary 2.25(3), the balanced two-interior delta family.