module module high

`IndisputableMonolith.StandardModel.WZMassRatio`

The module declares W and Z boson masses in GeV, their ratio, the Weinberg angle, and five supporting hypotheses inside the Recognition Science Standard Model layer. Researchers checking electroweak consistency with PDG data would cite these values when scoring mass-ratio predictions. The module consists entirely of definitions and hypothesis interfaces with no theorems or proofs.

claim$m_W = 80.377$ GeV, $m_Z = 91.1876$ GeV, mass ratio $m_W/m_Z$, Weinberg angle satisfying $1 - (m_W/m_Z)^2 = 0.231$, together with five hypotheses on the ratio bounds.

background

The module imports the RS time quantum τ₀ = 1 tick from Constants and places the declarations in the StandardModel domain. It introduces m_W and m_Z as explicit mass values, massRatio as their quotient, weinbergAngle and sin2ThetaW as the derived mixing parameter, and five hypothesis statements that encode the numerical interval claims. These objects supply the concrete inputs required by downstream score-card calculations.

proof idea

This is a definition module containing no proofs. It simply states the mass constants, computes the ratio and angle algebraically, and registers the five hypotheses as Prop placeholders.

why it matters in Recognition Science

The module supplies the exact PDG-derived inputs required by WZBosonRatioScoreCard to prove the interval bounds m_W/m_Z ∈ (0.87,0.89) and sin²θ_W ∈ (0.22,0.23). It thereby closes the numeric side of Phase 2 P2-WZ in the Recognition Science chain that links the forcing sequence T0-T8 to electroweak observables.

scope and limits

Does not derive the boson masses from the J-cost or phi-ladder.
Does not prove any of the five hypotheses.
Does not address radiative corrections or running couplings.
Does not relate the ratio to other Standard Model parameters.

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