total_flips
plain-language theorem explainer
Over one full 8-tick Gray-code cycle on the 3-cube, the three bit axes together flip exactly eight times: one flip per tick. Anyone deriving generation-dependent coupling or CKM structure from the directed walk cites this conservation identity. The proof is a one-shot native decision on the finite flip list.
Claim. If $n_i$ is the number of times bit $i\in\{0,1,2\}$ flips along the canonical 8-tick Gray-code cycle on $Q_3$, then $n_0+n_1+n_2=8$.
background
The module studies the directed 3-bit Gray-code walk on the cube $Q_3$, the geometric carrier of the Recognition Science eight-tick octave (forcing step T7). The walk visits every vertex once and returns; each step flips exactly one coordinate bit. The sequence of flipped bits is $[0,1,0,2,0,1,0,2]$.
bitFlipCount i simply counts occurrences of axis $i$ in that list. The J-cost $J(x)=J(1/x)$ remains particle–antiparticle symmetric (CPT), but the directed path need not treat the three axes equally. Summing the three counts to eight is the elementary bookkeeping that every tick contributes one flip, before any asymmetry statement is made.
Upstream, the same total appears in the Standard Model CKM layer as an identical numerical identity on generation flip counts, tying the cube walk to flavor structure.
proof idea
Term-mode proof by native_decide. The definition of each bit-flip count is a finite List.count over the eight-element flipped-bit list, so the three natural-number summands are closed terms; Lean evaluates the equality $4+2+2=8$ by native computation and closes the goal.
why it matters
This identity is the normalization step behind the module’s chirality story. Downstream, StandardModel.CKMExact.total_flips restates the same sum for generation flip counts, so CKM numerics inherit the eight-tick budget. With the total fixed at eight, the observed split $[4,2,2]$ (rather than the $S_3$-symmetric $[8/3,8/3,8/3]$) produces the nonzero flip-asymmetry vector $\Delta=(4/3,-2/3,-2/3)$ used by flipAsymmetryNonzero and cycle_is_chiral.
In the Recognition framework that vector is the geometric seed of CP violation with CPT preserved: face-pairs map to particle generations, so unequal flip exposure yields generation-dependent coupling and flavor mixing. The result sits on the eight-tick octave (T7) and feeds the master chirality certificate without touching the J-cost uniqueness chain (T5) itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.