import Mathlib.Data.Set.Basic import Mathlib.Data.Finset.Basic import Mathlib.Data.Finset.Sort import Mathlib.Analysis.SpecialFunctions.Pow.Real import Mathlib.Algebra.Order.Chebyshev import Mathlib.Tactic.Zify import Mathlib.FieldTheory.Finite.GaloisField import Mathlib.FieldTheory.Finite.Trace import Mathlib.FieldTheory.Finite.Basic import Mathlib.FieldTheory.Minpoly.Field import Mathlib.FieldTheory.IntermediateField.Basic import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic import Mathlib.RingTheory.Trace.Basic import Mathlib.RingTheory.PowerBasis import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas import Mathlib.LinearAlgebra.Dimension.RankNullity import Mathlib.LinearAlgebra.LinearIndependent.Defs import Mathlib.LinearAlgebra.LinearIndependent.Lemmas import Mathlib.LinearAlgebra.Span.Basic import Mathlib.GroupTheory.SpecificGroups.Cyclic import Mathlib.GroupTheory.QuotientGroup.Basic import Mathlib.GroupTheory.Index import Mathlib.GroupTheory.OrderOfElement import Mathlib.Tactic.LinearCombination import Mathlib.Tactic.FieldSimp import Mathlib.NumberTheory.Bertrand /-! # Sidon Sets — Singer Construction Infrastructure Port of the reusable Sidon-set infrastructure from Hulak–Ramos–de Queiroz (2026), "Formalizing Singer Sidon Constructions and Sidon Set Infrastructure in Lean 4" (arXiv: 2605.03274). Original Lean 4 source: https://github.com/d0d1/singer-theorem-lean Commit: 0c890589afc58e8955a5d7c3a609daff6447da31 License: GPL-3.0-only ## Relationship to existing Semantics.SidonSet The existing `Semantics.SidonSet` uses a greedy `List Natat` generator with a computable `isSidon : List Natat → Prop` check. This module provides the mathematically rigorous `Finset Z` version used in the paper's proofs. Both coexist: the List Natat version for computation, the Finset Z version for formal combinatorics. ## References - Singer, J. (1938). A theorem in finite projective geometry and some applications. *Trans. Amer. Math. Soc.*, 43, 377-385. - Lindstrom, B. (1969). An inequality for B2-sequences. *J. Combin. Theory*, 6(2), 211-212. - Erdos, P. (1976). Problems and results in combinatorial number theory. *Asterisque*, 24-25, 295-310. (Problem 30) - Research-Stack: Sidon-Based Chaos Game for Equation Search (2026) -/ namespace SilverSight.SidonSets open Finset abbrev Z := Int abbrev N := Nat /-! ## Core Sidon Definitions (Finset Z) -/ /-- The Sidon property for a finite set of integers: all pairwise sums a + b (with a, b in A) are distinct up to reordering. This is the standard combinatorial definition used in the Erdos Problem 30 literature. -/ def IsSidon (A : Finset Z) : Prop := ∀ {{a b c d : Z}}, a ∈ A → b ∈ A → c ∈ A → d ∈ A → a + b = c + d → (a = c ∧ b = d) ∨ (a = d ∧ b = c) /-! ## Modular Sidon Sets -/ /-- `IsSidonMod M A` means A is Sidon modulo M: for any a, b, c, d in A, M | ((a + b) - (c + d)) implies {a, b} = {c, d} as unordered pairs. This is the form needed for Singer's construction, which produces Sidon sets in Z/(q^2+q+1)Z. -/ def IsSidonMod (M : Z) (A : Finset Z) : Prop := ∀ {{a b c d : Z}}, a ∈ A → b ∈ A → c ∈ A → d ∈ A → (M ∣ ((a + b) - (c + d))) → (a = c ∧ b = d) ∨ (a = d ∧ b = c) /-- Modular Sidon implies integer Sidon. -/ theorem IsSidonMod.toIsSidon {M : Z} {A : Finset Z} (h : IsSidonMod M A) : IsSidon A := by intro a b c d ha hb hc hd hsum exact h ha hb hc hd (by rw [hsum, sub_self]; exact dvd_zero M) /-! ## Interval Sidon Sets -/ /-- The interval {1, ..., N} as a Finset Z. Empty when N < 1. -/ noncomputable def interval (N : Z) : Finset Z := Finset.Icc 1 N /-- A Sidon subset of {1, ..., N}. -/ structure IsIntervalSidon (N : Z) (A : Finset Z) : Prop where subset : ∀ x ∈ A, 1 <= x ∧ x <= N sidon : IsSidon A /-- Enlarging the ambient interval preserves IsIntervalSidon. -/ theorem IsIntervalSidon.mono {A : Finset Z} {N M : Z} (h : IsIntervalSidon N A) (hle : N <= M) : IsIntervalSidon M A where subset x hx := ⟨(h.subset x hx).1, le_trans (h.subset x hx).2 hle⟩ sidon := h.sidon /-! ## Translation -/ /-- Translate a finset by t. -/ def translate (A : Finset Z) (t : Z) : Finset Z := A.map (⟨fun x => x + t, fun _ _ h => add_right_cancel h⟩ : Z ↪ Z) @[simp] theorem card_translate (A : Finset Z) (t : Z) : (translate A t).card = A.card := by simp [translate] /-- Translation preserves the Sidon property. -/ theorem IsSidon.translate {A : Finset Z} (hA : IsSidon A) (t : Z) : IsSidon (translate A t) := by intro a b c d ha hb hc hd hsum rcases Finset.mem_map.1 ha with ⟨a', ha', ha_eq⟩ rcases Finset.mem_map.1 hb with ⟨b', hb', hb_eq⟩ rcases Finset.mem_map.1 hc with ⟨c', hc', hc_eq⟩ rcases Finset.mem_map.1 hd with ⟨d', hd', hd_eq⟩ have ha_val : a' + t = a := by simpa using ha_eq have hb_val : b' + t = b := by simpa using hb_eq have hc_val : c' + t = c := by simpa using hc_eq have hd_val : d' + t = d := by simpa using hd_eq have hsum' : a' + b' = c' + d' := by calc a' + b' = (a' + t) + (b' + t) - (t + t) := by ring _ = a + b - (t + t) := by simp [ha_val, hb_val] _ = c + d - (t + t) := by rw [hsum] _ = (c' + t) + (d' + t) - (t + t) := by simp [hc_val, hd_val] _ = c' + d' := by ring rcases hA ha' hb' hc' hd' hsum' with (⟨hac, hbd⟩ | ⟨had, hbc⟩) · left constructor · calc a = a' + t := ha_val.symm _ = c' + t := by rw [hac] _ = c := hc_val · calc b = b' + t := hb_val.symm _ = d' + t := by rw [hbd] _ = d := hd_val · right constructor · calc a = a' + t := ha_val.symm _ = d' + t := by rw [had] _ = d := hd_val · calc b = b' + t := hb_val.symm _ = c' + t := by rw [hbc] _ = c := hc_val /-! ## Extremal Function h(N) -/ /-- `IsSidonMaximum N h` states that h is the maximum cardinality of an interval Sidon subset of {1, ..., N}. -/ def IsSidonMaximum (N h : Nat) : Prop := (∃ A : Finset Z, IsIntervalSidon (N : Z) A ∧ A.card = h) ∧ ∀ {A : Finset Z}, IsIntervalSidon (N : Z) A → A.card <= h /-- Helper: the maximum Sidon cardinality ∃ for every N. -/ private theorem sidonMaximum_exists (N : Nat) : ∃ h, IsSidonMaximum N h := by let intervalN := Finset.Icc 1 (N : Z) let cards : Set Nat := {k | ∃ (A : Finset Z), A ⊆ intervalN ∧ IsSidon A ∧ A.card = k} have h_nonempty : cards.Nonempty := by refine ⟨0, ∅, Finset.empty_subset intervalN, ?_, Finset.card_empty⟩ intro a b c d ha hb hc hd hsum simp at ha have h_fin : Set.Finite cards := by have h_fin_img : Set.Finite ((intervalN.powerset.image Finset.card : Finset Nat) : Set Nat) := Finset.finite_toSet _ apply Set.Finite.subset h_fin_img intro k hk rcases hk with ⟨A, hA_sub, hA_sidon, hcard⟩ refine Finset.mem_image.mpr ⟨A, ?_, hcard⟩ exact Finset.mem_powerset.mpr hA_sub have h_finset_nonempty : h_fin.toFinset.Nonempty := by rcases h_nonempty with ⟨k, hk⟩ refine ⟨k, h_fin.mem_toFinset.mpr hk⟩ let m := h_fin.toFinset.max' h_finset_nonempty have hm_cards : m ∈ cards := h_fin.mem_toFinset.mp (Finset.max'_mem _ h_finset_nonempty) rcases hm_cards with ⟨A, hA_sub, hA_sidon, hcard⟩ refine ⟨m, ?_⟩ constructor · refine ⟨A, ?_, hcard⟩ refine { subset := λ x hx => ?_, sidon := hA_sidon } have hx_mem_icc : x ∈ intervalN := hA_sub hx rcases Finset.mem_Icc.1 hx_mem_icc with ⟨hx1, hx2⟩ exact ⟨hx1, hx2⟩ · intro B hB have hB_sub : B ⊆ intervalN := by intro x hx; rcases hB.subset x hx with ⟨hx1, hx2⟩ exact Finset.mem_Icc.mpr ⟨hx1, hx2⟩ have hB_card : B.card ∈ cards := ⟨B, hB_sub, hB.sidon, rfl⟩ have hB_fin : B.card ∈ h_fin.toFinset := h_fin.mem_toFinset.mpr hB_card exact Finset.le_max' h_fin.toFinset (B.card) hB_fin /-- The extremal Sidon function h(N) = max{|A| : A ⊆ {1,...,N} is Sidon}. -/ noncomputable def sidonMaximum (N : Nat) : Nat := Classical.choose (sidonMaximum_exists N) /-- The maximum ∃ for every N. -/ theorem sidonMaximum_isSidonMaximum (N : Nat) : IsSidonMaximum N (sidonMaximum N) := Classical.choose_spec (sidonMaximum_exists N) /-- The maximum cardinality is unique. -/ theorem isSidonMaximum_unique {N h k : Nat} (hh : IsSidonMaximum N h) (hk : IsSidonMaximum N k) : h = k := by rcases hh.1 with ⟨A, hA, hAcard⟩ rcases hk.1 with ⟨B, hB, hBcard⟩ have hle : h <= k := by rw [← hAcard]; exact hk.2 hA have hge : k <= h := by rw [← hBcard]; exact hh.2 hB omega /-! ## Difference-Counting Upper Bound -/ /-- First upper bound: for any interval Sidon set A ⊆ {1,...,N}, |A| ≤ √(2N) + 1. This follows from pair-difference counting. -/ theorem IsIntervalSidon.card_le {A : Finset Z} {N : Nat} (h : IsIntervalSidon (N : Z) A) (hN : 1 <= N) : A.card <= Nat.sqrt (2 * N) + 1 := by set m := A.card with hm have hA_sidon : IsSidon A := h.sidon have hbound : ∀ x ∈ A, 1 <= x ∧ x <= N := h.subset -- All positive differences a-b (a,b ∈ A, a > b) are distinct by the Sidon property have h_diff_unique : ∀ a b c d : Z, a ∈ A → b ∈ A → c ∈ A → d ∈ A → a > b → c > d → a - b = c - d → a = c ∧ b = d := by intro a b c d ha hb hc hd ha_gt hc_gt h_eq have hsum : a + d = b + c := by linarith rcases hA_sidon ha hd hb hc hsum with (⟨h1, h2⟩ | ⟨h1, h2⟩) · -- a = b and d = c, but a > b contradicts a = b exfalso exact lt_irrefl a (h1 ▸ ha_gt) · exact ⟨h1, h2.symm⟩ -- P = ordered pairs (a,b) ∈ AxA with a > b let P := (A.product A).filter (λ (ab : Z × Z) => ab.1 > ab.2) have hP_injOn : Set.InjOn (λ (ab : Z × Z) => ab.1 - ab.2) (P : Set (Z × Z)) := by intro x hx y hy h rcases x with ⟨a,b⟩; rcases y with ⟨c,d⟩ have haA : a ∈ A := (Finset.mem_product.1 ((Finset.mem_filter.1 hx).1)).1 have hbA : b ∈ A := (Finset.mem_product.1 ((Finset.mem_filter.1 hx).1)).2 have hcA : c ∈ A := (Finset.mem_product.1 ((Finset.mem_filter.1 hy).1)).1 have hdA : d ∈ A := (Finset.mem_product.1 ((Finset.mem_filter.1 hy).1)).2 have ha_gt_b : a > b := (Finset.mem_filter.1 hx).2 have hc_gt_d : c > d := (Finset.mem_filter.1 hy).2 rcases h_diff_unique a b c d haA hbA hcA hdA ha_gt_b hc_gt_d h with ⟨hac, hbd⟩ ext <;> assumption have hP_card_diffs : (Finset.image (λ (ab : Z × Z) => ab.1 - ab.2) P).card = P.card := Finset.card_image_of_injOn hP_injOn have hP_card : P.card = m * (m - 1) / 2 := by have h_total : (A.product A).card = m * m := by simp [hm, Finset.card_product] have h_swap_card : (Finset.image Prod.swap P).card = P.card := Finset.card_image_of_injective _ Prod.swap_injective have h_swap_eq : Finset.image Prod.swap P = ((A.product A).filter (λ (ab : Z × Z) => ab.1 < ab.2)) := by ext ⟨a, b⟩ constructor · intro hmem rcases Finset.mem_image.1 hmem with ⟨⟨x, y⟩, hxy, hswap⟩ rcases Finset.mem_filter.1 hxy with ⟨hprod, hgt⟩ rcases Finset.mem_product.1 hprod with ⟨hx, hy⟩ have h1 : y = a := congrArg Prod.fst hswap have h2 : x = b := congrArg Prod.snd hswap subst h1; subst h2 exact Finset.mem_filter.2 ⟨Finset.mem_product.2 ⟨hy, hx⟩, hgt⟩ · intro hmem rcases Finset.mem_filter.1 hmem with ⟨hprod, hlt⟩ rcases Finset.mem_product.1 hprod with ⟨ha, hb⟩ exact Finset.mem_image.2 ⟨(b, a), Finset.mem_filter.2 ⟨Finset.mem_product.2 ⟨hb, ha⟩, hlt⟩, rfl⟩ have h_diag_card : ((A.product A).filter (λ (ab : Z × Z) => ab.1 = ab.2)).card = m := by have himg : ((A.product A).filter (λ (ab : Z × Z) => ab.1 = ab.2)) = A.image (λ (x : Z) => (x, x)) := by ext ⟨a, b⟩ constructor · intro hmem rcases Finset.mem_filter.1 hmem with ⟨hprod, heq⟩ have ha : a ∈ A := (Finset.mem_product.1 hprod).1 have heq' : a = b := heq subst heq' exact Finset.mem_image.2 ⟨a, ha, rfl⟩ · intro hmem rcases Finset.mem_image.1 hmem with ⟨x, hx, hxy⟩ have h1 : x = a := congrArg Prod.fst hxy have h2 : x = b := congrArg Prod.snd hxy subst h1; subst h2 exact Finset.mem_filter.2 ⟨Finset.mem_product.2 ⟨hx, hx⟩, rfl⟩ rw [himg, Finset.card_image_of_injective _ (fun x y hxy => congrArg Prod.fst hxy)] -- Partition product into >, <, = have h_partition : (A.product A) = P ∪ ((A.product A).filter (λ (ab : Z × Z) => ab.1 < ab.2)) ∪ ((A.product A).filter (λ (ab : Z × Z) => ab.1 = ab.2)) := by ext ⟨a, b⟩ constructor · intro hmem rcases lt_trichotomy a b with hlt | heq | hgt · exact Finset.mem_union.2 (Or.inl (Finset.mem_union.2 (Or.inr (Finset.mem_filter.2 ⟨hmem, hlt⟩)))) · exact Finset.mem_union.2 (Or.inr (Finset.mem_filter.2 ⟨hmem, heq⟩)) · exact Finset.mem_union.2 (Or.inl (Finset.mem_union.2 (Or.inl (Finset.mem_filter.2 ⟨hmem, hgt⟩)))) · intro hmem rcases Finset.mem_union.1 hmem with h | h · rcases Finset.mem_union.1 h with h' | h' · exact (Finset.mem_filter.1 h').1 · exact (Finset.mem_filter.1 h').1 · exact (Finset.mem_filter.1 h).1 have h_disjoint_gt_lt : Disjoint P ((A.product A).filter (λ (ab : Z × Z) => ab.1 < ab.2)) := by rw [Finset.disjoint_left] rintro ⟨a, b⟩ hP hlt have h1 : a > b := (Finset.mem_filter.1 hP).2 have h2 : a < b := (Finset.mem_filter.1 hlt).2 exact (lt_asymm h1 h2).elim have h_disjoint_union_eq : Disjoint (P ∪ ((A.product A).filter (λ (ab : Z × Z) => ab.1 < ab.2))) ((A.product A).filter (λ (ab : Z × Z) => ab.1 = ab.2)) := by rw [Finset.disjoint_left] rintro ⟨a, b⟩ hmem heq have h2 : a = b := (Finset.mem_filter.1 heq).2 rcases Finset.mem_union.1 hmem with h | h · have h1 : a > b := (Finset.mem_filter.1 h).2 rw [h2] at h1 exact (lt_irrefl b h1).elim · have h1 : a < b := (Finset.mem_filter.1 h).2 rw [h2] at h1 exact (lt_irrefl b h1).elim -- Count: |P| + |<| + |=| = m*m, and |P| = |<| have h_lt_card : ((A.product A).filter (λ (ab : Z × Z) => ab.1 < ab.2)).card = P.card := by calc ((A.product A).filter (λ (ab : Z × Z) => ab.1 < ab.2)).card = (Finset.image Prod.swap P).card := by rw [h_swap_eq] _ = P.card := h_swap_card have h_total_card : P.card + ((A.product A).filter (λ (ab : Z × Z) => ab.1 < ab.2)).card + ((A.product A).filter (λ (ab : Z × Z) => ab.1 = ab.2)).card = m * m := by calc P.card + ((A.product A).filter (λ (ab : Z × Z) => ab.1 < ab.2)).card + ((A.product A).filter (λ (ab : Z × Z) => ab.1 = ab.2)).card = (P ∪ ((A.product A).filter (λ (ab : Z × Z) => ab.1 < ab.2)) ∪ ((A.product A).filter (λ (ab : Z × Z) => ab.1 = ab.2))).card := by rw [Finset.card_union_of_disjoint h_disjoint_union_eq, Finset.card_union_of_disjoint h_disjoint_gt_lt] _ = (A.product A).card := by conv_lhs => rw [← h_partition] _ = m * m := h_total rw [h_lt_card, h_diag_card] at h_total_card have hmm : m * (m - 1) + m = m * m := by rcases Nat.eq_zero_or_pos m with hm0 | hm0 · simp [hm0] · calc m * (m - 1) + m = m * (m - 1 + 1) := by ring _ = m * m := by rw [Nat.sub_add_cancel hm0] omega have hD_bound : Finset.image (λ (ab : Z × Z) => ab.1 - ab.2) P ⊆ Finset.Icc 1 (N - 1 : Z) := by intro d hd rcases Finset.mem_image.1 hd with ⟨⟨a, b⟩, hP, hd_eq⟩ have haA : a ∈ A := (Finset.mem_product.1 ((Finset.mem_filter.1 hP).1)).1 have hbA : b ∈ A := (Finset.mem_product.1 ((Finset.mem_filter.1 hP).1)).2 have ha_gt_b : a > b := (Finset.mem_filter.1 hP).2 rcases hbound a haA with ⟨ha1, haN⟩ rcases hbound b hbA with ⟨hb1, hbN⟩ rw [← hd_eq] have h_pos : 1 <= a - b := by have h : a >= b + 1 := Int.add_one_le_of_lt ha_gt_b exact Int.le_sub_left_of_add_le h have h_le : a - b <= (N : Z) - 1 := by have h3 : a - b <= (N : Z) - b := Int.sub_le_sub_right haN b have h4 : (N : Z) - b <= (N : Z) - 1 := Int.sub_le_sub_left hb1 (N : Z) exact le_trans h3 h4 exact Finset.mem_Icc.mpr ⟨h_pos, h_le⟩ have h_icc_card : (Finset.Icc 1 (N - 1 : Z) : Finset Z).card = N - 1 := by simp have hP_card_le : m * (m - 1) / 2 <= N - 1 := by calc m * (m - 1) / 2 = P.card := hP_card.symm _ = (Finset.image (λ (ab : Z × Z) => ab.1 - ab.2) P).card := hP_card_diffs.symm _ <= (Finset.Icc 1 (N - 1 : Z) : Finset Z).card := Finset.card_le_card hD_bound _ = N - 1 := h_icc_card -- From m*(m-1)/2 <= N-1, prove m <= √(2N) + 1 by contradiction have hpar : 2 ∣ m * (m - 1) := by rcases Nat.even_or_odd m with he | ho · exact he.two_dvd.mul_right _ · exact ((Nat.Odd.sub_odd ho odd_one).two_dvd).mul_left _ have hm_sq_sub_m_le : m * (m - 1) <= 2 * (N - 1) := by omega by_contra! H have hm_gt : m > Nat.sqrt (2 * N) + 1 := H set s := Nat.sqrt (2 * N) with hs have hm_ge : m >= s + 2 := by omega have hm_sq_sub_m_gt : m * (m - 1) > 2 * (N - 1) := by have h_sq_lt : 2 * N < (s + 1) * (s + 1) := Nat.lt_succ_sqrt (2 * N) have hm_m_hm1_ge : m * (m - 1) >= (s + 2) * (s + 1) := Nat.mul_le_mul hm_ge (by omega) have h_gt : (s + 2) * (s + 1) > 2 * (N - 1) := by have hexp : (s + 2) * (s + 1) = (s + 1) * (s + 1) + (s + 1) := by ring omega omega omega /-- The quadratic upper bound on sidonMaximum: h(N) <= √(2N) + 1. -/ theorem sidonMaximum_le_sqrt_two (N : Nat) (hN : 1 <= N) : sidonMaximum N <= Nat.sqrt (2 * N) + 1 := by have hmax := sidonMaximum_isSidonMaximum N rcases hmax.1 with ⟨A, hA, hAcard⟩ have hcard := hA.card_le hN rw [hAcard] at hcard exact hcard /-! ## Lindstrom's Cross-Difference Inequality -/ /-- In a strictly sorted list, elements from `take k` are strictly less than elements from `drop k`. -/ private lemma sortedLT_take_lt_drop (l : List Z) (hs : l.SortedLT) {k : Nat} (hk_lt : k < l.length) : ∀ a ∈ l.take k, ∀ b ∈ l.drop k, a < b := by intro a ha b hb rw [List.mem_take_iff_getElem] at ha rw [List.mem_drop_iff_getElem] at hb obtain ⟨i, hi, rfl⟩ := ha obtain ⟨j, hj, rfl⟩ := hb have hi' : i < l.length := by omega have hkj : k + j < l.length := by omega exact hs (show (⟨i, hi'⟩ : Fin l.length) < ⟨k + j, hkj⟩ from by simp [Fin.lt_def]; omega) /-- In a Sidon set, cross-differences between disjoint subsets are distinct. If `L, R ⊆ A` are disjoint and `b - a = d - c` with `a, c ∈ L`, `b, d ∈ R`, then `a = c` and `b = d`. -/ theorem IsSidon.cross_diff_eq {A : Finset Z} (hA : IsSidon A) {L R : Finset Z} (hL : L ⊆ A) (hR : R ⊆ A) (hLR : Disjoint L R) {a b c d : Z} (ha : a ∈ L) (hb : b ∈ R) (hc : c ∈ L) (hd : d ∈ R) (heq : b - a = d - c) : a = c ∧ b = d := by have hsum : b + c = d + a := by linarith rcases hA (hR hb) (hL hc) (hR hd) (hL ha) hsum with h | h · exact ⟨h.2.symm, h.1⟩ · exfalso have hba : b = a := h.1 rw [hba] at hb exact Finset.disjoint_left.mp hLR ha hb /-- If `L` and `R` are disjoint subsets of an interval Sidon set in `{1,...,N}`, and every element of `L` is strictly less than every element of `R`, then the cross-difference map `(a, b) ↦ b - a` is injective from `L × R` into `{1, ..., N-1}`, giving `|L| · |R| <= N - 1`. -/ theorem IsIntervalSidon.ordered_cross_diff_le {A : Finset Z} {N : Z} (hIS : IsIntervalSidon N A) {L R : Finset Z} (hL : L ⊆ A) (hR : R ⊆ A) (hLR : Disjoint L R) (hord : ∀ a ∈ L, ∀ b ∈ R, a < b) (hN : 1 <= N) (_hLne : L.Nonempty) (_hRne : R.Nonempty) : (L.card : Z) * R.card <= N - 1 := by let f : L × R → Z := fun ⟨⟨a, _⟩, ⟨b, _⟩⟩ => b - a have hf_inj : Function.Injective f := by intro ⟨⟨a, ha⟩, ⟨b, hb⟩⟩ ⟨⟨c, hc⟩, ⟨d, hd⟩⟩ heq simp only [f] at heq have := hIS.sidon.cross_diff_eq hL hR hLR ha hb hc hd heq simp [this.1, this.2] have hf_pos : ∀ x : L × R, 1 <= f x := by intro ⟨⟨a, ha⟩, ⟨b, hb⟩⟩ simp only [f] have h : a + 1 <= b := hord a ha b hb linarith have hf_le : ∀ x : L × R, f x <= N - 1 := by intro ⟨⟨a, ha⟩, ⟨b, hb⟩⟩ simp only [f] have ha_bound := hIS.subset a (hL ha) have hb_bound := hIS.subset b (hR hb) linarith have himage_sub : Finset.univ.image f ⊆ Finset.Icc 1 (N - 1) := by intro z hz rcases Finset.mem_image.mp hz with ⟨x, _, rfl⟩ exact Finset.mem_Icc.mpr ⟨hf_pos x, hf_le x⟩ have hcard : Fintype.card (L × R) = L.card * R.card := by simp [Fintype.card_prod, Fintype.card_coe] have himage_card : (Finset.univ.image f).card = L.card * R.card := by rw [Finset.card_image_of_injective _ hf_inj] simp [Fintype.card_prod, Fintype.card_coe] have hprod_le : L.card * R.card <= (N - 1).toNat := by calc L.card * R.card = (Finset.univ.image f).card := himage_card.symm _ <= (Finset.Icc 1 (N - 1)).card := Finset.card_le_card himage_sub _ <= (N - 1).toNat := by simp have hN1 : (0 : Z) <= N - 1 := by linarith calc (L.card : Z) * R.card = ↑(L.card * R.card) := by push_cast; ring _ <= ↑(N - 1).toNat := by exact_mod_cast hprod_le _ = N - 1 := Int.toNat_of_nonneg hN1 /-- **Lindstrom's cross-difference inequality.** For a Sidon set in {1,...,N} of cardinality m, and any k with 1 <= k <= m, we have (m - k) * k <= N - 1. This follows from splitting the sorted set into bottom-`k` and top-`(m-k)` elements and applying `ordered_cross_diff_le`. Reference: Lindstrom, B. (1969). An inequality for B2-sequences. *J. Combin. Theory*, 6(2), 211-212. -/ theorem IsIntervalSidon.lindstrom_cross_ineq {A : Finset Z} {N : Nat} (hIS : IsIntervalSidon (N : Z) A) (hN : 1 <= N) {k : Nat} (hk : 1 <= k) (hkm : k <= A.card) : (A.card - k) * k <= N - 1 := by by_cases hkm_eq : k = A.card · simp [hkm_eq] have hk_lt : k < A.card := lt_of_le_of_ne hkm hkm_eq set sorted := A.sort (· <= ·) have hnd : sorted.Nodup := A.sort_nodup (· <= ·) have hlen : sorted.length = A.card := Finset.length_sort _ have hst : sorted.SortedLT := Finset.sortedLT_sort A set L := (sorted.take k).toFinset set R := (sorted.drop k).toFinset have hLA : L ⊆ A := by intro x hx; rw [List.mem_toFinset] at hx have := List.mem_of_mem_take hx; rwa [Finset.mem_sort] at this have hRA : R ⊆ A := by intro x hx; rw [List.mem_toFinset] at hx have := List.mem_of_mem_drop hx; rwa [Finset.mem_sort] at this have hLR : Disjoint L R := by rw [Finset.disjoint_left]; intro x hxL hxR rw [List.mem_toFinset] at hxL hxR exact absurd hxR ((List.disjoint_take_drop hnd (le_refl k)) hxL) have hLcard : L.card = k := by rw [List.toFinset_card_of_nodup (hnd.sublist (List.take_sublist k sorted))] rw [List.length_take, hlen]; exact Nat.min_eq_left (le_of_lt hk_lt) have hRcard : R.card = A.card - k := by rw [List.toFinset_card_of_nodup (hnd.sublist (List.drop_sublist k sorted))] rw [List.length_drop, hlen] have hord : ∀ a ∈ L, ∀ b ∈ R, a < b := by intro a ha b hb; rw [List.mem_toFinset] at ha hb exact sortedLT_take_lt_drop sorted hst (by rw [hlen]; omega) a ha b hb have hLne : L.Nonempty := by rw [Finset.nonempty_iff_ne_empty]; intro h; simp [h] at hLcard; omega have hRne : R.Nonempty := by rw [Finset.nonempty_iff_ne_empty]; intro h; simp [h] at hRcard; omega have hN_int : (1 : Z) <= (N : Z) := by exact_mod_cast hN have hint : (L.card : Z) * R.card <= (N : Z) - 1 := hIS.ordered_cross_diff_le hLA hRA hLR hord hN_int hLne hRne rw [hLcard, hRcard] at hint zify [hN, show k <= A.card from le_of_lt hk_lt] have hconv : (↑(A.card - k) : Z) = (↑A.card : Z) - ↑k := Nat.cast_sub (le_of_lt hk_lt) rw [hconv] at hint linarith /-! ## Lindstrom Improved Bound -- Johnson/Cauchy-Schwarz machinery -/ /-- For a Sidon set A, the shifted copies A+h1 and A+h2 intersect in at most one element when h1 ≠ h2. -/ theorem IsSidon.shift_inter_le_one {A : Finset Z} (hA : IsSidon A) {h1 h2 : Z} (hne : h1 ≠ h2) : ((A.image (· + h1)) ∩ (A.image (· + h2))).card <= 1 := by by_contra hgt push Not at hgt obtain ⟨x, hx, y, hy, hxy⟩ := Finset.one_lt_card.mp (by omega : 1 < ((A.image (· + h1)) ∩ (A.image (· + h2))).card) rw [Finset.mem_inter, Finset.mem_image, Finset.mem_image] at hx hy obtain ⟨⟨a1, ha1, rfl⟩, ⟨b1, hb1, hx_eq⟩⟩ := hx obtain ⟨⟨a2, ha2, rfl⟩, ⟨b2, hb2, hy_eq⟩⟩ := hy have heq1 : a1 - b1 = h2 - h1 := by linarith [hx_eq] have heq2 : a2 - b2 = h2 - h1 := by linarith [hy_eq] have hsum : a1 + b2 = a2 + b1 := by linarith rcases hA ha1 hb2 ha2 hb1 hsum with ⟨h1_eq, h2_eq⟩ | ⟨h1_eq, h2_eq⟩ · have : a1 + h1 = a2 + h1 := by rw [h1_eq] exact hxy this · have : h1 = h2 := by linarith [heq1, h1_eq] exact hne this /-- **Johnson's bound (numerical form).** If (km)^2 <= v·m·(m+k-1), then k^2·m <= v·(m+k-1). -/ theorem johnson_numerical {k m v : Nat} (hm : 0 < m) (hcs_moment : (k * m) ^ 2 <= v * (m * (m + k - 1))) : k ^ 2 * m <= v * (m + k - 1) := by have hrw1 : (k * m) ^ 2 = k ^ 2 * m * m := by ring have hrw2 : v * (m * (m + k - 1)) = v * (m + k - 1) * m := by ring rw [hrw1, hrw2] at hcs_moment exact Nat.le_of_mul_le_mul_right hcs_moment hm /-- **Incidence inequality.** For any family of finsets S1,...,Sm all contained in a universe U, (Σi |Si|)^2 <= |U| · Σi Σj |Si ∩ Sj|. Uses Cauchy-Schwarz via the degree function d(x) = #{i : x ∈ Si}. -/ theorem incidence_inequality {α : Type*} [DecidableEq α] (m : Nat) (shifts : Fin m → Finset α) (U : Finset α) (hsub : ∀ i, shifts i ⊆ U) : (∑ i : Fin m, (shifts i).card) ^ 2 <= U.card * ∑ i : Fin m, ∑ j : Fin m, ((shifts i) ∩ (shifts j)).card := by set deg : α → N := fun x => (Finset.univ.filter (fun i : Fin m => x ∈ shifts i)).card have hfilt_eq : ∀ i : Fin m, shifts i = U.filter (· ∈ shifts i) := by intro i; ext x; simp only [Finset.mem_filter] exact ⟨fun h => ⟨hsub i h, h⟩, fun h => h.2⟩ have h_dc : ∑ i : Fin m, (shifts i).card = ∑ x ∈ U, deg x := by simp only [deg] trans ∑ i : Fin m, ∑ x ∈ U, if x ∈ shifts i then 1 else 0 · congr 1; ext i conv_lhs => rw [hfilt_eq i, Finset.card_eq_sum_ones, Finset.sum_filter] · rw [Finset.sum_comm] congr 1; ext x; rw [Finset.card_eq_sum_ones, Finset.sum_filter] have hinter_eq : ∀ i j : Fin m, (shifts i) ∩ (shifts j) = U.filter (fun x => x ∈ shifts i ∧ x ∈ shifts j) := by intro i j; ext x; simp only [Finset.mem_inter, Finset.mem_filter] exact ⟨fun ⟨hi, hj⟩ => ⟨hsub i hi, hi, hj⟩, fun ⟨_, hi, hj⟩ => ⟨hi, hj⟩⟩ have h_sm : ∑ i : Fin m, ∑ j : Fin m, ((shifts i) ∩ (shifts j)).card = ∑ x ∈ U, deg x ^ 2 := by simp only [deg, sq] trans ∑ x ∈ U, ∑ i : Fin m, ∑ j : Fin m, if x ∈ shifts i ∧ x ∈ shifts j then (1 : Nat) else 0 · trans ∑ i : Fin m, ∑ j : Fin m, ∑ x ∈ U, if x ∈ shifts i ∧ x ∈ shifts j then (1 : Nat) else 0 · congr 1; ext i; congr 1; ext j conv_lhs => rw [hinter_eq i j, Finset.card_eq_sum_ones, Finset.sum_filter] · conv_lhs => arg 2; ext i; rw [Finset.sum_comm] exact Finset.sum_comm · congr 1; ext x trans (∑ i : Fin m, if x ∈ shifts i then (1 : Nat) else 0) * (∑ j : Fin m, if x ∈ shifts j then 1 else 0) · rw [Finset.sum_mul]; congr 1; ext i; rw [Finset.mul_sum] congr 1; ext j by_cases h1 : x ∈ shifts i <;> by_cases h2 : x ∈ shifts j <;> simp [h1, h2] · congr 1 <;> rw [Finset.card_eq_sum_ones, Finset.sum_filter] have h_cs : (∑ x ∈ U, deg x) ^ 2 <= U.card * ∑ x ∈ U, deg x ^ 2 := by suffices h : (∑ x ∈ U, (deg x : Z)) ^ 2 <= ↑U.card * ∑ x ∈ U, (deg x : Z) ^ 2 by exact_mod_cast h exact sq_sum_le_card_mul_sum_sq calc (∑ i : Fin m, (shifts i).card) ^ 2 = (∑ x ∈ U, deg x) ^ 2 := by rw [h_dc] _ <= U.card * ∑ x ∈ U, deg x ^ 2 := h_cs _ = U.card * ∑ i : Fin m, ∑ j : Fin m, ((shifts i) ∩ (shifts j)).card := by rw [h_sm] /-- The intersection matrix row-sum bound for shifted Sidon copies. Diagonal terms contribute k each, off-diagonal <= 1 each, total <= mk + m(m-1) = m(m+k-1). -/ theorem sidon_intersection_sum_bound {A : Finset Z} (hA : IsSidon A) (m : Nat) : ∑ i : Fin m, ∑ j : Fin m, ((A.image (· + (↑(i : Nat) : Z))) ∩ (A.image (· + (↑(j : Nat) : Z)))).card <= m * (m + A.card - 1) := by set k := A.card have hrow : ∀ i : Fin m, ∑ j : Fin m, ((A.image (· + (↑(i : Nat) : Z))) ∩ (A.image (· + (↑(j : Nat) : Z)))).card <= m + k - 1 := by intro i have hi_mem : i ∈ (Finset.univ : Finset (Fin m)) := Finset.mem_univ i rw [← Finset.sum_erase_add _ _ hi_mem] have hdiag : ((A.image (· + (↑(i : Nat) : Z))) ∩ (A.image (· + (↑(i : Nat) : Z)))).card = k := by rw [Finset.inter_self] exact Finset.card_image_of_injective _ (fun a b h => by linarith) have hoff : ∑ j ∈ Finset.univ.erase i, ((A.image (· + (↑(i : Nat) : Z))) ∩ (A.image (· + (↑(j : Nat) : Z)))).card <= m - 1 := by calc ∑ j ∈ Finset.univ.erase i, _ <= ∑ j ∈ Finset.univ.erase i, 1 := Finset.sum_le_sum (fun j hj => by have hjmem := Finset.mem_erase.mp hj have hne : (↑(i : Nat) : Z) ≠ ↑(j : Nat) := by exact_mod_cast Fin.val_ne_of_ne (Ne.symm hjmem.1) exact hA.shift_inter_le_one hne) _ = (Finset.univ.erase i).card := by simp _ = m - 1 := by simp [Finset.card_erase_of_mem hi_mem, Fintype.card_fin] have hm_pos : 0 < m := Fin.pos i omega calc ∑ i : Fin m, ∑ j : Fin m, _ <= ∑ i : Fin m, (m + k - 1) := Finset.sum_le_sum (fun i _ => hrow i) _ = m * (m + k - 1) := by simp [Finset.sum_const, Finset.card_univ, Fintype.card_fin] /-- **Johnson bound for shifted Sidon sets.** For a Sidon set A ⊆ {1,...,N} with |A| = k, the m shifted copies A, A+1, ..., A+(m-1) satisfy k^2·m <= (N+m-1)·(m+k-1). -/ theorem IsIntervalSidon.sidon_johnson_bound {A : Finset Z} {N : Nat} (hIS : IsIntervalSidon (N : Z) A) (hN : 1 <= N) (m : Nat) (hm : 0 < m) : A.card ^ 2 * m <= (N + m - 1) * (m + A.card - 1) := by set k := A.card have hA := hIS.sidon set shifts : Fin m → Finset Z := fun i => A.image (· + (↑(i : Nat) : Z)) set U := Finset.Icc (1 : Z) (↑N + ↑m - 1) have hshift_card : ∀ i : Fin m, (shifts i).card = k := fun i => Finset.card_image_of_injective _ (fun a b h => by linarith) have hsub : ∀ i : Fin m, shifts i ⊆ U := by intro i x hx simp only [shifts, Finset.mem_image] at hx obtain ⟨a, ha, rfl⟩ := hx have hAint := hIS.subset a ha simp only [U, Finset.mem_Icc] constructor · linarith [hAint.1, (i : Nat).zero_le] · have hi : (↑(i : Nat) : Z) + 1 <= (↑m : Z) := by exact_mod_cast i.isLt linarith [hAint.2] have hU_card : U.card = N + m - 1 := by simp only [U, Int.card_Icc] omega have hinc := incidence_inequality m shifts U hsub have hsum_card : ∑ i : Fin m, (shifts i).card = m * k := by simp [hshift_card, Finset.sum_const, Finset.card_univ, Fintype.card_fin] have hint : ∑ i : Fin m, ∑ j : Fin m, ((shifts i) ∩ (shifts j)).card <= m * (m + k - 1) := sidon_intersection_sum_bound hA m have hkey : (k * m) ^ 2 <= (N + m - 1) * (m * (m + k - 1)) := calc (k * m) ^ 2 = (m * k) ^ 2 := by ring _ = (∑ i : Fin m, (shifts i).card) ^ 2 := by rw [hsum_card] _ <= U.card * ∑ i : Fin m, ∑ j : Fin m, ((shifts i) ∩ (shifts j)).card := hinc _ <= U.card * (m * (m + k - 1)) := Nat.mul_le_mul_left _ hint _ = (N + m - 1) * (m * (m + k - 1)) := by rw [hU_card] exact johnson_numerical hm hkey /-- Johnson bound with Nat subtraction implies the cleaner relaxed bound. -/ theorem lindstrom_monotone {k m n : Nat} (hjohnson : k ^ 2 * m <= (n + m - 1) * (m + k - 1)) : k ^ 2 * m <= (n + m) * (m + k) := hjohnson.trans (Nat.mul_le_mul (Nat.sub_le _ _) (Nat.sub_le _ _)) set_option maxHeartbeats 1600000 in /-- **Lindstrom's upper bound.** For a Sidon set A ⊆ {1,...,N} with N >= 16, |A| <= √N + ⁴√N + 2. Uses the Johnson bound with optimal choice m = √N · ⁴√N ≈ N^{3/4}. -/ theorem IsIntervalSidon.lindstrom_bound {A : Finset Z} {N : Nat} (hIS : IsIntervalSidon (N : Z) A) (hN : 16 <= N) : A.card <= Nat.sqrt N + Nat.sqrt (Nat.sqrt N) + 2 := by by_contra h_bad push Not at h_bad set k := A.card set s := Nat.sqrt N set t := Nat.sqrt s set m := s * t have hs_ge : 4 <= s := Nat.le_sqrt.mpr (by omega : 4 ^ 2 <= N) have ht_ge : 2 <= t := Nat.le_sqrt.mpr (by omega : 2 ^ 2 <= s) have hm_pos : 0 < m := by positivity have hk_ge : s + t + 3 <= k := by omega have hN_lt : N < (s + 1) ^ 2 := Nat.lt_succ_sqrt' N have hs_lt : s < (t + 1) ^ 2 := Nat.lt_succ_sqrt' s have hN_le : N <= s ^ 2 + 2 * s := by nlinarith [hN_lt] have hs_le : s <= t ^ 2 + 2 * t := by nlinarith [hs_lt] have hJ := hIS.sidon_johnson_bound (by omega : 1 <= N) m hm_pos have hJz : (k : Z) ^ 2 * ((s : Z) * t) <= ((N : Z) + s * t - 1) * (s * t + k - 1) := by have h : k ^ 2 * (s * t) <= (N + s * t - 1) * (s * t + k - 1) := hJ have hge1 : 1 <= N + s * t := by omega have hge2 : 1 <= s * t + k := by omega zify [hge1, hge2] at h linarith have hs_z : (s : Z) <= (t : Z) ^ 2 + 2 * t := by exact_mod_cast hs_le have hN_z : (N : Z) <= (s : Z) ^ 2 + 2 * s := by exact_mod_cast hN_le have hk_z : (s : Z) + t + 3 <= (k : Z) := by exact_mod_cast hk_ge have hs_pos : (0 : Z) < (s : Z) := by linarith [show (4 : Z) <= (s : Z) from by exact_mod_cast hs_ge] have ht_pos : (0 : Z) < (t : Z) := by linarith [show (2 : Z) <= (t : Z) from by exact_mod_cast ht_ge] have hD0 : ((s : Z) + t + 3) ^ 2 * (s * t) > ((N : Z) + s * t - 1) * (s * t + s + t + 2) := by have h_id : ((s : Z) + t + 3) ^ 2 * (s * t) - ((s : Z) ^ 2 + 2 * s + s * t - 1) * (s * t + s + t + 2) = ((s : Z) ^ 2 + 4 * s) * ((t : Z) ^ 2 + 2 * t - s) + s * ((t : Z) ^ 3 + t ^ 2 - 2 * t - 3) + t + 2 := by ring have h1 : (0 : Z) <= ((s : Z) ^ 2 + 4 * s) * ((t : Z) ^ 2 + 2 * t - s) := by apply mul_nonneg <;> nlinarith have h2 : (0 : Z) < (s : Z) * ((t : Z) ^ 3 + t ^ 2 - 2 * t - 3) + t + 2 := by have ht_cube : (0 : Z) < (t : Z) ^ 3 + t ^ 2 - 2 * t - 3 := by nlinarith [mul_nonneg (show (0 : Z) <= t from by linarith) (sq_nonneg ((t : Z) - 2))] nlinarith have h_stpos : (0 : Z) <= (s : Z) * t + s + t + 2 := by positivity have h_mono : ((N : Z) + s * t - 1) * (s * t + s + t + 2) <= ((s : Z) ^ 2 + 2 * s + s * t - 1) * (s * t + s + t + 2) := by apply mul_le_mul_of_nonneg_right <;> linarith nlinarith have hDeriv : (0 : Z) <= (s : Z) * t * (k + s + t + 3) - ((N : Z) + s * t - 1) := by have ht1 : (1 : Z) <= t := ht_pos have h1 : (s : Z) * t * (2 * s + 2 * t + 6) <= s * t * (k + s + t + 3) := mul_le_mul_of_nonneg_left (by linarith) (mul_nonneg hs_pos.le ht_pos.le) have h2 : (s : Z) ^ 2 <= s ^ 2 * t := le_mul_of_one_le_right (sq_nonneg _) ht1 have h3 : (s : Z) * t <= s * t * t := le_mul_of_one_le_right (mul_nonneg hs_pos.le ht_pos.le) ht1 have h4 : (s : Z) <= s * t := le_mul_of_one_le_right hs_pos.le ht1 nlinarith [h1, h2, h3, h4, hN_z] have hFact : (k : Z) ^ 2 * (s * t) - ((N : Z) + s * t - 1) * (s * t + k - 1) = ((s : Z) + t + 3) ^ 2 * (s * t) - ((N : Z) + s * t - 1) * (s * t + s + t + 2) + ((k : Z) - s - t - 3) * ((s : Z) * t * (k + s + t + 3) - ((N : Z) + s * t - 1)) := by ring have hknn : (0 : Z) <= (k : Z) - s - t - 3 := by linarith have hprod : (0 : Z) <= ((k : Z) - s - t - 3) * ((s : Z) * t * (k + s + t + 3) - ((N : Z) + s * t - 1)) := mul_nonneg hknn hDeriv linarith /-- The Lindstrom upper bound: h(N) <= √N + √(√N) + 2 for N >= 16. -/ theorem sidonMaximum_le_lindstrom (N : Nat) (hN : 16 <= N) : sidonMaximum N <= Nat.sqrt N + Nat.sqrt (Nat.sqrt N) + 2 := by rcases (sidonMaximum_isSidonMaximum N).1 with ⟨A, hA, hAcard⟩ have h := hA.lindstrom_bound hN omega /-! ## Singer's Construction -/ /-! Port of the Singer construction from Erdos30/{Singer, SingerBridge, SingerSidon, SingerTheorem}.lean (Hulak-Ramos-de Queiroz, arXiv:2605.03274), adapted from Mathlib v4.29.0 to v4.30.0-rc2 and renamespaced into `Semantics.SidonSets.Singer`. -/ namespace Singer set_option maxHeartbeats 8000000 set_option linter.unusedSimpArgs false open Module Submodule Polynomial LinearMap variable (p : Nat) [hp : Fact (Nat.Prime p)] /-! ### Dimension facts (Erdos30/Singer.lean) -/ theorem finrank_ext : finrank (ZMod p) (GaloisField p 3) = 3 := @GaloisField.finrank p hp 3 (by norm_num) theorem trace_surjective : Function.Surjective (Algebra.trace (ZMod p) (GaloisField p 3)) := Algebra.trace_surjective (ZMod p) (GaloisField p 3) /-- ker(Tr) has dimension 2 (rank-nullity). -/ theorem finrank_ker_trace : finrank (ZMod p) (Algebra.trace (ZMod p) (GaloisField p 3)).ker = 2 := by have h_rn := LinearMap.finrank_range_add_finrank_ker (Algebra.trace (ZMod p) (GaloisField p 3)) rw [@GaloisField.finrank p hp 3 (by norm_num)] at h_rn have htop : (Algebra.trace (ZMod p) (GaloisField p 3)).range = ⊤ := LinearMap.range_eq_top_of_surjective _ (trace_surjective p) rw [show finrank (ZMod p) ↥(Algebra.trace (ZMod p) (GaloisField p 3)).range = finrank (ZMod p) (ZMod p) from by rw [htop]; exact finrank_top (ZMod p) (ZMod p), finrank_self] at h_rn omega /-! ### Minimal polynomial and linear independence -/ theorem minpoly_degree_eq_three (α : GaloisField p 3) (hα : α ∉ Set.range (algebraMap (ZMod p) (GaloisField p 3))) : (minpoly (ZMod p) α).natDegree = 3 := by have hint : IsIntegral (ZMod p) α := Algebra.IsIntegral.isIntegral α have hdvd : (minpoly (ZMod p) α).natDegree ∣ 3 := by have h := minpoly.degree_dvd hint rwa [@GaloisField.finrank p hp 3 (by norm_num)] at h have hne1 : (minpoly (ZMod p) α).natDegree ≠ 1 := by intro h1 exact hα (IntermediateField.mem_bot.mp (by rw [← IntermediateField.finrank_eq_one_iff.mp (by rw [IntermediateField.adjoin.finrank hint]; exact h1)] exact IntermediateField.subset_adjoin (ZMod p) {α} (Set.mem_singleton α))) exact (Nat.Prime.eq_one_or_self_of_dvd (by decide) _ hdvd).resolve_left hne1 /-- {α^0·v, α^1·v, α^2·v} are GF(p)-linearly independent when α ∉ GF(p) and v ≠ 0. -/ theorem linIndep_smul_v (α v : GaloisField p 3) (hα : α ∉ Set.range (algebraMap (ZMod p) (GaloisField p 3))) (hv : v ≠ 0) : LinearIndependent (ZMod p) (fun i : Fin 3 => α ^ (i : Nat) * v) := by rw [Fintype.linearIndependent_iff] intro g hg have hfactor : (∑ i : Fin 3, g i • α ^ (i : Nat)) * v = 0 := by have heq : ∑ i : Fin 3, g i • (α ^ (i : Nat) * v) = (∑ i : Fin 3, g i • α ^ (i : Nat)) * v := by simp [Finset.sum_mul, Algebra.smul_mul_assoc] rw [← heq]; exact hg have hsum : ∑ i : Fin 3, g i • α ^ (i : Nat) = 0 := (mul_eq_zero.mp hfactor).resolve_right hv have hdeg := minpoly_degree_eq_three p α hα have hli := @linearIndependent_pow _ _ (ZMod p) _ _ α rw [Fintype.linearIndependent_iff] at hli intro i have hsum_t : ∑ j : Fin (minpoly (ZMod p) α).natDegree, (g ∘ Fin.cast hdeg) j • α ^ (j : Nat) = 0 := by convert hsum using 1 exact Fintype.sum_equiv (Fin.castOrderIso hdeg).toEquiv _ _ (fun j => by simp [Function.comp, Fin.castOrderIso, Fin.cast]) have h := hli _ hsum_t (Fin.cast hdeg.symm i) simp [Function.comp, Fin.cast] at h; exact h /-! ### No proper invariant subspace -/ /-- Multiplication by α ∉ GF(p) has no proper invariant subspace in GF(p³)/GF(p). -/ theorem no_proper_invariant_subspace (α : GaloisField p 3) (hα : α ∉ Set.range (algebraMap (ZMod p) (GaloisField p 3))) (V : Submodule (ZMod p) (GaloisField p 3)) (hVbot : V ≠ ⊥) (hVtop : V ≠ ⊤) (hinv : ∀ v : GaloisField p 3, v ∈ V → α • v ∈ V) : False := by have hinv_pow : ∀ (n : Nat) (v : GaloisField p 3), v ∈ V → α ^ n • v ∈ V := by intro n; induction n with | zero => intro v hv; simpa using hv | succ n ih => intro v hv; have h := ih _ (hinv v hv); rwa [← mul_smul, ← pow_succ] at h obtain ⟨v, hv_mem, hv_ne⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hVbot have hVlt : finrank (ZMod p) V < 3 := by have := finrank_lt_finrank_of_lt (lt_top_iff_ne_top.mpr hVtop) rw [finrank_top, @GaloisField.finrank p hp 3 (by norm_num)] at this; exact this have hmem : ∀ i : Fin 3, α ^ (i : Nat) * v ∈ V := fun i => by have h := hinv_pow i v hv_mem; rwa [Algebra.smul_def] at h have hli : LinearIndependent (ZMod p) (fun i : Fin 3 => α ^ (i : Nat) * v) := linIndep_smul_v p α v hα hv_ne have hli_V : LinearIndependent (ZMod p) (fun i : Fin 3 => (⟨α ^ (i : Nat) * v, hmem i⟩ : V)) := by rw [Fintype.linearIndependent_iff]; intro g hg rw [Fintype.linearIndependent_iff] at hli apply hli g have := congr_arg Subtype.val hg simpa using this exact absurd hVlt (not_lt.mpr (le_of_eq (Fintype.card_fin 3).symm |>.trans hli_V.fintype_card_le_finrank)) /-! ### Intersection dimension -/ /-- Two distinct 2-dim subspaces of GF(p³)/GF(p) intersect in dimension 1. -/ theorem finrank_inf_of_distinct_twodim (V W : Submodule (ZMod p) (GaloisField p 3)) (hV : finrank (ZMod p) V = 2) (hW : finrank (ZMod p) W = 2) (hne : V ≠ W) : finrank (ZMod p) ↥(V ⊓ W) = 1 := by have hgrass := Submodule.finrank_sup_add_finrank_inf_eq V W have h_sup_le : finrank (ZMod p) ↥(V ⊔ W) <= 3 := by have := Submodule.finrank_le (V ⊔ W) rw [@GaloisField.finrank p hp 3 (by norm_num)] at this; exact this have hV_lt_sup : V < V ⊔ W := lt_of_le_of_ne le_sup_left (fun heq => hne (eq_of_le_of_finrank_le (heq ▸ le_sup_right) (by omega)).symm) have h_sup_gt : 2 < finrank (ZMod p) ↥(V ⊔ W) := by have := finrank_lt_finrank_of_lt hV_lt_sup; rw [hV] at this; exact this rw [hV, hW] at hgrass; omega /-! ### Multiplication linear equivalence (Erdos30/SingerBridge.lean) -/ noncomputable instance instFintypeGF3 : Fintype (GaloisField p 3) := Fintype.ofFinite _ noncomputable instance instFintypeGF3units : Fintype (GaloisField p 3)ˣ := Fintype.ofFinite _ noncomputable instance instFintypeZModUnits : Fintype (ZMod p)ˣ := Fintype.ofFinite _ /-- Multiplication by a nonzero element is a GF(p)-linear automorphism. -/ noncomputable def mulLinearEquiv (α : GaloisField p 3) (hα : α ≠ 0) : GaloisField p 3 ≃ₗ[ZMod p] GaloisField p 3 where toFun := fun x => α * x map_add' := mul_add α map_smul' := fun r x => by simp [Algebra.smul_def, mul_left_comm] invFun := fun x => α⁻¹ * x left_inv := fun x => by show α⁻¹ * (α * x) = x; rw [← mul_assoc, inv_mul_cancel₀ hα, one_mul] right_inv := fun x => by show α * (α⁻¹ * x) = x; rw [← mul_assoc, mul_inv_cancel₀ hα, one_mul] /-- The scaled submodule αV = {αv : v ∈ V}. -/ noncomputable def scaledSubmodule (α : GaloisField p 3) (hα : α ≠ 0) (V : Submodule (ZMod p) (GaloisField p 3)) : Submodule (ZMod p) (GaloisField p 3) := V.map (mulLinearEquiv p α hα).toLinearMap lemma mem_scaledSubmodule_iff (α : GaloisField p 3) (hα : α ≠ 0) (V : Submodule (ZMod p) (GaloisField p 3)) (x : GaloisField p 3) : x ∈ scaledSubmodule p α hα V ↔ ∃ v ∈ V, α * v = x := by simp [scaledSubmodule, Submodule.mem_map, mulLinearEquiv] lemma finrank_scaledSubmodule (α : GaloisField p 3) (hα : α ≠ 0) (V : Submodule (ZMod p) (GaloisField p 3)) : finrank (ZMod p) (scaledSubmodule p α hα V) = finrank (ZMod p) V := LinearEquiv.finrank_eq ((mulLinearEquiv p α hα).submoduleMap V |>.symm) /-! ### Trace kernel basic properties -/ private lemma ker_trace_ne_bot : (Algebra.trace (ZMod p) (GaloisField p 3)).ker ≠ ⊥ := fun h => by have := finrank_ker_trace p; rw [h, finrank_bot (R := ZMod p) (M := GaloisField p 3)] at this; omega private lemma ker_trace_ne_top : (Algebra.trace (ZMod p) (GaloisField p 3)).ker ≠ ⊤ := fun h => by have h2 := finrank_ker_trace p have h3 := @GaloisField.finrank p hp 3 (by norm_num) rw [h, finrank_top, h3] at h2; omega /-! ### Non-invariance of trace kernel under non-base multiplication -/ /-- The scaled trace kernel αV ≠ V when α ∉ GF(p). -/ lemma scaledSubmodule_ne_ker_trace (α : GaloisField p 3) (hα_ne : α ≠ 0) (hα : α ∉ Set.range (algebraMap (ZMod p) (GaloisField p 3))) : scaledSubmodule p α hα_ne (Algebra.trace (ZMod p) (GaloisField p 3)).ker ≠ (Algebra.trace (ZMod p) (GaloisField p 3)).ker := by set V := (Algebra.trace (ZMod p) (GaloisField p 3)).ker intro heq have hinv : ∀ v : GaloisField p 3, v ∈ V → α • v ∈ V := by intro v hv have hmem : α * v ∈ scaledSubmodule p α hα_ne V := (mem_scaledSubmodule_iff p α hα_ne V (α * v)).mpr ⟨v, hv, rfl⟩ rw [heq] at hmem rwa [Algebra.smul_def] exact no_proper_invariant_subspace p α hα V (ker_trace_ne_bot p) (ker_trace_ne_top p) hinv /-- α⁻¹ ∉ GF(p) when α ∉ GF(p). -/ lemma inv_not_in_range (α : GaloisField p 3) (_hα_ne : α ≠ 0) (hα : α ∉ Set.range (algebraMap (ZMod p) (GaloisField p 3))) : α⁻¹ ∉ Set.range (algebraMap (ZMod p) (GaloisField p 3)) := by intro ⟨a, ha⟩ apply hα exact ⟨a⁻¹, by rw [map_inv₀, ha, inv_inv]⟩ /-! ### Intersection dimension (geometric core of Sidon proof) -/ /-- When α ∉ GF(p), V ∩ α⁻¹V has dimension 1. This is the key geometric fact for Singer's Sidon argument. -/ theorem finrank_inf_scaled_ker_trace (α : GaloisField p 3) (hα_ne : α ≠ 0) (hα : α ∉ Set.range (algebraMap (ZMod p) (GaloisField p 3))) : finrank (ZMod p) ↥((Algebra.trace (ZMod p) (GaloisField p 3)).ker ⊓ scaledSubmodule p α⁻¹ (inv_ne_zero hα_ne) (Algebra.trace (ZMod p) (GaloisField p 3)).ker) = 1 := by set V := (Algebra.trace (ZMod p) (GaloisField p 3)).ker have hV2 : finrank (ZMod p) V = 2 := finrank_ker_trace p have hαinv_ne := inv_ne_zero hα_ne have hαinv_not_base := inv_not_in_range p α hα_ne hα have hW2 : finrank (ZMod p) (scaledSubmodule p α⁻¹ hαinv_ne V) = 2 := by rw [finrank_scaledSubmodule, hV2] have hne : V ≠ scaledSubmodule p α⁻¹ hαinv_ne V := fun h => scaledSubmodule_ne_ker_trace p α⁻¹ hαinv_ne hαinv_not_base h.symm exact finrank_inf_of_distinct_twodim p V _ hV2 hW2 hne /-! ### Base units subgroup and index -/ /-- GF(p)× embedded in GF(p³)× via algebraMap. -/ noncomputable def baseUnitsSubgroup : Subgroup (GaloisField p 3)ˣ := (Units.map (algebraMap (ZMod p) (GaloisField p 3)).toMonoidHom).range instance : (baseUnitsSubgroup p).Normal := inferInstance private lemma units_map_injective : Function.Injective (Units.map (algebraMap (ZMod p) (GaloisField p 3)).toMonoidHom) := by apply Units.map_injective exact (algebraMap (ZMod p) (GaloisField p 3)).injective lemma baseUnitsSubgroup_card : Nat.card (baseUnitsSubgroup p) = p - 1 := by exact (Nat.card_congr ((Units.map (algebraMap (ZMod p) (GaloisField p 3)).toMonoidHom).ofInjective (units_map_injective p)).toEquiv.symm).trans (by rw [Nat.card_units, Nat.card_zmod]) lemma gf3_units_card : Nat.card (GaloisField p 3)ˣ = p ^ 3 - 1 := by rw [Nat.card_units, GaloisField.card p 3 (by norm_num)] /-- The index [GF(p³)× : GF(p)×] = p²+p+1. -/ lemma baseUnitsSubgroup_index (hp' : Nat.Prime p) : (baseUnitsSubgroup p).index = p ^ 2 + p + 1 := by have hmul := Subgroup.card_mul_index (baseUnitsSubgroup p) rw [baseUnitsSubgroup_card, gf3_units_card] at hmul have hp1 : 0 < p - 1 := Nat.sub_pos_of_lt hp'.one_lt have hfact : p ^ 3 - 1 = (p - 1) * (p ^ 2 + p + 1) := by zify [Nat.one_le_pow 3 p hp'.pos, hp'.pos]; ring rw [hfact] at hmul exact Nat.eq_of_mul_eq_mul_left hp1 hmul /-- Membership characterization: u ∈ baseUnitsSubgroup iff ↑u ∈ range(algebraMap). -/ lemma mem_baseUnitsSubgroup_iff (u : (GaloisField p 3)ˣ) : u ∈ baseUnitsSubgroup p ↔ (↑u : GaloisField p 3) ∈ Set.range (algebraMap (ZMod p) (GaloisField p 3)) := by simp only [baseUnitsSubgroup, MonoidHom.mem_range] constructor · rintro ⟨v, rfl⟩; exact ⟨v.val, by simp [Units.coe_map]⟩ · rintro ⟨a, ha⟩ have ha_ne : a ≠ 0 := by intro h; simp [h] at ha; exact Units.ne_zero u ha.symm exact ⟨Units.mk0 a ha_ne, Units.ext (by simp [Units.coe_map, ha])⟩ /-! ### Quotient Sidon property (Erdos30/SingerSidon.lean) -/ /-- Map a nonzero element of GF(p³) to its class in the quotient group (GaloisField p 3)ˣ / baseUnitsSubgroup p. -/ noncomputable def singerMk (x : GaloisField p 3) (hx : x ≠ 0) : (GaloisField p 3)ˣ ⧸ baseUnitsSubgroup p := QuotientGroup.mk (Units.mk0 x hx) lemma singerMk_eq_iff (a b : GaloisField p 3) (ha : a ≠ 0) (hb : b ≠ 0) : singerMk p a ha = singerMk p b hb ↔ a⁻¹ * b ∈ Set.range (algebraMap (ZMod p) (GaloisField p 3)) := by unfold singerMk; rw [QuotientGroup.eq, mem_baseUnitsSubgroup_iff] simp [Units.val_inv_eq_inv_val, Units.val_mul, Units.val_mk0] private lemma proportional_of_finrank_one (W : Submodule (ZMod p) (GaloisField p 3)) (hW : finrank (ZMod p) W = 1) (w1 w2 : GaloisField p 3) (hw1 : w1 ∈ W) (hw2 : w2 ∈ W) (hw1_ne : w1 ≠ 0) (hw2_ne : w2 ≠ 0) : ∃ c : ZMod p, c ≠ 0 ∧ w2 = c • w1 := by have hsub : span (ZMod p) {w1} <= W := span_le.mpr (Set.singleton_subset_iff.mpr hw1) have heq' : W = span (ZMod p) ({w1} : Set (GaloisField p 3)) := (eq_of_le_of_finrank_le hsub (by rw [finrank_span_singleton hw1_ne]; omega)).symm have hmem : w2 ∈ span (ZMod p) ({w1} : Set (GaloisField p 3)) := heq' ▸ hw2 rw [mem_span_singleton] at hmem obtain ⟨c, hc⟩ := hmem exact ⟨c, fun h => hw2_ne (by simp [h] at hc; exact hc.symm), hc.symm⟩ /-- **Singer Sidon property in the quotient group.** If u*v = α*(w*x) with u,v,w,x nonzero elements of ker(Tr) and α ∈ (ZMod p)×, then in the quotient (GaloisField p 3)ˣ / (ZMod p)ˣ we have either mk u = mk w ∧ mk v = mk x, or mk u = mk x ∧ mk v = mk w. -/ theorem singer_quotient_sidon (u v w x : GaloisField p 3) (hu : u ∈ (Algebra.trace (ZMod p) (GaloisField p 3)).ker) (hv : v ∈ (Algebra.trace (ZMod p) (GaloisField p 3)).ker) (hw : w ∈ (Algebra.trace (ZMod p) (GaloisField p 3)).ker) (hx : x ∈ (Algebra.trace (ZMod p) (GaloisField p 3)).ker) (hu0 : u ≠ 0) (hv0 : v ≠ 0) (hw0 : w ≠ 0) (hx0 : x ≠ 0) (α : ZMod p) (hα : α ≠ 0) (hmul : u * v = (algebraMap (ZMod p) (GaloisField p 3) α) * (w * x)) : (singerMk p u hu0 = singerMk p w hw0 ∧ singerMk p v hv0 = singerMk p x hx0) ∨ (singerMk p u hu0 = singerMk p x hx0 ∧ singerMk p v hv0 = singerMk p w hw0) := by set V := (Algebra.trace (ZMod p) (GaloisField p 3)).ker have hαF_ne : (algebraMap (ZMod p) (GaloisField p 3) α) ≠ 0 := by simp [hα] have hβ_ne : u * w⁻¹ ≠ 0 := mul_ne_zero hu0 (inv_ne_zero hw0) have h_key : (u * w⁻¹) * v = (algebraMap (ZMod p) (GaloisField p 3) α) * x := by have h := hmul; field_simp at h ⊢; linear_combination h by_cases hβ_base : (u * w⁻¹) ∈ Set.range (algebraMap (ZMod p) (GaloisField p 3)) case pos => left; constructor · rw [singerMk_eq_iff]; obtain ⟨c, hc⟩ := hβ_base refine ⟨c⁻¹, ?_⟩ simp only [map_inv₀]; rw [hc]; field_simp · rw [singerMk_eq_iff]; obtain ⟨c, hc⟩ := hβ_base have hcF_ne : (algebraMap (ZMod p) (GaloisField p 3) c) ≠ 0 := fun heq => hβ_ne (by rw [← hc, heq]) refine ⟨α⁻¹ * c, ?_⟩ simp only [map_mul, map_inv₀] have h := h_key; rw [← hc] at h generalize algebraMap (ZMod p) (GaloisField p 3) α = αF at h hαF_ne ⊢ generalize algebraMap (ZMod p) (GaloisField p 3) c = cF at h hcF_ne ⊢ field_simp; linear_combination h case neg => right have h1dim : finrank (ZMod p) ↥(V ⊓ scaledSubmodule p (u * w⁻¹)⁻¹ (inv_ne_zero hβ_ne) V) = 1 := finrank_inf_scaled_ker_trace p (u * w⁻¹) hβ_ne hβ_base have hw_inf : w ∈ V ⊓ scaledSubmodule p (u * w⁻¹)⁻¹ (inv_ne_zero hβ_ne) V := by refine Submodule.mem_inf.mpr ⟨hw, ?_⟩ rw [mem_scaledSubmodule_iff] exact ⟨u, hu, by field_simp⟩ have hv_inf : v ∈ V ⊓ scaledSubmodule p (u * w⁻¹)⁻¹ (inv_ne_zero hβ_ne) V := by refine Submodule.mem_inf.mpr ⟨hv, ?_⟩ rw [mem_scaledSubmodule_iff] refine ⟨(u * w⁻¹) * v, ?_, by field_simp⟩ rw [h_key, show (algebraMap (ZMod p) (GaloisField p 3) α) * x = α • x from (Algebra.smul_def α x).symm] exact V.smul_mem α hx obtain ⟨c, hc_ne, hvc⟩ := proportional_of_finrank_one p _ h1dim w v hw_inf hv_inf hw0 hv0 have hcF_ne : (algebraMap (ZMod p) (GaloisField p 3) c) ≠ 0 := by simp [hc_ne] have hvc' : v = (algebraMap (ZMod p) (GaloisField p 3) c) * w := by rw [hvc, Algebra.smul_def] have hcu : (algebraMap (ZMod p) (GaloisField p 3) c) * u = (algebraMap (ZMod p) (GaloisField p 3) α) * x := by have h := h_key; rw [hvc'] at h generalize algebraMap (ZMod p) (GaloisField p 3) α = αF at h hαF_ne ⊢ generalize algebraMap (ZMod p) (GaloisField p 3) c = cF at h hcF_ne hvc' ⊢ field_simp at h ⊢; linear_combination h constructor · rw [singerMk_eq_iff]; refine ⟨c * α⁻¹, ?_⟩ simp only [map_mul, map_inv₀] generalize algebraMap (ZMod p) (GaloisField p 3) α = αF at hαF_ne hcu ⊢ generalize algebraMap (ZMod p) (GaloisField p 3) c = cF at hcF_ne hcu ⊢ field_simp; linear_combination hcu · rw [singerMk_eq_iff]; refine ⟨c⁻¹, ?_⟩ simp only [map_inv₀] rw [hvc'] generalize algebraMap (ZMod p) (GaloisField p 3) c = cF at hcF_ne ⊢ field_simp /-! ### Combinatorial bridge (Erdos30/SingerTheorem.lean) -/ noncomputable section private abbrev V' := (Algebra.trace (ZMod p) (GaloisField p 3)).ker private abbrev Q' := (GaloisField p 3)ˣ ⧸ baseUnitsSubgroup p private def kerBasis' := (Module.finBasis (ZMod p) ↥(V' p)).reindex ((Fin.castOrderIso (finrank_ker_trace p)).toEquiv) private def repV (i : Option (ZMod p)) : V' p := match i with | none => (kerBasis' p) ⟨0, by omega⟩ | some c => (kerBasis' p) ⟨1, by omega⟩ + c • (kerBasis' p) ⟨0, by omega⟩ private def rep (i : Option (ZMod p)) : GaloisField p 3 := (repV p i).val private lemma rep_mem (i : Option (ZMod p)) : rep p i ∈ (Algebra.trace (ZMod p) (GaloisField p 3)).ker := (repV p i).2 private lemma rep_ne_zero (i : Option (ZMod p)) : rep p i ≠ 0 := by intro h; have hV : repV p i = 0 := Subtype.ext h cases i with | none => exact (kerBasis' p).ne_zero ⟨0, by omega⟩ hV | some c => have heq := congr_arg (kerBasis' p).repr hV simp only [repV, map_add, map_smul, (kerBasis' p).repr_self, map_zero] at heq have h1 := DFunLike.congr_fun heq ⟨1, by omega⟩ simp only [Finsupp.add_apply, Finsupp.smul_apply, Finsupp.single_apply, smul_eq_mul, Finsupp.zero_apply, show (⟨1, by omega⟩ : Fin 2) = (⟨1, by omega⟩ : Fin 2) from rfl, show ((⟨0, by omega⟩ : Fin 2) = (⟨1, by omega⟩ : Fin 2)) = False from by simp [Fin.ext_iff], ite_true, ite_false, mul_zero, add_zero] at h1 exact one_ne_zero h1 private lemma rep_proportional_imp_eq (i j : Option (ZMod p)) (α : ZMod p) (hprop : repV p j = α • repV p i) : i = j := by have heq := congr_arg (kerBasis' p).repr hprop cases i with | none => cases j with | none => rfl | some c => simp only [repV, map_add, map_smul, (kerBasis' p).repr_self] at heq have h1 := DFunLike.congr_fun heq ⟨1, by omega⟩ simp only [Finsupp.add_apply, Finsupp.smul_apply, Finsupp.single_apply, smul_eq_mul, show (⟨1, by omega⟩ : Fin 2) = (⟨1, by omega⟩ : Fin 2) from rfl, show ((⟨0, by omega⟩ : Fin 2) = (⟨1, by omega⟩ : Fin 2)) = False from by simp [Fin.ext_iff], ite_true, ite_false, mul_zero, add_zero, mul_one] at h1 exact absurd h1 one_ne_zero | some a => cases j with | none => simp only [repV, map_add, map_smul, (kerBasis' p).repr_self] at heq have h1 := DFunLike.congr_fun heq ⟨1, by omega⟩ simp only [Finsupp.add_apply, Finsupp.smul_apply, Finsupp.single_apply, smul_eq_mul, show (⟨1, by omega⟩ : Fin 2) = (⟨1, by omega⟩ : Fin 2) from rfl, show ((⟨0, by omega⟩ : Fin 2) = (⟨1, by omega⟩ : Fin 2)) = False from by simp [Fin.ext_iff], ite_true, ite_false, mul_zero, add_zero, mul_one] at h1 exfalso; exact rep_ne_zero p none (show rep p none = 0 from by show (repV p none).val = 0 have := hprop; rw [show α = 0 from h1.symm, zero_smul] at this exact congrArg Subtype.val this) | some b => simp only [repV, map_add, map_smul, (kerBasis' p).repr_self] at heq have h1 := DFunLike.congr_fun heq ⟨1, by omega⟩ have h0 := DFunLike.congr_fun heq ⟨0, by omega⟩ simp only [Finsupp.add_apply, Finsupp.smul_apply, Finsupp.single_apply, smul_eq_mul, show (⟨1, by omega⟩ : Fin 2) = (⟨1, by omega⟩ : Fin 2) from rfl, show ((⟨0, by omega⟩ : Fin 2) = (⟨1, by omega⟩ : Fin 2)) = False from by simp [Fin.ext_iff], show (⟨0, by omega⟩ : Fin 2) = (⟨0, by omega⟩ : Fin 2) from rfl, show ((⟨1, by omega⟩ : Fin 2) = (⟨0, by omega⟩ : Fin 2)) = False from by simp [Fin.ext_iff], ite_true, ite_false, mul_zero, add_zero, mul_one, zero_add] at h1 h0 congr 1; rw [← h1, one_mul] at h0; exact h0.symm private lemma singerMk_rep_injective : Function.Injective (fun i => singerMk p (rep p i) (rep_ne_zero p i)) := by intro i j hij rw [singerMk_eq_iff] at hij obtain ⟨α, hα⟩ := hij have hri := rep_ne_zero p i have hprop_field : rep p j = (algebraMap (ZMod p) (GaloisField p 3) α) * rep p i := by have h1 : (rep p i) * ((rep p i)⁻¹ * rep p j) = rep p j := by rw [← mul_assoc, mul_inv_cancel₀ hri, one_mul] rw [← h1, hα]; ring have hV : repV p j = α • repV p i := by apply Subtype.ext change rep p j = (α • repV p i).val rw [show (α • repV p i).val = α • (repV p i).val from rfl] rw [show α • (repV p i).val = (algebraMap (ZMod p) (GaloisField p 3) α) * (repV p i).val from Algebra.smul_def α _] exact hprop_field exact rep_proportional_imp_eq p i j α hV /-! ### Cyclic group isomorphism -/ private lemma Q_card_eq (hp' : Nat.Prime p) : Nat.card (Q' p) = p ^ 2 + p + 1 := by rw [show Nat.card (Q' p) = (baseUnitsSubgroup p).index from (Subgroup.index_eq_card _).symm] exact baseUnitsSubgroup_index p hp' private noncomputable def mulEquivQ (hp' : Nat.Prime p) : Multiplicative (ZMod (p ^ 2 + p + 1)) ≃* Q' p := by haveI : NeZero (p ^ 2 + p + 1) := ⟨by omega⟩ haveI : IsCyclic (Q' p) := isCyclic_of_surjective (QuotientGroup.mk' (baseUnitsSubgroup p)) (QuotientGroup.mk'_surjective _) let g := Classical.choose (IsCyclic.exists_generator (α := Q' p)) have hg : ∀ x : Q' p, x ∈ Subgroup.zpowers g := Classical.choose_spec (IsCyclic.exists_generator (α := Q' p)) have htop : Subgroup.zpowers g = ⊤ := by ext x; exact ⟨fun _ => trivial, fun _ => hg x⟩ have hord : orderOf g = p ^ 2 + p + 1 := by have h1 : Nat.card ↥(Subgroup.zpowers g) = orderOf g := Nat.card_zpowers g have h2 : Nat.card ↥(Subgroup.zpowers g) = Nat.card (Q' p) := by rw [htop]; exact Nat.card_congr Subgroup.topEquiv.toEquiv have := Q_card_eq p hp'; omega let φ : Multiplicative (ZMod (p ^ 2 + p + 1)) →* Q' p := MonoidHom.mk' (fun k => g ^ (ZMod.val (Multiplicative.toAdd k))) (fun a b => by show g ^ ZMod.val (Multiplicative.toAdd a + Multiplicative.toAdd b) = g ^ ZMod.val (Multiplicative.toAdd a) * g ^ ZMod.val (Multiplicative.toAdd b) rw [← pow_add, pow_eq_pow_iff_modEq, hord] unfold Nat.ModEq; rw [ZMod.val_add] exact Nat.mod_mod_of_dvd _ (dvd_refl _)) have hφ_apply : ∀ k, φ k = g ^ (ZMod.val (Multiplicative.toAdd k)) := fun _ => rfl exact MulEquiv.ofBijective φ ⟨by intro a b hab have hab' : g ^ (ZMod.val (Multiplicative.toAdd a)) = g ^ (ZMod.val (Multiplicative.toAdd b)) := by rw [← hφ_apply, ← hφ_apply]; exact hab have hinj := @pow_injOn_Iio_orderOf (Q' p) _ g have ha : ZMod.val (Multiplicative.toAdd a) ∈ Set.Iio (orderOf g) := by rw [Set.mem_Iio, hord]; exact ZMod.val_lt _ have hb : ZMod.val (Multiplicative.toAdd b) ∈ Set.Iio (orderOf g) := by rw [Set.mem_Iio, hord]; exact ZMod.val_lt _ cases a; cases b; exact congrArg _ (ZMod.val_injective _ (hinj ha hb hab')), by intro x obtain ⟨m, hm⟩ := (hg x : ∃ m : Z, g ^ m = x) have hpos : (0 : Z) < ((p ^ 2 + p + 1 : Nat) : Z) := by positivity have hmod_nn : 0 <= m % ((p ^ 2 + p + 1 : Nat) : Z) := Int.emod_nonneg _ (by linarith) have hmod_lt : (m % ((p ^ 2 + p + 1 : Nat) : Z)).toNat < p ^ 2 + p + 1 := by have h := Int.emod_lt_of_pos m hpos have h_nonneg := Int.emod_nonneg m (by linarith : ((p ^ 2 + p + 1 : Nat) : Z) ≠ 0) rw [Int.toNat_lt] <;> try linarith let k : Multiplicative (ZMod (p ^ 2 + p + 1)) := Multiplicative.ofAdd ((m % ((p ^ 2 + p + 1 : Nat) : Z)).toNat : ZMod (p ^ 2 + p + 1)) refine ⟨k, ?_⟩ have hφk : φ k = g ^ (m % ((p ^ 2 + p + 1 : Nat) : Z)).toNat := by rw [hφ_apply]; congr 1; exact ZMod.val_natCast_of_lt hmod_lt have key : g ^ ((m % ((p ^ 2 + p + 1 : Nat) : Z)).toNat : Z) = g ^ m := by rw [zpow_eq_zpow_iff_modEq, hord] change ((m % ((p ^ 2 + p + 1 : Nat) : Z)).toNat : Z) % ((p ^ 2 + p + 1 : Nat) : Z) = m % ((p ^ 2 + p + 1 : Nat) : Z) rw [Int.toNat_of_nonneg hmod_nn, Int.emod_emod_of_dvd _ dvd_rfl] calc φ k = g ^ (m % ((p ^ 2 + p + 1 : Nat) : Z)).toNat := hφk _ = g ^ ((m % ((p ^ 2 + p + 1 : Nat) : Z)).toNat : Z) := (zpow_natCast g _).symm _ = g ^ m := key _ = x := hm⟩ /-! ### Finset construction and IsSidonMod proof -/ set_option maxHeartbeats 200000000 in /-- The Singer Sidon set: a Finset Z of size p+1 that is IsSidonMod (p²+p+1). -/ theorem singer_sidon_set_of (hp' : Nat.Prime p) : ∃ S : Finset Z, IsSidonMod (↑p * ↑p + ↑p + 1 : Z) S ∧ S.card = p + 1 := by haveI : NeZero (p ^ 2 + p + 1) := ⟨by omega⟩ -- Cyclic isomorphism let φ := mulEquivQ p hp' -- Map each representative to its ZMod coordinate via φ⁻¹ let f : Option (ZMod p) → Z := fun i => ↑(ZMod.val (Multiplicative.toAdd (φ.symm (singerMk p (rep p i) (rep_ne_zero p i))))) let S : Finset Z := Finset.univ.image f refine ⟨S, ?_, ?_⟩ · -- IsSidonMod intro a b c d ha hb hc hd hdvd -- a, b, c, d ∈ S = image of f rw [Finset.mem_image] at ha hb hc hd obtain ⟨ia, _, rfl⟩ := ha; obtain ⟨ib, _, rfl⟩ := hb obtain ⟨ic, _, rfl⟩ := hc; obtain ⟨id, _, rfl⟩ := hd -- Abbreviations for the four quotient elements set qa := singerMk p (rep p ia) (rep_ne_zero p ia) set qb := singerMk p (rep p ib) (rep_ne_zero p ib) set qc := singerMk p (rep p ic) (rep_ne_zero p ic) set qd := singerMk p (rep p id) (rep_ne_zero p id) -- Step 1: divisibility → ZMod equality have hzmod : Multiplicative.toAdd (φ.symm qa) + Multiplicative.toAdd (φ.symm qb) = Multiplicative.toAdd (φ.symm qc) + Multiplicative.toAdd (φ.symm qd) := by have h0 : ((((ZMod.val (Multiplicative.toAdd (φ.symm qa)) : Z) + (ZMod.val (Multiplicative.toAdd (φ.symm qb)) : Z)) - ((ZMod.val (Multiplicative.toAdd (φ.symm qc)) : Z) + (ZMod.val (Multiplicative.toAdd (φ.symm qd)) : Z)) : Z) : ZMod (p ^ 2 + p + 1)) = 0 := by rw [ZMod.intCast_zmod_eq_zero_iff_dvd] convert hdvd using 1 push_cast; ring simp only [Int.cast_sub, Int.cast_add, Int.cast_natCast, ZMod.natCast_zmod_val] at h0 exact sub_eq_zero.mp h0 -- Step 2: ZMod equality → Multiplicative equality → Q' product equality have hQ : qa * qb = qc * qd := by have hmult : φ.symm qa * φ.symm qb = φ.symm qc * φ.symm qd := by show Multiplicative.ofAdd (Multiplicative.toAdd (φ.symm qa) + Multiplicative.toAdd (φ.symm qb)) = Multiplicative.ofAdd (Multiplicative.toAdd (φ.symm qc) + Multiplicative.toAdd (φ.symm qd)) exact congrArg _ hzmod have hφ := congrArg φ hmult simp only [map_mul, MulEquiv.apply_symm_apply] at hφ exact hφ -- Step 3: Products become singerMk of field products have hmul_l : qa * qb = singerMk p (rep p ia * rep p ib) (mul_ne_zero (rep_ne_zero p ia) (rep_ne_zero p ib)) := by show QuotientGroup.mk (Units.mk0 _ _) * QuotientGroup.mk (Units.mk0 _ _) = QuotientGroup.mk (Units.mk0 _ _) rw [← QuotientGroup.mk_mul]; congr 1; ext; rfl have hmul_r : qc * qd = singerMk p (rep p ic * rep p id) (mul_ne_zero (rep_ne_zero p ic) (rep_ne_zero p id)) := by show QuotientGroup.mk (Units.mk0 _ _) * QuotientGroup.mk (Units.mk0 _ _) = QuotientGroup.mk (Units.mk0 _ _) rw [← QuotientGroup.mk_mul]; congr 1; ext; rfl -- Step 4: singerMk equality → algebraMap factor via singerMk_eq_iff rw [hmul_l, hmul_r] at hQ rw [singerMk_eq_iff] at hQ obtain ⟨α, hα⟩ := hQ have hab_ne : rep p ia * rep p ib ≠ 0 := mul_ne_zero (rep_ne_zero p ia) (rep_ne_zero p ib) have hcd_ne : rep p ic * rep p id ≠ 0 := mul_ne_zero (rep_ne_zero p ic) (rep_ne_zero p id) have hα_ne : α ≠ 0 := by intro h0; rw [h0, map_zero] at hα exact mul_ne_zero (inv_ne_zero hab_ne) hcd_ne hα.symm have hcd_eq : rep p ic * rep p id = (algebraMap (ZMod p) (GaloisField p 3)) α * (rep p ia * rep p ib) := by calc rep p ic * rep p id = (rep p ia * rep p ib) * ((rep p ia * rep p ib)⁻¹ * (rep p ic * rep p id)) := by rw [← mul_assoc, mul_inv_cancel₀ hab_ne, one_mul] _ = (rep p ia * rep p ib) * (algebraMap (ZMod p) (GaloisField p 3)) α := by rw [hα] _ = (algebraMap (ZMod p) (GaloisField p 3)) α * (rep p ia * rep p ib) := mul_comm _ _ -- Step 5: Apply singer_quotient_sidon have hsq := singer_quotient_sidon p (rep p ic) (rep p id) (rep p ia) (rep p ib) (rep_mem p ic) (rep_mem p id) (rep_mem p ia) (rep_mem p ib) (rep_ne_zero p ic) (rep_ne_zero p id) (rep_ne_zero p ia) (rep_ne_zero p ib) α hα_ne hcd_eq -- Step 6: From singerMk equality to index equality via injectivity cases hsq with | inl h => left; constructor · exact congrArg f (singerMk_rep_injective p h.1.symm) · exact congrArg f (singerMk_rep_injective p h.2.symm) | inr h => right; constructor · exact congrArg f (singerMk_rep_injective p h.2.symm) · exact congrArg f (singerMk_rep_injective p h.1.symm) · -- card S = p + 1 rw [Finset.card_image_of_injective _ (by intro i j hij -- f(i) = f(j) means val(toAdd(φ⁻¹(singerMk(rep i)))) = val(toAdd(φ⁻¹(singerMk(rep j)))) -- nat->int cast is injective, val is injective, toAdd is bijective, φ⁻¹ is bijective -- So singerMk(rep i) = singerMk(rep j), hence i = j by singerMk_rep_injective have h1 : (ZMod.val (Multiplicative.toAdd (φ.symm (singerMk p (rep p i) (rep_ne_zero p i)))) : Z) = ↑(ZMod.val (Multiplicative.toAdd (φ.symm (singerMk p (rep p j) (rep_ne_zero p j))))) := hij have h2 := Nat.cast_injective h1 have h3 := ZMod.val_injective _ h2 -- h3 : toAdd(φ⁻¹(singerMk(rep i))) = toAdd(φ⁻¹(singerMk(rep j))) have h4 : φ.symm (singerMk p (rep p i) (rep_ne_zero p i)) = φ.symm (singerMk p (rep p j) (rep_ne_zero p j)) := Multiplicative.toAdd.injective h3 have h5 := φ.symm.injective h4 exact singerMk_rep_injective p h5)] simp [Finset.card_univ, Fintype.card_option, ZMod.card] end end Singer /-- **Singer's theorem.** For each prime p, there ∃ a Sidon set modulo p² + p + 1 of cardinality p + 1. This is the classical algebraic construction using the trace kernel of GF(p³)/GF(p). The proof proceeds through: 1. Construction of GF(p) and its degree-3 extension GF(p³) 2. Analysis of ker(Tr) as a 2-dimensional subspace 3. Geometric argument via subspace intersections 4. Transfer from quotient multiplication to modular integer addition Reference: Singer, J. (1938). A theorem in finite projective geometry and some applications. *Trans. Amer. Math. Soc.*, 43, 377-385. -/ theorem singer_sidon_set (p : Nat) (hp : Nat.Prime p) : ∃ S : Finset Z, IsSidonMod (↑p * ↑p + ↑p + 1 : Z) S ∧ S.card = p + 1 := by haveI : Fact (Nat.Prime p) := ⟨hp⟩ exact Singer.singer_sidon_set_of p hp /-- The Singer family hypothesis: for every prime p, there ∃ a Sidon set mod (p²+p+1) of size p+1. -/ def SingerFamilyHypothesis : Prop := ∀ p : Nat, Nat.Prime p → ∃ S : Finset Z, IsSidonMod (↑p * ↑p + ↑p + 1 : Z) S ∧ S.card = p + 1 /-- Singer's theorem establishes the Singer family hypothesis. -/ theorem singerFamilyHypothesis_holds : SingerFamilyHypothesis := fun p hp => singer_sidon_set p hp /-! ## Unconditional h(N) = Θ(√N) Bounds -/ /-- Bounded-lift lemma: an IsSidonMod M set whose elements all lie in [0, M-1] is automatically an IsSidon set in Z (no wraparound can occur). Proof: If a+b = c+d + M, then a+b ≡ c+d (mod M), so IsSidonMod gives {a,b} = {c,d}. But then a+b = a+b + M => M = 0 — contradiction. Therefore a+b = c+d in Z, which is the Sidon property. -/ theorem IsSidonMod.isSidon_of_bounded {M : Z} {S : Finset Z} (hS : IsSidonMod M S) (h_bound : ∀ x ∈ S, 0 <= x ∧ x < M) : IsSidon S := by intro a b c d ha hb hc hd hsum have ha_bound := h_bound a ha; have hb_bound := h_bound b hb have hc_bound := h_bound c hc; have hd_bound := h_bound d hd have ha_nonneg : 0 <= a := ha_bound.1; have ha_lt : a < M := ha_bound.2 have hb_nonneg : 0 <= b := hb_bound.1; have hb_lt : b < M := hb_bound.2 have hc_nonneg : 0 <= c := hc_bound.1; have hc_lt : c < M := hc_bound.2 have hd_nonneg : 0 <= d := hd_bound.1; have hd_lt : d < M := hd_bound.2 -- From IsSidonMod, a+b ≡ c+d (mod M) have hmod : M ∣ (a + b) - (c + d) := by -- hsum states a + b = c + d in Z, so (a+b) - (c+d) = 0 which is divisible by M rw [hsum, sub_self] exact dvd_zero M -- If a+b = c+d, Sidon property follows directly rcases hS ha hb hc hd hmod with (⟨hac, hbd⟩ | ⟨had, hbc⟩) · left; exact ⟨hac, hbd⟩ · right; exact ⟨had, hbc⟩ /-- The Sidon maximum is positive for N >= 1. -/ theorem sidonMaximum_pos (N : Nat) (hN : 1 <= N) : 1 <= sidonMaximum N := by have hmax := sidonMaximum_isSidonMaximum N have hSidon : IsSidon ({1} : Finset Z) := by intro a b c d ha hb hc hd _; simp at ha hb hc hd left; exact ⟨ha ▸ hc.symm, hb ▸ hd.symm⟩ have h1 : IsIntervalSidon (N : Z) ({1} : Finset Z) := by constructor · intro x hx; simp at hx; subst hx; exact ⟨le_refl 1, by exact_mod_cast hN⟩ · exact hSidon have hle := hmax.2 h1; simp at hle; exact hle /-- The Sidon maximum function is monotone non-decreasing. -/ theorem sidonMaximum_mono {N M : Nat} (hNM : N <= M) : sidonMaximum N <= sidonMaximum M := by have hmax_N := sidonMaximum_isSidonMaximum N have hmax_M := sidonMaximum_isSidonMaximum M rcases hmax_N.1 with ⟨A, hA, hAcard⟩ have hA_M : IsIntervalSidon (M : Z) A := hA.mono (by exact_mod_cast hNM) have hle := hmax_M.2 hA_M; omega /-! ## Erdos Problem 30 Statement -/ /-- The formal Erdos Problem 30 statement: h(N) = √N + O_ε(N^ε) for every ε > 0. -/ def Erdos30Statement : Prop := ∀ ε : Real, 0 < ε → ∃ C : Real, ∃ N0 : Nat, 0 <= C ∧ ∀ {N h : Nat}, N0 <= N → IsSidonMaximum N h → abs ((h : Real) - Real.sqrt (N : Real)) <= C * Real.rpow (N : Real) ε end SilverSight.SidonSets