Definitions specific to Section 6

The existing OnceMarkedBNExistence is the existence side of the once-marked Brill--Noether conjecture: every Young diagram of size at most the genus occurs. Section 6 instead uses the opposite, upper-census property: every Young diagram that occurs has size at most the genus. The paper calls that property a once-marked Brill--Noether general graph.

def Bananas.OnceMarkedBrillNoetherGeneral (G : CFGraph) (v : G.V) : Prop

Paper source: Definition 1.9, used throughout Section 6. (Definition 1.7 is the once-marked divisor census, OnceMarkedCensusContains, above.)

A once-marked graph is Brill--Noether general when every partition in its divisor census has size at most the genus. OnceMarkedCensusContains is an all-row, degree-independent encoding of membership in that census, so this is a literal formalization of the paper's definition rather than the differently directed OnceMarkedBNExistence predicate.

Equations

• Bananas.OnceMarkedBrillNoetherGeneral G v = ∀ (lambda : YoungDiagram), Utilities.OnceMarkedCensusContains G v lambda → ↑lambda.card ≤ G.genus

theorem Bananas.onceMarkedBrillNoetherGeneral_iff_normalized {G : CFGraph} (hconn : graphConnected G) (v : G.V) : OnceMarkedBrillNoetherGeneral G v ↔ ∀ (lambda : YoungDiagram), Utilities.OnceMarkedBNExists G v lambda → ↑lambda.card ≤ G.genus

On a connected graph the upper-census definition may equivalently use the finite normalized witness predicate. This is the form suited to the vertex wedge rank formula, while the definition above is the literal paper wording.