module module

`IndisputableMonolith.Cosmology.PolarizedBirthInterfaceCost`

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.GradedRungCost module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cosmology.LatticeBallEdges module_import
IndisputableMonolith.Cost module_import

declarations in this module (22)

def Jpow L49
lemma Jpow_zero L52
lemma Jpow_one L56
lemma Jpow_neg_one L60
lemma Jpow_of_abs_one L67
lemma Jcost_phi_pos L74
theorem level_diff L94
def edgeCost L103
theorem edgeCost_carried_zero L107
theorem edgeCost_interface L114
def interfaceCost L122
def carriedCost L125
def totalCost L128
theorem carriedCost_eq_zero L131
theorem interfaceCost_eq_card L138
theorem totalCost_eq_interfaceCost L144
theorem interfaceCost_card L164
theorem totalCost_card L170
theorem totalCost_mul L175
theorem runCost_growth L183
theorem costIncrement L200
theorem t55_cost_ledger L213