tau_pred_eq
The equality rs_mass_MeV(Lepton, 19) = tau_pred holds by direct instantiation of the lepton auxiliary lemma. Researchers verifying the phi-ladder mass predictions against PDG data cite this to close the tau rung in the verification chain. The proof is a one-line application of lepton_pred_eq_aux with exponent 76 and rung 19, discharging the relation via norm_num.
claimFor the lepton sector at rung 19, the recognition-science mass in MeV equals the explicit phi-power tau prediction: $rs_mass_{MeV}(Lepton, 19) = phi^{76}/4194304000000$.
background
In the Masses.Verification module the RS mass in MeV for sector s and rung r is defined by rs_mass_MeV(s, r) = 2^{B_pow(s)} * phi^{-5} * phi^{r0(s)} * phi^r / 10^6. For the lepton sector this reduces to the phi-ladder formula with B_pow = -22 and r0 = 62, giving masses in MeV units. The explicit tau_pred is the case phi^{76}/4194304000000. The module compares these predictions to PDG 2024 values while treating experimental masses as imported constants. The auxiliary lemma lepton_pred_eq_aux states that whenever n = -5 + 62 + r then rs_mass_MeV(Lepton, r) = phi^n / 4194304000000.
proof idea
This is a one-line wrapper that applies lepton_pred_eq_aux to the arguments 76, 19 together with a norm_num proof of the exponent equality -5 + 62 + 19 = 76.
why it matters in Recognition Science
The result is invoked in tau_relative_error to bound the relative deviation from the experimental tau mass and in phi_ladder_verified to establish the full lepton error bounds below 3 percent. It supplies the tau case in the direct verification that the phi-ladder model matches PDG tolerances, superseding the earlier mass_ladder_assumption. Within the Recognition Science framework this closes the rung-19 instance of the lepton mass formula on the phi-ladder.
scope and limits
- Does not derive the experimental tau mass from first principles.
- Does not extend the equality to quark or boson sectors.
- Does not claim exact numerical agreement with the PDG value, only equality to the RS formula.
- Does not address variation of phi or higher-order corrections.
Lean usage
rw [tau_pred_eq]formal statement (Lean)
79theorem tau_pred_eq : rs_mass_MeV .Lepton 19 = tau_pred :=
proof body
Term-mode proof.
80 lepton_pred_eq_aux 76 19 (by norm_num)
81
82/-! ## Phi-Power Transfer Lemmas -/
83