feat(ErdosProblems): 43

FormalConjectures/ErdosProblems/43.lean

@@ -0,0 +1,62 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+import FormalConjectures.ForMathlib.Combinatorics.Basic
+
+/-!
+# Erdős Problem 43
+*Reference:* [erdosproblems.com/43](https://www.erdosproblems.com/43)
+
+-/
+
+open scoped Pointwise
+
+/-- The maximum size of a Sidon set in `{1, ..., N}`. This version is computable. -/
+def maxSidonSetSize := maxSidonSetSize'
+
+/--
+If `A` and `B` are Sidon sets in `{1, ..., N}` with disjoint difference sets,
+is the sum of unordered pair counts bounded by that of an optimal Sidon set up to `O(1)`?
+-/
+@[category research open, AMS 11 05]
+theorem erdos_43 :
+    ∃ C : ℝ, ∀ (N : ℕ) (A B : Finset ℕ),
+      A ⊆ Finset.Icc 1 N →
+      B ⊆ Finset.Icc 1 N →
+      IsSidon A.toSet →
+      IsSidon B.toSet →
+      (A - A) ∩ (B - B) = ∅ →
+      ((A.card * (A.card - 1) + B.card * (B.card - 1)) / 2 : ℝ) ≤
+        (maxSidonSetSize N * (maxSidonSetSize N - 1) / 2 : ℝ) + C := by
+  sorry
+
+/--
+If `A` and `B` are equal-sized Sidon sets with disjoint difference sets,
+can the sum of pair counts be bounded by a strict fraction of the optimum?
+-/
+@[category research open, AMS 11 05]
+theorem erdos_43_equal_size :
+    ∃ c : ℝ, 0 < c ∧ ∀ (N : ℕ) (A B : Finset ℕ),
+      A ⊆ Finset.Icc 1 N →
+      B ⊆ Finset.Icc 1 N →
+      IsSidon A.toSet →
+      IsSidon B.toSet →
+      A.card = B.card →
+      (A - A) ∩ (B - B) = ∅ →
+      ((A.card * (A.card - 1) + B.card * (B.card - 1)) / 2 : ℝ) ≤
+        (1 - c) * (maxSidonSetSize N * (maxSidonSetSize N - 1) / 2 : ℝ) := by
+  sorry

FormalConjectures/ForMathlib/Combinatorics/Basic.lean

@@ -17,6 +17,9 @@ limitations under the License.
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Data.Set.Card
 import Mathlib.Order.Defs.PartialOrder
+import Mathlib.Data.Finset.Basic
+import Mathlib.Data.Finset.Powerset
+import Mathlib.Data.Nat.Enat
 
 open Function Set
 
@@ -38,3 +41,23 @@ lemma Set.IsAPOfLength.card (s : Set α) (l : ℕ∞) (hs : s.IsAPOfLength l) :
 lemma IsSidon.avoids_isAPOfLength_three {α : Type*} [AddCommMonoid α] (A : Set ℕ) (hA : IsSidon A) :
     (∀ Y, IsAPOfLength Y 3 → (A ∩ Y).ncard ≤ 2) := by
   sorry
+
+-- Decidability instance for computable versions
+instance decidableIsSidon (A : Finset ℕ) : Decidable (IsSidon A.toSet) := by
+  unfold IsSidon
+  classical
+  simp only [Set.mem_toSet, emforall, emimp]
+  apply decidable_of_iff _ (by simp)
+  exact decidable_of_iff (∀ i₁ j₁ i₂ j₂ ∈ A, i₁ + i₂ = j₁ + j₂ → (i₁ = j₁ ∧ i₂ = j₂) ∨ (i₁ = j₂ ∧ i₂ = j₁)) (by simp)
+
+
+/-- All subset sizes of Sidon sets in `{1, ..., n}`. -/
+def SidonSubsetsSizes (n : ℕ) : Finset ℕ :=
+  Finset.image Finset.card <| (Finset.Icc 1 n).powerset.filter (λ A => IsSidon A.toSet)
+
+lemma SidonSubsetsSizesNonempty (n : ℕ) : (SidonSubsetsSizes n).Nonempty := by
+  use 0
+  simp [SidonSubsetsSizes]
+
+def maxSidonSetSize' (n : ℕ) : ℕ :=
+  (SidonSubsetsSizes n).max' (SidonSubsetsSizesNonempty n)