Section 5 — Projective Non-Measurement from Spectral Truncation

This file proves the constructive spectral-truncation form of the paper witness lem:projective-non-measurement. The rounded projective family is obtained by functional calculus, using the threshold 1 - sqrt ζ in the nontrivial regime and the zero family in the large-error regime.

References

• references/ldt-paper/orthonormalization.tex (lines 420-550)
• Blueprint: Chapter 4 (blueprint/src/chapter/ch04_projective.tex)
• Related downstream applications: #422 (mainFormal), #834 (Step 6)

theorem MIPStarRE.LDT.MakingMeasurementsProjective.projectiveNonMeasurement_of_sourceAlmostProjective_two_mul {Outcome : Type uOutcome} [Fintype Outcome] {ι : Type uι} [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (A : Measurement Outcome ι) (ζ : Error) (hζ : 0 < ζ) (hζ_small : ζ ≤ 1 / 4) (hsource : ∑ a : Outcome, ev ψ (A.outcome a - A.outcome a * A.outcome a) ≤ 2 * ζ) : projectiveNonMeasurement ψ A ζ

Construct the paper witness lem:projective-non-measurement from the source almost-projective defect at the paper's 2ζ scale.

This is the spectral-truncation stage of Section 5 in the form needed by the top-level orthonormalization theorem: the input defect is bounded by 2 * ζ, and choosing the truncation threshold 1 - sqrt ζ gives the paper's 2 * sqrt ζ closeness bound together with the total bound (1 + 2 * sqrt ζ) * I.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.projectiveNonMeasurement_of_sourceAlmostProjective_zero {Outcome : Type uOutcome} [Fintype Outcome] {ι : Type uι} [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (A : Measurement Outcome ι) (hsource : ∑ a : Outcome, ev ψ (A.outcome a - A.outcome a * A.outcome a) ≤ 0) : projectiveNonMeasurement ψ A 0

The exact endpoint ζ = 0 of lem:projective-non-measurement.

Here the source almost-projective defect vanishes exactly. We round each effect to the spectral projector onto its 1-eigenspace. The total operator is then dominated by I, and the finite-spectrum comparison shows that the resulting state-dependent operator distance is exactly zero.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.projectiveNonMeasurement_of_sourceAlmostProjective_large {Outcome : Type uOutcome} [Fintype Outcome] {ι : Type uι} [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (A : Measurement Outcome ι) (ζ : Error) (hψ : ψ.IsNormalized) (hlarge : 1 / 4 < ζ) : projectiveNonMeasurement ψ A ζ

The large-error branch of lem:projective-non-measurement.

The paper treats the surrounding orthonormalization lemma as trivial when ζ > 1/4. On a normalized state, the zero projector family already satisfies the required 2\sqrt{ζ} state-dependent operator bound in this regime.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.projectiveNonMeasurement_of_sourceAlmostProjective_two_mul_full {Outcome : Type uOutcome} [Fintype Outcome] {ι : Type uι} [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (A : Measurement Outcome ι) (ζ : Error) (hψ : ψ.IsNormalized) (hsource : ∑ a : Outcome, ev ψ (A.outcome a - A.outcome a * A.outcome a) ≤ 2 * ζ) : projectiveNonMeasurement ψ A ζ

Unconditional constructive producer for lem:projective-non-measurement from the paper's 2ζ source-defect bound.

This theorem combines the exact endpoint ζ = 0, the nontrivial spectral proof for 0 < ζ ≤ 1/4, and the trivial large-error branch used in the surrounding paper argument.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.projectiveNonMeasurement_of_sourceAlmostProjective_full {Outcome : Type uOutcome} [Fintype Outcome] {ι : Type uι} [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (A : Measurement Outcome ι) (ζ : Error) (hψ : ψ.IsNormalized) (hsource : ∑ a : Outcome, ev ψ (A.outcome a - A.outcome a * A.outcome a) ≤ ζ) : projectiveNonMeasurement ψ A ζ

Unconditional constructive form of lem:projective-non-measurement.

This is the specialization of projectiveNonMeasurement_of_sourceAlmostProjective_two_mul_full to the stronger input hypothesis hsource ≤ ζ.

noncomputable def MIPStarRE.LDT.MakingMeasurementsProjective.spectralTruncationStatement_of_sourceAlmostProjective {Outcome : Type uOutcome} [Fintype Outcome] [DecidableEq Outcome] {ι : Type uι} [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (A : Measurement Outcome ι) (ζ : Error) (hψ : ψ.IsNormalized) (hsource : ∑ a : Outcome, ev ψ (A.outcome a - A.outcome a * A.outcome a) ≤ ζ) : SpectralTruncationStatement ψ A ζ

Construct the spectral truncation statement from the source almost-projective estimate.

This integrates the constructive witness theorem with the direct SpectralTruncationStatement used by the later Section 5 construction.

Equations

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