Polynomial agreement bound (Step 5 hammer)

Public packaging of Schwartz-Zippel for the project's Polynomial params class. This is the building block invoked at:

• paper references/ldt-paper/inductive_step.tex, lines 119–133 — the md/q term in the mainFormal self-consistency cascade,
• paper references/ldt-paper/commutativity-G.tex, the analogous step in comMain (issue #297).

The earlier private form of this lemma lived in MIPStarRE.LDT.Commutativity.Scaffold.Symmetry. Promoting it lets both comMain and mainFormal Step 5 (#425) share one proof.

References

• references/ldt-paper/inductive_step.tex
• references/ldt-paper/preliminaries.tex, Section 3

def MIPStarRE.LDT.Preliminaries.pointScalarEquiv (params : Parameters) [FieldModel params.q] : Point params ≃ (Fin params.m → Scalar params)

Coordinatewise transport between coded F_q points and the underlying scalar model. This is the equivalence used to apply Schwartz-Zippel inside MvPolynomial's scalar function space.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.Preliminaries.polynomialAgreement_avg_eq_scalarDomain (params : Parameters) [FieldModel params.q] (g g' : Polynomial params) : (avgOver (uniformDistribution (Point params)) fun (u : Point params) => if g.toFun u = g'.toFun u then 1 else 0) = avgOver (uniformDistribution (Fin params.m → Scalar params)) fun (u : Fin params.m → Scalar params) => if (MvPolynomial.eval u) g.poly = (MvPolynomial.eval u) g'.poly then 1 else 0

Reindex evaluation equality from coded Point params points to the scalar function space used by schwartzZippel_individualDegree.

theorem MIPStarRE.LDT.Preliminaries.polynomialAgreement_avg_le_mdq (params : Parameters) [FieldModel params.q] (g g' : Polynomial params) (hneq : g ≠ g') : (avgOver (uniformDistribution (Point params)) fun (u : Point params) => if g.toFun u = g'.toFun u then 1 else 0) ≤ ↑params.m * ↑params.d / ↑params.q

Schwartz-Zippel bound for the pointwise agreement indicator of two distinct full polynomial outcomes.

Packages the md/q loss term that appears at:

• references/ldt-paper/inductive_step.tex lines 119–133 (the mainFormal Step 5 self-consistency cascade, issue #425),
• references/ldt-paper/commutativity-G.tex (the comMain step, issue #297).

Both call sites previously held a private duplicate of this proof; this is the shared, reusable form.

theorem MIPStarRE.LDT.Preliminaries.axisLinePolynomialAgreement_avg_eq_scalarDomain (params : Parameters) [FieldModel params.q] (f h : AxisLinePolynomial params) : (avgOver (uniformDistribution (Fq params)) fun (t : Fq params) => if f.toFun t = h.toFun t then 1 else 0) = avgOver (uniformDistribution (Scalar params)) fun (x : Scalar params) => if Polynomial.eval x f.poly = Polynomial.eval x h.poly then 1 else 0

Reindex evaluation equality for degree-d line polynomials from coded Fq params parameters to the scalar field used by Mathlib's univariate polynomial API.

theorem MIPStarRE.LDT.Preliminaries.axisLinePolynomialAgreement_avg_le_mdq (params : Parameters) [FieldModel params.q] (f h : AxisLinePolynomial params) (hneq : f.poly ≠ h.poly) : (avgOver (uniformDistribution (Fq params)) fun (t : Fq params) => if f.toFun t = h.toFun t then 1 else 0) ≤ ↑params.m * ↑params.d / ↑params.q

Schwartz--Zippel for two distinct degree-d axis-line answers, stated with the ambient m*d/q loss used in the LDT estimates. The underlying univariate root count gives d/q, and params.hm deliberately pads it to the paper's ambient m*d/q loss.

theorem MIPStarRE.LDT.Preliminaries.polynomialCollision_sandwichTensor_le_mdq {ιA : Type u_1} {ιB : Type u_2} {β : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype β] (params : Parameters) [FieldModel params.q] (ψ : QuantumState (ιA × ιB)) (hnorm : ψ.IsNormalized) (Outer : SubMeas β ιA) (Inner : SubMeas (Polynomial params) ιA) (Right : SubMeas (Polynomial params) ιB) : ∑ gg : Polynomial params × Polynomial params, ∑ o : β, (if gg.1 = gg.2 then 0 else avgOver (uniformDistribution (Point params)) fun (u : Point params) => if gg.1.toFun u = gg.2.toFun u then 1 else 0) * ev ψ (leftTensor (Outer.outcome o * Inner.outcome gg.1 * Outer.outcome o) * rightTensor (Right.outcome gg.2)) ≤ ↑params.m * ↑params.d / ↑params.q

Tensor-form Schwartz-Zippel collision bound.

For each off-diagonal pair of polynomial outcomes, the point-collision coefficient is bounded by params.m * params.d / params.q via polynomialAgreement_avg_le_mdq. The remaining tensor residual is bounded by 1 using sandwichTensor_residual_sum_le_one, so the whole nonnegative collision sum has the same m d / q bound.

noncomputable def MIPStarRE.LDT.Preliminaries.polynomialCollisionMass {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (params : Parameters) [FieldModel params.q] (ψ : QuantumState (ιA × ιB)) (Left : SubMeas (Polynomial params) ιA) (Right : SubMeas (Polynomial params) ιB) : Error

The off-diagonal polynomial-collision mass used in mainFormal Step 5.

This is the weighted collision term in inductive_step.tex lines 122--127: for every distinct pair of full polynomial outcomes (g, h), the coefficient is Pr_u[g(u) = h(u)], and the quantum weight is the fixed cross-register mass ⟨ψ | G^A_g ⊗ G^B_h | ψ⟩.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.Preliminaries.polynomialCollisionMass_le_mdq {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (params : Parameters) [FieldModel params.q] (ψ : QuantumState (ιA × ιB)) (hnorm : ψ.IsNormalized) (Left : SubMeas (Polynomial params) ιA) (Right : SubMeas (Polynomial params) ιB) : polynomialCollisionMass params ψ Left Right ≤ ↑params.m * ↑params.d / ↑params.q

mainFormal Step 5's tensor-valued Schwartz--Zippel loss.

This is the specialization of polynomialCollision_sandwichTensor_le_mdq with no outer sandwich. It supplies exactly the paper's line-126 estimate for the collision term after the evaluated self-consistency defect has been expanded.