jcost_exp_cosh_form
plain-language theorem explainer
The identity equates J-cost of an exponential to hyperbolic cosine minus one. Researchers deriving the non-linear cost form for the strong-field Regge action cite it to access symmetry and positivity properties. The proof is a short algebraic reduction that substitutes the squared-ratio expression for J-cost and finishes with field and ring simplifications.
Claim. For every real number $y$, $J(e^y) = (e^y + e^{-y})/2 - 1$, where $J$ denotes the J-cost function.
background
J-cost is given equivalently by the expression $(x + x^{-1})/2 - 1$ or by the squared-ratio form $J(x) = (x-1)^2/(2x)$ for nonzero real $x$, as supplied by the upstream lemma Jcost_eq_sq. The module establishes the non-linear cosh form of J-cost that appears in the strong-field Regge action, with the explicit statement J(e^y) = (e^y + e^{-y})/2 - 1 and the four listed properties (vanishing only at zero, symmetry, strict positivity off zero, and non-negativity). The local setting is the Beltracchi Response §5 treatment of this identity inside the Recognition Science foundation layer.
proof idea
The term-mode proof applies the squared-ratio lemma Jcost_eq_sq to the nonzero argument exp y, rewrites the negative exponent via Real.exp_neg, clears the denominator with field_simp, and concludes by ring.
why it matters
The theorem supplies the cosh_form component of the JCostCoshCert definition that bundles the four core properties. It fills the central identity step in the J-Cost = Cosh -1 section of the Beltracchi response and supports the fixed-point and positivity requirements that feed the J-uniqueness step in the forcing chain. Downstream siblings such as jcost_exp_zero and jcost_exp_symm invoke it directly to establish the listed properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Simple pixel Transformers generate competitive ImageNet samples by predicting clean data
"Predicting clean data is fundamentally different from predicting noise or a noised quantity."