Semantic bridge ingredients for rich row-proof leaves

This module deliberately does not yet add a PTree constructor. It records the pointwise arithmetic facts which turn the executable W1--W5 receipts into closed-face data. Keeping these facts independent of the tree is useful: a rich leaf is evaluated at a single integral point before its block endpoints are decoded into a DegSpec.PiecewiseData and its chips into a weighted divisor.

The remaining assembly is not a matter of weakening the checker. It needs a finite-list decoder which supplies PiecewiseData.covers, PiecewiseData.ownsInterval, and PiecewiseData.balance, together with the two residual comparison lemmas documented at the end of this file.

def Utilities.Subdivision.ClosedRowProof.RichWitness.pointValue (w : RichWitness) (x : List ℤ) (a e i : ℕ) : ℤ

Evaluation of a named point. This is kept as an integer: W1 first proves nonnegativity, after which the lowerer may take toNat to obtain a path offset.

Equations

• w.pointValue x a e i = Utilities.Subdivision.ClosedRowProof.eval (w.point a e i) x

def Utilities.Subdivision.ClosedRowProof.RichWitness.blockLengthValue (w : RichWitness) (x : List ℤ) (a e i : ℕ) : ℤ

Evaluation of a declared block length.

Equations

• w.blockLengthValue x a e i = Utilities.Subdivision.ClosedRowProof.eval (w.blockLength a e i) x

@[simp]

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.pointValue_zero (w : RichWitness) (x : List ℤ) (a e : ℕ) : w.pointValue x a e 0 = 0

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.blockLengthValue_eq (w : RichWitness) (x : List ℤ) (a e i : ℕ) : w.blockLengthValue x a e i = eval (w.block a e i).endForm x - w.pointValue x a e i

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.pointValue_succ_sub (w : RichWitness) (x : List ℤ) (a e i : ℕ) : w.pointValue x a e (i + 1) - w.pointValue x a e i = w.blockLengthValue x a e i

Consecutive named points differ by the length of the intervening block. This is the arithmetic form of the RPF convention that point i + 1 is the right endpoint of block i.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.pointValue_mono_of_lengths (w : RichWitness) (x : List ℤ) (a e k : ℕ) (hLength : ∀ i < k, 0 ≤ w.blockLengthValue x a e i) {i j : ℕ} (hij : i ≤ j) (hj : j ≤ k) : w.pointValue x a e i ≤ w.pointValue x a e j

W1 monotonicity receipts make the evaluated named points weakly ordered. The index bounds are explicit because a rich block list is only constrained on its declared finite prefix.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.pointValue_nonneg_of_lengths (w : RichWitness) (x : List ℤ) (a e k i : ℕ) (hLength : ∀ j < k, 0 ≤ w.blockLengthValue x a e j) (hi : i ≤ k) : 0 ≤ w.pointValue x a e i

Every named point through the final endpoint is nonnegative. This is the integer fact needed before W1 endpoints can be decoded with Int.toNat.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.pointValue_le_of_lengths_last (w : RichWitness) (x : List ℤ) (a e k L i : ℕ) (hLength : ∀ j < k, 0 ≤ w.blockLengthValue x a e j) (hLast : w.pointValue x a e k = ↑L) (hi : i ≤ k) : w.pointValue x a e i ≤ ↑L

W1's final endpoint equality bounds every named point by the slot length.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.pointValue_eq_zero_lt_of_pointValue_pos (w : RichWitness) (x : List ℤ) (a e k i s : ℕ) (hLength : ∀ j < k, 0 ≤ w.blockLengthValue x a e j) (hi : i ≤ k) (hZero : w.pointValue x a e i = 0) (hPos : 0 < w.pointValue x a e s) : i < s

A positive evaluated named point separates all earlier named points from the tail. This is the arithmetic W1 bridge used to bound a collapsed prefix.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.lt_of_pointValue_eq_length_of_pointValue_lt (w : RichWitness) (x : List ℤ) (a e k L i s : ℕ) (hLength : ∀ j < k, 0 ≤ w.blockLengthValue x a e j) (hs : s ≤ k) (hLengthValue : w.pointValue x a e i = ↑L) (hLt : w.pointValue x a e s < ↑L) : s < i

The head-side counterpart: a named point strictly before the slot length separates every later point at the head.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.positiveCheck_sound {c : Cert} {Γ : Context} {f : Form} (hcheck : positiveCheck c Γ f = true) {x : List ℤ} (hx : Γ.Holds x) : 0 < eval f x

A strict W1 separation receipt is genuinely strict at every integral point satisfying its context.

W3 shape facts

The physical chip decoder needs only the two structural consequences of W3: every raw slot index is genuine, and for every anchor a chip is syntactically one of that slot's named interior endpoints. The latter becomes an equality of evaluated positions through eval_eq_of_formEq.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.slot_lt_of_w3Checks {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (hW3 : w.w3Checks core = true) {chip : ℕ × Form × ℤ} (hchip : chip ∈ w.chips) : chip.1 < p

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.chip_named_of_w3Checks {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (hW3 : w.w3Checks core = true) (a : Fin n) {chip : ℕ × Form × ℤ} (hchip : chip ∈ w.chips) : ∃ i < (w.blockList (↑a) chip.1).length - 1, formEq chip.2.1 (w.point (↑a) chip.1 (i + 1)) = true

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.chip_pointValue_eq_of_w3Checks {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (hW3 : w.w3Checks core = true) (a : Fin n) {chip : ℕ × Form × ℤ} (hchip : chip ∈ w.chips) (x : List ℤ) : ∃ i < (w.blockList (↑a) chip.1).length - 1, eval chip.2.1 x = w.pointValue x (↑a) chip.1 (i + 1)

W3's syntactic named-point witness has the expected geometric meaning at every parameter point: the raw form evaluates to that named endpoint.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.blockLength_nonneg_of_w1Checks {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hx : Γ.Holds x) (a : Fin n) (e : Fin p) (i : ℕ) (hi : i < (w.blockList ↑a ↑e).length) : 0 ≤ w.blockLengthValue x (↑a) (↑e) i

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.pointValue_last_eq_coord_of_w1Checks {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (a : Fin n) (e : Fin p) : w.pointValue x (↑a) (↑e) (w.blockList ↑a ↑e).length = eval (coordForm ↑e) x

W1's final named endpoint is the coordinate form for its slot.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.blockLength_nonneg_of_receipt (w : RichWitness) (Γ : Context) (x : List ℤ) (hx : Γ.Holds x) (a e i : ℕ) (hcheck : (w.blockReceipt a e i).monotone.check Γ (w.blockLength a e i) = true) : 0 ≤ w.blockLengthValue x a e i

W1's monotonicity certificate says precisely that the evaluated block length is nonnegative. This is the local fact used to order the decoded block ends.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.blockLower_bound_of_receipt (w : RichWitness) (Γ : Context) (x : List ℤ) (hx : Γ.Holds x) (a e i : ℕ) (hcheck : (w.blockReceipt a e i).lower.check Γ (subForm (w.block a e i).rise (smulForm (w.block a e i).lo (w.blockLength a e i))) = true) : (w.block a e i).lo * w.blockLengthValue x a e i ≤ eval (w.block a e i).rise x

The lower W2 receipt gives the numerical lower endpoint-slope bound for one decoded block.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.blockUpper_bound_of_receipt (w : RichWitness) (Γ : Context) (x : List ℤ) (hx : Γ.Holds x) (a e i : ℕ) (hcheck : (w.blockReceipt a e i).upper.check Γ (subForm (smulForm (w.block a e i).hi (w.blockLength a e i)) (w.block a e i).rise) = true) : eval (w.block a e i).rise x ≤ (w.block a e i).hi * w.blockLengthValue x a e i

The upper W2 receipt gives the numerical upper endpoint-slope bound for one decoded block.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.blockRise_eq_zero_of_bounds (w : RichWitness) (Γ : Context) (x : List ℤ) (hx : Γ.Holds x) (a e i : ℕ) (hLower : (w.blockReceipt a e i).lower.check Γ (subForm (w.block a e i).rise (smulForm (w.block a e i).lo (w.blockLength a e i))) = true) (hUpper : (w.blockReceipt a e i).upper.check Γ (subForm (smulForm (w.block a e i).hi (w.blockLength a e i)) (w.block a e i).rise) = true) (hEmpty : w.blockLengthValue x a e i = 0) : eval (w.block a e i).rise x = 0

A zero-length block has zero declared rise. This is the W2 fact which allows repeated finite endpoints to be discarded by canonical interpolation without changing the total potential change.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.blockBounds_of_w2Checks {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (hW2 : w.w2Checks core Γ = true) (a : Fin n) (e : Fin p) (i : ℕ) (hi : i < (w.blockList ↑a ↑e).length) : (w.blockReceipt (↑a) (↑e) i).lower.check Γ (subForm (w.block (↑a) (↑e) i).rise (smulForm (w.block (↑a) (↑e) i).lo (w.blockLength (↑a) (↑e) i))) = true ∧ (w.blockReceipt (↑a) (↑e) i).upper.check Γ (subForm (smulForm (w.block (↑a) (↑e) i).hi (w.blockLength (↑a) (↑e) i)) (w.block (↑a) (↑e) i).rise) = true

Extract the two numerical W2 receipts for a declared block.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.blockRise_eq_zero_of_w2Checks {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW2 : w.w2Checks core Γ = true) (hx : Γ.Holds x) (a : Fin n) (e : Fin p) (i : ℕ) (hi : i < (w.blockList ↑a ↑e).length) (hEmpty : w.blockLengthValue x (↑a) (↑e) i = 0) : eval (w.block (↑a) (↑e) i).rise x = 0

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.eval_foldl_addForm (forms : List Form) (initial : Form) (x : List ℤ) : eval (List.foldl addForm initial forms) x = eval initial x + (List.map (fun (form : Form) => eval form x) forms).sum

Evaluation commutes with an accumulated list of affine-form additions.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.eval_foldl_addForm_index {α : Type} (indices : List α) (form : α → Form) (initial : Form) (x : List ℤ) : eval (List.foldl (fun (z : Form) (i : α) => addForm z (form i)) initial indices) x = eval initial x + (List.map (fun (i : α) => eval (form i) x) indices).sum

Indexed version of eval_foldl_addForm, matching the RPF representation where a finite list of block indices selects the forms to add.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.foldl_range_eq_finset_sum (f : ℕ → ℤ) (k : ℕ) : List.foldl (fun (z : ℤ) (i : ℕ) => z + f i) 0 (List.range k) = ∑ i ∈ Finset.range k, f i

The ordered finite list range k computes the same additive sum as the finite-set presentation used by the piecewise interpolation interface.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.totalRises_eq_potentialDifference_of_w2Checks {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW2 : w.w2Checks core Γ = true) (a : Fin n) (e : Fin p) : ∑ i ∈ Finset.range (w.blockList ↑a ↑e).length, eval (w.block (↑a) (↑e) i).rise x = eval (w.pot ↑a ↑(core.head e)) x - eval (w.pot ↑a ↑(core.tail e)) x

W2 closure, evaluated at a point, is the finite sum of all declared block rises. This is the arithmetic input to piecewise_balance_of_total_rises.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.potential_eq_of_zeroLength_of_w1w2 {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hW2 : w.w2Checks core Γ = true) (hx : Γ.Holds x) (a : Fin n) (e : Fin p) (hZero : eval (coordForm ↑e) x = 0) : eval (w.pot ↑a ↑(core.head e)) x = eval (w.pot ↑a ↑(core.tail e)) x

On a zero-length slot, W1 collapses every block and W2 makes every rise zero; consequently the evaluated anchor potential agrees across the slot.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.value_eq_of_reachIn {n p : ℕ} (core : Certificate.ExplicitPotential.Core n p) (F : Finset (Fin p)) (value : Fin n → ℤ) (hEdge : ∀ e ∈ F, value (core.tail e) = value (core.head e)) {u v : Fin n} (hReach : Certificate.ContractionForestCensusGeneral.ReachIn core F u v) : value u = value v

Equality along every edge of a contracted set transports along the census reachability relation. This is the small graph-theoretic bridge from the zero-slot lemma to DegSpec.RepInvariant.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.repInvariant_of_w1w2_census {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hW2 : w.w2Checks core Γ = true) (hx : Γ.Holds x) (a : Fin n) (hn : 0 < n) (ℓ : Fin p → ℕ) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(ℓ e)) (hForest : Certificate.ContractionForestCensusGeneral.IsForest core (zeroSet ℓ)) (hNotLoopy : ¬Certificate.ContractionForestCensusGeneral.IsLoopy core (zeroSet ℓ)) : (censusSpec core hn ℓ hForest hNotLoopy).RepInvariant fun (v : Fin n) => eval (w.pot ↑a ↑v) x

The evaluated potential of a rich anchor is invariant on every contraction class of the census face.

W4: collapsed boundary runs

At a named interior vertex the only possible negative contribution of the piecewise script is the jump from the last slope before a run of coincident named endpoints to the first slope after it. The checker deliberately uses the lower bound of the outgoing block and the upper bound of the incoming block, so its integer residual is a lower bound for the actual coefficient.

The lemmas in this section are phrased without a subdivision graph. This is intentional: decoding named forms into a closed-face vertex is the only graph-specific part of the eventual proof, while the W4 arithmetic is exactly the calculation below. In particular repeated endpoints (zero-length blocks) need no special case: they simply enlarge the run.

def Utilities.Subdivision.ClosedRowProof.RichWitness.w4ChipSum (chip : ℕ → ℤ) (i j : ℕ) : ℤ

The chip sum used by W4, written in the same List.range/foldl form as the executable checker.

Equations

• Utilities.Subdivision.ClosedRowProof.RichWitness.w4ChipSum chip i j = List.foldl (fun (z : ℤ) (t : ℕ) => z + chip (i + t)) 0 (List.range (j + 1 - i))

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.w4Residual_eq_chipSum (w : RichWitness) (a e i j : ℕ) : w.w4Residual a e i j = w4ChipSum (fun (t : ℕ) => w.chipAt a e t) i j + (w.block a e j).lo - (w.block a e (i - 1)).hi

This is definitionally the chip portion of the executable W4 residual. Keeping the bridge explicit avoids a later proof depending on the particular implementation of w4Residual.

def Utilities.Subdivision.ClosedRowProof.RichWitness.w4Actual (chip : ℕ → ℤ) (incoming outgoing : ℤ) (i j : ℕ) : ℤ

The actual coefficient at a collapsed named-endpoint run: chips on the run plus outgoing slope minus incoming slope.

Equations

• Utilities.Subdivision.ClosedRowProof.RichWitness.w4Actual chip incoming outgoing i j = Utilities.Subdivision.ClosedRowProof.RichWitness.w4ChipSum chip i j + outgoing - incoming

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.w4Residual_le_actual (chip lo hi : ℕ → ℤ) (incoming outgoing : ℤ) (i j : ℕ) (hIncoming : incoming ≤ hi (i - 1)) (hOutgoing : lo j ≤ outgoing) : w4ChipSum chip i j + lo j - hi (i - 1) ≤ w4Actual chip incoming outgoing i j

The numerical residual checked by W4 is a lower bound for the actual coefficient whenever W2 bounds the two bordering slopes.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.w4_not_collapsed_of_strict_separation {left right : ℤ} (hsep : 0 < right - left) : left ≠ right

A strict W4 separation receipt rules out the only situation in which its corresponding run has to be tested: all named endpoints of that run decoding to the same closed-face vertex.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.w4_actual_nonneg_of_checked (chip lo hi : ℕ → ℤ) (incoming outgoing left right : ℤ) (i j : ℕ) (hIncoming : incoming ≤ hi (i - 1)) (hOutgoing : lo j ≤ outgoing) (hChecked : 0 ≤ w4ChipSum chip i j + lo j - hi (i - 1) ∨ 0 < right - left) (hCollapsed : left = right) : 0 ≤ w4Actual chip incoming outgoing i j

The local W4 soundness step. If the endpoints collapse, the strict separation alternative is impossible, hence a nonnegative checked residual remains; W2 then promotes it to nonnegativity of the actual divisor coefficient.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.w4_checked_or_separated_of_w4Checks {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW4 : w.w4Checks core Γ = true) (hx : Γ.Holds x) (a : Fin n) (e : Fin p) (i j : ℕ) (hI : 1 ≤ i) (hJ : j ≤ (w.blockList ↑a ↑e).length - 1) (hIJ : i ≤ j) (hNotTail : w.pointValue x (↑a) (↑e) i ≠ 0) (hNotHead : w.pointValue x (↑a) (↑e) j ≠ eval (coordForm ↑e) x) : 0 ≤ w.w4Residual (↑a) (↑e) i j ∨ 0 < w.pointValue x (↑a) (↑e) j - w.pointValue x (↑a) (↑e) i

Extract one of the two W4 alternatives for an admissible interior run. The executable checker enumerates the run by q = i - 1 and r = j - i; this lemma exposes the geometric indices directly, so the closed-face proof can feed a collapsed run to w4_actual_nonneg_of_checked.

def Utilities.Subdivision.ClosedRowProof.RichWitness.endpointValues (w : RichWitness) (x : List ℤ) (a e k : ℕ) : List ℕ

The finite endpoint list decoded from an evaluated rich slot. Its entry i is named point i + 1, so it is the end of block i.

Equations

• w.endpointValues x a e k = List.map (fun (i : ℕ) => (w.pointValue x a e (i + 1)).toNat) (List.range k)

@[simp]

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.endpointValues_length (w : RichWitness) (x : List ℤ) (a e k : ℕ) : (w.endpointValues x a e k).length = k

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.endpointValues_getD (w : RichWitness) (x : List ℤ) (a e k L i : ℕ) (hi : i < k) : (w.endpointValues x a e k).getD i L = (w.pointValue x a e (i + 1)).toNat

def Utilities.Subdivision.ClosedRowProof.RichWitness.finiteBlockEndsOfW1 (w : RichWitness) (x : List ℤ) (a e k L : ℕ) (hNonempty : 0 < k) (hLast : w.pointValue x a e k = ↑L) (hLength : ∀ i < k, 0 ≤ w.blockLengthValue x a e i) : MarkedGraphs.Certificate.FiniteBlockEnds L

W1's nonempty, monotone endpoint data decodes to the finite selector required by canonical piecewise interpolation. The input hLast is the evaluated W1 final-end equality; all block lengths are integral and the nonnegative receipts make the Int.toNat conversion exact.

Equations

• w.finiteBlockEndsOfW1 x a e k L hNonempty hLast hLength = MarkedGraphs.Certificate.FiniteBlockEnds.ofOrderedLast (w.endpointValues x a e k) ⋯ ⋯ ⋯

noncomputable def Utilities.Subdivision.ClosedRowProof.RichWitness.richBlockEnds {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hx : Γ.Holds x) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(d.length e)) (a : Fin n) (e : Fin p) : MarkedGraphs.Certificate.FiniteBlockEnds (d.length e)

The finite endpoint selector decoded from an accepted rich W1 block list on a concrete closed face.

Equations

• Utilities.Subdivision.ClosedRowProof.RichWitness.richBlockEnds d w core Γ x hW1 hx hCoord a e = w.finiteBlockEndsOfW1 x (↑a) (↑e) (w.blockList ↑a ↑e).length (d.length e) ⋯ ⋯ ⋯

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.richBlockEnds_endAt {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hx : Γ.Holds x) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(d.length e)) (a : Fin n) (e : Fin p) (i : ℕ) (hi : i < (w.blockList ↑a ↑e).length) : (richBlockEnds d w core Γ x hW1 hx hCoord a e).endAt i = (w.pointValue x (↑a) (↑e) (i + 1)).toNat

On an actual rich block, the finite decoder's endpoint is exactly the evaluated named right endpoint. Keeping this lookup lemma separate makes the W2 empty-block bridge below independent of the proof fields stored in FiniteBlockEnds.ofOrderedLast.

@[simp]

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.richBlockEnds_length {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hx : Γ.Holds x) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(d.length e)) (a : Fin n) (e : Fin p) : (richBlockEnds d w core Γ x hW1 hx hCoord a e).ends.length = (w.blockList ↑a ↑e).length

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.eval_block_rise_eq_zero_of_not_lt (w : RichWitness) (x : List ℤ) (a e i : ℕ) (hi : ¬i < (w.blockList a e).length) : eval (w.block a e i).rise x = 0

Beyond a declared rich block list, the fail-closed default block has zero rise, so it contributes nothing to the interpolation sum.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.blockRise_eq_zero_of_richBlockEnds_empty {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hW2 : w.w2Checks core Γ = true) (hx : Γ.Holds x) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(d.length e)) (a : Fin n) (e : Fin p) (i : ℕ) (hi : i < (w.blockList ↑a ↑e).length) (hEmpty : (richBlockEnds d w core Γ x hW1 hx hCoord a e).endAt i ≤ (richBlockEnds d w core Γ x hW1 hx hCoord a e).startAt i) : eval (w.block (↑a) (↑e) i).rise x = 0

If an actual decoded rich block has an empty finite interval, then W1 makes its evaluated length zero and W2 forces its declared rise to vanish. This is the exact bridge needed by PiecewiseData.empty_rise: repeated finite endpoints are harmless even when their RPF block records remain in the list.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.piecewise_balance_of_total_rises {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (potential : Fin n → ℤ) (blocks : (e : Fin p) → MarkedGraphs.Certificate.FiniteBlockEnds (d.length e)) (rises : Fin p → ℕ → ℤ) (hEmpty : ∀ (e : Fin p) (i : ℕ), (blocks e).endAt i ≤ (blocks e).startAt i → rises e i = 0) (hTotal : ∀ (e : Fin p), potential (d.core.head e) = potential (d.core.tail e) + ∑ i ∈ Finset.range (blocks e).ends.length, rises e i) (e : Fin p) : potential (d.core.head e) = potential (d.core.tail e) + ∑ k ∈ Finset.range (d.length e), Certificate.DegenerateSpec.DegSpec.blockSlope (fun (e : Fin p) (k : ℕ) => (blocks e).blockAt k) (fun (e : Fin p) (k : ℕ) => (blocks e).endAt k) rises e k

Once W2 has made every collapsed block's rise zero, its closure equality is exactly the balance field required by PiecewiseData. This is independent of the RPF list encoding and is the final arithmetic conversion used by the rich-leaf decoder.

noncomputable def Utilities.Subdivision.ClosedRowProof.RichWitness.richCensusPiecewiseData {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hW2 : w.w2Checks core Γ = true) (hx : Γ.Holds x) (ℓ : Fin p → ℕ) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(ℓ e)) (hn : 0 < n) (hForest : Certificate.ContractionForestCensusGeneral.IsForest core (zeroSet ℓ)) (hNotLoopy : ¬Certificate.ContractionForestCensusGeneral.IsLoopy core (zeroSet ℓ)) (a : Fin n) : (censusSpec core hn ℓ hForest hNotLoopy).PiecewiseData fun (v : Fin n) => eval (w.pot ↑a ↑v) x

The canonical piecewise interpolation data for one rich anchor on the census face selected by the current length vector.

Equations

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

noncomputable def Utilities.Subdivision.ClosedRowProof.RichWitness.richCensusPiecewiseScript {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hW2 : w.w2Checks core Γ = true) (hx : Γ.Holds x) (ℓ : Fin p → ℕ) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(ℓ e)) (hn : 0 < n) (hForest : Certificate.ContractionForestCensusGeneral.IsForest core (zeroSet ℓ)) (hNotLoopy : ¬Certificate.ContractionForestCensusGeneral.IsLoopy core (zeroSet ℓ)) (a : Fin n) : firingScript (censusSpec core hn ℓ hForest hNotLoopy).graph

The firing script denoted by the decoded rich block data.

Equations

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

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.richCensus_isStepSlope {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hW2 : w.w2Checks core Γ = true) (hx : Γ.Holds x) (ℓ : Fin p → ℕ) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(ℓ e)) (hn : 0 < n) (hForest : Certificate.ContractionForestCensusGeneral.IsForest core (zeroSet ℓ)) (hNotLoopy : ¬Certificate.ContractionForestCensusGeneral.IsLoopy core (zeroSet ℓ)) (a : Fin n) : (censusSpec core hn ℓ hForest hNotLoopy).IsStepSlope (w.richCensusPiecewiseScript core Γ x hW1 hW2 hx ℓ hCoord hn hForest hNotLoopy a) fun (e : Fin p) (k : ℕ) => Certificate.DegenerateSpec.DegSpec.blockSlope (w.richCensusPiecewiseData core Γ x hW1 hW2 hx ℓ hCoord hn hForest hNotLoopy a).blockAt (w.richCensusPiecewiseData core Γ x hW1 hW2 hx ℓ hCoord hn hForest hNotLoopy a).blockEnd (w.richCensusPiecewiseData core Γ x hW1 hW2 hx ℓ hCoord hn hForest hNotLoopy a).blockRise e k

The rich script's unit slopes are precisely its selected canonical block slopes; this is the entry point for the W4 interior coefficient calculation.

W4: selector changes on a rich closed face

The finite selector sees a forward jump precisely when a consecutive run of named endpoints has collapsed to the intervening subdivision vertex. The two lemmas below isolate that geometric fact from the subsequent chip-divisor accounting. Their indices agree with the checker: if the old selected block is i, then its named right endpoint is i + 1, while the new block is j.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.pointValue_eq_of_rich_selector_change {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hx : Γ.Holds x) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(d.length e)) (a : Fin n) (e : Fin p) (offset : Fin (d.length e - 1)) (hChange : (richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt ↑offset < (richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt (↑offset + 1)) : w.pointValue x (↑a) (↑e) ((richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt ↑offset + 1) = w.pointValue x (↑a) (↑e) ((richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt (↑offset + 1))

A forward change of the decoded rich block selector identifies the two named forms at the ends of the collapsed run. This is the geometric premise which rules out W4's strict-separation alternative.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.w4_actual_nonneg_of_rich_selector_change {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (Γ : Context) (x : List ℤ) (hW1 : w.w1Checks core Γ = true) (hW4 : w.w4Checks core Γ = true) (hx : Γ.Holds x) (hCoord : ∀ (e : Fin p), eval (coordForm ↑e) x = ↑(d.length e)) (a : Fin n) (e : Fin p) (offset : Fin (d.length e - 1)) (hChange : (richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt ↑offset < (richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt (↑offset + 1)) (incoming outgoing : ℤ) (hIncoming : incoming ≤ (w.block (↑a) (↑e) ((richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt ↑offset)).hi) (hOutgoing : (w.block (↑a) (↑e) ((richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt (↑offset + 1))).lo ≤ outgoing) : 0 ≤ w4Actual (fun (t : ℕ) => w.chipAt (↑a) (↑e) t) incoming outgoing ((richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt ↑offset + 1) ((richBlockEnds d w core Γ x hW1 hx hCoord a e).blockAt (↑offset + 1))

W4 promotes its checked residual to the actual slope-jump coefficient at a forward rich-selector change, once W2 has supplied the bordering slope bounds. The caller supplies the two bounds so this lemma can be used with the canonical script as well as any extensionally equal slope presentation.

W5: finite endpoint minima

The checker stores a conservative endpoint contribution as a finite minimum. The geometric part of the closed-face proof supplies a particular prefix (or suffix) length; this lemma is the deliberately small arithmetic bridge from that selected candidate to the stored minimum.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.minOver_le_candidate (f : ℕ → ℤ) (bound s : ℕ) (hs : s ≤ bound) : minOver f bound ≤ f s

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.tailContribution_le_candidate (w : RichWitness) (a e s : ℕ) (hs : s ≤ (w.plan a).headSlack.getD e 0) : w.tailContribution a e ≤ w.tailCandidate a e s

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.headContribution_le_candidate (w : RichWitness) (a e s : ℕ) (hs : s ≤ (w.plan a).tailSlack.getD e 0) : w.headContribution a e ≤ w.headCandidate a e s

Required next bridge lemmas

The following are the exact nontrivial obligations left before a theorem richLeafChecks_sound can be assembled.

• decode_piecewise: from the W1 monotonicity/final-end facts and the W2 receipts at x, construct d.PiecewiseData potential. Its proof requires a finite monotone-list selector (first block end strictly above a surviving step) and a telescoping lemma saying that the canonical steps over a block sum to its declared rise. The latter is not currently exported by SubdivisionArithmetic.

• w4_boundary_effective: identify a change of decoded block at an interior offset with a maximal run of named endpoints which evaluate to that offset. The W4 residual is the chip sum on this run plus the lower bound on the outgoing first slope minus the upper bound on the incoming last slope. DegSpec.prin_piecewiseScript_interiorVertex_nonneg_of_sameBlock already handles the complementary (non-boundary) case.

• w5_core_effective: after a prefix/suffix of named points collapses into a core class, compare the actual first/last selected slopes and all chips which decode to that class with tailContribution/headContribution. w5Checks then proves each uncontracted core summand nonnegative; summing it over a representative class and using DegSpec.prin_piecewiseScript_coreVertex proves the quotient-core case.

  Current formal interface obstruction. RichWitness.chips is still a raw List (Nat × Form × Int), whereas the closed-face library's only chipwise divisor API is Closed.WeightedChip.divisorOf, which accepts bounded Codes from an ExplicitPotential.CertificateData. A rich leaf has neither of those objects. Consequently the library has no definition for the rich chip divisor on d.graph, nor a coefficient theorem saying that chips which decode to the tail/head are exactly the C-faithful first-matched chipPrefix/suffix sums. W3 is enough to prove the needed bounds after such a decoder exists, but cannot state that comparison. The necessary next artifact is a row-local decoder from the raw rich chips and evaluated named endpoints to CFDiv d.graph, with core/interior coefficient formulae. The checker now assigns a chip to its first matching named interior endpoint, matching rpfcheck.c; the decoder theorem must preserve that convention when zero-length blocks duplicate endpoint forms.

The last two lemmas must use Closed.WeightedChip.divisorOf (or an equivalent row-local decoder), because a named point may become either endpoint on a closed face. Treating every declared chip as an interior vertex would be incorrect when a block collapses.