Self-consistency: core squared-mass bounds

The squared-mass lower bound derived from bipartite self-consistency (prop:cool-prop), the missing-mass bound used before prop:completing-to-measurement, and the comparison of bipartite strong self-consistency with diagonal consistency (prop:other-two-notions-of-self-consistency). This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/SelfConsistency/Core.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions").

Each statement takes a symmetric model S : SymModel 𝔓 K in place of the state ψ : QuantumState (ι × ι), as an explicit first argument in the namespace Preliminaries, with local operators in 𝔓. The vendored hypotheses hperm : PermInvState ψ (of bipartiteSSCSquaredMass and completionMissingMassBound) and hψ : ψ.IsNormalized (of completionMissingMassBound) are dropped: swap symmetry enters through bipartiteSSC_implies_localSSC_liftLeft, which uses the model's S.ev_L_eq_ev_R, and normalization is S.ev_one_of_isNormalized. The vendored consistency relation of otherTwoNotionsOfSelfConsistency and the two measurement lemmas is the two-space @ConsRel … ι ι …; here it is the model's S.ConsRel, both families being local to 𝔓.

The proof of otherTwoNotionsOfSelfConsistency compares ev(M ⊗ M) with ev(M ⊗ I) through S.opTensor_le_leftTensor, where the vendored proof builds the Kronecker identity M ⊗ I - M ⊗ M = M ⊗ (I - M) and its positivity by hand.

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

theorem MIPRE.LIDT.Co.Preliminaries.bipartiteSSCSquaredMass {𝔓 : 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 : SubMeas Outcome 𝔓) (ζ : ℝ) : S.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily A) ζ → ∑ a : Outcome, S.ev (S.L (A.outcome a * A.outcome a)) ≥ S.ev (S.L A.total) - ζ

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

If A is ζ-strongly self-consistent, then ∑_a ev(A_a² ⊗ I) ≥ ev(A ⊗ I) - ζ: bipartite strong self-consistency gives local strong self-consistency of the left lift (bipartiteSSC_implies_localSSC_liftLeft), whose defect is this gap. The vendored lemma asks for a permutation-invariant state.

theorem MIPRE.LIDT.Co.Preliminaries.completionMissingMassBound {𝔓 : 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 𝔓) (δ ζ : ℝ) (hssc : S.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily A.toSubMeas) ζ) (hclose : S.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (SubMeas.liftLeft S A.toSubMeas)) (constSubMeasFamily (SubMeas.liftLeft S B)) δ) : S.ev (S.L ((1 - B.total) * (1 - B.total))) ≤ 2 * √δ + ζ

lem:completion-missing-mass-bound.

The missing-mass estimate used immediately before prop:completing-to-measurement: if A is a ζ-strongly self-consistent measurement and its left lift is δ-close to that of B, then ev((I - B)² ⊗ I) ≤ 2√δ + ζ. The vendored lemma asks for a permutation-invariant, normalized state.

theorem MIPRE.LIDT.Co.Preliminaries.otherTwoNotionsOfSelfConsistency {𝔓 : 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 𝔓) (δ : ℝ) : S.BipartiteSSCRel 𝒟 A δ → S.ConsRel 𝒟 A A δ

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

Bipartite strong self-consistency of A implies its diagonal consistency A ≃_δ A: question by question, the total overlap ev(A ⊗ A) is at most ev(A ⊗ I) (S.opTensor_le_leftTensor, since A ≤ I), and the remaining expression is the bipartite SSC defect.

theorem MIPRE.LIDT.Co.Preliminaries.bipartiteSSCRel_of_consRel_self_measurement {𝔓 : 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 : IdxMeas Question Outcome 𝔓) (δ : ℝ) : S.ConsRel 𝒟 A.toIdxSubMeas A.toIdxSubMeas δ → S.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 MIPRE.LIDT.Co.Preliminaries.bipartiteSSCRel_iff_consRel_self_measurement {𝔓 : 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 : IdxMeas Question Outcome 𝔓) (δ : ℝ) : S.BipartiteSSCRel 𝒟 A.toIdxSubMeas δ ↔ S.ConsRel 𝒟 A.toIdxSubMeas A.toIdxSubMeas δ

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