fermionCharge
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.
claimDefine 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 in Recognition Science
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.
scope and limits
- Does not assign charges to neutrinos or other particles.
- Does not derive charges from Recognition Science axioms or the forcing chain.
- Does not compute masses or perform the PDG comparison.
- Does not include weak isospin or neutral-current structure.
Lean usage
example : fermionCharge .up = 2/3 := rflformal statement (Lean)
57def fermionCharge : Fermion → ℚ
58 | .electron | .muon | .tauon => -1
59 | .up | .charm | .top => 2/3
60 | .down | .strange | .bottom => -1/3
61