log_phi_lt_049
plain-language theorem explainer
This result establishes that the natural logarithm of the golden ratio is strictly less than 0.49. Numerics researchers verifying interval bounds on transcendental functions would cite it when confirming approximations for φ ≈ 1.618. The proof retrieves a precomputed interval containing log(φ) and compares its upper endpoint to 0.49 via norm_num and transitivity.
Claim. $log((1 + sqrt(5))/2) < 0.49$
background
The Numerics.Interval.Tactic module supplies tactics for proving bounds on transcendental expressions using interval arithmetic. logPhiInterval is the closed interval [0.48, 0.483] chosen to contain log(φ) with margin for Taylor verification. The upstream theorem log_phi_in_interval asserts that log(φ) belongs to this interval, proven using Taylor series bounds.
proof idea
The tactic proof invokes log_phi_in_interval to obtain the containing interval. It then shows via norm_num that the interval upper bound 482/1000 is less than 0.49. Finally it applies lt_of_le_of_lt to the interval membership and the numeric comparison.
why it matters
This example illustrates the interval tactic machinery used to certify numerical inequalities in the Recognition framework. It supports phi-related constants in the forcing chain (T5 J-uniqueness, T6 phi fixed point) by providing machine-checked bounds on log(φ). No downstream uses are recorded yet, but it closes a gap for log approximations in spacetime emergence calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.