theorem proved term proof

`ew_scale_implies_phi_ne_one`

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

formal statement (Lean)

  60theorem ew_scale_implies_phi_ne_one (h : scale_from_ledger) : phi ≠ 1 := by

Term-mode proof.

  61  linarith [h.1.1]
  62
  63/-- Electroweak-scale structure excludes the upper endpoint `phi = 2`. -/

Lean names referenced from this declaration's body.

scale in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS decl_use
scale_from_ledger in IndisputableMonolith.QFT.ElectroweakScaleStructure decl_use