Section 5 — Q/X/XHat/P core data

Scalar error estimates, core data structures, and shared operator-family definitions for the paper's Q/X/XHat/P intermediate layer.

noncomputable def MIPStarRE.LDT.MakingMeasurementsProjective.zetaQuarterRoot (ζ : Error) : Error

The quarter-root error term ζ^(1/4) used throughout the paper's late-stage orthonormalization estimates.

Equations

• MIPStarRE.LDT.MakingMeasurementsProjective.zetaQuarterRoot ζ = Real.rpow ζ (1 / 4)

theorem MIPStarRE.LDT.MakingMeasurementsProjective.zetaQuarterRoot_nonneg {ζ : Error} (hζ : 0 ≤ ζ) : 0 ≤ zetaQuarterRoot ζ

The quarter-root error term is nonnegative on nonnegative input.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.truncationInequality (δ x : Error) : 0 < δ → δ ≤ 1 / 2 → 0 ≤ x → x ≤ 1 → have trunc := if 1 - δ ≤ x then 1 else 0; (x - trunc) ^ 2 ≤ 1 / δ * (x - x ^ 2)

Scalar truncation inequality (lem:trunc-inequality).

For x ∈ [0,1], truncating at threshold 1 - δ changes x by at most (1 / δ) * (x - x^2) in squared distance.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.spectralTruncationError_nonneg {ζ : Error} (hζ : 0 ≤ ζ) : 0 ≤ spectralTruncationError ζ

The truncation error is nonnegative on nonnegative input.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.spectralTruncationError_eq_sqrt (ζ : Error) : spectralTruncationError ζ = √ζ

The truncation error is √ζ.

def MIPStarRE.LDT.MakingMeasurementsProjective.constOpFamily {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (A : OpFamily Outcome ι) : IdxOpFamily Unit Outcome ι

A raw operator family viewed as a constant indexed family on the trivial question set.

Equations

• MIPStarRE.LDT.MakingMeasurementsProjective.constOpFamily A x✝ = A

structure MIPStarRE.LDT.MakingMeasurementsProjective.QLayerData (Outcome : Type uOutcome) [Fintype Outcome] (ι : Type uι) [Fintype ι] [DecidableEq ι] : Type (max uOutcome (uι + 1))

Data for the paper's intermediate Q-layer: the rank-reduced family Q_a, its total operator Q, and the auxiliary projective measurement T_a used to define X_a, XHat_a, and P_a.

• auxSpace : FiniteHilbertSpace
• q : OpFamily Outcome ι
• t : ProjMeas Outcome self.auxSpace.carrier

def MIPStarRE.LDT.MakingMeasurementsProjective.Qa {Outcome : Type u_1} [Fintype Outcome] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (data : QLayerData Outcome ι) (a : Outcome) : Quantum.Op ι

The paper's operator Q_a.

Equations

• MIPStarRE.LDT.MakingMeasurementsProjective.Qa data a = data.q.outcome a

def MIPStarRE.LDT.MakingMeasurementsProjective.QTotal {Outcome : Type u_1} [Fintype Outcome] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (data : QLayerData Outcome ι) : Quantum.Op ι

The paper's total operator Q = ∑_a Q_a.

Equations

• MIPStarRE.LDT.MakingMeasurementsProjective.QTotal data = data.q.total

def MIPStarRE.LDT.MakingMeasurementsProjective.Ta {Outcome : Type u_1} [Fintype Outcome] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (data : QLayerData Outcome ι) (a : Outcome) : Quantum.Op data.auxSpace.carrier

The paper's auxiliary projector T_a.

Equations

• MIPStarRE.LDT.MakingMeasurementsProjective.Ta data a = data.t.outcome a

structure MIPStarRE.LDT.MakingMeasurementsProjective.RoundingToProjectorsWitness {Outcome : Type u_1} [Fintype Outcome] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (A : Measurement Outcome ι) (ζ : Error) (R : OpFamily Outcome ι) : Prop

Paper origin: references/ldt-paper/orthonormalization.tex:414-531 (\label{lem:projective-non-measurement}; full rounding-to-projectors lemma with 2√ζ closeness and (1+2√ζ)·I total bound).

Witness structure for the paper's rounding-to-projectors lemma.

A value RoundingToProjectorsWitness ψ A ζ R is the honest output consumed by this QXP rank-reduction layer: a chosen rounded family R_a together with the paper's 2√ζ closeness estimate and (1 + 2√ζ) I total-mass bound.

• projective (a : Outcome) : Quantum.IsProj (R.outcome a)
• closeness : SDDOpRel ψ (uniformDistribution Unit) (constOpFamily A.toOpFamily) (constOpFamily R) (2 * spectralTruncationError ζ)
• sum_eq_total : ∑ a : Outcome, R.outcome a = R.total
• total_le : R.total ≤ (↑1 + 2 * ↑(spectralTruncationError ζ)) • 1

@[reducible, inline]

abbrev MIPStarRE.LDT.MakingMeasurementsProjective.projectiveNonMeasurement {Outcome : Type uOutcome} {ι : Type uι} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A : Measurement Outcome ι) (ζ : Error) : Prop

Rounding to projectors (lem:projective-non-measurement).

This is the paper-facing proposition consumed by the QXP rank-reduction layer: there is a rounded projective family R_a equipped with the bounds recorded in RoundingToProjectorsWitness ψ A ζ R. The constructive spectral-truncation theorem supplies this witness from eq:A-looks-projective.

Equations

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

structure MIPStarRE.LDT.MakingMeasurementsProjective.RankReductionWitness {Outcome : Type u_1} [Fintype Outcome] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (A : Measurement Outcome ι) (ζ : Error) (data : QLayerData Outcome ι) : Prop

Paper origin: references/ldt-paper/orthonormalization.tex:540-553 (\label{lem:projective-low-rank-sum}; rank-reduction lemma with 12√ζ closeness, (1+2√ζ)·I total bound, and rank constraint ∑ rank(Q_a) ≤ d).

Witness structure for the rank-reduction lemma.

• projective (a : Outcome) : Quantum.IsProj (Qa data a)
• outcome_nonneg (a : Outcome) : 0 ≤ Qa data a
• sum_eq_total : ∑ a : Outcome, Qa data a = QTotal data
• source_almost_projective : ∑ a : Outcome, ev ψ (A.outcome a - A.outcome a * A.outcome a) ≤ 2 * ζ
• closeness : SDDOpRel ψ (uniformDistribution Unit) (constOpFamily A.toOpFamily) (constOpFamily data.q) (roundingToProjectiveError ζ)
• total_le : QTotal data ≤ (↑1 + 2 * ↑(spectralTruncationError ζ)) • 1
• totalRank_le : ∑ a : Outcome, Matrix.rank (Qa data a) ≤ Fintype.card ι
• auxDim_le : Fintype.card data.auxSpace.carrier ≤ Fintype.card ι

noncomputable def MIPStarRE.LDT.MakingMeasurementsProjective.pFamilyFromXHat {Outcome : Type u_1} [Fintype Outcome] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (qLayer : QLayerData Outcome ι) (xHat : Matrix qLayer.auxSpace.carrier ι ℂ) : OpFamily Outcome ι

The raw operator family obtained by sandwiching the auxiliary projectors T_a with a candidate XHat. This is the family later named P.

Equations

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

structure MIPStarRE.LDT.MakingMeasurementsProjective.QXPLayerData (Outcome : Type uOutcome) [Fintype Outcome] (ι : Type uι) [Fintype ι] [DecidableEq ι] : Type (max uOutcome (uι + 1))

Data for the paper's X/XHat/P layer built on top of Q_a and the auxiliary projectors T_a.

The local API deliberately stores only the primitive identities used by the subsequent P-vs-Q arguments. Earlier versions also carried explicit SVD matrices for X * Xᴴ, Xᴴ * X, and X * XHatᴴ; those fields required a general rectangular complex-matrix SVD producer that is not available in the current Mathlib toolchain and was not consumed by the downstream proofs.

• qLayer : QLayerData Outcome ι
• x : Matrix self.qLayer.auxSpace.carrier ι ℂ
• xHat : Matrix self.qLayer.auxSpace.carrier ι ℂ
• qa_eq (a : Outcome) : self.qLayer.q.outcome a = self.x.conjTranspose * Ta self.qLayer a * self.x
• qa_projective (a : Outcome) : Quantum.IsProj (self.qLayer.q.outcome a)
• xHat_coisometry : self.xHat * self.xHat.conjTranspose = 1
• x_gram_right : self.x.conjTranspose * self.x = QTotal self.qLayer
• xHat_mixed : self.x.conjTranspose * self.xHat = CFC.sqrt (QTotal self.qLayer)

def MIPStarRE.LDT.MakingMeasurementsProjective.Xa {Outcome : Type u_1} [Fintype Outcome] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (data : QXPLayerData Outcome ι) (a : Outcome) : Matrix data.qLayer.auxSpace.carrier ι ℂ

The paper's matrix X_a = T_a · X.

Equations

• MIPStarRE.LDT.MakingMeasurementsProjective.Xa data a = MIPStarRE.LDT.MakingMeasurementsProjective.Ta data.qLayer a * data.x

def MIPStarRE.LDT.MakingMeasurementsProjective.XHatA {Outcome : Type u_1} [Fintype Outcome] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (data : QXPLayerData Outcome ι) (a : Outcome) : Matrix data.qLayer.auxSpace.carrier ι ℂ

The paper's matrix XHat_a = T_a · XHat.

Equations

• MIPStarRE.LDT.MakingMeasurementsProjective.XHatA data a = MIPStarRE.LDT.MakingMeasurementsProjective.Ta data.qLayer a * data.xHat

def MIPStarRE.LDT.MakingMeasurementsProjective.Pa {Outcome : Type u_1} [Fintype Outcome] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (data : QXPLayerData Outcome ι) (a : Outcome) : Quantum.Op ι

The paper's operator P_a = XHat† · T_a · XHat.

Equations

• MIPStarRE.LDT.MakingMeasurementsProjective.Pa data a = data.xHat.conjTranspose * MIPStarRE.LDT.MakingMeasurementsProjective.Ta data.qLayer a * data.xHat

noncomputable def MIPStarRE.LDT.MakingMeasurementsProjective.PFamily {Outcome : Type u_1} [Fintype Outcome] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (data : QXPLayerData Outcome ι) : OpFamily Outcome ι

The raw operator family P = {P_a}.

Equations

• MIPStarRE.LDT.MakingMeasurementsProjective.PFamily data = MIPStarRE.LDT.MakingMeasurementsProjective.pFamilyFromXHat data.qLayer data.xHat

@[reducible, inline]

abbrev MIPStarRE.LDT.MakingMeasurementsProjective.matrixDecompositionQ (Outcome : Type u_1) [Fintype Outcome] (ι : Type u_2) [Fintype ι] [DecidableEq ι] : Type (max u_1 (u_2 + 1))

Paper label def:matrix-decomposition-Q.

The Lean formalization stores the chosen decomposition data for Q_a in the QLayerData structure.

Equations

• MIPStarRE.LDT.MakingMeasurementsProjective.matrixDecompositionQ Outcome ι = MIPStarRE.LDT.MakingMeasurementsProjective.QLayerData Outcome ι

@[reducible, inline]

abbrev MIPStarRE.LDT.MakingMeasurementsProjective.svdOfX (Outcome : Type u_1) [Fintype Outcome] (ι : Type u_2) [Fintype ι] [DecidableEq ι] : Type (max u_1 (u_2 + 1))

Paper label def:svd-of-X.

The paper describes this stage via an SVD of X; the Lean API records the constructive X/XHat/P identities needed downstream, avoiding an explicit rectangular complex-SVD structure.

Equations

• MIPStarRE.LDT.MakingMeasurementsProjective.svdOfX Outcome ι = MIPStarRE.LDT.MakingMeasurementsProjective.QXPLayerData Outcome ι

noncomputable def MIPStarRE.LDT.MakingMeasurementsProjective.projectiveP {Outcome : Type u_1} [Fintype Outcome] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (data : QXPLayerData Outcome ι) : OpFamily Outcome ι

Paper label def:projective-P.

The projective family P = {P_a} extracted from XHat.

Equations

• MIPStarRE.LDT.MakingMeasurementsProjective.projectiveP data = MIPStarRE.LDT.MakingMeasurementsProjective.PFamily data

theorem MIPStarRE.LDT.MakingMeasurementsProjective.xSquared_of_qa_eq {Outcome : Type uOutcome} [Fintype Outcome] {ι : Type uι} [Fintype ι] [DecidableEq ι] (qLayer : QLayerData Outcome ι) (q_sum_eq_total : ∑ a : Outcome, Qa qLayer a = QTotal qLayer) (x : Matrix qLayer.auxSpace.carrier ι ℂ) (qa_eq : ∀ (a : Outcome), qLayer.q.outcome a = x.conjTranspose * Ta qLayer a * x) : x.conjTranspose * x = QTotal qLayer

X squared from the Q_a = X† T_a X decomposition.

If each Q_a is represented as X† T_a X and the auxiliary measurement T = {T_a} sums to the identity, then the right Gram matrix of X is the total operator Q = ∑_a Q_a. This proves lem:X-squared from the Q_a = X† T_a X representation, independently of the later QXPLayerData record.

noncomputable def MIPStarRE.LDT.MakingMeasurementsProjective.QXPLayerData.ofQLayerAndSvdIdentities {Outcome : Type uOutcome} [Fintype Outcome] {ι : Type uι} [Fintype ι] [DecidableEq ι] (qLayer : QLayerData Outcome ι) (qa_projective : ∀ (a : Outcome), Quantum.IsProj (Qa qLayer a)) (q_sum_eq_total : ∑ a : Outcome, Qa qLayer a = QTotal qLayer) (x xHat : Matrix qLayer.auxSpace.carrier ι ℂ) (qa_eq : ∀ (a : Outcome), qLayer.q.outcome a = x.conjTranspose * Ta qLayer a * x) (xHat_coisometry : xHat * xHat.conjTranspose = 1) (xHat_mixed : x.conjTranspose * xHat = CFC.sqrt (QTotal qLayer)) : QXPLayerData Outcome ι

Assembles the QXPLayerData datum from a Q-layer and the SVD-derived identities.

Given a Q-layer (def:matrix-decomposition-Q), the matrix decomposition X of the paper, the chosen Xhat, and the two genuinely SVD-derived identities Xhat * Xhatᴴ = I (lem:X-hat-squared) and Xᴴ * Xhat = √Q (lem:X-times-X-hat), this assembles the QXPLayerData datum consumed by the downstream lem:P-Q-approx argument.

The identity x_gram_right (Xᴴ * X = Q, paper label lem:X-squared) is discharged by xSquared_of_qa_eq, from the representation Q_a = Xᴴ * T_a * X and the measurement identity for T. The other propositional fields, including qa_projective, are supplied by the caller.

The hypothesis qa_eq records exactly the lem:qa-restated choice, and the two SVD-derived hypotheses (xHat_coisometry and xHat_mixed) are precisely what the paper proves about Xhat = U · I_{m×d} · V†. These hypotheses are supplied by the sigma-range / rectangular polar-decomposition route, which provides the unitary and coisometry factors from the positive spectral subspace of Q. The paper's lem:X-squared, lem:X-hat-squared, and lem:X-times-X-hat are therefore proved given the QXPLayerData hypotheses; the end-to-end chain through the rounding-to-projectors, rank-reduction, and orthogonalization lemmas remains to be closed upstream.

Equations

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