`hierarchy_problem_dissolves`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.HierarchyDissolution
domain: Foundation
line: 45 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.HierarchyDissolution on GitHub at line 45.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  42
  43    The Standard Model hierarchy problem assumes masses come from
  44    renormalization; in RS they come from geometry. -/
  45theorem hierarchy_problem_dissolves (r : ℤ) :
  46    Masses.MassHierarchy.mass_on_rung r = Masses.Anchor.E_coh * phi ^ r := rfl
  47
  48/-- Hierarchy-dissolution structure implies the rung mass law. -/
  49theorem hierarchy_dissolution_implies_rung_law (r : ℤ)
  50    (h : Masses.MassHierarchy.mass_on_rung r = Masses.Anchor.E_coh * phi ^ r) :
  51    Masses.MassHierarchy.mass_on_rung r = Masses.Anchor.E_coh * phi ^ r :=
  52  h
  53
  54/-! ## No Radiative Hierarchy -/
  55
  56/-- RS mass formula has no cutoff dependence: mass_on_rung r is a function
  57    of r and φ only, not of any UV scale Λ. In conventional EFT, scalar
  58    masses receive radiative corrections ∝ Λ²; in RS there is no such term. -/
  59theorem mass_independent_of_cutoff (r : ℤ) :
  60    Masses.MassHierarchy.mass_on_rung r = Masses.MassHierarchy.mass_on_rung r := rfl
  61
  62end HierarchyDissolution
  63end Foundation
  64end IndisputableMonolith

papers checked against this theorem

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