RSPhysics006Cert
plain-language theorem explainer
Certificate bundle for Physics Module 6 (Higgs VEV scale): diagonal domain cost vanishes, domain cost is nonnegative for positive mass and energy arguments, and the canonical threshold is strictly positive. Cited by the module's inhabited certificate and any consumer that needs the three structural side-conditions in one place. The declaration is a pure structure type; inhabitation is discharged elsewhere by the sibling lemmas.
Claim. A certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Physics RS Module 6 records the structural claim that the Higgs vacuum expectation scale sits near a pure $\phi$-power: $v/M_Z \approx 246/91.2 \approx 2.70$ versus $\phi^2 \approx 2.618$ (about 3% off). The module is marked structural theorem status (zero sorry, zero axiom).
The certificate packages three side-conditions on the module's domain cost and threshold. Domain cost is the local cost functional on pairs of positive reals used in this physics layer; the diagonal identity $C(r,r)=0$ for $r\neq 0$ is the zero-defect self-match. Nonnegativity mirrors the foundation fact that recognition cost never goes negative: upstream, cost_nonneg states that the cost of any recognition event is nonnegative, via $J$-cost nonnegativity on positive states.
The canonical threshold is the positive cutoff against which the module compares the Higgs ratio; positivity is required so the comparison is well-posed.
proof idea
No proof body: this is a structure definition, not a theorem. The three fields are Prop-valued requirements. Inhabitation is supplied by the sibling definition cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and by cert_inhabited, which packages that witness as Nonempty.
why it matters
Gives Module 6 a single named certificate type so downstream code can demand the three structural facts without restating them. Parents in-module are cert (the concrete witness) and cert_inhabited (nonemptiness). In the Recognition framework this sits under the Higgs VEV comparison to $\phi^2$ on the $\phi$-ladder (T6 self-similar fixed point), using the nonnegative $J$-cost lineage from the forcing chain rather than a free phenomenological potential. It does not itself prove the 3% numerical match; it only certifies the cost and threshold scaffolding the module needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.