cp_broken_by_chirality
plain-language theorem explainer
CP is broken because the canonical 3-bit Gray-code cycle on the cube is chiral: axis flip counts are unequal, so forward and reverse walks are distinguishable. Anyone citing the RS geometric origin of CP violation (with CPT still intact via J-symmetry) would point here. The proof is a one-line alias of the computational chirality theorem on the Gray flip counts.
Claim. The Gray-code bit-flip count function on the 3-cube is chiral: it is not the case that all three axis counts agree. Equivalently, the directed eight-tick cycle treats the three axes unequally, so forward and backward traversals are distinguishable and CP is broken.
background
The module fixes the canonical 3-bit Gray walk on the cube $Q_3$, the eight-tick recognition path $[0,1,3,2,6,7,5,4]$ with flip pattern $[0,1,0,2,0,1,0,2]$. Chirality of a cycle is the predicate that its three axis flip counts are not all equal (equivalently, not $S_3$-invariant under axis permutation). The Gray flip-count map is just the bit-flip tally along that walk; computation gives the split $(4,2,2)$.
Separately, the J-cost obeys $J(x)=J(1/x)$, read as CPT (particle–antiparticle) symmetry. The directed walk breaks the residual CP symmetry while leaving that J-identity untouched. Upstream, the same module already proves the cycle is chiral by exhibiting bit $0$ flipping four times and bit $1$ twice. Face-pairs are tied to particle generations elsewhere in the foundation stack, so unequal flips become generation-dependent coupling.
proof idea
One-line term wrapper: the claim is definitionally the already-proved statement that the Gray flip-count function is chiral. That upstream proof is a short computation: assume all three counts equal, reduce via native decision that bit $0$ has count $4$ and bit $1$ has count $2$, and obtain $4=2$, contradiction. No new algebra is done here.
why it matters
This is the named CP-breaking half of the module’s CPT-vs-CP package: J-symmetry keeps CPT, while Gray-code chirality breaks CP. It sits next to the flip-asymmetry vector $\Delta=(4/3,-2/3,-2/3)$, the generation-coupling asymmetry, and the master chirality certificate. In the forcing chain it rides on the eight-tick octave (T7) and the three spatial axes (T8): the directed recognition operator on $Q_3$ is forced to treat axes unequally, which the module reads as the geometric seed of flavor mixing (CKM/PMNS). No downstream dependents are wired yet; the declaration is the public alias that packages the computational chirality fact as the CP-violation claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.