Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Projected-unitary encoding and singular vectors

Definition

Let H be a finite-dimensional complex inner-product space, let U:H→H be unitary, and let ΠR,ΠL:H→H be orthogonal projections. Write HR=ran⁡(ΠR) and HL=ran⁡(ΠL). The projected-unitary encoding (PUE) of this data is the linear map

A:HR→HL,Ax=ΠLUx.

Equivalently, its ambient-space compression is ΠLUΠR, restricted to HR and regarded as taking values in HL. The map A is a contraction: ∥A∥op≤1.

Put n=dim⁡HR, m=dim⁡HL, and r=rank⁡(A). A singular-value decomposition consists of orthonormal bases v1,…,vn of HR and u1,…,um of HL, and positive singular values 1≥σ1≥⋯≥σr>0, such that

A=∑j=1rσj∣uj⟩⟨vj∣.

The remaining right basis vectors span ker⁡A and the remaining left basis vectors span ker⁡A∗. Empty bases and sums are allowed when a dimension or the rank is zero. The pairing in each rank-one map is the root-linear-first Dirac conversion of Dirac Notation Conversion.

An exact square block encoding is a special case: identify the system with the all-zero ancilla subspace and take ΠL=ΠR equal to that subspace. Under the injection Ja of Finite block encoding, the compression is Ja∗UJa; an exact (α,a,0) block encoding has compressed block A/α.

Facts & Assumptions

Given: A finite-dimensional complex inner-product space H, a unitary U:H→H, orthogonal projections ΠR,ΠL, and the definitions of operator norm and PUE above.

[F1]

The orthogonal projection PWv is the W-component in V=W⊕W⊥: every vector is the sum of its projection into the range and an orthogonal vector in the complement.

[F2]

Pythagoras and finite orthogonal sums: the squared norm of a sum of orthogonal vectors is the sum of their squared norms.

[F4]

The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||: the operator norm is the maximum of ∥Tx∥ over unit vectors, with norm zero on the zero domain.

[F5]

Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition: every linear map between finite-dimensional inner-product spaces has orthonormal singular bases and positive singular values such that the displayed SVD formula holds.

[F6]

Dirac Notation Conversion: ∣u⟩⟨v∣ maps x to ⟨x,v⟩rootu.

[F7]

Finite block encoding: the all-zero ancilla compression of U is Ja∗UJa, and an exact block encoding sets this compression equal to the normalized target matrix.

[F8]

The adjoint T∗:W→V is characterised by ⟨Tv,w⟩W=⟨v,T∗w⟩V: the adjoint is characterized by ⟨Tx,y⟩=⟨x,T∗y⟩.

[F9]

Every linear map between finite-dimensional inner product spaces has a unique adjoint: every linear map between finite-dimensional inner-product spaces has a unique adjoint.

[F11]

Real and complex inner-product spaces and their induced length: the inner product is positive definite, so pairings with every vector distinguish vectors.

Proof

1.1givenF1F2F3F4algebra

If HR=0, then A is the zero map and its operator norm is zero by [F4]. Otherwise take any unit x∈HR. The decomposition Ux=ΠLUx+(I−ΠL)Ux has orthogonal terms by [F1], so [F2] gives ∥ΠLUx∥2≤∥Ux∥2. By [F3], ∥Ux∥=1, hence ∥Ax∥≤1. Taking the maximum over unit x proves ∥A∥op≤1.

1.2F7givenalgebra

In the square block-encoding case, Ja is the isometric identification of the system with HR=HL=ran⁡(Πa). The definition of the projected block in [F7] is exactly Ja∗UJa, and the exact case identifies it with the normalized target. Thus this is the stated special case.

2.1F4F5F6step 1.1algebra

Apply [F5] to the finite-dimensional map A:HR→HL. For each positive singular pair, Avj=σjuj and ∥vj∥=∥uj∥=1, so [F4] and step 1.1 give σj=∥Avj∥≤1. The rank-one terms in the SVD sum have the coordinate action fixed by [F6]. When r=0, the positive singular list and the displayed sum are empty; the kernel bases still exist by [F5].

3.1F5F6F8F9F11step 2.1algebra

For each k≤r and every x∈HR, the SVD formula, root-linear-first rank-one action [F6], and orthonormality of the uj give ⟨Ax,uk⟩=σk⟨x,vk⟩; for k>r the same pairing is zero. By [F8]–[F9], ⟨Ax,uk⟩=⟨x,A∗uk⟩, so positive definiteness [F11] gives A∗uk=σkvk for k≤r and A∗uk=0 for k>r. The SVD formula also gives Avk=σkuk for k≤r and Avk=0 for k>r. Since each singular list is a basis, expanding an arbitrary vector in those bases shows that ker⁡A=span⁡{vr+1,…,vn} and ker⁡A∗=span⁡{ur+1,…,um}: the positive-index coefficients must vanish because the corresponding singular values are positive and the other basis is orthonormal. The argument includes empty bases and sums.

4.1F1F8F9F10givenalgebra∎

By [F1], orthogonal decomposition gives ⟨ΠLUx,y⟩=⟨Ux,y⟩ and ⟨x,ΠRU∗y⟩=⟨x,U∗y⟩ for x∈HR and y∈HL. The adjoint rule [F8] for U therefore gives ⟨Ax,y⟩=⟨x,ΠRU∗y⟩. Thus y↦ΠRU∗y is an adjoint of A, and uniqueness [F9] yields A∗=ΠRU∗∣HL. Also, [F10] applies to the unitary U and shows that U∗=U−1 is unitary.

Depends on

Used by

Dependency tree · two levels

36 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources