bitFlipCount0
plain-language theorem explainer
The definition assigns the integer 4 to the Gray code chirality flip count on the 3-cube for axis 0, obtained by direct enumeration on the cycle [0,1,3,2,6,7,5,4]. Cosmologists deriving the exact φ-rung for the baryon-to-photon ratio η_B cite it as the chirality factor in the torsion-gap witness that yields -44. The assignment is a constant definition with no lemmas or computation steps.
Claim. Let $b_0$ denote the number of flips of bit 0 in the canonical Gray code cycle on the 3-cube, given by the sequence $[0,1,3,2,6,7,5,4]$. Then $b_0 = 4$.
background
The module derives the integer -44 that fixes the φ-rung of η_B via three equivalent combinatorial witnesses, all reducing to integrationGap D - 1 at D = 3. The chirality-torsion witness is -(bitFlipCount0 × torsionGap01) = -(4 × 11) = -44, where torsionGap01 comes from the CW-filtration spectrum {0, 11, 17}. This definition supplies the factor 4 from the Gray code on Q_3. Upstream, Gap45.Derivation.gap establishes that the integration gap equals 45 at D = 3, while the torsion spectrum and Gray code cycle are taken as standard combinatorial inputs.
proof idea
Direct definition that hard-codes the enumerated count of four bit-0 flips in the listed Gray code sequence. No lemmas or tactics are invoked; the value is asserted by inspection of the cycle.
why it matters
The definition supplies the chirality factor for eta_B_rung_from_chirality, which is proved equal to -44 and enters the EtaBExactRungCert structure that certifies agreement of the dimension, chirality, and fermionic-DOF witnesses. It thereby contributes to the structural unification of the integration gap at D = 3. In the Recognition framework this pins the η_B rung integer without new axioms, consistent with the eight-tick octave and D = 3 forcing steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.