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

fermion_flavors

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 219def fermion_flavors : ℕ :=

proof body

Definition body.

 220  let quarks := SpectralSector.dim .color * face_pairs 3 * 2  -- 3 colors × 3 gen × 2 (u/d)
 221  let leptons := SpectralSector.dim .hypercharge * face_pairs 3 * 2  -- 1 × 3 gen × 2 (ν/e)
 222  quarks + leptons
 223
 224/-- **THEOREM**: 24 chiral fermion flavors.
 225    Quarks: 3 colors × 3 generations × 2 flavors (up/down) = 18
 226    Leptons: 1 × 3 generations × 2 flavors (ν/e) = 6
 227    Total: 24 -/

used by (6)

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

depends on (5)

Lean names referenced from this declaration's body.