phi_pow51_in_interval_proven
plain-language theorem explainer
Golden ratio to the 51st power lies inside the closed rational interval with endpoints 45537548334 and 45537549354. Numerics work on the phi-ladder for mass formulas cites this bound to certify high-rung entries. The proof is a one-line simp that combines the pre-established strict lower and upper bounds with the definition of interval containment and le_of_lt.
Claim. Let $φ = (1 + √5)/2$. Then $45537548334 ≤ φ^{51} ≤ 45537549354$.
background
The module supplies algebraic bounds on powers of the golden ratio using rational approximations to √5. An Interval is a structure with rational endpoints lo and hi satisfying lo ≤ hi. The contains predicate on an interval I and real x holds exactly when lo ≤ x ≤ hi. This theorem depends on the auxiliary results phi_pow51_gt and phi_pow51_lt, which establish the strict inequalities 45537548334 < φ^51 and φ^51 < 45537549354. The module strategy begins from 2.236 < √5 < 2.237 to derive 1.618 < φ < 1.6185 and lifts the bounds to higher powers.
proof idea
The proof is a one-line simp tactic. It unfolds Interval.contains, substitutes the explicit definition of phi_pow51_interval_proven, applies phi_pow51_gt and phi_pow51_lt, and uses le_of_lt to convert the strict inequalities into the required non-strict bounds for membership.
why it matters
The result supplies a certified numerical anchor at exponent 51 on the phi-ladder and is invoked by phi_pow_51_in_interval in the Pow module to bridge to real-arithmetic computations. It supports the Recognition Science mass formula yardstick · φ^(rung-8+gap) and the derivation of constants such as ħ = φ^{-5} inside the eight-tick octave. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.