cert
plain-language theorem explainer
Packages the three structural facts needed for the Module 6 Higgs-VEV certificate: the domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Anyone citing the Module 6 structural theorem uses this inhabited certificate. The construction is a pure record assembly from three already-proved sibling lemmas.
Claim. There is a certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module 6 records the structural side of the Higgs-VEV observation $v/M_Z\approx 246/91.2\approx 2.70$, compared with $\varphi^2\approx 2.618$ (about 3% off). The module is marked structural: zero sorry, zero axioms.
The certificate structure bundles three elementary properties of a domain cost on positive reals: vanishing when the two arguments coincide (and are nonzero), nonnegativity for positive arguments, and positivity of a fixed canonical threshold. Upstream, the foundation layer already knows that every recognition-event cost is nonnegative via the J-cost minimum at identity; the module-local nonnegativity lemma is the corresponding statement for this domain cost.
proof idea
One-line record construction. The three fields of the certificate structure are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional reasoning occurs at this site.
why it matters
This is the inhabited witness that Module 6's structural claims hold as a single package. Downstream consumers (none yet wired in the graph) can take the certificate rather than re-proving diagonal vanishing, nonnegativity, and threshold positivity separately. In the broader RS chain it sits under the physics layer that compares laboratory ratios to powers of $\varphi$ forced by T5–T6 (J-uniqueness and the self-similar fixed point). It does not itself derive the 3% Higgs offset; it only certifies the cost-theoretic scaffolding used around that comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.