zBosonMass_GeV
plain-language theorem explainer
The declaration supplies the constant value 91.1876 GeV for the Z boson mass. Electroweak model builders in Recognition Science cite it when checking mass ratios against the weak mixing angle or when bounding the Higgs vacuum expectation value. The definition is a direct numeric assignment with no reduction steps or lemmas.
Claim. The Z boson mass is defined by the constant assignment $m_Z = 91.1876$ GeV.
background
The ElectroweakBosons module derives W and Z masses from the Higgs vacuum expectation value and the weak mixing angle within the Recognition Science framework. The module states that electroweak symmetry breaking corresponds to a J-cost minimum, yielding the gauge-boson mass relation $m_Z = m_W / cos(θ_W)$ and placing the scale on the φ-ladder. The supplied module doc lists the target values $m_Z ≈ 91.19$ GeV and $sin²θ_W ≈ 0.231$.
proof idea
The declaration is a direct constant definition that hardcodes the experimental central value 91.1876. No lemmas or tactics are invoked; the body is a single numeric literal.
why it matters
This constant feeds the parent theorems vev_determines_scale (which places the electroweak scale above the boson masses) and wz_ratio_equals_cos_theta (which verifies the observed ratio equals cos(θ_W) to within 0.005). It anchors the electroweak sector of the Recognition Science predictions (P-015, P-016) and supplies the φ-ladder rung used to test consistency with the eight-tick octave and the derived constants c = 1, ħ = φ^{-5}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.