log_phi_gt_048
plain-language theorem explainer
The lemma asserts that the natural logarithm of the golden ratio exceeds 0.48. Researchers deriving GCIC stiffness bounds, critical temperatures, or BCS ratio approximations cite it to anchor interval estimates on phi-derived constants. The proof is a one-line wrapper that imports the core bound from Numerics.Interval.Log and rewrites the local phi definition to Real.goldenRatio.
Claim. $0.48 < log φ$, where $φ = (1 + √5)/2$ is the golden ratio.
background
The GCIC Phase Thermodynamics module formalizes constants from the 'Two Upgrades for the GCIC Paper' for stiffness, phase barriers, and critical temperatures. Constants.phi is the golden ratio drawn from the CPM LawOfExistence bundle. Upstream results in Numerics.Interval.Log establish the bound via exp monotonicity: log(φ) > 0.48 iff φ > exp(0.48), using φ > 1.61803395 and a Taylor bound showing exp(0.48) < 1.61803395. Parallel statements appear in AlphaBounds and Tactic for interval arithmetic.
proof idea
This is a one-line wrapper. It binds the theorem log_phi_gt_048 from IndisputableMonolith.Numerics.Interval.Log, then applies simpa with the local Constants.phi and Real.goldenRatio to match the goal.
why it matters
The lemma supplies the lower bound on log(phi) required by gcic_stiffness_bounds and mf_critical_temperature_bounds in the same module. It also supports bcs_ratio_approx in Chemistry.SuperconductingTc, where 2 log(φ) + 1 approximates the BCS ratio near 1.96. In the Recognition framework it anchors the phi-ladder constants consistent with T5 J-uniqueness and the eight-tick octave, closing an interval needed for alpha bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.