Section 11 commutativity: scalar marginalization lemmas

Schwartz–Zippel marginalization helpers (eq:evaluate-gcom-at-points, eq:gcom4-diff) used in the final full-slice commutation theorem.

The public lemmas fullSlice_scalar_marginalize_x and fullSlice_scalar_marginalize_y are pure scalar inequalities. Their proofs compose internal tensor-form comparisons over the tensor averages defined in Transport/FullSlice/Averages.lean, with closenessOfIP at cost √ζ each.

See docs/decisions/713-scalar-tensor-decision.md for the full decision record.

References

• references/ldt-paper/commutativity-G.tex
• blueprint/src/chapter/ch08_commutativity.tex

theorem MIPStarRE.LDT.Commutativity.fullSlice_scalar_marginalize_x {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (zeta : Error) (hnorm : strategy.state.IsNormalized) (hself : family.StronglySelfConsistent strategy.state zeta) : |fullSliceABAAvg params strategy family - evaluatedSliceABAAvg params strategy family| ≤ 4 * √zeta

Paper first-term switch-sandwich transport (commutativity-G.tex lines 295--305), stated in the public scalar API.

The paper does not use an md/q Schwartz--Zippel step for the cubic first term. Instead, both the full and evaluated cubic terms are compared to the common G ⊗ G switch-sandwich center, costing 2√ζ on each side.

theorem MIPStarRE.LDT.Commutativity.fullSlice_scalar_marginalize_y {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (zeta : Error) (hnorm : strategy.state.IsNormalized) (hself : family.StronglySelfConsistent strategy.state zeta) : |fullSliceABABAvg params strategy family - evaluatedSliceABABAvg params strategy family| ≤ 2 * (↑params.m * ↑params.d / ↑params.q) + 4 * √zeta

Paper-faithful second-term transport bound.

The proved x-prefix (eq:gcom4 plus eq:gcom4-diff, paper lines 332--354) costs md/q + √ζ; the proved line-359 closenessOfIP comparison costs √ζ; the line-360 scalar↔tensor comparison is proved in xEvaluatedFullSliceABABAvg_to_xEvaluatedFullSliceABABtensorAvg and costs another √ζ; and the proved y-tail uses y-Schwartz--Zippel marginalization (paper lines 369--385) plus the √ζ doubly-evaluated scalar↔tensor comparison. Thus the whole scalar second-term comparison costs 2·md/q + 4√ζ.