jcost_recip_symmetric
plain-language theorem explainer
The recognition cost J is invariant under reciprocal inversion on the positive reals: J(x⁻¹) = J(x). Anyone citing the reciprocal involution as the common generator of cost symmetry and the golden-ratio scale will use this. The proof is a one-line rephrasing of the existing J-symmetry lemma after unfolding the local recip abbreviation.
Claim. For every real $x > 0$, the recognition cost satisfies $J(x^{-1}) = J(x)$, where $J(t) = (t + t^{-1})/2 - 1$.
background
The module treats the reciprocal map $\iota(x) = x^{-1}$ on $\mathbb{R}_{>0}$ as the single structural generator behind both the cost form and the golden-ratio scale. On the cost side the claim is that $J$ is exactly $\iota$-symmetric; on the scale side $\varphi$ is the unique fixed point $>1$ of the shift $g(x) = 1 + \iota(x)$.
Here $J$ is the standard RS recognition cost $J(x) = (x + x^{-1})/2 - 1$ (also written $\cosh(\log x) - 1$), the unique continuous solution forced by the Recognition Composition Law and the T5 uniqueness step. The local name recip is just that involution. The upstream lemma Jcost_symm already states $J(x) = J(x^{-1})$ for $x > 0$; the present declaration merely packages the same fact in the module's recip vocabulary so both halves of the generator story quantify over one object.
proof idea
Unfold the local definition of the reciprocal map, then apply the existing symmetry lemma Cost.Jcost_symm and reverse the equality. No new algebra: the identity is exactly $J(x^{-1}) = J(x)$ rewritten with the module's recip name.
why it matters
This is the cost half of the reciprocal-generator story. It feeds directly into recip_generates_cost_and_scale, which conjoins cost symmetry with the uniqueness of $\varphi$ as the fixed point $>1$ of the $\iota$-shift $1 + \iota$, and into the certificate reciprocalGeneratorCert_holds (field cost_symmetric).
The module's point is that OneLaw's conjunction of cost-form and $\varphi$-forcing is not a glued pair of unrelated facts: both quantify over the same involution. Cost symmetry is the T5/J-uniqueness landmark restated as an $\iota$-property; together with the scale side it makes $\iota$ logically upstream of both $J$'s symmetry axis and $\varphi$'s defining equation. The next sibling sharpens this further: the fixed point of $\iota$ coincides with the null set of $J$ (both only at the unit $x = 1$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.