pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.ParticleGenerations

show as:
view Lean formalization →

This module derives exactly three particle generations from the forced D=3 cube geometry and the phi-ladder in the J-cost ledger. It would be cited by researchers formalizing the standard-model fermion spectrum from discrete recognition rules. The argument proceeds via definitions of face-pair counts on the cube followed by direct theorems establishing three generations, excluding two or four.

claimThe number of particle generations equals 3, obtained from the face-pair count $D$ on the $D$-cube together with the self-similarity constraint on the J-cost functional $J(x) = (x + x^{-1})/2 - 1$.

background

The module follows DimensionForcing, which proves spatial dimension D=3 is forced by the RS framework, and PhiForcing, which proves that φ is forced by self-similarity in a discrete ledger with J-cost. It introduces face_pairs(D) as the count of opposite-face pairs on a D-dimensional cube, which equals D, and face_pairs_at_D3 as the specialization to the forced dimension. The local setting is the Foundation layer where cube symmetry and the phi-ladder together constrain the fermion spectrum.

proof idea

The module opens with the definition face_pairs(D) := D. It then applies the upstream D=3 result to obtain face_pairs_at_D3 and proves three_generations_from_dimension by matching the cube face count to the number of allowed rungs on the phi-ladder. Separate one-line theorems establish no_fourth_generation and not_two_generations by showing that additional or fewer generations would violate the J-cost self-similarity condition.

why it matters in Recognition Science

This module supplies the three-generation count that feeds GaugeFromCube (SU(3)×SU(2)×U(1) from Q3 automorphism), QuarkColors (N_c=3), TopologicalConservation (linking charges in D=3), and YangMillsMassGap (mass gap from J-cost). It closes the RS step from forced dimension T8 to the observed three-family structure, consistent with the eight-tick octave and the alpha band.

scope and limits

used by (4)

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)