module module

`IndisputableMonolith.Cosmology.VacuumHorizonForcing`

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.Cosmology.PhiRungLadder module_import

declarations in this module (20)

structure CausalContactRelation L70
def causalNeighborhood L82
theorem mem_causalNeighborhood_self L87
inductive HorizonType L95
structure HorizonModel L101
def particleHorizonModel L115
def hubbleRadiusModel L124
def deSitterModel L133
def vacuumEnergyExponent L145
theorem causal_accumulation_selects_particle_horizon L155
theorem hubbleRadius_excludes_past_contacts L174
theorem deSitter_requires_future L186
def particleHorizonRungCount L198
theorem vacuumExponent_particleHorizon L201
theorem hubble_vs_particle_rung_gap L207
theorem phi_power_ten_large L216
structure VacuumHorizonForcingCert L221
def vacuumHorizonForcingCert L229
theorem vacuumHorizonForcingCert_inhabited L237
theorem vacuum_horizon_forcing_one_statement L245