jcost_exp_zero
plain-language theorem explainer
jcost_exp_zero confirms that Jcost applied to e^0 equals zero, establishing the fixed-point property of the J-cost function at the identity. Researchers deriving the strong-field Regge action or verifying phi-ladder mass formulas cite this result to anchor the zero-cost condition. The proof is a one-line wrapper that rewrites via the general cosh identity and simplifies the arithmetic expression to zero.
Claim. $J(e^{0}) = 0$, where $J(z) = (z + z^{-1})/2 - 1$.
background
The module identifies J-cost with the hyperbolic cosine form J(e^y) = (e^y + e^{-y})/2 - 1. This non-linear expression appears in the strong-field Regge action and supplies the four listed properties: zero at the fixed point y=0, symmetry under sign flip of y, strict positivity for y nonzero, and global non-negativity. The upstream theorem jcost_exp_cosh_form states the general identity Jcost(Real.exp y) = (Real.exp y + Real.exp (-y))/2 - 1 for any real y, derived from the square definition of Jcost via field simplification and ring reduction.
proof idea
The proof is a one-line wrapper that applies the cosh-form lemma jcost_exp_cosh_form at y=0 and then invokes simp to reduce the resulting expression to zero.
why it matters
This supplies the zero_at_zero field inside the jCostCoshCert definition that bundles the four J-cost properties. It fills the fixed-point clause of T5 J-uniqueness in the forcing chain, where J(x) = (x + x^{-1})/2 - 1 is forced as the self-similar form. The certificate is referenced downstream for applications involving the Berry creation threshold and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.