theorem proved term proof

`w_mass_implies_ew_scale`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  92theorem w_mass_implies_ew_scale (h : w_mass_anomaly_from_ledger) : scale_from_ledger :=

proof body

Term-mode proof.

  93  h
  94
  95/-! ## φ-Ladder W Mass Derivation -/
  96
  97/-- **T-005 φ-Ladder Position**: The W boson mass position on the
  98    RS mass hierarchy (φ-ladder).
  99    
 100    The W mass is related to other electroweak-scale masses through
 101    φ-scaling relationships. -/

depends on (14)

Lean names referenced from this declaration's body.

Mass in IndisputableMonolith.Constants.RSNativeUnits decl_use
scale in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS decl_use
w_mass_anomaly_from_ledger in IndisputableMonolith.Cosmology.WMassAnomalyStructure decl_use
T in IndisputableMonolith.Foundation.Breath1024 decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
T in IndisputableMonolith.Gap45.SyncMinimization decl_use
Position in IndisputableMonolith.Gravity.CoherenceFall decl_use
W in IndisputableMonolith.Masses.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
W in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
W in IndisputableMonolith.Physics.MassTopology decl_use
scale_from_ledger in IndisputableMonolith.QFT.ElectroweakScaleStructure decl_use