jcost_symmetric
plain-language theorem explainer
For every positive real x, the recognition cost satisfies J(x) = J(1/x). This is the algebraic form of CPT invariance: particle and antiparticle carry identical cost. Anyone citing CPT preservation in the Gray-code chirality story, or the IC-005.5 complexity result, needs this identity. The proof unfolds the closed form of J and finishes by ring algebra.
Claim. Let $J(x) = \frac{x + x^{-1}}{2} - 1$. For every real $x > 0$, one has $J(x) = J(1/x)$.
background
The recognition cost (J-cost) on positive ratios is the unique continuous functional forced by the Recognition Composition Law and the T5 uniqueness step: $J(x) = (x + x^{-1})/2 - 1$, equivalently $\cosh(\log x) - 1$. It vanishes only at $x = 1$ and is nonnegative elsewhere.
This module sits in the Gray-code chirality development. The central contrast is that J is perfectly symmetric under $x \leftrightarrow 1/x$ (particle $\leftrightarrow$ antiparticle), while the directed 8-tick Gray walk on the 3-cube is chiral: bit-flip counts $[4,2,2]$ break $S_3$ axis symmetry. The module doc states the point bluntly: "This symmetry IS CPT invariance."
Upstream, Cost.Jcost (and the identical Cosmology copy) supply the closed form used here. Downstream complexity work reuses the same identity as a conditioning fact for the cost landscape.
proof idea
One-line algebraic proof. Unfold the definition of Cost.Jcost by simp, obtaining equality of $(x + x^{-1})/2 - 1$ with $((1/x) + (1/x)^{-1})/2 - 1$. The tactic ring then closes the identity on the field of reals (using $x > 0$ only to keep the reciprocal well-typed in context). No external lemmas beyond the definition are required.
why it matters
In the Gray-code chirality chain this identity is the CPT half of the CP/CPT split: chirality of the directed 8-tick walk breaks CP (and flavor symmetry across generations), while J-symmetry keeps CPT intact. The module lists it among the main results as the algebraic content of cpt_preserved.
It is the T5 J-cost in its most elementary symmetry form, and it feeds PhysicsComplexityStructure.jcost_symmetric (IC-005.5), whose doc-comment records that the reflection symmetry "ensures the optimization problem is well-conditioned." Without $J(x)=J(1/x)$, the particle/antiparticle cost balance and the CPT-preservation claim in the chirality certificate would have no algebraic anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.