Executable checks for rich row-proof leaves

This is the data-level half of the multi-block leaf checker. In particular, the W4 and W5 quantities below are integer computations on the declared block bounds and chips; only the certificates witnessing the length-dependent alternatives are delegated to Cert.check.

The indices deliberately agree with rpfcheck.c: a named point has index s : ℕ, is the end of block s - 1, and hence runs in W4 start at 1.

def Utilities.Subdivision.ClosedRowProof.RichWitness.point (w : RichWitness) (a e i : ℕ) : Form

The right end of block i - 1; index zero is the tail of the slot.

Equations

• w.point a e i = if i = 0 then [] else (w.block a e (i - 1)).endForm

def Utilities.Subdivision.ClosedRowProof.RichWitness.blockLength (w : RichWitness) (a e i : ℕ) : Form

The length of block i, as a form.

Equations

• w.blockLength a e i = Utilities.Subdivision.ClosedRowProof.subForm (w.block a e i).endForm (w.point a e i)

def Utilities.Subdivision.ClosedRowProof.RichWitness.chipAt (w : RichWitness) (a e i : ℕ) : ℤ

Total chip coefficient assigned to a named point.

This intentionally follows rpfcheck.c's W3 scan: a chip belongs to the first matching named interior point of the slot. The distinction matters when zero-length blocks make two named forms equal. In particular index zero is the tail, not a named interior point, so it never receives a chip. W3 separately ensures that every chip has such a matching interior point.

Equations

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

@[simp]

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.chipAt_zero (w : RichWitness) (a e : ℕ) : w.chipAt a e 0 = 0

def Utilities.Subdivision.ClosedRowProof.RichWitness.chipPrefix (w : RichWitness) (a e s : ℕ) : ℤ

Chip coefficients at named points 1, …, s, inclusive.

Equations

• w.chipPrefix a e s = List.foldl (fun (z : ℤ) (i : ℕ) => z + w.chipAt a e i) 0 (List.range (s + 1))

def Utilities.Subdivision.ClosedRowProof.RichWitness.tailCandidate (w : RichWitness) (a e s : ℕ) : ℤ

The W5 tail candidate when precisely the first s named points have fallen into the tail.

Equations

• w.tailCandidate a e s = w.chipPrefix a e s + (w.block a e s).lo

def Utilities.Subdivision.ClosedRowProof.RichWitness.headCandidate (w : RichWitness) (a e s : ℕ) : ℤ

The W5 head candidate when precisely the last s named points have fallen into the head.

Equations

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

def Utilities.Subdivision.ClosedRowProof.RichWitness.minOver (f : ℕ → ℤ) (bound : ℕ) : ℤ

Minimum of the endpoint candidates indexed by 0, …, bound.

This is public because the closed-face soundness proof uses the elementary fact that it is bounded above by every candidate represented by a collapsed endpoint prefix/suffix.

Equations

• Utilities.Subdivision.ClosedRowProof.RichWitness.minOver f bound = List.foldl (fun (z : ℤ) (i : ℕ) => min z (f (i + 1))) (f 0) (List.range bound)

def Utilities.Subdivision.ClosedRowProof.RichWitness.tailContribution (w : RichWitness) (a e : ℕ) : ℤ

The conservative W5 contribution of a slot at its tail.

Equations

• w.tailContribution a e = Utilities.Subdivision.ClosedRowProof.RichWitness.minOver (w.tailCandidate a e) ((w.plan a).headSlack.getD e 0)

def Utilities.Subdivision.ClosedRowProof.RichWitness.headContribution (w : RichWitness) (a e : ℕ) : ℤ

The conservative W5 contribution of a slot at its head.

Equations

• w.headContribution a e = Utilities.Subdivision.ClosedRowProof.RichWitness.minOver (w.headCandidate a e) ((w.plan a).tailSlack.getD e 0)

def Utilities.Subdivision.ClosedRowProof.RichWitness.w4Residual (w : RichWitness) (a e i j : ℕ) : ℤ

The constant residual of the W4 run from named point i through j.

Equations

• w.w4Residual a e i j = List.foldl (fun (z : ℤ) (t : ℕ) => z + w.chipAt a e (i + t)) 0 (List.range (j + 1 - i)) + (w.block a e j).lo - (w.block a e (i - 1)).hi

def Utilities.Subdivision.ClosedRowProof.RichWitness.positiveCheck (c : Cert) (Γ : Context) (f : Form) : Bool

The strict-integer certificate that a form is positive.

Equations

• Utilities.Subdivision.ClosedRowProof.RichWitness.positiveCheck c Γ f = c.check Γ (Utilities.Subdivision.ClosedRowProof.subForm f [1])

def Utilities.Subdivision.ClosedRowProof.RichWitness.w1Checks {n p : ℕ} (w : RichWitness) (_core : Certificate.ExplicitPotential.Core n p) (Γ : Context) : Bool

W1: block order, final endpoint, and endpoint-slack discipline.

Equations

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

def Utilities.Subdivision.ClosedRowProof.RichWitness.w2Checks {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) : Bool

W2: each block is realizable by convex interpolation and the block rises close the potential around every slot.

Equations

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

def Utilities.Subdivision.ClosedRowProof.RichWitness.w3Checks {n p : ℕ} (w : RichWitness) (_core : Certificate.ExplicitPotential.Core n p) : Bool

W3: each chip is on this slot's syntactically named interior point.

Equations

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

def Utilities.Subdivision.ClosedRowProof.RichWitness.tailConfined (w : RichWitness) (a e i : ℕ) : Bool

A named point whose form is syntactically the tail of its slot. Since W1 makes the named points weakly increasing from 0, such a point evaluates to 0 at every parameter value, so any collapsed run through it sits on the tail core vertex, where W5 — not W4 — accounts for it.

Equations

• w.tailConfined a e i = Utilities.Subdivision.ClosedRowProof.formEq (w.point a e i) []

def Utilities.Subdivision.ClosedRowProof.RichWitness.headConfined (w : RichWitness) (a e j : ℕ) : Bool

The head-side mirror of tailConfined.

Equations

• w.headConfined a e j = Utilities.Subdivision.ClosedRowProof.formEq (w.point a e j) (Utilities.Subdivision.ClosedRowProof.coordForm e)

def Utilities.Subdivision.ClosedRowProof.RichWitness.w4Checks {n p : ℕ} (w : RichWitness) (_core : Certificate.ExplicitPotential.Core n p) (Γ : Context) : Bool

W4: every possibly-collapsed interior run has nonnegative residual, or a strict separation receipt.

The run i … j ranges over all named interior indices 1 ≤ i ≤ j ≤ k − 1. It is exempt only when it is pinned to an endpoint by tailConfined / headConfined, which is the sound reading of spec §4.3's "every named interior point and every collapsed run of them".

The earlier implementation instead skipped i ≤ α and j > k − 1 − ω, using the declared endpoint slack. That is unsound: α bounds how many named points may slide onto the tail, not how many do, so a run starting at i ≤ α can collapse at a strictly interior vertex whose residual then goes unchecked. See the accompanying analysis.

Equations

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

def Utilities.Subdivision.ClosedRowProof.RichWitness.w5MultResidual {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (mult : ℤ) (a v : ℕ) : ℤ

W5 residual at one core vertex for one plan, with mult chips withdrawn at the plan's own vertex.

mult = 1 is a rank anchor: reaching a witnesses rank ≥ 1 there. mult = m is a legged goal's (comp x …) doubled anchor, where the claim is instead that D − m·1_x is winnable. The two run through identical machinery; this coefficient is the only difference, exactly as in rpfcheck.c's W5.

Equations

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

def Utilities.Subdivision.ClosedRowProof.RichWitness.w5Residual {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (a v : ℕ) : ℤ

W5 residual at one core vertex for one anchor.

Equations

• w.w5Residual core a v = w.w5MultResidual core 1 a v

def Utilities.Subdivision.ClosedRowProof.RichWitness.w5MultChecks {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (mult : ℤ) (a : ℕ) : Bool

W5 at multiplicity mult for the single plan at a: the extra row a legged rich leaf carries beyond richLeafChecks.

Equations

• w.w5MultChecks core mult a = Utilities.Certificate.ExplicitPotential.allFin fun (v : Fin n) => decide (0 ≤ w.w5MultResidual core mult a ↑v)

@[simp]

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.w5MultChecks_eq_true_iff {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (mult : ℤ) (a : ℕ) : w.w5MultChecks core mult a = true ↔ ∀ (v : Fin n), 0 ≤ w.w5MultResidual core mult a ↑v

def Utilities.Subdivision.ClosedRowProof.RichWitness.w5Checks {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) : Bool

W5: all conservative core residuals are effective.

Equations

• w.w5Checks core = Utilities.Certificate.ExplicitPotential.allFin fun (a : Fin n) => Utilities.Certificate.ExplicitPotential.allFin fun (v : Fin n) => decide (0 ≤ w.w5Residual core ↑a ↑v)

def Utilities.Subdivision.ClosedRowProof.RichWitness.richLeafChecks {n p : ℕ} (w : RichWitness) (_m : ℕ) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (degree : ℤ) : Bool

The executable W1--W5 checker for a rich multi-block leaf. Structural row conditions and degree are included here so that this is directly usable as the replacement leaf predicate by the tree layer.

Equations

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