phi_in_phiIntervalTight
plain-language theorem explainer
Golden ratio φ satisfies the certified bounds 1.61803395 ≤ φ ≤ 1.6180340. Numerics code for Recognition Science phi-ladder calculations would cite this result. The tactic proof reduces the containment claim by invoking two prior rational bounds on φ, normalizing decimals via calc and norm_num, then applying le_of_lt.
Claim. $1.61803395 ≤ φ ≤ 1.6180340$ where $φ = (1 + √5)/2$ and the interval is defined by the rational endpoints 161803395/100000000 and 16180340/10000000.
background
The module supplies rigorous bounds on φ = (1 + √5)/2 by comparing rational squares to 5. The strategy uses 2.236² < 5 < 2.237² to obtain 2.236 < √5 < 2.237 and hence 1.618 < φ < 1.6185, with tighter decimal approximations following the same pattern. The contains predicate from Interval.Basic states that a real x belongs to an Interval when lo ≤ x ≤ hi.
proof idea
Tactic-mode proof. simp only [Interval.contains, phiIntervalTight] reduces the goal to two inequalities. constructor splits them. The lower bound applies phi_gt_161803395 inside a calc that normalizes the rational to 1.61803395, then le_of_lt. The upper bound mirrors the steps with phi_lt_16180340.
why it matters
Supplies certified numerical bounds on φ for downstream Recognition Science numerics, supporting the self-similar fixed point (T6) and phi-ladder mass formulas. It bridges algebraic definitions of φ to interval arithmetic used in forcing-chain calculations. No downstream uses are recorded yet, so the result functions as a foundational primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.