phi_pow_7_bounds
The theorem establishes that 28 < φ^7 < 30 where φ is the golden ratio. Neutrino physicists citing Recognition Science predictions for the squared-mass ratio m₃²/m₂² would reference this bound to confirm the interval containing the NuFIT value ≈29.0. The proof is a one-line wrapper that pairs the separate lower and upper bound theorems already proved in the same module.
claim$28 < φ^7 < 30$ where $φ = (1 + √5)/2$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
The module Machine-Verified Numerical Predictions proves rigorous bounds on Recognition Science quantities using only algebraic identities and rational arithmetic. The golden ratio φ emerges from the forcing chain as the self-similar fixed point and serves as the yardstick in the mass formula on the phi-ladder. This local setting supplies machine-checked intervals that contain measured values without floating-point approximation or calibration anchors.
proof idea
The proof is a one-line wrapper that applies the conjunction of the upstream theorems phi_pow_7_gt_28 and phi_pow_7_lt_30. Those lemmas rewrite via phi_pow_7_eq and close the inequalities by linarith using the bounds φ > 1.618 and φ < 1.62 supplied by PhiBounds.
why it matters in Recognition Science
This declaration supplies the interval (28,30) for φ^7 that is used by the downstream theorem neutrino_squared_mass_ratio to establish the prediction m₃²/m₂² ∈ (29,30) matching NuFIT 5.3 data ≈29.0. It realizes the T6 phi forced as self-similar fixed point and the mass formula on the phi-ladder within the T0-T8 forcing chain. It closes a proved step in the numerical predictions without remaining hypotheses.
scope and limits
- Does not compute absolute neutrino masses.
- Does not address mixing angles or CP phases.
- Does not derive the ratio from experimental calibration.
- Does not extend beyond the phi-ladder mass predictions.
Lean usage
theorem neutrino_squared_mass_ratio : (29 : ℝ) < phi ^ 7 ∧ phi ^ 7 < (30 : ℝ) := by exact ⟨phi_pow_7_gt_29, phi_pow_7_bounds.2⟩formal statement (Lean)
72theorem phi_pow_7_bounds : (28 : ℝ) < phi ^ 7 ∧ phi ^ 7 < (30 : ℝ) :=
proof body
Term-mode proof.
73 ⟨phi_pow_7_gt_28, phi_pow_7_lt_30⟩
74
75/-- φ⁷ > 29: tighter lower bound for the neutrino prediction.
76 Uses phi > 1.618 (from PhiBounds) since 13 × 1.618 + 8 = 29.034 > 29. -/