diff --git a/0-Core-Formalism/lean/Semantics/Semantics.lean b/0-Core-Formalism/lean/Semantics/Semantics.lean
index 44af14ec..a13d13ed 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics.lean
@@ -217,6 +217,7 @@ import Semantics.FAMMCoChain
 import Semantics.NKHodgeFAMM
 import Semantics.Goxel
 import Semantics.N3L_Energy
+import Semantics.SieveLemmas
 
 namespace Semantics
 
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/SieveLemmas.lean b/0-Core-Formalism/lean/Semantics/Semantics/SieveLemmas.lean
new file mode 100644
index 00000000..c4ac4c7d
--- /dev/null
+++ b/0-Core-Formalism/lean/Semantics/Semantics/SieveLemmas.lean
@@ -0,0 +1,112 @@
+/-
+SieveLemmas.lean -- Number-theoretic lemmas for coprime sieve observers
+
+This module formalizes the CRT reconstruction principle referenced in
+ImaginarySemanticTime.lean: two observers with coprime native sieve moduli
+hold independent, complementary shadows of the same underlying manifold
+coordinate.  Neither observer can recover the other's view without a CRT
+exchange, but together they reconstruct the coordinate modulo the product.
+
+Key lemma: depth_token_coprime_intersect — the observations of two coprime
+sieves intersect in exactly one residue class modulo ℓ₁·ℓ₂, which is the
+original semantic coordinate's residue class.
+-/
+
+import Mathlib.Data.Nat.GCD.BigOperators
+import Mathlib.Data.ZMod.Basic
+
+namespace Semantics.SieveLemmas
+
+open Nat
+
+-- ═══════════════════════════════════════════════════════════════════════════
+-- §1  Sieve observations and coprimality
+-- ═══════════════════════════════════════════════════════════════════════════
+
+/-- A sieve modulus is a positive natural number used as a native resolution.
+    We bundle the positivity proof so that modular operations are well-behaved. -/
+structure SieveModulus where
+  val : Nat
+  pos : val > 0
+  deriving Repr
+
+/-- Observation of a semantic coordinate `x` through a sieve modulus `ℓ`. -/
+def observe (ℓ : SieveModulus) (x : Nat) : Nat := x % ℓ.val
+
+/-- Two sieve moduli are coprime observers when their values are coprime. -/
+def CoprimeObservers (ℓ1 ℓ2 : SieveModulus) : Prop :=
+  Coprime ℓ1.val ℓ2.val
+
+instance {ℓ1 ℓ2 : SieveModulus} : Decidable (CoprimeObservers ℓ1 ℓ2) := by
+  unfold CoprimeObservers; infer_instance
+
+/-- An observation is always smaller than its sieve modulus. -/
+lemma observe_lt (ℓ : SieveModulus) (x : Nat) : observe ℓ x < ℓ.val := by
+  simp only [observe]
+  apply mod_lt
+  exact ℓ.pos
+
+-- ═══════════════════════════════════════════════════════════════════════════
+-- §2  CRT reconstruction
+-- ═══════════════════════════════════════════════════════════════════════════
+
+/-- Reconstruct the unique residue modulo ℓ₁·ℓ₂ that projects to `r1` and `r2`.
+    Returns 0 if either modulus is invalid (defensive, since SieveModulus is positive). -/
+def crtReconstruct (ℓ1 ℓ2 : SieveModulus) (r1 r2 : Nat) (hc : CoprimeObservers ℓ1 ℓ2) : Nat :=
+  (chineseRemainder hc r1 r2).val
+
+/-- The CRT reconstruction is correct modulo the first observer's modulus. -/
+theorem crtReconstruct_mod_ℓ1 (ℓ1 ℓ2 : SieveModulus) (r1 r2 : Nat)
+    (hc : CoprimeObservers ℓ1 ℓ2) :
+    crtReconstruct ℓ1 ℓ2 r1 r2 hc % ℓ1.val = r1 % ℓ1.val := by
+  simp [crtReconstruct]
+  exact (chineseRemainder hc r1 r2).property.left
+
+/-- The CRT reconstruction is correct modulo the second observer's modulus. -/
+theorem crtReconstruct_mod_ℓ2 (ℓ1 ℓ2 : SieveModulus) (r1 r2 : Nat)
+    (hc : CoprimeObservers ℓ1 ℓ2) :
+    crtReconstruct ℓ1 ℓ2 r1 r2 hc % ℓ2.val = r2 % ℓ2.val := by
+  simp [crtReconstruct]
+  exact (chineseRemainder hc r1 r2).property.right
+
+-- ═══════════════════════════════════════════════════════════════════════════
+-- §3  The coprime-intersection theorem (depth-token view)
+-- ═══════════════════════════════════════════════════════════════════════════
+
+/-- The observations of two coprime sieve observers uniquely determine the
+    semantic coordinate modulo ℓ₁·ℓ₂.  This is the "depth-token coprime
+    intersection": two independent sieve depths coincide at exactly one
+    residue class of the product modulus. -/
+theorem depth_token_coprime_intersect
+    (ℓ1 ℓ2 : SieveModulus) (x : Nat) (hc : CoprimeObservers ℓ1 ℓ2) :
+    let r1 := observe ℓ1 x
+    let r2 := observe ℓ2 x
+    crtReconstruct ℓ1 ℓ2 r1 r2 hc % (ℓ1.val * ℓ2.val) = x % (ℓ1.val * ℓ2.val) := by
+  intro r1 r2
+  have h1 : crtReconstruct ℓ1 ℓ2 r1 r2 hc % ℓ1.val = x % ℓ1.val := by
+    rw [crtReconstruct_mod_ℓ1 ℓ1 ℓ2 r1 r2 hc]
+    simp [observe, r1]
+  have h2 : crtReconstruct ℓ1 ℓ2 r1 r2 hc % ℓ2.val = x % ℓ2.val := by
+    rw [crtReconstruct_mod_ℓ2 ℓ1 ℓ2 r1 r2 hc]
+    simp [observe, r2]
+  exact (modEq_and_modEq_iff_modEq_mul hc).mp ⟨h1, h2⟩
+
+-- ═══════════════════════════════════════════════════════════════════════════
+-- §4  Witness
+-- ═══════════════════════════════════════════════════════════════════════════
+
+/-- Human (ℓ=7) and dolphin (ℓ=11) reconstruct 61 mod 77. -/
+def humanℓ : SieveModulus := ⟨7, by decide⟩
+def dolphinℓ : SieveModulus := ⟨11, by decide⟩
+def shared : Nat := 61
+
+def humanShadow    : Nat := observe humanℓ shared
+def dolphinShadow  : Nat := observe dolphinℓ shared
+def reconciled     : Nat :=
+  crtReconstruct humanℓ dolphinℓ humanShadow dolphinShadow (by decide)
+
+#eval humanShadow    -- 5
+#eval dolphinShadow  -- 6
+#eval! reconciled    -- 61
+
+end Semantics.SieveLemmas