jCostCoshCert
plain-language theorem explainer
The jCostCoshCert definition assembles the five elementary properties of J-cost under exponential argument into one reusable certificate structure. A physicist working on the strong-field Regge action cites it to invoke J(e^y) = cosh(y) - 1 together with its fixed-point, symmetry, and positivity consequences without re-deriving each step. The construction is a direct structure literal that references the five supporting theorems for each field.
Claim. Define the certificate $JCostCoshCert$ by the structure whose fields are: cosh_form: $Jcost(e^y) = (e^y + e^{-y})/2 - 1$ for all real $y$; zero_at_zero: $Jcost(e^0) = 0$; symmetric: $Jcost(e^y) = Jcost(e^{-y})$ for all real $y$; nonneg: $0 ≤ Jcost(e^y)$ for all real $y$; pos_off_zero: $0 < Jcost(e^y)$ whenever $y ≠ 0$.
background
In the J-Cost = Cosh - 1 Identity module the J-cost function is identified with its hyperbolic-cosine representation $J(e^y) = cosh(y) - 1$. This non-linear form appears in the strong-field Regge action. The module records four immediate consequences: the function vanishes only at the fixed point $y = 0$, is even under sign flip of the exponent, is non-negative for all real exponents, and is strictly positive away from zero.
proof idea
The definition is a one-line wrapper that populates the $JCostCoshCert$ structure by direct assignment of each field to its supporting theorem: cosh_form receives jcost_exp_cosh_form, zero_at_zero receives jcost_exp_zero, symmetric receives jcost_exp_symm, nonneg receives jcost_exp_nonneg, and pos_off_zero receives jcost_exp_pos.
why it matters
This certificate supplies the cosh representation of J-cost required by Beltracchi Response §5 for the strong-field regime. It closes the elementary properties needed before any later appeal to the Recognition Composition Law or ascent of the phi-ladder. Although currently unused downstream, it provides the canonical interface for theorems that must invoke the fixed-point condition or non-negativity without repeating the derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.