From 538af8d1293223a7934d63047cc4ec2b6c031fc0 Mon Sep 17 00:00:00 2001 From: allaun Date: Sat, 4 Jul 2026 11:19:04 -0500 Subject: [PATCH] =?UTF-8?q?fix(lean):=20CRTSidonN=20compiles=20=E2=80=94?= =?UTF-8?q?=20n-moduli=20CRT=20Sidon=20theorem?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- formal/CoreFormalism/CRTSidonN.lean | 113 ++++++++++++++-------------- lakefile.lean | 2 +- 2 files changed, 59 insertions(+), 56 deletions(-) diff --git a/formal/CoreFormalism/CRTSidonN.lean b/formal/CoreFormalism/CRTSidonN.lean index 867df1ed..67b5d6a8 100644 --- a/formal/CoreFormalism/CRTSidonN.lean +++ b/formal/CoreFormalism/CRTSidonN.lean @@ -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ᵢ) diff --git a/lakefile.lean b/lakefile.lean index a21df71d..4210fada 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -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,