Rank-difference calculation for the cross-one-off marking

This file proves the first assertion of part (3) of paper Corollary 2.25 (cor-BananaDeltaComps). The marked points lie one step from opposite endpoints on two distinct strands. The proof packages the two remaining interior chips as a semibreak divisor, shifts them after deleting a marked point, and applies the endpoint/semibreak rank formula four times.

def Bananas.normalizedInteriorOffset {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (hp : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α p) : Fin (B.length α - 1)

The storage-oriented interior offset corresponding to a normalized interior strand position.

Equations

• Bananas.normalizedInteriorOffset B α p hp = if htail : B.core.tail α = 0 then ⟨↑p - 1, ⋯⟩ else ⟨B.length α - ↑p - 1, ⋯⟩

theorem Bananas.strandVertex_eq_interiorVertex_normalizedInteriorOffset {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (hp : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α p) : strandVertex B α p = Utilities.Certificate.SubdivisionGraph.Spec.interiorVertex B α (normalizedInteriorOffset B α p hp)

theorem Bananas.isSemibreak_two_distinct_strand_chips {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (q : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hp : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α p) (hq : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B β q) (hαβ : α ≠ β) : IsSemibreak B (oneChip (strandVertex B α p) + oneChip (strandVertex B β q))

Two normalized interior chips on distinct strands form a semibreak divisor.

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

Paper Corollary 2.25(3), first rank-difference calculation, in normalized coordinates.