phi_pow_7_bounds
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.