log_phi_lt_0483
plain-language theorem explainer
The inequality log φ < 0.483 holds for the golden ratio φ. Workers on Recognition Science numerics cite the result when tightening intervals for thermodynamic quantities such as stiffness and gap ratios. Its tactic proof converts the statement to an exponential comparison, substitutes explicit Taylor sum and error values, and finishes the chain with a rational upper bound on φ together with linarith.
Claim. $log φ < 0.483$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The Numerics.Interval.Log module supplies rigorous bounds on the natural logarithm via monotonicity on the positive reals and Taylor remainder estimates for the exponential. For log(φ) the strategy reduces the target to φ < exp(0.483) and applies a degree-10 Taylor expansion with explicit error at argument 0.483. Upstream lemmas from AlphaBounds furnish the concrete polynomial value exp_taylor_10_at_0483 and the remainder exp_error_10_at_0483.
proof idea
The script applies Real.log_lt_iff_lt_exp to rewrite the goal as φ < exp(0.483). It invokes Real.exp_bound with n=10 to obtain a Taylor-sum-minus-error lower bound. After equating the sum and error to the precomputed constants via simp and norm_num, it inserts the comparison φ < 1.6180340 and closes the chain to the true exponential with linarith.
why it matters
The bound completes the upper estimate for log φ required by the interval pipeline. It is invoked in gcic_stiffness_bounds to obtain κ ∈ (0.1152, 0.1167), in bcs_ratio_approx to locate the BCS gap ratio near 1.96, and in f_gap_lt for the gap-function bound. In the Recognition framework it anchors the numerical value of log φ that enters the phi-ladder mass formula and the predicted alpha inverse band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.