Proof obligation for `Polishchuk_Spielman` in `ArkLib/Data/CodingTheory/PolishchukSpielman.lean`

[alexanderlhicks]

A proof in ArkLib/Data/CodingTheory/PolishchukSpielman.lean contains a sorry.

🤖 AI Analysis:

Statement Explanation

This theorem, a variant of the Polishchuk-Spielman lemma, is a powerful "lifting" result for bivariate polynomials. It states that if a bivariate polynomial g is divisible by another polynomial f "locally" (i.e., when restricted to vertical and horizontal lines on a grid), then under certain degree conditions, g must be divisible by f "globally" (in the ring of bivariate polynomials F[X][Y]).

Hypotheses:

• You are given two bivariate polynomials, f and g, with their degrees in X and Y bounded by (a_x, a_y) and (b_x, b_y) respectively.
• You have two large finite sets of points, P_x and P_y, which form an evaluation grid. Their sizes are at least n_x and n_y.
• For every point y in P_y, the univariate polynomial f(X, y) divides g(X, y). The quotient is quot_X y.
• Similarly, for every x in P_x, the univariate polynomial f(x, Y) divides g(x, Y). The quotient is quot_Y x. (Note: there may be a type error in the provided code, as quot_Y x is given type F[X] but is used as a polynomial in Y).
• A crucial low-degree condition 1 > (b_x : ℚ) / (n_x : ℚ) + (b_y : ℚ) / (n_y : ℚ) holds. This inequality connects the degree of g to the size of the grid, and it's the key to ensuring that a polynomial with "too many" roots must be zero.

Goal:
You need to prove the existence of a single bivariate polynomial q such that:

1. g = q * f.
2. The degrees of q are bounded as expected: degreeX q ≤ b_x - a_x and natDegreeY q ≤ b_y - a_y.
3. This global quotient q is consistent with the local quotients. Specifically, q(x, Y) equals quot_Y x for many x in P_x, and q(X, y) equals quot_X y for many y in P_y. (Note: there seems to be another typo in the goal Bivariate.evalX y q = quot_X y, which evaluates q at X=y but compares it to a polynomial in X. It likely should be Bivariate.evalY y q = quot_X y).

Context

This lemma is a cornerstone result in algebraic coding theory, often used in the analysis of list-decoding algorithms for Reed-Solomon codes. The file's comments correctly attribute this variant to "Ben-Sasson et Al. Proximity Gaps for Reed-Solomon Codes," highlighting its application in theoretical computer science and cryptography.

The lemma's power comes from its ability to translate local information (divisibility on lines) into global structure (divisibility in the plane). This is a common theme in the "polynomial method." The proof relies heavily on the principle that a non-zero polynomial of low degree cannot have too many roots, a generalization of the Schwartz-Zippel lemma.

This proof will utilize the definitions from ArkLib.Data.Polynomial.Bivariate, such as degreeX, natDegreeY, evalX, and evalY, to formalize the concepts of degree and evaluation for bivariate polynomials.

Proof Suggestion

The proof is non-trivial and constructive. The main idea is to first construct a candidate quotient q, then define an "error" polynomial E = g - q * f, and finally use a degree-based argument to show that E must be the zero polynomial.

1. Handle trivial cases: Start by considering the case f = 0. The hypotheses should imply g = 0, making the goal easy to satisfy by choosing q = 0. From this point, you can assume f ≠ 0.

2. Construct a candidate q: Define a bivariate polynomial q that satisfies the required degree bounds (degreeX ≤ b_x - a_x, natDegreeY ≤ b_y - a_y) and agrees with one set of local quotients, say quot_Y.

   • You can do this using polynomial interpolation. Let q(X,Y) = ∑_j q_j(X) Y^j. For each j, q_j(X) is a polynomial in X of degree at most b_x - a_x.
   • Its value q_j(x) should be the j-th coefficient of the polynomial quot_Y x.
   • Choose a subset P'_x ⊆ P_x of size b_x - a_x + 1. Use Lagrange interpolation to define each q_j(X) as the unique polynomial of degree ≤ b_x - a_x that passes through the points (x, (quot_Y x).coeff j) for all x ∈ P'_x.
   • This construction completely defines q and guarantees evalX x q = quot_Y x for all x ∈ P'_x.

3. Define the error polynomial E: Let E := g - q * f. The goal is to show E = 0.

4. Show E has many roots on vertical lines: For any x ∈ P'_x, by construction q(x, Y) = quot_Y x. The hypothesis h_quot_Y states g(x, Y) = (quot_Y x) * f(x, Y). It follows that E(x, Y) = g(x, Y) - q(x, Y) * f(x, Y) = 0 (as a polynomial in Y) for every x ∈ P'_x.

5. Use the vertical roots to constrain E's structure: Since E(x, Y) = 0 for all x ∈ P'_x, the polynomial E(X, Y) must be divisible by (X - x) for each x ∈ P'_x. Therefore, E is divisible by Z(X) := ∏_{x ∈ P'_x} (X - x). Note that deg(Z(X)) = |P'_x| = b_x - a_x + 1.

6. The key degree argument:

   • Consider E on a horizontal line y ∈ P_y. From h_quot_X, g(X, y) = (quot_X y) * f(X, y).
   • So, E(X, y) = (quot_X y - q(X, y)) * f(X, y).
   • The degree in X of E(X, y) is at most b_x.
   • However, from step 5, we know Z(X) divides E(X, y). Since deg(Z(X)) = b_x - a_x + 1 and the degree of (quot_X y - q(X, y)) * f(X, y) is at most (b_x - a_x) + a_x = b_x, a polynomial of degree > b_x cannot divide a non-zero polynomial of degree ≤ b_x.
   • Conclude that E(X, y) must be the zero polynomial for every y ∈ P_y.

7. Show E is the zero polynomial: You have shown that E is zero on |P_y| ≥ n_y horizontal lines. The Y-degree of E is at most b_y. The crucial hypothesis h_le_1 implies n_y > b_y (you can prove this with linarith). A non-zero polynomial cannot have more roots than its degree. Thus, E must be the zero polynomial.

8. Prove the final agreement clauses:

   • Now that you have g = q * f, combine this with the hypotheses h_quot_X and h_quot_Y.
   • For x ∈ P_x, you'll get (q(x, Y) - quot_Y x) * f(x, Y) = 0. This implies q(x, Y) = quot_Y x for all x where f(x, Y) is not the zero polynomial. Since degreeX f ≤ a_x, this can only fail for at most a_x values of x. This gives you the set Q_x.
   • A similar argument gives you the set Q_y. This completes the proof.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

lemma Polishchuk_Spielman {F : Type} [Semiring F] [Field F]
  (P_x P_y : Finset F) [Nonempty P_x] [Nonempty P_y]
  (f g : F[X][Y]) (a_x a_y b_x b_y n_x n_y : ℕ)
  (quot_X : F → F[X]) (quot_Y : F → F[X])
  (h_bx_ge_ax : b_x ≥ a_x) (h_by_ge_ay : b_y ≥ a_y)
  (h_f_degX : a_x ≥ Bivariate.degreeX f) (h_g_degX : b_x ≥ Bivariate.degreeX g)
  (h_f_degY : a_y ≥ natDegreeY f) (h_g_degY : b_y ≥ natDegreeY g)
  (h_card_Px : n_x ≤ P_x.card) (h_card_Py : n_y ≤ P_y.card)
  (h_le_1 : 1 > (b_x : ℚ) / (n_x : ℚ) + (b_y : ℚ) / (n_y : ℚ))
  (h_quot_X : ∀ y ∈ P_y,
    (quot_X y).natDegree ≤ (b_x - a_x) ∧ Bivariate.evalY y g = (quot_X y) * (Bivariate.evalY y f))
  (h_quot_Y : ∀ x ∈ P_x,
    (quot_Y x).natDegree ≤ (b_y - a_y) ∧ Bivariate.evalX x g = (quot_Y x) * (Bivariate.evalX x f))
  : ∃ q : F[X][Y], g = q * f
    ∧ Bivariate.degreeX q ≤ b_x - a_x ∧ natDegreeY q ≤ b_y - a_y
    ∧ (∃ Q_x : Finset F, Q_x.card ≥ n_x - a_x ∧ Q_x ⊆ P_x ∧
        ∀ x ∈ Q_x, Bivariate.evalX x q = quot_Y x)
    ∧ (∃ Q_y : Finset F, Q_y.card ≥ n_y - a_y ∧ Q_y ⊆ P_y ∧
        ∀ y ∈ Q_y, Bivariate.evalX y q = quot_X y)
    := sorry