phi_inv_lt
plain-language theorem explainer
The declaration establishes the strict inequality φ^{-1} < 0.6186 for the golden ratio reciprocal. Numerics specialists in Recognition Science cite it to control error terms when enclosing powers of φ^{-1} inside intervals. The proof reduces the claim via the algebraic identity φ^{-1} = φ - 1 and closes it with the companion bound φ < 1.6185 using linear arithmetic.
Claim. $φ^{-1} < 0.6186$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module Numerics.Interval.PhiBounds develops rigorous decimal bounds on the golden ratio φ by starting from rational approximations to √5. The Interval structure provides a closed interval with rational endpoints lo ≤ hi. Upstream results include the identity theorem phi_inv_eq asserting φ^{-1} = φ - 1, and the bound phi_lt_16185 that φ < 1.6185 obtained from √5 < 2.237.
proof idea
The term-mode proof rewrites the left side using phi_inv_eq to obtain φ - 1 < 0.6186. It then applies the hypothesis from phi_lt_16185 that φ < 1.6185 and finishes with linarith.
why it matters
This result supplies the base case for the chain of bounds on negative powers of φ that appear in phi_inv2_lt and phi_inv3_lt. It also supports the interval membership proof phi_inv_in_interval_proven. Within the framework it anchors the numerical side of the phi-ladder by confirming concrete upper bounds consistent with the self-similar fixed point property of φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.