module module

`IndisputableMonolith.Foundation.LawOfExistence`

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

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

IndisputableMonolith.Cosmology.EarlyUniverse module_import
IndisputableMonolith.Foundation.ConstantDerivations module_import
IndisputableMonolith.Foundation.Determinism module_import
IndisputableMonolith.Foundation.DimensionalConstraints.CostLayer module_import
IndisputableMonolith.Foundation.DiscretenessForcing module_import
IndisputableMonolith.Foundation.GodelDissolution module_import
IndisputableMonolith.Foundation.InevitabilityEquivalence module_import
IndisputableMonolith.Foundation.InevitabilityStructure module_import
IndisputableMonolith.Foundation.InitialCondition module_import
IndisputableMonolith.Foundation.LedgerForcing module_import
IndisputableMonolith.Foundation.LogicFromCost module_import
IndisputableMonolith.Foundation.OntologyPredicates module_import
IndisputableMonolith.Foundation.PhiForcing module_import
IndisputableMonolith.Foundation.RecognitionForcing module_import
IndisputableMonolith.Foundation.StillnessGenerative module_import
IndisputableMonolith.Foundation.TimeEmergence module_import
IndisputableMonolith.Foundation.VariationalDynamics module_import
IndisputableMonolith.Gravity.ZeroParameterGravity module_import
IndisputableMonolith.Modal.Possibility module_import
IndisputableMonolith.NumberTheory.ZeroLocationCost module_import
IndisputableMonolith.Philosophy.ModalOntologyStructure module_import
IndisputableMonolith.Philosophy.ObjectiveMoralityStructure module_import
IndisputableMonolith.Thermodynamics.JCostThermoBridge module_import
IndisputableMonolith.Unification.UnifiedRH module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import

declarations in this module (21)

def J L29
def defect L32
theorem defect_at_one L35
theorem defect_nonneg L38
structure Exists L48
def DefectCollapse L53
theorem defect_zero_iff_one L58
theorem exists_implies_defect_zero L72
theorem defect_zero_implies_exists L76
theorem law_of_existence L80
theorem exists_iff_unity L84
theorem unity_unique_existent L89
theorem defect_one L96
theorem defect_pos_of_ne_one L99
theorem defect_tendsto_atTop_at_zero L109
theorem nothing_cannot_exist L130
def StructuredSet L155
theorem structured_set_singleton L157
theorem mem_structured_iff_exists L165
theorem existence_economically_inevitable L171
theorem complete_law_of_existence L190