w_mass_cdf_measurement
plain-language theorem explainer
The declaration records the CDF II 2022 measurement of the W boson mass as the real number 80433.5. Particle physicists and cosmologists working in the Recognition Science framework cite it when contrasting the reported electroweak anomaly against the phi-ladder scale. The proof is a one-line term that directly supplies the witness and closes the equality by reflexivity.
Claim. There exists a real number $m_W^{CDF}$ such that $m_W^{CDF} = 80433.5$, recording the CDF II measurement of the W boson mass in MeV.
background
The declaration belongs to the module that formalizes the RS structural account of the W-mass anomaly (T-005). The module sets the CDF II value against the SM baseline and the later ATLAS measurement, then resolves the discrepancy by identifying the CDF datum with the phi-ladder electroweak scale rather than the Higgs-fit value. Upstream results supply the generic Measurement structure (hardcoded experimental values) and the SM m_W definition (80.377 GeV) used for comparison.
proof idea
The proof is a one-line term that applies existential introduction to the literal real 80433.5 and discharges the equality subgoal by reflexivity.
why it matters
It supplies the experimental input datum for T-005, anchoring the claim that the CDF discrepancy measures the true RS electroweak scale on the phi-ladder. The value feeds module-level comparisons that treat the anomaly as a structural feature rather than evidence of physics beyond the Standard Model. No open scaffolding remains at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.