noncompact_uniform_convexity
plain-language theorem explainer
The inequality cosh(t) ≥ 1 for every real t confirms uniform convexity of the phase potential V. Researchers formalizing GCIC thermodynamics cite it when establishing bounds on stiffness and critical temperatures. The proof is a one-line wrapper applying the standard real-analytic lower bound on the hyperbolic cosine.
Claim. For every real number $t$, $1 ≤ cosh(t)$.
background
The GCIC Phase Thermodynamics module formalizes constants from the GCIC Response paper 'Two Upgrades for the GCIC Paper' (Feb 2026). It centers on a phase potential whose second derivative equals cosh(t), yielding uniform convexity. Upstream results supply structural conditions derived from seven axioms and define the uniform distribution on n points for entropy calculations.
proof idea
The proof is a one-line wrapper that applies the library lemma establishing cosh(t) ≥ 1 for all real t.
why it matters
It is bundled into gcic_thermodynamics_cert, which certifies positivity of stiffness, phase barrier, and mean-field critical temperature together with the convexity bound. The result supplies the base inequality needed for quadratic lower bounds on the potential and supports convexity requirements in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.