The midpoint torsion bound

The revised paper lemma lem-midpointTorsion excludes every positive even period through 2g - 2, and hence every positive period below g, for a length-two midpoint paired with a non-midpoint on another strand.

We use the paper's quotient/remainder reduction and Dhar argument, via the existing reduced banana normal forms. Reducing at either endpoint also handles the reflected case without choosing an orientation. In fact the even-period argument only needs the first mark to be a midpoint, of any strand length.

theorem Bananas.midpoint_not_linearEquiv_even_multiple {g k : ℕ} (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hi : 2 * ↑i = B.length α) (hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B β j) (hmid : 2 * ↑j ≠ B.length β) (hk : 0 < k) (heven : Even k) (hbound : k ≤ 2 * g - 2) : ¬linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (↑k • oneChip (strandVertex B α i)) (↑k • oneChip (strandVertex B β j))

The even-period midpoint bound, including either side of the second strand's midpoint. The first marked strand need not have length two.

theorem Bananas.midpoint_not_linearEquiv_small_multiple {g k : ℕ} (B : Banana g) (α β : Fin (g + 1)) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hi : 2 * ↑i = B.length α) (hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B β j) (hmid : 2 * ↑j ≠ B.length β) (hk : 0 < k) (hbound : k < g) : ¬linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (↑k • oneChip (strandVertex B α i)) (↑k • oneChip (strandVertex B β j))

Doubling a putative period gives the second assertion of lem-midpointTorsion, without an evenness assumption.

theorem Bananas.length_two_cross_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) (hαLen : B.length α = 2) (hi : ↑i = 1) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) k) : CorrectedMidpointException B α β i j ∧ k = 2 ∨ g ≤ k

The length-two branch of Proposition 4.19, now deduced from the stronger midpoint lemma rather than initial-slope estimates.