module module

`IndisputableMonolith.Cosmology.GradedRungCost`

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

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

IndisputableMonolith.Cosmology.RecognitionUnitStepPreservation module_import
IndisputableMonolith.Cosmology.RungDescentUnitStep module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cosmology.PolarizedBirthInterfaceCost module_import

declarations in this module (15)

def edgeCost L55
def UnitStep L61
theorem edgeCost_carried L65
theorem edgeCost_interface L72
def interfaceCost L86
def carriedCost L90
def totalCost L94
theorem carriedCost_eq_zero L98
theorem totalCost_eq_interfaceCost L107
theorem interfaceCost_eq_card L121
theorem totalCost_eq_card L133
theorem t56_graded_cost_ledger L142
theorem polarized_unitStep L161
theorem polarized_totalCost L172
theorem polarized_totalCost_card L178