Collision expansion and Schwartz-Zippel bounds

This module contains the generalizeB theorem wrappers, finite reparametrization and distribution bookkeeping, and the Schwartz-Zippel collision expansion that bounds the line-collision residual.

theorem MIPStarRE.LDT.GlobalVariance.generalizeB {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (_eps _delta _gamma : Error) (_hgood : strategy.IsGood _eps _delta _gamma) (G : SubMeas (Polynomial params) ι) (ψbi : QuantumState (ι × ι)) (hpoint : ∀ (g : Polynomial params), generalizeBDeviationAtPolynomial params strategy ψbi G g ≤ generalizeBError params) : GeneralizeBStatement params strategy ψbi G

lem:generalize-b.

theorem MIPStarRE.LDT.GlobalVariance.avgOver_axisParallelLineQuestionDistribution (params : Parameters) [FieldModel params.q] (f : AxisParallelLineQuestion params → Error) : avgOver (axisParallelLineQuestionDistribution params) f = avgOver (uniformDistribution (AxisParallelLine params × Fq params)) fun (ℓt : AxisParallelLine params × Fq params) => f (ℓt.1, ℓt.1.pointAt ℓt.2)

Reindex the axis-parallel line-question distribution as a uniform average over line/parameter seeds (ℓ,t) with sampled point u = ℓ(t).

This is the distributional bookkeeping used in expansion.tex, lines 281--288.

noncomputable def MIPStarRE.LDT.GlobalVariance.axisParallelLinePointParamEquiv (params : Parameters) [FieldModel params.q] : AxisParallelLine params × Fq params ≃ AxisParallelTestSample params × Fq params

Reindex a line representative and affine parameter by the sampled point on that line, keeping the direction and parameter as auxiliary data.

This is the finite bookkeeping behind expansion.tex, lines 300--302: averaging over a line representative ℓ and a parameter t is the same as averaging over the sampled base point u = ℓ(t), the direction, and the forgotten parameter.

Equations

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

theorem MIPStarRE.LDT.GlobalVariance.avgOver_axisParallelLineQuestionDistribution_to_axisParallelTestSample (params : Parameters) [FieldModel params.q] (f : AxisParallelTestSample params → Error) : (avgOver (axisParallelLineQuestionDistribution params) fun (qu : AxisParallelLineQuestion params) => f (qu.2, qu.1.direction)) = avgOver (uniformDistribution (AxisParallelTestSample params)) f

Combining the incident-pair distribution with the sampled-point marginal gives the native base-point test distribution.

theorem MIPStarRE.LDT.GlobalVariance.generalizeBLineCollisionTensorMass_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) (ℓ : AxisParallelLine params) (f : AxisLinePolynomial params) : 0 ≤ ev strategy.state (opTensor ((strategy.axisParallelMeasurement.toIdxProjMeas ℓ).outcome f) (G.outcome g))

Positivity of the tensor mass appearing in the line-collision expansion.

theorem MIPStarRE.LDT.GlobalVariance.generalizeBLineCollisionCoefficient_le (params : Parameters) [FieldModel params.q] (g : Polynomial params) (ℓ : AxisParallelLine params) (f : AxisLinePolynomial params) : (avgOver (uniformDistribution (Fq params)) fun (t : Fq params) => if f.toFun t = (Polynomial.restrictToAxisParallelLine params g ℓ).toFun t ∧ f.poly ≠ (Polynomial.restrictToAxisParallelLine params g ℓ).poly then 1 else 0) ≤ generalizeBError params

Schwartz--Zippel coefficient bound for a fixed polynomial, line, and line answer.

theorem MIPStarRE.LDT.GlobalVariance.generalizeBSeedCollisionExpansion_eq_lineCollisionExpansion {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (ψbi : QuantumState (ι × ι)) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) : generalizeBSeedCollisionExpansion params strategy ψbi G g = generalizeBLineCollisionExpansion params strategy ψbi G g

Commuting the uniform parameter average past the finite sum over line answers.

This is the purely finite-sum bookkeeping between the paper's seed average over (ℓ,t) and the coefficient-weighted display in expansion.tex, lines 286--288. The remaining #753 residual is now only the incident-question/postprocess equality between generalizeBCollisionResidual and generalizeBSeedCollisionExpansion.

theorem MIPStarRE.LDT.GlobalVariance.generalizeBCollisionResidual_eq_seedCollisionExpansion {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) : generalizeBCollisionResidual params strategy strategy.state G g = generalizeBSeedCollisionExpansion params strategy strategy.state G g

The incident-question collision residual is exactly the uniform line/parameter seed expansion from expansion.tex, lines 286--288.

The proof reindexes the axis-parallel line-test distribution by (ℓ,t) with sampled point u = ℓ(t), then expands the ProjMeas.postprocess fiber for the collision event f(t) = g|_ℓ(t) and f ≠ g|_ℓ.

theorem MIPStarRE.LDT.GlobalVariance.generalizeBLineCollisionExpansion_le_error {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) : generalizeBLineCollisionExpansion params strategy strategy.state G g ≤ generalizeBError params

The explicit line/parameter collision expansion is bounded by m*d/q.

This proves the Schwartz--Zippel and normalization parts of the residual estimate from expansion.tex, lines 286--288. The preceding generalizeBCollisionResidual_eq_seedCollisionExpansion theorem supplies the incident-question/postprocess identity needed to apply this bound to the original collision residual.

theorem MIPStarRE.LDT.GlobalVariance.generalizeBSeedCollisionExpansion_le_error {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) : generalizeBSeedCollisionExpansion params strategy strategy.state G g ≤ generalizeBError params

The uniform line/parameter seed collision expansion is bounded by m*d/q.

The proof first commutes the finite seed average into the coefficient-weighted line expansion, then applies the Schwartz--Zippel coefficient bound and tensor normalization estimate above.

theorem MIPStarRE.LDT.GlobalVariance.generalizeBCollisionResidual_le_error {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) : generalizeBCollisionResidual params strategy strategy.state G g ≤ generalizeBError params

The pointwise collision residual in lem:generalize-b is bounded by m*d/q.

This combines the incident-question reindexing with the seed/line expansion, Schwartz--Zippel coefficient bound, and submeasurement-normalization estimate from expansion.tex, lines 281--288.

theorem MIPStarRE.LDT.GlobalVariance.generalizeBPointwiseSchwartzZippel {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (g : Polynomial params) : generalizeBDeviationAtPolynomial params strategy strategy.state G g ≤ generalizeBError params

Pointwise Schwartz--Zippel bound for the strategy-state form of lem:generalize-b.

This is the paper's estimate at expansion.tex, lines 281--288, after the projective expansion converts the squared norm into the collision residual.

theorem MIPStarRE.LDT.GlobalVariance.generalizeBFromSchwartzZippel {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (_eps _delta _gamma : Error) (_hgood : strategy.IsGood _eps _delta _gamma) (G : SubMeas (Polynomial params) ι) : GeneralizeBStatement params strategy strategy.state G

lem:generalize-b for the strategy state, with the pointwise Schwartz--Zippel estimate discharged internally. The good-strategy hypothesis is kept in the statement to match the paper context of expansion.tex, lines 271--288, although the algebraic Schwartz--Zippel proof itself does not use ε, δ, or γ.