pith. machine review for the scientific record. sign in
theorem other other high

Q3_face_pairs

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 104theorem Q3_face_pairs : face_pairs 3 = 3 := by native_decide

depends on (2)

Lean names referenced from this declaration's body.