The three endpoint/penultimate Delta families

This completes part (2) of paper Corollary 2.25 for the marking consisting of the common left endpoint and the penultimate point of one strand.

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

Corollary 2.25(2), first family: a positive right-endpoint multiple up to the genus has marked second difference one.

theorem Bananas.rankDelta_oneOff_balanced_interior_family {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (b r : ℕ) (hg : 0 < g) (hb : b ≤ 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, ⋯⟩)) (↑b • oneChip (leftEndpoint B) + ↑b • oneChip (rightEndpoint B) + oneChip (strandVertex B alpha ⟨r, ⋯⟩)) = 1

Corollary 2.25(2), second family.

theorem Bananas.rankDelta_oneOff_terminal_family {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (a b : ℕ) (hba : b < a) (hag : a ≤ g) (hLength : 1 < B.length alpha) : rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (↑a • oneChip (leftEndpoint B) + ↑b • oneChip (rightEndpoint B) + oneChip (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) = if a = g then 1 else 0

Corollary 2.25(2), third family. A terminal chip contributes the extra corner exactly at the boundary a = g.

theorem Bananas.rankDelta_oneOff_three_families {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (a b r : ℕ) (hba : b < a) (hag : a ≤ g) (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, ⋯⟩)) (a • oneChip (rightEndpoint B)) = 1 ∧ rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (↑b • oneChip (leftEndpoint B) + ↑b • oneChip (rightEndpoint B) + oneChip (strandVertex B alpha ⟨r, ⋯⟩)) = 1 ∧ rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) (↑a • oneChip (leftEndpoint B) + ↑b • oneChip (rightEndpoint B) + oneChip (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) = if a = g then 1 else 0

Corollary 2.25(2), packaged with the paper's common hypotheses 0 ≤ b < a ≤ g and 0 < r < n_alpha - 1.