def
definition
rho_lambda_observed
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cosmology.CosmologicalConstant on GitHub at line 46.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
74/-- Hypothesis 2: Λ ∝ (τ₀ / t_universe)²
75
76 t_universe ~ 4.4 × 10¹⁷ s