Exercise PLAN-506

A unitary compression obeys B†B+G†G=I, so its full operator norm is at most1. Rotated-column Gram orthogonality gives C^2+S^2=I and a CS decomposition with zero-sine-safe basis completion; the normalized singular-value or Hermitian signed arguments then lie in[-1,1].

1. The first p columns of the partitioned unitary satisfy the full Gram identity B†B+G†G=I_p, which bounds ||Bx||≤||x|| for every vector x.
2. For B=W_1 C V_1†, the rotated Gram identity (GV_1)†GV_1=I_p-C^2 implies 0≤c_j≤1 and mutually orthogonal lower-column vectors with squared lengths1-c_j^2.
3. Set s_j=sqrt(1-c_j^2). Normalize GV_1 e_j only when s_j>0, choose orthonormal complement vectors at s_j=0, and complete W_2 using q≥p, obtaining W_2†GV_1=[S;0].
4. The column isometry L=[C;S;0] and complement K=[[S,0],[-C,0],[0,I]] form a unitary; expressing the remaining transformed columns in K supplies V_2 and the full CS form, with C^2+S^2=I_p.
5. Qubitization's actual singular-value arguments c_j lie in[0,1]; in a Hermitian eigenvalue variant the signed eigenvalues lie in[-1,1], with any target scaling applied to the encoded block first.
6. Real-angle Chebyshev formulas therefore apply on[-1,1], using polynomial limits at zero endpoint sine; this is a domain statement, not a uniform second-kind bound or a circuit/finite-bit resource guarantee.

Work over the complex field and partition U=[[B,F],[G,H]], where B is p×p, G is q×p and U is unitary on dimension p+q, with p≤q. The first p columns of U are an isometry, so the entire Gram identity is B†B+G†G=I_p. In particular, for every x∈C^p, ||Bx||^2=||x||^2-||Gx||^2≤||x||^2. Hence ||B||≤1, not merely a bound on each original column separately. Individual column lengths alone would not imply this spectral bound: [[1,1],[0,0]] has both columns of norm1 but largest singular value sqrt(2), and cannot be such a unitary compression.

Take an SVD B=W_1 C V_1†, where W_1,V_1 are p×p unitary and C=diag(c_1,...,c_p) is nonnegative. Conjugating the Gram identity by V_1 gives (GV_1)†(GV_1)=I_p-C^2. The diagonal entries are squared norms, so1-c_j^2≥0; together with c_j≥0 this proves0≤c_j≤1. The columns of GV_1 are mutually orthogonal, with lengths s_j=sqrt(1-c_j^2). Thus S=diag(s_1,...,s_p) is real nonnegative and C^2+S^2=I_p.

Here is an explicit endpoint-safe construction of the CS structure, including the zero-sine cases. For every j with s_j>0, let w_j=GV_1 e_j/s_j. These vectors form an orthonormal family in C^q. For indices with s_j=0, the corresponding GV_1 e_j is zero, so do not divide by s_j. Instead choose additional orthonormal w_j from the orthogonal complement of the already chosen nonzero-sine vectors. Since q≥p, there is room to choose all first p vectors and then complete them to a q-dimensional orthonormal basis. Let W_2 be the unitary with these vectors as columns. Then W_2†GV_1=[S;0_(q-p)×p]. This construction also covers c_j=1 (s_j=0), c_j=0 (s_j=1), and repeated singular values; no representative is asserted unique.

The transformed unitary U_hat=diag(W_1†,W_2†) U diag(V_1,I_q) therefore has its first p columns equal to L=[C;S;0], where the row blocks have sizes p,p,q-p. Define the (p+q)×q matrix K=[[S,0],[-C,0],[0,I_(q-p)]]. Because C and S are commuting real diagonal matrices with C^2+S^2=I, one has L†L=I_p, K†K=I_q and L†K=0. Thus [L,K] is a complete unitary basis. The remaining q columns Y of U_hat are another orthonormal basis of L's orthogonal complement, so there is a q×q unitary V_2 with Y=K V_2†. Consequently U=diag(W_1,W_2) [[C,S,0],[S,-C,0],[0,0,I_(q-p)]] diag(V_1†,V_2†). This is the claimed cosine-sine form with nonnegative C,S. When q=p the final row/column blocks are absent; empty p=0 blocks, if allowed, reduce to an arbitrary q-dimensional unitary and the same basis-completion statement.

For qubitization applied to this encoded block B, the scalar singular-value arguments are precisely the c_j∈[0,1], hence lie in[-1,1]. In the Hermitian/eigenvalue variant, the real eigenvalues may be negative, but |lambda_j|≤||B||≤1, so the signed arguments also lie in[-1,1]. For a general nonnormal block, its possibly complex eigenvalues are not substituted into the singular-value construction. If B represents a separately scaled target A/alpha, this range conclusion concerns the actual normalized block's arguments, sigma_j(A)/alpha, not automatically unscaled sigma_j(A).

For each real argument t∈[-1,1], choose theta=arccos(t)∈[0,pi]. Then T_m(t)=cos(m theta), and in the interior U_l(t)=sin((l+1)theta)/sin(theta), with polynomial endpoint values U_l(1)=l+1 and U_l(-1)=(-1)^l(l+1). Thus no nonreal angle or division by a zero endpoint sine is needed to evaluate the polynomials on the encoded spectrum. Outside[-1,1] the polynomials are still defined, but this real-angle parametrization is unavailable and hyperbolic growth can occur. Staying inside the interval is a domain guarantee, not a uniform bound of1 on second-kind polynomials or a numerical-error/finite-bit stability theorem. The SVD and basis-completion argument proves mathematical existence of the factorization; it does not certify an efficient circuit to implement its basis changes or any query/gate count.

1. Uses the full identity B†B+G†G=I_p (or its all-vector norm inequality), not individual column lengths alone, to justify that B is a contraction and its singular values are at most1. (1 weight)
2. After B=W_1 C V_1†, derives (GV_1)†GV_1=I_p-C^2 and C^2+S^2=I_p with S nonnegative; justifies the CS basis structure by orthonormal completion, explicitly avoiding division by zero when s_j=0. (1 weight)
3. Identifies the actual encoded block's singular-value arguments c_j∈[0,1], and, for a Hermitian eigenvalue variant, its signed real eigenvalues in[-1,1]; does not substitute arbitrary nonnormal eigenvalues or unnormalized target values. (1 weight)
4. Explains why these arguments admit the real-angle Chebyshev formulas on[-1,1], with polynomial endpoint values rather than undefined sine quotients, without claiming a uniform second-kind bound, compiled basis-change cost or numerical precision guarantee. (1 weight)

No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.

Read the Lean track and existing diagnostic warmups

• website/research/sources.json

  lin-wiebe-2026-qasc

  Source SHA-256: 9f85f45f20ed5a46931ad0dec3b94ee09748bc56e39fae29b0aefe910440b0ae · MIT metadata only
• Primary source

Contract: 0f0d845ee3ff78f5091140f693f4b70c9e552cfebd742062c3f1d45e8042018f

Item digest: 3952e37c50db165ef6c493b022e8cdfb651aa4b11c09b5c8a045bc4f26233def

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 6. This is not measured graph distance or model difficulty.

{ "predecessor_item_digest": "f77a7a84ab1bb6ed5de47988c4b7da7369747254ab22e347e0bd4192d0cc9913", "predecessor_key": "qcb-core-plan-506-cosine-sine-constraint-and-range", "repair_record": "shared/repairs/plan-506-unitary-compression-gram-repair.json", "repair_record_digest": "0b41bdab4b8ec2575cbb444bce29200125e83fad05ccfed50e8a427842bf9a93", "review_record": "reports/textbook-v1/repairs/plan-506-unitary-compression-gram-repair-review.json", "review_digest": "d03e4749f18992790076ccc692dad76db29176d1215659a9a0db78b99d9ef246" }