work in progress on thue's lemma

Compfiles/Bulgaria1998P11.lean

@@ -176,6 +176,84 @@ lemma too_good_to_be_true (n l : ℕ)
 lemma Thue's_lemma (a m : ℤ) : ∃ (x y : ℤ), a * x + y ≡ 0 [ZMOD m] ∧ 0 < x ^ 2 ∧ x ^ 2 ≤ m ∧ y ^ 2 ≤ m :=
   sorry
 
+lemma thue
+    {n : ℕ} (hm : 1 < n)
+    (a : ℕ)
+    (hn : Nat.Coprime a n) :
+    ∃ (x y : ℤ), x = (a : ZMod n) * y ∧ 0 < |x| ∧ 0 < |y| ∧ x ^ 2 < n ∧ y ^ 2 ≤ n := by
+  -- https://services.artofproblemsolving.com/download.php?id=YXR0YWNobWVudHMvMy8yL2QzYjEzOGM0ODE3YzYwZGU4NGFmOTEwZDc0ZGNhODRjOGMyMzZlLnBkZg==&rn=dGh1ZS12NC5wZGY=
+
+  -- let r = ⌊√n⌋, i.e. r is the unique integer for which
+  -- r² ≤ n < (r + 1)².
+  let r := Nat.sqrt n
+
+  -- The number of pairs (x,y) so that 0 ≤ x,y ≤ r is (r + 1)² which
+  -- is greater than n.
+
+  --
+  -- Therefore there must be two different pairs (x₁, y₁) and (x₂, y₂)
+  -- such that
+  --     x₁ - ay₁ = x₂ - ay₂ (mod n)
+  --     i.e.
+  --     x₁ - x₂ = a(y₁ - y₂) (mod n)
+  --
+
+  let D := Fin (r + 1) × Fin (r + 1)
+  let f : D → ZMod n := fun ⟨x,y⟩ ↦ (x.val : ZMod n) - a * (y.val : ZMod n)
+  have cardD : Fintype.card D = (r + 1)^2 := by
+    unfold_let D
+    rw [sq, Fintype.card_prod, Fintype.card_fin]
+
+  have : NeZero n := NeZero.of_gt hm
+  have cardZ : Fintype.card (ZMod n) = n := ZMod.card n
+
+  have hDZ : Fintype.card (ZMod n) < Fintype.card D := by
+    rw [cardD, cardZ]
+    exact Nat.lt_succ_sqrt' n
+
+  obtain ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩, hxyn, hxy⟩ :=
+    Fintype.exists_ne_map_eq_of_card_lt f hDZ
+  dsimp [f] at hxy
+  have hxy' : ↑↑x₁ - ↑↑x₂ = (a : ZMod n) * ↑↑y₁ - a * ↑↑y₂ :=
+    sub_eq_sub_iff_sub_eq_sub.mp hxy
+  use (x₁ : ℤ) - (x₂ : ℤ)
+  use (y₁ : ℤ) - (y₂ : ℤ)
+  have h3 : (((x₁ : ℕ): ℤ) : ZMod n) - (((x₂ : ℕ): ℤ) : ZMod n) =
+            (((((x₁ : ℕ): ℤ) -((x₂ : ℕ): ℤ)) : ℤ) : ZMod n) := by
+    norm_cast
+
+  constructor
+  · have h1 : ((x₁ : ℕ): ZMod n) = (((x₁ : ℕ): ℤ) : ZMod n)  := by
+      norm_cast
+    have h2 : ((x₂ : ℕ): ZMod n) = (((x₂ : ℕ): ℤ) : ZMod n)  := by
+      norm_cast
+    rw [h1, h2, h3] at hxy'
+    rw [hxy']
+    rw [←mul_sub]
+    congr 1
+    norm_cast
+  refine ⟨?_, ?_, ?_, ?_⟩
+  · by_contra! H
+    replace H : |((x₁:ℕ):ℤ) - ↑↑x₂| = 0 := by
+      have : (0 : ℤ) ≤ |((x₁:ℕ):ℤ) - ↑↑x₂| := abs_nonneg (↑↑x₁ - ↑↑x₂)
+      exact (Int.le_antisymm this H).symm
+    replace H : (((x₁:ℕ):ℤ) - ↑↑x₂) = 0 := by aesop
+    replace H : ((x₁:ℕ):ℤ) = ↑↑x₂ := Int.eq_of_sub_eq_zero H
+    replace H : x₁.val = x₂.val := Int.ofNat_inj.mp H
+    replace H : x₁ = x₂ := Fin.eq_of_val_eq H
+    rw [H, sub_self, ←mul_sub] at hxy'
+    sorry
+  · have hx₁ : x₁.val < r + 1 := x₁.prop
+    have hx₂ : x₂.val < r + 1 := x₂.prop
+    have hr1 : r^2 ≤ n := Nat.sqrt_le' n
+    have hr2 : n < (r + 1)^2 := Nat.lt_succ_sqrt' n
+    sorry
+  · sorry
+  · sorry
+
+example (a b n : ℕ) (ha : a < n + 1) (hb : b < n + 1) : ((a : ℤ) - (b : ℤ))^2 ≤ n^2 := by
+  nlinarith
+
 lemma mod_z_of_mod_n {a b m : ℕ} (h : a ≡ b [MOD m]) : a ≡ b [ZMOD m] := by
   dsimp [Int.ModEq]
   rw[show a % m = @Nat.cast ℤ _ (a % m) by norm_num]