The affine-period bound for the same-strand one-off marking #
The three residue formulas of Lemma 4.23 force every positive affine period
to lie strictly beyond g + floor(g/(n-1)), the exact natural-number form of
the paper's rational cutoff (n/(n-1))g.
theorem
Bananas.oneOff_affine_period_gt_cutoff
{g k : ℕ}
(B : Banana g)
(alpha : Fin (g + 1))
(tau : ℤ → ℤ)
(hg : 2 ≤ g)
(hk : 0 < k)
(hLength : 1 < B.length alpha)
(hTau :
IsTransmissionPermutation
(mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B)
(strandVertex B alpha ⟨B.length alpha - 1, ⋯⟩))
(g • oneChip (rightEndpoint B)) tau)
(hAffine : IsKAffine k tau)
:
Lemma 4.23's period consequence, in exact integral form.
Bijectivity is not needed here: the forced transmission rows together with
k-affinity already exclude every positive k at or below the cutoff.