raw_prediction_discrepancy
plain-language theorem explainer
Recognition Science bare ladder ratios sit off PDG lepton mass ratios by a few percent: experiment exceeds φ^11 for μ/e and falls short of φ^17 for τ/e. Anyone auditing the raw (pre-radiative) mass ladder cites this inequality pair. The proof is pure interval arithmetic: experimental ratio bounds versus certified φ-power enclosures, closed by linarith.
Claim. The experimental muon-to-electron mass ratio strictly exceeds $\varphi^{11}$, and the experimental tau-to-electron mass ratio is strictly less than $\varphi^{17}$.
background
This module is a quarantined verification layer: it imports PDG 2024 experimental masses and compares them to Recognition Science φ-ladder predictions. The RS mass formula is $m = \mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}}$, with coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$. Lepton ratios therefore collapse to pure powers of $\varphi$ once the common electron yardstick cancels.
The bare RS claims are $m_\mu/m_e=\varphi^{11}$ and $m_\tau/m_e=\varphi^{17}$. Sibling constants supply the experimental ratios ratio_mu_e_exp and ratio_tau_e_exp together with certified numerical enclosures (ratio_mu_e_exp_value, ratio_tau_e_exp_value). Matching enclosures for the golden-ratio powers come from the Numerics.Interval.PhiBounds stack (phi_pow_11_approx, phi_pow_17_approx).
The module doc stresses that these comparisons sit outside the certified surface precisely because experimental inputs are external to the forcing chain.
proof idea
Term-mode proof that packages four numerical facts and closes with linear arithmetic.
- Pull the experimental interval for $\mu/e$ (
ratio_mu_e_exp_value) and for $\tau/e$ (ratio_tau_e_exp_value). - Pull the certified bounds on $\varphi^{11}$ and $\varphi^{17}$ (
phi_pow_11_approx,phi_pow_17_approx). constructorsplits the conjunction.- First goal: lower bound of experiment exceeds upper bound of $\varphi^{11}$, discharged by
linarithon those two inequalities. - Second goal: upper bound of experiment is below lower bound of $\varphi^{17}$, again
linarith.
No algebraic identity about $\varphi$ is proved here; the work is entirely interval comparison.
why it matters
Documents the raw few-percent mismatch between bare φ-ladder lepton ratios and PDG values before radiative corrections. The doc-comment table records $\varphi^{11}\approx 199$ vs experiment $\approx 206.77$ (~4%) and $\varphi^{17}\approx 3571$ vs $\approx 3477$ (~3%), and points to ElectronMass.lean for the claim that $\alpha^2$ and higher corrections close the gap.
In the broader framework this sits downstream of the mass formula (yardstick $\times\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) and of T6 ($\varphi$ as the self-similar fixed point). It does not feed further Lean theorems yet (used_by is empty); it is an audit checkpoint that the bare prediction is systematically off in the stated directions, so any later correction layer must raise $\mu/e$ and lower $\tau/e$.
Because the module is quarantined, this result never enters the certified forcing surface; it only constrains how radiative or anchor refinements are allowed to move the ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.