cert
plain-language theorem explainer
Packages a three-field certificate that the domain cost vanishes on equal arguments, stays non-negative for positive mass and energy, and that the canonical threshold is positive. Anyone citing the structural proton-radius-from-J-cost claim in the foundation layer uses this inhabitant. The body is a pure structure assembly wiring three already-proved field lemmas.
Claim. There is a certificate consisting of: (i) for every nonzero real $r$, the domain cost of $(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
The module treats the proton charge radius as a structural consequence of the Recognition Science J-cost on a phi-ladder, not as a fitted length. Status is a structural theorem with no sorry and no axioms. The experimental target 0.841 fm is mentioned only as orientation; the local claim is algebraic, not a numerical match to femtometers.
Domain cost is the cost functional restricted to the mass/energy (or radius) pair that the certificate tracks. The structure ProtonRadius3Cert demands three properties: diagonal vanishing (equal arguments cost nothing), nonnegativity for positive inputs, and a strictly positive canonical threshold against which the cost is compared.
Upstream, nonnegativity of recognition cost is already known from the observer-forcing layer: every recognition event has cost at least zero because the underlying J-cost is nonnegative on positive states. The present certificate reuses that style of bound at the domain-cost level.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional tactics or algebraic work occur in the body; it only witnesses that those three facts assemble into ProtonRadius3Cert.
why it matters
Gives a single named certificate object for the foundation module on proton radius from J-cost. Downstream consumers (none yet recorded in the graph) can take the whole bundle rather than re-proving diagonal vanishing, nonnegativity, and threshold positivity separately.
In the Recognition framework this sits under the structural reading of length scales from the J-cost and the phi-ladder (T5 J-uniqueness, T6 phi fixed point, T8 forcing D = 3). The module doc frames the radius as structural, not a fit: the certificate is the Lean packaging of that structural claim's cost-side hypotheses.
It does not close a numerical prediction gap; it only certifies the cost inequalities the structural story needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.