Bridging the banana transmission vocabulary to AspPerm

Bananas/ models a transmission permutation as a raw function ℤ → ℤ (IsTransmissionPermutation, IsKAffine, kInversions), because that is the shape the paper's Definition 2.11 writes down and the shape the inversion counting arguments use. Utilities models the same notion over the demazure dependency's AspPerm, via Utilities.SatisfiesTransmission (an inequality against the slipface τ.s).

This file supplies the adapter between those two formulations. Nothing here is banana-specific: it holds for any connected CFGraph with two marks.

What is proved

exists_aspPerm_rank_eq_of_isTransmissionPermutation is the substantive half. Given a raw transmission permutation τ for D, it produces the AspPerm σ with σ.func = τ and the equality

rank G (D + a • u - b • v) = σ.s (a + 1) b - 1

at every lattice point. TransmissionInequality is the ≥ weakening of this.

The degree normalization deg D = genus G + σ.χ, the other conjunct of SatisfiesTransmission, looks like an extra side condition but is automatic: AspPerm.s_eq at the origin gives χ(σ) = σ.s 0 0 - (σ⁻¹).s 0 0, the two counting lemmas of ThetaNonrecurrence identify those with rank (D - u) + 1 and rank (K - (D - u)) + 1, and Riemann-Roch turns the difference into deg (D - u) - g + 1 = deg D - g. So satisfiesTransmission_of_isTransmissionPermutation is unconditional and constructs a SatisfiesTransmission witness directly.

theorem Bananas.exists_aspPerm_rank_eq_of_isTransmissionPermutation {G : CFGraph} (u v : G.V) (hconn : _root_.graphConnected G) (D : CFDiv G) (τ : ℤ → ℤ) (hτ : IsTransmissionPermutation (mark G u v) D τ) : ∃ (σ : AspPerm), σ.func = τ ∧ ∀ (a b : ℤ), rank G (D + a • oneChip u - b • oneChip v) = σ.s.func (a + 1) b - 1

The AspPerm underlying a raw transmission permutation, together with the exact marked rank formula it computes.

This is the translation lemma between the two transmission formalisms. The AspPerm is the one whose slipface is the marked rank surface of D - u, and σ.s (a + 1) b is exactly rank (D + a·u - b·v) + 1.

theorem Bananas.satisfiesTransmissionOn_of_isTransmissionPermutation {G : CFGraph} (u v : G.V) (hconn : _root_.graphConnected G) (D : CFDiv G) (τ : ℤ → ℤ) (hτ : IsTransmissionPermutation (mark G u v) D τ) (S : Set (ℤ × ℤ)) : ∃ (σ : AspPerm), σ.func = τ ∧ Utilities.SatisfiesTransmissionOn G u v σ D S

Every raw transmission permutation yields the transmission inequalities of Utilities.Transmission for the corresponding AspPerm, on any test set.

Unlike satisfiesTransmission_of_isTransmissionPermutation this needs no degree hypothesis, because SatisfiesTransmissionOn carries none.

theorem Bananas.degree_eq_genus_add_chi_of_isTransmissionPermutation {G : CFGraph} (u v : G.V) (hconn : _root_.graphConnected G) (D : CFDiv G) (τ : ℤ → ℤ) (hτ : IsTransmissionPermutation (mark G u v) D τ) (σ : AspPerm) (hσFunc : σ.func = τ) : CFDiv.degree D = G.genus + σ.χ

The degree normalization is automatic.

SatisfiesTransmission requires deg D = g + χ(σ), which looks like an extra side condition. It is not: for the AspPerm attached to a transmission permutation of D it follows from Riemann-Roch. Evaluating AspPerm.s_eq at (0,0) gives χ(σ) = σ.s 0 0 - (σ⁻¹).s 0 0, and the two counting lemmas identify those with rank (D - u) + 1 and rank (K - (D - u)) + 1, so χ(σ) = rank (D - u) - rank (K - (D - u)) = deg (D - u) - g + 1 = deg D - g.

theorem Bananas.satisfiesTransmission_of_isTransmissionPermutation {G : CFGraph} (u v : G.V) (hconn : _root_.graphConnected G) (D : CFDiv G) (τ : ℤ → ℤ) (hτ : IsTransmissionPermutation (mark G u v) D τ) : ∃ (σ : AspPerm), σ.func = τ ∧ Utilities.SatisfiesTransmission G u v σ D

The full bridge, unconditionally: a raw transmission permutation for D gives an AspPerm satisfying Utilities.SatisfiesTransmission for D.

This gives a direct construction of a SatisfiesTransmission witness.

theorem Bananas.exists_aspPerm_satisfiesTransmission_of_allSubmodular {g k : ℕ} (B : Banana g) (u v : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V) (hk : TorsionWitness (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) u v) k) (hsub : AllSubmodular (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) u v)) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) : ∃ (σ : AspPerm), IsKAffine k σ.func ∧ Utilities.SatisfiesTransmission (Utilities.Certificate.SubdivisionGraph.Spec.graph B) u v σ D

Specialization to a banana graph: all-submodularity and a torsion witness already produce a raw transmission permutation for every divisor (exists_affine_transmission_of_allSubmodular), so they produce a full AspPerm-level transmission witness for every divisor too.

This is the form in which the Section 4 banana results — for instance evenlyMarkedTheta_kGeneral, whose KGeneralTransmission conclusion contains exactly this data — become usable by the AspPerm/wedge machinery.