gray_flip_total
plain-language theorem explainer
The Gray-code flip multiset [4, 2, 2] sums to 8, matching the total bit flips in one eight-tick cycle. Cosmology derivations that budget Q₃ phase modes from the [4,2,2] asymmetry cite this identity. The proof is a one-line computational decision on a concrete finite list.
Claim. If the Gray-code flip counts are the list $[4,2,2]$, then their sum equals $8$: the total number of bit flips across one eight-tick cycle.
background
The module derives the dark-energy fraction $\Omega_\Lambda = 11/16 - \alpha/\pi$ from phase saturation on the eight-tick DFT. The eight-tick cycle is the T7 octave forced by the Recognition chain; mode addressing uses a 3-bit Gray code whose axis-asymmetry is recorded as the list $[4,2,2]$.
That list is the structural input to the Q₃-mode count: $4+4+2+1=11$ under hierarchical activation (dominant-axis flips, second-axis activations, and residual sectors). The present statement only closes the flip-budget side: the three entries sum to the full eight ticks of the cycle.
Upstream, gray_code_flip_counts is defined exactly as $[4,2,2]$ and documented as the $[4,2,2]$ Gray-code asymmetry that generates the 11-mode count used in baryogenesis and the $\Omega_\Lambda$ saturated fraction.
proof idea
One-line computational proof: decide evaluates the concrete List.sum of $[4,2,2]$ and checks equality with $8$. No lemmas beyond the definition of the flip-count list are required.
why it matters
In the $\Omega_\Lambda$ derivation the saturated fraction $11/16$ rests on two combinatorial facts: sixteen $4$-bit addresses for the eight-tick cycle, and eleven Q₃-symmetric modes built from the $[4,2,2]$ Gray-code asymmetry. This theorem certifies that the flip counts themselves exhaust the eight-tick period (T7), so the asymmetry is a partition of the full cycle rather than an ad-hoc truncation.
No downstream theorem currently depends on it in the graph, but sibling declarations (N_modes_total, N_modes_saturated, omega_raw, omega_lambda and the Planck-band inequalities) sit in the same module and inherit the same $[4,2,2]$ bookkeeping. It is a small proved brick in the phase-mode budget that feeds the claimed interval $\Omega_\Lambda \in (0.680, 0.700)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.