theorem proved term proof

`ew_scale_implies_phi_window`

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

formal statement (Lean)

  51theorem ew_scale_implies_phi_window (h : scale_from_ledger) : 1 < phi ∧ phi < 2 :=

Term-mode proof.

  52  h.1
  53
  54/-- Electroweak-scale structure implies rung-wise no-fine-tuning identity. -/

Lean names referenced from this declaration's body.

rung in IndisputableMonolith.Compat.Constants decl_use
scale in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS decl_use
rung in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
rung in IndisputableMonolith.Masses.AnchorPolicy decl_use
rung in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
scale_from_ledger in IndisputableMonolith.QFT.ElectroweakScaleStructure decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use
rung in IndisputableMonolith.RSBridge.Anchor decl_use