Full-slice scalar-to-tensor closeness comparison

closenessOfIP comparisons transform scalar quartic averages into manifestly positive tensor-form partners. The same route includes tensor-marginalization identities connecting full-slice and evaluated-slice ABAB averages.

The core closenessOfIP scalar↔tensor comparison lemmas are factored into ClosenessCore.lean (extracted per #1127).

The tensor-form lemmas are internal to the scalar/tensor comparison recorded in docs/decisions/713-scalar-tensor-decision.md; downstream code should use the scalar public API exposed by the full-slice transport theorems.

References

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

theorem MIPStarRE.LDT.Commutativity.xEvaluatedSliceBABAtensor_to_xEvaluatedFullSliceABABAvg {ι : 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) : |xEvaluatedSliceBABAtensorAvg params strategy family - xEvaluatedFullSliceABABAvg params strategy family| ≤ √zeta

theorem MIPStarRE.LDT.Commutativity.fullSliceABAB_to_xEvaluatedSliceBABAtensorAvg {ι : 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 - xEvaluatedSliceBABAtensorAvg params strategy family| ≤ ↑params.m * ↑params.d / ↑params.q + √zeta

Proved x-prefix from the full scalar quartic to the x-evaluated BAB ⊗ A tensor endpoint.

This combines the first two paper steps for the second term in commutativity-G.tex lines 332--354: the eq:gcom4 scalar-to-BAB ⊗ A comparison costs √ζ, and the eq:gcom4-diff Schwartz--Zippel postprocessing of the x polynomial outcome costs md/q. The remaining paper lines 356--360 are intentionally not included here; they are the two closenessOfIP legs from xEvaluatedSliceBABAtensorAvg to xEvaluatedFullSliceABABtensorAvg.

theorem MIPStarRE.LDT.Commutativity.xEvaluatedFullSliceABABtensor_to_evaluatedSliceABABAvg {ι : 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) : |xEvaluatedFullSliceABABtensorAvg params strategy family - evaluatedSliceABABAvg params strategy family| ≤ ↑params.m * ↑params.d / ↑params.q + √zeta

Proved y-tail from the mixed ABA ⊗ B tensor endpoint to the evaluated scalar quartic.

This combines the paper steps after the x-stage has already reached xEvaluatedFullSliceABABtensorAvg: y-Schwartz-Zippel marginalization (commutativity-G.tex lines 369--385) followed by the √ζ closenessOfIP move that swaps a trailing G^y_{[h(v)=b]} between the scalar quartic and the ABA ⊗ B tensor -- the doubly-evaluated analogue of paper line 360, exposed via evaluatedSliceABAB_scalar_to_ABABtensor.