pith. machine review for the scientific record. sign in
def definition def or abbrev high

experimentalStatus

show as:
view Lean formalization →

experimentalStatus assembles the current experimental anchors for the φ-derived W/Z mass ratio in Recognition Science. A physicist checking electroweak consistency with golden-ratio gauge structure would cite this list when comparing measured values to the predicted cos(θ_W). The body is a direct list literal that enumerates three status pairs without further computation.

claimThe experimental status is the list of WZFalsifier records: ⟨m_W/m_Z measurement, 0.8815 ± 0.0002, precisely known⟩, ⟨sin²(θ_W) measurement, 0.2229 ± 0.0003⟩, ⟨φ-connection, In progress - promising⟩.

background

In the StandardModel.WZMassRatio module the W and Z masses are introduced as the constants m_W = 80.377 GeV and m_Z = 91.1876 GeV. The WZFalsifier structure is defined with two fields: a string describing the potential falsifier and a string recording its current status. The module documentation frames the entire file as SM-003, whose goal is to obtain the observed ratio m_W/m_Z ≈ 0.881 from φ-quantized SU(2)×U(1) mixing, where the ratio equals cos(θ_W) by definition.

proof idea

This is a direct definition that constructs the list by enumerating three WZFalsifier instances; no lemmas or tactics are applied.

why it matters in Recognition Science

The definition supplies the experimental interface required by the SM-003 derivation of the W/Z mass ratio from φ-structure. It records the measured ratio, the Weinberg angle, and the status of the φ-connection, thereby closing the loop between the Recognition Science mass ladder and electroweak data. No downstream theorems yet consume it, leaving open its later use in full φ-ladder predictions for the gauge sector.

scope and limits

formal statement (Lean)

 219def experimentalStatus : List WZFalsifier := [

proof body

Definition body.

 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

depends on (3)

Lean names referenced from this declaration's body.