log_phi_gt_048
plain-language theorem explainer
The inequality 0.48 < log(φ) holds where φ = (1 + √5)/2. Numerics and thermodynamics groups in the Recognition Science pipeline cite this bound when deriving interval constraints on stiffness or BCS ratios. The proof is a short tactic sequence that pulls the lower endpoint of a pre-verified interval containing log(φ) and compares it to 0.48 by rational comparison.
Claim. $0.48 < log((1 + √5)/2)$
background
The Numerics.Interval.Tactic module supplies tactics that turn precomputed interval containments into explicit bounds on transcendental expressions. logPhiInterval is the closed interval [0.48, 0.483] whose endpoints are chosen so that Taylor expansion of log at φ verifies containment. The upstream result log_phi_in_interval asserts that log((1 + √5)/2) lies inside this interval; its proof reduces the claim to the definition of the interval and the identity (1 + √5)/2 = goldenRatio.
proof idea
The tactic proof invokes log_phi_in_interval to obtain the containment, applies norm_num to establish 0.48 < 481/1000, and finishes with lt_of_lt_of_le on the lower endpoint.
why it matters
This bound feeds gcic_stiffness_bounds (which constrains κ ∈ (0.1152, 0.1167)) and bcs_ratio_approx (which places the BCS ratio near 1.96). It supplies the concrete lower anchor required by the phi-ladder numerics that appear in T6 self-similarity and the eight-tick octave, closing one link in the chain from interval arithmetic to thermodynamic and chemical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.