Section 5 — Q/X/XHat/P q-completeness

Completeness estimates for the rank-reduced Q family in the paper's Q/X/XHat/P intermediate layer.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.spectralTruncationError_le_half (ζ : Error) (_hζ : 0 ≤ ζ) (hζq : ζ ≤ 1 / 4) : spectralTruncationError ζ ≤ 1 / 2

Under the small-error hypothesis ζ ≤ 1/4, the truncation error is at most 1/2.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.spectralTruncationError_le_zetaQuarterRoot (ζ : Error) (hζ : 0 ≤ ζ) (hζq : ζ ≤ 1 / 4) : spectralTruncationError ζ ≤ zetaQuarterRoot ζ

Under the small-error hypothesis ζ ≤ 1/4, the spectral truncation error is bounded by the fourth-root error scale used in the Q/X/XHat/P layer.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.qCompleteness {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A : Measurement Outcome ι) (ζ : Error) (data : QLayerData Outcome ι) (hψ : ψ.IsNormalized) (hζ : 0 ≤ ζ) (hζ_small : ζ ≤ 1 / 4) : RankReductionWitness ψ A ζ data → ev ψ (QTotal data) ≥ 1 - 11 * zetaQuarterRoot ζ

Completeness of Q (lem:Q-completeness).

If Q_a is the rank-reduced family from lem:projective-low-rank-sum, then its total operator Q has expectation at least 1 - 11 ζ^(1/4).

theorem MIPStarRE.LDT.MakingMeasurementsProjective.sqrtQCompleteness {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A : Measurement Outcome ι) (ζ : Error) (data : QLayerData Outcome ι) (hψ : ψ.IsNormalized) (hζ : 0 ≤ ζ) (hζ_small : ζ ≤ 1 / 4) : RankReductionWitness ψ A ζ data → ev ψ (CFC.sqrt (QTotal data)) ≥ 1 - 12 * zetaQuarterRoot ζ

Completeness of sqrt Q (lem:sqrt-Q-completeness).

The square root of the total operator Q remains almost complete on ψ.