Pith. sign in
module module high

IndisputableMonolith.Foundation.ParticleGenerations

show as:
view Lean formalization →

Opposite-face pairs of the D-cube are identified with fermion generations, so the forced spatial dimension D = 3 yields exactly three generations. The module defines the face-pair count, specializes it at D = 3, and excludes two-only and four-generation alternatives. Gauge, chirality, mass-basis, and baryogenesis modules import these facts. The argument is a combinatorial count of face pairs plus the upstream dimension-forcing result.

claimA $D$-cube has exactly $D$ pairs of opposite faces. At the forced spatial dimension $D = 3$ there are three such pairs, identified with the three Standard Model fermion generations. In particular there is no consistent two-generation or four-generation counting from this geometry.

background

Recognition Science forces spatial dimension $D = 3$ (forcing chain step T8) in the DimensionForcing module, via topological linking and related arguments on the discrete ledger. Independently, PhiForcing forces the golden ratio $\varphi$ as the self-similar fixed point of the J-cost ledger. The present module sits between those foundations and the particle-sector geometry on the 3-cube $Q_3$.

The elementary geometric fact is that a $D$-dimensional hypercube has $2D$ faces, which pair into $D$ opposite pairs (each coordinate axis contributes one pair of faces normal to that axis). The module treats those opposite-face pairs as the combinatorial slots for fermion generations. Sibling objects record the general count, its value at $D = 3$, and the exclusion of two- and four-generation alternatives.

Downstream, each face of $Q_3$ is tied to a generation pair in FaceWinding, and Gray-code chirality on those faces supplies the geometric origin of CP violation used in baryogenesis.

proof idea

The module is a short foundation layer, not a deep proof development. It defines the opposite-face-pair count as the integer $D$ for a $D$-cube, then specializes at the forced value $D = 3$ to obtain three pairs. Two companion statements rule out a pure two-generation counting and a fourth generation from the same face-pair geometry. The only external input is the already-proved forcing of $D = 3$ from DimensionForcing; no new analytic estimates are required.

why it matters in Recognition Science

Three generations is an empirical Standard Model input; here it is read off the forced cube geometry once $D = 3$ is in hand (T8). FaceWinding quotes the generation-pair identification explicitly when assigning signed winding numbers on $Q_3$ faces as the geometric seed of CP violation. GrayCodeChirality and MassWeakBases build the chiral cycle and the mass/weak eigenstate bases on that same three-dimensional generation space, feeding the CKM overlap.

GaugeFromCube derives $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ from $\mathrm{Aut}(Q_3)$ and needs the generation count aligned with the cube. Cosmology importers (SakharovFromLedger, BaryonAsymmetryDerivation) use the generation structure together with Gray-code chirality so that $J_{CP} > 0$ plus Sakharov conditions yield $\eta_B > 0$. QuarkColors and TopologicalConservation likewise sit on the three-generation cube bookkeeping. Without this module the particle-sector face geometry would float free of the dimension-forcing chain.

scope and limits

used by (13)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (5)