ca_is_local

formal source

  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'
 126    rw [abs_sub_le_iff]
 127    constructor <;> linarith
 128
 129/-! ## SAT Gadgets -/
 130
 131/-- A SAT clause encoded as CA cells -/