`ew_scale_implies_phi_ne_one`

proved

show as: view math explainer →

module: IndisputableMonolith.QFT.ElectroweakScaleStructure
domain: QFT
line: 60 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.ElectroweakScaleStructure on GitHub at line 60.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  57  h.2 r
  58
  59/-- Electroweak-scale structure excludes the degenerate endpoint `phi = 1`. -/
  60theorem ew_scale_implies_phi_ne_one (h : scale_from_ledger) : phi ≠ 1 := by
  61  linarith [h.1.1]
  62
  63/-- Electroweak-scale structure excludes the upper endpoint `phi = 2`. -/
  64theorem ew_scale_implies_phi_ne_two (h : scale_from_ledger) : phi ≠ 2 := by
  65  linarith [h.1.2]
  66
  67/-! ## φ Connection -/
  68
  69/-- φ > 1 forces geometric growth. Mass ratios are powers of φ. -/
  70theorem phi_gt_one : 1 < phi := one_lt_phi
  71
  72end ElectroweakScaleStructure
  73end QFT
  74end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.