phi_inv_in_interval_proven
plain-language theorem explainer
The inverse of the golden ratio lies in the closed interval [0.618, 0.6186]. Numerics researchers would cite this to certify decimal approximations of φ^{-1} without floating-point error. The tactic proof unfolds the containment predicate, splits the conjunction, and discharges each side by invoking prior strict inequalities together with norm_num reductions.
Claim. Let $I$ be the closed interval with rational endpoints $0.618$ and $0.6186$. Let $φ = (1 + √5)/2$. Then $φ^{-1} ∈ I$.
background
The module supplies rigorous decimal bounds for the golden ratio and its inverse by comparing squares to bound √5 from above and below. An Interval is a structure with rational endpoints lo and hi together with a proof that lo ≤ hi. Containment of a real x in such an interval is the proposition lo ≤ x ≤ hi.
proof idea
The tactic proof first applies simp to unfold contains and the concrete interval definition. Constructor splits the resulting conjunction. The lower bound is obtained from phi_inv_gt via a calc block that normalizes 618/1000 to 0.618 and applies le_of_lt. The upper bound is obtained symmetrically from phi_inv_lt with norm_num.
why it matters
This theorem certifies that the pre-chosen rational interval actually contains φ^{-1}, anchoring numerical work on powers of φ that rely on the Fibonacci recurrence. It sits inside the broader Recognition Science treatment of φ as the self-similar fixed point and supplies a concrete, machine-checked decimal anchor for the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.