face_pairs
plain-language theorem explainer
The definition computes the number of pairs of coordinate axes in D dimensions as the binomial coefficient binom D 2. Researchers deriving gauge groups and particle generations from hypercube symmetries cite this when linking D equals 3 to the three color charges or three generations. It is implemented as a direct arithmetic expression without additional lemmas.
Claim. For a natural number $D$, the number of 2-face pair axes on the D-dimensional cube equals $D(D-1)/2$.
background
The Spectral Emergence module starts from the forced dimension D equals 3 and the 3-cube Q_3 with 8 vertices. It shows how the cube's face structure forces the Standard Model content, including gauge ranks summing to 6 and exactly three generations. The count of face-pair axes corresponds to choosing two distinct dimensions, which aligns with the S_3 action on axes for color. This relies on the cube automorphism group of order 48 and the J-cost structures from upstream modules on ledger factorization and complexity.
proof idea
The declaration is a one-line definition that applies the standard formula for the number of unordered pairs from D items.
why it matters
This count enters the gauge generation unification theorem, where it equals the fundamental representation dimension for the color sector, and supports the gauge group certificate identifying B_3 with the Standard Model symmetries. It realizes the link from the eight-tick octave and D equals 3 in the forcing chain to the three generations and three colors. No open questions are attached to this basic count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.