`step`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.CellularAutomata
domain: Complexity
line: 95 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Complexity.CellularAutomata on GitHub at line 95.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  92  | _, c, _ => c
  93
  94/-- Apply local rule globally to create successor tape -/
  95noncomputable def step (tape : Tape) : Tape :=
  96  fun i => localRule (extractNeighborhood tape i)
  97
  98/-! ## Locality Proof -/
  99
 100/-- The CA is local: each cell depends only on its radius-1 neighborhood -/
 101theorem ca_is_local (tape : Tape) (i : ℤ) :
 102    (step tape) i = localRule (extractNeighborhood tape i) := rfl
 103
 104/-- The CA is k-local for k = 1 -/
 105theorem ca_k_local : radius = 1 := rfl
 106
 107/-- Dependency cone: after t steps, position i depends only on [i-t, i+t] -/
 108theorem dependency_cone (tape : Tape) (i : ℤ) (t : ℕ) :
 109    ∃ (cone : Finset ℤ),
 110      cone.card ≤ 2 * t + 1 ∧
 111      ∀ i' ∈ cone, |i' - i| ≤ t := by
 112  -- The cone is {i - t, ..., i + t}
 113  use (Finset.Icc (i - t) (i + t)).image id
 114  constructor
 115  · -- Card bound
 116    simp only [Finset.image_id]
 117    calc (Finset.Icc (i - t) (i + t)).card
 118        = (i + t) - (i - t) + 1 := by
 119          rw [Int.card_Icc]
 120          ring_nf
 121      _ = 2 * t + 1 := by ring
 122  · -- Distance bound
 123    intro i' hi'
 124    simp only [Finset.mem_image, Finset.mem_Icc, id_eq] at hi'
 125    obtain ⟨j, ⟨hj_lo, hj_hi⟩, rfl⟩ := hi'

papers checked against this theorem

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