If \(x \geq 1-\delta \), then \(\mathsf{trunc}_\delta (x)=1\). Since \(\delta \leq 1/2\) below, one also has \(x \geq \delta \), so

If \(x {\lt} 1-\delta \), then \(\mathsf{trunc}_\delta (x)=0\), and similarly

Write the eigendecomposition of \(A_a\) as

Choose

define \(\mathsf{trunc}_\delta :[0,1] \to \{ 0,1\} \) by \(\mathsf{trunc}_\delta (x)=1\) when \(x \geq 1-\delta \) and \(0\) otherwise, and set

By 4.16,

Summing expectations and using 2 gives

so \(A_a \otimes I \approx _{2\zeta /\delta } R_a \otimes I\).

For every \(x \in [0,1]\), one has \(\mathsf{trunc}_\delta (x) \leq x/(1-\delta )\), hence

Summing over \(a\) and using that \(A\) is a measurement,

where the last estimate uses \(\delta \leq 1/2\). Setting \(\delta =\sqrt{\zeta }\) gives the claim, and 1 ensures \(\delta \leq 1/2\).

Choose \(L\) to be a set of \(d\) indices on which the sum of \(f\) is maximal. If some \(s \in S\) and \(l \in L\) satisfied \(f(l) {\lt} f(s)\), replacing \(l\) by \(s\) would increase this sum, so every small index is bounded by every large index. Summing the inequalities \(f(s) \leq f(l)\) over all pairs \((s,l) \in S \times L\) gives

Since \(\alpha \) is the disjoint union of \(L\) and \(S\), adding \(|S|\sum _{s \in S} f(s)\) to both sides yields

The hypotheses \(|L|=d\) and \(r \leq (1+2\sqrt{\zeta })d\) imply \(|S|/r \leq 2\sqrt{\zeta }\). Dividing by \(r\) and using \(\sum _{x \in \alpha } f(x) \leq 1+2\sqrt{\zeta }\) gives

Finally, \(\zeta \leq 1/4\) implies \(\sqrt{\zeta } \leq 1/2\), and hence \(2\sqrt{\zeta }(1+2\sqrt{\zeta }) \leq 4\sqrt{\zeta }\).

Let \(\{ R_a\} \) be given by 4.17. Write \(r_a=\mathrm{rank}(R_a)\) and \(r=\sum _a r_a\). If \(r \leq d\), take \(Q_a=R_a\). Otherwise,

Let \(\lvert v_{a,1} \rangle ,\ldots ,\lvert v_{a,r_a} \rangle \) be an orthonormal basis for the range of \(R_a\), so

Define the overlaps

Their total satisfies

Let \(\mathsf{Large}\) be the set of the \(d\) largest overlaps \(o_{a,i}\), breaking ties arbitrarily, and let \(\mathsf{Small}\) be the complement. Then

by 4. Averaging the overlaps over the \(r\) indices gives

using 6, 5, and 1.

For each \(a\), let \(\mathsf{Large}_a=\{ i : (a,i)\in \mathsf{Large}\} \) and define

Then \(\sum _a \mathrm{rank}(Q_a)=|\mathsf{Large}| \leq d\), and \(Q_a \leq R_a\) for every \(a\), so

Also,

is a projector, hence

by 7. Therefore \(R_a \otimes I \approx _{4\sqrt{\zeta }} Q_a \otimes I\). Combining this with 4.17 and the triangle inequality for \(\approx _\delta \) gives

Since each \(Q_a\) is projective,

By Cauchy–Schwarz,

from 4.20. A second Cauchy–Schwarz estimate yields

Combining 8 and 9 with 2 gives

since \(\zeta \leq \zeta ^{1/4}\) under 1.

Diagonalize \(Q=\sum _i \nu _i \lvert u_i \rangle \langle u_i \rvert \). Because \(Q \leq (1+2\sqrt{\zeta })I\) by 4.20, each \(\nu _i\) is at most \(1+2\sqrt{\zeta }\). Therefore

The scalar estimate

gives \(\sqrt{Q} \geq (1-\sqrt{\zeta })Q\). Hence 4.21 implies

Since \(Q \leq (1+2\sqrt{\zeta })I\) by 4.20,

using 1 in the last step.

Choose an orthonormal basis of the range of each projector \(Q_a\). The rank-one expansion gives the displayed decomposition, and the orthogonality of the labelled basis vectors makes the family \(T\) a projective measurement.

Apply the finite-dimensional singular value decomposition to \(X\) and record exactly the consequences used later: the identities for \(X^\dagger X\), \(\widehat X\widehat X^\dagger \), \(X^\dagger \widehat X\), and the restatement of the \(Q_a\)’s. The unitary-group constructors are the same rectangular-SVD calculation, with the square factors taken as elements of the relevant unitary groups rather than as matrices accompanied by separate unitarity equations. In the sigma-range specialization, the auxiliary row space is the lifted finite-enumeration carrier associated to the ranks of the \(Q_a\)’s, which is definitionally the carrier of the canonical sigma-range \(Q\)-layer.

The definition is the formal \(Q/X/\widehat X/P\) construction: once \(\widehat X\) is chosen from the stored singular-value data, each \(P_a\) is defined as the positive operator \(\widehat X_a^\dagger \widehat X_a\).

Multiply the definition of \(X\) by \(T_a\) on the left and use that \(T_a\) selects exactly the basis vectors \(\lvert a,i \rangle \):

The identity \(X_a^\dagger X_a = Q_a\) follows by expanding the basis sums. The remaining equalities come from 4.28 and the projectivity of \(T\):

Use that \(T\) is a measurement and then 4.29:

The additional paper identities involving \(U,V,\Sigma \) are the usual SVD computations. The Lean development also records the spectral calculation which will identify the mixed positive-Gram-image product with \(\sqrt Q\): the positive eigenvalues give the nonzero columns, while the zero eigenspace has zero coefficient in the square-root expansion and is killed by \(X\). The conjugate right-eigenvector rows over the positive spectrum are also orthonormal. Equivalently, any row-space vector orthogonal to the positive Gram images is killed by \(X^\dagger \).

Expand the square and apply 4.30 and 4.29 term by term:

while

and \(X_a^\dagger I_{m \times m} X_a = X_a^\dagger X_a = Q_a\). Substituting these identities into

gives the claim.

Since \(T\) is projective,

The paper proves this by multiplying out \(\widehat{X}=U\cdot I_{m\times d}\cdot V^\dagger \) and using the unitarity of \(U\) and \(V\). In Lean, the dimension hypothesis \(m\leq d\) already gives a rectangular matrix with orthonormal rows on the sigma auxiliary space; the chosen matrix sigmaFinXHatCoisometry and its specification record this existence result as a hypothesis for the future construction. The formal lemma orthonormal_normalized_image_of_adjoint_comp_eigenvectors records the singular-vector normalization calculation, while normalized_matrix_image_rows_mul_conjTranspose combines the corresponding row-coisometry identity, and positive_gram_spectrum_image_rows_transpose_mixed records the adjoint action \(X^\dagger (\lambda ^{-1/2}Xv)=\lambda ^{1/2}v\) on the positive spectral part of the Gram operator. The formal lemma exists_unitaryGroup_with_positive_gram_spectrum_rows records the next finite-dimensional step: after choosing distinct row positions for the positive spectrum, these normalized image rows extend to a square unitary group element on the row space. The companion lemma exists_rectangular_coisometry_extending_orthonormal_rows records the analogous rectangular completion for prescribed right rows when the dimension bound permits it. The formal lemma unitaryGroup_mul_rectangular_coisometry and its right-multiplication companion rectangular_coisometry_mul_conjTranspose_unitaryGroup record the two unitary-preservation steps in the paper’s multiplication. The formal lemma rectangularSvd_xHat_coisometry_unitaryGroup applies these preservation steps to the rectangular-SVD expression. The unconditional positive-Gram route is exists_xHat_of_sigmaFinRangeEmbedding_positiveGram, which constructs \(\widehat X\) from the rank-reduction witness and proves \(\widehat X\widehat X^\dagger =I\) together with the mixed square-root identity below.

The paper obtains this from the SVD formula for \(X\) and the definition of \(\widehat X\). In Lean, the unconditional QXP data first proves that \(X\widehat X^\dagger \) is Hermitian and positive. The formal lemma x_mul_xHat_adjoint_spectral_theorem then applies Mathlib’s spectral theorem for Hermitian matrices, giving the displayed \(U\Sigma U^\dagger \) form with the Mathlib eigenvector unitary and the diagonal matrix of real eigenvalues. The auxiliary lemma rectangularSvd_x_mul_xHat_conjTranspose_raw records the same calculation under explicit rectangular-SVD data, where the middle factor \(S I_{m\times d}^\dagger \) is the formal square matrix \(\Sigma _{m\times m}\). The formal lemma rectangularSvd_xHat_mixed_of_sqrtQ_unitaryGroup records the second matrix calculation in the form whose square-root target is the operator \(Q\) supplied by the QXP construction. The formal lemma rectangularSvd_middle_eq_sqrt_of_square records the spectral step: a positive middle factor whose square is \(Q\) is the positive square root of \(Q\). The reduced datum then records this mixed-product identity as a primitive consequence, which is exactly the part needed in 4.36 and 4.38.

The paper diagonalizes the positive operator \(X\widehat X^\dagger \) using the SVD notation. The formal proof avoids storing that SVD explicitly: set \(Y=X\widehat X^\dagger \). The primitive identities imply that \(Y\) is hermitian, nonnegative, and satisfies \(Y^2=XX^\dagger \). Hence \((X-\widehat X)(X-\widehat X)^\dagger =(Y-I)^2\), and positivity of \(Y\) gives \((Y-I)^2\leq (Y^2-I)^2=(XX^\dagger -I)^2\).

For outcomes \(a,b\),

where the second line uses 4.33, the third uses that \(T\) is projective, and the last uses 4.32. Summing over \(a\) shows \(\sum _a P_a \leq I\), so \(P\) is a projective sub-measurement. The formalization also records the sharper identity

and the resulting total-domination estimates used later in the monotone-total self-improvement route.

The formal proof follows this argument directly from the primitive \(X\), \(\widehat X\), and \(P\) identities; the \(30\zeta ^{1/4}\) estimate is derived here rather than stored as part of the reduced datum. The unitary-group rectangular-SVD lemma combines the same estimate with the positive-square identification of the middle factor from 4.34; the square unitary factors are again carried as elements of the relevant unitary groups. The positive-Gram sigma-space lemma also records the coisometry \(X X^\dagger =I\) for the original sigma embedding when the projective \(Q\)-family is subnormalized; this is the construction-level hypothesis later used to obtain the QXP-internal fresh-outcome comparison \(Q_{\mathrm{none}} \leq P_{\mathrm{none}}\). An additional source-to-\(Q\) comparison is still needed for source-facing residual domination. The quantity to bound is

using the projectivity of \(Q\) and \(P\). The first term is at most \(1+2\sqrt{\zeta }\) by 4.20, and the second is at most \(1\) because \(P\) is a sub-measurement.

For the last two terms,

By 4.29,

The main estimate is

This follows by Cauchy–Schwarz:

is bounded by the square root of

times the square root of \(\sum _a \langle \psi \rvert (P_a)^2 \otimes I \lvert \psi \rangle \leq 1\). The first factor is at most \(4\sqrt{\zeta }\) by 4.36, 4.31, and 4.23, so the total error is at most \(2\zeta ^{1/4}\).

The right-hand side of 13 is real, because

where the first equality uses 4.28, 4.32, and 4.33 and that \(T\) is a measurement, and the second uses 4.34. Hence 4.22 and 13 imply

Substituting this into 12 and then into 11 gives