Finite-length transmission existence

The transmission existence problem ranges over affine sign-preserving permutations with at most genus G inversions. Finiteness is a separate hypothesis: in Mathlib, Set.ncard is zero on an infinite set, so the bare inequality

(invSet tau).ncard <= genus G

does not express finite Coxeter length by itself.

The predicate in this file is the general two-marked existence condition. Its restriction to shifted Grassmannian permutations is exactly the once-marked Brill--Noether existence predicate.

def Utilities.FiniteTransmissionPerm (tau : AspPerm) : Prop

The inversion set of tau is finite. Keeping this named avoids the incorrect convention that Set.ncard alone detects finite ASP length.

Equations

• Utilities.FiniteTransmissionPerm tau = (invSet tau.func).Finite

def Utilities.TransmissionExistence (G : CFGraph) (u v : G.V) : Prop

Every finite-length ASP transmission problem allowed by the genus has a witness on the twice-marked graph (G,u,v).

Equations

• Utilities.TransmissionExistence G u v = ∀ (tau : AspPerm), Utilities.FiniteTransmissionPerm tau → ↑(invSet tau.func).ncard ≤ G.genus → Utilities.TransmissionExists G u v tau

def Utilities.TransmissionExistenceConjecture : Prop

The general transmission-existence conjecture for finite connected twice-marked graphs.

Equations

• Utilities.TransmissionExistenceConjecture = ∀ (G : CFGraph), graphConnected G → ∀ (u v : G.V), Utilities.TransmissionExistence G u v

theorem Utilities.finiteTransmissionPerm_shiftedGrassmannianPerm (lambda : YoungDiagram) (chi : ℤ) : FiniteTransmissionPerm (shiftedGrassmannianPerm lambda chi)

Every shifted Grassmannian permutation has finite transmission length.

theorem Utilities.grassmannianTransmissionExistence_of_transmissionExistence {G : CFGraph} {u v : G.V} (h : TransmissionExistence G u v) : GrassmannianTransmissionExistence G u v

General finite-length transmission existence contains the complete Grassmannian transmission family.

theorem Utilities.onceMarkedBNExistence_of_transmissionExistence {G : CFGraph} (hG : graphConnected G) (u v : G.V) (h : TransmissionExistence G u v) : OnceMarkedBNExistence G u

On a connected graph, the general twice-marked conjecture implies the once-marked Brill--Noether existence statement at its first mark.

Inversion and mark symmetry

theorem Utilities.inv_set_inverse_eq_revMap_image (tau : AspPerm) : invSet tau⁻¹.func = tau.revMap '' invSet tau.func

Reversing an inversion and applying tau to both entries identifies the inversion set of tau with that of its inverse.

theorem Utilities.revMap_injective (tau : AspPerm) : Function.Injective tau.revMap

The inversion-reversal map is injective.

theorem Utilities.ncard_inv_set_inverse (tau : AspPerm) : (invSet tau⁻¹.func).ncard = (invSet tau.func).ncard

ASP inversion preserves the inversion number, including the infinite case under Mathlib's Set.ncard convention.

theorem Utilities.finiteTransmissionPerm_inverse_iff (tau : AspPerm) : FiniteTransmissionPerm tau⁻¹ ↔ FiniteTransmissionPerm tau

Finite transmission length is invariant under ASP inversion.

theorem Utilities.transmissionExistence_swap_iff {G : CFGraph} (hG : graphConnected G) (u v : G.V) : TransmissionExistence G v u ↔ TransmissionExistence G u v

Riemann--Roch duality makes the fully quantified transmission-existence predicate symmetric in its two marked vertices.

Graph relabeling

theorem Utilities.CFGraphIso.transmissionExistence_map_iff {G : CFGraph} {H : CFGraph} (equivalence : CFGraphIso G H) (x y : G.V) : TransmissionExistence H (equivalence.vertexEquiv x) (equivalence.vertexEquiv y) ↔ TransmissionExistence G x y

Full finite-length transmission existence is invariant under relabeling the graph and both marked vertices.