Section 11 commutativity: evaluated-question transport #
Core Schwartz–Zippel transport on the evaluated-question space, comparing full-polynomial and point-evaluated outcomes.
References #
references/ldt-paper/commutativity-G.texblueprint/src/chapter/ch08_commutativity.tex
theorem
MIPStarRE.LDT.Commutativity.fullSliceCommutation_of_evaluated_on_evaluated_questions
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
(gamma zeta : Error)
(hnorm : strategy.state.IsNormalized)
(hgamma_nonneg : 0 ≤ gamma)
(hzeta_nonneg : 0 ≤ zeta)
(hself : family.StronglySelfConsistent strategy.state zeta)
(hEval :
SDDOpRel strategy.state (uniformDistribution (EvaluatedSliceQuestion params))
(evaluatedFromFullSliceProductLeft params strategy family)
(evaluatedFromFullSliceProductRight params strategy family) (commDataProcessedGError params gamma zeta))
:
SDDOpRel strategy.state (uniformDistribution (EvaluatedSliceQuestion params))
(fun (q : EvaluatedSliceQuestion params) =>
fullSliceProductLeft params strategy family (fullSliceQuestionOfEvaluatedSlice params q))
(fun (q : EvaluatedSliceQuestion params) =>
fullSliceProductRight params strategy family (fullSliceQuestionOfEvaluatedSlice params q))
(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.