module module high

`IndisputableMonolith.Cosmology.WMassAnomalyStructure`

This module supplies the electroweak scale structure required as a prerequisite for any Recognition Science prediction of the W boson mass. It imports the E-004 ElectroweakScaleStructure framework and the RS time quantum from Constants to organize anomaly ledger relations. Particle cosmologists studying mass discrepancies would cite it when connecting the phi-ladder to electroweak scales. The module is purely definitional with no proofs.

claimThe module defines the electroweak scale structure prerequisite $EWS$ together with ledger-based anomaly relations for the W-boson mass $m_W$ in RS cosmology.

background

The module sits in the cosmology domain and imports the RS time quantum $ au_0 = 1$ tick from Constants together with the ElectroweakScaleStructure module. The latter formalizes the RS structural framework for the EWSB scale under registry item E-004. Local notation follows the phi-ladder and Recognition Composition Law already established in the upstream electroweak module.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the prerequisite structures for any RS $m_W$ prediction, as stated in its documentation. It feeds the sibling definitions that link the electroweak scale to W-mass anomaly explanations via the ledger. No downstream usages are recorded yet.

scope and limits

Does not derive numerical mass values.
Does not prove anomaly resolution.
Does not interface with experimental data.
Does not extend beyond electroweak prerequisites.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.QFT.ElectroweakScaleStructure module_import

declarations in this module (15)

theorem has_ew_scale_structure L83
def w_mass_anomaly_from_ledger L87
theorem w_mass_anomaly_structure L89
theorem w_mass_implies_ew_scale L92
theorem w_mass_phi_ladder_position L102
theorem w_mass_rs_prediction L120
theorem w_mass_sm_prediction L134
theorem w_mass_cdf_measurement L141
theorem w_mass_atlas_measurement L148
theorem w_z_mass_ratio L162
theorem w_mass_from_z L176
theorem w_mass_anomaly_explained L194
theorem w_mass_sigma_comparison L211
structure WMassAnomalyResolution L250
theorem w_mass_anomaly_resolved L262