module module high

`IndisputableMonolith.StandardModel.ElectroweakMassBridge`

The ElectroweakMassBridge module supplies the W and Z boson mass-squared expressions that connect the Higgs vacuum expectation value to gauge couplings inside the Recognition Science Standard Model chain. Low-energy Higgs EFT researchers cite it when closing the link from RS scalar coordinate to electroweak observables. It is a definition module whose content consists of direct algebraic assignments and elementary inequalities.

claim$m_W^2 = g^2 v^2 / 4$ and $m_Z^2 = (g^2 + g'^2) v^2 / 4$, together with the derived ratios and non-negativity statements that follow from $v > 0$.

background

Recognition Science starts from a single functional equation whose forcing chain yields T5 (J-uniqueness), T6 (phi fixed point), T7 (eight-tick octave) and T8 (D = 3). The upstream HiggsEFTBridge module formalises the first segment of the chain: RS cost geometry maps to an effective scalar coordinate ε = h / v, which then supplies the canonical Higgs EFT. Constants supplies the base time quantum τ₀ = 1 tick in RS-native units. ElectroweakMassBridge sits immediately downstream and translates the Higgs vacuum expectation value into the gauge-boson masses that appear in the low-energy limit.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the HiggsEFTLowEnergyLimit master certificate that bundles the full RS-to-Higgs-EFT chain, the LongitudinalVectorScattering module that tests high-energy unitarity, and the root IndisputableMonolith module that exposes the master forcing-chain theorem. It supplies the concrete electroweak mass link required by the six-module Standard-Model sequence cited in the companion paper.

scope and limits

Does not derive the numerical values of g or v from RS primitives.
Does not include fermion mass terms or Yukawa couplings.
Does not address loop corrections or running of couplings.
Does not treat the symmetry-breaking mechanism itself.

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