Section 3 — Definitions

Core definitions for the low individual degree test: evaluation families, matching mass, consistency defect, and test-passing predicates.

All operator fields now use Op ι directly with a generic Fintype index ι.

noncomputable def MIPStarRE.LDT.evaluateAt {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (u : Point params) (G : SubMeas (Polynomial params) ι) : SubMeas (Fq params) ι

Evaluate a polynomial-valued submeasurement at a point.

Equations

• MIPStarRE.LDT.evaluateAt params u G = MIPStarRE.LDT.postprocess G fun (g : MIPStarRE.LDT.Polynomial params) => g.toFun u

@[simp]

theorem MIPStarRE.LDT.evaluateAt_postprocess_appendAtHeight_appendPoint {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (G : SubMeas (Polynomial params) ι) (x : Fq params) (u : Point params) (y : Fq params) : evaluateAt params.next (appendPoint params u y) (postprocess G fun (g : Polynomial params) => Polynomial.appendAtHeight params g x) = evaluateAt params u G

Evaluation after adjoining an unused coordinate agrees with evaluation before adjoining that coordinate.

noncomputable def MIPStarRE.LDT.polynomialEvaluationFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (G : SubMeas (Polynomial params) ι) : IdxSubMeas (Point params) (Fq params) ι

View a global polynomial submeasurement as a point-indexed answer family.

Equations

• MIPStarRE.LDT.polynomialEvaluationFamily params G u = MIPStarRE.LDT.evaluateAt params u G

noncomputable def MIPStarRE.LDT.polynomialEvaluationMeasurementFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (G : Measurement (Polynomial params) ι) : IdxMeas (Point params) (Fq params) ι

View a global polynomial measurement as a point-indexed answer measurement family.

The submeasurement-valued polynomialEvaluationFamily is the form used by most consistency statements. The heterogeneous triangle step in the final theorem uses complete measurements, so this version keeps the same postprocessing while retaining the total-mass proof.

Equations

• MIPStarRE.LDT.polynomialEvaluationMeasurementFamily params G u = { toSubMeas := MIPStarRE.LDT.evaluateAt params u G.toSubMeas, total_eq_one := ⋯ }

@[reducible, inline]

noncomputable abbrev MIPStarRE.LDT.Test.polynomialEvaluationMeasurementFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (G : Measurement (Polynomial params) ι) : IdxMeas (Point params) (Fq params) ι

Namespace-compatible form of polynomialEvaluationMeasurementFamily.

This name is used by the two-space final-theorem route, where the surrounding theorems live in the Test namespace.

Equations

• MIPStarRE.LDT.Test.polynomialEvaluationMeasurementFamily params G = MIPStarRE.LDT.polynomialEvaluationMeasurementFamily params G

noncomputable def MIPStarRE.LDT.evaluateFiberFamilyAtNextPoint {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (G : IdxSubMeas (Fq params) (Polynomial params) ι) : IdxSubMeas (Point params.next) (Fq params) ι

Evaluate an indexed slice family at a point (u, x) in F_q^{m+1}.

Equations

• MIPStarRE.LDT.evaluateFiberFamilyAtNextPoint params G u = MIPStarRE.LDT.evaluateAt params (MIPStarRE.LDT.truncatePoint params u) (G (MIPStarRE.LDT.pointHeight params u))

noncomputable def MIPStarRE.LDT.qMatchMass {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A B : SubMeas Outcome ι) : Error

Questionwise matching mass ∑_a ⟨ψ, A_a B_a ψ⟩, summed over outcomes.

Equations

• MIPStarRE.LDT.qMatchMass ψ A B = ∑ a : Outcome, MIPStarRE.LDT.ev ψ (A.outcome a * B.outcome a)

noncomputable def MIPStarRE.LDT.qConsDefect {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A B : SubMeas Outcome ι) : Error

Questionwise off-diagonal mass surrogate for consistency.

Equations

• MIPStarRE.LDT.qConsDefect ψ A B = max 0 (MIPStarRE.LDT.ev ψ (A.total * B.total) - MIPStarRE.LDT.qMatchMass ψ A B)

noncomputable def MIPStarRE.LDT.qSDDCore {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A B : Outcome → Quantum.Op ι) : Error

Questionwise squared-distance defect.

Equations

• MIPStarRE.LDT.qSDDCore ψ A B = ∑ a : Outcome, MIPStarRE.LDT.ev ψ (Matrix.conjTranspose (A a - B a) * (A a - B a))

noncomputable def MIPStarRE.LDT.qSDD {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A B : SubMeas Outcome ι) : Error

Questionwise squared-distance defect.

Equations

• MIPStarRE.LDT.qSDD ψ A B = MIPStarRE.LDT.qSDDCore ψ A.outcome B.outcome

noncomputable def MIPStarRE.LDT.qSDDOp {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A B : OpFamily Outcome ι) : Error

State-dependent distance for raw operator families. Matches the paper's ≈_δ for arbitrary matrix families. This keeps the raw-family API separate while sharing the same core formula as qSDD.

Equations

• MIPStarRE.LDT.qSDDOp ψ A B = MIPStarRE.LDT.qSDDCore ψ A.outcome B.outcome

noncomputable def MIPStarRE.LDT.qSSCDefect {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A : SubMeas Outcome ι) : Error

Questionwise strong self-consistency defect.

Equations

• MIPStarRE.LDT.qSSCDefect ψ A = max 0 (MIPStarRE.LDT.ev ψ A.total - ∑ a : Outcome, MIPStarRE.LDT.ev ψ (A.outcome a * A.outcome a))

noncomputable def MIPStarRE.LDT.consError {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A B : IdxSubMeas Question Outcome ι) : Error

Averaged off-diagonal mass for consistency statements.

Equations

• MIPStarRE.LDT.consError ψ 𝒟 A B = MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => MIPStarRE.LDT.qConsDefect ψ (A q) (B q)

noncomputable def MIPStarRE.LDT.sddError {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A B : IdxSubMeas Question Outcome ι) : Error

Averaged squared distance for ≈_δ.

Equations

• MIPStarRE.LDT.sddError ψ 𝒟 A B = MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => MIPStarRE.LDT.qSDD ψ (A q) (B q)

noncomputable def MIPStarRE.LDT.sddErrorOp {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A B : IdxOpFamily Question Outcome ι) : Error

Averaged squared distance for raw operator families.

Equations

• MIPStarRE.LDT.sddErrorOp ψ 𝒟 A B = MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => MIPStarRE.LDT.qSDDOp ψ (A q) (B q)

noncomputable def MIPStarRE.LDT.sscError {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ι) : Error

Averaged defect in strong self-consistency.

Equations

• MIPStarRE.LDT.sscError ψ 𝒟 A = MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => MIPStarRE.LDT.qSSCDefect ψ (A q)

noncomputable def MIPStarRE.LDT.subMeasMass {Outcome : Type u_1} {ι : Type u_2} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (A : SubMeas Outcome ι) : Error

Total mass of a submeasurement on state ψ, computed from the concrete total operator.

Equations

• MIPStarRE.LDT.subMeasMass ψ A = MIPStarRE.LDT.ev ψ A.total

noncomputable def MIPStarRE.LDT.idxSubMeasMass {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ι) : Error

Averaged total mass of an indexed submeasurement.

Equations

• MIPStarRE.LDT.idxSubMeasMass ψ 𝒟 A = MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => MIPStarRE.LDT.subMeasMass ψ (A q)

noncomputable def MIPStarRE.LDT.bndError {Outcome : Type u_1} {ι : Type u_2} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (A : SubMeas Outcome ι) (Z : Quantum.Op ι) : Error

Defect in domination by an operator witness, measured at the expectation-value level.

Equations

• MIPStarRE.LDT.bndError ψ A Z = max 0 (MIPStarRE.LDT.subMeasMass ψ A - MIPStarRE.LDT.ev ψ Z)

noncomputable def MIPStarRE.LDT.qBipartiteMatchMass {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (ψ : QuantumState (ιA × ιB)) (A : SubMeas Outcome ιA) (B : SubMeas Outcome ιB) : Error

Bipartite matching mass ∑_a ⟨ψ, (A_a ⊗ B_a) ψ⟩, with A on the left register and B on the right register of a tensor-product state.

Equations

• MIPStarRE.LDT.qBipartiteMatchMass ψ A B = ∑ a : Outcome, MIPStarRE.LDT.ev ψ (MIPStarRE.LDT.opTensor (A.outcome a) (B.outcome a))

noncomputable def MIPStarRE.LDT.qBipartiteConsDefect {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (ψ : QuantumState (ιA × ιB)) (A : SubMeas Outcome ιA) (B : SubMeas Outcome ιB) : Error

Bipartite questionwise consistency defect.

In the paper (Definition 4.8), the consistency of A on H_A and B on H_B for a shared state |ψ⟩ ∈ H_A ⊗ H_B is: E_x ∑_{a≠b} ⟨ψ| A^x_a ⊗ B^x_b |ψ⟩ ≤ δ which equals max 0 (⟨ψ| A_total ⊗ B_total |ψ⟩ − ∑_a ⟨ψ| A_a ⊗ B_a |ψ⟩).

Equations

• MIPStarRE.LDT.qBipartiteConsDefect ψ A B = max 0 (MIPStarRE.LDT.ev ψ (MIPStarRE.LDT.opTensor A.total B.total) - MIPStarRE.LDT.qBipartiteMatchMass ψ A B)

noncomputable def MIPStarRE.LDT.bipartiteConsError {Question : Type u_1} {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (ψ : QuantumState (ιA × ιB)) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ιA) (B : IdxSubMeas Question Outcome ιB) : Error

Averaged bipartite off-diagonal mass for consistency statements.

Equations

• MIPStarRE.LDT.bipartiteConsError ψ 𝒟 A B = MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => MIPStarRE.LDT.qBipartiteConsDefect ψ (A q) (B q)

theorem MIPStarRE.LDT.qBipartiteConsDefect_eq_qConsDefect_placed {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (ψ : QuantumState (ιA × ιB)) (A : SubMeas Outcome ιA) (B : SubMeas Outcome ιB) : qBipartiteConsDefect ψ A B = qConsDefect ψ (leftPlacedSubMeas A) (rightPlacedSubMeas B)

Bridge lemma: the bipartite consistency defect equals the same-space qConsDefect applied to the left/right-placed submeasurements.

theorem MIPStarRE.LDT.bipartiteConsError_eq_consError_placed {Question : Type u_1} {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (ψ : QuantumState (ιA × ιB)) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ιA) (B : IdxSubMeas Question Outcome ιB) : bipartiteConsError ψ 𝒟 A B = consError ψ 𝒟 (fun (q : Question) => leftPlacedSubMeas (A q)) fun (q : Question) => rightPlacedSubMeas (B q)

Bridge lemma: averaged bipartite consistency equals the same-space consError applied to the left/right-placed families.

structure MIPStarRE.LDT.ConsRel {Question : Type u_1} {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (ψ : QuantumState (ιA × ιB)) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ιA) (B : IdxSubMeas Question Outcome ιB) (δ : Error) : Prop

Consistency relation (bipartite, paper Definition 4.8).

The state ψ lives on H_A ⊗ H_B, Alice's submeasurement A acts on H_A, and Bob's submeasurement B acts on H_B. The relation encodes E_{x ∼ D} ∑_{a≠b} ⟨ψ| A^x_a ⊗ B^x_b |ψ⟩ ≤ δ.

• offDiagonalBound : bipartiteConsError ψ 𝒟 A B ≤ δ

structure MIPStarRE.LDT.SDDRel {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A B : IdxSubMeas Question Outcome ι) (δ : Error) : Prop

State-dependent distance relation.

• squaredDistanceBound : sddError ψ 𝒟 A B ≤ δ

structure MIPStarRE.LDT.SDDOpRel {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A B : IdxOpFamily Question Outcome ι) (δ : Error) : Prop

State-dependent distance relation for raw operator families.

• squaredDistanceBound : sddErrorOp ψ 𝒟 A B ≤ δ

structure MIPStarRE.LDT.SSCRel {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ι) (δ : Error) : Prop

Strong self-consistency relation.

• diagonalOverlapBound : sscError ψ 𝒟 A ≤ δ

noncomputable def MIPStarRE.LDT.qBipartiteSSCDefect {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (A : SubMeas Outcome ι) : Error

Bipartite questionwise strong self-consistency defect. This is the paper's SSC condition (Definition 4.3/4.4): max 0 (∑ₐ ev ψ (Aₐ ⊗ I) − ∑ₐ ev ψ (Aₐ ⊗ Aₐ)). It measures the gap between the total mass on one register and the diagonal cross-register overlap.

Equations

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

noncomputable def MIPStarRE.LDT.bipartiteSSCError {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ι) : Error

Averaged bipartite SSC defect.

Equations

• MIPStarRE.LDT.bipartiteSSCError ψ 𝒟 A = MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => MIPStarRE.LDT.qBipartiteSSCDefect ψ (A q)

structure MIPStarRE.LDT.BipartiteSSCRel {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ι) (δ : Error) : Prop

Bipartite strong self-consistency relation (paper's definition). Uses the cross-register overlap ∑ₐ ev ψ (Aₐ ⊗ Aₐ) rather than the local square ∑ₐ ev ψ (Aₐ² ⊗ I).

• overlapBound : bipartiteSSCError ψ 𝒟 A ≤ δ

structure MIPStarRE.LDT.CompletenessAtLeast {Outcome : Type u_1} {ι : Type u_2} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (A : SubMeas Outcome ι) (r : Error) : Prop

Completeness statement for a submeasurement.

• lowerBound : subMeasMass ψ A ≥ r

structure MIPStarRE.LDT.BoundedByOperator {Outcome : Type u_1} {ι : Type u_2} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (A : SubMeas Outcome ι) (Z : Quantum.Op ι) (δ : Error) : Prop

Boundedness statement witnessed by an operator.

• witnessOpPSD : 0 ≤ Z
• upperBound : bndError ψ A Z ≤ δ

Nonnegativity lemmas for defect measures

theorem MIPStarRE.LDT.qSDD_nonneg {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A B : SubMeas Outcome ι) : 0 ≤ qSDD ψ A B

The squared-distance defect is nonneg since each summand is ⟨ψ, M†M ψ⟩ ≥ 0.

theorem MIPStarRE.LDT.sddError_nonneg {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A B : IdxSubMeas Question Outcome ι) : 0 ≤ sddError ψ 𝒟 A B

The averaged squared-distance error is nonneg.

theorem MIPStarRE.LDT.qBipartiteConsDefect_nonneg {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (ψ : QuantumState (ιA × ιB)) (A : SubMeas Outcome ιA) (B : SubMeas Outcome ιB) : 0 ≤ qBipartiteConsDefect ψ A B

The bipartite consistency defect is nonneg by definition (max 0 _).

theorem MIPStarRE.LDT.bipartiteConsError_nonneg {Question : Type u_1} {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (ψ : QuantumState (ιA × ιB)) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ιA) (B : IdxSubMeas Question Outcome ιB) : 0 ≤ bipartiteConsError ψ 𝒟 A B

The averaged bipartite consistency error is nonneg.

theorem MIPStarRE.LDT.qBipartiteMatchMass_nonneg {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (ψ : QuantumState (ιA × ιB)) (A : SubMeas Outcome ιA) (B : SubMeas Outcome ιB) : 0 ≤ qBipartiteMatchMass ψ A B

The bipartite matching mass is nonnegative because each summand is the expectation of a positive semidefinite tensor product.

theorem MIPStarRE.LDT.qBipartiteConsDefect_le_one_of_isNormalized {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (ψ : QuantumState (ιA × ιB)) (hψ : ψ.IsNormalized) (A : SubMeas Outcome ιA) (B : SubMeas Outcome ιB) : qBipartiteConsDefect ψ A B ≤ 1

For a normalized state, a bipartite consistency defect is at most 1.

theorem MIPStarRE.LDT.bipartiteConsError_le_one_of_isProbability {Question : Type u_1} {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (ψ : QuantumState (ιA × ιB)) (hψ : ψ.IsNormalized) (𝒟 : Distribution Question) (h𝒟 : 𝒟.IsProbability) (A : IdxSubMeas Question Outcome ιA) (B : IdxSubMeas Question Outcome ιB) : bipartiteConsError ψ 𝒟 A B ≤ 1

Under a probability question distribution, the averaged bipartite consistency error is bounded by 1.

theorem MIPStarRE.LDT.bipartiteConsError_uniform_le_one {Question : Type u_1} {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype Question] [DecidableEq Question] [Nonempty Question] [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (ψ : QuantumState (ιA × ιB)) (hψ : ψ.IsNormalized) (A : IdxSubMeas Question Outcome ιA) (B : IdxSubMeas Question Outcome ιB) : bipartiteConsError ψ (uniformDistribution Question) A B ≤ 1

Under the uniform question distribution, the averaged bipartite consistency error is bounded by 1.

theorem MIPStarRE.LDT.qBipartiteSSCDefect_nonneg {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (A : SubMeas Outcome ι) : 0 ≤ qBipartiteSSCDefect ψ A

The bipartite strong self-consistency defect is nonneg by definition (max 0 _).

theorem MIPStarRE.LDT.bipartiteSSCError_nonneg {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ι) : 0 ≤ bipartiteSSCError ψ 𝒟 A

The averaged bipartite strong self-consistency error is nonneg.

Postprocessing preserves totals

theorem MIPStarRE.LDT.postprocess_total {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype α] [Fintype β] (A : SubMeas α ι) (f : α → β) : (postprocess A f).total = A.total

Postprocessing preserves the total operator.

theorem MIPStarRE.LDT.qSDD_self {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A : SubMeas Outcome ι) : qSDD ψ A A = 0

The self-distance qSDD ψ A A is zero.

theorem MIPStarRE.LDT.sddError_self {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ι) : sddError ψ 𝒟 A A = 0

The averaged self-distance sddError ψ 𝒟 A A is zero.