mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-08-17 16:10:36 +00:00
103 lines
4 KiB
Text
103 lines
4 KiB
Text
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
|