phiIntervalTight
plain-language theorem explainer
This definition supplies a closed rational interval with endpoints 1.61803395 and 1.6180340 that contains the golden ratio φ. Numerics code in Recognition Science cites it to certify interval arithmetic for φ-dependent calculations such as phi-ladder mass formulas. The definition is a direct record construction whose single validity obligation is discharged by a norm_num check on the rational endpoints.
Claim. Let $I$ be the closed interval with rational endpoints $lo = 161803395/100000000$ and $hi = 16180340/10000000$ satisfying $lo ≤ hi$.
background
The module supplies rigorous rational bounds on φ = (1 + √5)/2. Interval is the structure with fields lo : ℚ, hi : ℚ and valid : lo ≤ hi (from Numerics.Interval.Basic). The local strategy begins from the algebraic inequalities 2.236² < 5 < 2.237² and tightens the resulting bounds on √5 to obtain the displayed decimal approximations for φ.
proof idea
The definition is a direct structure literal that supplies the two rational endpoints and invokes the norm_num tactic to prove the single field valid : lo ≤ hi.
why it matters
The interval is the target of the downstream theorem phi_in_phiIntervalTight, which asserts that φ lies inside these bounds. It supports numerical certification steps that rely on the self-similar fixed point φ (T6) and the eight-tick octave (T7) when evaluating phi-ladder expressions or the mass formula yardstick · φ^(rung-8+gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.