fermionZ
plain-language theorem explainer
fermionZ maps each of the nine charged Standard Model fermions to the integer Z used in the mass gap by composing the sector classifier with the charge classifier. Mass phenomenology groups cite it when evaluating the phi-ladder term for leptons and quarks inside the zero-parameter RS mass law. The definition is realized as a one-line functional composition of the three maps.
Claim. For fermion $f$, define $Z(f) := Z(s(f), Q(f))$ where $s(f)$ returns Lepton for electron/muon/tauon, UpQuark for up/charm/top, DownQuark for down/strange/bottom; $Q(f)$ returns $-1$, $2/3$ or $-1/3$ respectively; and $Z(s,Q)$ is the integer anchor map $Z(s,Q) = (6Q)^2 + (6Q)^4$ (plus 4 for quarks).
background
The module states RS mass predictions for Standard Model particles via the law $m = $ yardstick(Sector) $× ϕ^{r-8 + gap(Z)}$, with zero free parameters, drawing from cube geometry for D=3 and charge structure. Fermion is the inductive type enumerating electron, muon, tauon, up, charm, top, down, strange, bottom. fermionSector sends the three leptons to Lepton, the three up-quarks to UpQuark, and the three down-quarks to DownQuark. fermionCharge returns -1 for leptons, 2/3 for up-quarks, and -1/3 for down-quarks. The upstream Z definition from Anchor computes (Q6² + Q6⁴) for leptons and adds 4 for quarks, with Q6 = 6Q.
proof idea
One-line definition that feeds the sector and charge of the input fermion into the anchor Z function.
why it matters
fermionZ supplies the Z argument to the downstream fermionMass definition, which applies the mass law predict_mass. It encodes the charge-dependent gap in the phi-ladder for fermions, consistent with the Recognition Science mass formula and the eight-tick octave structure. No open questions are attached to this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.