Self-consistency: core squared-mass bounds

Squared-mass lower bound lemma derived from bipartite self-consistency on permutation-invariant states (prop:cool-prop).

References

• references/ldt-paper/preliminaries.tex
• blueprint/src/chapter/ch03_preliminaries.tex

theorem MIPStarRE.LDT.Preliminaries.bipartiteSSCSquaredMass {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (hperm : PermInvState ψ) (A : SubMeas Outcome ι) (ζ : Error) : BipartiteSSCRel ψ (uniformDistribution Unit) (constSubMeasFamily A) ζ → ∑ a : Outcome, ev ψ (leftTensor (A.outcome a * A.outcome a)) ≥ ev ψ (leftTensor A.total) - ζ

Squared mass lower bound from bipartite SSC (prop:cool-prop).

If A is ζ-strongly self-consistent on a permutation-invariant state, then ∑_a ⟨ψ| A_a² ⊗ I |ψ⟩ ≥ ∑_a ⟨ψ| A_a ⊗ I |ψ⟩ − ζ.

Proof:

1. Apply Cauchy-Schwarz to the families A_a ⊗ I and I ⊗ A_a.
2. Use permutation invariance to identify the two square-mass factors.
3. Conclude ∑ₐ ⟨ψ|(A_a)^2 ⊗ I|ψ⟩ ≥ ∑ₐ ⟨ψ|A_a ⊗ A_a|ψ⟩.
4. Combine with BipartiteSSCRel on the constant Unit-indexed family.

theorem MIPStarRE.LDT.Preliminaries.completionMissingMassBound {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (hperm : PermInvState ψ) (hψ : ψ.IsNormalized) (A : Measurement Outcome ι) (B : SubMeas Outcome ι) (δ ζ : Error) (hssc : BipartiteSSCRel ψ (uniformDistribution Unit) (constSubMeasFamily A.toSubMeas) ζ) (hclose : SDDRel ψ (uniformDistribution Unit) (constSubMeasFamily A.liftLeft) (constSubMeasFamily B.liftLeft) δ) : ev ψ (leftTensor ((1 - B.total) * (1 - B.total))) ≤ 2 * √δ + ζ

lem:completion-missing-mass-bound.

This is the source-style missing-mass estimate used immediately before prop:completing-to-measurement in the paper. The current formalization keeps the left-register placement explicit via leftTensor.

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

prop:other-two-notions-of-self-consistency.

Proof:

1. Expand qConsDefect for the left/right lifts.
2. Bound the total-overlap term ⟨ψ|A ⊗ A|ψ⟩ by ⟨ψ|A ⊗ I|ψ⟩ using A.total ≤ I.
3. The remaining expression is exactly the bipartite SSC defect.
4. Average over questions and use the hypothesis.

theorem MIPStarRE.LDT.Preliminaries.bipartiteSSCRel_of_consRel_self_measurement {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A : IdxMeas Question Outcome ι) (δ : Error) : ConsRel ψ 𝒟 A.toIdxSubMeas A.toIdxSubMeas δ → BipartiteSSCRel ψ 𝒟 A.toIdxSubMeas δ

Diagonal consistency for a full measurement is exactly bipartite strong self-consistency.

This is the converse of otherTwoNotionsOfSelfConsistency in the special case where the indexed family is measurement-valued. Completeness identifies both total-mass terms with the identity operator, so the self-ConsRel defect G ⊗ I ≃ I ⊗ G and the diagonal SSC defect have the same questionwise quantity.

theorem MIPStarRE.LDT.Preliminaries.bipartiteSSCRel_iff_consRel_self_measurement {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A : IdxMeas Question Outcome ι) (δ : Error) : BipartiteSSCRel ψ 𝒟 A.toIdxSubMeas δ ↔ ConsRel ψ 𝒟 A.toIdxSubMeas A.toIdxSubMeas δ

For full measurements, bipartite SSC and diagonal self-consistency are equivalent.