fermionCharge
plain-language theorem explainer
fermionCharge assigns electric charges to the nine charged Standard Model fermions inside the Recognition Science mass verification. Particle physicists comparing the phi-ladder mass formula to PDG values cite it to obtain the integer Z that enters the gap term. The definition is a direct exhaustive case split on the Fermion inductive type returning the rationals -1, 2/3 or -1/3.
Claim. Define the charge map $q : Fermion → ℚ$ by $q(electron) = q(muon) = q(tauon) = -1$, $q(up) = q(charm) = q(top) = 2/3$, $q(down) = q(strange) = q(bottom) = -1/3$.
background
The module states the RS mass law $m(particle) = yardstick(Sector) × φ^(r - 8 + gap(Z))$ with yardstick and rung derived from cube geometry (D=3) and wallpaper groups, zero free parameters. The local Fermion inductive type enumerates the charged leptons and quarks: electron, muon, tauon, up, charm, top, down, strange, bottom. Upstream Anchor modules supply a broader Fermion type that additionally includes neutrinos.
proof idea
The definition is implemented by direct pattern matching on the nine constructors of the Fermion type, returning the corresponding rational charge in each case.
why it matters
fermionCharge supplies the charge argument to the downstream fermionZ definition that computes Z(sector, charge) for insertion into the mass-law gap term. It thereby connects the Recognition Science phi-ladder to standard-model charge assignments, supporting the PDG numerical comparison documented in the module. Mass-law positivity and phi-scaling are already proved upstream in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.