rs_mass_MeV
plain-language theorem explainer
rs_mass_MeV supplies the Recognition Science mass prediction in MeV units for any sector and integer rung. Particle physicists comparing RS outputs to PDG data cite it when computing residuals for leptons, quarks, and the Z boson. The definition is a direct arithmetic expression that multiplies the sector power of two, the fixed phi to the minus five, the sector offset r0, the rung exponent, and divides by one million.
Claim. For sector $s$ and rung $r$, the predicted mass in MeV is $2^{B(s)} phi^{-5} phi^{r_0(s)} phi^r / 10^6$, where $B(s)$ and $r_0(s)$ are the sector-specific exponents obtained from cube and wallpaper geometry.
background
The Verification module compares RS mass predictions to PDG values while treating experimental masses as quarantined imported constants. Sector is the inductive type with constructors Lepton, UpQuark, DownQuark, and Electroweak. B_pow maps each sector to its power-of-two exponent derived from cube edge counting, for example -22 for leptons. r0 maps each sector to its phi-exponent offset derived from wallpaper plus cube geometry, for example 62 for leptons. Constants supplies the phi value together with the other RS constants.
proof idea
This is a direct definition that assembles the mass expression by substituting B_pow s for the power of two, Constants.phi raised to -5, to r0 s, and to r, then dividing by 1000000. It applies the upstream definitions of B_pow and r0 with no additional lemmas or tactics.
why it matters
ChargedLeptonMassScoreCardCert invokes rs_mass_MeV to certify relative residuals below 0.003 for the electron and similar bounds for muon and tau. ElectroweakMasses uses it to define z_pred for the Z boson at rung 1. The definition realizes the RS mass formula on the phi-ladder, with sector exponents B_pow and r0 obtained from the eight-tick octave and three-dimensional geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.