structure definition def or abbrev

`ParticleHorizon`

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

formal statement (Lean)

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

cmb_horizon in IndisputableMonolith.Cosmology.HorizonProblem decl_use

depends on (2)

Lean names referenced from this declaration's body.

radius in IndisputableMonolith.Complexity.CellularAutomata decl_use
was in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use