proton_radius_estimate
plain-language theorem explainer
The Recognition Science proton radius estimate is the algebraic expression one quarter of the reduced Compton wavelength of the proton times the square root of six pi over the strong coupling. Physicists examining the proton radius puzzle would cite this formula as the RS prediction derived from confinement and form factor. The definition is a direct one-line algebraic assignment with no lemmas or reductions.
Claim. The proton charge radius estimate is given by $r_p = (1/4) (h_{over m_p c}) sqrt(6 pi / alpha_s)$, where $h_{over m_p c}$ denotes the reduced Compton wavelength of the proton and $alpha_s$ the strong coupling constant.
background
The module on Proton Charge Radius from Recognition Science sets the local theoretical setting for deriving the proton charge radius, referencing the paper RS_Proton_Radius_Puzzle.tex. This definition supplies the explicit RS estimate obtained from confinement plus form factor considerations. The two real inputs are the reduced Compton wavelength ratio and the strong coupling; no upstream lemmas from JcostCore or elsewhere are invoked.
proof idea
This is a one-line definition whose body is the direct algebraic expression (1/4) * h_over_mpc * Real.sqrt (6 * Real.pi / alpha_s). No lemmas are applied and no tactics are used; the declaration simply names the formula.
why it matters
The definition supplies the concrete formula whose positivity is proved by the downstream theorem proton_radius_positive in the same module. It fills the explicit RS prediction for the proton charge radius in the context of the referenced paper on the proton radius puzzle. The expression connects to the Recognition Science framework through its use of coupling constants and confinement scales, though it does not invoke the forcing chain or RCL directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.