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 counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Main/Auxiliary/ScalarMarginalization.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The public lemmas fullSlice_scalar_marginalize_x and fullSlice_scalar_marginalize_y are pure scalar inequalities. Their proofs compose the tensor-form comparisons over the tensor averages of Co/Commutativity/Transport/FullSlice/Averages.lean, with closenessOfIP at cost √ζ each (the scalar/tensor decision is recorded upstream in docs/decisions/713-scalar-tensor-decision.md).

The vendored hypothesis hnorm : strategy.state.IsNormalized is dropped from both public lemmas: normalization is a theorem of the model (VecState.ev_one_of_isNormalized), and the ported Preliminaries.switchSandwich and transport bridges no longer take it. The two summation helpers take the model S : SymModel 𝔓 K as an explicit first argument, where the vendored ones take ψ; avgOver_slice_total_left_sandwich_eq takes it after params, as the vendored one takes ψ.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

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

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedPointProj {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) : IdxProjSubMeas (MIPStarRE.LDT.Point params.next) (MIPStarRE.LDT.Fq params) 𝔓

The evaluated point family viewed as a projective submeasurement family.

Equations

• MIPRE.LIDT.Co.Commutativity.evaluatedPointProj params family u = { toSubMeas := MIPRE.LIDT.Co.Commutativity.evaluatedPointFamily params family u, proj := ⋯ }

theorem MIPRE.LIDT.Co.Commutativity.abs_sub_le_of_two_step {a b c e₁ e₂ : ℝ} (hab : |a - b| ≤ e₁) (hbc : |b - c| ≤ e₂) : |a - c| ≤ e₁ + e₂

Triangle inequality with explicit bounds for an intermediate point.

theorem MIPRE.LIDT.Co.Commutativity.sum_ev_leftTensor_sandwich_total {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} [Fintype α] (S : SymModel 𝔓 K) (A : 𝔓) (B : SubMeas α 𝔓) : ∑ b : α, S.ev (S.L (A * B.outcome b * A)) = S.ev (S.L (A * B.total * A))

Summing the inner outcome in an ABA expectation turns it into the submeasurement total.

theorem MIPRE.LIDT.Co.Commutativity.sum_ev_middle_total {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} [Fintype α] (S : SymModel 𝔓 K) (G : 𝔓) (A : SubMeas α 𝔓) : ∑ a : α, S.ev (S.L G * S.R (A.outcome a)) = S.ev (S.L G * S.R A.total)

Summing the right-register outcome in the middle switch-sandwich term turns it into the submeasurement total.

theorem MIPRE.LIDT.Co.Commutativity.avgOver_slice_total_left_sandwich_eq {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (A : 𝔓) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (y : MIPStarRE.LDT.Fq params) => S.ev (S.L (A * (family.meas y).total * A))) = S.ev (S.L A * S.L family.averagedSubMeas.total * S.L A)

Averaging the middle total in an ABA sandwich produces the averaged slice operator G = E_y Gʸ.

theorem MIPRE.LIDT.Co.Commutativity.fullSliceABAAvg_eq_leftSandwichExpectation {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) : fullSliceABAAvg params strategy family = Preliminaries.leftSandwichExpectation strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) family.meas family.averagedSubMeas.total

Full-slice cubic first term as the left switch-sandwich expectation.

theorem MIPRE.LIDT.Co.Commutativity.evaluatedSliceABAAvg_eq_leftSandwichExpectation {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) : evaluatedSliceABAAvg params strategy family = Preliminaries.leftSandwichExpectation strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) (evaluatedPointProj params family) family.averagedSubMeas.total

Evaluated-slice cubic first term as the evaluated left switch-sandwich expectation.

theorem MIPRE.LIDT.Co.Commutativity.fullSlice_middleSandwichExpectation_eq_evaluated {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) : Preliminaries.middleSandwichExpectation strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) family.meas family.averagedSubMeas.total = Preliminaries.middleSandwichExpectation strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) (evaluatedPointProj params family) family.averagedSubMeas.total

The full and evaluated switch-sandwich middle terms are the same G ⊗ G average.

theorem MIPRE.LIDT.Co.Commutativity.fullSlice_scalar_marginalize_x {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (zeta : ℝ) (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 MIPRE.LIDT.Co.Commutativity.fullSlice_scalar_marginalize_y {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (zeta : ℝ) (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√ζ.