phi_in_phiInterval
plain-language theorem explainer
Golden ratio φ = (1 + √5)/2 lies inside the rational interval [1.618, 1.619]. Interval arithmetic for powers of φ cites this result to anchor phiInterval. The tactic proof reduces containment to two inequalities by invoking the supplied bounds 1.618 < φ and φ < 1.6185 together with norm_num on the rational endpoints.
Claim. Let $I$ be the closed interval with rational endpoints $1618/1000$ and $1619/1000$. Then $1618/1000 ≤ (1 + √5)/2 ≤ 1619/1000$.
background
The module supplies interval arithmetic for the power function via the identity x^y = exp(y log x). An Interval is a structure carrying rational lo and hi with lo ≤ hi. The predicate contains holds when a real x satisfies lo ≤ x ≤ hi. The definition phiInterval fixes lo = 1618/1000 and hi = 1619/1000. Upstream theorems establish 1.618 < goldenRatio and goldenRatio < 1.6185 by comparing √5 to 2.236 and 2.237 respectively.
proof idea
The tactic first simplifies contains to the pair of inequalities. Constructor splits the conjunction. The lower bound is obtained by rewriting 1618/1000 to 1.618 and applying phi_gt_1618. The upper bound rewrites 1.6185 to 1619/1000 and applies phi_lt_16185, with norm_num discharging the rational conversions in each calc block.
why it matters
This result supplies the base membership fact used by phi_pow_140_in_interval and phi_pow_142_in_interval when bounding high powers of φ for galactic-scale numerics. It is also invoked directly by the tactic lemmas phi_gt_161, phi_lt_162 and phi_interval_contains. The interval anchors the phi-ladder computations that appear throughout the numerics layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.