mW_observed
Recognition Science supplies the observed W boson mass as the constant 80.4 GeV to anchor its J-cost derivation of electroweak symmetry breaking. A physicist working on the Standard Model inside the Recognition framework would cite this value when verifying the W-Z hierarchy or matching experimental inputs. The declaration is a direct numerical assignment in real numbers that enables the ordering theorem in the same module.
claimThe observed W-boson mass is defined as $m_W = 80.4$ GeV.
background
The module treats electroweak symmetry breaking as spontaneous selection of a J-cost minimum. The Higgs potential is identified with the J-cost functional, the vacuum expectation value with that minimum, and the breaking SU(2)_L × U(1)_Y → U(1)_EM with the ledger choosing a specific configuration. Observed masses are introduced as empirical anchors with the stated values m_W ≈ 80.4 GeV and m_Z ≈ 91.2 GeV.
proof idea
The declaration is a direct definition that assigns the real number 80.4. No lemmas or tactics are applied.
why it matters in Recognition Science
This constant is the input to the theorem observed_wz_mass_hierarchy, whose doc-comment states that observed W and Z masses are positive and strictly ordered. It fills the empirical slot in SM-009, where the Higgs potential equals the J-cost functional. In the larger framework it supports phi-ladder mass formulas and consistency checks against the alpha band.
scope and limits
- Does not derive the numerical value from J-cost minimization or the phi-ladder.
- Does not specify units or conversion conventions beyond the implicit GeV scale.
- Does not incorporate quantum corrections or renormalization-group running.
Lean usage
theorem test : mW_observed = 80.4 := rflformal statement (Lean)
89noncomputable def mW_observed : ℝ := 80.4