module module

`IndisputableMonolith.Cosmology.RungDescentUnitStep`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cosmology.GradedRungCost module_import

declarations in this module (18)

def shiftDown L57
def shiftUp L61
lemma shiftDown_pos L64
lemma shiftDown_neg L67
lemma shiftUp_pos L70
lemma shiftUp_neg L73
theorem shiftDown_unitStep_of_cut L83
theorem shiftDown_top_unitStep L110
def edgeVerts L132
lemma fst_mem_edgeVerts L135
lemma snd_mem_edgeVerts L139
theorem exists_top_descent_unitStep L147
theorem shiftUp_bot_unitStep L171
def ckLevels L196
def ckEdges L199
theorem ckLevels_unitStep L203
theorem ckLevels_descend_min_breaks L210
theorem t59_rung_descent_preservation L222