pith. machine review for the scientific record. sign in
def definition def or abbrev

cmb_horizon

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  55noncomputable def cmb_horizon : ParticleHorizon := {

proof body

Definition body.

  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. -/

depends on (12)

Lean names referenced from this declaration's body.