theorem
proved
tactic proof
dependency_cone
show as:
view Lean formalization →
formal statement (Lean)
108theorem dependency_cone (tape : Tape) (i : ℤ) (t : ℕ) :
109 ∃ (cone : Finset ℤ),
110 cone.card ≤ 2 * t + 1 ∧
111 ∀ i' ∈ cone, |i' - i| ≤ t := by
proof body
Tactic-mode proof.
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 -/