Orientation divisors and rank one

ordiv G O = indeg_O - 1 has degree g - 1, so the orientation model is a natural setting for the critical pencil (1, g-1).

legal_of_ordiv_iff characterizes the legal firing sets of an orientation divisor. The main sufficient criterion, rank_ge_one_of_inHeavyReachable, says that ordiv G O has rank at least one when its class contains, for each vertex q, a source-free orientation with 2 ≤ indeg q. By gioan_reversalEquiv_of_linear_equiv, this hypothesis can also be expressed as reachability in the cycle--cocycle reversal system.

Source-free orientations: the floor

def Utilities.Gonality.SourceFree {G : CFGraph} (O : CFOrientation G) : Prop

O has no source: every vertex receives at least one edge.

Equations

• Utilities.Gonality.SourceFree O = ∀ (v : G.V), 1 ≤ indeg G O v

def Utilities.Gonality.InHeavyAt {G : CFGraph} (O : CFOrientation G) (q : G.V) : Prop

O is in-heavy at q: source-free, and q receives at least two edges. This is exactly the condition making ordiv G O - oneChip q effective.

Equations

• Utilities.Gonality.InHeavyAt O q = (Utilities.Gonality.SourceFree O ∧ 2 ≤ indeg G O q)

theorem Utilities.Gonality.InHeavyAt.sourceFree {G : CFGraph} {O : CFOrientation G} {q : G.V} (h : InHeavyAt O q) : SourceFree O

theorem Utilities.Gonality.effective_ordiv_of_sourceFree {G : CFGraph} {O : CFOrientation G} (h : SourceFree O) : effective (ordiv G O)

A source-free orientation has an effective divisor.

theorem Utilities.Gonality.winnable_ordiv_of_sourceFree {G : CFGraph} {O : CFOrientation G} (h : SourceFree O) : winnable G (ordiv G O)

rank (ordiv G O) ≥ 0 for a source-free orientation.

theorem Utilities.Gonality.effective_ordiv_sub_one_chip_of_inHeavyAt {G : CFGraph} {O : CFOrientation G} {q : G.V} (h : InHeavyAt O q) : effective (ordiv G O - oneChip q)

In-heaviness at q is exactly effectivity of ordiv G O - oneChip q.

The surviving statement: in-heavy reachability certifies rank one

theorem Utilities.Gonality.rank_ge_one_of_inHeavyReachable {G : CFGraph} (O : CFOrientation G) (h : ∀ (q : G.V), ∃ (O' : CFOrientation G), linearEquiv G (ordiv G O) (ordiv G O') ∧ InHeavyAt O' q) : rank G (ordiv G O) ≥ 1

In-heavy reachability certifies rank one. If the divisor class of ordiv G O contains, for every vertex q, an orientation divisor that is source-free and in-heavy at q, then rank G (ordiv G O) ≥ 1.

By gioan_reversalEquiv_of_linear_equiv the hypothesis is equivalent to reachability of such an orientation from O in the cycle–cocycle reversal system, which is the form the distillation note states. The converse fails — see the module docstring.

theorem Utilities.Gonality.rank_ge_one_of_inHeavyReachable' {G : CFGraph} (O : CFOrientation G) (h : ∀ (q : G.V), ∃ (O' : CFOrientation G), linearEquiv G (ordiv G O) (ordiv G O') ∧ SourceFree O' ∧ 2 ≤ indeg G O' q) : rank G (ordiv G O) ≥ 1

The same statement with the reachability hypothesis phrased through the reversal system, using Gioan's theorem in the direction already proved in Utilities/Foundations/OrientationReversal.lean.

Why strong connectivity is an obstruction

Dhar's fire on ordiv G O reads only the induced subdigraph on the unburnt set.

def Utilities.Gonality.arcsWithin {G : CFGraph} (O : CFOrientation G) (U : Finset G.V) : ℕ

The arcs of O with both ends in U, counted at their heads.

Equations

• Utilities.Gonality.arcsWithin O U = ∑ u ∈ U, ∑ w ∈ U, flow O w u

def Utilities.Gonality.arcsOut {G : CFGraph} (O : CFOrientation G) (U : Finset G.V) : ℕ

The arcs of O leaving U.

Equations

• Utilities.Gonality.arcsOut O U = ∑ u ∈ U, ∑ w ∈ Uᶜ, flow O u w

theorem Utilities.Gonality.legal_of_ordiv_iff {G : CFGraph} (O : CFOrientation G) (U : Finset G.V) (u : G.V) : outdegreeSet G U u ≤ ordiv G O u ↔ ∑ w ∈ Uᶜ, flow O u w + 1 ≤ ∑ w ∈ U, flow O w u

Legality for an orientation divisor is intrinsic to the induced subdigraph.

u ∈ U can pay its whole boundary out of ordiv G O exactly when it receives strictly more arcs from inside U than it sends outside U. The arcs entering u from outside U cancel: they are counted once by indeg and once by outdegreeSet.

The characterization is expressed entirely in terms of arc counts inside and across the boundary of U.

theorem Utilities.Gonality.card_add_arcsOut_le_arcsWithin_of_legal {G : CFGraph} (O : CFOrientation G) (U : Finset G.V) (h : ∀ u ∈ U, outdegreeSet G U u ≤ ordiv G O u) : U.card + arcsOut O U ≤ arcsWithin O U

The counting corollary. A set that Dhar's fire fails to burn must induce a subdigraph with at least |U| + (arcs leaving U) internal arcs.

For a strongly connected O every proper nonempty U has 1 ≤ arcsOut O U, so every legal set induces a subgraph with strictly more edges than vertices — first Betti number at least two once the boundary is counted. On sparse graphs (cubic cores, say) such sets are rare, ordiv G O is already q-reduced at the in-degree-one vertices, and the rank is zero. That is the whole failure.

theorem Utilities.Gonality.not_legal_of_arcsWithin_lt {G : CFGraph} (O : CFOrientation G) (U : Finset G.V) (h : arcsWithin O U < U.card + arcsOut O U) : ¬∀ u ∈ U, outdegreeSet G U u ≤ ordiv G O u

The contrapositive, in the form the failure analysis uses: a set too sparse inside, or leaking too many arcs, cannot be unburnt.