  48  simpa [step8] using iterate_defect_nonincreasing dyn 8 s
  49
  50/-- The 8-step dynamics itself is a one-step defect-nonincreasing system. -/
  51def windowDynamics {α : Type} (dyn : OneStepDynamics α) : OneStepDynamics α where
  52  step := step8 dyn
  53  defect := dyn.defect
  54  defect_nonincreasing := step8_defect_nonincreasing dyn
  55
  56/-- Repeated 8-tick windows remain defect-nonincreasing. -/
  57theorem window_certificate_extends {α : Type} (dyn : OneStepDynamics α) :
  58    ∀ n s, dyn.defect (((step8 dyn)^[n]) s) ≤ dyn.defect s := by
  59  simpa [windowDynamics] using iterate_defect_nonincreasing (windowDynamics dyn)
  60
  61/-- The pattern-level 8-tick cycle exists in D=3. -/
  62theorem eight_tick_cycle_exists : ∃ w : CompleteCover 3, w.period = 8 :=
  63  period_exactly_8
  64
  65/-- Any full cover of 3-bit patterns needs at least 8 ticks. -/
  66theorem eight_tick_minimal {T : Nat}
  67    (pass : Fin T → Pattern 3) (covers : Function.Surjective pass) :
  68    8 ≤ T :=
  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 :=

papers checked against this theorem

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