Mechanical API audit for two remaining statement targets

This file is intentionally disjoint from Statements.lean and the shared library. It records the strongest reductions available from the current API; the remaining hypotheses are the graph-specific arithmetic/counting lemmas.

Evenly marked theta: the generic transmission reduction

theorem Bananas.evenlyMarkedTheta_kGeneral_of_torsion_and_count (B : Banana 2) (α β : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (k : ℕ) (hEven : EvenlyMarkedTheta B α β i j) (hk : TorsionWitness (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) k) (hCount : ∀ (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)), ∃ (τ : ℤ → ℤ), IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) D τ ∧ IsKAffine k τ ∧ kInversionCount k τ ≤ (Utilities.Certificate.SubdivisionGraph.Spec.graph B).genus.toNat) : KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) k

The generic API can also discharge the per-divisor existence/finiteness part from torsion and submodularity, but not the genus inversion bound.

theorem Bananas.evenlyMarkedTheta_affine_existence_audit (B : Banana 2) (α β : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (k : ℕ) (hEven : EvenlyMarkedTheta B α β i j) (hk : TorsionWitness (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) k) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : ∃ (τ : ℤ → ℤ), IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α i) (strandVertex B β j)) D τ ∧ IsKAffine k τ ∧ (kInversions k τ).Finite

Cross one-off: what the generic APIs actually yield

theorem Bananas.cross_oneOff_affine_existence_audit {g k : ℕ} (_hg : 3 ≤ g) (B : Banana g) (α β : Fin (g + 1)) (_hαβ : α ≠ β) (hα : 1 < B.length α) (hβ : 1 < B.length β) (hsub : AllSubmodular (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α ⟨1, ⋯⟩) (strandVertex B β ⟨B.length β - 1, ⋯⟩))) (hk : TorsionWitness (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α ⟨1, ⋯⟩) (strandVertex B β ⟨B.length β - 1, ⋯⟩)) k) (E : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : ∃ (τ : ℤ → ℤ), IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α ⟨1, ⋯⟩) (strandVertex B β ⟨B.length β - 1, ⋯⟩)) E τ ∧ IsKAffine k τ ∧ (kInversions k τ).Finite

This is the exact missing strengthening for the both-off target (cor-bothOffMax, Corollary 4.31): the current API supplies the preceding theorem, but no way to choose a divisor E or to prove the displayed lower bound for its permutation. Concretely, what is missing is a proof of

∃ (E : CFDiv B.graph) (τ : ℤ → ℤ),
  IsTransmissionPermutation (mark B.graph u v) E τ ∧ IsKAffine k τ ∧
  Nat.choose g 2 + g / (B.length β - 1) ≤ kInversionCount k τ

for u = v_{α,1}, v = v_{β,n_β-1}. This was previously recorded as a theorem taking that statement as a hypothesis and returning it unchanged (P → P), which asserts nothing; it is stated here as a comment instead.