ElectroweakMassBridgeCert
plain-language theorem explainer
The ElectroweakMassBridgeCert structure assembles the non-negativity of the W and Z mass squares, their ordering with strict inequality for positive g', and the identification of the mass-squared ratio with cos² of the Weinberg angle, all holding for positive gauge couplings and positive electroweak scale v. A physicist assembling the recognition-substrate derivation of the electroweak sector cites this certificate when composing the low-energy effective theory. The construction is a direct assembly of the supporting lemmas mW_sq_nonneg, mZ_sq_
Claim. Let $m_W^2(g,v)=g^2 v^2/4$ and $m_Z^2(g,g',v)=(g^2+g'^2)v^2/4$. The structure asserts $m_W^2(g,v)≥0$, $m_Z^2(g,g',v)≥0$, $m_W^2(g,v)≤m_Z^2(g,g',v)$ with the last inequality strict for $g'>0$ and $v>0$, the ratio equality $m_W^2(g,v)/m_Z^2(g,g',v)=g^2/(g^2+g'^2)$, the identity $g^2/(g^2+g'^2)+g'^2/(g^2+g'^2)=1$, and the window $0<g^2/(g^2+g'^2)≤1$ for $g>0$.
background
This module formalizes the Standard Model tree-level gauge-boson mass relations in terms of the recognition-substrate scale v supplied by the Higgs EFT bridge together with arbitrary positive gauge couplings g and g'. The explicit formulas are $m_W^2=g^2 v^2/4$ and $m_Z^2=(g^2+g'^2)v^2/4$, with the Weinberg angle defined by cos θ_W = g / √(g² + g'²). The certificate collects the algebraic consequences of these expressions under positivity assumptions on g, g', and v. The local theoretical setting is the conditional bridge from the RS substrate scale v (formalized in HiggsEFTBridge) to the SM gauge masses; numerical identification of g and g' with measured values remains an open empirical input separate from this algebraic layer.
proof idea
The declaration is a structure definition whose fields are populated by direct reference to the sibling lemmas: mW_sq_nn is set to mW_sq_nonneg, mZ_sq_nn to mZ_sq_nonneg, mW_le_mZ to mW_sq_le_mZ_sq, mW_lt_mZ to the conditional version mW_sq_lt_mZ_sq_of_gp_pos, ratio_eq_cos_sq to mW_over_mZ_sq_eq_cos_sq, and the remaining fields to cos2_plus_sin2 and cos_sq_window. No additional reasoning steps are required beyond the assembly.
why it matters
This certificate supplies the gauge-mass relations required by HiggsEFTLowEnergyLimitCert, which composes the cost-geometry to Higgs EFT bridge with the W/Z mass structure. It fills the tree-level SM mass-relations step in the recognition chain, conditional on the substrate scale v and positive couplings. The open question it touches is the numerical calibration of g and g' from the RS substrate, tracked under the OPEN_NORMALIZATION tag. It remains compatible with the companion prediction sin² θ_W = (3 − φ)/6 from the Masses module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.