Doubled-anchor rows for an explicit-potential certificate #

Two executable rows that a marked leaf needs and an unmarked one does not:

dominatesMarkCheck — the certificate's core divisor carries at least chips chips at a distinguished vertex, and nothing negative anywhere. This is W7 read at a mark.
multResidualCheck — the W5 residual table read with multiplicity mult at an anchor rather than with multiplicity one. multTargetCoefficient is the single arithmetic definition it needs, and it is targetCoefficient on the nose at mult = 1.

Both are allFin/decide Booleans over Fin n, so an emitter discharges them on concrete data and the kernel replays them. Each comes with the Prop it characterizes and an iff, so a consumer may use either form.

These lived in MarkedGraphs/Certificate/DegenerateDoubledAnchor.lean until 2026-08-31. Nothing about them is specific to a genus, a row, or a marked-graph existence statement, and the generic row-proof checker under Utilities/Subdivision/ClosedRowProof/ needs them to state its marked leaf checkers, so they belong on this side of the boundary. The soundness theorems that consume them — effective_degenerateDivisor_sub_smul_one_chip, class_mult_balance_nonnegative, winnable_sub_smul_one_chip_degenerateCoreVertex — stay private, where their only consumers are.

W7 at a mark: the divisor dominates, point-independently #

source

def Utilities.Certificate.ExplicitPotential.CertificateData.DominatesMark {m n p : ℕ} (certificate : CertificateData m n p) (mark : Fin n) (chips : ℤ) :

Prop

The checker's W7 domination row. The core divisor carries at least chips chips at mark and nothing negative anywhere else. Written as a single uniform inequality so that the Boolean form below is one allFin.

Equations

certificate.DominatesMark mark chips = ∀ (vertex : Fin n), 0 ≤ certificate.divisor vertex - if vertex = mark then chips else 0

Instances For

source

def Utilities.Certificate.ExplicitPotential.CertificateData.dominatesMarkCheck {m n p : ℕ} (certificate : CertificateData m n p) (mark : Fin n) (chips : ℤ) :

Bool

Executable form of DominatesMark, for an emitter to discharge by decide on concrete data.

Equations

certificate.dominatesMarkCheck mark chips = Utilities.Certificate.ExplicitPotential.allFin fun (vertex : Fin n) => decide (0 ≤ certificate.divisor vertex - if vertex = mark then chips else 0)

Instances For

source

@[simp]

theorem Utilities.Certificate.ExplicitPotential.CertificateData.dominatesMarkCheck_eq_true_iff {m n p : ℕ} (certificate : CertificateData m n p) (mark : Fin n) (chips : ℤ) :

certificate.dominatesMarkCheck mark chips = true ↔ certificate.DominatesMark mark chips

W5 at multiplicity `mult` #

source

def Utilities.Certificate.ExplicitPotential.CertificateData.multTargetCoefficient {m n p : ℕ} (certificate : CertificateData m n p) (mult : ℤ) (anchor vertex : Fin n) :

ℤ

The target coefficient at a core vertex after removing mult chips at the anchor. At mult = 1 this is targetCoefficient, syntactically.

Equations

certificate.multTargetCoefficient mult anchor vertex = certificate.divisor vertex - if vertex = anchor then mult else 0

Instances For

source

theorem Utilities.Certificate.ExplicitPotential.CertificateData.multTargetCoefficient_one {m n p : ℕ} (certificate : CertificateData m n p) (anchor vertex : Fin n) :

certificate.multTargetCoefficient 1 anchor vertex = certificate.targetCoefficient anchor vertex

source

def Utilities.Certificate.ExplicitPotential.CertificateData.MultResidual {m n p : ℕ} (certificate : CertificateData m n p) (mult : ℤ) (anchor : Fin n) :

Prop

The checker's W5 with mult in place of 1. This is the whole semantic content of the (comp x …) plan: everything else — the slack discipline, the potential, the endpoint bookkeeping — is shared verbatim with the n rank anchors.

Equations

certificate.MultResidual mult anchor = ∀ (vertex : Fin n), 0 ≤ certificate.multTargetCoefficient mult anchor vertex + certificate.lowerEndpointContribution anchor vertex