Pith. sign in
module module high

IndisputableMonolith.Foundation.GrayCodeChirality

show as:
view Lean formalization →

On the 3-cube, the standard 8-tick Gray-code Hamiltonian cycle flips the three coordinate bits with multiplicities 4, 2, and 2. That imbalance is the chirality witness: the cycle is not bit-symmetric. Cosmology (baryon asymmetry, Sakharov) and CKM/CP modules cite the flip counts and the IsChiral predicate. Arguments are finite enumeration over the eight cycle edges plus elementary arithmetic.

claimFor the standard Gray-code Hamiltonian cycle on the 3-cube $Q_3$, the per-coordinate bit-flip counts are $n_0=4$, $n_1=2$, $n_2=2$ (total $8$). The cycle is chiral: the triple $(n_0,n_1,n_2)$ is not fully symmetric. Bit 0 is strictly the most flipped coordinate; bits 1 and 2 match. The cost $J$ stays even under $x\mapsto x^{-1}$.

background

Recognition Science runs recognition on the Boolean 3-cube $Q_3$ (forced by $D=3$ in the T0–T8 chain) with an eight-tick Gray-code Hamiltonian cycle (the T7 octave, period $2^3$). Each edge of the cycle flips exactly one coordinate bit. This module counts, for each bit $i\in{0,1,2}$, how many of the eight edges flip that bit.

Upstream, FaceWinding supplies signed face windings of the same cycle as the geometric seed of CP violation; ParticleGenerations identifies the three cube axes with the three fermion generations. Cost supplies the J-cost used to check that the recognition cost remains inversion-symmetric even while the cycle geometry is chiral.

The sibling objects package the counts (grayFlipCounts, per-bit lemmas), the asymmetry predicates (flipAsymmetryNonzero, IsChiral), and the global statement that the Gray cycle is chiral.

proof idea

Definition layer first: bit-flip count along the fixed 8-tick Gray cycle, then the triple of counts. Concrete lemmas are exhaustive checks on that finite edge list: bit 0 flips on four edges, bits 1 and 2 on two each, total eight. Asymmetry is then pure arithmetic: the triple $(4,2,2)$ is not constant, bit 0 strictly dominates, and bits 1 and 2 agree. cycle_is_chiral assembles those facts into the IsChiral witness. Separately, jcost_symmetric records that $J$ is even under inversion, so chirality is geometric rather than a cost asymmetry. No analytic estimates; everything is finite casework on $Q_3$.

why it matters in Recognition Science

Gray-code chirality $[4,2,2]$ is the discrete CP-odd seed that later modules promote into Standard Model and cosmology observables. Downstream, CKMFromCube quotes it explicitly among the structural ingredients (with generation torsion ${0,11,17}$); CycleOperator builds the unitary on $\mathbb{C}^8$ induced by the same directed cycle; MassWeakBases, CPPhaseDerivation, and JarlskogInvariant turn that directed geometry into mixing phases and $J_{CP}$.

On the cosmology side, BaryonAsymmetryDerivation states that $\eta_B>0$ follows from $J_{CP}>0$ "from Gray-code chirality" plus Sakharov conditions; SakharovFromLedger and EtaBExactRungDerivation import the same seed for C/CP violation and the $\phi$-rung pinning of $\eta_B$. Without a proved flip imbalance on the eight-tick cycle, the sign of matter excess and the CKM phase stack have nothing discrete to stand on.

scope and limits

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (24)