Bounded mechanical audit: evenly marked theta transmission

This file is intentionally disjoint from Statements.lean and all shared helpers. It records only reductions that compile from the current API. In particular, it is not an attempted proof of the theorem-level gaps.

Exact names exposed by the current library

The following declarations are the complete generic route from a torsion witness and all-submodularity to affine transmission and finite inversion support. Exact torsion for evenly marked theta graphs is now supplied by ThetaExactTorsionRelabel; the generic API supplies no inversion-count bound.

The audit's point is that these API entry points exist with these shapes. Stated as anonymous examples rather than #checks: both are compile-time checks, but #check prints an info on every build.

Period-two reductions that are available mechanically

theorem Bananas.period_two_first_coordinate {τ : ℤ → ℤ} {p : ℤ × ℤ} (hp : p ∈ kInversions 2 τ) : p.1 = 0 ∨ p.1 = 1

theorem Bananas.period_two_value_decomposition {τ : ℤ → ℤ} (hτ : IsKAffine 2 τ) (y : ℤ) : τ y = τ (y % 2) + y / 2 * 2

theorem Bananas.period_two_inversion_finiteness {M : TwiceMarked} {τ : ℤ → ℤ} (hk : TorsionWitness M 2) (hτ : IsKAffine 2 τ) : (kInversions 2 τ).Finite

Reduction of the evenly-marked theorem to the count inequality

Torsion, all-submodularity, existence of an affine transmission permutation, and finiteness of its inversion set are already unconditional. Thus the only theta-specific input still needed is a bound for any affine transmission permutation produced by the generic API.

theorem Bananas.evenlyMarkedTheta_kGeneral_of_uniform_inversion_bound (B : Banana 2) (α β : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hEven : EvenlyMarkedTheta B α β i j) (hBound : ∀ (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (τ : ℤ → ℤ), IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) D τ → IsKAffine (B.length α / (B.length α).gcd ↑i) τ → kInversionCount (B.length α / (B.length α).gcd ↑i) τ ≤ (Utilities.Certificate.SubdivisionGraph.Spec.graph B).genus.toNat) : KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) (B.length α / (B.length α).gcd ↑i)

A witness at period two mechanically propagates to period four; this is why an exact-order proof must establish minimality separately.

theorem Bananas.period_two_witness_propagates {M : TwiceMarked} (hk : TorsionWitness M 2) : TorsionWitness M 4

The remaining theta-specific ingredient is a genus-sized bound on kInversionCount k τ for every affine transmission permutation. The exact torsion witness and its minimality are proved in ThetaExactTorsionRelabel; all-submodularity and affine-transmission existence are already generic.

The paper obtains this bound through its genus-two inversion formula (Lemma 4.10) and nonrecurrence. Neither has yet been formalized in the current API.