Section 11 commutativity: evaluated-question transport

Core Schwartz–Zippel transport on the evaluated-question space, comparing full-polynomial and point-evaluated outcomes: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Main/EvaluatedQuestions.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The vendored hypothesis hnorm : strategy.state.IsNormalized is dropped from fullSliceCommutation_of_evaluated_on_evaluated_questions: normalization is a theorem of the model (VecState.ev_one_of_isNormalized), and none of the lemmas the proof composes takes it any more. Callers pass params strategy family gamma zeta hgamma_nonneg hzeta_nonneg hself hEval.

New here

commDataProcessedGError_to_comMainError_arith, the real arithmetic of the small-parameter case of fullSliceCommutation_of_evaluated_on_evaluated_questions, which the vendored proof does inline; split out so that the operator-level proof does not elaborate 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.commDataProcessedGError_to_comMainError_arith (params : MIPStarRE.LDT.Parameters) (gamma zeta : ℝ) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hzeta_le : zeta ≤ 1) (hdq_le : ↑params.d / ↑params.q ≤ 1) : 16 * √zeta + 4 * (↑params.m * ↑params.d / ↑params.q) + 2 * √(MIPStarRE.LDT.Commutativity.commDataProcessedGError params gamma zeta) ≤ MIPStarRE.LDT.Commutativity.comMainError params gamma zeta

The error arithmetic of fullSliceCommutation_of_evaluated_on_evaluated_questions in its small-parameter case: for 0 ≤ γ, 0 ≤ ζ ≤ 1 and d/q ≤ 1, 16√ζ + 4md/q + 2√(48m(√γ + √ζ)) ≤ 30m(γ^¼ + ζ^¼ + (d/q)^¼), from √ζ ≤ ζ^¼, d/q ≤ (d/q)^¼, √(48m(√γ + √ζ)) ≤ √(48m)(γ^¼ + ζ^¼) and √(48m) ≤ 7m.

theorem MIPRE.LIDT.Co.Commutativity.fullSliceCommutation_of_evaluated_on_evaluated_questions {𝔓 : 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 𝔓) (gamma zeta : ℝ) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hEval : strategy.state.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (evaluatedFromFullSliceProductLeft params strategy family) (evaluatedFromFullSliceProductRight params strategy family) (MIPStarRE.LDT.Commutativity.commDataProcessedGError params gamma zeta)) : strategy.state.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => fullSliceProductLeft params strategy family (MIPStarRE.LDT.Commutativity.fullSliceQuestionOfEvaluatedSlice params q)) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => fullSliceProductRight params strategy family (MIPStarRE.LDT.Commutativity.fullSliceQuestionOfEvaluatedSlice params q)) (MIPStarRE.LDT.Commutativity.comMainError params gamma zeta)

Core Schwartz-Zippel transport on the evaluated-question space.

This is the substantive remaining step: compare the full polynomial outcomes with their point-evaluated postprocessings while paying the two md/q Schwartz-Zippel losses and the self-consistency bookkeeping.