Section 5 — Locality-preserving projectivization repair

This file proves the locality-preserving repair route for the late Section 5 Q/X/XHat/P argument.

Scope

The spectral-truncation stage (the first part of the proof of rounding to projectors) is already proved by spectralTruncationStatement_of_sourceAlmostProjective in MakingMeasurementsProjective/SpectralTruncation/ProjectiveNonMeasurement.lean, which is fully proved via projectiveNonMeasurement_of_sourceAlmostProjective_full. Proofs that require the spectral truncation statement should call that declaration directly.

The main result recorded here:

• leftLiftedProjectivizationRepair — paper origin references/ldt-paper/orthonormalization.tex lines 534–860 (rank reduction and the Q/√Q completeness setup) and 862–1194 (the X/X̂/P algebra producing the lifted projective sub-measurement, including the final triangle-inequality assembly). The formal proof below follows that local Q/X/XHat/P route by passing to the left marginal state, constructing the local projective family there, and transporting the final estimate back to left lifts.

The theorem proved here is the direct output of that route under a normalized bipartite state and the source almost-projective estimate for the left-lifted measurement. It is stated directly in terms of this estimate, rather than in terms of a separate repair-input assumption, and provides the unconditional repair step used by the orthonormalization theorem.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.leftPlacedProjectivizationRepair_of_sourceAlmostProjective_two_mul {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 : Measurement Outcome ιA) (ζ : Error) (hζ : 0 ≤ ζ) (hsource : ∑ a : Outcome, ev ψ ((leftLiftedMeasurement A).outcome a - (leftLiftedMeasurement A).outcome a * (leftLiftedMeasurement A).outcome a) ≤ 2 * ζ) : ∃ (P : ProjSubMeas Outcome ιA), SDDRel ψ (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas A.toSubMeas)) (constSubMeasFamily (leftPlacedSubMeas P.toSubMeas)) (orthonormalizationMainLemmaError ζ)

Locality-preserving Q/X/XHat/P repair for a left-lifted measurement at the paper's 2ζ source-defect scale.

This is the sharp Section 5 repair route needed in the proof of thm:orthonormalization: if the left-lifted source almost-projective defect is bounded by 2 * ζ, then the final local projective submeasurement is still obtained with the paper's 84 * ζ^(1/4) envelope.

Paper origin: references/ldt-paper/orthonormalization.tex:862-1194, recorded for the scalar constant repair in docs/paper-gaps/issue-1032-orthonormalization-constant.tex.

Faithful encoding: This is the paper's locality-preserving construction at the 2ζ scale needed by the completion-to-measurement proof of thm:orthonormalization.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.rightPlacedProjectivizationRepair_of_sourceAlmostProjective_two_mul {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) (B : Measurement Outcome ιB) (ζ : Error) (hζ : 0 ≤ ζ) (hsource : ∑ a : Outcome, ev ψ ((rightLiftedMeasurement B).outcome a - (rightLiftedMeasurement B).outcome a * (rightLiftedMeasurement B).outcome a) ≤ 2 * ζ) : ∃ (P : ProjSubMeas Outcome ιB), SDDRel ψ (uniformDistribution Unit) (constSubMeasFamily (rightPlacedSubMeas B.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas P.toSubMeas)) (orthonormalizationMainLemmaError ζ)

Right-register locality-preserving Q/X/XHat/P repair at the paper's 2ζ source-defect scale.

This is the tensor-factor counterpart of leftPlacedProjectivizationRepair_of_sourceAlmostProjective_two_mul. It uses the right marginal state and returns a local projective submeasurement on Bob's space whose right placement is close to the given right-lifted measurement.

Faithful encoding: Paper origin: references/ldt-paper/projectivization.tex; this is the right-register two-space form of the projectivization repair used by the source proof of thm:main-formal.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.leftLiftedProjectivizationRepair_of_sourceAlmostProjective_two_mul {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] [DecidableEq Outcome] (ψ : QuantumState (ι × ι)) (hψ : ψ.IsNormalized) (A : Measurement Outcome ι) (ζ : Error) (hζ : 0 ≤ ζ) (hsource : ∑ a : Outcome, ev ψ ((leftLiftedMeasurement A).outcome a - (leftLiftedMeasurement A).outcome a * (leftLiftedMeasurement A).outcome a) ≤ 2 * ζ) : ∃ (P : ProjSubMeas Outcome ι), RoundedProjMeasStatement ψ (leftLiftedMeasurement A) P.liftLeft (orthonormalizationMainLemmaError ζ)

Square-register form of the locality-preserving repair theorem.

This is the specialization of leftPlacedProjectivizationRepair_of_sourceAlmostProjective_two_mul to the case where the two tensor factors have the same carrier.

Paper origin: references/ldt-paper/orthonormalization.tex:862-1194 (\label{lem:P-Q-approx} and the final projectivization-repair assembly).

Faithful encoding: This is the square-register specialization of the source-faithful left-register construction above.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.leftLiftedProjectivizationRepair {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] [DecidableEq Outcome] (ψ : QuantumState (ι × ι)) (hψ : ψ.IsNormalized) (A : Measurement Outcome ι) (ζ : Error) (hsource : ∑ a : Outcome, ev ψ ((leftLiftedMeasurement A).outcome a - (leftLiftedMeasurement A).outcome a * (leftLiftedMeasurement A).outcome a) ≤ ζ) : ∃ (P : ProjSubMeas Outcome ι), RoundedProjMeasStatement ψ (leftLiftedMeasurement A) P.liftLeft (orthonormalizationMainLemmaError ζ)

Paper-labelled name for the locality-preserving projectivization repair.

This is the theorem recorded by the blueprint entry lem:locality-preserving-projectivization: from the source almost-projective estimate for the left-lifted family, it constructs a local projective submeasurement whose left lift is close with the 84 ζ^(1/4) envelope.

Paper origin: references/ldt-paper/orthonormalization.tex:862-1194.

Faithful encoding: This is the paper-labelled name for the proved locality-preserving construction.