gray_code_flip_counts
plain-language theorem explainer
The 3-bit Gray-code walk on the eight-tick cycle has hierarchical flip multiplicities 4, 2, and 2. Cosmologists deriving the dark-energy fraction from phase saturation cite this list as the combinatorial seed of the Q₃ mode count 11. It is a literal constant definition, not a proved identity.
Claim. The Gray-code flip-count list for one eight-tick cycle is $[4, 2, 2]$.
background
The module derives the cosmological constant fraction $\Omega_\Lambda = 11/16 - \alpha/\pi$ from phase-mode saturation on the eight-tick DFT. Of 44 frequency modes, 11 are $Q_3$-symmetric; the saturated fraction $11/16$ uses $16 = 2^4$ (4-bit addressing of the cycle) and the mode count 11 built from Gray-code asymmetry.
In the holography layer, one recognition tick on a boundary plaquette flips a single vertex bit: the Gray-code step of the 8-tick traversal. The fundamental time quantum is one tick ($\tau_0 = 1$). The list $[4,2,2]$ records how many times each hierarchical flip class fires in one full octave (period $2^3$, landmark T7).
Doc-comment arithmetic: 4 dominant-axis flips + 4 second-axis activations + 2 + 1 = 11, the structural input to the baryogenesis Gray code and to $\Omega_\Lambda$.
proof idea
Pure definition: the constant list is written as $[4, 2, 2]$. No tactics, no lemmas. Downstream gray_flip_total discharges the sum identity by decide.
why it matters
Parent use is gray_flip_total, which proves the list sums to 8 (total flips in one 8-tick cycle). That total anchors the hierarchical activation story $11 = 4 + 4 + 2 + 1$ feeding $N_{\mathrm{modes,saturated}}$ and ultimately $\omega_\lambda = 11/16 - \alpha/\pi$.
Within Recognition Science this is the combinatorial face of the eight-tick octave (T7) and the three spatial axes (T8): the $[4,2,2]$ asymmetry is how $S_3$ breaking on the 3-bit Gray code produces the 11 $Q_3$ modes in the $\Omega_\Lambda$ budget. It does not itself close the Planck-band certificate; it only supplies the flip multiplicities those later inequalities consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.