Section 11 commutativity: the reverse insertions of the evaluated-slice paper chain

The two reverse eq:add-an-a bounds after the paper line-87 phase-five removal, packaged into the combined phase-67 bridge consumed by ProcessedG: the counterpart of Commutativity/ScalarApproximation/PaperChainReverse.lean under MIPRE/Background/LIDT/MIPStarRE/LDT/ in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

evaluatedSlice_phaseSixSeven_reverse_bound drops the vendored hypothesis hnorm : strategy.state.IsNormalized, a theorem of the model, so its arguments are params strategy zeta family hcombined_fst hcombined_snd; the two hypotheses are stated with evaluatedPointFamilyLeft strategy.state and Preliminaries.totalSandwichFamily strategy.state, which take the model explicitly in the port.

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.evaluatedSlice_phaseSixSeven_reverse_bound {𝔓 : 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) (zeta : ℝ) (family : IdxPolyFamily params 𝔓) (hcombined_fst : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => evaluatedPointFamilyLeft strategy.state params family q.1) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => Preliminaries.totalSandwichFamily strategy.state (evaluatedPointFamily params family) (evaluatedSlicePointMeas params strategy) q.1) (4 * zeta)) (hcombined_snd : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => evaluatedPointFamilyLeft strategy.state params family q.2) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => Preliminaries.totalSandwichFamily strategy.state (evaluatedPointFamily params family) (evaluatedSlicePointMeas params strategy) q.2) (4 * zeta)) : have 𝒟 := MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params); have phase5PaperRemoved := evaluatedSlicePhaseFivePaperRemoved params strategy family; have phase7GonnaCite := evaluatedSlicePhaseSevenGonnaCite params strategy family; |MIPStarRE.LDT.avgOver 𝒟 phase5PaperRemoved - MIPStarRE.LDT.avgOver 𝒟 phase7GonnaCite| ≤ 4 * √zeta

Paper lines 99--104: the combined phase-67 reverse-insertion bridge.

The scalar-chain assembly only needs the endpoint comparison from the paper line-87/eq:gcom10 term to eq:gonna-cite-this-in-just-a-bit. This lemma packages the two proved eq:add-an-a reverse insertions (2√ζ each) through one triangle inequality, so downstream code no longer has to carry the intermediate phase-six endpoint.