log_phi_lt_0483
plain-language theorem explainer
A rigorous upper bound log(φ) < 0.483 is established where φ denotes the golden ratio. Researchers deriving GCIC stiffness κ = (log φ)²/2 or BCS ratios would cite it to constrain thermodynamic intervals. The proof is a one-line wrapper that imports the bound from Numerics.Interval.Log and rewrites via the identification of Constants.phi with Real.goldenRatio.
Claim. $log φ < 0.483$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The GCIC Phase Thermodynamics module specializes CPM constants for phase-structure calculations, including stiffness and critical-temperature bounds. The Constants structure supplies the abstract bundle of parameters (Knet, Cproj, Ceng, Cdisp) with non-negativity axioms. The bound originates in Numerics.Interval.Log, where log(φ) < 0.483 is obtained from the equivalence log x < c ↔ x < exp(c) together with the Taylor-derived inequality exp(0.483) > 1.6180340.
proof idea
The proof is a one-line wrapper: it obtains the theorem from IndisputableMonolith.Numerics.Interval.Log and applies simpa to substitute the definitions of Constants.phi and Real.goldenRatio.
why it matters
The lemma supplies the upper endpoint for gcic_stiffness_bounds (κ ∈ (0.1152, 0.1167)), mf_critical_temperature_bounds, and phase_barrier_upper inside the same module. It directly supports the GCIC Response paper propositions on stiffness and phase structure. Within the Recognition framework it anchors the numerical control of the phi-ladder constants that appear in the T6 self-similar fixed point and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.