w_mass_sm_prediction
plain-language theorem explainer
The theorem encodes the Standard Model electroweak fit value for the W boson mass as exactly 80357 MeV. Researchers comparing the CDF II measurement to the LEP/SLD/Tevatron global fit would cite this constant when quantifying the reported discrepancy. The proof proceeds by a direct term-mode construction that witnesses the existential quantifier with the literal value and reflexivity.
Claim. There exists a real number $m_W^{SM}$ such that $m_W^{SM} = 80357$ MeV.
background
In the module addressing the CDF W-mass anomaly (T-005), the Standard Model prediction serves as the baseline for the reported discrepancy with the CDF II measurement of 80433.5 MeV. The upstream Measurement structure from IndisputableMonolith.Data.Import defines a record with name, value, and error fields for hardcoded experimental inputs. Related definitions include the W boson mass in the StandardModel module as 80.377 GeV, which aligns closely with the 80357 MeV value used here after unit conversion.
proof idea
The proof is a one-line term-mode construction. It applies the existential introduction constructor to the pair consisting of the real number 80357 and the reflexivity tactic that discharges the equality.
why it matters
This declaration supplies the SM baseline value required for the T-005 analysis of the CDF anomaly within the Recognition Science framework. It feeds the comparison that leads to the RS explanation via the phi-ladder electroweak scale, as outlined in the module documentation. The value 80357 MeV is the global fit result from LEP/SLD/Tevatron data, distinct from the RS-native prediction derived from phi^5 scaling and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.