Kernel-checked rank-one certificates

This module is the small handwritten soundness layer for externally generated rank-one witnesses on a fixed finite graph. A certificate contains only passive data:

• a divisor D; and
• for every vertex q, an integer firing script which makes D - q effective.

The Boolean checker evaluates degrees, Laplacians, and pointwise inequalities inside Lean. The soundness theorem then turns a successful check into BNExists G 1 d. Consequently a C (or other) program may search for and emit the data, but it is not part of the trusted proof.

Our script convention agrees with ChipFiringWithLean.prin: the checked residual is D - q + prin G sigma, equivalently D - q - L sigma.

theorem Utilities.Certificate.effective_degree_one_eq_one_chip {G : CFGraph} {E : CFDiv G} (hEffective : effective E) (hDegree : CFDiv.degree E = 1) : ∃ (q : G.V), E = oneChip q

An effective degree-one divisor consists of a single chip at one vertex.

structure Utilities.Certificate.RankOne (G : CFGraph) : Type u_1

Passive certificate data for a rank-one divisor on a fixed graph.

• divisor : CFDiv G

  The proposed divisor whose rank is to be certified as at least one.

• scripts : G.V → firingScript G

  The proposed firing script for each removed-chip vertex; residual effectivity is checked by ValidAt.

def Utilities.Certificate.RankOne.residual {G : CFGraph} (certificate : RankOne G) (q : G.V) : CFDiv G

The result of removing the chip at q and applying its certificate script.

Equations

• certificate.residual q = certificate.divisor - oneChip q + (prin G) (certificate.scripts q)

def Utilities.Certificate.RankOne.ValidAt {G : CFGraph} (certificate : RankOne G) (q : G.V) : Prop

Propositional validity at one vertex.

Equations

• certificate.ValidAt q = effective (certificate.residual q)

def Utilities.Certificate.RankOne.Valid {G : CFGraph} (certificate : RankOne G) (d : ℤ) : Prop

A rank-one certificate with the requested divisor degree.

Equations

• certificate.Valid d = (CFDiv.degree certificate.divisor = d ∧ ∀ (q : G.V), certificate.ValidAt q)

def Utilities.Certificate.RankOne.checkEffective {G : CFGraph} (D : CFDiv G) : Bool

Executable pointwise effectivity test.

Equations

• Utilities.Certificate.RankOne.checkEffective D = decide (∀ (v : G.V), 0 ≤ D v)

def Utilities.Certificate.RankOne.checkAt {G : CFGraph} (certificate : RankOne G) (q : G.V) : Bool

Executable check of the script associated to one removed chip.

Equations

• certificate.checkAt q = Utilities.Certificate.RankOne.checkEffective (certificate.residual q)

def Utilities.Certificate.RankOne.check {G : CFGraph} (certificate : RankOne G) (d : ℤ) : Bool

Executable check of the degree and every vertex script.

Equations

• certificate.check d = (decide (CFDiv.degree certificate.divisor = d) && decide (∀ (q : G.V), certificate.checkAt q = true))

@[simp]

theorem Utilities.Certificate.RankOne.checkEffective_eq_true_iff {G : CFGraph} (D : CFDiv G) : checkEffective D = true ↔ effective D

@[simp]

theorem Utilities.Certificate.RankOne.checkAt_eq_true_iff {G : CFGraph} (certificate : RankOne G) (q : G.V) : certificate.checkAt q = true ↔ certificate.ValidAt q

@[simp]

theorem Utilities.Certificate.RankOne.check_eq_true_iff {G : CFGraph} (certificate : RankOne G) (d : ℤ) : certificate.check d = true ↔ certificate.Valid d

theorem Utilities.Certificate.RankOne.sub_one_chip_linear_equiv_residual {G : CFGraph} (certificate : RankOne G) (q : G.V) : linearEquiv G (certificate.divisor - oneChip q) (certificate.residual q)

A certificate script supplies an explicit linear equivalence from D - q to its residual.

theorem Utilities.Certificate.RankOne.winnable_sub_one_chip_of_validAt {G : CFGraph} (certificate : RankOne G) (q : G.V) (hValid : certificate.ValidAt q) : winnable G (certificate.divisor - oneChip q)

Soundness at one vertex: a checked effective residual makes D - q winnable.

theorem Utilities.Certificate.RankOne.rank_ge_one_of_valid {G : CFGraph} (certificate : RankOne G) {d : ℤ} (hValid : certificate.Valid d) : rank G certificate.divisor ≥ 1

The mathematical soundness theorem for the passive certificate object.

theorem Utilities.Certificate.RankOne.bnExists_of_valid {G : CFGraph} (certificate : RankOne G) (d : ℤ) (hValid : certificate.Valid d) : BNExists G 1 d

A propositionally valid certificate is already a rank-one Brill--Noether witness.

theorem Utilities.Certificate.RankOne.bnExists_of_check_eq_true {G : CFGraph} (certificate : RankOne G) (d : ℤ) (hCheck : certificate.check d = true) : BNExists G 1 d

A successful Boolean check yields a kernel-checked Brill--Noether rank-one existence theorem.