  69  eight_tick_min pass covers
  70
  71/-- A finite-window certificate for the 8-step operator. -/
  72structure EightTickCertificate (α : Type) where
  73  dyn : OneStepDynamics α
  74  initial : α
  75  one_window_bound :
  76    dyn.defect (step8 dyn initial) ≤ dyn.defect initial
  77
  78/-- The one-window certificate propagates to every later 8-tick window. -/
  79theorem eight_tick_certificate_propagates {α : Type} (cert : EightTickCertificate α) :
  80    ∀ n, cert.dyn.defect (((step8 cert.dyn)^[n]) cert.initial) ≤
  81      cert.dyn.defect cert.initial :=
  82by
  83  intro n
  84  exact window_certificate_extends cert.dyn n cert.initial
  85
  86end
  87
  88end EightTickDynamics
  89end NavierStokes
  90end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.