Pith. sign in
module module high

IndisputableMonolith.Foundation.ParticleGenerations

show as:
view Lean formalization →

Opposite-face pairs on a D-cube number exactly D, so the forced spatial dimension D = 3 yields three fermion generations and rules out two or four. Anyone tying SM generation count, face windings, CKM bases, or baryogenesis to the RS cube cites this module. The argument is a combinatorial face count specialized at DimensionForcing, with explicit exclusion lemmas.

claimA $D$-cube has exactly $D$ pairs of opposite faces. At the forced dimension $D = 3$ there are three such pairs, identified with three fermion generations; the module also records that the generation count is neither two nor four.

background

Recognition Science forces spatial dimension $D = 3$ (T8) in DimensionForcing, via topological linking and related arguments on the discrete ledger. Independently, PhiForcing fixes $\varphi$ as the self-similar fixed point of the J-cost ledger. This module sits on those two foundations and asks what the cube geometry implies for fermion generations.

The basic geometric object is the count of opposite-face pairs on a $D$-cube: faces come in parallel opposite pairs, one pair per coordinate axis, hence $D$ pairs total. At $D = 3$ the 3-cube $Q_3$ therefore carries three such pairs. Downstream modules treat each pair as a generation slot (FaceWinding: "Each face of $Q_3$ corresponds to a generation pair").

Sibling declarations package the count (face_pairs), its $D = 3$ specialization, the positive claim of three generations from dimension, and the exclusions of a fourth generation and of only two generations.

proof idea

Definition-first module with short combinatorial theorems. face_pairs is the identity map on dimension (D pairs for a D-cube). face_pairs_at_D3 evaluates that count at the forced $D = 3$. three_generations_from_dimension is the identification of that value with the generation count. no_fourth_generation and not_two_generations are the complementary inequalities, discharging the usual phenomenological alternatives by the same face-pair arithmetic rather than by dynamical mass bounds.

why it matters in Recognition Science

This is the RS origin of "exactly three generations": not an input, but the face-pair count of the forced 3-cube. FaceWinding builds signed windings on those generation faces as the geometric seed of CP violation. GrayCodeChirality uses the same face structure to prove the canonical Gray-code cycle on $Q_3$ is chiral. GaugeFromCube and QuarkColors hang SM gauge and color structure on $Q_3$ automorphisms and faces; MassWeakBases defines mass and weak eigenbases on the three-dimensional generation space whose overlap is the CKM matrix.

Cosmology imports the module for baryogenesis scaffolding: SakharovFromLedger and BaryonAsymmetryDerivation need a fixed generation count and CP-odd face data before they can discuss $\eta_B$ sign and magnitude. In the forcing chain this is the bridge from T8 ($D = 3$) into particle content.

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)