cert_inhabited
plain-language theorem explainer
The certificate type for Physics Module 9 (proton-electron mass-ratio scaffolding) is nonempty. Anyone citing structural completeness of this module uses this fact. The proof is a one-line term that packages the existing certificate value into a Nonempty witness.
Claim. There exists a certificate asserting: the domain cost vanishes on equal nonzero arguments, $C(r,r)=0$ for $r\neq 0$; the domain cost is nonnegative for positive mass arguments; and the canonical threshold is strictly positive.
background
Physics RS Module 9 treats the proton-electron mass ratio in Recognition Science units. The module notes that $\varphi^{12}\approx 321.9$, leaving a factor-$\sim 5.7$ gap relative to the empirical ratio $\approx 1836$, so the present content is structural rather than a finished mass derivation.
The certificate structure packages three elementary properties of the module's domain cost and threshold: diagonal vanishing of the cost for nonzero equal arguments, nonnegativity of the cost on positive mass pairs, and positivity of the canonical threshold. These are the local standing assumptions against which later mass-ladder or gap corrections would be checked.
The module imports Constants and Cost, so the cost is the RS J-cost family (or a domain specialization of it) already fixed upstream by the forcing chain.
proof idea
One-line term proof. The module already defines a concrete value cert of type RSPhysics009Cert. The theorem is simply the Nonempty introduction ⟨cert⟩, i.e. packaging that value as a witness that the certificate type is inhabited. No further lemmas are applied.
why it matters
Module 9 is marked STRUCTURAL THEOREM (0 sorry, 0 axiom). This inhabitation result closes the certificate interface: downstream consumers can assume a bundle of cost-diagonal, cost-nonnegativity, and threshold-positivity facts without reconstructing them.
In the broader RS picture the proton-electron ratio sits on the $\varphi$-ladder (mass yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). The module itself records that bare $\varphi^{12}$ undershoots 1836 by about 5.7, so the open physics question is the gap correction, not certificate existence. No downstream uses are recorded yet; the lemma is infrastructure for later ratio or gap theorems in this file family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.