mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
fix(lean): CRTSidonN compiles — n-moduli CRT Sidon theorem
14 fixes applied by agent: - Extracted coprime_to_product lemma (replaced broken 3-level nested induction) - Extracted pairwise_coprime_cons_all_coprime lemma - Fixed Int.natCast_dvd_natCast, Int.dvd_neg direction, Nat.add_mod rewrites - Fixed hL_dvd_nat builder, hprod_dvd simpa, nlinarith→calc for Nat - All 3297 jobs, 0 errors, 0 warnings
This commit is contained in:
parent
83b4f0ce2c
commit
538af8d129
2 changed files with 59 additions and 56 deletions
|
|
@ -84,6 +84,35 @@ If L is a pairwise coprime list, and each Lᵢ divides d, then
|
|||
We prove this by strong induction on the list length.
|
||||
|
||||
-/
|
||||
/-- If L₀ is coprime to every element of tail, then L₀ is coprime to the product. -/
|
||||
lemma coprime_to_product (L₀ : ℕ) : ∀ (tail : List ℕ), (∀ x ∈ tail, Nat.Coprime L₀ x) → Nat.Coprime L₀ tail.prod := by
|
||||
intro tail hall
|
||||
induction tail with
|
||||
| nil => simp
|
||||
| cons h t ih =>
|
||||
have h_coprime_h : Nat.Coprime L₀ h := hall h (by simp)
|
||||
have h_coprime_t : ∀ x ∈ t, Nat.Coprime L₀ x := by
|
||||
intro x hx
|
||||
exact hall x (by simp [hx])
|
||||
simpa [List.prod_cons] using (Nat.Coprime.mul_right h_coprime_h (ih h_coprime_t))
|
||||
|
||||
/-- If (L₀ :: tail) is pairwise coprime, then L₀ is coprime to every element of tail. -/
|
||||
lemma pairwise_coprime_cons_all_coprime (L₀ : ℕ) (tail : List ℕ) (hCoprime : PairwiseCoprime (L₀ :: tail)) :
|
||||
∀ x ∈ tail, Nat.Coprime L₀ x := by
|
||||
intro x hx
|
||||
rcases List.mem_iff_get.mp hx with ⟨n, hn⟩
|
||||
-- n : Fin tail.length, hn : tail.get n = x
|
||||
have hi_len : n.1 < tail.length := n.2
|
||||
have h_src : n.1 + 1 < (L₀ :: tail).length := by
|
||||
simpa [List.length_cons] using hi_len
|
||||
have h := hCoprime 0 (n.1 + 1) (by simp) h_src (by omega)
|
||||
-- h simplifies to L₀.gcd (tail.get n) = 1
|
||||
have h_gcd : L₀.gcd (tail.get n) = 1 := by
|
||||
simpa using h
|
||||
-- Need L₀.Coprime x, i.e., L₀.gcd x = 1
|
||||
rw [hn] at h_gcd
|
||||
exact h_gcd
|
||||
|
||||
/-- Product of a list of ℕ. -/
|
||||
def listProd (ls : List ℕ) : ℕ := ls.prod
|
||||
|
||||
|
|
@ -106,7 +135,8 @@ theorem pairwise_coprime_product_dvd (L : List ℕ) (hCoprime : PairwiseCoprime
|
|||
| cons L₀ tail IH =>
|
||||
-- L = L₀ :: tail, product = L₀ * tail.prod
|
||||
-- L₀ ∣ d (from hDiv at index 0)
|
||||
have hL0_dvd : L₀ ∣ d := hDiv 0 (by simp)
|
||||
have hL0_dvd : L₀ ∣ d := hDiv 0 (by
|
||||
simpa using Nat.zero_lt_succ (tail.length))
|
||||
-- tail elements divide d (from hDiv at shifted indices)
|
||||
have hTail_dvd : ∀ i (hi : i < tail.length), (tail.get ⟨i, hi⟩) ∣ d := by
|
||||
intro i hi
|
||||
|
|
@ -120,57 +150,15 @@ theorem pairwise_coprime_product_dvd (L : List ℕ) (hCoprime : PairwiseCoprime
|
|||
-- L₀ is coprime to tail.prod
|
||||
-- (because L₀ is coprime to each element of tail)
|
||||
have hL0_coprime_tail_prod : Nat.Coprime L₀ tail.prod := by
|
||||
-- Nat.Coprime L₀ (∏tail) iff gcd(L₀, ∏tail) = 1
|
||||
-- This follows from L₀ coprime to each element of tail
|
||||
-- We prove by induction on tail
|
||||
induction tail using List.rec with
|
||||
| nil => simp [List.prod, Nat.coprime_one_right]
|
||||
| cons L₁ tail' IH' =>
|
||||
-- tail = L₁ :: tail', product = L₁ * tail'.prod
|
||||
-- gcd(L₀, L₁ * tail'.prod) = 1
|
||||
-- We know: gcd(L₀, L₁) = 1 (from hCoprime)
|
||||
-- By IH': gcd(L₀, tail'.prod) = 1
|
||||
-- Since gcd(L₀, L₁) = 1 and gcd(L₀, tail'.prod) = 1:
|
||||
-- gcd(L₀, L₁ * tail'.prod) = 1
|
||||
-- This follows from: if gcd(a,b)=1 and gcd(a,c)=1 then gcd(a,b*c)=1
|
||||
have hL0_coprime_L1 : Nat.Coprime L₀ L₁ :=
|
||||
hCoprime 0 1 (by simp) (by simp) (by omega)
|
||||
have hTailCoprime' : PairwiseCoprime tail' := by
|
||||
intro i j hi hj hij
|
||||
exact hCoprime (i + 2) (j + 2) (by simp [hi]) (by simp [hj]) (by omega)
|
||||
have hDiv_tail' : ∀ i (hi : i < tail'.length), (tail'.get ⟨i, hi⟩) ∣ d := by
|
||||
intro i hi
|
||||
-- hDiv covers the full L = L₀ :: L₁ :: tail', so index i+2
|
||||
have hlen : (L₀ :: L₁ :: tail').length = 2 + tail'.length := by simp
|
||||
have hi' : i + 2 < (L₀ :: L₁ :: tail').length := by omega
|
||||
exact hDiv (i + 2) hi'
|
||||
have hL0_coprime_tail'_prod : Nat.Coprime L₀ tail'.prod := by
|
||||
-- By structural induction on tail', using:
|
||||
-- L₀ coprime to each element → L₀ coprime to product
|
||||
induction tail' using List.rec with
|
||||
| nil => simp
|
||||
| cons L₂ tail'' IH'' =>
|
||||
have hL0_coprime_L2 : Nat.Coprime L₀ L₂ :=
|
||||
hCoprime 0 2 (by simp) (by simp) (by omega)
|
||||
have hTail''_coprime : PairwiseCoprime tail'' := by
|
||||
intro i j hi hj hij
|
||||
exact hCoprime (i + 3) (j + 3) (by simp [hi]) (by simp [hj]) (by omega)
|
||||
have hL0_coprime_tail''_prod : Nat.Coprime L₀ tail''.prod :=
|
||||
exact IH''
|
||||
exact (Nat.Coprime.mul_right hL0_coprime_L2 hL0_coprime_tail''_prod)
|
||||
-- gcd(L₀, L₁ * tail'.prod) = 1
|
||||
-- Use: Nat.Coprime.mul_right or Nat.coprime_mul
|
||||
-- If gcd(L₀, L₁) = 1 and gcd(L₀, tail'.prod) = 1
|
||||
-- then gcd(L₀, L₁ * tail'.prod) = 1
|
||||
-- gcd(L₀, L₁ * tail'.prod) = 1
|
||||
exact (Nat.Coprime.mul_right hL0_coprime_L1 hL0_coprime_tail'_prod)
|
||||
apply coprime_to_product L₀ tail
|
||||
apply pairwise_coprime_cons_all_coprime L₀ tail hCoprime
|
||||
-- Since L₀ ∣ d and tail.prod ∣ d and gcd(L₀, tail.prod) = 1:
|
||||
-- L₀ * tail.prod ∣ d
|
||||
-- Use: Nat.Coprime.dvd_mul or Nat.mul_dvd_of_coprime
|
||||
have hprod_dvd : L₀ * tail.prod ∣ d :=
|
||||
Nat.Coprime.mul_dvd_of_dvd_of_dvd hL0_coprime_tail_prod hL0_dvd hTailProd_dvd
|
||||
-- product of (L₀ :: tail) = L₀ * tail.prod
|
||||
simp [List.prod, hprod_dvd]
|
||||
simpa [List.prod_cons] using hprod_dvd
|
||||
|
||||
/-! ### Generalized CRT uniqueness (n moduli) -/
|
||||
|
||||
|
|
@ -205,6 +193,7 @@ theorem mod_eq_of_coprime_list {a b : ℕ} (L : List ℕ)
|
|||
omega
|
||||
rw [hd_eq] at h
|
||||
rw [Int.natCast_dvd_natCast] at h
|
||||
exact h
|
||||
-- ∏Lᵢ ∣ d
|
||||
have hprod_dvd : L.prod ∣ d := pairwise_coprime_product_dvd L hCoprime hL_dvd_nat
|
||||
-- |a - b| < ∏Lᵢ (since a, b < ∏Lᵢ)
|
||||
|
|
@ -237,8 +226,8 @@ theorem mod_eq_of_coprime_list {a b : ℕ} (L : List ℕ)
|
|||
have h := hL_dvd i hi
|
||||
rw [hd_eq] at h
|
||||
-- (Lᵢ : ℤ) ∣ -(d : ℤ) → (Lᵢ : ℤ) ∣ (d : ℤ)
|
||||
have h' : (L.get ⟨i, hi⟩ : ℤ) ∣ (d : ℤ) := Int.dvd_neg.mpr h
|
||||
rwa [Int.natCast_dvd_natCast_iff] at h'
|
||||
have h' : (L.get ⟨i, hi⟩ : ℤ) ∣ (d : ℤ) := Int.dvd_neg.mp h
|
||||
rwa [Int.natCast_dvd_natCast] at h'
|
||||
have hprod_dvd : L.prod ∣ d := pairwise_coprime_product_dvd L hCoprime hL_dvd_nat
|
||||
have hd_lt : d < L.prod := by
|
||||
dsimp [d]
|
||||
|
|
@ -248,7 +237,12 @@ theorem mod_eq_of_coprime_list {a b : ℕ} (L : List ℕ)
|
|||
· dsimp [d] at hq
|
||||
rw [hq0, mul_zero] at hq
|
||||
omega
|
||||
· have hprod_le : L.prod ≤ d := by rw [hq]; have : 1 ≤ q := by omega; nlinarith
|
||||
· have hprod_le : L.prod ≤ d := by
|
||||
rw [hq]
|
||||
have : 1 ≤ q := by omega
|
||||
calc
|
||||
L.prod = L.prod * 1 := by simp
|
||||
_ ≤ L.prod * q := Nat.mul_le_mul_left L.prod this
|
||||
omega
|
||||
|
||||
/-! ### Reflection → sum congruence -/
|
||||
|
|
@ -301,7 +295,7 @@ theorem sidon_preserved_mod_n (A : Finset ℕ) (hSidon : IsSidon A) (S : ℕ)
|
|||
∀ ⦃a b c d : ℕ⦄, a ∈ A → b ∈ A → c ∈ A → d ∈ A →
|
||||
-- identity component (index 0)
|
||||
(a % (L.head hNonempty) + b % (L.head hNonempty)) % (L.head hNonempty) =
|
||||
(c % (L.get ⟨0, by simp⟩) + d % (L.get ⟨0, by simp⟩)) % (L.get ⟨0, by simp⟩) →
|
||||
(c % (L.head hNonempty) + d % (L.head hNonempty)) % (L.head hNonempty) →
|
||||
-- reflection components (indices ≥ 1)
|
||||
(∀ i (hi : 1 ≤ i) (hi' : i < L.length),
|
||||
((S - a) % (L.get ⟨i, hi'⟩) + (S - b) % (L.get ⟨i, hi'⟩)) % (L.get ⟨i, hi'⟩) =
|
||||
|
|
@ -311,8 +305,10 @@ theorem sidon_preserved_mod_n (A : Finset ℕ) (hSidon : IsSidon A) (S : ℕ)
|
|||
-- Step 1: identity component → (a+b) % L₀ = (c+d) % L₀
|
||||
have hlen0 : 0 < L.length := List.length_pos_of_ne_nil hNonempty
|
||||
have hL0_cong : (a + b) % (L.head hNonempty) = (c + d) % (L.head hNonempty) := by
|
||||
rw [Nat.add_mod, Nat.add_mod]
|
||||
exact h_id
|
||||
calc
|
||||
(a + b) % (L.head hNonempty) = (a % (L.head hNonempty) + b % (L.head hNonempty)) % (L.head hNonempty) := by rw [Nat.add_mod]
|
||||
_ = (c % (L.head hNonempty) + d % (L.head hNonempty)) % (L.head hNonempty) := h_id
|
||||
_ = (c + d) % (L.head hNonempty) := by rw [← Nat.add_mod]
|
||||
-- Step 2: reflection components → (a+b) % Lᵢ = (c+d) % Lᵢ for all i ≥ 1
|
||||
have hRef_cong : ∀ i (hi : 1 ≤ i) (hi' : i < L.length),
|
||||
(a + b) % (L.get ⟨i, hi'⟩) = (c + d) % (L.get ⟨i, hi'⟩) := by
|
||||
|
|
@ -321,7 +317,12 @@ theorem sidon_preserved_mod_n (A : Finset ℕ) (hSidon : IsSidon A) (S : ℕ)
|
|||
have hS_b : b ≤ S := hS b hb
|
||||
have hS_c : c ≤ S := hS c hc
|
||||
have hS_d : d ≤ S := hS d hd
|
||||
exact reflection_implies_sum_cong hS_a hS_b hS_c hS_d (h_ref i hi hi')
|
||||
have h_ref_simple : ((S - a) + (S - b)) % (L.get ⟨i, hi'⟩) = ((S - c) + (S - d)) % (L.get ⟨i, hi'⟩) := by
|
||||
calc
|
||||
((S - a) + (S - b)) % (L.get ⟨i, hi'⟩) = ((S - a) % (L.get ⟨i, hi'⟩) + (S - b) % (L.get ⟨i, hi'⟩)) % (L.get ⟨i, hi'⟩) := by rw [Nat.add_mod]
|
||||
_ = ((S - c) % (L.get ⟨i, hi'⟩) + (S - d) % (L.get ⟨i, hi'⟩)) % (L.get ⟨i, hi'⟩) := h_ref i hi hi'
|
||||
_ = ((S - c) + (S - d)) % (L.get ⟨i, hi'⟩) := by rw [← Nat.add_mod]
|
||||
exact reflection_implies_sum_cong hS_a hS_b hS_c hS_d h_ref_simple
|
||||
-- Step 3: All components congruent: (a+b) ≡ (c+d) (mod Lᵢ) for ALL i
|
||||
have hAll_cong : ∀ i (hi : i < L.length),
|
||||
(a + b) % (L.get ⟨i, hi⟩) = (c + d) % (L.get ⟨i, hi⟩) := by
|
||||
|
|
@ -330,8 +331,10 @@ theorem sidon_preserved_mod_n (A : Finset ℕ) (hSidon : IsSidon A) (S : ℕ)
|
|||
· subst hi0
|
||||
-- L.get ⟨0, hi⟩ = L.head hNonempty (both return first element)
|
||||
have h_head_eq : L.get ⟨0, hi⟩ = L.head hNonempty := by
|
||||
simp
|
||||
rw [h_head_eq, h_head_eq]
|
||||
cases L
|
||||
· exfalso; exact hNonempty rfl
|
||||
· simp
|
||||
rw [h_head_eq]
|
||||
exact hL0_cong
|
||||
· exact hRef_cong i (by omega) hi
|
||||
-- Step 4: By generalized CRT, a+b = c+d (since both < ∏Lᵢ)
|
||||
|
|
|
|||
|
|
@ -47,7 +47,7 @@ lean_lib «SilverSightFormal» where
|
|||
`CoreFormalism.HopfFibration,
|
||||
`CoreFormalism.StrandCapacityBound,
|
||||
`CoreFormalism.CRTSidon,
|
||||
-- `CoreFormalism.CRTSidonN, -- TODO(lean-port): auto-generated, ~10 remaining structural issues
|
||||
`CoreFormalism.CRTSidonN,
|
||||
`SilverSight.AngrySphinx,
|
||||
`SilverSight.CollatzBraid,
|
||||
`SilverSight.GoldenSpiral,
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue