phi_inv5_gt
plain-language theorem explainer
The inequality establishes a lower bound of 0.089 for the fifth power of the reciprocal of the golden ratio. Numerics researchers verifying constants in Recognition Science would cite this when confirming interval membership for phi-related quantities. The short tactic proof assembles lower bounds on the second and third powers, confirms positivity of the base, rewrites the fifth power as their product, and applies nonlinear arithmetic.
Claim. $0.089 < (φ^{-1})^5$ where $φ = (1 + √5)/2$ is the golden ratio.
background
This module supplies rigorous numerical bounds on the golden ratio and its reciprocal powers using algebraic inequalities derived from bounds on the square root of five. The approach begins with 2.236² < 5 < 2.237² to sandwich √5, then derives corresponding intervals for φ = (1 + √5)/2 and its inverse. The present result builds directly on the earlier theorems establishing (φ^{-1})² > 0.381 and (φ^{-1})³ > 0.2359.
proof idea
The proof invokes the prior results for the second and third powers of the reciprocal golden ratio. It establishes positivity of the base and its powers up to the third. An algebraic identity rewrites the fifth power as the product of the second and third powers. Nonlinear arithmetic then combines these facts to deduce the desired lower bound.
why it matters
This bound contributes to the chain of inequalities that confirm the fifth power of the reciprocal golden ratio lies within a specific interval, as used in the subsequent theorem establishing interval containment. In the Recognition Science framework, such bounds support the use of φ^{-5} as a scaling factor in constants like ħ = φ^{-5}. It closes a numerical verification step in the phi-ladder constructions without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.