phi_pow_6_bounds
plain-language theorem explainer
The declaration proves that the sixth power of the golden ratio satisfies 17 < φ⁶ < 18. Researchers modeling quark and lepton mass hierarchies cite it to bound the bottom-to-strange ratio or the tau-to-muon ratio after rung corrections. The proof rewrites φ⁶ via the Fibonacci identity to 8φ + 5 and invokes linear arithmetic on the established bounds 1.5 < φ < 1.62.
Claim. $17 < φ^6 < 18$, where $φ = (1 + √5)/2$ is the golden ratio and φ^6 supplies the generation mass ratio bound via the phi-ladder.
background
In Recognition Science the golden ratio φ is the self-similar fixed point forced at T6. Particle masses sit on the phi-ladder as yardstick × φ^(rung − 8 + gap(Z)). The module supplies machine-verified intervals for every key RS prediction, with φ^6 listed for the generation mass ratio m_b/m_s ~ 17.9. Upstream supplies the exact identity φ^6 = 8φ + 5 (Fibonacci recurrence) together with the tight bounds 1.5 < φ and φ < 1.62.
proof idea
The term proof first rewrites the sixth power by the upstream identity phi_sixth_eq, then splits the conjunction and applies linarith to the lower bound phi_gt_onePointFive on the left and to the upper bound phi_lt_onePointSixTwo on the right.
why it matters
The result is invoked directly by bottom_strange_ratio_bounds to certify m_b/m_s = φ^6 ∈ (17,18), by tau_muon_ratio_bounds for the tau/muon ratio, and by top_charm_ratio_bounds. It populates the φ^6 row in the module table of proved predictions and supports the mass formula on the phi-ladder. The parent structure NumericalPredictionsCert aggregates all such bounds into a single verified certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.