z_mass_near_91
plain-language theorem explainer
The theorem establishes that the Recognition Science Z boson mass in GeV units satisfies an absolute deviation of less than 1 from the value 91. Electroweak model builders comparing RS-derived spectra to collider measurements would cite this numerical bound. The proof reduces the mass definition by targeted simplification and confirms the inequality through direct numerical evaluation.
Claim. $|m_Z - 91| < 1$ where $m_Z$ denotes the Z-boson mass in GeV obtained from the electroweak symmetry breaking and phi-ladder relations.
background
The module derives W and Z boson masses from the Higgs mechanism in Recognition Science, where electroweak symmetry breaking corresponds to a J-cost minimum. The vacuum expectation value near 246 GeV sets the scale, and the mass relation $m_Z = m_W / cos θ_W$ follows from the gauge structure with the weak mixing angle emerging from geometric embedding. The phi-ladder places the electroweak scale at a specific rung, yielding the listed predictions including $m_Z ≈ 91.19$ GeV.
proof idea
The proof is a one-line wrapper that unfolds the definition of the RS Z-boson mass via simp only on that definition, then applies norm_num to discharge the numerical inequality.
why it matters
This bound supports the electroweak predictions listed in the module (P-015, P-016) and supplies the Z-mass hypothesis for the downstream positivity result wz_masses_positive. It aligns with the mass formula on the phi-ladder and the eight-tick octave structure of the forcing chain. The step closes a verification link between the anchor definitions and the observed electroweak scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.