module module

`IndisputableMonolith.Cosmology.RecognitionUnitStepPreservation`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Cosmology.GradedRungCost module_import
IndisputableMonolith.Cosmology.RecognitionEquilibrium module_import

declarations in this module (15)

def UnitStepReal L44
def EdgeTouches L49
theorem pairResolve_unitStep_of_local L59
def f0 L80
def f1 L81
def f2 L82
def chain3Edges L85
def chain3Levels L88
lemma chain3Levels_f0 L93
lemma chain3Levels_f1 L94
lemma chain3Levels_f2 L95
theorem chain3_unitStep L98
lemma chain3_resolved_second_gap L107
theorem chain3_pairResolve_breaks_unitStep L120
theorem t58_unitStep_preservation_honest L132