module module

`IndisputableMonolith.Unification.RegistryPredictionsProved`

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

used by (1)

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

IndisputableMonolith.Cosmology.CosmologicalConstantDerivation module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.Alpha module_import
IndisputableMonolith.Constants.GapWeight module_import
IndisputableMonolith.Foundation.PhiForcing module_import

declarations in this module (9)

theorem omega_lambda_lt_11_16 L34
lemma alphaInv_gt_2 L54
theorem omega_lambda_positive L117
theorem omega_lambda_bounds L132
theorem phi_6_hierarchy_bounds L139
theorem phi_11_hierarchy_lower L150
theorem hierarchy_phi_power_structure L155
structure RegistryPredictionsCert L169
theorem registry_predictions_cert_exists L179