  42      exact le_trans (dyn.defect_nonincreasing ((dyn.step^[n]) s)) (ihn s)
  43
  44/-- A single 8-tick window is defect-nonincreasing. -/
  45theorem step8_defect_nonincreasing {α : Type} (dyn : OneStepDynamics α) :
  46    ∀ s, dyn.defect (step8 dyn s) ≤ dyn.defect s := by
  47  intro s
  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 :

papers checked against this theorem

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