Components of the length-two cross-exception argument.

Bananas.Semibreak supplies the Dhar support lemma; this file records the midpoint, rank-difference, and dual-degree steps.

Dependent updates of the one-chip-per-strand representation.

def Bananas.replaceSemibreakChip {g : ℕ} (B : Banana g) (chips : (γ : Fin (g + 1)) → Option (Fin (B.length γ - 1))) (β : Fin (g + 1)) (newChip : Option (Fin (B.length β - 1))) (γ : Fin (g + 1)) : Option (Fin (B.length γ - 1))

Replace the optional interior chip on one strand, keeping the chips on every other strand.

Equations

• Bananas.replaceSemibreakChip B chips β newChip γ = if h : γ = β then ⋯ ▸ newChip else chips γ

@[simp]

theorem Bananas.replaceSemibreakChip_same {g : ℕ} (B : Banana g) (chips : (γ : Fin (g + 1)) → Option (Fin (B.length γ - 1))) (β : Fin (g + 1)) (newChip : Option (Fin (B.length β - 1))) : replaceSemibreakChip B chips β newChip β = newChip

theorem Bananas.replaceSemibreakChip_other {g : ℕ} (B : Banana g) (chips : (γ : Fin (g + 1)) → Option (Fin (B.length γ - 1))) (β γ : Fin (g + 1)) (newChip : Option (Fin (B.length β - 1))) (hγ : γ ≠ β) : replaceSemibreakChip B chips β newChip γ = chips γ

theorem Bananas.semibreakDivisor_replace_chip {g : ℕ} (B : Banana g) (chips : (γ : Fin (g + 1)) → Option (Fin (B.length γ - 1))) (β : Fin (g + 1)) (oldChip newChip : Fin (B.length β - 1)) : semibreakDivisor B (replaceSemibreakChip B chips β (some newChip)) = semibreakDivisor B (replaceSemibreakChip B chips β (some oldChip)) + oneChip (Utilities.Certificate.SubdivisionGraph.Spec.interiorVertex B β newChip) - oneChip (Utilities.Certificate.SubdivisionGraph.Spec.interiorVertex B β oldChip)

theorem Bananas.semibreakDivisor_remove_chip {g : ℕ} (B : Banana g) (chips : (γ : Fin (g + 1)) → Option (Fin (B.length γ - 1))) (β : Fin (g + 1)) (oldChip : Fin (B.length β - 1)) : semibreakDivisor B (replaceSemibreakChip B chips β none) = semibreakDivisor B (replaceSemibreakChip B chips β (some oldChip)) - oneChip (Utilities.Certificate.SubdivisionGraph.Spec.interiorVertex B β oldChip)

theorem Bananas.isSemibreak_remove_chip {g : ℕ} (B : Banana g) (chips : (γ : Fin (g + 1)) → Option (Fin (B.length γ - 1))) (β : Fin (g + 1)) (_oldChip : Fin (B.length β - 1)) : IsSemibreak B (semibreakDivisor B (replaceSemibreakChip B chips β none))

theorem Bananas.isSemibreak_remove_interior_chip_of_eq_one {g : ℕ} (B : Banana g) (E : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (hE : IsSemibreak B E) (β : Fin (g + 1)) (offset : Fin (B.length β - 1)) (hmem : E (Utilities.Certificate.SubdivisionGraph.Spec.interiorVertex B β offset) = 1) : IsSemibreak B (E - oneChip (Utilities.Certificate.SubdivisionGraph.Spec.interiorVertex B β offset))

Removing an occupied raw interior chip from a semibreak divisor remains semibreak. This is the coordinate-free form of the midpoint update below.

The preceding identity is phrased in the chip-coordinate API. This adapter exposes the same operation from the paper-facing IsSemibreak predicate at a length-two midpoint.

theorem Bananas.isSemibreak_remove_midpoint_chip {g : ℕ} (B : Banana g) (E : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (hE : IsSemibreak B E) (α : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (hα : B.length α = 2) (hi : ↑i = 1) (hmem : E (strandVertex B α i) = 1) : IsSemibreak B (E - oneChip (strandVertex B α i))

In the low-degree range, removing a chip already present in the semibreak part leaves the normal-form rank unchanged. This is the rank calculation used for the “midpoint is a base point” half of the proposed exception proof.

theorem Bananas.rank_bananaNormalForm_remove_midpoint_chip {g : ℕ} (B : Banana g) (E : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (hE : IsSemibreak B E) (α : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (hα : B.length α = 2) (hi : ↑i = 1) (a b : ℤ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hdeg : a + b + CFDiv.degree E ≤ ↑g) (hmem : E (strandVertex B α i) = 1) : rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (bananaNormalForm B a b E) = rank (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (bananaNormalForm B a b E - oneChip (strandVertex B α i))

noncomputable def Bananas.basePointDrop (M : TwiceMarked) (D : CFDiv M.graph) : ℤ

The drop in divisor rank when one chip is removed from the first mark.

Equations

• Bananas.basePointDrop M D = rank M.graph D - rank M.graph (D - oneChip M.u)

A convenient difference form of the path-pair sliding identities.

theorem Bananas.linear_equiv_rearrange_pair {G : CFGraph} {A B C D : CFDiv G} (h : linearEquiv G (A + B) (C + D)) : linearEquiv G (A - C) (D - B)

theorem Bananas.path_pair_linearEquiv_tail_sum_sub {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i k : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (hi : 0 < ↑i) (hk : 0 < ↑k) (hsum : ↑i + ↑k < B.length α) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α i) - oneChip (Utilities.Certificate.SubdivisionGraph.Spec.coreVertex B (B.core.tail α))) (oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α ⟨↑i + ↑k, ⋯⟩) - oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α k))

theorem Bananas.path_pair_linearEquiv_head_excess_sub {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i k : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (hi : ↑i < B.length α) (hk : ↑k < B.length α) (hsum : B.length α < ↑i + ↑k) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α i) - oneChip (Utilities.Certificate.SubdivisionGraph.Spec.coreVertex B (B.core.head α))) (oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α ⟨↑i + ↑k - B.length α, ⋯⟩) - oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B α k))

theorem Bananas.rankDelta_eq_basePointDrop_sub (M : TwiceMarked) (D : CFDiv M.graph) : rankDelta M D = basePointDrop M D - basePointDrop M (D - oneChip M.v)

theorem Bananas.two_smul_midpoint_linearEquiv_endpoints {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (hα : B.length α = 2) (hi : ↑i = 1) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (2 • oneChip (strandVertex B α i)) (oneChip (leftEndpoint B) + oneChip (rightEndpoint B))

theorem Bananas.deg_canonical_dual {g : ℕ} (B : Banana g) (u v : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : CFDiv.degree (canonicalDivisor (Utilities.Certificate.SubdivisionGraph.Spec.graph B) + oneChip u + oneChip v - D) = 2 * ↑g - CFDiv.degree D