X-evaluated full-slice closeness comparison

The single closenessOfIP comparison for the x-evaluated/full-y scalar-to-tensor transition: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Transport/FullSlice/Bridges/ClosenessXEval.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The comparison is 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, as the ported Preliminaries.closenessOfIP no longer takes it.

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.xEvaluatedFullSliceABABAvg_to_xEvaluatedFullSliceABABtensorAvg {𝔓 : 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) : |xEvaluatedFullSliceABABAvg params strategy family - xEvaluatedFullSliceABABtensorAvg params strategy family| ≤ √zeta

X-evaluated/full-y scalar-to-tensor comparison for paper line 360 (the vendored hypothesis hnorm : strategy.state.IsNormalized is a theorem of the model).

After the x-side Schwartz--Zippel step, the first family has already been postprocessed at u, while the y-family is still full-polynomial. This lemma proves the second closenessOfIP move in commutativity-G.tex lines 356--360: move the trailing G^y_h in G^x_[g(u)=a] G^y_h G^x_[g(u)=a] G^y_h ⊗ I to the right register, yielding G^x_[g(u)=a] G^y_h G^x_[g(u)=a] ⊗ G^y_h.

The preceding line-359 comparison from the BAB ⊗ A tensor endpoint to this scalar endpoint remains separate because it follows a different closenessOfIP leg.