phi_pow_7_gt_29
plain-language theorem explainer
The bound 29 < φ^7 tightens the lower edge of the Recognition Science neutrino mass-squared ratio prediction. Neutrino oscillation analysts would cite it when aligning the φ^7 formula against NuFIT 5.3 results. The proof substitutes the algebraic reduction φ^7 = 13φ + 8 and feeds the known inequality φ > 1.618 into linear arithmetic.
Claim. The golden ratio satisfies $29 < φ^7$, where $φ = (1 + √5)/2$.
background
Recognition Science assigns the neutrino squared-mass ratio m₃²/m₂² to the seventh power of the golden ratio φ. The module collects machine-checked bounds showing that each such prediction falls inside an interval that contains the measured value. Here φ^7 is shown to exceed 29, using the identity φ^7 = 13φ + 8 from the sibling lemma and the lower estimate 1.618 < φ imported from the PhiBounds library.
proof idea
Rewrite the target inequality with the lemma phi_pow_7_eq to replace φ^7 by 13φ + 8. Import the fact 1.618 < φ from Numerics.Interval.PhiBounds.phi_gt_1618, unfold the local definition of phi, and close the goal with linarith.
why it matters
The result is invoked inside neutrino_squared_mass_ratio to obtain the complete interval (29, 30) for m₃²/m₂². That theorem records the match to NuFIT data for normal ordering and is listed among the seam-free predictions in the module header. It supplies the missing lower half of the φ^7 entry in the table of verified mass ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.