generations_eq_dimension
plain-language theorem explainer
The number of opposite face pairs on the three-dimensional cube equals three, fixing the count of particle generations. Researchers deriving Standard Model structure from the forced dimension D=3 would cite this equality. The proof is a direct term application of the three_generations lemma.
Claim. The number of pairs of opposite faces on the three-dimensional cube equals three, which sets the fermion generation count to three.
background
The Spectral Emergence module starts from the forced spatial dimension D=3 (T8) to construct the binary cube Q₃ with eight vertices. The face_pairs definition counts D pairs of opposite faces on a D-dimensional cube, so face_pairs D := D. Upstream results include the ParticleGenerations.face_pairs definition and the three_generations lemma that specializes it at D=3. This sits inside the self-consistency loop T8 (D=3) → Q₃ → face-pair count → three generations, alongside the |Aut(Q₃)|=48 fermion states and φ-ladder masses.
proof idea
The proof is a one-line term wrapper that directly invokes the three_generations lemma from the ParticleGenerations module.
why it matters
This theorem supplies the explicit link from cube geometry to the three generations required by the module's derivation of SU(3)×SU(2)×U(1) content and the 24 chiral flavors. It fills the step D=3 → 3 face pairs → 3 generations in the T8-forced chain. The result supports the claim that |Aut(Q₃)|=48 matches the Standard Model fermion state count with zero free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.