module module

`IndisputableMonolith.CrossDomain.WorkingMemoryFromCube`

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

def canonicalSpan L25
theorem canonicalSpan_eq L26
def spanAt L29
theorem span_at_3 L31
theorem span_at_2 L32
theorem span_at_1 L33
theorem span_at_0 L34
theorem span_at_4 L35
theorem span_strict_mono L38
theorem super_normal_jump L47
theorem miller_bracket L50
structure WorkingMemoryFromCubeCert L53
def workingMemoryFromCubeCert L61