jcost_exp_symm
plain-language theorem explainer
Symmetry of the J-cost function under sign flip of the exponent holds for every real y. Workers on the Recognition Science forcing chain cite it to confirm evenness of J around the fixed point. The proof substitutes the explicit cosh expression on both sides, cancels the double negation, and reduces the identity by ring.
Claim. For every real number $y$, $J(e^y) = J(e^{-y})$, where the J-cost is defined by $J(z) := (z + z^{-1})/2 - 1$.
background
The J-Cost = Cosh -1 Identity module derives the explicit non-linear form J(e^y) = (e^y + e^{-y})/2 -1 that appears in the strong-field Regge action. It records four elementary properties: vanishing only at y=0, symmetry under y to -y, strict positivity off zero, and global non-negativity. The upstream result jcost_exp_cosh_form supplies the cosh expression itself, obtained from Jcost_eq_sq by field_simp and ring.
proof idea
Term-mode proof that rewrites both sides via the cosh-form lemma jcost_exp_cosh_form, applies neg_neg to remove the double negation, and closes with ring to equate the resulting expressions.
why it matters
The theorem supplies the symmetric slot inside the JCostCoshCert bundle that packages the core J-cost properties. It fills the symmetry requirement for the J-uniqueness step (T5) in the UnifiedForcingChain, where J(x) is identified with cosh(log x) -1; this evenness is a prerequisite for the self-similar fixed point phi and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.