Corrected high-genus midpoint exceptions

The paper states the order-two exception in Proposition 4.19 and Corollary 6.4 with both supporting strands of length two. The corrected all-submodularity classification shows that this is too restrictive. If one mark is the midpoint of a length-two strand, it may be paired with any interior point of a distinct strand. When that second point is itself a midpoint (so its strand merely has even length), both points double to the endpoint pencil. The marked graph therefore has exact torsion order two and has 2-general transmission.

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

The corrected exceptional family in Proposition 4.19 and Corollary 6.4: the marks lie at midpoints of distinct strands, and at least one of the two strands has length two.

Equations

• Bananas.CorrectedMidpointException B α β i j = (α ≠ β ∧ 2 * ↑i = B.length α ∧ 2 * ↑j = B.length β ∧ (B.length α = 2 ∨ B.length β = 2))

theorem Bananas.correctedMidpointException_torsionOrder_two {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (h : CorrectedMidpointException B α β i j) : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) 2

Exact torsion order for the corrected exceptional family.

theorem Bananas.correctedMidpointException_allSubmodular {g : ℕ} (hg : 3 ≤ g) (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (h : CorrectedMidpointException B α β i j) : AllSubmodular (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j))

Every divisor is submodular for the corrected exceptional family.

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

Corrected positive half of Corollary 6.4: every exceptional midpoint marking has 2-general transmission.