Section 11 commutativity: final results

The top-level thm:com-main statement, lifting evaluated commutation back to full-slice commutation via the two-step Schwartz–Zippel marginalization, and lem:normalization-condition: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Main/Results.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The conclusions are SDDOpRels of joint operator families on the symmetric model strategy.state of a SymStrat params.next 𝔓 K; lem:normalization-condition is about local operators of any C*-algebra 𝔓 with its order, with star for the vendored ᴴ.

The vendored hypothesis hnorm : strategy.state.IsNormalized is dropped from comMain_of_commutativityPoints (where it stood between gamma zeta and hcomm) and from comMain (between eps delta gamma zeta and hgood), as the port conventions drop hψ : ψ.IsNormalized: none of the lemmas the proofs compose takes it any more. Callers pass params strategy gamma zeta hcomm hgamma_nonneg family hcons hself hbound and params strategy eps delta gamma zeta hgood family hcons hself hbound. The nonnegativity of gamma in comMain is gamma_nonneg_of_isGood, which the vendored proof inlines.

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-points.tex
• references/ldt-paper/commutativity-G.tex
• blueprint/src/chapter/ch08_commutativity.tex

theorem MIPRE.LIDT.Co.Commutativity.comMain_of_commutativityPoints {𝔓 : 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) (gamma zeta : ℝ) (hcomm : strategy.state.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.GlobalVariance.PointPairQuestion params.next)) (CommutativityPoints.pointMeasurementProductLeft params.next strategy) (CommutativityPoints.pointMeasurementProductRight params.next strategy) (MIPStarRE.LDT.CommutativityPoints.commutativityPointsError params.next gamma)) (hgamma_nonneg : 0 ≤ gamma) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) : ComMainConclusion params strategy family gamma zeta

Paper origin: references/ldt-paper/commutativity-G.tex (\label{thm:com-main}).

The paper theorem is formulated directly for the family family.meas; any explicit auxiliary family used by the scalar approximation proof is internal to the proof.

theorem MIPRE.LIDT.Co.Commutativity.comMain {𝔓 : 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) (eps delta gamma zeta : ℝ) (hgood : strategy.IsGood eps delta gamma) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) (hself : family.StronglySelfConsistent strategy.state zeta) (hbound : IdxPolyFamily.SliceBoundednessInput strategy family zeta) : ComMainConclusion params strategy family gamma zeta

Paper origin: references/ldt-paper/commutativity-G.tex (\label{thm:com-main}).

The paper theorem is formulated directly for the family family.meas; any explicit auxiliary family used by the scalar approximation proof is internal to the proof.

theorem MIPRE.LIDT.Co.Commutativity.normalizationCondition {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {OutcomeA : Type u_3} {OutcomeB : Type u_4} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA 𝔓) (Q : ProjSubMeas OutcomeB 𝔓) : NormalizationConditionStatement P Q

lem:normalization-condition.