Section 5 — Positive-Gram sigma-space specialization

Application of the positive-Gram polar construction to the canonical sigma-space layer obtained from a rank-reduction witness.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.xHat_of_positive_gram_spectrum_unitaryGroup_choices {μ : Type u_1} {ι : Type u_2} [Fintype μ] [DecidableEq μ] [Fintype ι] [DecidableEq ι] (X : Matrix μ ι ℂ) (Q : Matrix ι ι ℂ) (hQ : Q.IsHermitian) (hQ_pos : Q.PosSemidef) (hgram : X.conjTranspose * X = Q) (e : { i : ι // 0 < hQ.eigenvalues i } ↪ μ) (U : ↥(Matrix.unitaryGroup μ ℂ)) (W : Matrix μ ι ℂ) (hU_rows : ∀ (i : { i : ι // 0 < hQ.eigenvalues i }) (r : μ), ↑U (e i) r = positiveGramSpectrumImageRows X Q hQ i r) (hW : W * W.conjTranspose = 1) (hW_rows : ∀ (i : { i : ι // 0 < hQ.eigenvalues i }) (r : ι), W (e i) r = positiveGramSpectrumRightRows Q hQ i r) : (↑U).transpose * W * ((↑U).transpose * W).conjTranspose = 1 ∧ X.conjTranspose * ((↑U).transpose * W) = CFC.sqrt Q

Explicit positive-Gram polar extension from chosen row-extension data with the left factor represented as a unitary group element.

The existential construction of Xhat first chooses an embedding of the positive spectral subspace into the auxiliary row space, then chooses a unitary group element U extending the normalized image rows and a rectangular coisometry W extending the right singular rows. This theorem records the deterministic matrix produced from those choices, namely Uᵀ * W, together with the two QXP identities it satisfies.

The explicit form is useful when a later argument needs to impose additional structure on the chosen rows, such as fresh option-completion row preservation used to derive the QXP-internal comparison Q_none ≤ P_none.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.exists_xHat_of_positive_gram_spectrum {μ : Type u_1} {ι : Type u_2} [Fintype μ] [DecidableEq μ] [Fintype ι] [NonUnitalContinuousFunctionalCalculus ℝ (Matrix ι ι ℂ) IsSelfAdjoint] (X : Matrix μ ι ℂ) (Q : Matrix ι ι ℂ) (hQ : Q.IsHermitian) (hQ_pos : Q.PosSemidef) (hgram : X.conjTranspose * X = Q) (hcard : Fintype.card μ ≤ Fintype.card ι) : ∃ (xHat : Matrix μ ι ℂ), xHat * xHat.conjTranspose = 1 ∧ X.conjTranspose * xHat = CFC.sqrt Q

Existence of the polar-extension Xhat from a positive Gram factorization.

If Q = X†X is positive semidefinite and the row dimension is at most the column dimension, the positive spectral rows of Q determine a rectangular coisometry Xhat satisfying the two primitive QXP identities: Xhat Xhat† = I and X† Xhat = sqrt Q.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.exists_xHat_of_sigmaFinRangeEmbedding_positiveGram {Outcome : Type uOutcome} [Fintype Outcome] [DecidableEq Outcome] {ι : Type uι} [Fintype ι] [DecidableEq ι] {ψ : QuantumState ι} {A : Measurement Outcome ι} {ζ : Error} {qLayer : QLayerData Outcome ι} (hRank : RankReductionWitness ψ A ζ qLayer) [Nonempty (FiniteHilbertSpace.sigmaFinCarrier fun (a : Outcome) => Matrix.rank (qLayer.q.outcome a))] : ∃ (xHat : Matrix (sigmaRangeCarrier qLayer.q) ι ℂ), xHat * xHat.conjTranspose = 1 ∧ (sigmaFinRangeEmbedding qLayer.q.outcome ⋯).conjTranspose * xHat = CFC.sqrt (QTotal qLayer)

Sigma-range specialization of the positive-Gram Xhat construction.

For a rank-reduction witness, the canonical sigma-space embedding satisfies X†X = Q. The stored total-rank bound supplies the rectangular dimension hypothesis, so the positive-Gram construction produces the Xhat required by the QXP data package.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.exists_qxpLayerData_ofRankReductionSigmaRangePositiveGram {Outcome : Type uOutcome} [Fintype Outcome] [DecidableEq Outcome] {ι : Type uι} [Fintype ι] [DecidableEq ι] {ψ : QuantumState ι} {A : Measurement Outcome ι} {ζ : Error} {qLayer : QLayerData Outcome ι} (hRank : RankReductionWitness ψ A ζ qLayer) [Nonempty (FiniteHilbertSpace.sigmaFinCarrier fun (a : Outcome) => Matrix.rank (qLayer.q.outcome a))] : ∃ (xHat : Matrix (sigmaRangeCarrier qLayer.q) ι ℂ), xHat * xHat.conjTranspose = 1 ∧ (sigmaFinRangeEmbedding qLayer.q.outcome ⋯).conjTranspose * xHat = CFC.sqrt (QTotal qLayer) ∧ ∃ (data : QXPLayerData Outcome ι) (hq : data.qLayer = sigmaRangeQLayer qLayer.q), (hq ▸ data.x = have this := sigmaFinRangeEmbedding qLayer.q.outcome ⋯; this) ∧ hq ▸ data.xHat = have this := xHat; this

Produce the canonical sigma-space QXP layer from the positive-Gram Xhat.

This removes the last explicit Xhat input from the sigma-space constructor: the rank-reduction witness supplies the projective Q layer and the rectangular dimension bound, while exists_xHat_of_sigmaFinRangeEmbedding_positiveGram supplies the coisometry and mixed square-root identities.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.exists_qxpLayerData_ofRankReductionSigmaRangePositiveGram_with_x_coisometry {Outcome : Type uOutcome} [Fintype Outcome] [DecidableEq Outcome] {ι : Type uι} [Fintype ι] [DecidableEq ι] {ψ : QuantumState ι} {A : Measurement Outcome ι} {ζ : Error} {qLayer : QLayerData Outcome ι} (hRank : RankReductionWitness ψ A ζ qLayer) (hsum_le_one : ∑ a : Outcome, qLayer.q.outcome a ≤ 1) [Nonempty (FiniteHilbertSpace.sigmaFinCarrier fun (a : Outcome) => Matrix.rank (qLayer.q.outcome a))] : ∃ (xHat : Matrix (sigmaRangeCarrier qLayer.q) ι ℂ), xHat * xHat.conjTranspose = 1 ∧ (sigmaFinRangeEmbedding qLayer.q.outcome ⋯).conjTranspose * xHat = CFC.sqrt (QTotal qLayer) ∧ ∃ (data : QXPLayerData Outcome ι) (hq : data.qLayer = sigmaRangeQLayer qLayer.q), (hq ▸ data.x = have this := sigmaFinRangeEmbedding qLayer.q.outcome ⋯; this) ∧ (hq ▸ data.xHat = have this := xHat; this) ∧ data.x * data.x.conjTranspose = 1

Produce the canonical positive-Gram sigma-space QXP layer, and record coisometry of the sigma embedding X.

The additional hypothesis is the usual subnormalization condition for the projective family Q_a. It implies that the finite sigma-range embedding has orthonormal rows, so the canonical X in the resulting QXPLayerData is a coisometry.