module module

`IndisputableMonolith.Cosmology.FlatnessProblem`

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 (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.PhiForcing module_import

declarations in this module (17)

structure DensityParameter L47
def omega_observed L53
def critical_density L64
theorem omega_deviation_grows L77
def planck_fine_tuning L90
theorem extreme_fine_tuning_required L92
theorem inflation_flattens L105
theorem rs_flatness_necessity L120
def curvatureCost L131
theorem flat_minimizes_cost L135
theorem critical_density_from_phi L155
def phi_cosmology_relations L167
def vs_multiverse L183
def observational_tests L199
def inflation_rs_synthesis L215
def implications L230
structure FlatnessFalsifier L243