fermionMass
plain-language theorem explainer
fermionMass assigns each Standard Model fermion its predicted mass by feeding its sector, rung, and charge gap into the Recognition Science mass law. Particle physicists checking RS predictions against PDG data would cite this definition when stating positivity or explicit values for the nine charged fermions. It is a one-line wrapper that composes the master mass formula with the three fermion extractors.
Claim. The mass of fermion $f$ is $m(f) = y(s) · φ^{r-8+g(Z)}$, where $s$ is the sector of $f$, $r$ its rung on the phi-ladder, $Z$ its charge number, $y(s)$ the sector yardstick, $φ$ the golden ratio, and $g$ the gap correction.
background
The module states the mass law as $m = $ yardstick(Sector) $× φ^{r-8 + gap(Z)}$, derived from cube geometry in three dimensions with zero free parameters. Upstream, MassLaw.predict_mass supplies the core formula yardstick sector * (phi ^ ((rung : ℝ) - 8 + gap_correction Z_val)) and is described as the master mass law that predicts the mass of a species in a given sector. Fermion is the inductive type listing the nine charged fermions (electron, muon, tauon, up, charm, top, down, strange, bottom), with sector, rung, and Z extracted by sibling definitions that map leptons to the Lepton sector and quarks to UpQuark or DownQuark sectors.
proof idea
This definition is a one-line wrapper that applies predict_mass to the outputs of fermionSector, fermionRung, and fermionZ for the input fermion.
why it matters
The definition supplies the mass values used by all_fermion_masses_pos and the individual positivity theorems (electron_mass_pos, muon_mass_pos, charm_mass_pos, etc.). It implements the mass law inside the Recognition Science framework, where masses follow phi-scaling on the ladder with D=3 and the eight-tick octave. The module documentation notes that full numerical verification against PDG 2024 values remains a hypothesis pending interval arithmetic on phi-rpow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.