diff --git a/0-Core-Formalism/lean/Semantics/Semantics/CopyIfTactic.lean b/0-Core-Formalism/lean/Semantics/Semantics/CopyIfTactic.lean
new file mode 100644
index 00000000..ececc47b
--- /dev/null
+++ b/0-Core-Formalism/lean/Semantics/Semantics/CopyIfTactic.lean
@@ -0,0 +1,60 @@
+/-
+CopyIfTactic.lean — Pre-filter tactic for Lean 4
+
+Implements the copy-if pattern as a native Lean tactic:
+1. Check if goal is trivially closable (zero delta) → close immediately
+2. If non-trivial (non-zero delta) → delegate to solver
+
+Usage:
+  theorem foo : 1 = 1 := by copy_if
+  theorem bar : x + 0 = x := by copy_if
+  theorem baz : complex_statement := by copy_if
+
+The tactic tries fast closers in order of cost:
+  1. rfl (instant — zero delta)
+  2. decide (fast — decidable)
+  3. omega (fast — linear arithmetic)
+  4. simp (slow — full simplification)
+-/
+import Mathlib.Tactic
+
+namespace Semantics.CopyIfTactic
+
+open Lean Elab Tactic
+
+/-- The copy_if tactic: try fast closers in order, fail if none work.
+    Lean implementation of the vectorized copy_if pattern.
+    Each closer is a "zero delta" check — if the goal is already in
+    normal form for that tactic, it closes instantly. -/
+macro "copy_if" : tactic => `(tactic|
+  first
+  | rfl
+  | decide
+  | omega
+  | norm_num
+  | simp
+  | fail "copy_if: non-trivial goal, needs solver"
+)
+
+/-- The copy_if? tactic: like copy_if but reports which closer worked. -/
+elab "copy_if?" : tactic => do
+  let tactics : List (String × Syntax) := [
+    ("rfl",     ← `(tactic| rfl)),
+    ("decide",  ← `(tactic| decide)),
+    ("omega",   ← `(tactic| omega)),
+    ("norm_num",← `(tactic| norm_num)),
+    ("simp",    ← `(tactic| simp)),
+  ]
+
+  for (name, tac) in tactics do
+    try
+      evalTactic tac
+      logInfo s!"copy_if?: closed with {name}"
+      return
+    catch _ =>
+      continue
+
+  logWarning "copy_if?: non-trivial goal"
+  throwError "copy_if?: goal is non-trivial"
+
+end Semantics.CopyIfTactic
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/TestCopyIf.lean b/0-Core-Formalism/lean/Semantics/Semantics/TestCopyIf.lean
new file mode 100644
index 00000000..5e702e0b
--- /dev/null
+++ b/0-Core-Formalism/lean/Semantics/Semantics/TestCopyIf.lean
@@ -0,0 +1,36 @@
+/-
+TestCopyIf.lean — Tests for the copy_if tactic
+-/
+import Semantics.CopyIfTactic
+
+namespace Semantics.TestCopyIf
+open Semantics.CopyIfTactic
+
+-- Trivial: rfl (zero delta)
+theorem test_rfl : 1 = 1 := by copy_if
+theorem test_rfl2 : True := by copy_if
+theorem test_rfl3 : ∀ x : Nat, x = x := by intro x; copy_if
+
+-- Trivial: decide (decidable)
+theorem test_decide : 1 + 1 = 2 := by copy_if
+theorem test_decide2 : true = true := by copy_if
+theorem test_decide3 : 3 > 2 := by copy_if
+
+-- Trivial: omega (linear arithmetic)
+theorem test_omega (x : Nat) : x + 0 = x := by copy_if
+theorem test_omega2 (x : Int) : x - x = 0 := by copy_if
+theorem test_omega3 (x y : Nat) : x + y = y + x := by copy_if
+
+-- Trivial: norm_num (numeric)
+theorem test_norm_num : (2 : Nat) + 2 = 4 := by copy_if
+theorem test_norm_num2 : (3 : Int) * 4 = 12 := by copy_if
+
+-- Non-trivial: should fail with "non-trivial goal"
+-- theorem test_non_trivial (x : Nat) : x * 0 = 0 := by copy_if
+
+-- copy_if? variant: shows which closer worked
+theorem test_which_rfl : 1 = 1 := by copy_if?
+theorem test_which_decide : 3 > 2 := by copy_if?
+theorem test_which_omega (x : Nat) : x + 0 = x := by copy_if?
+
+end Semantics.TestCopyIf