Polynomial-sum (cardinality-free) bounds for Section 8 transport

Cardinality-free sum-over-g bounds for the building blocks of the local-variance transport chain. These avoid the per-polynomial blow-up that one would get by summing the pointwise estimates: instead they use both the line-measurement POVM identity ∑_f B^ℓ_f = B^ℓ.total and the polynomial submeasurement normalization ∑_g G_g = G.total ≤ 1 to keep the right-register weight under control.

Paper anchor

references/ldt-paper/expansion.tex, lines 282-289 (proof of lem:generalize-b) and lines 317-321 (eq:equivalent-local-variance).

theorem MIPStarRE.LDT.GlobalVariance.generalizeBLineCollisionExpansion_polysum_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

Polynomial-sum analogue of generalizeBLineCollisionExpansion_le_error.

The line-collision expansion summed over all polynomials is bounded by generalizeBError = md/q without multiplying by the polynomial cardinality. The proof first applies the per-polynomial Schwartz-Zippel coefficient bound, then uses generalizeBLineCollisionTensorMass_polysum_le_one to bound the joint tensor mass. This is the cardinality-free reformulation of expansion.tex:282-289 underlying eq:equivalent-local-variance.

theorem MIPStarRE.LDT.GlobalVariance.generalizeBSeedCollisionExpansion_polysum_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

Polynomial-sum analogue of generalizeBSeedCollisionExpansion_le_error.

This is just the line/parameter expansion-equality identity composed with the polynomial-sum line bound.

theorem MIPStarRE.LDT.GlobalVariance.generalizeBCollisionResidual_polysum_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

Polynomial-sum analogue of generalizeBCollisionResidual_le_error.

Reduces to the line/parameter expansion via the incident-question reindexing identity, then applies the polynomial-sum line bound.

theorem MIPStarRE.LDT.GlobalVariance.generalizeBDeviationAtPolynomial_polysum_le_error {ι : 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

Polynomial-sum analogue of generalizeBPointwiseSchwartzZippel.

This is the cardinality-free bound that mirrors expansion.tex:282-289: the total weighted Schwartz-Zippel residual summed over all polynomials is bounded by md/q, not N · md/q. This is exactly the form used inside eq:equivalent-local-variance for the md/q transport steps in lem:local-variance-of-points (steps 3 and 4 of the six-step chain in expansion.tex:308-309).