structure
definition
HorizonFalsifier
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.HorizonProblem on GitHub at line 220.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
217 1. CMB anomalies have mundane explanations
218 2. No φ-structure in inflationary parameters
219 3. Horizon problem solution requires only local physics -/
220structure HorizonFalsifier where
221 anomalies_mundane : Prop
222 no_phi_in_inflation : Prop
223 purely_local_solution : Prop
224 falsified : anomalies_mundane ∧ no_phi_in_inflation ∧ purely_local_solution → False
225
226end HorizonProblem
227end Cosmology
228end IndisputableMonolith