Section 5 — Rounding To Projectors Core

Internal lemmas for the orthogonalization and rounding-to-projectors chain.

This file extracts the consistency-to-almost-projective and spectral/rounding steps so that QXPLayer.lean can depend on them without importing the full Section 5 theorem file.

References

• references/ldt-paper/orthonormalization.tex
• blueprint/src/chapter/ch04_projective.tex

Orthonormalization helper lemmas

theorem MIPStarRE.LDT.MakingMeasurementsProjective.sourceAlmostProjective_nonneg {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A : Measurement Outcome ι) : 0 ≤ ∑ a : Outcome, ev ψ (A.outcome a - A.outcome a * A.outcome a)

The source idempotence defect of a measurement is nonnegative.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.consistencyToAlmostProjective {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] [DecidableEq Outcome] (ψ : QuantumState (ιA × ιB)) (A : Measurement Outcome ιA) (B : Measurement Outcome ιB) (ζ : Error) : ConsRel ψ (uniformDistribution Unit) (constSubMeasFamily A.toSubMeas) (constSubMeasFamily B.toSubMeas) ζ → AlmostProjMeasStatement ψ (leftLiftedMeasurement A) (consistencyToAlmostProjectiveError ζ)

Consistency implies almost-projective: if A is ζ-consistent with B, then A is 2ζ-almost-projective.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.consistencyToAlmostProjective_right {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] [DecidableEq Outcome] (ψ : QuantumState (ιA × ιB)) (A : Measurement Outcome ιA) (B : Measurement Outcome ιB) (ζ : Error) : ConsRel ψ (uniformDistribution Unit) (constSubMeasFamily A.toSubMeas) (constSubMeasFamily B.toSubMeas) ζ → AlmostProjMeasStatement ψ (rightLiftedMeasurement B) (consistencyToAlmostProjectiveError ζ)

Right-register form of consistency-to-almost-projective: if A and B are ζ-consistent across (H_A\otimes H_B), then Bob's lifted measurement is 2ζ-almost-projective on the right tensor factor.

def MIPStarRE.LDT.MakingMeasurementsProjective.zeroProjSubMeas {Outcome : Type u_1} {ι : Type u_2} [Fintype Outcome] [Fintype ι] [DecidableEq ι] : ProjSubMeas Outcome ι

The zero family is a projective submeasurement. This supplies trivial large-error branches where the target error bound is already at least the universal qSDD ≤ 1 estimate.

Equations

• MIPStarRE.LDT.MakingMeasurementsProjective.zeroProjSubMeas = { outcome_pos := ⋯, sum_eq_total := ⋯, total_le_one := ⋯, proj := ⋯ }

theorem MIPStarRE.LDT.MakingMeasurementsProjective.qSDD_leftPlaced_zeroProjSubMeas_le_one {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)) (hψ : ψ.IsNormalized) (A : SubMeas Outcome ιA) : qSDD ψ (leftPlacedSubMeas A) (leftPlacedSubMeas zeroProjSubMeas.toSubMeas) ≤ 1

The zero projective submeasurement is within unit qSDD of any lifted submeasurement on a normalized state.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.qSDD_rightPlaced_zeroProjSubMeas_le_one {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)) (hψ : ψ.IsNormalized) (A : SubMeas Outcome ιB) : qSDD ψ (rightPlacedSubMeas A) (rightPlacedSubMeas zeroProjSubMeas.toSubMeas) ≤ 1

The zero projective submeasurement is within unit qSDD of any right-placed submeasurement on a normalized bipartite state.