pith. machine review for the scientific record. sign in
def definition def or abbrev high

generationCount

show as:
view Lean formalization →

generationCount fixes the number of fermion generations at exactly 3 to match the spatial dimension D. Researchers deriving Standard Model fermion counts from Recognition Science cite it when verifying the cube face-pair correspondence or computing total Weyl fermions. The definition is a direct constant assignment with no lemmas or computation.

claimThe number of fermion generations is defined to be 3, equal to the spatial dimension $D$.

background

In the Recognition Science framework the Standard Model fermion content is obtained from the spatial dimension. Module documentation states: 'Three generations of fermions from RS — A1 SM Depth. The Standard Model has three generations of fermions. RS: 3 = D (spatial dimension) = F₂³ axes = cube face-pairs.' Each generation is assigned four fermions (up, down, charged lepton, neutrino), yielding twelve Weyl fermions that equal the number of cube edges.

proof idea

This is a direct definition that assigns the constant 3. No lemmas are applied and no tactics are used.

why it matters in Recognition Science

The definition supplies the generation count required by the GenerationCert structure, which asserts three_generations : generationCount = 3 together with totalFermions = 12 and the cube-edge match. It realizes the module claim that three generations equal D, closing the link from forcing-chain step T8 (D = 3) to observed fermion generations. The sibling theorem generations_eq_D simply reflects the definition via rfl.

scope and limits

formal statement (Lean)

  20def generationCount : ℕ := 3  -- = D

used by (3)

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