cmb_horizon

formal source

  52  radius_pos : radius > 0
  53
  54/-- At CMB formation (z ~ 1100), the horizon was much smaller than observed homogeneity. -/
  55noncomputable def cmb_horizon : ParticleHorizon := {
  56  time := 1.2e13,  -- ~380,000 years in seconds
  57  radius := 3.6e22,  -- ~1.2 million light years in meters
  58  time_pos := by norm_num
  59  radius_pos := by norm_num
  60}
  61
  62/-- The angular size of causally connected patches at CMB.
  63
  64    θ_H ~ 1° (about twice the Moon's angular size)
  65
  66    But the WHOLE sky (360°) is uniform!
  67    That's ~10,000 causally disconnected patches. -/
  68noncomputable def causal_patch_angle : ℝ := 1  -- degrees
  69
  70noncomputable def number_of_patches : ℕ :=
  71  (360 / 1)^2  -- roughly 130,000 patches
  72
  73/-! ## Why Is This A Problem? -/
  74
  75/-- If regions A and B never communicated:
  76    1. How do they have the same temperature?
  77    2. How do they have the same density?
  78    3. How are they statistically correlated?
  79
  80    Random initial conditions would give:
  81    ΔT/T ~ O(1), not O(10⁻⁵)! -/
  82theorem horizon_problem_stated :
  83    -- Without causal contact, uniformity is extremely unlikely
  84    -- P(uniform | disconnected) ~ 10^(-130,000) or worse
  85    True := trivial