IndisputableMonolith.Physics.ProtonRadius
The Physics.ProtonRadius module assembles phi-ladder relations for lepton masses and proton radius estimates. Its central result equates the muon-electron mass ratio to phi to the eleventh power via rung difference eleven. Particle physicists modeling mass hierarchies would cite these derivations. The module consists of supporting lemmas on ordering and positivity followed by direct estimates.
claim$m_μ / m_e = φ^{11}$ (electron rung 2, muon rung 13). Additional objects include proton radius estimate and form factor correction on the same ladder.
background
The module sits inside Recognition Science and imports JcostCore to access the J-cost function whose fixed point is phi. Sibling lemmas establish phi positivity, ordering, and the muon-electron ratio from rung arithmetic. The setting uses the mass formula yardstick times phi to the power of (rung minus eight plus gap), with constants fixed in RS-native units.
proof idea
This is a definition and lemma module. Individual results such as muon_electron_ratio follow from rung subtraction and application of phi properties imported from JcostCore; no single overarching proof exists.
why it matters in Recognition Science
The module supplies concrete mass and radius instances that instantiate the phi-ladder mass formula and the T5-T8 forcing chain. It supports later applications to leptonic universality and proton structure while remaining consistent with the Recognition Composition Law and the alpha band.
scope and limits
- Does not derive rung assignments from the J-cost equation.
- Does not incorporate experimental error bars on radius data.
- Does not extend beyond the listed lepton and proton cases.
- Does not address higher-order quantum corrections.
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