log_phi_interval_contains
plain-language theorem explainer
The declaration establishes that the natural log of the golden ratio lies inside the closed interval from 0.48 to 0.483. Numerics researchers bounding transcendental functions via interval arithmetic would cite this containment when verifying logarithmic expressions tied to the golden ratio. The proof is a direct one-line reference to the prior theorem that confirms the bound through Taylor series estimates.
Claim. $[0.48, 0.483]$ contains $log((1 + sqrt(5))/2)$
background
The module supplies tactics for proving bounds on transcendental expressions such as logarithms by means of interval arithmetic. The contains predicate on an interval I and real number x holds exactly when the lower endpoint of I is at most x and x is at most the upper endpoint. The concrete interval logPhiInterval is fixed with lower bound 0.48 and upper bound 0.483 so that it brackets the approximate value log(φ) ≈ 0.4812 and permits verification with a finite Taylor expansion.
proof idea
The proof is a one-line wrapper that directly invokes the upstream theorem log_phi_in_interval, which itself applies Taylor series bounds to establish the containment.
why it matters
The result supplies a verified numerical bracket for log(φ) that supports interval-based arguments involving the golden ratio, the self-similar fixed point forced in the Recognition Science chain. It closes a concrete instance of the interval tactic machinery without introducing new hypotheses. No immediate downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.