theorem proved term proof

`ew_scale_implies_no_fine_tuning`

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

formal statement (Lean)

  55theorem ew_scale_implies_no_fine_tuning (h : scale_from_ledger) (r : ℤ) :
  56    Masses.MassHierarchy.mass_on_rung r = Masses.MassHierarchy.mass_on_rung r :=

proof body

Term-mode proof.

  57  h.2 r
  58
  59/-- Electroweak-scale structure excludes the degenerate endpoint `phi = 1`. -/

depends on (3)

Lean names referenced from this declaration's body.

scale in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS decl_use
mass_on_rung in IndisputableMonolith.Masses.MassHierarchy decl_use
scale_from_ledger in IndisputableMonolith.QFT.ElectroweakScaleStructure decl_use