phi_pow5_gt
plain-language theorem explainer
The declaration proves that the golden ratio raised to the fifth power exceeds 11.09. Numerics researchers verifying Recognition Science constants would cite this bound when checking interval containment for phi-powered expressions. The proof reduces the target via the closed algebraic form for phi^5 and applies linear arithmetic to the known lower bound on phi.
Claim. $11.09 < ((1 + sqrt(5))/2)^5$
background
This module supplies rigorous numerical bounds on the golden ratio φ = (1 + √5)/2 by leveraging algebraic identities and comparisons with rational approximations to √5. The local strategy begins with the inequalities 2.236 < √5 < 2.237 to derive 1.618 < φ < 1.6185, with tighter variants available for higher precision.
proof idea
The proof is a one-line wrapper that first rewrites the target inequality using the equality φ^5 = 5φ + 3. It then imports the hypothesis 1.618 < φ and concludes via linear arithmetic that 5φ + 3 exceeds 11.09.
why it matters
This bound supports the interval containment theorem for φ^5 in the Pow module, which in turn verifies numerical consistency for Recognition Science quantities such as the gravitational constant expressed in native units. It closes a small link in the forcing chain by confirming that φ^5 lies above the threshold needed for the phi-ladder mass formulas and the alpha inverse band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.