cpt_ok_cp_broken
plain-language theorem explainer
CPT invariance and CP violation coexist in Recognition Science: the cost J satisfies J(x)=J(1/x) for all positive x, while the canonical 3-bit Gray-code cycle on the cube is chiral. Anyone citing the geometric origin of CP breaking with CPT intact will use this pairing. The proof is a one-line product of the two component theorems.
Claim. For every real $x>0$, $J(x)=J(x^{-1})$, and the Gray-code bit-flip counts on $Q_3$ are chiral: they are not all equal across the three axes.
background
The module GrayCodeChirality locates CP violation in the directed 8-tick Gray-code walk on the 3-cube $Q_3$. The recognition cost is $J(x)=(x+x^{-1})/2-1$ (also written $\cosh(\log x)-1$). It is symmetric under $x\leftrightarrow x^{-1}$, which the framework identifies with CPT: particle and antiparticle carry equal cost.
Chirality is defined on flip-count vectors: a cycle is chiral when its three axis flip counts are not all equal, equivalently when they fail $S_3$ invariance. The canonical Gray path flips bits in the schedule $[0,1,0,2,0,1,0,2]$, giving counts $(4,2,2)$ and asymmetry vector $(4/3,-2/3,-2/3)$ of nonzero norm. Face-pairs of $Q_3$ are particle generations, so unequal flips mean generation-dependent drive per cycle.
Upstream, cpt_preserved proves $J(x)=J(x^{-1})$ by direct algebra on the formula, and cycle_is_chiral proves the Gray counts are unequal by native computation of the bit-flip tallies.
proof idea
Term-mode pairing: the goal is a conjunction, and the proof is the pair of the two already-proved conjuncts. The first component is the universal J-symmetry theorem (algebraic simp and ring on the cost formula). The second is the chirality theorem for the Gray flip-count function, obtained by showing bit 0 flips four times and bit 1 twice, so the counts cannot be constant on all axis pairs. No new computation occurs here.
why it matters
This is the module's headline coexistence statement: CPT stays intact while CP is broken by geometry. The module doc frames it as the RS origin of CP violation: J-symmetry is CPT, and the directed Gray walk's 4:2:2 flip split breaks axis permutation symmetry, hence CP. Framework landmarks in play are T5 (J uniqueness), T7 (eight-tick octave on $2^3$ vertices), and T8 ($D=3$), which fix the cube and the cost. Downstream the same file builds generation-specific coupling and a master chirality certificate from this split; the present theorem is the clean two-clause summary a later certificate or paper proposition can quote. No external used_by edges are recorded yet, so its role is local packaging rather than a deep dependency hub.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.