logPhiInterval
plain-language theorem explainer
The definition supplies the closed interval [0.48, 0.483] that contains log(φ) for the golden ratio φ = (1 + √5)/2. Numerics proofs in the Recognition framework cite it to anchor Taylor-series bounds on the logarithm without floating-point error. The construction is a direct Interval record whose ordering is discharged by a single norm_num check.
Claim. Let $I = [0.48, 0.483]$. Then $I$ is an interval (i.e., lower bound ≤ upper bound) that is intended to contain $log φ$ where $φ = (1 + √5)/2$.
background
The module develops interval arithmetic for the natural logarithm to support rigorous bounds inside the Recognition framework. An Interval pairs a lower real lo with an upper real hi together with a proof that lo ≤ hi. The strategy for log exploits monotonicity on (0, ∞) together with the Taylor expansion of log(1 + x) for |x| < 1; the error after n terms is bounded by |x|^{n+1} / ((n+1)(1 - |x|)). The concrete interval here is sized for x = φ - 1 ≈ 0.618 so that a modest number of Taylor terms suffices to keep the error below the target width.
proof idea
The definition is a direct record construction. The only non-trivial field is the validity proof, which is discharged by a single norm_num tactic confirming 48/100 ≤ 483/1000.
why it matters
This interval anchors every subsequent log(φ) bound in the Numerics.Interval.Log module and is invoked by log_phi_in_interval, log_phi_lt_0483, and the tactic lemmas log_phi_gt_048 and log_phi_lt_049. It supplies the numerical control required to close the phi-ladder mass formula and the alpha-band estimates, since φ is the self-similar fixed point forced at step T6 of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.