dependency_cone

formal source

 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 -/
 132structure ClauseGadget (n : ℕ) where
 133  /-- Variable indices appearing in the clause -/
 134  variables : List (Fin n)
 135  /-- Negation flags for each variable -/
 136  negated : List Bool
 137  /-- Starting position on tape -/
 138  position : ℤ