WMassAnomalyResolution
plain-language theorem explainer
The structure packages an RS-predicted W-boson mass interval 80400 to 80450 MeV, the SM Higgs-fit value 80357 MeV, the CDF datum 80433.5 MeV, the ATLAS datum 80367 MeV, and the assertion that the discrepancy is thereby resolved. Particle physicists testing electroweak-scale predictions against collider data would cite the record when comparing the phi-ladder value to recent measurements. It is introduced as a bare structure definition whose fields are five independent propositions.
Claim. A W-mass anomaly resolution is a record containing an RS-predicted mass $m$ satisfying $80400 < m < 80450$, the SM prediction $m = 80357$, the CDF measurement $m = 80433.5$, the ATLAS measurement $m = 80367$, and the proposition that the anomaly is explained.
background
In Recognition Science the electroweak scale is fixed by the phi-ladder rather than a free Higgs vacuum expectation value. The W mass is obtained from the same self-similar structure that sets all particle masses via the yardstick times phi to a power determined by rung and gap(Z). Module T-005 formalizes the claim that the CDF II measurement lies close to the RS value while the SM fit sits lower, interpreting the tension as a measurement offset.
proof idea
The declaration is a structure definition whose fields are five independent propositions; no lemmas are applied and the body is empty.
why it matters
This structure supplies the concrete data bundle required by the theorem w_mass_anomaly_resolved that constructs an explicit instance with RS value 80420 MeV. It fills the T-005 registry item that resolves the CDF W-mass anomaly as an artifact of the phi-ladder electroweak scale. Within the forcing chain the result follows the derivation of the eight-tick octave and D = 3, using the Recognition Composition Law to fix the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.