log_phi_lt_0483
plain-language theorem explainer
The lemma proves log φ < 0.483 where φ is the golden-ratio constant from the Recognition Science bundle. Researchers deriving GCIC stiffness intervals or BCS critical-temperature ratios cite it to close numerical gaps in thermodynamic bounds. The proof reduces the claim via log_lt_iff_lt_exp to a direct comparison of the pre-established decimal upper bound on φ against a Taylor lower bound on exp(0.483), then chains the two inequalities with lt_trans.
Claim. $log φ < 0.483$, where φ denotes the golden-ratio constant (1 + √5)/2 from the Recognition Science Constants structure.
background
The Numerics.Interval.AlphaBounds module supplies rigorous interval bounds on α^{-1} derived from the symbolic Recognition framework. Within this setting φ is the self-similar fixed point forced at T6 of the UnifiedForcingChain, satisfying the J-uniqueness relation J(x) = (x + x^{-1})/2 - 1. The lemma supplies a concrete upper bound on log φ that is later combined with the matching lower bound log φ > 0.48 to control logarithmic terms appearing in stiffness and gap formulas.
proof idea
The short tactic proof first rewrites the goal with Real.log_lt_iff_lt_exp using φ_pos. It then obtains the auxiliary fact φ < 1.6180340 by linarith from W8Bounds.phi_lt_16180340. The final step applies lt_trans (from ArithmeticFromLogic) to chain this fact with the sibling lemma exp_0483_gt, which supplies the Taylor lower bound 1.6209... < exp(0.483).
why it matters
The bound is a required numerical anchor for the α^{-1} interval (137.030, 137.039) and for the eight-tick octave scaling. It is invoked directly by gcic_stiffness_bounds (producing κ ∈ (0.1152, 0.1167)), by bcs_ratio_approx in SuperconductingTc, and by phase_barrier_upper and mf_critical_temperature_bounds in the GCIC.Thermodynamics paper. The 0.483 threshold is chosen to lie safely above the actual log φ while remaining compatible with the phi-ladder mass formula and the RCL identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.