Section 5 — Q/X/XHat/P algebraic identities #
Algebraic identities for the Q/X/XHat/P layer, including the
restatements of Q_a, P_a, the mixed product, and projectivity of P.
X_a = T_a X (lem:xa-t).
Q_a restated (lem:qa-restated).
Rewrites the paper's operator Q_a in terms of X_a, X, and T_a.
If the original X rows are already coisometric and the mixed product
X† XHat agrees with the Gram operator X† X, then the polar replacement
XHat is equal to X.
This is the algebraic form of the observation used in the residual-domination
route: on a part where the row block already lies in the unit singular
subspace, the XHat replacement does not change it.
Row-block form of
xHat_eq_x_of_x_mul_conjTranspose_eq_one_of_mixed_eq_gram.
If the original X rows are already coisometric, then the polar
replacement XHat is equal to X.
Indeed, X X† = I makes the Gram operator X† X idempotent. Since this Gram
operator is positive, its positive square root is itself; the stored mixed
identity X† XHat = sqrt (X† X) therefore reduces to the hypothesis of
xHat_eq_x_of_x_mul_conjTranspose_eq_one_of_mixed_eq_gram.
Row-block form of xHat_eq_x_of_x_mul_conjTranspose_eq_one.
The total Q operator in a QXP layer is Hermitian.
This follows from lem:X-squared: the total operator is the right Gram matrix
X†X. The statement gives downstream spectral arguments a canonical
Hermitian witness for QTotal data.qLayer.
The total Q operator in a QXP layer is positive semidefinite.
This is the positivity companion to qtotal_isHermitian_of_x_squared; after
QTotal is identified with the Gram matrix X†X, positivity follows from the
standard Gram-matrix argument.
The spectral eigenvalues of the total Q operator are nonnegative.
This is the scalar form of qtotal_posSemidef_of_x_squared used when the
rectangular polar construction separates the positive and zero spectral
subspaces.
QXP-layer form of the positive-Gram row extension theorem.
For the matrix X stored in a QXP layer, the positive spectral part of
Q = X†X determines normalized image rows. These rows can be placed in
distinct auxiliary coordinates and then completed to a square unitary group
element on the auxiliary Hilbert space.
X-expression to Q-expression (lem:X-expression-to-Q-expression).
Converts the quadratic error term in X X† - I to the corresponding
Q_a Q Q_a - Q_a expression.
P_a restated (lem:pa-restated).
Rewrites P_a in terms of XHat, XHat_a, and T_a.
The P_a operator is the right Gram matrix of the corresponding
XHat_a row block.
This is the row-block form of paRestated: the auxiliary projector T_a is
idempotent, so inserting the second copy of T_a does not change the
operator.
If the XHat construction preserves one row block, then the corresponding
Q and P outcomes agree.
This lemma isolates the row-block identity used for the fresh outcome in the option-completed orthonormalization step.
Fresh-outcome domination follows from preservation of the fresh row block in the option-completed QXP layer.
This is only a QXP-internal comparison: it upgrades fresh-row preservation to
Q_none ≤ P_none. The former generic RestrictSome monotone-total route would
also have needed a source-to-Q comparison
(optionCompletion A).outcome none ≤ Q_none; that comparison is not part of
this lemma, and the present formal development no longer uses that generic
route. See
docs/reports/issue-1642-restrictsome-residual-domination-obstruction.md.
The adjoint mixed product Xhat† X equals the positive square root of
Q.
This is the adjoint form of the stored identity X† Xhat = sqrt Q. It is
used to identify the operator Y = X Xhat† in the proof of
lem:squared-difference.
The operator X Xhat† is Hermitian in a QXP layer.
The square of X Xhat† is X X† in a QXP layer.
The operator X Xhat† is positive semidefinite in a QXP layer.
Spectral form of the paper's identity
X * Xhat† = U * Σ * U† in lem:X-times-X-hat.
The unitary is the Mathlib eigenvector unitary of the already proved Hermitian
operator X * Xhat†; the diagonal matrix is the corresponding real spectrum,
embedded in ℂ. This is the unconditional form used by the later
lem:squared-difference argument.
Squared difference (lem:squared-difference).
Bounds the defect between X and XHat by the squared defect of X X†
from the auxiliary identity.
The sum of the QXP P-operators is the Gram operator XHat† XHat.
This is the total-mass identity for the canonical projective submeasurement produced from the Q/X/XHat/P layer.
Projectivity of P (lem:P-projectivity).
The family P_a built from XHat and T_a is a projective
submeasurement.
The canonical projective submeasurement obtained from the Q/X/XHat/P
layer. Its outcomes are the paper's operators P_a.
Instances For
The total of the canonical QXP projective submeasurement is XHat† XHat.
This exposes the total-mass identity implicit in pProjectivity, which is
needed when comparing the repaired projective family to the source
submeasurement in later monotonicity arguments.
The expectation of the QXP projective total is the sum of the expectations
of the paper projectors P_a.
Outcomewise domination of the QXP projectors implies domination of the total operator.
This is the summation form of the monotone-total invariant needed downstream:
once the concrete repair proves P_a ≤ A_a for every outcome, the canonical
QXP projective total is bounded by the source submeasurement total.
Total-domination invariant for the QXP repair.
This proposition is the construction-level operator comparison required by the paper-tight monotone-total route: the canonical projective family obtained from the QXP layer has total operator bounded by the source submeasurement total. It is deliberately stronger than state-dependent-distance closeness and should be proved from the concrete repair, not inferred from the orthonormalization error estimate alone.
The projective QXP total is bounded by the source submeasurement total.
Instances For
Outcomewise operator domination is a sufficient way to prove the QXP total-domination invariant.
A QXP total-domination witness gives the scalar right-register comparison used by the final-fields transport.