IndisputableMonolith.Foundation.ProtonRadius3FromJCost
Certificate module linking a dimensionless proton-radius ratio to the unique J-cost at a fixed positive threshold. It packages nonnegativity and evaluation identities for a domain cost, then inhabits a ProtonRadius3Cert record. Cite when closing the geometric step that forces the factor three from cost geometry rather than from QCD fitting. The argument is definitional packaging plus elementary positivity, not a long derivation.
claimDefine a domain cost $C$ built from the unique $J$-cost $J(x)=(x+x^{-1})/2-1$, record $C\ge 0$ and its value at the equality locus, fix a canonical positive threshold $\tau_*>0$, and inhabit a certificate $\mathrm{ProtonRadius3Cert}$ asserting that the proton-radius factor three is the geometric content of that thresholded cost identity.
background
Recognition Science forces a unique nonnegative cost $J$ on ratios (T5): $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$, satisfying the Recognition Composition Law. The Cost import supplies that functional; Constants supplies the RS tick $\tau_0=1$ and related native units.
This module works in the Foundation layer. It introduces a domain-restricted cost (evaluation of $J$ on a geometric domain relevant to the proton length scale), proves elementary nonnegativity and an on-locus evaluation identity, and names a positive canonical threshold against which the cost is compared.
The certificate type bundles those facts into a single inhabited record so downstream radius or mass-ladder arguments can assume the factor-three claim without reopening the cost algebra.
proof idea
Definition-and-certificate module, not a deep proof script. domainCost is introduced from $J$; domainCost_nonneg and domainCost_at_eq are short positivity/evaluation lemmas. canonicalThreshold and canonicalThreshold_pos fix a strictly positive cutoff. ProtonRadius3Cert is a structure; cert and cert_inhabited supply a concrete inhabitant wiring the cost identities to the threshold. No multi-step tactic chain beyond packaging.
why it matters in Recognition Science
Places the proton-radius factor three on the same J-uniqueness footing as the rest of the forcing chain (T5), rather than as an external QCD input. Downstream radius or ladder identities can consume ProtonRadius3Cert as a black-box geometric fact. With no recorded used_by edges yet, the module is a Foundation leaf meant to be imported by later proton-structure or mass-yardstick developments. It touches the open question of how far pure cost geometry determines hadronic length ratios before dynamics enter.
scope and limits
- Does not derive the experimental proton charge radius in SI units.
- Does not prove QCD form factors or parton dynamics.
- Does not fix numerical $\alpha$ or $G$; only the cost-threshold geometry.
- Does not claim the certificate is consumed by a named parent theorem yet.
- Does not replace the full T0–T8 forcing chain; it assumes $J$-uniqueness.