jlog_above_half_square
plain-language theorem explainer
The inequality cosh(t) - 1 ≥ t²/2 holds for every real t and supplies the quadratic lower bound used in GCIC phase thermodynamics. Workers on stiffness, barrier heights, and critical temperatures in the GCIC Response paper cite this estimate to control defect costs. The proof is a one-line wrapper that applies the upstream cosh quadratic lower bound theorem and closes with linear arithmetic.
Claim. For all real numbers $t$, $t^2/2 ≤ cosh t - 1$.
background
The module Papers.GCIC.Thermodynamics formalizes constants from the GCIC Response paper on phase structure upgrades. The relevant upstream result is the theorem cosh_quadratic_lower_bound, which states cosh x ≥ 1 + x²/2 for all real x; its proof rests on the Taylor series cosh x = 1 + x²/2 + x⁴/24 + ⋯ with all higher terms non-negative, or equivalently on uniform convexity of cosh. Cost is the abbrev for Quantity CostUnit in the RSNative core, providing the dimensional setting in which the bound is applied to J-cost quantities.
proof idea
The proof is a one-line wrapper. It obtains the reversed inequality directly from Cost.cosh_quadratic_lower_bound t and closes the goal with linarith.
why it matters
The bound feeds the stiffness and phase-barrier lemmas in the same module (gcic_stiffness, phase_barrier, mf_critical_temperature). It supplies the uniform-convexity estimate required for the thermodynamic analysis in the GCIC paper and aligns with the J-uniqueness step (T5) of the forcing chain, where J(x) = cosh(log x) - 1 appears as the cost function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.