tau_pred
plain-language theorem explainer
tau_pred supplies the Recognition Science prediction for the tau lepton mass as phi to the 76th power divided by 4194304000000 MeV. Researchers verifying the phi-ladder against PDG data cite this value inside certification structures and bound theorems. The declaration is a direct noncomputable definition with no reduction steps or proof obligations.
Claim. The predicted tau lepton mass is $m_τ = φ^{76} / 4194304000000$ MeV, where $φ$ is the golden ratio constant from the CPM bundle and the exponent corresponds to rung 19 on the lepton ladder.
background
The Masses.Verification module compares RS mass predictions to PDG 2024 data for the lepton sector. The module documentation states the lepton formula $m(Lepton, r) = φ^{57+r} / (2^{22} × 10^6)$ MeV with B_pow = -22 and r0 = 62; tau_pred instantiates the r = 19 case. The upstream Constants structure from CPM.LawOfExistence is an abstract bundle that supplies the phi constant appearing in the expression.
proof idea
The declaration is a one-line definition that directly assigns the phi-power expression for the tau rung.
why it matters
tau_pred is referenced by MassVerificationCert to assert the tau prediction lies in (1821, 1823) and by phi_ladder_verified to confirm the relative error against m_tau_exp is under 0.03. It fills the tau slot in the lepton mass ladder verification described in the module documentation. This supports the phi-ladder model in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.