module module moderate

`IndisputableMonolith.StandardModel.WZMassRatio`

The WZMassRatio module supplies numerical definitions for the W and Z boson masses using PDG values in GeV along with derived ratio and Weinberg angle quantities. It supplies the concrete inputs required for Phase 2 electroweak checks inside Recognition Science. The module consists entirely of definitions and imports only the base Constants module.

claim$m_W = 80.377$ GeV, $m_Z = 91.1876$ GeV; mass ratio $m_W/m_Z$; $\sin^2 heta_W = 1 - (m_W/m_Z)^2$

background

This module sits in the StandardModel domain and imports IndisputableMonolith.Constants, whose fundamental object is the RS time quantum $ au_0 = 1$ tick. The sibling definitions m_W, m_Z, massRatio, weinbergAngle and their value companions provide the empirical mass pair needed to interface with the phi-ladder mass formula and the Recognition Composition Law. No RS-native units or J-cost appear inside the module itself.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the WZBosonRatioScoreCard, which establishes the algebraic bounds $m_W/m_Z \in (0.87,0.89)$ and $\sin^2 heta_W \in (0.22,0.23)$ from the supplied PDG values as part of Phase 2 P2-WZ. It supplies the concrete mass inputs required to test Recognition Science predictions against experimental electroweak data.

scope and limits

Does not derive the masses from the J-function or phi-ladder.
Does not contain theorems or proofs.
Does not express masses in RS-native units.
Does not address the alpha band or forcing chain steps T5-T8.

used by (1)

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

IndisputableMonolith.Physics.WZBosonRatioScoreCard module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (24)

def m_W L47
def m_Z L50
def massRatio L53
theorem mass_ratio_value L56
def weinbergAngle L61
def sin2ThetaW L64
theorem sin2_theta_w_value L67
def hypothesis1 L78
def hypothesis2 L85
def hypothesis3 L92
def hypothesis4 L99
def hypothesis5 L106
def hypothesis6 L114
def bestPhiPrediction L123
theorem mass_ratio_from_couplings L137
def couplingRatio L145
theorem tan_theta_w_value L151
def sin2ThetaW_predicted L167
theorem sin2_prediction_vs_observed L169
def sin2ThetaW_alt L180
def implications L190
def predictions L203
structure WZFalsifier L215
def experimentalStatus L219