Fermion
plain-language theorem explainer
The Fermion inductive type enumerates the twelve Standard Model fermions by species label. Recognition Science researchers cite this enumeration to index the Z-map, gap function, and phi-ladder mass assignments. The declaration is a direct inductive construction that derives decidable equality, representation, and inhabitedness with no further computation.
Claim. Let $F$ be the inductive type whose constructors are $d,s,b,u,c,t,e,mu,tau,nu_1,nu_2,nu_3$, corresponding to the six quarks, three charged leptons, and three neutrinos.
background
The RSBridge.Anchor module supplies the core bridge from the recognition framework to particle physics. It defines the Fermion species, the charge-indexed integer $Z_i = q̃^2 + q̃^4$ (plus 4 for quarks), the gap function $F(Z) = ln(1 + Z/phi)/ln(phi)$, and the mass-at-anchor scale. The local theoretical setting is Single Anchor Phenomenology, which asserts that the integrated RG residue at the anchor equals the gap function to tolerance ~1e-6. Upstream results include the scalar coefficient mu in the quadratic projector relation $A^2 = mu A$ and the generation torsion tau taking values 0, 11, 17 for generations 0, 1, 2.
proof idea
The declaration is a direct inductive definition that introduces twelve distinct constructors and attaches deriving instances for DecidableEq, Repr, and Inhabited. No lemmas or tactics are invoked; the structure is primitive.
why it matters
This definition supplies the indexing set for downstream certificates such as FermionKineticCert (which derives fifteen fermions per generation from five EW sectors times three colors) and SpectralEmergenceCert (which obtains three generations from the D=3 cube geometry). It fills the enumeration step that connects the forced eight-tick octave and D=3 spatial dimensions to the observed fermion spectrum. Parent results include generations_eq_dimension and the structural derivation fermionsPerGeneration_val.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.