cosh_quadratic_lower_bound
plain-language theorem explainer
The inequality cosh x ≥ 1 + x²/2 holds for every real x. Derivations of Landauer bounds on recognition cost and lower bounds on phase stiffness cite it to obtain quadratic estimates from the hyperbolic expression. The proof invokes the Taylor series representation of cosh, isolates the first two terms, and applies the nonnegativity of all higher terms together with the comparison between partial sums and the infinite sum.
Claim. $cosh x ≥ 1 + x²/2$ for all real $x$.
background
The Cost module develops the recognition cost Jcost satisfying Jcost(e^t) = cosh(t) - 1, an identity that follows from the Recognition Composition Law and J-uniqueness. This supplies the elementary inequality that converts the exact hyperbolic cost into a quadratic form used for dissipation and stiffness calculations. Jmetric is defined as the square root of twice Jcost, turning the cost into a metric on the positive reals.
proof idea
The tactic proof calls Real.hasSum_cosh to obtain the power series. It proves each term x^(2n)/(2n)! is nonnegative by rewriting as (x²)^n / (2n)! and applying pow_nonneg together with Nat.cast_nonneg. It then uses the summable-series comparison sum_le_tsum to bound the total sum from below by the sum of the n=0 and n=1 terms, which simplify directly to 1 + x²/2.
why it matters
The bound is invoked by landauer_bound_holds to establish the quadratic Landauer inequality for recognition cost, by Jtilde_stiffness_lb to bound the reduced phase potential from below, and by coshRemainder_nonneg to prove the remainder is nonnegative. It supports the transition from the J-uniqueness definition (T5) to explicit calculations in the eight-tick octave and three-dimensional forcing chain. The result closes the analytic gap needed for discrete-tier mass formulas and thermodynamic bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.