bit12_equal
plain-language theorem explainer
Bits 1 and 2 of the canonical 3-bit Gray-code cycle on the cube flip equally often over one eight-tick period. Anyone tracking the residual S₂ symmetry of the flip-count vector (4,2,2) cites this equality. Together with the four-fold flip of bit 0 it shows the walk breaks full S₃ axis permutation down to S₂×1. The proof is a one-line native decision on a finite list count.
Claim. During the canonical eight-tick Gray-code walk on the 3-cube, the number of flips of axis $1$ equals the number of flips of axis $2$: $\mathrm{count}(1)=\mathrm{count}(2)$.
background
The module studies the directed Gray-code cycle on the 3-cube $Q_3$, the geometric carrier of the eight-tick recognition operator. The walk visits the eight vertices in the order $[0,1,3,2,6,7,5,4]$ and therefore flips coordinate bits in the pattern $[0,1,0,2,0,1,0,2]$.
bitFlipCount b is the number of times bit $b\in{0,1,2}$ appears in that flip list (equivalently, the length of the preimage under the flipped-bit map). Empirically the counts are $(4,2,2)$: bit 0 flips four times while bits 1 and 2 each flip twice. The J-cost itself remains particle–antiparticle symmetric, $J(x)=J(1/x)$, so CPT is preserved; the directed walk is what can break CP.
Sibling lemmas record the individual counts (bit0_flips_four, bit1_flips_two, bit2_flips_two) and the nonzero flip-asymmetry vector $\Delta=(4/3,-2/3,-2/3)$. The present equality is the statement that the two minority axes are interchangeable.
proof idea
Pure computation. Both sides are natural-number values of a list count over a fixed eight-element flip sequence of type Fin 3. native_decide evaluates the two closed terms in the kernel and closes the goal by reflexivity of equality on ℕ. No algebraic lemma is required beyond the definition of the flip-count function.
why it matters
The equality is the residual symmetry half of the chirality certificate. Full S₃ would demand all three flip counts equal; the four-fold excess on bit 0 already kills that, and equality of bits 1 and 2 shows the stabilizer is exactly S₂ on the last two axes. Module-level results that package this fact include flipAsymmetryNonzero, cycle_is_chiral, and the generation-coupling asymmetry that links face-pairs to particle generations.
In the Recognition forcing chain this sits under the eight-tick octave (T7) and the D=3 spatial identification (T8): the three cube axes are the three generations, so unequal flip exposure is the geometric seed of flavor mixing (CKM/PMNS) and of CP violation with CPT intact. The J-cost symmetry $J(x)=J(1/x)$ remains the CPT side; directed Gray-code chirality is the CP-breaking side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.