phi_ladder_verified
The phi-ladder mass formula reproduces the electron, muon and tau masses to within 0.3 percent, 4 percent and 3 percent of PDG values. Researchers comparing discrete scale models to experiment would reference this numerical check. The term proof rewrites each predicted mass via its defining equation and invokes the corresponding relative-error lemma.
claimThe relative errors satisfy $|m_e^pred - m_e^exp|/m_e^exp < 0.003$, $|m_μ^pred - m_μ^exp|/m_μ^exp < 0.04$ and $|m_τ^pred - m_τ^exp|/m_τ^exp < 0.03$, where the predictions are given by the Recognition Science lepton mass formula $m(Lepton,r) = φ^{57+r}/(2^{22}×10^6)$ MeV evaluated at rungs 2, 13 and 19.
background
The module treats experimental PDG values as imported constants, quarantined from the certified Recognition Science surface. The lepton-sector formula is $m(Lepton,r) = φ^{57+r}/(2^{22}×10^6)$ MeV, with B_pow = -22 and r0 = 62. The inductive type Lepton enumerates the three charged states; the functions electron_pred, muon_pred and tau_pred are defined via rs_mass_MeV applied to those states at the indicated rungs. Upstream results supply the rung constant, the phi scaling operation, and the structural bridge that packages model state for traceability.
proof idea
The term proof applies three rewrite rules that substitute the explicit definitions of the predicted masses from their equality lemmas (electron_pred_eq, muon_pred_eq, tau_pred_eq), then applies the exact tactic to the triple of pre-established relative-error bounds.
why it matters in Recognition Science
This verification closes the lepton sector of the mass ladder and supersedes the earlier mass_ladder_assumption. It confirms that the phi-ladder formula, derived from J-uniqueness and the phi fixed point (T5-T6), reproduces observed lepton masses to the stated precision. No downstream theorems depend on it yet; it serves as a standalone numerical anchor for the Recognition Science mass predictions.
scope and limits
- Does not derive the PDG values from Recognition Science axioms.
- Does not extend to the quark sector without gap corrections.
- Does not claim exact equality, only the stated relative-error bounds.
- Does not address neutrino masses or mixing angles.
formal statement (Lean)
325theorem phi_ladder_verified :
326 (|electron_pred - m_e_exp| / m_e_exp < 0.003) ∧
327 (|muon_pred - m_mu_exp| / m_mu_exp < 0.04) ∧
328 (|tau_pred - m_tau_exp| / m_tau_exp < 0.03) := by
proof body
Term-mode proof.
329 rw [show electron_pred = rs_mass_MeV .Lepton 2 from electron_pred_eq.symm,
330 show muon_pred = rs_mass_MeV .Lepton 13 from muon_pred_eq.symm,
331 show tau_pred = rs_mass_MeV .Lepton 19 from tau_pred_eq.symm]
332 exact ⟨electron_relative_error, muon_relative_error, tau_relative_error⟩
333
334/-! ## Quark Sector — φ-Ladder Structural Predictions
335
336Quark masses use: rs_mass_MeV(UpQuark, r) = 2^(-1) × φ^(-5) × φ^35 × φ^r / 10^6
337 = φ^(30+r) / 2000000 MeV.
338
339For DownQuark: rs_mass_MeV(DownQuark, r) = 2^23 × φ^(-5) × φ^(-5) × φ^r / 10^6
340 = 2^23 × φ^(r-10) / 10^6 MeV.
341
342The absolute mass scale requires the gap correction Z, which for quarks involves
343large integer Z-charges (ZOf_up ≈ 276, ZOf_down ≈ 24 in the RS bridge).
344The gap-corrected predictions are pending full RSBridge calibration.
345
346What IS proved without gap correction:
347- All quark masses are positive
348- Within-sector mass ratios follow the φ-ladder (generation spacing)
349- The up-charm-top spacing φ^11 and φ^6 respectively reproduce correct orders of magnitude
350-/
351
352/-- The up-quark structural mass (UpQuark sector, rung 4, Z=0 gap correction). -/