module module

`IndisputableMonolith.Cosmology.HorizonProblem`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (15)

structure ParticleHorizon L48
def cmb_horizon L55
def causal_patch_angle L68
def number_of_patches L70
theorem horizon_problem_stated L82
structure InflationParameters L99
def standardInflation L105
theorem rs_universal_clock L123
def synchronization_mechanism L134
def costOfInhomogeneity L149
theorem homogeneous_minimizes_cost L153
def complementary_explanation L176
def predictions L191
def observationalEvidence L207
structure HorizonFalsifier L220