coshRemainder_nonneg
plain-language theorem explainer
The theorem establishes that the remainder cosh(x) - 1 - x²/2 is non-negative for every real x. Researchers extending the J-cost action beyond the quadratic regime in simplicial gravity models would cite this bound to control higher-order corrections. The proof is a one-line wrapper that unfolds the definition and invokes the quadratic lower bound for cosh together with linear arithmetic.
Claim. For every real number $x$, $0 ≤ cosh(x) - 1 - x²/2$.
background
This declaration sits in the Nonlinear J-Cost / Regge Bridge module, which addresses Beltracchi §6 by showing that the exact J-cost action remains well-defined for arbitrary log-potential differences ε_i - ε_j. The nonlinear coupling is given by J(exp(ε_i - ε_j)) = cosh(ε_i - ε_j) - 1, which reduces to the Laplacian action only at leading order. The function coshRemainder(x) is defined as cosh(x) - 1 - x²/2 and isolates the first nonlinear correction, known to begin at order x⁴/24.
proof idea
The proof unfolds the definition of coshRemainder and applies the upstream theorem cosh_quadratic_lower_bound, which asserts cosh(x) ≥ 1 + x²/2 for all real x. Linear arithmetic then immediately yields non-negativity of the difference.
why it matters
The result is invoked by quarticRemainder_nonneg to establish that the full quartic remainder term in the decomposition exactJCostAction = laplacian_action + quartic_remainder is non-negative. It thereby supplies the Lean-level justification that the J-cost side of the identification holds without a weak-field assumption, directly filling the gap noted in the module doc-comment for Beltracchi §6. In the broader Recognition framework this supports the exact nonlinear action at all orders while leaving the Regge deficit-angle side as a separate hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.