observed_wz_mass_hierarchy
plain-language theorem explainer
The theorem asserts that the observed W boson mass is positive, the observed Z boson mass is positive, and the W mass is strictly less than the Z mass. A particle physicist embedding empirical inputs into the Recognition Science derivation of electroweak symmetry breaking would cite this result. The proof is a direct term-mode verification that splits the conjunction and normalizes the numerical constants.
Claim. $0 < m_W^{obs} ∧ 0 < m_Z^{obs} ∧ m_W^{obs} < m_Z^{obs}$
background
The module recasts electroweak symmetry breaking as J-cost minimization, identifying the Higgs potential with the J-cost functional and the vacuum expectation value with the cost minimum that breaks SU(2)_L × U(1)_Y to U(1)_EM. Upstream, the shifted cost H(x) = J(x) + 1 satisfies the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y) after reparametrization of the Recognition Composition Law. The theorem supplies the empirical positivity and ordering of the W and Z masses required before the phi-ladder mass formulas and VEV minimization are applied.
proof idea
The term proof applies constructor to split the three-way conjunction into separate goals. Each goal is discharged by norm_num on the constant definitions of mW_observed and mZ_observed, which evaluate directly to the required inequalities.
why it matters
The result anchors the observed mass ordering as an input to the electroweak breaking derivation in the Standard Model module. It precedes the Higgs potential, VEV, and boson mass calculations listed as siblings and supports the RS mechanism that equates the Higgs potential to J-cost. No downstream uses are recorded, so it functions as a base empirical fact for the phi-ladder mass hierarchy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.