ProtonRadius3Cert
plain-language theorem explainer
Certificate structure that packages three structural hypotheses for extracting the proton charge radius from domain cost on the phi-ladder: diagonal vanishing, non-negativity on positive arguments, and a positive canonical threshold. Anyone citing the Foundation or Physics proton-radius modules depends on an inhabitant of this bundle. It is a pure structure definition with no proof body; inhabitation is discharged by sibling lemmas.
Claim. A proton-radius certificate is a triple of properties: (i) for every real $r \neq 0$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all $m,e > 0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats the proton charge radius as a structural consequence of the Recognition Science cost calculus on the phi-ladder (with spatial dimension $D = 3$ from the forcing chain). Domain cost is the local cost functional on pairs of positive reals (mass/energy or scale arguments); it is built from the unique J-cost $J(x) = (x + x^{-1})/2 - 1$ forced by the Recognition Composition Law. The canonical threshold is the positive cutoff against which that cost is compared when fixing the radius scale.
Upstream, non-negativity of recognition-event cost is already known: every recognition event has cost $\ge 0$ because $J$ is nonnegative on the positive reals. The present structure lifts that idea to the two-argument domain cost used for the proton-radius derivation, and adds diagonal vanishing (perfect match costs nothing) plus threshold positivity.
Local status is structural: zero sorry, zero axiom. Numerical sketches in the module header ($r_p \sim \phi^k \ell_{\mathrm{Pl}}$ or $\phi^{-D}$ times an electron Compton length) motivate the scale but are not part of the certificate itself.
proof idea
No proof body: this is a structure declaration. It simply names three fields that any valid certificate must supply: diagonal vanishing of domain cost, non-negativity of domain cost on positive arguments, and positivity of the canonical threshold. Downstream cert fills the fields by applying the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then wraps that inhabitant as Nonempty.
why it matters
This certificate is the interface between the J-cost foundation and the proton-radius claim. Both Foundation and Physics copies of the module inhabit it (cert, cert_inhabited), so any later theorem that quotes a certified proton radius from domain cost depends on these three properties being available as a single package.
In the broader framework it sits under the structural (not numerical) reading of the proton charge radius on the phi-ladder, with $D = 3$ from T8 and the unique J from T5/RCL. The module header flags the target experimental scale $\sim 0.841,\mathrm{fm}$ while stressing that the formal content here is structural: cost vanishes on match, never goes negative, and the threshold used to cut the ladder is positive. Closing a full numerical match to $0.841,\mathrm{fm}$ remains outside this declaration; the certificate only locks the cost-theoretic hypotheses that such a derivation may assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.