phi_pow_6_bounds
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 in Recognition Science
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.
scope and limits
- Does not fix the exact experimental mass ratio value.
- Does not derive the specific rung numbers for any particle.
- Does not incorporate higher-order corrections to the phi power.
- Does not prove existence or stability of the particles involved.
Lean usage
theorem bottom_strange_ratio_bounds : (17 : ℝ) < phi ^ 6 ∧ phi ^ 6 < (18 : ℝ) := phi_pow_6_boundsformal statement (Lean)
48theorem phi_pow_6_bounds : (17 : ℝ) < phi ^ 6 ∧ phi ^ 6 < (18 : ℝ) := by
proof body
Term-mode proof.
49 have h6 : phi ^ 6 = 8 * phi + 5 := phi_sixth_eq
50 constructor
51 · rw [h6]; linarith [phi_gt_onePointFive]
52 · rw [h6]; linarith [phi_lt_onePointSixTwo]
53
54/-- φ⁷ ∈ (28, 30): the neutrino squared-mass ratio m₃²/m₂² = φ⁷.
55 This is the sharpest seam-free prediction of the framework.
56 Uses φ⁷ = φ·φ⁶ = φ(8φ+5) = 8φ²+5φ = 8(φ+1)+5φ = 13φ+8. -/