mZ_observed
plain-language theorem explainer
Recognition Science fixes the observed Z boson mass at 91.2 GeV as an empirical input for electroweak calculations. Particle physicists deriving mass hierarchies from J-cost minima in the Higgs sector would cite this constant when checking consistency with the phi-ladder. The definition is a direct numerical assignment with no further reduction or proof obligations.
Claim. The observed Z boson mass is defined by $m_Z^obs := 91.2$ (in GeV).
background
The module derives electroweak symmetry breaking from the J-cost functional, identifying the Higgs potential $V(φ) = -μ²|φ|² + λ|φ|⁴$ with a J-cost expression whose minimum yields the vacuum expectation value. Upstream, cost is the J-cost of a recognition event (ObserverForcing.cost) or the derived cost of a multiplicative recognizer (MultiplicativeRecognizerL4.cost). The local setting treats the Higgs mechanism as ledger selection of a J-cost minimum that breaks SU(2)_L × U(1)_Y to U(1)_EM while assigning masses to W and Z.
proof idea
Direct constant definition that assigns the empirical value 91.2 with no lemmas or tactics applied.
why it matters
Supplies the numerical anchor for the downstream theorem observed_wz_mass_hierarchy, which asserts the strict ordering 0 < mW_observed < mZ_observed. It closes the empirical side of the J-cost derivation of electroweak breaking (SM-009) and sits inside the T5–T8 forcing chain where masses arise on the phi-ladder. No open scaffolding remains at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.