Period separation for the corrected cross-one-off block #
The existing torsion dichotomy records only g ≤ k, but its nonzero-rise
argument actually proves the strict inequality g < k. In the long-second-
strand regime the zero-rise exception is impossible. Since then
crossOneOffCutoff g n ≤ g+1, this supplies exactly the separation needed
by the corrected finite-row inversion count.
theorem
Bananas.crossOneOff_torsionOrder_gt_genus_of_second_long
{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)
(hTO :
IsTorsionOrder
(mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩)
(strandVertex B beta ⟨B.length beta - 1, ⋯⟩))
k)
:
A cross-one-off exact torsion order is strictly larger than the genus
when the second strand has length at least g+1.
theorem
Bananas.crossOneOff_cutoff_le_torsionOrder
{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)
(hTO :
IsTorsionOrder
(mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩)
(strandVertex B beta ⟨B.length beta - 1, ⋯⟩))
k)
:
The exact torsion order separates the whole corrected row cutoff from the affine period.
theorem
Bananas.crossOneOff_kGeneral_cutoff_le_period
{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)
(hK :
KGeneralTransmission
(mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩)
(strandVertex B beta ⟨B.length beta - 1, ⋯⟩))
k)
:
In particular, a k-general cross-one-off marking supplies the missing
period-separation premise in corrected Corollary 4.31.