phi_pow5_lt
plain-language theorem explainer
The inequality establishes that the fifth power of the golden ratio satisfies φ^5 < 11.1. Numerics specialists working inside the Recognition Science framework cite the bound when confirming interval membership for φ^5 during ladder and constant calculations. The short proof reduces the power via the algebraic identity φ^5 = 5φ + 3, then applies the pre-established upper bound φ < 1.6185 together with linear arithmetic.
Claim. $φ^5 < 11.1$, where $φ = (1 + √5)/2$ is the golden ratio.
background
The module supplies rigorous numerical bounds on the golden ratio φ = (1 + √5)/2 by leveraging algebraic relations among its powers and tight bounds on √5. The strategy begins with 2.236² < 5 < 2.237² to obtain 1.618 < φ < 1.6185, with further refinements for tighter intervals as needed for downstream constants.
proof idea
The proof first rewrites the target using the identity φ^5 = 5φ + 3 supplied by phi_pow5_eq. It then invokes the bound φ < 1.6185 from phi_lt_16185 and closes the resulting linear inequality with linarith.
why it matters
This bound feeds the interval-containment result for φ^5 in the Pow module. In the Recognition framework it anchors numerical checks on the phi-ladder, where φ is the self-similar fixed point forced at T6 and enters the mass formula as yardstick · φ^(rung − 8 + gap(Z)). The result also supports placement of constants such as G = φ^5 / π inside the required precision band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.