log_phi_in_interval
plain-language theorem explainer
The theorem confirms that the natural logarithm of the golden ratio lies inside the closed rational interval logPhiInterval. Numerics researchers verifying bounds on phi for Recognition Science calculations would cite it when composing interval proofs. The tactic proof equates the input to Real.goldenRatio, then splits the containment into independent lower and upper inequalities supplied by prior lemmas.
Claim. $log((1 + sqrt(5))/2)$ satisfies the containment predicate for the interval whose lower and upper rational endpoints are fixed by logPhiInterval, i.e., lower endpoint ≤ value ≤ upper endpoint.
background
The module supplies interval arithmetic for the natural logarithm on positive reals, using monotonicity of log together with Taylor remainder estimates for log(1+x) when 0 < x < 1. Here x = phi - 1 ≈ 0.618. The structure Interval is a closed interval with rational endpoints lo ≤ hi; the predicate contains asserts that a real lies between those endpoints. Upstream lemmas log_phi_gt_048 and log_phi_lt_0483 establish the strict inequalities 0.48 < log phi and log phi < 0.483 via exp monotonicity and separate phi bounds; the present theorem tightens them into a single interval statement.
proof idea
The tactic first rewrites ((1 + sqrt 5)/2) to Real.goldenRatio by ring. Constructor splits the conjunction inside contains. The lower half converts the rational 48/100 to real, invokes log_phi_gt_048, and closes with le_of_lt after norm_num. The upper half invokes log_phi_lt_0483, converts 483/1000, and closes with le_of_lt after norm_num.
why it matters
The result supplies the verified containment fact that downstream tactic lemmas (log_phi_interval_contains, log_phi_gt_048, log_phi_lt_049) directly invoke. It supports numerical checks on phi, the self-similar fixed point forced at step T6 of the unified forcing chain. The module doc-comment notes that the bounds rest on Taylor error estimates for log(1+x) with x = phi - 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.