IsChiral
plain-language theorem explainer
A 3-axis flip-count assignment is chiral when the three counts are not all equal, i.e. not S₃-invariant. Anyone proving CP violation from the Gray-code 8-tick walk on the cube cites this predicate. It is a one-line propositional definition: negation of universal equality of the three natural-number counts.
Claim. A function $c : \{0,1,2\} \to \mathbb{N}$ (bit-flip counts on the three axes of $Q_3$) is chiral if it is not the case that $c(i)=c(j)$ for all axes $i,j$. Equivalently, the flip counts are not all equal, so they break full permutation symmetry of the three spatial axes.
background
The module Gray Code Chirality fixes the geometric origin of CP violation in Recognition Science. The 8-tick recognition operator walks a directed Gray-code Hamiltonian cycle on the 3-cube $Q_3$, with path $[0,1,3,2,6,7,5,4]$. Each step flips one bit; the resulting flip pattern is $[0,1,0,2,0,1,0,2]$, so bit 0 flips four times and bits 1 and 2 flip twice each.
The J-cost satisfies $J(x)=J(1/x)$, which the module identifies with CPT invariance. Chirality is the complementary notion: the directed walk treats the three axes unequally. Axes are tied to particle generations via face-pairs, so unequal flip counts mean generation-dependent coupling and flavor mixing.
IsChiral packages the combinatorial content of that asymmetry: a flip-count triple is chiral precisely when it fails to be constant on $\mathrm{Fin},3$. Downstream theorems instantiate it at the concrete Gray-code counts $(4,2,2)$.
proof idea
Pure definitional abbreviation. The body is the proposition $\neg(\forall i,j:\mathrm{Fin},3,, c(i)=c(j))$. No tactics, no lemmas: proving IsChiral c means exhibiting two axes whose counts differ. The sibling theorem cycle_is_chiral does exactly that by native_decide on bitFlipCount 0 = 4 and bitFlipCount 1 = 2.
why it matters
This predicate is the formal hinge between the Gray-code geometry and CP violation. cycle_is_chiral asserts it for the canonical counts; cp_broken_by_chirality and cpt_ok_cp_broken rephrase that as CP broken while CPT (J-symmetry) is preserved. ChiralityCert bundles IsChiral grayFlipCounts with the explicit $(4,2,2)$ split and bijectivity of the cycle.
Downstream, derivation_chain_complete in the baryon-asymmetry derivation lists IsChiral grayFlipCounts as the chirality link in the Sakharov chain (three generations from $D=3$, flip asymmetry $[4,2,2]$, positive Jarlskog). BaryonAsymmetryCert and CKMStructureCert sit on the same spine. Framework landmarks: T7 eight-tick octave, T8 $D=3$, and the directed recognition path that breaks $S_3$ while leaving $J(x)=J(1/x)$ intact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.