pith. machine review for the scientific record. sign in
def

lambda_observed

definition
show as:
view math explainer →
module
IndisputableMonolith.Cosmology.CosmologicalConstant
domain
Cosmology
line
43 · github
papers citing
none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cosmology.CosmologicalConstant on GitHub at line 43.

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

  40/-! ## Observed Value -/
  41
  42/-- The observed cosmological constant Λ ≈ 1.1 × 10⁻⁵² m⁻². -/
  43noncomputable def lambda_observed : ℝ := 1.1e-52
  44
  45/-- The corresponding dark energy density ρ_Λ ≈ 6 × 10⁻²⁷ kg/m³. -/
  46noncomputable def rho_lambda_observed : ℝ := 6e-27
  47
  48/-- The dark energy scale in eV: (ρ_Λ c² / ℏ³ c³)^(1/4) ≈ 2 meV. -/
  49noncomputable def dark_energy_scale_eV : ℝ := 2e-3  -- eV
  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! -/
  61theorem cosmological_constant_problem :
  62    -- ρ_predicted / ρ_observed ~ 10¹²³
  63    -- This is the most extreme fine-tuning in physics
  64    True := trivial
  65
  66/-! ## Possible φ-Connections -/
  67
  68/-- Hypothesis 1: Λ ∝ τ₀⁻²
  69
  70    If Λ ~ 1/τ₀², then Λ ~ 6 × 10⁵³ m⁻² (way too large).
  71    Need additional suppression. -/
  72noncomputable def hypothesis1 : ℝ := 1 / tau0^2
  73