cpt_preserved
plain-language theorem explainer
For every positive real ratio, the recognition cost equals the cost of its reciprocal: particle and antiparticle share the same J-cost. Anyone citing CPT preservation inside the Gray-code chirality or CP-phase certificates needs this identity. The proof unfolds the closed form of J and finishes by ring algebra.
Claim. For all real $x > 0$, $J(x) = J(x^{-1})$, where the recognition cost is $J(x) = \frac{x + x^{-1}}{2} - 1$. Equivalently, particle and antiparticle ratios carry identical cost.
background
The module GrayCodeChirality locates CP violation in the directed 3-bit Gray-code walk on the cube $Q_3$. The central contrast is that the scalar cost is reciprocal-symmetric while the walk is not.
The recognition cost is the unique T5 functional $J(x) = (x + x^{-1})/2 - 1$ (also $\cosh(\log x) - 1$). Upstream definitions in Cost and Cosmology.RefineTrigger fix exactly this closed form on positive reals; non-negativity and the Recognition Composition Law sit upstream of the present identity.
Module doc states the reading used here: "$J(x) = J(1/x)$ is perfectly symmetric under particle$\leftrightarrow$antiparticle exchange. This symmetry IS CPT invariance." The eight-tick directed path then breaks CP without touching that scalar symmetry.
proof idea
Term-mode proof by direct algebra. Introduce $x > 0$, unfold Cost.Jcost to $(x + x^{-1})/2 - 1$, and apply ring. The reciprocal form is identical after clearing denominators, so no positivity lemmas beyond the hypothesis domain are required.
why it matters
This is item 3 of the module's main results: CPT preserved while CP is broken by Gray-code chirality. It is the cpt_ok field of chiralityCert and the left conjunct of cpt_ok_cp_broken ("$J(x)=J(1/x)$ (CPT) AND the cycle is chiral (CP violation)").
Downstream, StandardModel.CPPhaseDerivation reuses the same reciprocal symmetry inside CPPhaseCert / cpPhaseCert (the cpt_preserved slot, there as phase plus anti-phase equals zero). Framework-wise it is the cost-level reading of T5 J-uniqueness: the unique cost forced by the RCL is automatically CPT-even, so any CP-odd physics must come from directed structure (the 4:2:2 flip asymmetry on the eight-tick octave), not from the scalar cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.