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

Generation

show as:
view Lean formalization →

The inductive type labels the three fermion generations as distinct cases for use in deriving CKM mixing angles from rung differences on the phi-ladder. Researchers computing quark mixing parameters or the Jarlskog invariant would reference this type when assigning the rung values 0, 11, and 17 to the generations. The declaration is realized as a direct inductive definition with three constructors, matching the finite-type versions appearing in the spectral and ledger modules.

claimThe type of fermion generations is the inductive type with three constructors: first, second, and third.

background

The CKM module derives mixing matrix elements from rung differences between up and down quark generations on the phi-ladder, with the module doc stating that angles satisfy θ_ij ~ φ^{-Δτ/2} and the CP phase arises from residue asymmetry. Generations are characterized by parity patterns across the three spatial dimensions in the upstream ThreeGenerations module, while the SpectralEmergence version is an abbreviation for Fin 3 that confirms the count equals the cube dimension. The RSLedger version supplies the explicit inductive definition of the three generations of fermions.

proof idea

This declaration is a direct inductive definition that introduces the three constructors first, second, and third. No lemmas or tactics are applied beyond standard inductive type formation.

why it matters in Recognition Science

The type supplies the domain for CKMPhenomenology and jarlskog computations that produce the mixing angles and Jarlskog invariant as forced dimensionless outputs. It feeds the parent result three_generations_from_dimension, which resolves the three-generation count from D = 3 via face pairs of the Q3 cube. In the framework this realizes the T8 forcing of three spatial dimensions and links to the eight-tick octave structure.

scope and limits

formal statement (Lean)

  21inductive Generation | first | second | third
  22deriving DecidableEq, Repr
  23

used by (40)

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

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.