Lepton
plain-language theorem explainer
The Lepton inductive type enumerates the six standard-model lepton flavors as distinct constructors in the Recognition Science cross-domain setting. Researchers verifying structural counts of six across physics and biology domains cite this definition to confirm the lepton sector matches the cube-face enumeration for three spatial dimensions. The declaration is a direct inductive enumeration that automatically derives Fintype and related instances for cardinality proofs.
Claim. The lepton sector consists of the six flavors $e, mu, tau, nu_e, nu_mu, nu_tau$.
background
The CubeFaceUniversality module identifies the integer six with the face count of the three-cube Q3, whose Euler characteristic is V - E + F = 8 - 12 + 6 = 2. This count is required to appear uniformly in each listed domain because six equals 2 times 3, with 2 the binary state per face and 3 the spatial dimension. The supplied Lepton definition supplies the six flavors needed for the lepton_has_6 theorem and the CubeFaceUniversalityCert structure.
proof idea
Inductive definition that directly introduces the six constructors electron, muon, tau, nuE, nuMu, nuTau. Automatic derivation of DecidableEq, Repr, BEq and Fintype supplies the cardinality Fintype.card Lepton = 6 used in downstream statements.
why it matters
This definition supplies the lepton enumeration required by CubeFaceUniversalityCert and by the theorems quark_lepton_sum and fermion_antifermion_total. It instantiates the Recognition Science claim that spatial dimension equals three, with the six faces arising as the product of binary face states and spatial dimension. The upstream tau definition from the Anchor module supplies the generation torsion values used in related mass and power formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.