pith. machine review for the scientific record. sign in
theorem proved term proof

w_mass_atlas_measurement

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 148theorem w_mass_atlas_measurement :
 149    ∃ (m_W_ATLAS : ℝ), m_W_ATLAS = 80367 :=

proof body

Term-mode proof.

 150  ⟨(80367 : ℝ), rfl⟩
 151
 152/-! ## W-Z Mass Ratio from φ -/
 153
 154/-- **T-005 W-Z Ratio**: The ratio m_W/m_Z has φ-structure.
 155
 156    m_W/m_Z = cos(θ_W) where θ_W is the weak mixing angle.
 157    
 158    In RS, the weak mixing angle has φ-corrections:
 159    sin²(θ_W) ≈ 0.231 + δφ where δφ ≈ 0.001 comes from 8-tick cycle.
 160    
 161    This gives: m_W/m_Z ≈ 0.881 (vs SM 0.8815) -/

depends on (18)

Lean names referenced from this declaration's body.