pith. machine review for the scientific record. sign in
theorem proved tactic proof

eight_tick_certificate_propagates

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

formal statement (Lean)

  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 :=

proof body

Tactic-mode proof.

  82by
  83  intro n
  84  exact window_certificate_extends cert.dyn n cert.initial
  85
  86end
  87
  88end EightTickDynamics
  89end NavierStokes
  90end IndisputableMonolith

depends on (4)

Lean names referenced from this declaration's body.