X-evaluated full-slice closeness comparison #
Single closenessOfIP comparison for the x-evaluated/full-y scalar-to-tensor
transition; extracted from Closeness.lean per #1127.
References #
references/ldt-paper/commutativity-G.texblueprint/src/chapter/ch08_commutativity.tex
theorem
MIPStarRE.LDT.Commutativity.xEvaluatedFullSliceABABAvg_to_xEvaluatedFullSliceABABtensorAvg
{ι : 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)
:
|xEvaluatedFullSliceABABAvg params strategy family - xEvaluatedFullSliceABABtensorAvg params strategy family| ≤ √zeta
X-evaluated/full-y scalar-to-tensor comparison for paper line 360.
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.