module module

`IndisputableMonolith.Cosmology.RecognitionWorkBound`

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

declarations in this module (7)

def tickWork L45
def tickActivations L52
theorem tickWork_le L55
theorem tickActivations_le_two L66
theorem cycle_work_le L74
theorem cycle_activations_le L86
theorem recognition_work_localizes L96