bit0_most_flipped
plain-language theorem explainer
Bit 0 of the canonical 3-bit Gray-code cycle on the cube flips strictly more often than bits 1 and 2. Anyone citing the geometric origin of CP violation or generation-asymmetric coupling needs this inequality. The proof is a one-shot native decision on the finite flip counts [4,2,2].
Claim. During one full 8-tick Gray-code cycle on $Q_3$, the number of flips of bit $0$ strictly exceeds the number of flips of bit $1$, and also strictly exceeds the number of flips of bit $2$.
background
The module establishes that the canonical 3-bit Gray-code cycle on the cube $Q_3$ is chiral: the directed walk distinguishes clockwise from counterclockwise face traversal. That chirality is the Recognition Science origin of CP violation.
The eight-tick recognition operator walks the Gray-code path $[0,1,3,2,6,7,5,4]$, flipping bits in the pattern $[0,1,0,2,0,1,0,2]$. The helper bitFlipCount simply counts, for each axis $b\in{0,1,2}$, how many times that bit appears in the flip pattern. The module doc records the resulting counts as $[4,2,2]$.
J-cost itself is symmetric under $x\leftrightarrow 1/x$ (CPT), so any CP-odd effect must come from the directed path geometry rather than from the cost functional. The flip-count asymmetry is the first concrete witness that the path treats the three cube axes unequally, breaking $S_3$ down to $S_2\times 1$.
proof idea
Pure finite computation. After bitFlipCount is defined as the multiplicity of each bit in the fixed eight-step flip list, the two strict inequalities are decided by native_decide on the concrete natural numbers. No algebraic lemma is required beyond the definition of the count.
why it matters
This is the elementary witness that axis 0 is the preferred (most-flipped) axis of the Gray-code cycle. Downstream, edge_dressed_prefers_axis0 in MassWeakBases re-exports the same inequality to justify that the edge-dressed generation couples preferentially to axis 0, because that axis has the most passive edge interactions per cycle.
In the module's larger story it feeds the flip-asymmetry vector $\Delta=(4/3,-2/3,-2/3)$, the nonzero-norm certificate flipAsymmetryNonzero, and ultimately cycle_is_chiral and the CP-breaking claims. Framework-wise it sits on the T7 eight-tick octave: the directed 8-step walk on $Q_3$ is what forces the $4:2:2$ split and the generation-dependent coupling that the module identifies with CKM/PMNS mixing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.