Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.Commutativity.Main.Auxiliary.HEvalTransport

Section 11 commutativity: hEval/closenessOfIP transport #

Evaluated-side closeness-of-IP transport and strong hEval bounds (eq:evaluate-gcom-at-points through eq:don't-understand-the-numbering-system).

Provides the evaluated-side closenessOfIP chain on CAB products, including zero-operator triangulation helpers and the sharp bound fullSlice_closenessOfIP_CAB_hEval_sqrt and its paper-envelope estimate fullSlice_closenessOfIP_CAB_hEval.

References #

source
theorem MIPStarRE.LDT.Commutativity.fullSlice_closenessOfIP_CAB_hEval_sqrt {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) (hnorm : strategy.state.IsNormalized) (hEval : SDDOpRel strategy.state (uniformDistribution (EvaluatedSliceQuestion params)) (evaluatedFromFullSliceProductLeft params strategy family) (evaluatedFromFullSliceProductRight params strategy family) (commDataProcessedGError params gamma zeta)) :
|evaluatedSliceABAAvg params strategy family - evaluatedSliceABABAvg params strategy family| ≤ √(commDataProcessedGError params gamma zeta)

Strong evaluated-side hEval transport bound.

The direct evaluated-side route transports hEval to evaluatedSliceProductLeft/Right, rewrites the resulting SDDOpRel via evaluatedSliceCommutation_qSDDOp_avg_eq, and combines it with the a priori normalized-state bound sddErrorOp ≤ 4 for the evaluated product families. It yields the sharper estimate |evaluatedSliceABAAvg - evaluatedSliceABABAvg| ≤ √ν, where ν = commDataProcessedGError params gamma zeta. The paper-envelope estimate fullSlice_closenessOfIP_CAB_hEval below recovers the older 6√ζ + √ν statement when that displayed Section 11 bound is convenient.

source
theorem MIPStarRE.LDT.Commutativity.fullSlice_closenessOfIP_CAB_hEval {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) (hnorm : strategy.state.IsNormalized) (hEval : SDDOpRel strategy.state (uniformDistribution (EvaluatedSliceQuestion params)) (evaluatedFromFullSliceProductLeft params strategy family) (evaluatedFromFullSliceProductRight params strategy family) (commDataProcessedGError params gamma zeta)) :
|evaluatedSliceABAAvg params strategy family - evaluatedSliceABABAvg params strategy family| ≤ 6 * √zeta + √(commDataProcessedGError params gamma zeta)

Combined closenessOfIP chain on the evaluated side (commutativity-G.tex lines 301, 334, 359-360, 394, 396), stated with the paper's displayed 6√ζ + √ν envelope.