Fermion
plain-language theorem explainer
The Fermion inductive type enumerates the nine charged Standard Model fermions consisting of the electron, muon, tauon, and the six quarks. Mass-law verifications and kinetic certificates cite this enumeration to apply the yardstick times phi to the power rung minus eight plus gap formula with zero free parameters. The declaration is a direct inductive definition that derives decidable equality, representation, and finite-type instances automatically.
Claim. The inductive type of charged Standard Model fermions is generated by the nine constructors electron, muon, tauon, up, charm, top, down, strange, bottom.
background
The Standard Model mass verification module states the mass law as m(particle) equals yardstick of the sector times phi raised to the power of rung minus eight plus gap from Z, with all constants fixed by cube geometry in three dimensions and the recognition composition law. This Fermion type restricts attention to the nine charged species. Upstream anchor definitions supply the broader inductive type that includes three neutrino flavors, from which the present enumeration is extracted for PDG comparisons.
proof idea
The declaration is an inductive definition that enumerates the nine charged fermions and derives the DecidableEq, Repr, and Fintype instances in a single step.
why it matters
This definition supplies the domain for all downstream mass-law applications that verify phi-ladder predictions for Standard Model fermions. It is used by the FermionKineticCert structure to certify positive masses and exact phi ratios, by SpectralEmergenceCert to obtain the 24 chiral flavors from D equals 3, and by constant lemmas such as rung and l0_pos. It bridges the geometric forcing chain T0-T8 to numerical verification inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.