phi_inv5_interval_proven
plain-language theorem explainer
This definition supplies a closed rational interval [0.089, 0.091] certified to contain (φ^{-1})^5. Numerics researchers in Recognition Science cite it when bounding inverse powers of the golden ratio. The construction is a direct definition whose validity reduces to a single norm_num tactic.
Claim. Define the closed interval $I = [89/1000, 91/1000]$ with rational endpoints satisfying $89/1000 ≤ 91/1000$.
background
The module provides rigorous bounds on the golden ratio φ = (1 + √5)/2 using algebraic properties of squares and successive decimal refinements. It begins with 2.236² < 5 < 2.237² to obtain 1.618 < φ < 1.6185 and extends this approach to powers including (φ^{-1})^5.
proof idea
This is a definition that directly sets the lower bound to 89/1000 and the upper bound to 91/1000. The validity condition lo ≤ hi is discharged by the norm_num tactic.
why it matters
This interval definition is used by the theorem phi_inv5_in_interval_proven to establish containment of (goldenRatio^{-1})^5 and by definitions in the Pow module for φ^{-5} bounds. It fills a numerical slot in the Recognition Science framework for the self-similar fixed point φ and supports constants such as ħ = φ^{-5}. The work contributes to closing scaffolding around the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.