The non-multilinear mass, and Schwartz--Zippel in the agreement direction

This file is the repair of the campaign's critical finding at ledger node 1.2.2.15, recorded in blueprint rem:qld-admitted.

The separating stage of the appendix needs to replace, inside a Born average, the evaluation g(u) of an outcome g of individual degree at most d by the evaluation Coded(g) . ind_m(u) --- which is the evaluation at u of the multilinear interpolant of g's values on the cube {0,1}^m. The two agree for multilinear g and not otherwise.

An earlier revision of the paper bounded the substitution error by 2 E_u 1[g(u) != g_k(u)] <= 2md/q. That applies Schwartz--Zippel backwards. What Schwartz--Zippel gives is that two distinct polynomials of total degree at most md agree on at most an md/q fraction of F_q^m; so for a non-multilinear g the disagreement indicator has expectation close to 1, not close to 0, and the step as written was equivalent to an unproven assertion.

The two halves of the correct argument are the two halves of this file, and neither mentions the game.

The agreement bound, in the right direction

prob_agree_ldEnc_le_of_not_multilinear: a polynomial of individual degree at most d that is not multilinear agrees with the multilinear interpolant of any boolean-cube data on at most an md/q fraction of points. The point is that non-multilinearity makes g distinct from every multilinear polynomial at once, so a single application of MIPRE.LowDegree.prob_agree_le_individualDegree covers every k uniformly --- which is what the next step needs, since it sums over k.

The mass bound

nonMultilinear_mass_le: the combinatorial step that turns the agreement bound into a bound on the mass the outcome distribution places on non-multilinear outcomes. Stated for abstract nonnegative weights, because that is all it uses: a distribution S on outcomes, a subdistribution T dominated by it, a set ML of good outcomes, the agreement bound T g <= c * S g off ML, and a lower bound 1 - eta on T's total. The conclusion is S (ML^c) <= eta + c.

sum_sub_le_of_eq_on: the substitution error itself, once the mass is bounded. Two families agreeing on ML and each dominated by S in absolute value differ in total by at most twice the mass off ML.

What is not here

That the substituted quantity agrees with the original on the multilinear outcomes --- the paper's parenthesis "there g_{Coded(g)} = g" --- is the statement that a multilinear polynomial is the interpolant of its own values on {0,1}^m, i.e. that multilinear interpolation is unique. It is an independent fact about MvPolynomial, not part of this repair, and it is an outstanding ingredient: sum_sub_le_of_eq_on accordingly takes the agreement on the good set as a hypothesis rather than deriving it.

Schwartz--Zippel against every multilinear polynomial at once

theorem MIPRE.QLD.prob_agree_ldEnc_le_of_not_multilinear {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} {g : MvPolynomial (Fin m) F} (hg : ∀ (i : Fin m), MvPolynomial.degreeOf i g ≤ d) (hd : 1 ≤ d) (hnml : ¬∀ (i : Fin m), MvPolynomial.degreeOf i g ≤ 1) (a : (Fin m → Bool) → F) : ↑(LowDegree.agree g (LowDegree.ldEnc a)).card / ↑(Fintype.card F) ^ m ≤ ↑m * ↑d / ↑(Fintype.card F)

A non-multilinear polynomial of individual degree at most d agrees with the multilinear interpolant of any cube data on at most an md/q fraction of F_q^m.

This is Schwartz--Zippel in the agreement direction, which is the direction the appendix needs and the direction an earlier revision of the paper had backwards. The hypothesis is that g fails to be multilinear, and the conclusion is uniform in the interpolated data a --- both matter: the consumer sums over all of F_q^M, and would gain nothing from a bound depending on a.

The mass the outcome distribution places off a good set

theorem MIPRE.QLD.nonMultilinear_mass_le {G : Type u_2} [Fintype G] [DecidableEq G] {S T : G → ℝ} {ML : Finset G} {c eta : ℝ} (hS : ∀ (g : G), 0 ≤ S g) (hsum : ∑ g : G, S g = 1) (hT : ∀ (g : G), T g ≤ S g) (hoff : ∀ g ∉ ML, T g ≤ c * S g) (hc : 0 ≤ c) (hlow : 1 - eta ≤ ∑ g : G, T g) : ∑ g ∈ Finset.univ \ ML, S g ≤ eta + c

The mass bound. If T is dominated by the distribution S, is at most c times S away from the good set ML, and still carries total weight at least 1 - eta, then S puts at most eta + c off ML.

This is the appendix's aggregation step, and it is the shape the repaired argument needs: the agreement bound of prob_agree_ldEnc_le_of_not_multilinear is exactly the hypothesis hoff at c = md/q. The proof is one split of the total: on ML only the domination T <= S is available, off ML the agreement bound applies, and comparing with sum S = 1 isolates the mass off ML.

theorem MIPRE.QLD.sum_sub_le_of_eq_on {G : Type u_2} [Fintype G] [DecidableEq G] {A B S : G → ℝ} {ML : Finset G} (hon : ∀ g ∈ ML, A g = B g) (hA : ∀ (g : G), |A g| ≤ S g) (hB : ∀ (g : G), |B g| ≤ S g) : |∑ g : G, A g - ∑ g : G, B g| ≤ 2 * ∑ g ∈ Finset.univ \ ML, S g

The substitution error. Two families that agree on ML and are each dominated in absolute value by S differ in total by at most twice the mass off ML.