phi_pow_7_lt_30
plain-language theorem explainer
Physicists modeling neutrino mass hierarchies cite the bound φ^7 < 30 to place the ratio m₃²/m₂² inside the interval (28, 30). The result follows from the algebraic reduction of φ^7 to the linear form 13φ + 8 together with the numerical upper limit φ < 1.62. This one-line wrapper completes the sandwich inequality for the neutrino prediction on the phi-ladder.
Claim. $φ^7 < 30$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module proves machine-verified inequalities for Recognition Science predictions using only algebraic identities and rational arithmetic. The golden ratio satisfies φ² = φ + 1, so every higher power reduces to a linear combination aφ + b with integer coefficients. The upstream lemma phi_pow_7_eq supplies the explicit identity φ^7 = 13φ + 8. A separate upstream result establishes the concrete bound φ < 1.62.
proof idea
This is a one-line wrapper. The rewrite step invokes phi_pow_7_eq to replace φ^7 by 13φ + 8. Linear arithmetic then closes the proof with the imported bound phi_lt_onePointSixTwo.
why it matters
The declaration supplies the upper half of phi_pow_7_bounds, which asserts 28 < φ^7 < 30. That interval contains the experimental neutrino squared-mass ratio m₃²/m₂² ≈ 29.0 and thereby validates the phi-ladder prediction for the neutrino sector. The result sits inside the chain that derives mass ratios from the self-similar fixed point of φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.