module module high

`IndisputableMonolith.StandardModel.ElectroweakMassBridge`

The ElectroweakMassBridge module supplies the tree-level mass formulas for the W and Z bosons together with the Weinberg angle in the Recognition Science setting. It translates the Higgs vacuum expectation value v from the upstream HiggsEFTBridge into Standard Model electroweak parameters. Physicists verifying the low-energy limit of the RS-derived Higgs sector would reference these identities when checking unitarity bounds. The module contains only direct definitions and elementary inequalities with no non-trivial proofs.

claim$m_W^2 = g^2 v^2/4$, $m_Z^2 = (g^2 + g'^2)v^2/4$, together with the derived relations $m_W < m_Z$, $m_W/m_Z = g/√(g^2+g'^2)$, and the trigonometric identities $cos^2θ_W = g^2/(g^2+g'^2)$, $sin^2θ_W = g'^2/(g^2+g'^2)$ that follow from neutral-gauge-boson diagonalization.

background

This module sits inside the Standard Model chain that begins with the RS cost geometry in HiggsEFTBridge, where the dimensionless coordinate ε = h/v is introduced and the canonical Higgs EFT is reached. It imports the fundamental time quantum τ₀ = 1 from Constants. The module defines the squared masses mW_sq and mZ_sq directly from the gauge couplings and the Higgs vev, together with the trigonometric identities for the weak mixing angle that follow from the diagonalization of the neutral gauge boson mass matrix.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions here are imported by the HiggsEFTLowEnergyLimit master certificate and by the LongitudinalVectorScattering module that checks perturbative unitarity in W_L W_L scattering. They close the link from RS cost geometry through the canonical Higgs EFT to the concrete electroweak mass spectrum required for the high-energy cancellation arguments.

scope and limits

Does not derive the values of the gauge couplings g and g' from Recognition Science primitives.
Does not include loop corrections or running of parameters with energy scale.
Does not address the Higgs mass or potential beyond the vev.
Does not treat fermion mass generation or Yukawa couplings.

used by (3)

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

IndisputableMonolith module_import
IndisputableMonolith.StandardModel.HiggsEFTLowEnergyLimit module_import
IndisputableMonolith.StandardModel.LongitudinalVectorScattering module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.StandardModel.HiggsEFTBridge module_import

declarations in this module (19)

def mW_sq L50
def mZ_sq L53
def mW L56
def mZ L59
theorem mW_sq_nonneg L62
theorem mZ_sq_nonneg L69
theorem mW_sq_le_mZ_sq L78
theorem mW_sq_lt_mZ_sq_of_gp_pos L87
theorem mW_over_mZ_sq L100
def cos_sq_thetaW_SM L110
def sin_sq_thetaW_SM L113
theorem cos_sq_plus_sin_sq_thetaW L116
theorem mW_over_mZ_sq_eq_cos_sq L126
theorem cos_sq_thetaW_in_unit_interval L132
theorem mZ_sq_ge_mW_sq L143
theorem mW_over_mZ_eq_cos_thetaW L147
structure ElectroweakMassBridgeCert L176
def electroweakMassBridgeCert L195
theorem electroweakMassBridgeCert_inhabited L204