  45
  46    At CMB time (t ~ 380,000 years), d_H ~ 1.2 million light years.
  47    But the CMB spans the whole sky, which is much larger! -/
  48structure ParticleHorizon where
  49  time : ℝ  -- Cosmic time
  50  radius : ℝ  -- Horizon radius
  51  time_pos : time > 0
  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?

papers checked against this theorem

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