IndisputableMonolith.Physics.ProtonRadius
This module establishes the muon-electron mass ratio as phi to the eleventh power via explicit rung assignments on the phi-ladder, together with supporting lemmas and a proton radius estimate. Physicists applying Recognition Science mass formulas would cite these relations for lepton and hadron properties. The content consists of a chain of lemmas on phi positivity and inequalities that directly enable the rung-difference calculation.
claim$m_\mu / m_e = \phi^{11}$ with electron rung 2 and muon rung 13; proton radius estimate follows the same phi-ladder scaling.
background
The module sits inside the Recognition Science derivation of particle masses from the single functional equation. It imports JcostCore, which supplies the J-cost function J(x) = (x + x^{-1})/2 - 1 and the composition law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The supplied doc comment fixes the rung difference of 11 between the electron (rung 2) and muon (rung 13).
Sibling declarations include positivity and ordering lemmas for phi together with the explicit ratio theorem and the proton-radius estimate. These rest on the phi-ladder mass formula yardstick * phi^(rung - 8 + gap(Z)) already present in the upstream JcostCore definitions.
proof idea
The module opens with basic lemmas establishing phi > 1 and phi positivity, then applies the rung-difference arithmetic to obtain the mass-ratio theorem, and closes with the radius estimate. Each step is a direct algebraic consequence of the J-cost identities imported from JcostCore; no separate tactic scripts are required beyond the imported lemmas.
why it matters in Recognition Science
The module supplies the concrete lepton mass ratio and proton radius relations required by the Recognition Science mass formula. It realizes the T5 J-uniqueness and T6 phi fixed-point steps for the specific case of charged leptons. Although no downstream declarations are listed, the results feed the framework's physics calculations that connect the eight-tick octave and D = 3 to observable particle properties.
scope and limits
- Does not derive phi itself from the forcing chain.
- Does not compare the radius estimate to experimental values.
- Does not treat particles other than the electron, muon, and proton.
- Does not invoke the alpha band or G, c, hbar constants.
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