experimentalStatus
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.