A linear non-existence certificate for positive rank #

Every gonality upper bound in this repository is witnessed by a divisor and a firing script. This module supplies the missing other half: a small, checkable witness that a given divisor does not have positive rank.

The obstacle is that qReduced (in the chip-firing dependency) quantifies over all subsets of V \ {q}, so deciding it directly costs 2^{n-1}. A burning order replaces that quantifier by an n-step linear check:

a list π = (q = u₀, u₁, …) containing every vertex, in which every entry after the first satisfies D(uⱼ) < Σ_{i<j} numEdges G uⱼ uᵢ.

Soundness (qReduced_of_burningOrder): given a nonempty S ⊆ V \ {q}, the least index j with uⱼ ∈ S has all its predecessors outside S, so the displayed inequality already exhibits a vertex of S that cannot afford to fire. The order is exactly a run of Dhar's burning algorithm recorded as data, but nothing about the algorithm — termination, maximality, or otherwise — is needed to check it.

The full certificate refuting rank G D ≥ 1 is the triple (v, x, π):

a vertex v;
a firing script x carrying D to D' := D + prin G x;
a burning order π for (D', v);

together with D' ≥ 0 off v and D' v ≤ 0 (not_rank_ge_one_of_burningOrder). Every component is decide-shaped: BurningOrder quantifies over Fin π.length and G.V, both finite.

Burning orders #

source

def Utilities.Gonality.BurningOrder (G : CFGraph) (D : CFDiv G) (v : G.V) (order : List G.V) :

Prop

A burning order for (D, v): a list of vertices whose head is v, containing every vertex, in which every entry after the first has strictly fewer chips than it has edges to its predecessors.

Repetitions are harmless; only the first occurrence of each vertex matters to the soundness proof.

Equations

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

Instances For

source

@[instance_reducible]

instance Utilities.Gonality.instDecidableBurningOrder {G : CFGraph} (D : CFDiv G) (v : G.V) (order : List G.V) :

Decidable (BurningOrder G D v order)

Equations

Utilities.Gonality.instDecidableBurningOrder D v order = id inferInstance

source

theorem Utilities.Gonality.qReduced_of_burningOrder {G : CFGraph} {D : CFDiv G} {v : G.V} {order : List G.V} (hEff : qEffective v D) (h : BurningOrder G D v order) :

qReduced G v D

Soundness of a burning order. It certifies q-reducedness, replacing the 2^{n-1} subset quantifier of qReduced by an n-step check.

The non-existence certificate #

source

theorem Utilities.Gonality.not_rank_ge_one_of_burningOrder {G : CFGraph} {D : CFDiv G} {v : G.V} {x : firingScript G} {order : List G.V} (hEff : qEffective v (D + (prin G) x)) (hOrder : BurningOrder G (D + (prin G) x) v order) (hzero : (D + (prin G) x) v ≤ 0) :

¬rank G D ≥ 1

The certificate refuting positive rank. A vertex v, a script x, and a burning order for D + prin G x at v whose divisor is effective off v and carries no chip at v.

The proof is two lines of divisor bookkeeping on top of qReduced_of_burningOrder: linear equivalence preserves rank, and a q-reduced divisor of positive rank carries a chip at q (one_le_apply_of_q_reduced_of_rank_geq_one).

source

structure Utilities.Gonality.RankZeroCertificate (G : CFGraph) (D : CFDiv G) :

Type u_1

Packaged form: the data of a certificate, bundled so that a generated table can carry one row per divisor.

vertex : G.V
The base point of the reduction.
script : firingScript G
The firing script carrying D to its vertex-reduced representative.
order : List G.V
A burning order recording a run of Dhar's algorithm as data.