Formalize paper about Restricted Sums

Stream: general

[Nick_adfor]

The paper, titled “The Polynomial Method and Restricted Sums of Congruence Classes”, is authored by Noga Alon, Melvyn B. Nathanson, and Imre Ruzsa. It was published in the Journal of Number Theory in 1996. It contains Generalization of the Cauchy–Davenport Theorem and Restricted Sums of Distinct Residues. I'm wondering if trying to formalize the theorem in this paper is beneficial to mathlib.

[Yaël Dillies]

Do you have a link to the paper oe a theorem statement, for people on mobile?

[Nick_adfor]

https://web.math.princeton.edu/~nalon/PDFS/anrf3.pdf

[Nick_adfor]

Yaël Dillies said:

Do you have a link to the paper oe a theorem statement, for people on mobile?

The theorem is about addictive number theory. And I'm wondering if the newest mathlib is suitable for the proof.

[Kevin Buzzard]

(additive number theory)

[Sébastien Gouëzel]

addictive number theory is very cute, though :-)

[Ruben Van de Velde]

Isn't that all number theory? :innocent:

[Nick_adfor]

Seems that it is addictive : )

[Nick_adfor]

Our group is investigating how the mathematical concepts from Stanley’s Combinatorial Commutative Algebra will be implemented and verified using Lean’s mathlib library.

[Nick_adfor]

And the paper's technology is introduced in the book.

[Yaël Dillies]

Yep, that's all doable in mathlib with little work. You can look at the formalisation of Schwartz-Zippel in mathlib as an example to follow

[Antoine Chambert-Loir]

Note that the combinatorial nullstellensatz is already there.

[Nick_adfor]

I've reviewed the work in Mathlib on Alon's Combinatorial Nullstellensatz by Antoine Chambert-Loir and the generalization of the Cauchy-Davenport theorem by Yaël Dillies and Bhavik Mehta. It's a pleasure to meet the authors here.

[Nick_adfor]

I may ask what happens to this theorem (generalisation of the Cauchy-Davenport theorem to arbitrary groups).

import Mathlib

open scoped Finset

open scoped Pointwise

variable {G α : Type*}

variable [Group α] [DecidableEq α] {x y : Finset α × Finset α} {s t : Finset α}

/-- A generalization of the Cauchy-Davenport Theorem (Theorem 1.1) to  ZMod p. -/
theorem cauchy_davenport {p : ℕ} (hp : Nat.Prime p)
{s t : Finset (ZMod p)} (hs : s.Nonempty) (ht : t.Nonempty) :
  min p (#s + #t - 1) ≤ #(s + t) := by exact ZMod.cauchy_davenport hp hs ht

[Nick_adfor]

In Alon's article the theorems and lemmas proved this way:

[Nick_adfor]

image.png

[Nick_adfor]

If this generalisation of the Cauchy-Davenport theorem to arbitrary groups contains 2.1 then things will be easier, right :)

[Nick_adfor]

import Mathlib

open Finsupp

open scoped Finset

variable {R : Type*} [CommRing R]

open MvPolynomial

open Finsupp Function

/-- Lemma 2.2 :
A multivariate polynomial that vanishes on a large product finset is the zero polynomial. -/
lemma eq_zero_of_eval_zero_at_prod_finset {σ : Type*} [Finite σ] [IsDomain R]
    (P : MvPolynomial σ R) (S : σ → Finset R)
    (Hdeg : ∀ i, P.degreeOf i < #(S i))
    (Heval : ∀ (x : σ → R), (∀ i, x i ∈ S i) → eval x P = 0) :
    P = 0 := by
      exact MvPolynomial.eq_zero_of_eval_zero_at_prod_finset P S Hdeg Heval

variable {p : ℕ} [Fact (Nat.Prime p)] {k : ℕ}

set_option maxHeartbeats 1000000 in
/-- **Alon-Nathanson-Ruzsa Theorem** (Theorem 2.1)
Proof strategy: Use Lemma 2.2 (eq_zero_of_eval_zero_at_prod_finset) to prove Theorem 2.1

Proof outline:
1. Assume the conclusion is false, i.e., there exists a set E ⊆ Z_p with |E| = m such that ⊕ₕ∑Aᵢ ⊆ E
2. Construct the polynomial Q(x₀,...,xₖ) = h(x₀,...,xₖ) · ∏_{e∈E} (x₀+...+xₖ - e)
   - deg(Q) = deg(h) + m = ∑cᵢ
   - For all (a₀,...,aₖ) ∈ ∏Aᵢ, we have Q(a₀,...,aₖ) = 0
   - The coefficient of monomial ∏xᵢ^{cᵢ} in Q is nonzero

3. For each i, define gᵢ(xᵢ) = ∏_{a∈Aᵢ} (xᵢ - a) = xᵢ^{cᵢ+1} - ∑ⱼ bᵢⱼxᵢʲ
4. Construct polynomial Q̅ by replacing all occurrences of xᵢ^{cᵢ+1} in Q with ∑ⱼ bᵢⱼxᵢʲ
   - For each aᵢ ∈ Aᵢ, gᵢ(aᵢ) = 0, so Q̅ still vanishes on ∏Aᵢ
   - deg_{xᵢ}(Q̅) ≤ cᵢ

5. Apply Lemma 2.2:
   - Q̅ vanishes on ∏Aᵢ
   - Degree in each variable ≤ cᵢ
   - Therefore Q̅ ≡ 0

6. But the coefficient of ∏xᵢ^{cᵢ} in Q̅ is the same as in Q:
   - The replacement process doesn't affect this specific monomial
   - By assumption, this coefficient is nonzero in Q
   - Therefore it's nonzero in Q̅, contradicting Q̅ ≡ 0

Key points:
- Use polynomial replacement technique to reduce degrees to satisfy Lemma 2.2 conditions
- The replacement process preserves the coefficient of the target monomial
- Proof by contradiction
-/
theorem ANR_polynomial_method (h : MvPolynomial (Fin (k + 1)) (ZMod p))
    (A : Fin (k + 1) → Finset (ZMod p))
    (c : Fin (k + 1) → ℕ)
    (hA : ∀ i, (A i).card = c i + 1)
    (m : ℕ) (hm : m = (∑ i, c i) - h.totalDegree)
    (h_coeff : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c)
    ((∑ i : Fin (k + 1), MvPolynomial.X i) ^ m * h) ≠ 0) :
    let S : Finset (ZMod p) :=
      (Fintype.piFinset A).filter (fun f => h.eval f ≠ 0) |>.image (fun f => ∑ i, f i)
    S.card ≥ m + 1 ∧ m < p := by sorry

[Yaël Dillies]

Nick_adfor said:

I may ask what happens to this theorem (generalisation of the Cauchy-Davenport theorem to arbitrary groups).

See https://github.com/YaelDillies/MiscYD/blob/master/MiscYD/AddCombi/Kneser/Kneser.lean

[Nick_adfor]

It's terrible that I may think this lemma I need is wrong (????)

import Mathlib

variable {p : ℕ} [Fact (Nat.Prime p)] {k : ℕ}

open MvPolynomial

lemma Q_total_degree_eq_sum_c (h : MvPolynomial (Fin (k + 1)) (ZMod p))
    (A : Fin (k + 1) → Finset (ZMod p))
    (c : Fin (k + 1) → ℕ)
    (hA : ∀ i, (A i).card = c i + 1)
    (m : ℕ) (hm : m = (∑ i, c i) - h.totalDegree)
    (h_coeff : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c)
              ((∑ i : Fin (k + 1), MvPolynomial.X i) ^ m * h) ≠ 0)
    (E : Multiset (ZMod p)) (hE_card : E.card = m)
    (sumX : MvPolynomial (Fin (k + 1)) (ZMod p))
    (Q : MvPolynomial (Fin (k + 1)) (ZMod p))
    (hsumX_def : sumX = ∑ i, MvPolynomial.X i)
    (hQ_def : Q = h * (E.map (fun e => sumX - C e)).prod) :
    Q.totalDegree = ∑ i, c i := by
  sorry

[Nick_adfor]

Now the whole theorem ANR writes like this. admit for proved and sorry for unfinished (maybe even wrong)

import Mathlib

open Finsupp

open scoped Finset

variable {R : Type*} [CommRing R]

open MvPolynomial

/-- Lemma 2.2 :

A multivariate polynomial that vanishes on a large product finset is the zero polynomial. -/

lemma eq_zero_of_eval_zero_at_prod_finset {σ : Type*} [Finite σ] [IsDomain R]

    (P : MvPolynomial σ R) (S : σ → Finset R)

    (Hdeg : ∀ i, P.degreeOf i < #(S i))

    (Heval : ∀ (x : σ → R), (∀ i, x i ∈ S i) → eval x P = 0) :

    P = 0 := by

      exact MvPolynomial.eq_zero_of_eval_zero_at_prod_finset P S Hdeg Heval

variable {p : ℕ} [Fact (Nat.Prime p)] {k : ℕ}

/-- Definition of elimination polynomials g_i -/

noncomputable def elimination_polynomials (A : Fin (k + 1) → Finset (ZMod p))

    (c : Fin (k + 1) → ℕ) (hA : ∀ i, (A i).card = c i + 1) :

    Fin (k + 1) → MvPolynomial (Fin (k + 1)) (ZMod p) :=

  fun i => ∏ a ∈ A i, (MvPolynomial.X i - C a)

/-- Elimination polynomials vanish on their defining sets -/

lemma elimination_polynomials_vanish (g : Fin (k + 1) → MvPolynomial (Fin (k + 1)) (ZMod p))

    (A : Fin (k + 1) → Finset (ZMod p)) (c : Fin (k + 1) → ℕ) (hA : ∀ i, (A i).card = c i + 1)

    (hg : g = elimination_polynomials A c hA) :

    ∀ (x : Fin (k + 1) → ZMod p) i, x i ∈ A i → eval x (g i) = 0 := by

  intro x i hx

  rw [hg, elimination_polynomials, eval_prod]

  apply Finset.prod_eq_zero hx

  simp

noncomputable def reduce_polynomial_degrees (P : MvPolynomial (Fin (k + 1)) (ZMod p))

    (g : Fin (k + 1) → MvPolynomial (Fin (k + 1)) (ZMod p))

    (c : Fin (k + 1) → ℕ) : MvPolynomial (Fin (k + 1)) (ZMod p) :=

  P.support.sum fun m =>

    let coeff := P.coeff m

    let needs_replacement : Finset (Fin (k + 1)) :=

      Finset.filter (fun i => m i > c i) Finset.univ

    if h : needs_replacement.Nonempty then

      let i : Fin (k + 1) := needs_replacement.min' h

      let new_m : (Fin (k + 1)) →₀ ℕ :=

        Finsupp.update m i (m i - (c i + 1))

      coeff • (MvPolynomial.monomial new_m 1) * g i

    else

      coeff • MvPolynomial.monomial m 1

lemma totalDegree_prod_sumX_minus_eq {m : ℕ} (E : Multiset (ZMod p)) (hE_card : E.card = m) :

    ((E.map (fun e => (∑ i, MvPolynomial.X i : MvPolynomial (Fin (k + 1))

    (ZMod p)) - C e)).prod).totalDegree = m := by admit

lemma totalDegree_le_of_coeff_ne_zero {P : MvPolynomial (Fin (k + 1)) (ZMod p)}

    {d : ℕ} (h : ∃ m, MvPolynomial.coeff m P ≠ 0 ∧ ∑ i, (m i : ℕ) = d) :

    d ≤ P.totalDegree := by

  aesop (config := {warnOnNonterminal := false});

  have h_deg_le_total : ∀ m ∈ P.support, m.sum (fun i e => e) ≤ P.totalDegree := by

    exact fun m hm => Finset.le_sup ( f := fun m : Fin ( k + 1 ) →₀ ℕ => m.sum fun i e => e ) hm;

  simpa [ Finsupp.sum_fintype ] using h_deg_le_total w ( by simpa )

set_option maxHeartbeats 2000000 in

/-- **Alon-Nathanson-Ruzsa Theorem** (Theorem 2.1)

Proof strategy: Use Lemma 2.2 (eq_zero_of_eval_zero_at_prod_finset) to prove Theorem 2.1

Proof outline:

1. Assume the conclusion is false, i.e., there exists a set E ⊆ Z_p with |E| = m such that ⊕ₕ∑Aᵢ ⊆ E

2. Construct the polynomial Q(x₀,...,xₖ) = h(x₀,...,xₖ) · ∏_{e∈E} (x₀+...+xₖ - e)

   - deg(Q) = deg(h) + m = ∑cᵢ

   - For all (a₀,...,aₖ) ∈ ∏Aᵢ, we have Q(a₀,...,aₖ) = 0

   - The coefficient of monomial ∏xᵢ^{cᵢ} in Q is nonzero

3. For each i, define gᵢ(xᵢ) = ∏_{a∈Aᵢ} (xᵢ - a) = xᵢ^{cᵢ+1} - ∑ⱼ bᵢⱼxᵢʲ

4. Construct polynomial Q̅ by replacing all occurrences of xᵢ^{cᵢ+1} in Q with ∑ⱼ bᵢⱼxᵢʲ

   - For each aᵢ ∈ Aᵢ, gᵢ(aᵢ) = 0, so Q̅ still vanishes on ∏Aᵢ

   - deg_{xᵢ}(Q̅) ≤ cᵢ

5. Apply Lemma 2.2:

   - Q̅ vanishes on ∏Aᵢ

   - Degree in each variable ≤ cᵢ

   - Therefore Q̅ ≡ 0

6. But the coefficient of ∏xᵢ^{cᵢ} in Q̅ is the same as in Q:

   - The replacement process doesn't affect this specific monomial

   - By assumption, this coefficient is nonzero in Q

   - Therefore it's nonzero in Q̅, contradicting Q̅ ≡ 0

Key points:
- Use polynomial replacement technique to reduce degrees to satisfy Lemma 2.2 conditions
- The replacement process preserves the coefficient of the target monomial
- Proof by contradiction
-/

theorem ANR_polynomial_method (h : MvPolynomial (Fin (k + 1)) (ZMod p))

    (A : Fin (k + 1) → Finset (ZMod p))

    (c : Fin (k + 1) → ℕ)

    (hA : ∀ i, (A i).card = c i + 1)

    (m : ℕ) (hm : m = (∑ i, c i) - h.totalDegree)

    (h_coeff : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c)

    ((∑ i : Fin (k + 1), MvPolynomial.X i) ^ m * h) ≠ 0) :

    let S : Finset (ZMod p) :=

      (Fintype.piFinset A).filter (fun f => h.eval f ≠ 0) |>.image (fun f => ∑ i, f i)

    S.card ≥ m + 1 ∧ m < p := by

  -- Define the restricted sumset S

  set S : Finset (ZMod p) :=

  ((Fintype.piFinset A).filter (fun f => h.eval f ≠ 0)).image (fun f => ∑ i, f i) with hS_def

  -- Step 1: Prove |S| ≥ m + 1 by contradiction

  have hS_card : S.card ≥ m + 1 := by

    by_contra! H

    have hS_size : S.card ≤ m := by omega

    obtain ⟨E, hE_sub, hE_card⟩ : ∃ E : Multiset (ZMod p), S.val ⊆ E ∧ E.card = m := by

      refine ⟨S.val + Multiset.replicate (m - S.card) (0 : ZMod p),

              Multiset.subset_of_le (by simp), ?_⟩

      simp [hS_size]

    -- Define the polynomial Q

    set sumX : MvPolynomial (Fin (k + 1)) (ZMod p) := ∑ i, MvPolynomial.X i with hsumX_def

    set Q : MvPolynomial (Fin (k + 1)) (ZMod p) :=

      h * (E.map (fun e => sumX - C e)).prod with hQ_def

    -- Q vanishes on ∏Aᵢ

    have hQ_zero : ∀ (x : Fin (k + 1) → ZMod p), (∀ i, x i ∈ A i) → eval x Q = 0 := by admit

    have hQ_total_deg : Q.totalDegree = ∑ i, c i := by

      rw [hQ_def, hsumX_def]

      have hQ_coeff_ne_zero : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c) Q ≠ 0 := by sorry

      have h_ge : (∑ i, c i) ≤ Q.totalDegree :=

        totalDegree_le_of_coeff_ne_zero ⟨Finsupp.equivFunOnFinite.symm c, hQ_coeff_ne_zero, by simp⟩

      have h_le : Q.totalDegree ≤ ∑ i, c i := by

        rw [hQ_def, hsumX_def]

        calc

          (h * (E.map (fun e => (∑ i, MvPolynomial.X i) - C e)).prod).totalDegree

            ≤ h.totalDegree +

            ((E.map (fun e => (∑ i, MvPolynomial.X i) - C e)).prod).totalDegree :=

              totalDegree_mul _ _

          _ = h.totalDegree + m := by rw [totalDegree_prod_sumX_minus_eq E hE_card]

          _ = (∑ i, c i) - m + m := by

            rw [hm]

            subst hE_card

            simp_all [S, sumX, Q]

            rw [Nat.add_comm]

            have sub_add_eq : (∑ i, c i) - h.totalDegree + h.totalDegree = ∑ i, c i := by

              have : h.totalDegree ≤ ∑ i, c i := by

                have : 0 ≤ (∑ i, c i) - h.totalDegree := by omega

                simp

                sorry

              exact Nat.sub_add_cancel this

            rw [sub_add_eq]

          _ = ∑ i, c i := by omega

      subst hE_card

      simp_all [S, sumX, Q]

      omega

    have hQ_coeff : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c) Q ≠ 0 := by

      rw [hQ_def, coeff_mul]

      sorry

    set g : Fin (k + 1) → MvPolynomial (Fin (k + 1)) (ZMod p) :=

      elimination_polynomials A c hA with hg_def

    set Q_bar : MvPolynomial (Fin (k + 1)) (ZMod p) :=

      reduce_polynomial_degrees Q g c with hQ_bar_def

    have hQ_bar_zero : ∀ (x : Fin (k + 1) → ZMod p), (∀ i, x i ∈ A i) → eval x Q_bar = 0 := by

      intro x hx

      sorry

    have hQ_bar_deg : ∀ i, Q_bar.degreeOf i ≤ c i := by

      intro i

      sorry

    have hQ_bar_zero_poly : Q_bar = 0 :=

      _root_.eq_zero_of_eval_zero_at_prod_finset Q_bar A (fun i => by

        have := hQ_bar_deg i

        grind) hQ_bar_zero

    have hQ_bar_coeff : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c) Q_bar ≠ 0 := by

      sorry

    rw [hQ_bar_zero_poly] at hQ_bar_coeff

    simp at hQ_bar_coeff

  -- Step 2: Prove m < p first (this is needed for the main argument)

  have hmp : m < p := by

    by_contra! H  -- H: m ≥ p

    -- If m ≥ p, use the Frobenius endomorphism property in characteristic p

    have frobenius_identity : ((∑ i : Fin (k + 1), MvPolynomial.X i) ^ p :

    MvPolynomial (Fin (k + 1)) (ZMod p)) = ∑ i, MvPolynomial.X i ^ p := by

      subst hm

      simp_all only [ne_eq, ge_iff_le, S]

      exact sum_pow_char p Finset.univ X

    -- This changes the structure of (∑ X_i)^m when m ≥ p, leading to contradiction with h_coeff

    subst hm

    simp_all only [ne_eq, ge_iff_le, S]

    sorry  -- Detailed argument needed here

  exact ⟨hS_card, hmp⟩

[Nick_adfor]

The proof is currently stuck at hQ_total_deg. There's even this absurd situation where I can't prove A ≥ B from A - B ≥ 0.

But looking at it from another angle, the only thing that seems directly usable in hS_card is hQ_bar_coeff (which currently has sorry). Does proving hQ_bar_coeff actually require hQ_total_deg? I'm not sure...

[Aaron Liu]

Nick_adfor said:

There's even this absurd situation where I can't prove A ≥ B from A - B ≥ 0.

Did you try docs#sub_nonneg

[Aaron Liu]

oh are you working with Nats

[Aaron Liu]

If you are then I will tell you the definition of A - B when everything is a Nat is what normal mathematicians would call $\max(A-B,0)$

[Aaron Liu]

so A - B ≥ 0 doesn't actually tell you anything

[Nick_adfor]

Aaron Liu said:

If you are then I will tell you the definition of A - B when everything is a Nat is what normal mathematicians would call $\max(A-B,0)$

Really? I had never considered that. This is an issue that simply doesn't arise in conventional mathematics.

[Nick_adfor]

Nick_adfor said:

The proof is currently stuck at hQ_total_deg. There's even this absurd situation where I can't prove A ≥ B from A - B ≥ 0.

But looking at it from another angle, the only thing that seems directly usable in hS_card is hQ_bar_coeff (which currently has sorry). Does proving hQ_bar_coeff actually require hQ_total_deg? I'm not sure...

As I've said here, does proving hQ_bar_coeff actually require hQ_total_deg? Maybe not......

[Nick_adfor]

article precise.lean
Now the code writes like this.

[Nick_adfor]

The core challenge I'm facing is the difficulty in handling type conversions between ZMod p and ℕ in Lean.

What should be mathematically straightforward - proving that a polynomial coefficient equals zero - becomes surprisingly complex in the formalization. The main issues are:

1. Type coercion hurdles: Simple numeric values like 0 and 1 require explicit type annotations and careful conversion between ℕ and ZMod p
2. Index management complexity: Dealing with indices ranging from 1 to k introduces substantial boilerplate code

[Nick_adfor]

Aaron Liu said:

If you are then I will tell you the definition of A - B when everything is a Nat is what normal mathematicians would call $\max(A-B,0)$

What about equation like A-B

import Mathlib

open Finsupp

open scoped Finset

variable {R : Type*} [CommRing R]

open MvPolynomial

variable {p : ℕ} [Fact (Nat.Prime p)] {k : ℕ}

theorem ANR_polynomial_method (h : MvPolynomial (Fin (k + 1)) (ZMod p))
    (A : Fin (k + 1) → Finset (ZMod p))
    (c : Fin (k + 1) → ℕ)
    (hA : ∀ i, (A i).card = c i + 1)
    (m : ℕ) (hm : m = (∑ i, c i) - h.totalDegree)
    (h_coeff : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c)
    ((∑ i : Fin (k + 1), MvPolynomial.X i) ^ m * h) ≠ 0) :
    let S : Finset (ZMod p) :=
      (Fintype.piFinset A).filter (fun f => h.eval f ≠ 0) |>.image (fun f => ∑ i, f i)
    S.card ≥ m + 1 ∧ m < p := by
        have h_h_deg : h.totalDegree = (∑ i, c i) - m := by
          rw [hm]
          sorry
        sorry

[Nick_adfor]

I should prove **⊢** h.totalDegree ≤ ∑ i, c i (it seems not true!)

[Aaron Liu]

I don't see immediately why this follows

[Aaron Liu]

maybe you want instead (hm : m + h.totalDegree = ∑ i, c i)

[Nick_adfor]

It is from an article that hm writes this way.

[Nick_adfor]

I never think of hm may be not written as m + h.totalDegree = ∑ i, c i.

[Nick_adfor]

Aaron Liu said:

maybe you want instead (hm : m + h.totalDegree = ∑ i, c i)

Genius Aaron!

[Nick_adfor]

I can hardly prove h.totalDegree = (∑ i, c i) - m from m = (∑ i, c i) - h.totalDegree but I can write hm as m + h.totalDegree = ∑ i, c i !!!!!!

[Nick_adfor]

Another terrible one: I cannot prove that the product of m MvPolynomials with degree = 1 are degree = m

: ((((((

import Mathlib

open Finsupp

open scoped Finset

variable {R : Type*} [CommRing R]

open MvPolynomial

variable {p : ℕ} [Fact (Nat.Prime p)] {k : ℕ}

/-- Definition of elimination polynomials g_i -/
noncomputable def elimination_polynomials (A : Fin (k + 1) → Finset (ZMod p)) :
    Fin (k + 1) → MvPolynomial (Fin (k + 1)) (ZMod p) :=
  fun i => ∏ a ∈ A i, (MvPolynomial.X i - C a)

noncomputable def reduce_polynomial_degrees (P : MvPolynomial (Fin (k + 1)) (ZMod p))
    (g : Fin (k + 1) → MvPolynomial (Fin (k + 1)) (ZMod p))
    (c : Fin (k + 1) → ℕ) : MvPolynomial (Fin (k + 1)) (ZMod p) :=

  P.support.sum fun m =>
    let coeff := P.coeff m
    let needs_replacement : Finset (Fin (k + 1)) :=
      Finset.filter (fun i => m i > c i) Finset.univ
    if h : needs_replacement.Nonempty then
      let i : Fin (k + 1) := needs_replacement.min' h
      let new_m : (Fin (k + 1)) →₀ ℕ :=
        Finsupp.update m i (m i - (c i + 1))
      coeff • (MvPolynomial.monomial new_m 1) * g i
    else
      coeff • MvPolynomial.monomial m 1

set_option maxHeartbeats 2000000 in
/-- **Alon-Nathanson-Ruzsa Theorem** (Theorem 2.1)
Proof strategy: Use Lemma 2.2 (eq_zero_of_eval_zero_at_prod_finset) to prove Theorem 2.1

Proof outline:
1. Assume the conclusion is false, i.e., there exists a set E subset Z_p with |E| = m such that restricted sumset subset E
2. Construct the polynomial Q(x_0,...,x_k) = h(x_0,...,x_k) * prod_{e in E} (x_0+...+x_k - e)
   - deg(Q) = deg(h) + m = sum c_i
   - For all (a_0,...,a_k) in prod A_i, we have Q(a_0,...,a_k) = 0
   - The coefficient of monomial prod x_i^{c_i} in Q is nonzero

3. For each i, define g_i(x_i) = prod_{a in A_i} (x_i - a) = x_i^{c_i+1} - sum_j b_ij x_i^j
4. Construct polynomial Q_bar by replacing all occurrences of x_i^{c_i+1} in Q with sum_j b_ij x_i^j
   - For each a_i in A_i, g_i(a_i) = 0, so Q_bar still vanishes on prod A_i
   - deg_{x_i}(Q_bar) <= c_i

5. Apply Lemma 2.2:
   - Q_bar vanishes on prod A_i
   - Degree in each variable <= c_i
   - Therefore Q_bar = 0

6. But the coefficient of prod x_i^{c_i} in Q_bar is the same as in Q:
   - The replacement process doesn't affect this specific monomial
   - By assumption, this coefficient is nonzero in Q
   - Therefore it's nonzero in Q_bar, contradicting Q_bar = 0

Key points:
- Use polynomial replacement technique to reduce degrees to satisfy Lemma 2.2 conditions
- The replacement process preserves the coefficient of the target monomial
- Proof by contradiction
-/
theorem ANR_polynomial_method (h : MvPolynomial (Fin (k + 1)) (ZMod p))
    (A : Fin (k + 1) → Finset (ZMod p))
    (c : Fin (k + 1) → ℕ)
    (hA : ∀ i, (A i).card = c i + 1)
    (m : ℕ) (hm : m + h.totalDegree = ∑ i, c i)
    (h_coeff : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c)
    ((∑ i : Fin (k + 1), MvPolynomial.X i) ^ m * h) ≠ 0) :
    let S : Finset (ZMod p) :=
      (Fintype.piFinset A).filter (fun f => h.eval f ≠ 0) |>.image (fun f => ∑ i, f i)
    S.card ≥ m + 1 ∧ m < p := by
  -- Define the restricted sumset S
  set S : Finset (ZMod p) :=
  ((Fintype.piFinset A).filter (fun f => h.eval f ≠ 0)).image (fun f => ∑ i, f i) with hS_def

  -- Step 1: Prove |S| >= m + 1 by contradiction
  have hS_card : S.card ≥ m + 1 := by
    by_contra! H

    have hS_size : S.card ≤ m := by omega
    obtain ⟨E, hE_sub, hE_card⟩ : ∃ E : Multiset (ZMod p), S.val ⊆ E ∧ E.card = m := by
      refine ⟨S.val + Multiset.replicate (m - S.card) (0 : ZMod p),
              Multiset.subset_of_le (by simp), ?_⟩
      simp [hS_size]

    -- Define the polynomial Q
    set sumX : MvPolynomial (Fin (k + 1)) (ZMod p) := ∑ i, MvPolynomial.X i with hsumX_def
    set Q : MvPolynomial (Fin (k + 1)) (ZMod p) :=
      h * (E.map (fun e => sumX - C e)).prod with hQ_def

    have hQ_total_deg : Q.totalDegree = ∑ i, c i := by
      rw [hQ_def, hsumX_def]
      have h_prod_deg : ((E.map (fun e => sumX - C e)).prod).totalDegree = m := by
        rw [hsumX_def]
        have degree_of_each : ∀ e : ZMod p, (sumX - C e).totalDegree = 1 := by admit
        have h_prod_deg : ((Multiset.map (fun e ↦ ∑ i : Fin (k + 1), X i - C e) E).prod).totalDegree = m := by
          have h1 : ∀ e : ZMod p, (∑ i : Fin (k + 1), X i - C e).totalDegree = 1 := by
            intro e
            simp_all [S, sumX, Q]
          have h2 : (sumX ^ m).totalDegree = m := by
            rw [hsumX_def]
            sorry
          sorry
        exact h_prod_deg
      have h_h_deg : h.totalDegree = (∑ i, c i) - m := by
        exact Nat.eq_sub_of_add_eq' hm
      sorry
    sorry
  sorry

[Nick_adfor]

https://github.com/NickAdfor/The-polynomial-method-and-restricted-sums-of-congruence-classes/blob/main/妈咪河移位.lean

Now I've finished Theorem 2.1

[Nick_adfor]

But I've a question that Theorem 1.1 (C-D Theorem.lean) need to be proved from Theorem 2.1 (妈咪河移位.lean theorem ANR_polynomial_method). How can I import 妈咪河移位.lean in C-D Theorem.lean?

[Nick_adfor]

It's my first time to use GitHub to manage all my packages. I don't know how to make it easy both for me to update and for visitors to check. My some-kind-of-silly workflow is in README.md

[Nick_adfor]

As one can see there's a lot of set_option maxHeartbeats 2000000 in theorem. That is because of aesop are consuming (time-consuming or heartbeat-consuming? I don't know how to name it). I may think that coder should do more than just finish writing the code, some optimation is needed.

[Nick_adfor]

Anyway, the code is now half-finished (at least it can run) with help of Aristotle and tips from Aaron Liu. The proof utilizes a polynomial method approach to prove Cauchy-Davenport Theorem. This work extends the contributions of Antoine Chambert-Loir's Nullstellensatz (Lemma 2.2 in our work). However, the problem regarding restricted sums of distinct residues in Alon's article remains unresolved. Additionally, the application of the Schwartz-Zippel from Yaël Dillies requires further verification. Also, there's a Frobenius way we haven't investigated. Therefore, more work is needed to complete this line of research.