log_phi_gt_048
The lemma establishes that log(φ) > 0.48 where φ denotes the golden ratio. Interval numerics and thermodynamic calculations in the Recognition framework cite this bound to anchor gap functions and stiffness estimates. The proof rewrites the claim via exponential monotonicity and chains a Taylor upper bound on exp(0.48) with the lower bound φ > 1.61803395 using transitivity.
claim$0.48 < log φ$ where $φ = (1 + √5)/2$ is the golden ratio constant.
background
The AlphaBounds module develops rigorous interval bounds on α⁻¹ using the Recognition Science constants. This lemma supplies a concrete lower bound on log(φ) that enters downstream gap and critical temperature estimates. Upstream results include exp_048_lt, which asserts exp(0.48) < 1.6161... via a 10-term Taylor series, and phi_gt_161803395, which asserts 1.61803395 < φ. The transitivity result lt_trans chains these inequalities.
proof idea
The proof rewrites the target via Real.lt_log_iff_exp_lt to obtain the equivalent exp(0.48) < φ. It extracts a lower bound on φ from W8Bounds.phi_gt_161803395 by linarith. The final step applies lt_trans to combine this lower bound with the Taylor-derived exp_048_lt.
why it matters in Recognition Science
This bound feeds the BCS ratio approximation in Chemistry.SuperconductingTc and the stiffness bounds in Papers.GCIC.Thermodynamics. It anchors the self-similar fixed point φ from the forcing chain and supports interval arithmetic for α⁻¹. The result closes a concrete numerical step in the phi-ladder numerics.
scope and limits
- Does not establish an upper bound on log(φ).
- Does not compute the exact numerical value of log(φ).
- Does not derive bounds on α or other constants directly.
- Does not extend to logarithms in bases other than e.
Lean usage
have h := log_phi_gt_048formal statement (Lean)
169private lemma log_phi_gt_048 : (0.48 : ℝ) < log IndisputableMonolith.Constants.phi := by
proof body
Tactic-mode proof.
170 rw [Real.lt_log_iff_exp_lt IndisputableMonolith.Constants.phi_pos]
171 have hphi_lo : (((16161 / 10000 : ℚ) : ℝ)) < IndisputableMonolith.Constants.phi := by
172 have hphi : (1.61803395 : ℝ) < IndisputableMonolith.Constants.phi := W8Bounds.phi_gt_161803395
173 linarith
174 exact lt_trans exp_048_lt hphi_lo
175