phi_pow70_gt
plain-language theorem explainer
Golden ratio to the 70th power exceeds 425698000000000. Mass verification code in Recognition Science cites the bound when checking the phi-ladder formula at rung 70. The argument rewrites the exponent as 54 plus 16, invokes the pre-proved lower bounds for those powers, and chains the target constant through norm_num and nlinarith.
Claim. $425698000000000 < ((1 + sqrt(5))/2)^{70}$
background
The module Numerics.Interval.PhiBounds supplies rigorous numerical bounds on powers of the golden ratio φ = (1 + √5)/2. It starts from the algebraic inequalities 2.236² < 5 < 2.237² that yield 1.618 < φ < 1.6185 and then refines these stepwise to higher exponents for mass verification. The present theorem depends on the upstream lemmas phi_pow54_gt (φ^54 > 192894126000) and phi_pow16_gt (φ^16 > 2206.9).
proof idea
The proof first rewrites φ^70 as φ^54 * φ^16 via ring_nf. It obtains the lower bounds from phi_pow54_gt and phi_pow16_gt, establishes positivity of both powered terms, and chains the target constant through norm_num followed by two applications of nlinarith.
why it matters
The bound is invoked by phi70_gt in Masses.Verification (after rewriting phi to goldenRatio) and by the subsequent phi_pow76_gt. It supplies a concrete numerical anchor for the phi-ladder mass formula at high rungs, where φ is the self-similar fixed point forced at step T6 of the unified forcing chain. The result closes a numerical gap needed for concrete mass predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.