Pith. sign in
module module moderate

IndisputableMonolith.Physics.ElectroweakBosons

show as:
view Lean formalization →

Defines the electroweak sector constants used by Recognition Science: W and Z masses in GeV, the Higgs VEV, Weinberg angle factors, and the weak coupling. Supplies the classical identity m_W/m_Z = cos θ_W and numerical nearness claims (W≈80 GeV, Z≈91 GeV). Downstream weak-force emergence imports these as fixed inputs. Content is mostly named constants and short algebraic identities, not a deep derivation.

claimElectroweak inputs: $m_W$, $m_Z$ (GeV), Higgs VEV $v$, $\sin^2\theta_W$, $\cos\theta_W$, ratio $m_W/m_Z$, identity $m_W/m_Z=\cos\theta_W$, predicted $m_Z$ from $m_W$, and weak coupling $g$, with nearness statements $m_W\approx 80\,\mathrm{GeV}$ and $m_Z\approx 91\,\mathrm{GeV}$.

background

Recognition Science builds particle masses and couplings on the φ-ladder forced by self-similarity of a discrete J-cost ledger (PhiForcing). Constants supplies the RS time quantum and related unit conventions. The electroweak sector still needs the standard kinematic anchors: W and Z pole masses, the Higgs vacuum expectation value, and the Weinberg angle that mixes the neutral gauge fields.

This module packages those anchors in GeV units together with the textbook relation $m_W = m_Z\cos\theta_W$ and a weak coupling $g$. It does not re-derive the Standard Model Lagrangian; it fixes the numerical and algebraic interface that later RS modules use when arguing that the weak force emerges from ledger structure.

proof idea

Definition-heavy module. Masses, VEV, $\sin^2\theta_W$, $\cos\theta_W$, and $g$ are named constants or simple closed forms. The ratio identity is the classical electroweak relation $m_W/m_Z=\cos\theta_W$, proved by direct algebra from those definitions. Predicted $m_Z$ from $m_W$ is the same identity rearranged. Nearness lemmas compare the numeric values to 80 GeV and 91 GeV. No deep forcing argument lives here; φ-forcing and ledger structure sit upstream and are consumed later.

why it matters in Recognition Science

WeakForceEmergence (P-019) imports this module as the electroweak numeric and algebraic substrate: radioactive decay and neutrino couplings in RS are stated relative to $m_W$, $m_Z$, $\theta_W$, and $g$. Without a single place for those symbols, the emergence narrative cannot cite concrete GeV-scale targets or the cos-θ mass relation.

In the broader framework the module sits downstream of φ-forcing and Constants, and upstream of weak-force ledger arguments. It does not itself close a T0–T8 forcing step; it bridges RS units to the measured electroweak scale so later claims can be checked against $m_W\sim 80$ GeV and $m_Z\sim 91$ GeV.

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)