Section 5 — P-Q approximation for QXP layers #
The final comparison estimates between the projective family P produced
from XHat and the original projective Q layer.
The mixed X--Xhat summation appearing in the proof of
lem:P-Q-approx.
After rewriting Q_a and P_a through the matrices X, Xhat, and the
projective measurement T, the sum of the mixed terms collapses to
Xᴴ * Xhat, hence to sqrt Q by lem:X-times-X-hat.
P is close to Q (lem:P-Q-approx).
The final internal comparison in the paper's repair step is derived from the
primitive X/XHat/P identities in QXPLayerData, the rank-reduction witness,
and the standard small-error hypotheses. No closeness bound is stored inside
QXPLayerData; the proof below follows the paper's expansion through
squaredDifference, qAlmostProjective, and sqrtQCompleteness.
Apply lem:P-Q-approx to the canonical sigma-space QXP layer obtained
from a rank-reduction witness.
The theorem keeps the SVD/polar data for Xhat explicit, but removes the
remaining bookkeeping needed to use pQApprox: the rank-reduction witness is
transported to the sigma-space layer, and the resulting QXPLayerData is the
canonical one built from sigmaFinRangeEmbedding.
Apply lem:P-Q-approx to the positive-Gram sigma-space QXP layer.
This is the constructor-facing form of the local Q -> X -> Xhat -> P stage.
The rank-reduction witness supplies the sigma-space X; the positive-Gram
polar construction supplies Xhat; and the theorem concludes the paper's
P-versus-Q approximation without any external SVD data.
Apply lem:P-Q-approx to the positive-Gram sigma-space QXP layer, and
also record coisometry of the original sigma embedding X.
The additional hypothesis is the subnormalization of the projective Q family.
Under this hypothesis the range basis vectors chosen for distinct outcomes are
orthogonal, so the finite sigma-range embedding has orthonormal rows. This is
the construction-level coisometry condition later used to preserve the fresh
option-completion row and hence to obtain the QXP-internal comparison
Q_none ≤ P_none. An additional source-to-Q comparison is still required to
recover (optionCompletion A).outcome none ≤ P.outcome none; see
docs/reports/issue-1642-restrictsome-residual-domination-obstruction.md.
Apply lem:P-Q-approx to unitary-group rectangular SVD data and the
positive-square characterization of the middle factor.
The square SVD factors are represented as elements of Matrix.unitaryGroup;
hence the unitarity laws are not separate hypotheses.