Pith. sign in
module module high

IndisputableMonolith.Foundation.GrayCodeChirality

show as:
view Lean formalization →

Gray-code chirality on the 3-cube counts how often each coordinate bit flips along the 8-tick Hamiltonian cycle. The flip profile is (4,2,2): one axis is preferred, so the cycle is chiral. Cosmology and CKM modules cite this asymmetry as the geometric source of CP violation and a positive Jarlskog invariant. The argument is finite bit-flip enumeration plus non-vanishing asymmetry lemmas.

claimAlong the 8-tick Gray-code Hamiltonian cycle on the cube $Q_3$, the three coordinate bits flip $(4,2,2)$ times respectively. The cycle is chiral: the flip counts are unequal, and bit 0 flips strictly more often than bits 1 and 2. The associated recognition cost $J$ remains symmetric under $x\mapsto x^{-1}$.

background

Recognition Science forces an eight-tick octave (T7) as the minimal closed recognition cycle on the Boolean 3-cube $Q_3$. A Gray-code ordering visits every vertex once by flipping one bit per step and returns after eight ticks. FaceWinding defines signed winding numbers of that cycle around the six faces of $Q_3$, the geometric foundation for CP violation; each face pairs with a generation pair from ParticleGenerations, which formalizes why there are exactly three fermion generations (P-001).

This module measures chirality of the cycle by counting, for each of the three bit axes, how many of the eight edges flip that bit. The Cost import supplies the $J$-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), used here to record that cost symmetry under inversion does not erase the geometric flip asymmetry.

proof idea

The module defines per-bit flip counters on the fixed Gray cycle, then proves by direct counting that bit 0 flips four times and bits 1 and 2 flip twice each (eight flips total). From those counts it obtains a nonzero flip asymmetry, the statement that bit 0 is the most flipped axis, and equality of the two lesser counts. Chirality is the predicate that the three flip counts are not fully symmetric; the cycle satisfies it. A short companion lemma records that $J$ is inversion-symmetric, so the chirality is geometric rather than a cost artifact.

why it matters in Recognition Science

CKMFromCube builds the Cabibbo-Kobayashi-Maskawa matrix from $Q_3$ geometry, generation torsion ${0,11,17}$, and the Gray-code chirality profile $[4,2,2]$. CycleOperator turns the same directed Gray cycle into a unitary on $\mathbb{C}^8$ from which CKM structure emerges; MassWeakBases uses the generation layout for mass versus weak eigenstates. Cosmology imports the module for baryogenesis: BaryonAsymmetryDerivation takes $\eta_B>0$ from $J_{CP}>0$ (Jarlskog from Gray-code chirality) plus Sakharov conditions; SakharovFromLedger and EtaBExactRungDerivation close the ledger and $\phi$-rung routes to the integer $-44$. CPPhaseDerivation and JarlskogInvariant sit on the same chirality source. The module therefore supplies the discrete geometric origin of CP violation in the RS stack.

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)