Section 3 — Definitions

Core definitions for the low individual degree test: evaluation families, matching mass, consistency defect, and test-passing predicates. This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Test/Defs.lean in the port of planning/c6b-plan.md (milestone M0, section "Port conventions").

The evaluation families (evaluateAt, polynomialEvaluationFamily, ...) are generic over the ordered ⋆-ring R of Co/Basic/SubMeasurementCore.lean. The ev-level defects and relations are used with dot notation on the state: the vendored qSDD ψ A B is S.qSDD A B, SDDRel ψ 𝒟 A B δ is S.SDDRel 𝒟 A B δ.

• A same-space quantity (qMatchMass, qConsDefect, qSDDCore, qSDD, qSDDOp, qSSCDefect, consError, sddError, sddErrorOp, sscError, subMeasMass, idxSubMeasMass, bndError, SDDRel, SDDOpRel, SSCRel, CompletenessAtLeast, BoundedByOperator) uses only the state, so it is a VecState declaration (Co/Basic/QuantumState.lean), about joint operators in K →L[ℂ] K. It applies to any vector state, with no swap symmetry: the vendored uses with a state on one space, a reduced state or a state tensored with an ancilla (MakingMeasurementsProjective) port without building a symmetric model; and S.qSDD A B for S : SymModel 𝔓 K is S.toVecState.qSDD A B.
• A bipartite quantity (qBipartiteMatchMass, qBipartiteConsDefect, bipartiteConsError, ConsRel, qBipartiteSSCDefect, bipartiteSSCError, BipartiteSSCRel) places local families in 𝔓 on the two factors through S.opTensor, so it is a SymModel declaration. The two-space ProjStrat of Co/Test/StrategyCore.lean has no counterpart of these: see there.

As everywhere in the port, the normalization hypothesis hψ : ψ.IsNormalized of the vendored bounds is dropped: V.ev 1 = 1 is a theorem of every vector state.

New here

Three bridges to the repository calculus, through V.toStateModel and S.toBipartite (Co/Basic/QuantumState.lean):

• VecState.qSDDCore_eq_sum_snorm_sq: qSDDCore is ∑ₐ ‖(Aₐ - Bₐ) Ψ‖²;
• SymModel.bipartiteConsError_eq_inconsistency: for measurements, the bipartite consistency error is MIPRE.BipartiteModel.inconsistency (MIPRE/Foundations/ModelStrategy.lean) of the model, weighted by the distribution; its per-question form, for sub-measurements, is SymModel.qBipartiteConsDefect_eq_sum_ne, the off-diagonal Born mass;
• SymModel.sddError_liftLeft_liftRight_eq_xPovmDist: for measurements, the squared distance of the left and right lifts is MIPRE.BipartiteModel.xPovmDist (MIPRE/Foundations/CrossConsistency.lean).

Not ported

Every declaration of the vendored file has a counterpart here.

noncomputable def MIPRE.LIDT.Co.evaluateAt {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (u : MIPStarRE.LDT.Point params) (G : SubMeas (MIPStarRE.LDT.Polynomial params) R) : SubMeas (MIPStarRE.LDT.Fq params) R

Evaluate a polynomial-valued submeasurement at a point.

Equations

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

@[simp]

theorem MIPRE.LIDT.Co.evaluateAt_postprocess_appendAtHeight_appendPoint {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (G : SubMeas (MIPStarRE.LDT.Polynomial params) R) (x : MIPStarRE.LDT.Fq params) (u : MIPStarRE.LDT.Point params) (y : MIPStarRE.LDT.Fq params) : evaluateAt params.next (MIPStarRE.LDT.appendPoint params u y) (postprocess G fun (g : MIPStarRE.LDT.Polynomial params) => MIPStarRE.LDT.Polynomial.appendAtHeight params g x) = evaluateAt params u G

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

noncomputable def MIPRE.LIDT.Co.polynomialEvaluationFamily {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (G : SubMeas (MIPStarRE.LDT.Polynomial params) R) : IdxSubMeas (MIPStarRE.LDT.Point params) (MIPStarRE.LDT.Fq params) R

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

Equations

• MIPRE.LIDT.Co.polynomialEvaluationFamily params G u = MIPRE.LIDT.Co.evaluateAt params u G

noncomputable def MIPRE.LIDT.Co.polynomialEvaluationMeasurementFamily {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (G : Measurement (MIPStarRE.LDT.Polynomial params) R) : IdxMeas (MIPStarRE.LDT.Point params) (MIPStarRE.LDT.Fq params) R

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

• MIPRE.LIDT.Co.polynomialEvaluationMeasurementFamily params G u = { toSubMeas := MIPRE.LIDT.Co.evaluateAt params u G.toSubMeas, total_eq_one := ⋯ }

@[reducible, inline]

noncomputable abbrev MIPRE.LIDT.Co.Test.polynomialEvaluationMeasurementFamily {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (G : Measurement (MIPStarRE.LDT.Polynomial params) R) : IdxMeas (MIPStarRE.LDT.Point params) (MIPStarRE.LDT.Fq params) R

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

• MIPRE.LIDT.Co.Test.polynomialEvaluationMeasurementFamily params G = MIPRE.LIDT.Co.polynomialEvaluationMeasurementFamily params G

noncomputable def MIPRE.LIDT.Co.evaluateFiberFamilyAtNextPoint {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (G : IdxSubMeas (MIPStarRE.LDT.Fq params) (MIPStarRE.LDT.Polynomial params) R) : IdxSubMeas (MIPStarRE.LDT.Point params.next) (MIPStarRE.LDT.Fq params) R

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

Equations

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

Postprocessing preserves totals

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

Postprocessing preserves the total operator.

theorem MIPRE.LIDT.Co.avgOver_eq_sum_weight {Question : Type u_1} [Fintype Question] (𝒟 : MIPStarRE.LDT.Distribution Question) (f : Question → ℝ) : MIPStarRE.LDT.avgOver 𝒟 f = ∑ q : Question, 𝒟.weight q * f q

An average against a distribution, written over the whole question type.

Questionwise defects

noncomputable def MIPRE.LIDT.Co.VecState.qMatchMass {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Outcome : Type u_2} [Fintype Outcome] (A B : SubMeas Outcome (K →L[ℂ] K)) : ℝ

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

Equations

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

noncomputable def MIPRE.LIDT.Co.VecState.qConsDefect {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Outcome : Type u_2} [Fintype Outcome] (A B : SubMeas Outcome (K →L[ℂ] K)) : ℝ

Questionwise off-diagonal mass surrogate for consistency.

Equations

• V.qConsDefect A B = max 0 (V.ev (A.total * B.total) - V.qMatchMass A B)

noncomputable def MIPRE.LIDT.Co.VecState.qSDDCore {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Outcome : Type u_2} [Fintype Outcome] (A B : Outcome → K →L[ℂ] K) : ℝ

Questionwise squared-distance defect.

Equations

• V.qSDDCore A B = ∑ a : Outcome, V.ev (star (A a - B a) * (A a - B a))

noncomputable def MIPRE.LIDT.Co.VecState.qSDD {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Outcome : Type u_2} [Fintype Outcome] (A B : SubMeas Outcome (K →L[ℂ] K)) : ℝ

Questionwise squared-distance defect.

Equations

• V.qSDD A B = V.qSDDCore A.outcome B.outcome

noncomputable def MIPRE.LIDT.Co.VecState.qSDDOp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Outcome : Type u_2} [Fintype Outcome] (A B : OpFamily Outcome (K →L[ℂ] K)) : ℝ

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

Equations

• V.qSDDOp A B = V.qSDDCore A.outcome B.outcome

noncomputable def MIPRE.LIDT.Co.VecState.qSSCDefect {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Outcome : Type u_2} [Fintype Outcome] (A : SubMeas Outcome (K →L[ℂ] K)) : ℝ

Questionwise strong self-consistency defect.

Equations

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

Averaged defects

noncomputable def MIPRE.LIDT.Co.VecState.consError {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxSubMeas Question Outcome (K →L[ℂ] K)) : ℝ

Averaged off-diagonal mass for consistency statements.

Equations

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

noncomputable def MIPRE.LIDT.Co.VecState.sddError {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxSubMeas Question Outcome (K →L[ℂ] K)) : ℝ

Averaged squared distance for ≈_δ.

Equations

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

noncomputable def MIPRE.LIDT.Co.VecState.sddErrorOp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxOpFamily Question Outcome (K →L[ℂ] K)) : ℝ

Averaged squared distance for raw operator families.

Equations

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

noncomputable def MIPRE.LIDT.Co.VecState.sscError {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome (K →L[ℂ] K)) : ℝ

Averaged defect in strong self-consistency.

Equations

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

noncomputable def MIPRE.LIDT.Co.VecState.subMeasMass {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Outcome : Type u_2} [Fintype Outcome] (A : SubMeas Outcome (K →L[ℂ] K)) : ℝ

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

Equations

• V.subMeasMass A = V.ev A.total

noncomputable def MIPRE.LIDT.Co.VecState.idxSubMeasMass {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome (K →L[ℂ] K)) : ℝ

Averaged total mass of an indexed submeasurement.

Equations

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

noncomputable def MIPRE.LIDT.Co.VecState.bndError {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Outcome : Type u_2} [Fintype Outcome] (A : SubMeas Outcome (K →L[ℂ] K)) (Z : K →L[ℂ] K) : ℝ

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

Equations

• V.bndError A Z = max 0 (V.subMeasMass A - V.ev Z)

Relations

structure MIPRE.LIDT.Co.VecState.SDDRel {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxSubMeas Question Outcome (K →L[ℂ] K)) (δ : ℝ) : Prop

State-dependent distance relation.

• squaredDistanceBound : V.sddError 𝒟 A B ≤ δ

structure MIPRE.LIDT.Co.VecState.SDDOpRel {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxOpFamily Question Outcome (K →L[ℂ] K)) (δ : ℝ) : Prop

State-dependent distance relation for raw operator families.

• squaredDistanceBound : V.sddErrorOp 𝒟 A B ≤ δ

structure MIPRE.LIDT.Co.VecState.SSCRel {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome (K →L[ℂ] K)) (δ : ℝ) : Prop

Strong self-consistency relation.

• diagonalOverlapBound : V.sscError 𝒟 A ≤ δ

structure MIPRE.LIDT.Co.VecState.CompletenessAtLeast {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Outcome : Type u_2} [Fintype Outcome] (A : SubMeas Outcome (K →L[ℂ] K)) (r : ℝ) : Prop

Completeness statement for a submeasurement.

• lowerBound : V.subMeasMass A ≥ r

structure MIPRE.LIDT.Co.VecState.BoundedByOperator {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Outcome : Type u_2} [Fintype Outcome] (A : SubMeas Outcome (K →L[ℂ] K)) (Z : K →L[ℂ] K) (δ : ℝ) : Prop

Boundedness statement witnessed by an operator.

• witnessOpPSD : 0 ≤ Z
• upperBound : V.bndError A Z ≤ δ

Nonnegativity lemmas for defect measures

theorem MIPRE.LIDT.Co.VecState.qSDD_nonneg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Outcome : Type u_2} [Fintype Outcome] (A B : SubMeas Outcome (K →L[ℂ] K)) : 0 ≤ V.qSDD A B

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

theorem MIPRE.LIDT.Co.VecState.sddError_nonneg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxSubMeas Question Outcome (K →L[ℂ] K)) : 0 ≤ V.sddError 𝒟 A B

The averaged squared-distance error is nonneg.

Self-distance

theorem MIPRE.LIDT.Co.VecState.qSDD_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Outcome : Type u_2} [Fintype Outcome] (A : SubMeas Outcome (K →L[ℂ] K)) : V.qSDD A A = 0

The self-distance qSDD A A is zero.

theorem MIPRE.LIDT.Co.VecState.sddError_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome (K →L[ℂ] K)) : V.sddError 𝒟 A A = 0

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

Bridges to the repository calculus

theorem MIPRE.LIDT.Co.VecState.qSDDCore_eq_sum_snorm_sq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {Outcome : Type u_2} [Fintype Outcome] (A B : Outcome → K →L[ℂ] K) : V.qSDDCore A B = ∑ a : Outcome, ‖(A a - B a) V.Ψ‖ ^ 2

The squared-distance defect is a sum of squared state norms: qSDDCore A B = ∑ₐ ‖(Aₐ - Bₐ) Ψ‖², each term being V.toStateModel.snorm (Aₐ - Bₐ) ^ 2 (toStateModel_snorm).

Bipartite defects

noncomputable def MIPRE.LIDT.Co.SymModel.qBipartiteMatchMass {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (A B : SubMeas Outcome 𝔓) : ℝ

Bipartite matching mass ∑_a ⟨Ψ, (A_a ⊗ B_a) Ψ⟩, with A on the first factor and B on the second (S.opTensor).

Equations

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

noncomputable def MIPRE.LIDT.Co.SymModel.qBipartiteConsDefect {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (A B : SubMeas Outcome 𝔓) : ℝ

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 |ψ⟩) (qBipartiteConsDefect_eq_sum_ne).

Equations

• S.qBipartiteConsDefect A B = max 0 (S.ev (S.opTensor A.total B.total) - S.qBipartiteMatchMass A B)

noncomputable def MIPRE.LIDT.Co.SymModel.bipartiteConsError {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxSubMeas Question Outcome 𝔓) : ℝ

Averaged bipartite off-diagonal mass for consistency statements.

Equations

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

theorem MIPRE.LIDT.Co.SymModel.qBipartiteConsDefect_eq_qConsDefect_placed {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (A B : SubMeas Outcome 𝔓) : S.qBipartiteConsDefect A B = S.qConsDefect (S.leftPlacedSubMeas A) (S.rightPlacedSubMeas B)

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

theorem MIPRE.LIDT.Co.SymModel.bipartiteConsError_eq_consError_placed {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxSubMeas Question Outcome 𝔓) : S.bipartiteConsError 𝒟 A B = S.consError 𝒟 (fun (q : Question) => S.leftPlacedSubMeas (A q)) fun (q : Question) => S.rightPlacedSubMeas (B q)

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

Relations

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

Consistency relation (bipartite, paper Definition 4.8).

Alice's submeasurement A acts on the first factor and Bob's submeasurement B on the second. The relation encodes E_{x ∼ D} ∑_{a≠b} ⟨ψ| A^x_a ⊗ B^x_b |ψ⟩ ≤ δ.

• offDiagonalBound : S.bipartiteConsError 𝒟 A B ≤ δ

noncomputable def MIPRE.LIDT.Co.SymModel.qBipartiteSSCDefect {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (A : SubMeas Outcome 𝔓) : ℝ

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

• S.qBipartiteSSCDefect A = max 0 (S.ev (S.L A.total) - ∑ a : Outcome, S.ev (S.opTensor (A.outcome a) (A.outcome a)))

noncomputable def MIPRE.LIDT.Co.SymModel.bipartiteSSCError {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome 𝔓) : ℝ

Averaged bipartite SSC defect.

Equations

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

structure MIPRE.LIDT.Co.SymModel.BipartiteSSCRel {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome 𝔓) (δ : ℝ) : 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 : S.bipartiteSSCError 𝒟 A ≤ δ

Nonnegativity lemmas for defect measures

theorem MIPRE.LIDT.Co.SymModel.qBipartiteConsDefect_nonneg {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (A B : SubMeas Outcome 𝔓) : 0 ≤ S.qBipartiteConsDefect A B

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

theorem MIPRE.LIDT.Co.SymModel.bipartiteConsError_nonneg {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxSubMeas Question Outcome 𝔓) : 0 ≤ S.bipartiteConsError 𝒟 A B

The averaged bipartite consistency error is nonneg.

theorem MIPRE.LIDT.Co.SymModel.qBipartiteMatchMass_nonneg {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (A B : SubMeas Outcome 𝔓) : 0 ≤ S.qBipartiteMatchMass A B

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

theorem MIPRE.LIDT.Co.SymModel.qBipartiteConsDefect_le_one_of_isNormalized {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (A B : SubMeas Outcome 𝔓) : S.qBipartiteConsDefect A B ≤ 1

A bipartite consistency defect is at most 1 (the state is normalized).

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

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

theorem MIPRE.LIDT.Co.SymModel.bipartiteConsError_uniform_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Question : Type u_3} {Outcome : Type u_4} [Fintype Question] [DecidableEq Question] [Nonempty Question] [Fintype Outcome] (A B : IdxSubMeas Question Outcome 𝔓) : S.bipartiteConsError (MIPStarRE.LDT.uniformDistribution Question) A B ≤ 1

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

theorem MIPRE.LIDT.Co.SymModel.qBipartiteSSCDefect_nonneg {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (A : SubMeas Outcome 𝔓) : 0 ≤ S.qBipartiteSSCDefect A

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

theorem MIPRE.LIDT.Co.SymModel.bipartiteSSCError_nonneg {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome 𝔓) : 0 ≤ S.bipartiteSSCError 𝒟 A

The averaged bipartite strong self-consistency error is nonneg.

Bridges to the repository calculus

theorem MIPRE.LIDT.Co.SymModel.qBipartiteConsDefect_eq_sum_ne {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] [DecidableEq Outcome] (A B : SubMeas Outcome 𝔓) : S.qBipartiteConsDefect A B = ∑ a : Outcome, ∑ b : Outcome, if a = b then 0 else S.toBipartite.bornProb (A.outcome a) (B.outcome b)

The bipartite consistency defect is the off-diagonal Born mass ∑_{a ≠ b} ⟨Ψ, (A_a ⊗ B_b) Ψ⟩, for any two sub-measurements: the max 0 of the definition is inactive, since the total overlap is the sum of all the Born weights.

theorem MIPRE.LIDT.Co.SymModel.bipartiteConsError_eq_inconsistency {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Question : Type u_3} {Outcome : Type u_4} [Fintype Question] [Fintype Outcome] [DecidableEq Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxMeas Question Outcome 𝔓) : S.bipartiteConsError 𝒟 A.toIdxSubMeas B.toIdxSubMeas = S.toBipartite.inconsistency 𝒟.weight (fun (q : Question) => (A q).toPOVMIn) fun (q : Question) => (B q).toPOVMIn

The bipartite consistency error of two measurement families is the inconsistency of the model (MIPRE.BipartiteModel.inconsistency), weighted by the question distribution.

theorem MIPRE.LIDT.Co.SymModel.sddError_liftLeft_liftRight_eq_xPovmDist {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Question : Type u_3} {Outcome : Type u_4} [Fintype Question] [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxMeas Question Outcome 𝔓) : S.sddError 𝒟 (IdxSubMeas.liftLeft S A.toIdxSubMeas) (IdxSubMeas.liftRight S B.toIdxSubMeas) = S.toBipartite.xPovmDist 𝒟.weight (fun (q : Question) => (A q).toPOVMIn) fun (q : Question) => (B q).toPOVMIn

The squared distance of the left and right lifts of two measurement families is the cross-party distance of the model (MIPRE.BipartiteModel.xPovmDist), weighted by the question distribution: the vendored A ⊗ I ≈_δ I ⊗ B is the appendix's A ⊗ Id ≃_δ Id ⊗ B.