pith. sign in
module module moderate

IndisputableMonolith.Physics.ElectroweakBosons

show as:
view Lean formalization →

The ElectroweakBosons module supplies definitions for W and Z boson masses, vacuum expectation value, weak mixing angle, and related ratios expressed in GeV. Physicists deriving the weak force from the RS ledger would cite these constants when matching to observed electroweak parameters. It is a definition module consisting of direct assignments without proofs or derivations.

claimDefinitions of the W-boson mass $m_W$ (GeV), Z-boson mass $m_Z$ (GeV), vacuum expectation value $v$ (GeV), $\sin^2 heta_W$, $ rac{m_W}{m_Z}$, and weak coupling $g$ in the Recognition Science framework.

background

The module imports the RS time quantum $ au_0 = 1$ tick from Constants and the self-similar discrete ledger with J-cost from PhiForcing, where phi is forced as the fixed point of self-similarity. These supply the phi-ladder and J-cost structure used to anchor electroweak scales. The local setting is the emergence of the weak sector from the same ledger that produces the phi-forced constants and eight-tick octave.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies the electroweak parameters that feed the WeakForceEmergence module (P-019), which derives the weak nuclear force from the ledger structure. It closes the interface between the phi-forcing foundation and the explicit boson masses needed for weak interaction phenomenology.

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)