No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
89theorem w_mass_anomaly_structure : w_mass_anomaly_from_ledger := has_ew_scale_structure
proof body
Term-mode proof.
90
91/-- W-mass anomaly structure implies electroweak-scale-side input. -/
depends on (6)
Lean names referenced from this declaration's body.
-
scale
in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS
decl_use
-
has_ew_scale_structure
in IndisputableMonolith.Cosmology.WMassAnomalyStructure
decl_use
-
w_mass_anomaly_from_ledger
in IndisputableMonolith.Cosmology.WMassAnomalyStructure
decl_use
-
W
in IndisputableMonolith.Masses.Anchor
decl_use
-
W
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
W
in IndisputableMonolith.Physics.MassTopology
decl_use