The Section 6 large-period banana obstruction

The corrected Proposition 4.19 torsion dichotomy combines here with the Section 6 Brill--Noether obstruction: a k-general transmission marking on a high-genus banana cannot have k ≥ g, since Proposition 6.1 would make the underlying banana Brill--Noether general.

theorem Bananas.kGeneralTransmission_implies_nsmForBananaException {g k : ℕ} (hg : 3 ≤ g) (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hK : KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) k) : NSMForBananaException B (strandVertex B α i) (strandVertex B β j)

Theorem 3.9 reduces every high-genus banana marking with general transmission to one of its corrected endpoint-aware exceptional families.

theorem Bananas.banana_not_kGeneralTransmission_of_genus_le_period {g k : ℕ} (hg : 3 ≤ g) (B : Banana g) (u v : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V) (hkg : g ≤ k) : ¬KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) u v) k

The Proposition 6.1 branch in Corollary 6.4 (cor:bananasWithKGT).

For a banana of genus at least three, any general-transmission period at least the genus contradicts the degree-two endpoint pencil. Thus the unformalized Proposition 4.19 dichotomy only needs to rule out its remaining order-two exceptional alternatives.

def Bananas.CorrectedBananaTorsionDichotomy {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) : Prop

The corrected Section 4 input required by Corollary 6.4. This is Proposition 4.19 with its published two-length-two exception replaced by the larger CorrectedMidpointException family.

Equations

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

theorem Bananas.corrected_banana_kGeneral_iff_of_torsionDichotomy {g k : ℕ} (hg : 3 ≤ g) (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hDichotomy : CorrectedBananaTorsionDichotomy B α β i j) : KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) k ↔ CorrectedMidpointException B α β i j ∧ k = 2

Corrected Corollary 6.4, parameterized by its Proposition 4.19 input. The following theorem supplies that input unconditionally.

theorem Bananas.corrected_banana_kGeneral_iff {g k : ℕ} (hg : 3 ≤ g) (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) : KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) k ↔ CorrectedMidpointException B α β i j ∧ k = 2

Corrected Corollary 6.4: a high-genus banana has k-general transmission exactly for the distinct-strand midpoint family with at least one length-two strand, and then exactly at period two.