Explicit-potential local subdivision certificates

This module defines a local arithmetic checker for rank-one subdivision certificates. It deliberately avoids shortest-path and negative-cycle reasoning. A certificate supplies, for every rank-one anchor, one integral linear potential on the expanded core. The displayed cone contains the endpoint inequalities for those potentials literally.

The Boolean checker verifies only exact integer data:

• expanded edges are loopless;
• the proposed divisor has the advertised degree;
• endpoint slope bounds are compatible and make every core residual nonnegative; and
• every positivity/bound form needed by the semantics is either the zero form or occurs in the displayed cone.

The theorems below turn an accepted record and a point in its cone into the positive segment lengths, endpoint slope inequalities, nonnegative core balances, and nonnegative interior second differences needed to assemble an actual firing script on a subdivision graph. The graph-construction layer is kept separate so that this file remains a small arithmetic trust boundary.

@[reducible, inline]

abbrev Utilities.Certificate.ExplicitPotential.AffineForm (m : ℕ) : Type

Local shorthand for the affine-cover arithmetic type.

Equations

• Utilities.Certificate.ExplicitPotential.AffineForm m = Utilities.Certificate.AffineCover.AffineForm m

@[reducible, inline]

abbrev Utilities.Certificate.ExplicitPotential.FormsHold {m : ℕ} (forms : List (AffineCover.AffineForm m)) (point : Fin m → ℤ) : Prop

Local shorthand for conjunctions of affine-cover rows.

Equations

• Utilities.Certificate.ExplicitPotential.FormsHold = Utilities.Certificate.AffineCover.FormsHold

def Utilities.Certificate.ExplicitPotential.allFin {k : ℕ} (test : Fin k → Bool) : Bool

Executable universal quantification over a finite index type.

Equations

• Utilities.Certificate.ExplicitPotential.allFin test = Utilities.Certificate.AffineCover.allFin test

@[simp]

theorem Utilities.Certificate.ExplicitPotential.allFin_eq_true_iff {k : ℕ} (test : Fin k → Bool) : allFin test = true ↔ ∀ (index : Fin k), test index = true

structure Utilities.Certificate.ExplicitPotential.Core (n p : ℕ) : Type

A finite loopless expanded core, with p ordered edge copies.

• tail : Fin p → Fin n

  The tail vertex of each ordered core edge occurrence.

• head : Fin p → Fin n

  The head vertex of each ordered core edge occurrence.

structure Utilities.Certificate.ExplicitPotential.AnchorWitness (m n p : ℕ) : Type

Endpoint slopes and a core potential for one removed-chip test.

• alpha : Fin p → ℤ

  The integer tail-end slope contribution on each slot, used in the lower bound on the potential rise.

• beta : Fin p → ℤ

  The integer head-end slope contribution on each slot, whose negative bounds the potential rise from above.

• potential : Fin n → AffineForm m

  The affine potential value at each core vertex for this removed-chip test.

structure Utilities.Certificate.ExplicitPotential.CertificateData (m n p : ℕ) : Type

Passive local data for a rank-one divisor over one length cone.

• core : Core n p

  The ordered core incidence data underlying the local certificate.

• segment : Fin p → AffineForm m

  The affine length expression assigned to each core slot.

• divisor : Fin n → ℤ

  The proposed integer chip weight at each core vertex.

• witness : Fin n → AnchorWitness m n p

  The endpoint-slope and affine-potential witness for removing a chip at each anchor vertex.

• cone : List (AffineForm m)

  The affine inequalities defining the local length region; validity of the proposed witnesses on this region is checked separately.

def Utilities.Certificate.ExplicitPotential.AffineForm.scale {m : ℕ} (scalar : ℤ) (form : AffineForm m) : AffineForm m

Integral scalar multiplication, kept explicit to make the generated data grammar independent of typeclass inference.

Equations

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

def Utilities.Certificate.ExplicitPotential.AffineForm.sub {m : ℕ} (left right : AffineForm m) : AffineForm m

Difference of two integral affine forms.

Equations

• left.sub right = { fixedValue := left.fixedValue - right.fixedValue, coefficient := fun (coordinate : Fin m) => left.coefficient coordinate - right.coefficient coordinate }

def Utilities.Certificate.ExplicitPotential.AffineForm.positive {m : ℕ} (form : AffineForm m) : AffineForm m

The strict-integral positivity row form(point) - 1 >= 0.

Equations

• form.positive = { fixedValue := form.fixedValue - 1, coefficient := form.coefficient }

@[simp]

theorem Utilities.Certificate.ExplicitPotential.AffineForm.eval_scale {m : ℕ} (scalar : ℤ) (form : AffineForm m) (point : Fin m → ℤ) : AffineCover.AffineForm.eval (scale scalar form) point = scalar * AffineCover.AffineForm.eval form point

@[simp]

theorem Utilities.Certificate.ExplicitPotential.AffineForm.eval_sub {m : ℕ} (left right : AffineForm m) (point : Fin m → ℤ) : AffineCover.AffineForm.eval (left.sub right) point = AffineCover.AffineForm.eval left point - AffineCover.AffineForm.eval right point

@[simp]

theorem Utilities.Certificate.ExplicitPotential.AffineForm.eval_positive {m : ℕ} (form : AffineForm m) (point : Fin m → ℤ) : AffineCover.AffineForm.eval form.positive point = AffineCover.AffineForm.eval form point - 1

def Utilities.Certificate.ExplicitPotential.CertificateData.rise {m n p : ℕ} (certificate : CertificateData m n p) (anchor : Fin n) (edge : Fin p) : AffineForm m

The potential rise from the tail to the head of one expanded edge.

Equations

• certificate.rise anchor edge = ((certificate.witness anchor).potential (certificate.core.head edge)).sub ((certificate.witness anchor).potential (certificate.core.tail edge))

def Utilities.Certificate.ExplicitPotential.CertificateData.lowerForm {m n p : ℕ} (certificate : CertificateData m n p) (anchor : Fin n) (edge : Fin p) : AffineForm m

The displayed lower endpoint inequality rise - alpha * length >= 0.

Equations

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

def Utilities.Certificate.ExplicitPotential.CertificateData.upperForm {m n p : ℕ} (certificate : CertificateData m n p) (anchor : Fin n) (edge : Fin p) : AffineForm m

The displayed upper endpoint inequality -beta * length - rise >= 0.

Equations

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

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

The target coefficient at a core vertex after removing the anchor chip.

Equations

• certificate.targetCoefficient anchor vertex = certificate.divisor vertex - if vertex = anchor then 1 else 0

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

The conservative endpoint contribution checked before seeing any lengths.

Equations

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

def Utilities.Certificate.ExplicitPotential.CertificateData.Valid {m n p : ℕ} (certificate : CertificateData m n p) (degree : ℤ) : Prop

Point-independent exact validity of a passive local record.

Equations

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

def Utilities.Certificate.ExplicitPotential.CertificateData.check {m n p : ℕ} (certificate : CertificateData m n p) (degree : ℤ) : Bool

Executable exact validity checker.

Equations

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

@[simp]

theorem Utilities.Certificate.ExplicitPotential.CertificateData.check_eq_true_iff {m n p : ℕ} (certificate : CertificateData m n p) (degree : ℤ) : certificate.check degree = true ↔ certificate.Valid degree

theorem Utilities.Certificate.ExplicitPotential.CertificateData.segment_positive_of_valid {m n p : ℕ} (certificate : CertificateData m n p) {degree : ℤ} (hValid : certificate.Valid degree) (point : Fin m → ℤ) (hCone : FormsHold certificate.cone point) (edge : Fin p) : 0 < AffineCover.AffineForm.eval (certificate.segment edge) point

Every expanded segment has positive integral length at a point in an accepted local cone.

def Utilities.Certificate.ExplicitPotential.CertificateData.segmentNat {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) (edge : Fin p) : ℕ

The natural-number segment length decoded from an integral point.

Equations

• certificate.segmentNat point edge = (Utilities.Certificate.AffineCover.AffineForm.eval (certificate.segment edge) point).toNat

theorem Utilities.Certificate.ExplicitPotential.CertificateData.segmentNat_cast_eq {m n p : ℕ} (certificate : CertificateData m n p) {degree : ℤ} (hValid : certificate.Valid degree) (point : Fin m → ℤ) (hCone : FormsHold certificate.cone point) (edge : Fin p) : ↑(certificate.segmentNat point edge) = AffineCover.AffineForm.eval (certificate.segment edge) point

theorem Utilities.Certificate.ExplicitPotential.CertificateData.segmentNat_positive {m n p : ℕ} (certificate : CertificateData m n p) {degree : ℤ} (hValid : certificate.Valid degree) (point : Fin m → ℤ) (hCone : FormsHold certificate.cone point) (edge : Fin p) : 0 < certificate.segmentNat point edge

def Utilities.Certificate.ExplicitPotential.CertificateData.riseValue {m n p : ℕ} (certificate : CertificateData m n p) (anchor : Fin n) (point : Fin m → ℤ) (edge : Fin p) : ℤ

Numerical core-potential rise at one integral length point.

Equations

• certificate.riseValue anchor point edge = Utilities.Certificate.AffineCover.AffineForm.eval (certificate.rise anchor edge) point

theorem Utilities.Certificate.ExplicitPotential.CertificateData.rise_bounds_of_valid {m n p : ℕ} (certificate : CertificateData m n p) {degree : ℤ} (hValid : certificate.Valid degree) (point : Fin m → ℤ) (hCone : FormsHold certificate.cone point) (anchor : Fin n) (edge : Fin p) : (certificate.witness anchor).alpha edge * AffineCover.AffineForm.eval (certificate.segment edge) point ≤ certificate.riseValue anchor point edge ∧ certificate.riseValue anchor point edge ≤ -(certificate.witness anchor).beta edge * AffineCover.AffineForm.eval (certificate.segment edge) point

Membership of the explicit lower/upper forms yields their endpoint rise bounds with no shortest-path theorem.

theorem Utilities.Certificate.ExplicitPotential.CertificateData.interpolated_endpoint_bounds {m n p : ℕ} (certificate : CertificateData m n p) {degree : ℤ} (hValid : certificate.Valid degree) (point : Fin m → ℤ) (hCone : FormsHold certificate.cone point) (anchor : Fin n) (edge : Fin p) : (certificate.witness anchor).alpha edge ≤ SubdivisionArithmetic.step (certificate.segmentNat point edge) (certificate.riseValue anchor point edge) 0 ∧ (certificate.witness anchor).beta edge ≤ -SubdivisionArithmetic.step (certificate.segmentNat point edge) (certificate.riseValue anchor point edge) (certificate.segmentNat point edge - 1)

The two endpoint slopes supplied by integer interpolation dominate the advertised alpha/beta bounds.

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

Actual interpolated endpoint contribution at a core vertex.

Equations

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

theorem Utilities.Certificate.ExplicitPotential.CertificateData.lowerEndpointContribution_le_endpointContribution {m n p : ℕ} (certificate : CertificateData m n p) {degree : ℤ} (hValid : certificate.Valid degree) (point : Fin m → ℤ) (hCone : FormsHold certificate.cone point) (anchor vertex : Fin n) : certificate.lowerEndpointContribution anchor vertex ≤ certificate.endpointContribution anchor point vertex

theorem Utilities.Certificate.ExplicitPotential.CertificateData.core_balance_nonnegative {m n p : ℕ} (certificate : CertificateData m n p) {degree : ℤ} (hValid : certificate.Valid degree) (point : Fin m → ℤ) (hCone : FormsHold certificate.cone point) (anchor vertex : Fin n) : 0 ≤ certificate.targetCoefficient anchor vertex + certificate.endpointContribution anchor point vertex

At every expanded core vertex, the target plus actual interpolated edge contributions is nonnegative.

theorem Utilities.Certificate.ExplicitPotential.CertificateData.interior_balance_nonnegative {m n p : ℕ} (certificate : CertificateData m n p) (anchor : Fin n) (point : Fin m → ℤ) (edge : Fin p) (offset : ℕ) (hOffset : 0 < offset) : 0 ≤ SubdivisionArithmetic.potential (certificate.segmentNat point edge) (certificate.riseValue anchor point edge) (offset - 1) - 2 * SubdivisionArithmetic.potential (certificate.segmentNat point edge) (certificate.riseValue anchor point edge) offset + SubdivisionArithmetic.potential (certificate.segmentNat point edge) (certificate.riseValue anchor point edge) (offset + 1)

Interpolation is convex at every positive interior offset, hence its second difference (the path-interior principal-divisor coefficient) is nonnegative.