Section 5 — Q/X/XHat/P low-rank truncation

Rank-reduction auxiliary-space constructions and the low-rank truncation branch for the paper's Q/X/XHat/P intermediate layer.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.projectiveLowRankSum_auxData_of_rank_bound {Outcome : Type uOutcome} [Fintype Outcome] [Nonempty Outcome] {ι : Type uι} [Fintype ι] [Nonempty ι] (m : Outcome → ℕ) (hm : ∑ a : Outcome, m a ≤ Fintype.card ι) : ∃ (auxSpace : FiniteHilbertSpace) (t : ProjMeas Outcome auxSpace.carrier), t.total = 1 ∧ Fintype.card auxSpace.carrier ≤ Fintype.card ι

Concrete auxiliary-space construction from a direct total-rank bound.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.projectiveLowRankSum_auxData_of_projectors {Outcome : Type uOutcome} [Fintype Outcome] [Nonempty Outcome] {ι : Type uι} [Fintype ι] [DecidableEq ι] [Nonempty ι] (R : Outcome → Quantum.Op ι) (hproj : ∀ (a : Outcome), Quantum.IsProj (R a)) (htotal_le_one : ∑ a : Outcome, R a ≤ 1) : ∃ (auxSpace : FiniteHilbertSpace) (t : ProjMeas Outcome auxSpace.carrier), t.total = 1 ∧ Fintype.card auxSpace.carrier ≤ Fintype.card ι

Concrete auxiliary-space construction for the exact-projector case.

When the honest sigma-carrier Σ a, Fin (rank R_a) is nonempty, we use its lifted finite-enumeration model. If all ranks vanish, then that carrier is empty, but FiniteHilbertSpace requires a nonempty carrier; in that degenerate branch we fall back to the one-point space ULift Unit.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.projectiveLowRankSum_of_projectors {Outcome : Type uOutcome} {ι : Type uι} [Fintype ι] [DecidableEq ι] [Nonempty ι] [Fintype Outcome] [Nonempty Outcome] (ψ : QuantumState ι) (A : Measurement Outcome ι) (ζ : Error) (hζ : 0 ≤ ζ) (R : OpFamily Outcome ι) (hR : RoundingToProjectorsWitness ψ A ζ R) (hsum_le_one : ∑ a : Outcome, R.outcome a ≤ 1) (source_almost_projective : ∑ a : Outcome, ev ψ (A.outcome a - A.outcome a * A.outcome a) ≤ 2 * ζ) : ∃ (data : QLayerData Outcome ι), RankReductionWitness ψ A ζ data

Concrete rank-reduction construction once the rounded family is already an exact projector submeasurement ∑_a R_a ≤ I.

This exact-projector branch is currently kept for the blueprint cross-reference to the paper's r ≤ d statement; the public theorem routes through projectiveLowRankSum_of_rank_bound after #726.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.projectiveLowRankSum_of_rank_bound {Outcome : Type uOutcome} {ι : Type uι} [Fintype ι] [DecidableEq ι] [Nonempty ι] [Fintype Outcome] [Nonempty Outcome] (ψ : QuantumState ι) (A : Measurement Outcome ι) (ζ : Error) (hζ : 0 ≤ ζ) (R : OpFamily Outcome ι) (hR : RoundingToProjectorsWitness ψ A ζ R) (hrank : ∑ a : Outcome, Matrix.rank (R.outcome a) ≤ Fintype.card ι) (source_almost_projective : ∑ a : Outcome, ev ψ (A.outcome a - A.outcome a * A.outcome a) ≤ 2 * ζ) : ∃ (data : QLayerData Outcome ι), RankReductionWitness ψ A ζ data

Concrete rank-reduction construction once the rounded projectors already have total rank at most the ambient dimension. This is the r ≤ d branch of the paper's rank-reduction proof, and is also the final packaging step after the r > d truncation branch constructs its lower-rank family.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.projectiveLowRankSum_truncate {Outcome : Type uOutcome} {ι : Type uι} [Fintype ι] [DecidableEq ι] [Nonempty ι] [Fintype Outcome] [Nonempty Outcome] (ψ : QuantumState ι) (hψ : ψ.IsNormalized) (A : Measurement Outcome ι) (ζ : Error) (hζ : 0 ≤ ζ) (hζ_le : ζ ≤ 1 / 4) (R : OpFamily Outcome ι) (hR : RoundingToProjectorsWitness ψ A ζ R) (source_almost_projective : ∑ a : Outcome, ev ψ (A.outcome a - A.outcome a * A.outcome a) ≤ 2 * ζ) : ∃ (data : QLayerData Outcome ι), RankReductionWitness ψ A ζ data

Construct the rank-reduced projector family in the r > d truncation branch, starting from the rounded projectors R_a.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.projectiveLowRankSum_of_roundingWitness {Outcome : Type uOutcome} {ι : Type uι} [Fintype ι] [DecidableEq ι] [Nonempty ι] [Fintype Outcome] (ψ : QuantumState ι) (A : Measurement Outcome ι) (ζ : Error) (hψ : ψ.IsNormalized) (hζ : 0 ≤ ζ) (hζ_le : ζ ≤ 1 / 4) (q : OpFamily Outcome ι) (hrounded : RoundingToProjectorsWitness ψ A ζ q) (source_almost_projective : ∑ a : Outcome, ev ψ (A.outcome a - A.outcome a * A.outcome a) ≤ 2 * ζ) : ∃ (data : QLayerData Outcome ι), RankReductionWitness ψ A ζ data

Internal rank-reduction constructor from an already rounded projective family.

Construct the paper's rank-reduced family Q_a, together with the auxiliary projective measurement T_a, so that Q_a remains close to A_a, its total stays bounded by (1 + 2√ζ)I, and the auxiliary dimension is at most the original ambient dimension.

Paper source: proof of \label{lem:projective-low-rank-sum} in references/ldt-paper/orthonormalization.tex:540-658, after applying \label{lem:projective-non-measurement}.

Source: This is a source-faithful internal helper for the part of the proof after the rounded family R_a has been obtained. It starts from a chosen rounded family carrying the explicit witness RoundingToProjectorsWitness ψ A ζ q; equivalently, it consumes a concrete witness of the statement projectiveNonMeasurement ψ A ζ. The paper-facing projectiveLowRankSum applies the rounding lemma internally before calling this constructor.

The auxiliary space ℂ^m and the projective measurement T_a = ∑_i |a,i⟩⟨a,i| come from the subsequent "Matrix decomposition of Q_a" definition (orthonormalization.tex:777-795). The proof uses the r ≤ d rank-bound branch directly and otherwise performs the paper's r > d truncation branch from orthonormalization.tex:559-658: it chooses the top-overlap Large set, assembles the truncated projectors from MIPStarRE.Quantum.IsProj.rangeONB, proves the 4√ζ truncation error, and then builds the finite auxiliary projective measurement from the resulting rank bound. The broader downstream QXPLayerData construction is intentionally separated from this rank-reduction theorem: its statement now requires only the primitive X / XHat / P identities used later, rather than explicit rectangular complex-SVD matrices.