JCostCoshCert
plain-language theorem explainer
JCostCoshCert packages five properties of the J-cost function on exponentials, confirming its identity with the shifted hyperbolic cosine. Researchers modeling the strong-field Regge action cite this certificate to access the explicit non-linear J form. The structure collects independent lemmas for the cosh identity, zero value at the fixed point, symmetry, non-negativity, and strict positivity off zero.
Claim. Let $J$ denote the J-cost function. Then $J(e^y) = (e^y + e^{-y})/2 - 1$ for all real $y$, with $J(1) = 0$, $J(e^y) = J(e^{-y})$, $J(e^y) ≥ 0$, and $J(e^y) > 0$ for $y ≠ 0$.
background
The J-cost function is defined by $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$, equivalently written as cosh(log x) - 1. This module records the direct substitution $J(e^y) = cosh y - 1$ together with its immediate algebraic consequences. The local theoretical setting is the non-linear cosh form of J-cost that appears in the strong-field Regge action, as stated in Beltracchi Response §5.
proof idea
The structure definition assembles five sibling lemmas without a proof body of its own. jcost_exp_cosh_form supplies the cosh identity, jcost_exp_zero the zero value, jcost_exp_symm the symmetry, jcost_exp_nonneg the non-negativity, and jcost_exp_pos the strict positivity. The certificate is formed by direct reference to these results.
why it matters
This certificate supplies the explicit non-linear J form required downstream for the strong-field Regge action. It is instantiated by jCostCoshCert and aligns with T5 J-uniqueness in the forcing chain, where J(x) = (x + x^{-1})/2 - 1. The result confirms the fixed-point vanishing and positivity properties used in the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.