lepton_pred_eq_aux
plain-language theorem explainer
The auxiliary lemma equates the Recognition Science mass formula for a lepton at rung r to phi raised to n divided by 4194304000000 in MeV, under the relation n equals 57 plus r. Researchers comparing predicted lepton masses against PDG experimental values would cite this result to obtain the explicit phi-power expressions for the electron, muon, and tau. The proof reduces the expression by substituting the lepton-specific exponent offsets and combining powers of phi via the given integer relation.
Claim. The RS-predicted lepton mass at rung $r$ satisfies $m(r) = phi^n / 4194304000000$ (in MeV) whenever $n = 57 + r$.
background
In the mass verification module the function rs_mass_MeV computes the predicted mass in MeV for a given sector and rung via the expression (2)^(B_pow s) * phi^(-5) * phi^(r0 s) * phi^r / 1000000. For the lepton sector, B_pow equals -22 and r0 equals 62, as stated by the theorems B_pow_Lepton_eq and r0_Lepton_eq. These offsets are derived from wallpaper group structure and cube-face geometry rather than chosen arbitrarily. The module performs a quarantined comparison of these integer-rung predictions to PDG 2024 experimental data for the three charged leptons.
proof idea
The proof unfolds the rs_mass_MeV definition and simplifies using the lepton-specific B_pow and r0 equalities. It establishes that phi is nonzero, combines the three phi powers into a single phi^n term via the hypothesis and zpow_add, then applies a conv tactic to isolate the 2^(-22) factor. This factor is rewritten as the reciprocal of 4194304, after which field_simp and ring close the equality.
why it matters
This lemma supplies the common algebraic reduction used by the explicit predictions electron_pred_eq, muon_pred_eq, and tau_pred_eq. It instantiates the lepton-sector mass formula m(Lepton, r) = phi^(57+r) / (2^22 * 10^6) in MeV that is compared to PDG data. Within the Recognition Science framework it realizes the phi-ladder mass formula for leptons, where the rung offsets follow from the eight-tick octave and the three spatial dimensions. The result closes the verification path for these three particles with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.