Q3_face_pairs
plain-language theorem explainer
A three-dimensional cube has exactly three pairs of opposite faces. Researchers deriving the Standard Model gauge groups and three fermion generations from the binary cube Q3 in Recognition Science would cite this count. The proof evaluates the combinatorial definition of face pairs directly via native decision.
Claim. For the three-dimensional cube the number of face pairs is three: $D(D-1)/2=3$ at $D=3$, or equivalently the binomial coefficient $C(3,2)=3$.
background
The Spectral Emergence module starts from the forced dimension D=3 (T8) to build the binary cube Q3 with 8 vertices. It shows this structure forces SU(3) x SU(2) x U(1) gauge content, exactly three particle generations, and 48 chiral fermion states matching |Aut(Q3)|. The face_pairs definition counts pairs of opposite faces on the D-cube as D(D-1)/2, which equals the number of 2-face pair axes C(D,2).
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the face_pairs expression at dimension three.
why it matters
This result supplies the face-pair count of three for D=3, which the module links directly to three particle generations. It supports the self-consistency loop from T8 through the eight-tick octave and phi-forcing to the gauge dimensions 3+2+1 and the match of 48 states to chiral fermions. The declaration closes a basic combinatorial step in the Q3 derivation of the Standard Model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.