Preliminary definitions and statement structures

This file collects the lightweight statement and definition layer for the preliminaries chapter of the LDT development. It records the paper's consistency, sandwich, and completion statements in a form used by later files. This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/Defs.lean in the port of planning/c6b-plan.md (milestone M0, section "Port conventions").

The declarations live in MIPRE.LIDT.Co.Preliminaries, mirroring the vendored MIPStarRE.LDT.Preliminaries. Since dot notation on S : SymModel 𝔓 K only reaches MIPRE.LIDT.Co.SymModel, the model is an ordinary explicit argument here: it takes the place of the vendored state ψ where the vendored declaration has one (agreementProbability ψ 𝒟 A B is agreementProbability S 𝒟 A B), and is a new first explicit argument where it has none (diagonalSandwichFamily A B is diagonalSandwichFamily S A B), as for the lifts IdxSubMeas.liftLeft S A of Co/Basic/SubMeasurementFamilies.lean.

Local families (the vendored IdxSubMeas Question Outcome ι) have their operators in 𝔓, and the placed and sandwich families, which act on the joint space, in K →L[ℂ] K. The vendored CompTransferStmt is about a state on a single space ι, so it takes a vector state V : VecState K (Co/Basic/QuantumState.lean) and joint families.

In the symmetric model both tensor factors are 𝔓, so the "two-space" declarations (heterogeneousDiagonalSandwichFamily, heterogeneousTotalSandwichFamily, ConsSubMeasHeterogeneousStmt) have the same types as their same-space versions; they are kept, with the same bodies, so that the vendored callers of either form port as they stand, and the families agree by rfl (heterogeneousDiagonalSandwichFamily_eq, heterogeneousTotalSandwichFamily_eq).

Main definitions

• BipartiteSDDRel: the paper-style left/right state-dependent distance relation.
• ConsAgreement: the measurement reformulation of consistency.
• ConsSubMeasStmt, SwitchSandwichStmt, CompTransferStmt, and CompletingToMeasStmt: conclusion statements for the main preliminary propositions.
• completeAtOutcome: completion of a submeasurement at a distinguished outcome.

New here

• heterogeneousDiagonalSandwichFamily_eq, heterogeneousTotalSandwichFamily_eq: in the symmetric model the two-space sandwich families are the same-space ones (rfl).

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/preliminaries.tex

Consistency and distance statements

structure MIPRE.LIDT.Co.Preliminaries.BipartiteSDDRel {𝔓 : 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 𝔓) (δ : ℝ) : Prop

Source-style left/right relation A^x_a ⊗ I ≈_δ I ⊗ B^x_a.

• leftRightSquaredDistanceBound : S.sddError 𝒟 (IdxSubMeas.liftLeft S A) (IdxSubMeas.liftRight S B) ≤ δ

structure MIPRE.LIDT.Co.Preliminaries.OpBounded01 {R : Type u_3} [Ring R] [PartialOrder R] (B : R) : Prop

Condition 0 ≤ B ≤ I for the switch-sandwich argument.

• nonnegative : 0 ≤ B
• boundedByIdentity : 0 ≤ 1 - B

noncomputable def MIPRE.LIDT.Co.Preliminaries.agreementProbability {𝔓 : 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 𝔓) : ℝ

Agreement probability from prop:simeq-for-measurements.

Equations

• MIPRE.LIDT.Co.Preliminaries.agreementProbability S 𝒟 A B = 1 - S.bipartiteConsError 𝒟 A.toIdxSubMeas B.toIdxSubMeas

structure MIPRE.LIDT.Co.Preliminaries.ConsAgreement {𝔓 : 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 𝔓) (δ : ℝ) : Prop

Conclusion statement for the measurement reformulation of consistency.

• agreementLowerBound : agreementProbability S 𝒟 A B ≥ 1 - δ

theorem MIPRE.LIDT.Co.Preliminaries.diagonalSandwichFamily_total_le_one {𝔓 : 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) (A : IdxSubMeas Question Outcome 𝔓) (B : IdxMeas Question Outcome 𝔓) (q : Question) : ∑ a : Outcome, S.L ((A q).outcome a) * S.R ((B q).outcome a) ≤ 1

A diagonal sandwich family has total operator at most the identity.

theorem MIPRE.LIDT.Co.Preliminaries.totalSandwichFamily_total_le_one {𝔓 : 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) (A : IdxSubMeas Question Outcome 𝔓) (B : IdxMeas Question Outcome 𝔓) (q : Question) : ∑ a : Outcome, S.L (A q).total * S.R ((B q).outcome a) ≤ 1

A total sandwich family has total operator at most the identity.

noncomputable def MIPRE.LIDT.Co.Preliminaries.diagonalSandwichFamily {𝔓 : 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) (A : IdxSubMeas Question Outcome 𝔓) (B : IdxMeas Question Outcome 𝔓) : IdxSubMeas Question Outcome (K →L[ℂ] K)

A_a ⊗ B_a, the diagonal bipartite family from prop:cons-sub-meas.

This same-space version is the specialization used by the existing main-theorem path. The paper-facing two-space version is heterogeneousDiagonalSandwichFamily.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.Preliminaries.totalSandwichFamily {𝔓 : 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) (A : IdxSubMeas Question Outcome 𝔓) (B : IdxMeas Question Outcome 𝔓) : IdxSubMeas Question Outcome (K →L[ℂ] K)

A ⊗ B_a, the total bipartite family from prop:cons-sub-meas.

This same-space version is the specialization used by the existing main-theorem path. The paper-facing two-space version is heterogeneousTotalSandwichFamily.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.Preliminaries.heterogeneousDiagonalSandwichFamily {𝔓 : 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) (A : IdxSubMeas Question Outcome 𝔓) (B : IdxMeas Question Outcome 𝔓) : IdxSubMeas Question Outcome (K →L[ℂ] K)

A_a ⊗ B_a for the two-space statement of prop:cons-sub-meas.

Here A acts on the left tensor factor and B on the right one (S.L and S.R). In the symmetric model both factors are 𝔓, so this is diagonalSandwichFamily by rfl (heterogeneousDiagonalSandwichFamily_eq).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.Preliminaries.heterogeneousTotalSandwichFamily {𝔓 : 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) (A : IdxSubMeas Question Outcome 𝔓) (B : IdxMeas Question Outcome 𝔓) : IdxSubMeas Question Outcome (K →L[ℂ] K)

A ⊗ B_a for the two-space statement of prop:cons-sub-meas.

The total operator A^x = ∑_a A^x_a remains on the left tensor factor, while the measurement outcome B^x_a remains on the right tensor factor. In the symmetric model this is totalSandwichFamily by rfl (heterogeneousTotalSandwichFamily_eq).

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LIDT.Co.Preliminaries.heterogeneousDiagonalSandwichFamily_eq {𝔓 : 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) (A : IdxSubMeas Question Outcome 𝔓) (B : IdxMeas Question Outcome 𝔓) : heterogeneousDiagonalSandwichFamily S A B = diagonalSandwichFamily S A B

In the symmetric model the two-space diagonal sandwich family is the same-space one.

theorem MIPRE.LIDT.Co.Preliminaries.heterogeneousTotalSandwichFamily_eq {𝔓 : 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) (A : IdxSubMeas Question Outcome 𝔓) (B : IdxMeas Question Outcome 𝔓) : heterogeneousTotalSandwichFamily S A B = totalSandwichFamily S A B

In the symmetric model the two-space total sandwich family is the same-space one.

structure MIPRE.LIDT.Co.Preliminaries.ConsSubMeasStmt {𝔓 : 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 : IdxSubMeas Question Outcome 𝔓) (B : IdxMeas Question Outcome 𝔓) (γ : ℝ) : Prop

Same-space output statement for prop:cons-sub-meas.

The paper-facing two-space output statement is ConsSubMeasHeterogeneousStmt.

• diagonalControl : S.SDDRel 𝒟 (IdxSubMeas.liftLeft S A) (diagonalSandwichFamily S A B) γ
• sandwichControl : S.SDDRel 𝒟 (diagonalSandwichFamily S A B) (totalSandwichFamily S A B) γ
• combinedControl : S.SDDRel 𝒟 (IdxSubMeas.liftLeft S A) (totalSandwichFamily S A B) (4 * γ)

structure MIPRE.LIDT.Co.Preliminaries.ConsSubMeasHeterogeneousStmt {𝔓 : 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 : IdxSubMeas Question Outcome 𝔓) (B : IdxMeas Question Outcome 𝔓) (γ : ℝ) : Prop

Two-space output statement for prop:cons-sub-meas.

It records the two estimates A^x_a ⊗ I ≈_γ A^x_a ⊗ B^x_a and A^x_a ⊗ B^x_a ≈_γ A^x ⊗ B^x_a, and the resulting 4γ estimate from A^x_a ⊗ I to A^x ⊗ B^x_a.

• diagonalControl : S.SDDRel 𝒟 (IdxSubMeas.placeLeft S A) (heterogeneousDiagonalSandwichFamily S A B) γ

  A^x_a ⊗ I is close to the diagonal family A^x_a ⊗ B^x_a.

• sandwichControl : S.SDDRel 𝒟 (heterogeneousDiagonalSandwichFamily S A B) (heterogeneousTotalSandwichFamily S A B) γ

  The diagonal family A^x_a ⊗ B^x_a is close to A^x ⊗ B^x_a.

• combinedControl : S.SDDRel 𝒟 (IdxSubMeas.placeLeft S A) (heterogeneousTotalSandwichFamily S A B) (4 * γ)

  The two preceding estimates give A^x_a ⊗ I ≈_{4γ} A^x ⊗ B^x_a.

Sandwich expectations

noncomputable def MIPRE.LIDT.Co.Preliminaries.leftSandwichExpectation {𝔓 : 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 : IdxProjSubMeas Question Outcome 𝔓) (B : 𝔓) : ℝ

Averaged left term E_x ∑_a ⟨ψ, (A_a B A_a ⊗ I) ψ⟩.

Equations

• MIPRE.LIDT.Co.Preliminaries.leftSandwichExpectation S 𝒟 A B = MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, S.ev (S.L ((A q).outcome a) * S.L B * S.L ((A q).outcome a))

noncomputable def MIPRE.LIDT.Co.Preliminaries.middleSandwichExpectation {𝔓 : 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 : IdxProjSubMeas Question Outcome 𝔓) (B : 𝔓) : ℝ

Averaged middle term E_x ∑_a ⟨ψ, (B ⊗ A_a) ψ⟩.

Equations

• MIPRE.LIDT.Co.Preliminaries.middleSandwichExpectation S 𝒟 A B = MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, S.ev (S.L B * S.R ((A q).outcome a))

noncomputable def MIPRE.LIDT.Co.Preliminaries.rightSandwichExpectation {𝔓 : 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 : IdxProjSubMeas Question Outcome 𝔓) (B : 𝔓) : ℝ

Averaged right term E_x ∑_a ⟨ψ, (B A_a ⊗ I) ψ⟩.

Equations

• MIPRE.LIDT.Co.Preliminaries.rightSandwichExpectation S 𝒟 A B = MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, S.ev (S.L (B * (A q).outcome a))

structure MIPRE.LIDT.Co.Preliminaries.SwitchSandwichStmt {𝔓 : 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 : IdxProjSubMeas Question Outcome 𝔓) (B : 𝔓) (δ : ℝ) : Prop

Conclusion statement for prop:switch-sandwich.

• leftSandwichTransfer : |leftSandwichExpectation S 𝒟 A B - middleSandwichExpectation S 𝒟 A B| ≤ 2 * √δ
• rightSandwichTransfer : |middleSandwichExpectation S 𝒟 A B - rightSandwichExpectation S 𝒟 A B| ≤ √δ

structure MIPRE.LIDT.Co.Preliminaries.CompTransferStmt {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome (K →L[ℂ] K)) (P : IdxProjSubMeas Question Outcome (K →L[ℂ] K)) (ε : ℝ) : Prop

Conclusion statement for prop:completeness-transfer-projective-P.

The vendored statement is about a state on a single space, so the state is a vector state V : VecState K (a symmetric model is accepted through its coercion) and A and P are families of joint operators.

• completenessTransfer : V.idxSubMeasMass 𝒟 A ≥ V.idxSubMeasMass 𝒟 P.toIdxSubMeas - 2 * √ε

Completion

theorem MIPRE.LIDT.Co.Preliminaries.completeAtOutcome_sum_eq_one {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {Outcome : Type u_2} [Fintype Outcome] [DecidableEq Outcome] (B : SubMeas Outcome R) (a0 : Outcome) : (∑ a : Outcome, if a = a0 then B.outcome a + (1 - B.total) else B.outcome a) = 1

The completed outcomes sum to the identity.

noncomputable def MIPRE.LIDT.Co.Preliminaries.completeAtOutcome {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {Outcome : Type u_2} [Fintype Outcome] (B : SubMeas Outcome R) (a0 : Outcome) : Measurement Outcome R

Canonical completion of B by adjoining the residual I - Σ_a B_a to the distinguished outcome a0.

Equations

• One or more equations did not get rendered due to their size.

structure MIPRE.LIDT.Co.Preliminaries.CompletingToMeasStmt {𝔓 : 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 : Measurement Outcome 𝔓) (B : SubMeas Outcome 𝔓) (C : Measurement Outcome 𝔓) (a0 : Outcome) (δ ζ : ℝ) : Prop

Analytic conclusion for prop:completing-to-measurement once a witness C has been fixed.

The theorem completingToMeasurement separately records that the chosen witness is the canonical completion completeAtOutcome B a0, so this structure stores only the closeness statement from the paper.

• closenessAfterCompletion : S.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (SubMeas.liftLeft S A.toSubMeas)) (constSubMeasFamily (SubMeas.liftLeft S C.toSubMeas)) (2 * δ + 4 * √δ + 2 * ζ)