Quantum Signal Processing (QSP) is the backbone underneath QSVT, block encoding, and Hamiltonian simulation: a product of single-qubit rotations interleaved with a fixed signal operator computes, in its matrix entries, a pair of polynomials in the signal. The forward direction — that any phase list yields a unitary whose entries are degree-bounded polynomials satisfying a unitarity constraint — is the easy half. The converse — that every admissible polynomial pair is realized by some phase sequence — is the theorem that makes QSP a design tool rather than a curiosity. It is also the one people wave their hands at.
We finished a machine-checked proof of both directions in the Quantum toolkit's Lean 4 proof root (QuantumProofs/QSP.lean), and the file is sorry-free.
The two theorems
Forward (qsp_unitary). For every list of phases φ and every (x, s) with s² = 1 − x², the QSP product U satisfies Uᴴ U = 1. This is the unitarity keystone — proved by induction on the phase list, each rotation preserving the invariant.
Converse (qsp_converse). For every degree d and every admissible polynomial pair (A, C) — admissibility being the parity and degree conditions plus the Gram identity A·A⋆ + (1−X²)·C·C⋆ = 1 — there exists a phase list of length d whose QSP product realizes (A, C), up to a global phase. The global-phase caveat is not slop: it is a genuine SL₂ obstruction, and the statement names it explicitly.
How the converse goes through
The converse is a degree induction with a "peel" step: given an admissible degree-d pair, peel off one phase angle, drop the degree by one, and recurse. Making that rigorous is most of the work, and it factors into a chain of supporting lemmas, all closed:
- Gram identity at (0,0) — the unitarity polynomial identity
A·A⋆ + (1−X²)·C·C⋆ = 1, the algebraic spine of admissibility. gram_lead_modulus— from that identity, the leading coefficients ofAandChave equal modulus.cancel_angle_exists— the angle that cancels the top-degree term exists, with an explicit formula.peel_first_column_drop/peel_degree_drop— one angle reduces both polynomials' degree; the rung of the induction.parity_coeff_zero— the parity condition forces the off-parity coefficients to vanish, so the degree genuinely drops by one rather than by two.gram_peel_invariant/realize_step— the Gram identity is preserved under the peel, so the recursion stays inside the admissible set and the realization reassembles.- Base cases
d = 0, 1(constructive angle realization) and an explicit degree-2 rung (qsp_converse_deg2: every unit-modulus(a, b)is realized by two phases).
Each of these is a named lemma you can point at, not a comment that says "by a standard argument."
Why bother proving the converse
Because QSP is where our circuit-synthesis claims bottom out. When the toolkit compiles a polynomial transform of a block-encoded operator into a phase sequence, the correctness of that compilation is the converse theorem. Having it machine-checked — parity, degree, Gram identity, the global-phase caveat, and all — means the synthesis path rests on a proof a machine has verified, not on a paper we trust.
This sits alongside the rest of the Quantum toolkit's formal layer: gate identities, Grover bounds, QFT/QPE accuracy, error-correction, and block-encoding statements in Lean 4 (with mathlib) and a smaller Rocq set. The QSP file is the latest piece, and it closes the hardest of the lot.