ChiralityCert
plain-language theorem explainer
A master certificate packaging Gray-code chirality on the 3-cube: unequal bit-flip counts (4,2,2), J-cost inversion symmetry (CPT), generation coupling asymmetry 2:1, and bijective coverage of the eight vertices. Anyone citing the RS geometric origin of CP violation while CPT is preserved will point here. It is a pure structure definition; the verified inhabitant is assembled elsewhere from the module lemmas.
Claim. A chirality certificate is a record asserting: (i) the Gray-code flip-count map on three axes is chiral (not all three counts equal); (ii) for every $x>0$, $J(x)=J(x^{-1})$; (iii) bit-flip counts are $4,2,2$ on axes $0,1,2$; (iv) generation $0$ sees twice the flips of generation $1$; (v) the directed $3$-bit Gray path visits every vertex of $Q_3$ exactly once (bijective).
background
The module treats the canonical $3$-bit Gray cycle on the cube $Q_3$ as the geometric carrier of recognition ticks. The walk flips bits in the pattern that yields counts $(4,2,2)$ rather than a uniform $8/3$ per axis. Chirality is defined exactly as failure of full $S_3$ invariance of those counts: the flip-count function is not constant on the three axes.
The recognition cost $J(x)=(x+x^{-1})/2-1$ is symmetric under $x\mapsto x^{-1}$. In the RS reading that symmetry is CPT. Face-pairs of the cube are identified with particle generations, so each generation inherits the flip count of its axis; generation flip count is literally the bit-flip count. The directed walk therefore couples unequally to the three generations while the cost functional remains inversion-symmetric.
Upstream facts already proved in-module include the explicit counts (bit $0$ flips four times; bits $1$ and $2$ twice each), non-vanishing flip asymmetry, and the computational theorem that the Gray cycle is chiral.
proof idea
No proof body: this is a structure (record type) whose five fields are propositions. Field chiral demands IsChiral grayFlipCounts; cpt_ok is universal $J$-symmetry; flipCounts packages the three concrete equalities; asymmetry is the $2\times$ generation coupling relation; allVisited is bijectivity of the Gray path. Inhabitation is deferred to the downstream definition that fills each field by named lemmas (cycle_is_chiral, cpt_preserved, the three bit-count theorems, generation_coupling_asymmetry, and path bijectivity).
why it matters
Module doc lists this as the sixth main result: the master certificate bundling Gray-code chirality, CPT preservation via $J$, the $4{:}2{:}2$ split, generation coupling asymmetry, and full vertex coverage. Downstream, a single verified inhabitant is built by plugging in those lemmas, giving a one-object handle for the claim that directed eight-tick recognition on $Q_3$ breaks CP (chiral walk, nonzero flip-asymmetry vector $(4/3,-2/3,-2/3)$) while preserving CPT.
In the forcing chain this sits with the eight-tick octave (T7) and $D=3$ (T8): the $2^3$ period and three spatial axes are exactly the Gray-code setting. The unequal axis driving is the stated RS origin of flavor mixing (CKM/PMNS) and of CP violation without CPT violation. Anyone assembling the CP/CPT story from foundation lemmas cites this bundle rather than the five pieces separately.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.