Pith. sign in
module module high

IndisputableMonolith.StandardModel.ElectroweakMassBridge

show as:
view Lean formalization →

The ElectroweakMassBridge module supplies the W and Z boson mass formulas together with weak mixing angle identities that connect the Higgs vacuum expectation value to electroweak observables in the Recognition Science setting. Researchers tracing the Standard Model low-energy limit would reference these when verifying consistency with collider data. The module contains only definitions and direct algebraic consequences with no non-trivial proofs.

claim$m_W^2 = g^2 v^2 / 4$, $m_Z^2 = (g^2 + g'^2) v^2 / 4$, $\\,\cos^2\theta_W = g^2 / (g^2 + g'^2)$, together with the ordering $m_W^2 \le m_Z^2$ and the identity $\cos^2\theta_W + \sin^2\theta_W = 1$.

background

This module operates inside the Standard Model section of the Recognition Science framework. It imports the RS time quantum from Constants and the effective scalar coordinate construction from HiggsEFTBridge, whose doc-comment states the chain RS cost geometry to effective scalar coordinate to canonical Higgs EFT. The module introduces the electroweak mass expressions that follow once the vacuum expectation value v is obtained from the dimensionless RS coordinate ε = h/v after symmetry breaking.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the electroweak mass bridge required by the Higgs EFT Low-Energy Limit master certificate and the Longitudinal Vector-Boson Scattering analysis. It completes the mass step in the chain from RS cost geometry through the Higgs EFT to the W and Z masses, enabling the high-energy unitarity cancellation checks described in the downstream documentation.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (19)