IndisputableMonolith.Physics.ProtonRadius
This module assembles definitions and theorems for proton radius estimates together with lepton mass ratios inside the Recognition Science phi-ladder. It records the muon-electron mass ratio as phi to the eleventh power from the rung difference between electron (rung 2) and muon (rung 13). Researchers deriving particle properties from the J-cost function would cite these results. The module consists of positivity facts, ratio lemmas, and radius calculations built directly on the imported JcostCore machinery.
claim$m_μ/m_e = φ^{11}$ with electron rung 2 and muon rung 13. Proton radius follows from the mass formula yardstick × φ^(rung − 8 + gap(Z)) applied to the appropriate rung.
background
Recognition Science derives masses from the J-cost function J(x) = (x + x^{-1})/2 − 1 supplied by the imported JcostCore module. Particle states occupy discrete rungs on the self-similar phi-ladder whose spacing is fixed by the T5 J-uniqueness and T6 phi fixed-point steps. The module introduces auxiliary facts phi_pos and phi_gt_one to guarantee ordering and positivity before computing explicit ratios and radius estimates.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The declarations supply concrete rung assignments and radius estimates that feed the Recognition Science mass formula and the T0-T8 forcing chain. They instantiate the phi-ladder for leptons and the proton, supporting later derivations of constants such as alpha and G in native units.
scope and limits
- Does not derive the J-cost equation or the phi-ladder from first principles.
- Does not incorporate experimental error bars on measured radii or masses.
- Does not treat particles other than electrons, muons, and protons.
- Does not address form-factor corrections beyond the listed sibling.
depends on (1)
declarations in this module (13)
-
theorem
phi_pos -
theorem
phi_gt_one -
def
muon_electron_ratio -
theorem
muon_heavier -
theorem
muon_ratio_pos -
theorem
muonic_smaller -
def
proton_radius_estimate -
theorem
proton_radius_positive -
abbrev
proton_radius_codata -
theorem
leptonic_universality -
theorem
old_value_differs -
def
form_factor_correction -
theorem
form_factor_near_one