tau_muon_ratio_bounds
plain-language theorem explainer
Recognition Science places the tau-muon mass ratio on the phi-ladder at rung difference 6, yielding the prediction m_tau/m_mu approx phi^6. This theorem supplies the machine-checked interval 17 < phi^6 < 18 that contains the measured value near 17.9. Lepton spectroscopists and RS model builders cite the bound when testing generation hierarchies against data. The proof is a direct one-line reference to the algebraic identity for phi^6 together with the established bounds on phi.
Claim. $17 < phi^6 < 18$, which bounds the Recognition Science prediction for the tau-muon mass ratio $m_τ/m_μ ≈ phi^6$.
background
Recognition Science assigns particle masses to rungs on a phi-ladder, with ratios between generations given by integer powers of the golden ratio phi = (1 + sqrt(5))/2. The module establishes rigorous algebraic bounds on these powers so that each predicted interval contains the corresponding experimental mass ratio. The upstream result phi_pow_6_bounds proves the same interval for phi^6 by rewriting it as 8*phi + 5 via the Fibonacci identity and applying linear arithmetic to the known bounds 1.5 < phi < 1.62.
proof idea
One-line wrapper that directly invokes phi_pow_6_bounds.
why it matters
The declaration supplies one entry in the module's table of verified numerical predictions, confirming that the RS mass formula reproduces the observed tau-muon ratio inside a formally proved interval. It rests on the self-similar fixed point phi (T6) and the eight-tick octave structure that generates the rung spacings. No downstream theorems depend on it in the current graph, but it closes the numerical check for lepton generation ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.