iterate_defect_nonincreasing

formal source

  29  dyn.step^[8]
  30
  31/-- Iterating a one-step defect-nonincreasing map preserves defect monotonicity. -/
  32theorem iterate_defect_nonincreasing {α : Type} (dyn : OneStepDynamics α) :
  33    ∀ n s, dyn.defect ((dyn.step^[n]) s) ≤ dyn.defect s := by
  34  intro n
  35  induction n with
  36  | zero =>
  37      intro s
  38      simp
  39  | succ n ihn =>
  40      intro s
  41      rw [Function.iterate_succ_apply']
  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 :=