chiralityCert
plain-language theorem explainer
A single certificate packages the Gray-code chirality facts on the 3-cube: the directed 8-tick walk is chiral, J-cost remains CPT-symmetric, bit flips are 4:2:2, generation 0 couples twice as strongly as generation 1, and the path visits every vertex. Anyone citing the geometric origin of CP violation or generation-axis coupling in RS will point here. The body is a pure structure assembly from already-proved lemmas.
Claim. There exists a verified chirality certificate for the canonical 3-bit Gray cycle on $Q_3$: the flip-count triple is chiral; $J(x)=J(x^{-1})$ for all $x>0$; bit-flip counts equal $(4,2,2)$; generation-$0$ flip count is twice generation-$1$; and the Gray path is bijective onto the eight vertices.
background
The module treats the canonical Gray walk on the 3-cube $Q_3$ as the geometric carrier of the eight-tick recognition cycle (T7). The directed edge sequence flips bits in the pattern that yields counts $(4,2,2)$ rather than a uniform $8/3$ per axis. That imbalance is the flip-asymmetry vector $\Delta=(4/3,-2/3,-2/3)$, whose nonzero norm breaks $S_3$ axis permutation symmetry.
Face-pairs of the cube are identified with particle generations. Unequal flip counts therefore mean unequal generation-axis coupling per cycle, which the module presents as the RS origin of flavor mixing and of CP violation. Simultaneously the cost $J$ obeys $J(x)=J(1/x)$, so particle-antiparticle exchange remains cost-neutral: CPT is preserved while directed chirality breaks CP.
ChiralityCert is the master bundle: chirality of the flip counts, CPT identity for $J$, the concrete $(4,2,2)$ counts, the generation-coupling ratio, and bijectivity of the Gray path.
proof idea
One-line structure constructor. Each field is filled by a named prior result: chirality from cycle_is_chiral (non-equality of flip counts via native_decide); CPT from cpt_preserved (direct expansion of $J$ and ring); flip counts from the three native_decide lemmas bit0_flips_four, bit1_flips_two, bit2_flips_two; asymmetry from the first conjunct of generation_coupling_asymmetry; full vertex coverage from grayCycle3_bijective. No new reasoning occurs at this site.
why it matters
This certificate is the single export that downstream cycle-operator work consumes. In particular generation_axis_coupling reads the flip-count triple straight off the certificate, tying generation $g$ to axis $g$ with strength equal to the bit-flip count per eight-tick period.
Within the forcing chain it sits under T7 (eight-tick octave on $2^3$ vertices) and under the geometric reading of $D=3$. It separates the two discrete symmetries cleanly: J-symmetry keeps CPT, directed Gray chirality supplies CP violation and the generation hierarchy. The module's main results list (flipAsymmetryNonzero, cycle_is_chiral, cpt_preserved, generation_coupling_asymmetry) all land here as one auditable object rather than a scatter of lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.