cert_inhabited
plain-language theorem explainer
The certificate bundle for Physics Module 10 (Higgs-mass structural package) is nonempty: there exists a record packing diagonal vanishing of domain cost, nonnegativity for positive mass/energy, and positivity of the canonical threshold. Anyone wiring this module into a larger RS physics export cites it to discharge the inhabitedness obligation. The proof is a one-constructor term that hands the prebuilt `cert` witness to `Nonempty`.
Claim. There exists a certificate packing three facts: (i) the domain cost of any nonzero real against itself is zero; (ii) for positive mass and energy the domain cost is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 10 packages the Recognition Science structural claim that the Higgs mass sits on the phi-ladder: $m_H \approx 125.25,\mathrm{GeV}$ is matched by a rung near $\phi^{13}$ after the usual GeV yardstick conversion (module status: structural theorem, zero sorry, zero axiom).
The certificate structure collects three elementary properties of the local cost and threshold: domain cost vanishes on the diagonal for nonzero arguments, is nonnegative when both arguments are positive, and the canonical threshold is positive. Domain cost is the module's specialization of the RS J-cost comparison between a mass-like and an energy-like coordinate; the canonical threshold is the positive cutoff used to gate the match.
Upstream, the structure itself is only a Prop-carrying record; inhabitedness is what turns the three lemmas into a single exportable unit.
proof idea
Term-mode one-liner. Nonempty is introduced by the anonymous constructor ⟨cert⟩, where cert is the in-module value already assembled from the three component proofs (diagonal vanishing, nonnegativity, threshold positivity). No tactics, no further lemmas.
why it matters
Gives the module a single inhabited certificate object so downstream physics exports can require Nonempty RSPhysics010Cert rather than three separate hypotheses. Fits the RS mass-formula pattern (yardstick times $\phi$ to a rung offset) and the structural-theorem discipline of the forcing chain: cost nonnegativity and diagonal zero are the local echoes of J-cost axioms (T5 / RCL), while threshold positivity keeps the match gate well-defined. No further used-by edges are recorded yet; the declaration closes the module's export surface rather than feeding a named parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.