lepton_has_6
plain-language theorem explainer
lepton_has_6 establishes that the Lepton type has cardinality exactly six. Particle physicists and Recognition Science researchers cite it when enumerating Standard Model fermions under the cube-face count. The proof is a one-line wrapper that unfolds the HasCubeFaceCount predicate and decides the equality.
Claim. Let Lepton be the inductive type with constructors electron, muon, tau, nuE, nuMu, nuTau. Then Fintype.card Lepton = 6.
background
HasCubeFaceCount T is the proposition that a type T equipped with Fintype has cardinality exactly 6. Lepton is the inductive enumeration of the six Standard Model leptons. The module collects such instances of the count 6 as the face enumeration of the 3-cube, a direct consequence of three spatial dimensions.
proof idea
The proof is a one-line wrapper. It unfolds HasCubeFaceCount to expose the cardinality equality and applies the decide tactic to confirm it holds for the six constructors of Lepton.
why it matters
This theorem supplies the lepton entry in cubeFaceUniversalityCert and is invoked by quark_lepton_sum and fermion_antifermion_total to reach the totals 12 and 24. It instantiates the C15 structural claim that 6 equals the product of binary face states and D = 3 from the forcing chain T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.