def
definition
experimentalStatus
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.StandardModel.WZMassRatio on GitHub at line 219.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
216 falsifier : String
217 status : String
218
219def experimentalStatus : List WZFalsifier := [
220 ⟨"m_W / m_Z measurement", "0.8815 ± 0.0002, precisely known"⟩,
221 ⟨"sin²(θ_W) measurement", "0.2229 ± 0.0003"⟩,
222 ⟨"φ-connection", "In progress - promising"⟩
223]
224
225end WZMassRatio
226end StandardModel
227end IndisputableMonolith