module module

`IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts`

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.Foundation.UniversalForcing.AdmissibleClass module_import

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.UniversalForcing.Strict.Biology module_import
IndisputableMonolith.Foundation.UniversalForcing.Strict.Ethics module_import
IndisputableMonolith.Foundation.UniversalForcing.Strict.Metaphysical module_import
IndisputableMonolith.Foundation.UniversalForcing.Strict.Music module_import
IndisputableMonolith.Foundation.UniversalForcing.Strict.Narrative module_import

declarations in this module (19)

theorem ratioCost_zero_iff L45
def ratioCost_decidable L52
theorem compose_assoc L55
theorem compose_left_id L62
theorem lineageCost_zero_iff L76
def lineageCost_decidable L83
theorem reproduce_assoc L86
theorem reproduce_left_id L92
theorem eventCost_zero_iff L107
def eventCost_decidable L114
theorem eventCompose_assoc L117
theorem eventCompose_left_id L124
theorem actionCost_zero_iff L137
def actionCost_decidable L144
theorem preferenceCompose_assoc L147
theorem preferenceCompose_left_id L154
def metaphysical_ground_invariant L170
structure RichDomainCostsCert L181
theorem richDomainCostsCert_holds L205