pith. machine review for the scientific record. sign in
def definition def or abbrev high

rs_mass_MeV

show as:
view Lean formalization →

The mass assignment in Recognition Science units gives the MeV value for sector s at rung r as 2 to the power B(s) times phi to the combined exponent -5 plus r0(s) plus r, then divided by 10^6. Particle physicists checking lepton and electroweak predictions against PDG data cite this formula for the phi-ladder masses. It is a direct algebraic definition that composes the pre-derived sector exponents B and r0 with the universal phi scaling.

claim$m(s,r) = 2^{B(s)} ϕ^{-5} ϕ^{r_0(s)} ϕ^r / 10^6$ in MeV, where $s$ is a sector (lepton, up-quark, down-quark or electroweak), $B(s)$ is the sector power of two from cube edge counting, $r_0(s)$ is the sector phi-exponent offset from wallpaper geometry, and $r ∈ ℤ$ is the rung index.

background

The module compares Recognition Science mass predictions to PDG experimental values, which are imported constants rather than derived. The lepton-sector formula simplifies to $ϕ^{57+r} / (2^{22} × 10^6)$ MeV because B(Lepton) = -22 and r0(Lepton) = 62. B_pow assigns the powers of two per sector from cube edge counting; r0 assigns the phi-exponent offsets per sector from wallpaper plus cube geometry. Upstream, the Constants structure bundles the Recognition Science constants including phi, while Anchor.Sector enumerates the four sectors.

proof idea

This is a direct noncomputable definition that multiplies 2 raised to B_pow(s), phi to the power -5, phi to r0(s), phi to r, then divides by 10^6. It applies the definitions of B_pow and r0 from the Anchor module together with the phi constant from Constants.

why it matters in Recognition Science

This definition supplies the concrete values used in ChargedLeptonMassScoreCardCert to certify relative errors below 0.003 for the electron, 0.04 for the muon and 0.03 for the tau; it also supplies z_pred for the Z boson. It realizes the phi-ladder mass formula of the Recognition Science framework, with exponents fixed by the eight-tick octave and D = 3 geometry. It touches the open question of how tightly the phi scaling reproduces observed masses without extra parameters.

scope and limits

Lean usage

def electron_mass_MeV : ℝ := rs_mass_MeV .Lepton 2

formal statement (Lean)

  42noncomputable def rs_mass_MeV (s : Anchor.Sector) (r : ℤ) : ℝ :=

proof body

Definition body.

  43  (2 : ℝ) ^ (B_pow s) * Constants.phi ^ (-(5 : ℤ)) *
  44    Constants.phi ^ (r0 s) * Constants.phi ^ r / 1000000
  45
  46/-! ## npow prediction helpers -/
  47

used by (27)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.