Explicit quadratic inversion growth on bananas

This gives the precise formal reading of the quantity M in Theorem 4.18: there is a divisor whose affine transmission permutation has at least the displayed number of normalized inversion classes. The paper leaves "sufficiently long" informal; the three theorems below retain the actual verified length hypotheses for its endpoint, one-off, and cross-one-off families.

def Bananas.HasInversionLowerBound (M : TwiceMarked) (k q : ℕ) : Prop

A marked graph has a transmission permutation with at least q normalized k-inversion classes. This is the existential lower-bound form of the paper's maximum M.

Equations

• One or more equations did not get rendered due to their size.

theorem Bananas.endpoint_has_quadratic_inversion_lower_bound {g k : ℕ} (B : Banana g) (hSub : AllSubmodular (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (rightEndpoint B))) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (rightEndpoint B)) k) : HasInversionLowerBound (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (rightEndpoint B)) k ((g + 1).choose 2)

Endpoint branch of Theorem 4.18 / Proposition 4.21.

theorem Bananas.oneOff_has_quadratic_inversion_lower_bound {g k : ℕ} (B : Banana g) (alpha : Fin (g + 1)) (hg : 2 ≤ g) (hLength : 1 < B.length alpha) (hSub : AllSubmodular (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩))) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) k) : HasInversionLowerBound (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩)) k (g.choose 2 + g / (B.length alpha - 1))

Same-strand one-off branch of Theorem 4.18 / Proposition 4.25.

theorem Bananas.crossOneOff_has_quadratic_inversion_lower_bound {g k : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (hg : 3 ≤ g) (hab : alpha ≠ beta) (hAlpha : 1 < B.length alpha) (hBetaLong : g + 1 ≤ B.length beta) (hLong : CrossOneOffLongEnough g (B.length alpha) (B.length beta)) (hSub : AllSubmodular (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩))) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) k) : HasInversionLowerBound (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) k (correctedCrossOneOffForcedCount g (B.length beta))

Cross-one-off branch of Theorem 4.18 / corrected Corollary 4.31. The long-second-strand hypothesis supplies the period separation that the published proof left implicit.

theorem Bananas.crossOneOff_has_quadratic_inversion_lower_bound_of_not_both_two {g k : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (hg : 3 ≤ g) (hab : alpha ≠ beta) (hAlpha : 1 < B.length alpha) (hBeta : 1 < B.length beta) (hLong : CrossOneOffLongEnough g (B.length alpha) (B.length beta)) (hSub : AllSubmodular (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩))) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) k) : HasInversionLowerBound (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) k (correctedCrossOneOffForcedCount g (B.length beta))

Cross-one-off branch of Theorem 4.18 / corrected Corollary 4.31, with no hypothesis relating the two marked strand lengths: CrossOneOffLongEnough already forces B.length alpha ≥ g + 1 ≥ 4 > 2, so the period-separation premise is now supplied unconditionally by crossOneOff_cutoff_le_torsionOrder_of_not_both_two (Bananas/CrossOneOffShortStrandPeriod.lean) in place of the long-second-strand hypothesis hBetaLong.