Preliminary comparison theorems: core layer

Core comparison lemmas and measurement-agreement translations for the preliminaries chapter: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/ComparisonCore.lean in the port of planning/c6b-plan.md (milestone M0, section "Port conventions").

As in Co/Preliminaries/Defs.lean, the declarations live in MIPRE.LIDT.Co.Preliminaries and take the symmetric model S : SymModel 𝔓 K as an ordinary explicit argument in place of the vendored state ψ (simeqToApprox S 𝒟 A B δ); ConsRel.mono lives in the namespace of the ported relation, MIPRE.LIDT.Co.SymModel.ConsRel, so that h.mono hδ works on h : S.ConsRel 𝒟 A B δ. Local families have their operators in 𝔓; the same-space statements questionSDD_le_two_questionConsistency and qSDDOp_symm are about joint operators, in K →L[ℂ] K, and take a vector state S : VecState K (Co/Basic/QuantumState.lean; a symmetric model is accepted through its coercion); conjTranspose_mul_mono holds in any star-ordered ring.

The vendored proof of simeqToApprox lifts the two measurements to the joint space and applies the same-space bound. Here its per-question core is the repository's cross-party bound MIPRE.BipartiteModel.xSqNorm_sum_le_two_mul (MIPRE/Foundations/CrossConsistency.lean) on S.toBipartite, through VecState.qSDDCore_eq_sum_snorm_sq of Co/Test/Defs.lean: this is questionSDD_liftLeft_liftRight_le_two_questionConsistency. In the symmetric model the "heterogeneous" placements IdxSubMeas.placeLeft, placeRight are the lifts, so the heterogeneous statements follow from the same-space ones by rfl.

New here

• questionSDD_liftLeft_liftRight_le_two_questionConsistency: for two measurements on the local algebra, the squared distance of their left and right lifts is at most twice their bipartite consistency defect (the per-question core of simeqToApprox).

Not ported

Every declaration of the vendored file has a counterpart here.

theorem MIPRE.LIDT.Co.SymModel.ConsRel.mono {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] {S : SymModel 𝔓 K} {𝒟 : MIPStarRE.LDT.Distribution Question} {A B : IdxSubMeas Question Outcome 𝔓} {δ δ' : ℝ} (hδ : δ ≤ δ') : S.ConsRel 𝒟 A B δ → S.ConsRel 𝒟 A B δ'

Monotonicity of ConsRel in the allowed error parameter.

theorem MIPRE.LIDT.Co.Preliminaries.postprocessPreservesMeasurements {α : Type u_1} {β : Type u_2} {R : Type u_3} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Fintype α] [Fintype β] (A : SubMeas α R) (f : α → β) : (postprocess A f).total = A.total

prop:post-processing-preserves.

Postprocessing preserves the total operator, so it preserves both the submeasurement and measurement conditions.

theorem MIPRE.LIDT.Co.Preliminaries.conjTranspose_mul_mono {R : Type u_1} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {X Y Z : R} (hXY : X ≤ Y) : star Z * X * Z ≤ star Z * Y * Z

Loewner-order monotonicity of the sandwich Z* X Z. If X ≤ Y then Z* X Z ≤ Z* Y Z.

theorem MIPRE.LIDT.Co.Preliminaries.simeqForMeasurements {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxMeas Question Outcome 𝔓) (δ : ℝ) : S.ConsRel 𝒟 A.toIdxSubMeas B.toIdxSubMeas δ ↔ ConsAgreement S 𝒟 A B δ

prop:simeq-for-measurements.

theorem MIPRE.LIDT.Co.Preliminaries.questionSDD_le_two_questionConsistency {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : VecState K) (A B : Measurement Outcome (K →L[ℂ] K)) : S.qSDD A.toSubMeas B.toSubMeas ≤ 2 * S.qConsDefect A.toSubMeas B.toSubMeas

Atomic mathematical fact: for a full measurement, the squared-distance defect is at most 2 * qConsDefect.

theorem MIPRE.LIDT.Co.Preliminaries.questionSDD_liftLeft_liftRight_le_two_questionConsistency {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : SymModel 𝔓 K) (A B : Measurement Outcome 𝔓) : S.qSDD (SubMeas.liftLeft S A.toSubMeas) (SubMeas.liftRight S B.toSubMeas) ≤ 2 * S.qBipartiteConsDefect A.toSubMeas B.toSubMeas

For two measurements on the local algebra, the squared distance of the left and right lifts is at most twice their bipartite consistency defect: the per-question core of simeqToApprox. It is the repository's MIPRE.BipartiteModel.xSqNorm_sum_le_two_mul on S.toBipartite.

theorem MIPRE.LIDT.Co.Preliminaries.simeqToApprox {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxMeas Question Outcome 𝔓) (δ : ℝ) : S.ConsRel 𝒟 A.toIdxSubMeas B.toIdxSubMeas δ → BipartiteSDDRel S 𝒟 A.toIdxSubMeas B.toIdxSubMeas (2 * δ)

prop:simeq-to-approx.

theorem MIPRE.LIDT.Co.Preliminaries.simeqToApprox_heterogeneous {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxMeas Question Outcome 𝔓) (δ : ℝ) : S.ConsRel 𝒟 A.toIdxSubMeas B.toIdxSubMeas δ → S.SDDRel 𝒟 (IdxSubMeas.placeLeft S A.toIdxSubMeas) (IdxSubMeas.placeRight S B.toIdxSubMeas) (2 * δ)

Heterogeneous form of prop:simeq-to-approx.

The paper's consistency relation is naturally bipartite: Alice's measurement acts on the first factor and Bob's on the second. This theorem is the same calculation as simeqToApprox, expressed with the placements IdxSubMeas.placeLeft and IdxSubMeas.placeRight, which in the symmetric model are the lifts.

theorem MIPRE.LIDT.Co.Preliminaries.ev_leftTensor_mul_rightTensor_nonneg {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {X Y : 𝔓} (hX : 0 ≤ X) (hY : 0 ≤ Y) : 0 ≤ S.ev (S.L X * S.R Y)

The expectation of X ⊗ Y is nonnegative for positive X and Y.

theorem MIPRE.LIDT.Co.Preliminaries.qMatchMass_leftRight_postprocess_ge {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (A B : SubMeas α 𝔓) (f : α → β) : S.qMatchMass (S.leftPlacedSubMeas (postprocess A f)) (S.rightPlacedSubMeas (postprocess B f)) ≥ S.qMatchMass (S.leftPlacedSubMeas A) (S.rightPlacedSubMeas B)

Postprocessing two opposite-side families by the same readout map can only increase their matching mass: the new diagonal terms are the old ones plus nonnegative cross terms within each fibre.

theorem MIPRE.LIDT.Co.Preliminaries.qBipartiteSSCDefect_postprocess_le {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (M : SubMeas α 𝔓) (f : α → β) : S.qBipartiteSSCDefect (postprocess M f) ≤ S.qBipartiteSSCDefect M

Postprocessing can only decrease the bipartite strong self-consistency defect: the total mass is preserved while the diagonal overlap term can only increase.

theorem MIPRE.LIDT.Co.Preliminaries.qConsDefect_leftRight_postprocess_le {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (A B : SubMeas α 𝔓) (f : α → β) : S.qConsDefect (S.leftPlacedSubMeas (postprocess A f)) (S.rightPlacedSubMeas (postprocess B f)) ≤ S.qConsDefect (S.leftPlacedSubMeas A) (S.rightPlacedSubMeas B)

Postprocessing two opposite-side families by the same readout map can only decrease their consistency defect: the total overlap is preserved and the matching mass can only increase.

theorem MIPRE.LIDT.Co.Preliminaries.consRelDataProcessing_questionDependent {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxSubMeas Question α 𝔓) (δ : ℝ) (f : Question → α → β) : S.ConsRel 𝒟 A B δ → S.ConsRel 𝒟 (fun (q : Question) => postprocess (A q) (f q)) (fun (q : Question) => postprocess (B q) (f q)) δ

Question-dependent postprocessing preserves bipartite consistency.

theorem MIPRE.LIDT.Co.Preliminaries.simeqDataProcessing_heterogeneous {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxMeas Question α 𝔓) (δ : ℝ) (f : α → β) : S.ConsRel 𝒟 A.toIdxSubMeas B.toIdxSubMeas δ → S.ConsRel 𝒟 (fun (q : Question) => postprocess (A q).toSubMeas f) (fun (q : Question) => postprocess (B q).toSubMeas f) δ

Heterogeneous form of prop:simeq-data-processing.

This is the paper-faithful opposite-side statement: the two families are first placed on opposite tensor factors of a bipartite state, and only then postprocessed. The generic same-side qConsDefect monotonicity statement is false for arbitrary noncommuting submeasurements.

theorem MIPRE.LIDT.Co.Preliminaries.simeqDataProcessing {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxMeas Question α 𝔓) (δ : ℝ) (f : α → β) : S.ConsRel 𝒟 A.toIdxSubMeas B.toIdxSubMeas δ → S.ConsRel 𝒟 (fun (q : Question) => postprocess (A q).toSubMeas f) (fun (q : Question) => postprocess (B q).toSubMeas f) δ

prop:simeq-data-processing.

This is the source-labelled same-space statement. The proof is the heterogeneous opposite-side data-processing theorem specialized to equal local spaces.

theorem MIPRE.LIDT.Co.Preliminaries.consRel_uniform_prod_fst {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} {β : Type u_4} {Outcome : Type u_5} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] [Fintype Outcome] (S : SymModel 𝔓 K) (A B : IdxSubMeas α Outcome 𝔓) (δ : ℝ) (hAB : S.ConsRel (MIPStarRE.LDT.uniformDistribution α) A B δ) : S.ConsRel (MIPStarRE.LDT.uniformDistribution (α × β)) (fun (ab : α × β) => A ab.1) (fun (ab : α × β) => B ab.1) δ

If a uniformly sampled consistency statement depends only on the first coordinate of a product question, it lifts to the full product with the same error.

theorem MIPRE.LIDT.Co.Preliminaries.consRel_uniform_equiv {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} {β : Type u_4} {Outcome : Type u_5} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] [Fintype Outcome] (e : α ≃ β) (S : SymModel 𝔓 K) (A B : IdxSubMeas α Outcome 𝔓) (δ : ℝ) : S.ConsRel (MIPStarRE.LDT.uniformDistribution α) A B δ ↔ S.ConsRel (MIPStarRE.LDT.uniformDistribution β) (fun (b : β) => A (e.symm b)) (fun (b : β) => B (e.symm b)) δ

Reindexing a uniformly sampled consistency statement along an equivalence.

theorem MIPRE.LIDT.Co.Preliminaries.qSDDOp_symm {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : VecState K) (A B : OpFamily Outcome (K →L[ℂ] K)) : S.qSDDOp A B = S.qSDDOp B A

qSDDOp is symmetric: swapping the two operator families gives the same squared-distance sum.