phiIntervalTight
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.
claimLet $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 in Recognition Science
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)).
scope and limits
- Does not derive the bounds from the minimal polynomial of φ.
- Does not extend the endpoints to real-number arithmetic.
- Does not claim that the interval is the tightest possible rational enclosure.
formal statement (Lean)
91def phiIntervalTight : Interval where
92 lo := 161803395 / 100000000 -- 1.61803395
proof body
Definition body.
93 hi := 16180340 / 10000000 -- 1.6180340
94 valid := by norm_num
95
96/-- φ is contained in phiIntervalTight - PROVEN -/