phi_pow_7_gt_28
plain-language theorem explainer
Recognition Science predicts the neutrino squared-mass ratio m₃²/m₂² equals φ^7 for the golden ratio φ. This theorem proves the strict lower bound 28 < φ^7. Researchers verifying the framework's mass ladder would cite it to anchor the interval containing the measured value near 29. The proof is a one-line wrapper that substitutes the algebraic identity φ^7 = 13φ + 8 and applies linear arithmetic with φ > 1.61.
Claim. Let φ = (1 + √5)/2 be the golden ratio. Then 28 < φ^7.
background
The module supplies machine-verified inequalities for every key Recognition Science prediction. It establishes that φ^7 lies in (28, 30), which the framework identifies with the neutrino squared-mass ratio m₃²/m₂². The golden ratio satisfies the recurrence φ² = φ + 1, which produces the closed-form identity φ^7 = 13φ + 8. An upstream lemma supplies the auxiliary bound φ > 1.61. The upstream doc-comment states: 'φ⁷ ∈ (28, 30): the neutrino squared-mass ratio m₃²/m₂² = φ⁷. This is the sharpest seam-free prediction of the framework.'
proof idea
This is a one-line wrapper. It rewrites the target inequality by substituting the equality φ^7 = 13φ + 8 from the sibling lemma, then invokes linarith on the known lower bound φ > 1.61 to obtain 13φ + 8 > 28.
why it matters
The result is the lower half of the parent theorem that packages both sides of the interval (28, 30). That parent theorem confirms the Recognition Science mass-ladder prediction for the neutrino ratio. It supports the phi-ladder construction (T6) and the eight-tick octave structure by delivering a formally checked numerical anchor without floating-point evaluation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.