Section 11 commutativity: the tail endpoints of the evaluated-slice paper chain

The two postprocessed self-consistency moves at the end of the paper-faithful scalar chain: the counterpart of Commutativity/ScalarApproximation/PaperChainTail.lean under MIPRE/Background/LIDT/MIPStarRE/LDT/ in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

Both lemmas drop the vendored hypothesis hnorm : strategy.state.IsNormalized, a theorem of the model, so their arguments are params strategy zeta family hpostSSC_snd; hpostSSC_snd is stated with evaluatedPointFamilyLeft strategy.state and evaluatedPointFamilyRight strategy.state, which take the model explicitly in the port. The vendored proof of the phase-nine bound obtains the self-adjointness of the placed families from Matrix.PosSemidef; here it is IsSelfAdjoint.of_nonneg, and the right placement commutes past the left one by rightTensor_mul_leftTensor_eq_opTensor.

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_phaseEight_tail_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 𝔓) (hpostSSC_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) => evaluatedPointFamilyRight strategy.state params family q.2) zeta) : have 𝒟 := MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params); have phase7GonnaCite := evaluatedSlicePhaseSevenGonnaCite params strategy family; have phase8TailRight := evaluatedSlicePhaseEightTailRight params strategy family; |MIPStarRE.LDT.avgOver 𝒟 phase7GonnaCite - MIPStarRE.LDT.avgOver 𝒟 phase8TailRight| ≤ √zeta

Paper line 117--118: move the second-coordinate factor to the right register.

theorem MIPRE.LIDT.Co.Commutativity.evaluatedSlice_phaseNine_tail_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 𝔓) (hpostSSC_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) => evaluatedPointFamilyRight strategy.state params family q.2) zeta) : have 𝒟 := MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params); have phase8TailRight := evaluatedSlicePhaseEightTailRight params strategy family; have avgBAB := fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => ∑ ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params, evaluatedSliceBABTerm params strategy family q ab; |MIPStarRE.LDT.avgOver 𝒟 phase8TailRight - MIPStarRE.LDT.avgOver 𝒟 avgBAB| ≤ √zeta

Paper line 118--119: move the second-coordinate factor back to the left register.