proton_radius_positive
plain-language theorem explainer
The declaration proves that the Recognition Science proton radius estimate is strictly positive whenever the reduced Compton wavelength parameter and strong coupling are positive. Physicists modeling the proton radius puzzle would cite it to confirm the estimate produces a valid length scale. The proof is a direct term-mode reduction that unfolds the formula and applies standard positivity lemmas for multiplication and square roots.
Claim. If $h > 0$ and $α_s > 0$, then the proton radius estimate $r_p = (1/4) h √(6π / α_s)$ satisfies $r_p > 0$.
background
The module develops the proton charge radius within Recognition Science, following the paper RS_Proton_Radius_Puzzle.tex. The key definition is the proton radius estimate, an explicit formula (1/4) h_over_mpc √(6 π / α_s) obtained from confinement plus form factor corrections. The module imports JcostCore to embed the estimate inside the broader cost framework of Recognition Science.
proof idea
The proof is a term-mode derivation. It unfolds proton_radius_estimate to expose the product and square root, then applies mul_pos twice (first with a norm_num constant 1/4 > 0 and the hypothesis on h_over_mpc), and finally invokes Real.sqrt_pos_of_pos together with a positivity tactic on the argument of the square root.
why it matters
The result confirms that the confinement-plus-form-factor estimate remains positive, a basic consistency requirement for any physical radius in the Recognition Science treatment of the proton radius puzzle. It directly supports the paper RS_Proton_Radius_Puzzle.tex by discharging the positivity obligation for the explicit formula. No downstream theorems are recorded, so the lemma functions as a local sanity check inside the Physics.ProtonRadius module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.