W5 aggregation on a contracted core class

W5 is checked before zero-length core edges are contracted, one original core vertex at a time. This small lemma is the purely algebraic part of its closed-face use: any actual endpoint contributions which dominate W5's conservative tail/head minima remain effective after summing an entire contraction class. It deliberately contains no raw-chip decoding; that geometry supplies the two domination hypotheses at the call site.

It is deliberately based on RichLeafSound rather than on the final assembly module, so that RichLeafFullSound.richLeaf_sound can consume it; the hTail/hHead hypotheses are produced by RichChipBridge.

def Utilities.Subdivision.ClosedRowProof.RichWitness.w5ActualResidual {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (mult : ℤ) (a : Fin n) (tail head : Fin p → ℤ) (v : Fin n) : ℤ

The actual residual at an original core vertex, parameterized by the tail/head endpoint contributions furnished by the closed-face geometry.

Equations

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

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.w5Residual_nonneg_of_w5Checks {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (hW5 : w.w5Checks core = true) (a v : Fin n) : 0 ≤ w.w5Residual core ↑a ↑v

W5's Boolean table exposes a nonnegative residual at every original core vertex.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.w5ActualResidual_nonneg {n p : ℕ} (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (mult : ℤ) (a : Fin n) (tail head : Fin p → ℤ) (hTail : ∀ (e : Fin p), w.tailContribution ↑a ↑e ≤ tail e) (hHead : ∀ (e : Fin p), w.headContribution ↑a ↑e ≤ head e) (v : Fin n) (hbase : 0 ≤ w.w5MultResidual core mult ↑a ↑v) : 0 ≤ w.w5ActualResidual core mult a tail head v

If the actual endpoint contributions dominate W5's conservative minima, then every original-core residual is effective.

theorem Utilities.Subdivision.ClosedRowProof.RichWitness.w5ActualResidual_class_nonneg {n p : ℕ} (d : Certificate.DegenerateSpec.DegSpec n p) (w : RichWitness) (core : Certificate.ExplicitPotential.Core n p) (mult : ℤ) (a : Fin n) (hbase : ∀ (v : Fin n), 0 ≤ w.w5MultResidual core mult ↑a ↑v) (tail head : Fin p → ℤ) (hTail : ∀ (e : Fin p), w.tailContribution ↑a ↑e ≤ tail e) (hHead : ∀ (e : Fin p), w.headContribution ↑a ↑e ≤ head e) (vertex : Fin n) : 0 ≤ ∑ v : Fin n with d.rep v = d.rep vertex, w.w5ActualResidual core mult a tail head v

W5 survives contraction: summing the actual residuals over an arbitrary quotient-core class is nonnegative. The class is written using the exact fiber that richCoreDivisor and the piecewise-script core formula use.