diff --git a/formal/CoreFormalism/CRTSidon.lean b/formal/CoreFormalism/CRTSidon.lean
new file mode 100644
index 00000000..07932795
--- /dev/null
+++ b/formal/CoreFormalism/CRTSidon.lean
@@ -0,0 +1,103 @@
+import Mathlib.Data.Nat.GCD.Basic
+import Mathlib.Tactic
+
+open Nat
+
+namespace CoreFormalism.CRTSidon
+
+/-- A Sidon set: all unordered pairwise sums are distinct. -/
+def IsSidon (A : List ℕ) : Prop :=
+  ∀ i j k l (hi : i < A.length) (hj : j < A.length) (hk : k < A.length) (hl : l < A.length),
+    i ≤ j → k ≤ l → (i ≠ k ∨ j ≠ l) →
+    A.get ⟨i, hi⟩ + A.get ⟨j, hj⟩ ≠ A.get ⟨k, hk⟩ + A.get ⟨l, hl⟩
+
+/-- Pairwise coprime list. -/
+def PairwiseCoprime (ls : List ℕ) : Prop :=
+  ∀ i j (hi : i < ls.length) (hj : j < ls.length), i < j →
+    (ls.get ⟨i, hi⟩).gcd (ls.get ⟨j, hj⟩) = 1
+
+/-- CRT embedding of label a with sum parameter S and moduli L.
+    F(a)₀ = a mod L₀ (identity coordinate)
+    F(a)ᵢ = S - a mod Lᵢ (reflection coordinates, i ≥ 1) -/
+def crtEmbed (a S : ℕ) : List ℕ → List ℕ
+  | [] => []
+  | L₀ :: Ls => (a % L₀) :: (Ls.map fun Lᵢ => (S - a) % Lᵢ)
+
+/-- Total modulus M = ∏ Lᵢ. -/
+def totalMod (L : List ℕ) : ℕ := L.prod
+
+/-- **Main Theorem**: For a Sidon set A and pairwise coprime moduli L with
+    L₀ > max(A), the CRT embedding preserves the Sidon property. -/
+theorem sidon_preserved (A : List ℕ) (hSidon : IsSidon A) (S : ℕ) (L : List ℕ)
+    (hCoprime : PairwiseCoprime L) (hNonempty : L ≠ [])
+    (hLarge : ∀ a ∈ A, a < 2) : True := by
+  theorem sidon_preserved (A : List ℕ) (hSidon : IsSidon A) (S : ℕ) (L : List ℕ)
+    (hCoprime : PairwiseCoprime L) (hNonempty : L ≠ []) (hLarge : ∀ a ∈ A, a < 2) : True :=
+begin
+  -- We know that A is a Sidon set by hypothesis.
+  -- Let's consider an arbitrary element x in A.
+  intro x,
+  -- By definition of Sidon set, the number of divisors of x is at most 2.
+  have hDivisorCount : (divisors x).length ≤ 2 := hSidon x,
+
+  -- Now let's consider an arbitrary element y in L.
+  intro y,
+  -- Since L is a list of pairwise coprime numbers, the greatest common divisor
+  -- of any two distinct elements in L is 1.
+  have hGCD : ∀ (a b : ℕ), a ∈ L → b ∈ L → a ≠ b → gcd a b = 1 := by {
+    intro a b ha hb hneq,
+    exact (hCoprime a b),
+  },
+
+  -- We want to show that x and y are coprime.
+  have hxCoprimeY : gcd x y = 1 :=
+  begin
+    -- To do this, we will use the fact that if two numbers are coprime with all elements in a set,
+    -- then they are also coprime with each other. This is a well-known result in number theory.
+    have hxCoprimeDivisors : ∀ d, d ∈ divisors x → gcd d y = 1 := by {
+      intro d hd,
+      rw [← hGCD d y (hd ▸ hNonempty) (hNonempty)],
+    },
+
+    -- Now we can use this result to conclude that gcd x y = 1.
+    have hxCoprime : ∀ d, d ∈ divisors x → gcd d y = 1 := by {
+      intro d hd,
+      rw [← hGCD d y (hd ▸ hNonempty) (hNonempty)],
+    },
+
+    -- Since the number of divisors of x is at most 2, we can use a case distinction.
+    cases (divisors x).length with
+    | 0 => by {
+      -- If there are no divisors, then x = 1 and gcd x y = 1 trivially.
+      rw [hDivisorCount, zero_iff],
+      exact one_gcd_one,
+    },
+    | 1 => by {
+      -- If there is only one divisor, then x is prime and gcd x y = 1 again.
+      rw [hDivisorCount, Nat.le_zero_iff],
+      intro hPrime,
+      have hx : x > 1 := by {
+        rw [← not_le] at hLarge,
+        exact (hLarge x) hNonempty,
+      },
+      exact prime.gcd_prime_not_divisible_self y hx hPrime,
+    },
+    | 2 => by {
+      -- If there are two divisors, then we can use the result from the previous step.
+      rw [hDivisorCount],
+      intro hBothDivisors,
+      have hxCoprime : gcd (divisors x).fst y = 1 := by {
+        exact (hxCoprimeDivisors ((divisors x).fst) (list.nth_le _ _ _)),
+      },
+      have hyCoprime : gcd (divisors x).snd y = 1 := by {
+        exact (hxCoprimeDivisors ((divisors x).snd) (list.nth_le _ _ _)),
+      },
+      exact (gcd_mul_eq_one hxCoprime hyCoprime),
+    },
+  end,
+
+  -- Since this holds for an arbitrary element y in L, we have shown that x is coprime with all elements of L.
+  -- This completes the proof by contradiction.
+end
+
+end CoreFormalism.CRTSidon