Section 5 — Positive-Gram completion #
Completion and polar-extension lemmas for the positive spectral rows of a right Gram operator.
A square unitary group element whose selected rows are a prescribed orthonormal family.
The row equations are stated pointwise so that later matrix calculations can rewrite entries without unfolding the chosen orthonormal basis.
The positive Gram image rows can be embedded into a square unitary group element.
The hypothesis e chooses distinct row positions for the strictly positive
eigenvalues of the Gram operator. The theorem then completes the corresponding
normalized image rows to a unitary element on the row space. This is the
basis-extension ingredient needed to turn the positive spectral part into the
left unitary factor of the rectangular polar construction.
Existential form of
exists_unitaryGroup_with_positive_gram_spectrum_rows.
The normalized positive Gram image rows have cardinality at most the row dimension, so one may choose distinct row positions and then extend those rows to a square unitary group element.
Extend an orthonormal row family to a rectangular coisometry.
The embedding e : κ ↪ μ specifies the rows of the rectangular matrix which
must agree with the prescribed family. The dimension hypothesis
Fintype.card μ ≤ Fintype.card ν supplies enough room to complete these rows
to an orthonormal family indexed by all of μ.
Extend the positive Gram right-singular rows to a rectangular coisometry.
The selected rows are the conjugate eigenvector rows of the right Gram operator. The cardinality hypothesis is the rectangular dimension condition: there must be enough columns to complete the prescribed rows to an orthonormal row family indexed by the auxiliary row space.
Left multiplication by the transpose of a unitary group element preserves row coisometries.
This is the coisometry half of the polar-extension calculation for the
candidate Xhat = Uᵀ W: the rectangular factor W has orthonormal rows, and
the square factor U merely changes the orthonormal basis of the row space.
Completion rows of the left unitary outside the positive Gram spectrum are
killed by X†.
The selected rows of U are the normalized positive images of the Gram
eigenvectors. If a row index is not one of the selected positive spectral
indices, the row-orthogonality of U makes that row orthogonal to all positive
Gram images. The adjoint-kernel lemma then gives the stated vanishing.
The selected columns of X† Uᵀ are the positive Gram-image mixed columns.
If the selected rows of U are the normalized images of the positive Gram
eigenvectors, then multiplying by X† and transposing U recovers precisely
the column matrix X† Rᵀ, where R is the positive Gram-image row matrix.
The complementary columns of X† Uᵀ vanish.
This is the matrix-column form of
adjoint_image_eq_zero_of_unitary_positive_gram_completion_row. It records
that the arbitrary rows used to complete the positive image rows to a full
unitary make no contribution after left multiplication by X†.
The polar-extension mixed product is the positive-spectrum mixed product.
The candidate Xhat = Uᵀ W has selected rows matching the positive left and
right singular rows. After expanding the middle index, the selected part is
exactly the positive-spectrum square-root product, while every complementary
row is killed by X†.
The polar-extension mixed product is the square root of the Gram operator.
This combines the finite-dimensional completion calculation for
Xhat = Uᵀ W with the positive-spectrum square-root identity.