Full-slice scalar-to-tensor closeness comparison

closenessOfIP comparisons transform scalar quartic averages into manifestly positive tensor-form partners, and the same route includes the tensor-marginalization identities connecting full-slice and evaluated-slice ABAB averages: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Transport/FullSlice/Bridges/Closeness.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions"). The core comparison fullSliceABAB_scalar_to_BABAtensor is in ClosenessCore.lean.

The comparisons are stated on the symmetric model of a strategy strategy : SymStrat params.next 𝔓 K, the vendored leftTensor (ι₂ := ι) and rightTensor (ι₁ := ι) being strategy.state.L and strategy.state.R. The vendored hypothesis hnorm : strategy.state.IsNormalized is a theorem of the model and is dropped from every statement, as the ported Preliminaries.closenessOfIP and closenessOfIPAdjoint no longer take it. leftTensor_sandwich_adjoint_normalization_family is a placement lemma and takes the model (S : SymModel 𝔓 K) as its first explicit argument. The tensor-form lemmas are internal to the scalar/tensor comparison recorded upstream in docs/decisions/713-scalar-tensor-decision.md; downstream code should use the scalar API exposed by the full-slice transport theorems.

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

theorem MIPRE.LIDT.Co.Commutativity.leftTensor_sandwich_adjoint_normalization_family {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Ω : Type u_3} {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (P : Ω → SubMeas α 𝔓) (Q : Ω → ProjSubMeas β 𝔓) (ω : Ω) : ∑ a : α, star (∑ b : β, S.L ((Q ω).outcome b * (P ω).outcome a * (Q ω).outcome b)) * ∑ b : β, S.L ((Q ω).outcome b * (P ω).outcome a * (Q ω).outcome b) ≤ 1

The adjoint-side placed normalization condition for a family of sandwiches C^ω_{a,b} = Q^ω_b P^ω_a Q^ω_b ⊗ I, one for each index ω: the C-hypothesis of closenessOfIPAdjoint.

theorem MIPRE.LIDT.Co.Commutativity.xEvaluatedSliceBABAtensor_to_xEvaluatedFullSliceABABAvg {𝔓 : 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) : |xEvaluatedSliceBABAtensorAvg params strategy family - xEvaluatedFullSliceABABAvg params strategy family| ≤ √zeta

X-evaluated BAB ⊗ A tensor to x-evaluated scalar quartic (paper commutativity-G.tex line 359; the vendored hypothesis hnorm : strategy.state.IsNormalized is a theorem of the model): one closenessOfIPAdjoint application moves the evaluated G^x_[g(u)=a] from the right register to the front of the left one.

theorem MIPRE.LIDT.Co.Commutativity.evaluatedSliceABAB_scalar_to_ABABtensor {𝔓 : 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) : |evaluatedSliceABABAvg params strategy family - evaluatedSliceABABtensorAvg params strategy family| ≤ √zeta

Evaluated-slice y-side scalar-to-tensor comparison (the vendored hypothesis hnorm : strategy.state.IsNormalized is a theorem of the model): move the trailing G^y_[h(v)=b] in the scalar quartic to the right register, producing the tensor form in paper commutativity-G.tex line 360.

theorem MIPRE.LIDT.Co.Commutativity.fullSliceABAB_to_xEvaluatedSliceBABAtensorAvg {𝔓 : 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 - 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 (the vendored hypothesis hnorm : strategy.state.IsNormalized is a theorem of the model).

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 MIPRE.LIDT.Co.Commutativity.xEvaluatedFullSliceABABtensor_to_evaluatedSliceABABAvg {𝔓 : 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) : |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 (the vendored hypothesis hnorm : strategy.state.IsNormalized is a theorem of the model).

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.