Slope arithmetic for torsion classes on banana graphs

This file generalizes the normalized-slope part of ThetaPrincipal.lean from three strands to an arbitrary banana. It is the potential-theoretic input to the corrected Proposition 4.19: a principal multiple of a marked difference has one common endpoint rise, while every unmarked strand carries a nonzero integral slope when that rise is nonzero.

def Bananas.bananaPathValue {g : ℕ} (B : Banana g) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin (g + 1)) (r : ℕ) : ℤ

Evaluate a firing script at a strand position, with value zero beyond the strand endpoint.

Equations

• Bananas.bananaPathValue B script α r = if hr : r ≤ B.length α then script (Bananas.strandVertex B α ⟨r, ⋯⟩) else 0

def Bananas.bananaStepSlope {g : ℕ} (B : Banana g) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin (g + 1)) (r : ℕ) : ℤ

The difference of consecutive firing-script values along a strand.

Equations

• Bananas.bananaStepSlope B script α r = Bananas.bananaPathValue B script α (r + 1) - Bananas.bananaPathValue B script α r

theorem Bananas.bananaPathValue_eq {g : ℕ} (B : Banana g) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin (g + 1)) (r : ℕ) (hr : r ≤ B.length α) : bananaPathValue B script α r = script (strandVertex B α ⟨r, ⋯⟩)

theorem Bananas.bananaStepSlope_eq {g : ℕ} (B : Banana g) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin (g + 1)) (r : ℕ) (hr : r < B.length α) : bananaStepSlope B script α r = script (strandVertex B α ⟨r + 1, ⋯⟩) - script (strandVertex B α ⟨r, ⋯⟩)

theorem Bananas.sum_bananaStepSlope {g : ℕ} (B : Banana g) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin (g + 1)) : ∑ r ∈ Finset.range (B.length α), bananaStepSlope B script α r = script (rightEndpoint B) - script (leftEndpoint B)

def Bananas.bananaStorageSlope {g : ℕ} (B : Banana g) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin (g + 1)) (r : ℕ) : ℤ

Express the strand slope in the stored edge orientation, reversing its order and sign when needed.

Equations

• Bananas.bananaStorageSlope B script α r = if B.core.tail α = 0 then Bananas.bananaStepSlope B script α r else -Bananas.bananaStepSlope B script α (B.length α - 1 - r)

theorem Bananas.bananaStorageSlope_isStepSlope {g : ℕ} (B : Banana g) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : Utilities.Certificate.SubdivisionGraph.Spec.IsStepSlope B script (bananaStorageSlope B script)

theorem Bananas.prin_normalized_interior_general {g : ℕ} (B : Banana g) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin (g + 1)) (r : Fin (B.length α - 1)) : (prin (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) script (strandVertex B α ⟨↑r + 1, ⋯⟩) = bananaStepSlope B script α (↑r + 1) - bananaStepSlope B script α ↑r

theorem Bananas.prin_leftEndpoint_eq_sum_initialSlope {g : ℕ} (B : Banana g) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : (prin (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) script (leftEndpoint B) = ∑ α : Fin (g + 1), bananaStepSlope B script α 0

theorem Bananas.prin_rightEndpoint_eq_neg_sum_finalSlope {g : ℕ} (B : Banana g) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : (prin (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) script (rightEndpoint B) = -∑ α : Fin (g + 1), bananaStepSlope B script α (B.length α - 1)

Extracting the initial slope from a principal divisor

def Bananas.bananaInteriorSum {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : ℤ

The sum of a divisor's coefficients at the interior vertices of one strand.

Equations

• Bananas.bananaInteriorSum B α D = ∑ r : Fin (B.length α - 1), D (Bananas.strandVertex B α ⟨↑r + 1, ⋯⟩)

def Bananas.bananaInteriorMoment {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : ℤ

The sum of interior divisor coefficients weighted by their distance from the left endpoint.

Equations

• Bananas.bananaInteriorMoment B α D = ∑ r : Fin (B.length α - 1), ↑(↑r + 1) * D (Bananas.strandVertex B α ⟨↑r + 1, ⋯⟩)

theorem Bananas.bananaInteriorSum_prin {g : ℕ} (B : Banana g) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin (g + 1)) : bananaInteriorSum B α ((prin (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) script) = bananaStepSlope B script α (B.length α - 1) - bananaStepSlope B script α 0

theorem Bananas.bananaInteriorMoment_prin {g : ℕ} (B : Banana g) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin (g + 1)) : bananaInteriorMoment B α ((prin (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) script) = ↑(B.length α) * bananaStepSlope B script α (B.length α - 1) - (script (rightEndpoint B) - script (leftEndpoint B))

theorem Bananas.initialSlope_equation {g : ℕ} (B : Banana g) (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (α : Fin (g + 1)) : ↑(B.length α) * bananaStepSlope B script α 0 = script (rightEndpoint B) - script (leftEndpoint B) + bananaInteriorMoment B α ((prin (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) script) - ↑(B.length α) * bananaInteriorSum B α ((prin (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) script)

The initial slope on a strand is determined by the common rise and the zeroth and first interior moments of the principal divisor.

theorem Bananas.bananaInteriorSum_one_chip {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B β j) : bananaInteriorSum B α (oneChip (strandVertex B β j)) = if α = β then 1 else 0

theorem Bananas.bananaInteriorMoment_one_chip {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B β j) : bananaInteriorMoment B α (oneChip (strandVertex B β j)) = if α = β then ↑↑j else 0

theorem Bananas.bananaInteriorSum_one_chip_leftEndpoint {g : ℕ} (B : Banana g) (α : Fin (g + 1)) : bananaInteriorSum B α (oneChip (leftEndpoint B)) = 0

theorem Bananas.bananaInteriorMoment_one_chip_leftEndpoint {g : ℕ} (B : Banana g) (α : Fin (g + 1)) : bananaInteriorMoment B α (oneChip (leftEndpoint B)) = 0

theorem Bananas.bananaInteriorSum_one_chip_rightEndpoint {g : ℕ} (B : Banana g) (α : Fin (g + 1)) : bananaInteriorSum B α (oneChip (rightEndpoint B)) = 0

theorem Bananas.bananaInteriorMoment_one_chip_rightEndpoint {g : ℕ} (B : Banana g) (α : Fin (g + 1)) : bananaInteriorMoment B α (oneChip (rightEndpoint B)) = 0

theorem Bananas.bananaInteriorSum_sub {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (D E : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : bananaInteriorSum B α (D - E) = bananaInteriorSum B α D - bananaInteriorSum B α E

theorem Bananas.bananaInteriorSum_zsmul {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (z : ℤ) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : bananaInteriorSum B α (z • D) = z * bananaInteriorSum B α D

theorem Bananas.bananaInteriorMoment_sub {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (D E : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : bananaInteriorMoment B α (D - E) = bananaInteriorMoment B α D - bananaInteriorMoment B α E

theorem Bananas.bananaInteriorMoment_zsmul {g : ℕ} (B : Banana g) (α : Fin (g + 1)) (z : ℤ) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : bananaInteriorMoment B α (z • D) = z * bananaInteriorMoment B α D

theorem Bananas.exists_prin_eq_neg_marked_difference_of_torsionWitness {G : CFGraph} (u v : G.V) (k : ℕ) (hk : TorsionWitness (mark G u v) k) : ∃ (script : firingScript G), (prin G) script = ↑k • (oneChip v - oneChip u)

A torsion witness supplies a potential whose principal divisor is the negative marked difference. This orientation makes the left-endpoint sum equal to -k in the endpoint cases.

theorem Bananas.torsion_interior_initialSlope_equations {g k : ℕ} (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hi : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α i) (hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B β j) (hαβ : α ≠ β) (hk : TorsionWitness (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) k) : ∃ (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (rise : ℤ) (slope : Fin (g + 1) → ℤ), rise = script (rightEndpoint B) - script (leftEndpoint B) ∧ ∑ γ : Fin (g + 1), slope γ = 0 ∧ ↑(B.length α) * slope α = rise + ↑(B.length α - ↑i) * ↑k ∧ ↑(B.length β) * slope β = rise - ↑(B.length β - ↑j) * ↑k ∧ ∀ (γ : Fin (g + 1)), γ ≠ α → γ ≠ β → ↑(B.length γ) * slope γ = rise

Initial-slope equations for a principal multiple of two distinct interior marks. The three cases are the two marked strands and every unmarked strand.

The finite-sum arithmetic behind the torsion lower bound

theorem Bananas.endpoint_slope_period_gt_genus {g k : ℕ} (hk : 0 < k) (length : Fin (g + 1) → ℕ) (hlen : ∀ (a : Fin (g + 1)), 0 < length a) (s : Fin (g + 1) → ℤ) (rise : ℤ) (hrise : ∀ (a : Fin (g + 1)), rise = ↑(length a) * s a) (hsum : ∑ a : Fin (g + 1), s a = -↑k) : g < k

If every strand has the same nonzero integral rise and the left endpoint is one of the marks, the marked multiple is strictly larger than the genus. This is the slope form of paper Lemma 4.20.

theorem Bananas.endpoint_penultimate_slope_period_gt_genus {g k : ℕ} (hk : 0 < k) (distinguished : Fin (g + 1)) (length : Fin (g + 1) → ℕ) (hlen : ∀ (a : Fin (g + 1)), 0 < length a) (hdist : 2 ≤ length distinguished) (s : Fin (g + 1) → ℤ) (rise : ℤ) (hriseOther : ∀ (a : Fin (g + 1)), a ≠ distinguished → rise = ↑(length a) * s a) (hriseDist : rise = ↑(length distinguished) * s distinguished + ↑k) (hsum : ∑ a : Fin (g + 1), s a = -↑k) : g < k

Slope form of the endpoint/penultimate case (paper Lemma 4.23).

theorem Bananas.interior_torsion_rise_zero_or_period_ge_genus {g k : ℕ} (_hg : 1 ≤ g) (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hi : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α i) (hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B β j) (hαβ : α ≠ β) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) k) : ∃ (script : firingScript (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (rise : ℤ) (slope : Fin (g + 1) → ℤ), rise = script (rightEndpoint B) - script (leftEndpoint B) ∧ ∑ γ : Fin (g + 1), slope γ = 0 ∧ ↑(B.length α) * slope α = rise + ↑(B.length α - ↑i) * ↑k ∧ ↑(B.length β) * slope β = rise - ↑(B.length β - ↑j) * ↑k ∧ (∀ (γ : Fin (g + 1)), γ ≠ α → γ ≠ β → ↑(B.length γ) * slope γ = rise) ∧ (rise = 0 ∨ g ≤ k)

For two distinct interior marks, a nonzero endpoint rise already forces the torsion period to be at least the genus. This is the common sign argument behind all interior exceptional cases of Proposition 4.19.

theorem Bananas.fintype_sum_eq_two_of_zero_off {n : ℕ} (s : Fin n → ℤ) (a b : Fin n) (hab : a ≠ b) (hoff : ∀ (c : Fin n), c ≠ a → c ≠ b → s c = 0) : ∑ c : Fin n, s c = s a + s b

theorem Bananas.zero_rise_cross_oneOff_forces_both_length_two {g k : ℕ} (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hαβ : α ≠ β) (hi : ↑i = 1) (hj : ↑j + 1 = B.length β) (hiInt : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α i) (hjInt : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B β j) (hk : 0 < k) (slope : Fin (g + 1) → ℤ) (hsum : ∑ γ : Fin (g + 1), slope γ = 0) (hAlpha : ↑(B.length α) * slope α = ↑(B.length α - ↑i) * ↑k) (hBeta : ↑(B.length β) * slope β = -↑(B.length β - ↑j) * ↑k) (hOther : ∀ (γ : Fin (g + 1)), γ ≠ α → γ ≠ β → ↑(B.length γ) * slope γ = 0) : B.length α = 2 ∧ B.length β = 2

In the zero-rise near-opposite case, both marked strands have length two. This is the corrected zero-rise core of paper Lemma 4.27.

theorem Bananas.cross_oneOff_torsion_dichotomy {g k : ℕ} (hg : 1 ≤ g) (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hαβ : α ≠ β) (hiInt : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α i) (hjInt : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B β j) (hi : ↑i = 1) (hj : ↑j + 1 = B.length β) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) k) : CorrectedMidpointException B α β i j ∧ k = 2 ∨ g ≤ k

Corrected Lemma 4.27 for the near-opposite interior family.

theorem Bananas.isTorsionOrder_swap_marks {G : CFGraph} (u v : G.V) {k : ℕ} (hTO : IsTorsionOrder (mark G u v) k) : IsTorsionOrder (mark G v u) k

theorem Bananas.leftEndpoint_penultimate_torsionOrder_gt_genus {g k : ℕ} (B : Banana g) (β : Fin (g + 1)) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hjInt : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B β j) (hj : ↑j + 1 = B.length β) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B β j)) k) : g < k

Corrected Lemma 4.23: an endpoint and the penultimate point of a strand have torsion order strictly larger than the genus.

theorem Bananas.rightEndpoint_one_torsionOrder_gt_genus {g k : ℕ} (B : Banana g) (α : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (hiInt : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B α i) (hi : ↑i = 1) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (rightEndpoint B) (strandVertex B α i)) k) : g < k

Reflected endpoint/near-endpoint form of the preceding theorem.