RSPhysics009Cert
plain-language theorem explainer
Certificate bundle for Physics Module 9 (proton-electron mass ratio scaffolding): diagonal domain cost vanishes, domain cost is nonnegative on positive reals, and the canonical threshold is strictly positive. Downstream code cites the inhabited instance `cert`. Pure structure definition; no proof obligations live here.
Claim. A certificate is a triple of facts: (1) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (2) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (3) the canonical threshold is strictly positive.
background
Physics RS Module 9 targets the proton-electron mass ratio in the Recognition Science ladder picture. The module notes the bare rung estimate $\phi^{12}\approx 321.9$ and the residual factor $\sim 5.7$ gap to the empirical ratio $\approx 1836$, flagged as needing a correction term. Status is structural: zero sorry, zero axioms.
The certificate packages three elementary cost/threshold properties used by that scaffolding. Domain cost is the module-local cost on pairs of positive reals (siblings prove it vanishes on the diagonal and is nonnegative off it). Canonical threshold is the positive cutoff against which mass-ratio or gap comparisons are judged. Upstream, the global recognition cost is already known nonnegative: any recognition event has cost $\ge 0$ via nonnegativity of the $J$-cost on positive states.
Together these facts give a minimal, checkable interface before any numerical mass-ratio claim is asserted.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements. Inhabitation is discharged later by the noncomputable definition cert, which plugs in the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. cert_inhabited then wraps that term as Nonempty.
why it matters
Gives Module 9 a single named certificate type so downstream proofs can depend on one object rather than three loose lemmas. Parents are the concrete inhabitant cert and the nonempty theorem cert_inhabited. In the broader RS chain this sits under mass-ladder bookkeeping (yardstick times $\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$), not under the forcing chain T5–T8 itself. It does not close the $\sim 5.7$ gap from $\phi^{12}$ to $1836$; it only certifies the cost/threshold hygiene the module needs before that correction is stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.