three_generations_from_dimension
plain-language theorem explainer
The theorem shows that the number of opposite face pairs on the physical 3-cube equals 3, which the framework maps directly to the three fermion generations. Researchers deriving the standard model from Recognition Science would cite this to ground the generational count in dimension forcing. The proof is a one-line term reduction that substitutes the definitions of face_pairs and D_physical then applies reflexivity.
Claim. The number of pairs of opposite faces on the physical 3-cube is 3, hence the ledger assigns exactly three fermion generations.
background
The module formalizes P-001 on the origin of three fermion generations. DimensionForcing supplies the constant D_physical := 3 as the unique spatial dimension. The local definition face_pairs(D) := D counts the pairs of opposite faces on a D-cube; each pair supplies one independent coherence axis in the ledger's mode structure. The upstream result D_physical is RS-compatible and is forced by the eight-tick octave together with spinor structure. The module setting is the cube geometry Q_3 whose face-pair count fixes the generation number.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the local definition face_pairs (the identity on the dimension) and the constant D_physical, then closes by reflexivity.
why it matters
This declaration resolves P-001 by deriving the three-generation count from the forced spatial dimension D=3 (T8 in the unified forcing chain). It supplies the direct link between cube geometry and the ledger's mode-counting, confirming that neither two nor four generations arise. The result anchors downstream ledger constructions in CKM mixing and spectral emergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.