IndisputableMonolith.Cosmology.WMassAnomalyStructure
Packages Recognition Science's structural account of the W-boson mass anomaly: RS and SM predictions, CDF/ATLAS measurements, and the link from m_W to the electroweak scale and the phi-ladder. Particle phenomenologists and cosmologists citing RS mass claims would use it. The module is definitional and relational: it wires ledger-side EW structure to mass ratios and anomaly predicates rather than proving a new numerical identity from scratch.
claimThe module fixes the Recognition Science structure of the $W$ mass anomaly: an electroweak-scale hypothesis, RS and SM predictions $m_W^{\mathrm{RS}}$ and $m_W^{\mathrm{SM}}$, CDF/ATLAS measured values, the ratio $m_W/m_Z$, the $\varphi$-ladder rung of $m_W$, and predicates that the anomaly is explained once the EW scale is fixed by the ledger.
background
Recognition Science places particle masses on a $\varphi$-ladder (yardstick times $\varphi$ to a rung offset by gap terms). The $W$ boson is not free-floating: any RS $m_W$ claim presupposes a fixed electroweak scale. The imported E-004 module formalizes that scale structure; the Constants import supplies the RS-native tick $\tau_0$.
Experimentally, the CDF $m_W$ measurement sits high relative to the Standard Model electroweak fit, while ATLAS is closer to the SM band. This module names both measurements, the SM prediction, and an RS prediction side by side, together with the ratio $m_W/m_Z$ and a reconstruction of $m_W$ from $m_Z$.
Sibling definitions encode the logical spine: presence of EW-scale structure, implication from a $W$-mass anomaly to that structure, ladder position, and a predicate that the anomaly is explained once the ledger fixes the scale.
proof idea
This is a structure module, not a single deep proof. It imports electroweak-scale structure and RS constants, then introduces definitions and thin lemmas that (i) assert EW-scale structure as a prerequisite, (ii) place $m_W$ on the $\varphi$-ladder, (iii) record SM vs RS predictions and CDF/ATLAS values, (iv) relate $m_W$ to $m_Z$ by a mass ratio, and (v) package "anomaly explained from the ledger" as a named predicate. Downstream users compose these names; heavy algebra lives upstream in the EW-scale and constants layers.
why it matters in Recognition Science
Without a clean interface between the electroweak scale (registry E-004) and the $W$ mass, RS cannot claim a ledger-side resolution of the CDF/ATLAS tension. This module is that interface in the Cosmology domain: it makes explicit that EW-scale structure is prerequisite for any RS $m_W$ prediction, and it exposes the anomaly, ladder position, and $m_W/m_Z$ ratio as first-class objects.
No downstream Lean dependents are recorded yet (used_by is empty), so its role is infrastructural: future cosmology and precision-EW theorems cite these names rather than re-deriving the measurement bookkeeping. It sits downstream of the forcing-chain constants and mass-ladder machinery (phi, rung offsets) and upstream of any claim that RS explains the $W$ anomaly quantitatively.
scope and limits
- Does not numerically settle CDF vs ATLAS vs SM; it structures the comparison.
- Does not derive the electroweak scale; that lives in the imported E-004 module.
- Does not prove a full mass-formula identity for m_W from T0–T8 here.
- Does not claim experimental preference; measurements are named inputs.
- Does not feed recorded downstream theorems yet (no used_by edges).
depends on (2)
declarations in this module (15)
-
theorem
has_ew_scale_structure -
def
w_mass_anomaly_from_ledger -
theorem
w_mass_anomaly_structure -
theorem
w_mass_implies_ew_scale -
theorem
w_mass_phi_ladder_position -
theorem
w_mass_rs_prediction -
theorem
w_mass_sm_prediction -
theorem
w_mass_cdf_measurement -
theorem
w_mass_atlas_measurement -
theorem
w_z_mass_ratio -
theorem
w_mass_from_z -
theorem
w_mass_anomaly_explained -
theorem
w_mass_sigma_comparison -
structure
WMassAnomalyResolution -
theorem
w_mass_anomaly_resolved