phi_pow58_gt
plain-language theorem explainer
A lower bound of 1.3219 × 10^12 holds for the 58th power of the golden ratio. Workers on phi-power chains in Recognition Science numerics cite it to derive reciprocal estimates. The argument reduces the claim to a product of two earlier bounds and closes the inequality with linear arithmetic.
Claim. $1.3219 × 10^{12} < φ^{58}$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module develops rigorous numerical bounds for powers of the golden ratio φ using its algebraic definition and properties of real numbers. It starts from interval bounds on √5 derived from integer squares and lifts them to φ and its powers. Upstream results include the multiplicative equality φ^58 = φ^54 × φ^4 together with the separate lower bounds φ^54 > 192894126000 and φ^4 > 6.854.
proof idea
The tactic proof first rewrites via the equality theorem for the 58th power. It then pulls in the lower bounds for the 54th and 4th powers, asserts positivity of those powers, and executes a calc block that compares the target constant to the product of the bounds before applying nlinarith to transfer the inequalities.
why it matters
This theorem supplies the key inequality needed for the reciprocal bound on φ^{-58}. Within the Recognition Science framework it supports numerical control of the phi-ladder appearing in mass formulas and derivations of constants such as the inverse fine-structure constant lying in (137.030, 137.039). It forms part of the verified bounds around the self-similar fixed point phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.