bit1_flips_two
plain-language theorem explainer
During one full 8-tick Gray-code cycle on the 3-cube, coordinate bit 1 flips exactly twice. Anyone building generation flip weights, CKM structure certificates, or the chirality master certificate cites this count. The proof is a one-line native decision over the finite flipped-bit list.
Claim. Along the canonical $3$-bit Gray-code cycle of length $8$, the number of times bit $1$ is flipped equals $2$.
background
The module studies the canonical directed Gray-code walk on the $3$-cube $Q_3$, the geometric carrier of the eight-tick recognition cycle. The walk visits all eight vertices once and returns; successive edges flip exactly one coordinate bit. The sequence of flipped bits is $[0,1,0,2,0,1,0,2]$.
The helper bitFlipCount tallies, for each axis $b\in{0,1,2}$, how often that bit appears in the flip list. Those three integers are the raw data for the flip-asymmetry vector $\Delta=(4/3,-2/3,-2/3)$, which measures how far the directed cycle breaks $S_3$ axis-permutation symmetry.
In the Recognition Science setting this asymmetry is the geometric seed of CP violation: J-cost remains symmetric under $x\leftrightarrow 1/x$ (CPT), while the directed path treats the three generation axes unequally.
proof idea
One-line computational proof. native_decide evaluates bitFlipCount 1, which is the list-count of the value $1$ inside the fixed eight-element flip sequence, and checks equality with $2$. No algebraic lemmas are required beyond the definition of the count.
why it matters
This is the middle leg of the flip triple $[4,2,2]$ that breaks cube symmetry. It is packaged directly into the chirality certificate (flipCounts), re-exported as the generation-2 flip count, and fed into mixing-angle data and CKM flip weights (axis 1 receives weight $1/4$). Downstream, the same equality appears in the flip-weight sum and value theorems and in the Berry-phase generation-2 computation.
Framework landmark: the eight-tick octave (T7) forces a period-$8$ Gray cycle on $Q_3$; the $4:2:2$ split is what makes that cycle chiral and therefore the RS origin of flavor mixing and CP violation while preserving CPT via J-symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.