Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.Commutativity.Main.Results

Section 11 commutativity: final results #

Top-level thm:com-main statement, lifting evaluated commutation back to full-slice commutation via the two-step Schwartz–Zippel marginalization.

The two-step lift uses a hybrid scalar/tensor architecture (Option 3): the public conclusion is an SDDOpRel on operator families, composed from scalar transport lemmas whose proofs internally use tensor-form intermediates for the PSD Schwartz–Zippel argument. See docs/decisions/713-scalar-tensor-decision.md.

References #

source
theorem MIPStarRE.LDT.Commutativity.comMain_of_commutativityPoints {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (gamma zeta : Error) (hnorm : strategy.state.IsNormalized) (hcomm : SDDOpRel strategy.state (uniformDistribution (GlobalVariance.PointPairQuestion params.next)) (CommutativityPoints.pointMeasurementProductLeft params.next strategy) (CommutativityPoints.pointMeasurementProductRight params.next strategy) (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.

source
theorem MIPStarRE.LDT.Commutativity.comMain {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (eps delta gamma zeta : Error) (hnorm : strategy.state.IsNormalized) (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.

source
theorem MIPStarRE.LDT.Commutativity.normalizationCondition {ι : Type u_1} [Fintype ι] [DecidableEq ι] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA ι) (Q : ProjSubMeas OutcomeB ι) :
NormalizationConditionStatement P Q

lem:normalization-condition.