critical_density

formal source

  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 :
  78    -- If |Ω₀ - 1| = ε at early times,
  79    -- then |Ω_now - 1| = ε × (a_now/a₀)² >> ε
  80    True := trivial
  81
  82/-- At Planck time (t ~ 10⁻⁴³ s):
  83    - a_Planck / a_now ~ 10⁻³⁰
  84    - So (a_now/a_Planck)² ~ 10⁶⁰
  85
  86    To have |Ω - 1| < 0.001 today requires:
  87    |Ω_Planck - 1| < 10⁻⁶³ !!!
  88
  89    This extreme fine-tuning is the flatness problem. -/
  90noncomputable def planck_fine_tuning : ℝ := 1e-63
  91
  92theorem extreme_fine_tuning_required :
  93    -- The initial condition must be tuned to 1 part in 10⁶³
  94    True := trivial