ratio_tau_e_exp_value
plain-language theorem explainer
The experimental tau-to-electron mass ratio sits strictly between 3477 and 3478. Mass-comparison and discrepancy analyses cite this bound when contrasting PDG data with the RS φ-ladder prediction φ^17 ≈ 3571. The proof unfolds the ratio of the two experimental mass constants and closes both inequalities by numerical normalization.
Claim. The experimental mass ratio $m_\tau^{\mathrm{exp}}/m_e^{\mathrm{exp}}$ satisfies $3477 < m_\tau^{\mathrm{exp}}/m_e^{\mathrm{exp}} < 3478$.
background
This module compares Recognition Science mass predictions against PDG 2024 values. It is quarantined from the certified surface because it imports experimental numbers and uses the anchor/φ-ladder mass system rather than deriving masses from first principles alone.
RS masses take the form $m(\mathrm{species}) = \mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}}$, with coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$. Electron mass in RS units is the rung-2 value $E_{\mathrm{coh}}\cdot\varphi^2$. The experimental constants $m_\tau^{\mathrm{exp}}$ and $m_e^{\mathrm{exp}}$ are PDG inputs; their ratio is the quantity bounded here.
The surrounding numerical-bounds section packages such interval facts so later discrepancy theorems can compare experiment to pure powers of $\varphi$ without redoing floating-point work.
proof idea
Unfold the definition of the experimental ratio into the quotient of the two experimental mass constants. Split the conjunction and discharge each strict inequality with norm_num, which evaluates the concrete rational (or decimal) PDG values to place the quotient in $(3477,3478)$. No external lemmas are required beyond definitional unfolding and numeric normalization.
why it matters
Feeds the key discrepancy theorem raw_prediction_discrepancy, which records that RS predicts $\varphi^{17}\approx 3571$ for $m_\tau/m_e$ while experiment lies near 3477 (about 3% low on the RS side). That parent result pairs the present bound with the analogous muon-electron experimental interval and the pure powers $\varphi^{11}$ and $\varphi^{17}$.
In the broader framework the mass formula is the φ-ladder yardstick construction; the eight-tick/octave and $D=3$ forcing steps fix the discrete rung structure, but radiative corrections in $\alpha^2$ and higher are claimed to close the few-percent gap (see ElectronMass). This lemma is the certified experimental anchor for the tau/electron column of that comparison table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.