Grassmannian transmission existence: the universal interface

GrassmannianTransmissionExistence and its equivalence with the once-marked Brill--Noether statement, rehomed from GrassmannianLowGenus.lean (which imports this file and keeps the genus-bounded consequences) so that the genus-generic transmission layer does not depend on the low-genus census.

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

Every shifted Grassmannian transmission problem allowed by the genus has a witness. The second mark is retained because it belongs to the transmission presentation, although the Grassmannian locus depends only on the first mark up to existence.

Equations

• One or more equations did not get rendered due to their size.

theorem Utilities.grassmannianTransmissionExistence_iff_onceMarkedBNExistence {G : CFGraph} (hG : graphConnected G) (u v : G.V) : GrassmannianTransmissionExistence G u v ↔ OnceMarkedBNExistence G u

The universal Grassmannian transmission statement is exactly the once-marked Brill--Noether statement.