pith. machine review for the scientific record. sign in
def definition def or abbrev

dark_energy_scale_eV

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  49noncomputable def dark_energy_scale_eV : ℝ := 2e-3  -- eV

proof body

Definition body.

  50
  51/-! ## The Problem -/
  52
  53/-- Naive QFT prediction: ρ_vac ~ m_P⁴ / (ℏ³ c³) ~ 10⁹⁶ kg/m³.
  54
  55    This is 10¹²³ times larger than observed!
  56
  57    Even with supersymmetry cutoff at 1 TeV:
  58    ρ_SUSY ~ (1 TeV)⁴ ~ 10⁴⁸ kg/m³
  59
  60    Still 10⁷⁵ times too large! -/

depends on (4)

Lean names referenced from this declaration's body.