Section 5 — Q/X/XHat/P rank reduction #
Sigma-space projectors and rank-reduction lemmas for the paper's Q/X/XHat/P
intermediate layer.
If a family of projectors sums to at most the identity, then the sum of their ranks is at most the ambient dimension.
If a family of projectors sums to at most c • I, then the sum of their
ranks is at most c times the ambient dimension.
A chosen finite-enumeration model of the paper's carrier Σ a, Fin (m a).
Using Fin (Fintype.card Outcome) keeps the base carrier in a small universe;
sigmaFin then lifts it to the requested auxiliary-space universe with ULift.
Equations
- MIPStarRE.LDT.MakingMeasurementsProjective.FiniteHilbertSpace.sigmaFinCarrier m = ((i : Fin (Fintype.card Outcome)) × Fin (m ((Fintype.equivFin Outcome).symm i)))
Instances For
The finite Hilbert space whose preferred basis is a lifted finite-enumeration
model of Σ a, Fin (m a).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The lifted sigma carrier associated to the ranks of an operator family.
Equations
Instances For
The block projective measurement on the lifted finite-enumeration model of
Σ a, Fin (m a) selecting the a-block.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The matrix X associated to a projective family on the sigma auxiliary
space.
Rows are indexed by the finite model of Σ a, Fin (rank Q_a). The row
corresponding to (a,i) is the bra vector ⟨v_{a,i}|, where
v_{a,i} is the ith vector in the chosen orthonormal basis of the range of
Q_a. This is the Lean form of
X = Σ_a Σ_i |a,i⟩⟨v_{a,i}| in the paper.
Equations
- MIPStarRE.LDT.MakingMeasurementsProjective.sigmaFinRangeEmbedding Q hproj x j = star ((MIPStarRE.Quantum.IsProj.rangeONB (Q ((Fintype.equivFin Outcome).symm x.down.fst)) ⋯).vec x.down.snd j)
Instances For
The literal block projective measurement on Σ a, Fin (m a) selecting the
a-summand. This is the paper's measurement
T_a = Σ_i |a,i⟩⟨a,i| before replacing the sigma type by the universe-stable
finite-enumeration model used in sigmaFinProjMeas. The two constructions are
kept separate so that sigmaRangeEmbedding_qa_eq follows the paper's literal
index set, while the finite-enumeration form supplies the nonempty auxiliary
Hilbert space used by QXPLayerData.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The paper's literal matrix X = Σ_a Σ_i |a,i⟩⟨v_{a,i}|
on the sigma auxiliary space.
Equations
- MIPStarRE.LDT.MakingMeasurementsProjective.sigmaRangeEmbedding Q hproj x j = star ((MIPStarRE.Quantum.IsProj.rangeONB (Q x.fst) ⋯).vec x.snd j)
Instances For
The literal sigma-space range embedding realizes each projector as
Q_a = X† T_a X.
This is the matrix-decomposition identity immediately underlying the paper's
Q_a restatement. It is independent of the later polar/SVD construction of
Xhat.
The finite-enumeration range embedding realizes each projector as
Q_a = X† T_a X.
This is the universe-stable form of sigmaRangeEmbedding_qa_eq, with the same
sigma basis encoded by FiniteHilbertSpace.sigmaFinCarrier.
The finite-enumeration range embedding has right Gram matrix equal to the total operator of the projective family.
This is the canonical sigma-space form of the paper's identity X† X = Q. The
proof uses only that the auxiliary projectors T_a form a measurement and the
pointwise restatement Q_a = X† T_a X, together with the recorded total
identity ∑ a, Q_a = Q.
A finite family of projectors whose total is bounded by the identity has orthogonal distinct summands.
Distinct projectors in a subnormalized projective family have orthogonal chosen range basis vectors.
For a subnormalized projective family, the finite sigma range embedding has orthonormal rows.
The finite-enumeration Q layer associated to an operator family.
The auxiliary Hilbert space is the finite-enumeration model of
Σ a, Fin (rank Q_a), lifted to the universe of the ambient space. The block
measurement selecting the summands indexed by a fixed outcome is projective.
This construction requires the sigma carrier to be nonempty; the degenerate
all-ranks-zero case is handled separately by the low-rank auxiliary-space
producer.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Assemble QXPLayerData from the canonical sigma-space embedding and the
remaining SVD/polar identities for Xhat.
The matrix X and the auxiliary projective measurement are fixed to be the
finite-enumeration sigma construction associated to the projective family q.
Thus the hypothesis Q_a = X† T_a X required by
QXPLayerData.ofQLayerAndSvdIdentities is supplied by
sigmaFinRangeEmbedding_qa_eq; only the coisometry and mixed-square-root
identities for Xhat remain as inputs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Assemble the sigma-space Q/X/Xhat/P layer from a rank-reduction witness
and the remaining SVD/polar identities for Xhat.
The rank-reduction witness supplies the two facts about the family Q_a that
enter the matrix decomposition: each Q_a is a projection, and
∑_a Q_a = Q. The auxiliary space, the projective measurement T, and the
matrix X are therefore the canonical finite-enumeration construction attached
to the ranks of the projectors Q_a. As in the paper, the only data still not
constructed here are the coisometry and mixed square-root identities for the
chosen matrix Xhat.
Assemble the canonical sigma-space Q/X/Xhat/P layer and record
coisometry of the sigma embedding X.
This is a Lean-only strengthening of
exists_qxpLayerData_ofRankReductionSigmaRangeAndSvdIdentities. The additional
conclusion follows from the subnormalization hypothesis
∑_a Q_a ≤ I: for a projective family, the finite-enumeration sigma embedding
has orthonormal rows. The statement is used by the Section 5 formalization
near references/ldt-paper/orthonormalization.tex lines 862--1194, where the
paper works with the same canonical X and the SVD-derived Xhat.
A one-point projective measurement concentrating all mass on the chosen outcome.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The lifted finite-enumeration model of Σ a, Fin (m a) has cardinality
bounded by the ambient dimension whenever the total multiplicity is bounded.
Paper source: references/ldt-paper/orthonormalization.tex:540-553
(\label{lem:projective-low-rank-sum}).
A rank-reduction witness can be viewed on the canonical sigma-range auxiliary space attached to the same projective family. This is a Lean-only transport from an arbitrary auxiliary model of the projective family to the finite enumeration of its range bases; the mathematical hypotheses are exactly the rank-reduction witness fields.
Faithful encoding: The theorem changes only the auxiliary-space model used
to present the same projective family Q_a; it is not an additional
mathematical assumption or proof obligation.
If the sigma auxiliary space has dimension at most the ambient Hilbert
space, then there is a rectangular matrix Xhat whose rows are orthonormal.
This is the formal content of the paper's identity
\widehat X \widehat X^\dagger = I_m that follows only from the rectangular
dimension bound m ≤ d. The companion mixed identity
X^\dagger \widehat X = √Q is the remaining polar/SVD input.
The total-rank bound in lem:projective-low-rank-sum supplies the
coisometry part of the paper's Xhat construction on the sigma auxiliary
space.
A chosen rectangular coisometry on the sigma auxiliary space, obtained from the total-rank bound.
Equations
Instances For
The chosen sigma-space rectangular coisometry has orthonormal rows.