module module

`IndisputableMonolith.NavierStokes.EightTickDynamics`

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

declarations in this module (10)

structure OneStepDynamics L22
def step8 L28
theorem iterate_defect_nonincreasing L32
theorem step8_defect_nonincreasing L45
def windowDynamics L51
theorem window_certificate_extends L57
theorem eight_tick_cycle_exists L62
theorem eight_tick_minimal L66
structure EightTickCertificate L72
theorem eight_tick_certificate_propagates L79