  44    - Ω = 1: Flat (Euclidean) geometry
  45    - Ω > 1: Positive curvature (closed, spherical)
  46    - Ω < 1: Negative curvature (open, hyperbolic) -/
  47structure DensityParameter where
  48  value : ℝ
  49  uncertainty : ℝ
  50  value_pos : value > 0
  51
  52/-- Current observation: Ω = 1.0000 ± 0.0002 -/
  53noncomputable def omega_observed : DensityParameter := {
  54  value := 1.0,
  55  uncertainty := 0.0002,
  56  value_pos := by norm_num
  57}
  58
  59/-- The critical density at the current epoch.
  60
  61    ρ_c = 3H₀²/(8πG) ≈ 9.5 × 10⁻²⁷ kg/m³
  62
  63    This is incredibly dilute: about 5 hydrogen atoms per cubic meter! -/
  64noncomputable def critical_density : ℝ :=
  65  -- H₀ ~ 70 km/s/Mpc ~ 2.3e-18 s⁻¹
  66  3 * (2.3e-18)^2 / (8 * Real.pi * G)
  67
  68/-! ## Why Is Flatness A Problem? -/
  69
  70/-- The equation for Ω evolution:
  71
  72    |Ω - 1| ∝ a²(t) in radiation domination
  73    |Ω - 1| ∝ a(t) in matter domination
  74
  75    So deviations from 1 GROW with time!
  76    Ω = 1 is an unstable equilibrium (like balancing a pencil). -/
  77theorem omega_deviation_grows :

papers checked against this theorem

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