Reusable transmission API checks

This file is deliberately disjoint from Statements.lean. It records the mechanical consequences of the present contracts, and separates those from the geometric/non-recurrence input used by the evenly-marked theta theorem.

The present torsion contract is not an exact-order contract

Paper sources: def-EA / def-tauD and the exact-order implication lem:kgtImpliesTorsionOrder.

theorem Bananas.torsionWitness_of_dvd {M : TwiceMarked} {k m : ℕ} (hk : TorsionWitness M k) (hkm : k ∣ m) (hm : 0 < m) : TorsionWitness M m

A torsion witness propagates to every positive multiple of its period.

This is intentionally stated for the current TorsionWitness definition: it proves that the predicate records an annihilating period, not minimality.

theorem Bananas.torsionWitness_diagonal (G : CFGraph) (u : G.V) {k : ℕ} (hk : 0 < k) : TorsionWitness (mark G u u) k

In particular, the diagonal marking has a witness at every positive period. This exposes why distinctness and minimality cannot be inferred from TorsionWitness alone.

theorem Bananas.isTorsionOrder_iff_minimalWitness {M : TwiceMarked} {k : ℕ} : IsTorsionOrder M k ↔ TorsionWitness M k ∧ ∀ (m : ℕ), 0 < m → TorsionWitness M m → k ≤ m

IsTorsionOrder is the missing minimality wrapper around a witness.

Affine transmission consequences

theorem Bananas.kInversions_finite_of_torsionWitness_and_isKAffine {M : TwiceMarked} {k : ℕ} {τ : ℤ → ℤ} (hk : TorsionWitness M k) (hAffine : IsKAffine k τ) : (kInversions k τ).Finite

The finiteness conjunct in KGeneralTransmission is automatic once its positive witness and affine-period conjunct are available.

theorem Bananas.KGeneralTransmission.exists_affine_transmission {M : TwiceMarked} {k : ℕ} (hK : KGeneralTransmission M k) (D : CFDiv M.graph) : ∃ (τ : ℤ → ℤ), IsTransmissionPermutation M D τ ∧ IsKAffine k τ ∧ kInversionCount k τ ≤ M.graph.genus.toNat

Paper source: def-tauD and def-inv.

A KGeneralTransmission package contains, for every divisor, an affine transmission permutation with the expected inversion bound. The finite-set field is reconstructed from the other fields, so downstream APIs need not carry it as an independent hypothesis.

theorem Bananas.KGeneralTransmission_iff_without_finiteness {M : TwiceMarked} {k : ℕ} : KGeneralTransmission M k ↔ TorsionWitness M k ∧ AllSubmodular M ∧ ∀ (D : CFDiv M.graph), ∃ (τ : ℤ → ℤ), IsTransmissionPermutation M D τ ∧ IsKAffine k τ ∧ kInversionCount k τ ≤ M.graph.genus.toNat

Paper source: the contract used in def-EA and def-inv.

Equivalent presentation of the current KGeneralTransmission contract with the automatically generated finiteness conjunct omitted.

theorem Bananas.exists_affine_transmission_of_allSubmodular {M : TwiceMarked} (hconn : _root_.graphConnected M.graph) {k : ℕ} (hk : TorsionWitness M k) (hsub : AllSubmodular M) (D : CFDiv M.graph) : ∃ (τ : ℤ → ℤ), IsTransmissionPermutation M D τ ∧ IsKAffine k τ ∧ (kInversions k τ).Finite

On a connected graph, the converse affine construction is available for each submodular divisor from a torsion witness. This is the mechanical transmission step needed before any theta-specific inversion count.

Exact contract boundary

theorem Bananas.KGeneralTransmission.to_torsionWitness {M : TwiceMarked} {k : ℕ} : KGeneralTransmission M k → TorsionWitness M k

The current definition of KGeneralTransmission does not by itself expose an IsTorsionOrder result. This is a deliberately explicit boundary: the paper's exact-order lemma needs a separate proof using the rank/inversion count at D = 0, not a definitional simplification of this predicate.

Negative rank-difference obstruction

theorem Bananas.not_kGeneralTransmission_of_negative_rankDelta (M : TwiceMarked) (k : ℕ) (hNeg : ∃ (D : CFDiv M.graph), rankDelta M D < 0) : ¬KGeneralTransmission M k

A single negative marked second difference rules out k-general transmission, independently of the period and inversion-count clauses.