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

z_pred

show as:
view Lean formalization →

z_pred defines the predicted Z boson mass in MeV by evaluating the RS mass formula at the Electroweak sector and rung 1. Particle physicists checking Recognition Science mass predictions against PDG data would cite this definition when verifying the 0.13 percent accuracy bound. It is realized as a direct one-line application of the rs_mass_MeV helper with the sector and rung parameters.

claim$z_{pred} = 2 phi^{51} / 10^6$ in MeV, where $phi$ is the golden ratio and the exponent 51 follows from the phi-ladder assignment for the Z boson at rung 1 in the Electroweak sector.

background

The ElectroweakMasses module predicts boson masses from the Recognition Science phi-ladder. The upstream definition rs_mass_MeV(s, r) computes $2^{B_{pow} s} phi^{-5} phi^{r0 s} phi^r / 10^6$, where s is the sector and r the rung. For the Z boson the module assigns the Electroweak sector at rung 1, which simplifies to the explicit form $2 phi^{51}/10^6$ MeV. The module distinguishes this assignment from the W boson (derived via the Weinberg angle) and the Higgs (approximated from the W mass).

proof idea

The definition is a one-line wrapper that applies rs_mass_MeV to the Electroweak sector at rung 1.

why it matters in Recognition Science

z_pred supplies the central value used by the Electroweak verification certificate EWCert and by the bounds and error theorems z_mass_bounds, z_relative_error, and wz_ratio_eq_cos. It implements the module mechanism that replaces the earlier undifferentiated r_boson placeholder with sector-specific rung assignments. In the broader framework it realizes the mass quantization step on the phi-ladder that follows from T5 J-uniqueness and the phi fixed point.

scope and limits

formal statement (Lean)

  73noncomputable def z_pred : ℝ := rs_mass_MeV .Electroweak 1

proof body

Definition body.

  74

used by (6)

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

depends on (1)

Lean names referenced from this declaration's body.