jcost_exp_pos
plain-language theorem explainer
J(e^y) is strictly positive for any nonzero real y. Researchers confirming the positivity axioms for the J-cost in its exponential representation within Recognition Science would cite this. The proof reduces the statement to the general J-cost positivity result by verifying that the exponential avoids the value one.
Claim. For all real numbers $y$ with $y ≠ 0$, $0 < J(e^y)$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The module develops the representation J(e^y) = (e^y + e^{-y})/2 - 1, the non-linear cosh form of J-cost that appears in the strong-field Regge action. Key properties include J(e^y) = 0 iff y = 0, symmetry under sign flip of y, non-negativity, and strict positivity for y ≠ 0. The upstream lemma states that J(x) > 0 for x > 0 and x ≠ 1, proved by rewriting Jcost via its square form and applying positivity of squares to the numerator.
proof idea
The tactic proof first shows exp y ≠ 1 from y ≠ 0 via the equivalence exp y = 1 iff y = 0. It then applies the lemma establishing J-cost positivity for positive arguments unequal to one, using that exp y > 0.
why it matters
This supplies the strict positivity clause in the JCostCoshCert definition that bundles the core properties of the cosh representation. It supports the J-uniqueness step in the forcing chain by confirming the fixed point at y = 0 is the sole zero of J. The module doc ties the form to the strong-field Regge action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.