pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Physics.ElectroweakBosons

show as:
view Lean formalization →

This module defines the W and Z boson masses in GeV along with the vacuum expectation value, weak mixing angle, and their ratios inside the Recognition Science framework. Particle physicists seeking mass predictions from self-similar discrete ledgers would cite these values when comparing to collider data. The module assembles the quantities as definitions that convert RS-native units (from phi-forcing and constants) into GeV-scale numbers near the observed 80 GeV and 91 GeV.

claimThe module supplies $m_W$ (W-boson mass), $m_Z$ (Z-boson mass), $v$ (vacuum expectation value), and $s_W^2 = 1 - (m_W/m_Z)^2$ expressed in GeV, together with the numerical approximations $m_W/m_Z = c_W$ and the weak coupling $g$.

background

Recognition Science starts from a discrete ledger equipped with J-cost, where the PhiForcing module proves that the golden ratio φ arises as the unique self-similar fixed point satisfying the functional equation J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The Constants module fixes the fundamental time quantum τ₀ = 1 tick. ElectroweakBosons converts these structures into the electroweak sector by placing the W and Z masses on the phi-ladder and expressing them in laboratory GeV units.

proof idea

This is a definition module, no proofs. It directly assembles the listed quantities (wBosonMass_GeV, zBosonMass_GeV, vev_GeV, sin2_theta_W, wz_mass_ratio, etc.) from the imported constants and phi-forcing results.

why it matters in Recognition Science

The definitions supply the concrete boson masses required by the downstream WeakForceEmergence module (P-019), which derives the weak nuclear force from the underlying ledger structure. They close the numerical link between the phi-forced constants and the observed electroweak scale.

scope and limits

used by (1)

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 (36)