量子信号処理を形式的に：Lean 4 による逆定理

量子信号処理（QSP）は、QSVT、ブロックエンコーディング、ハミルトニアンシミュレーションの基盤となる技法です。固定された信号演算子と単一量子ビット回転を交互に積み重ねた積は、その行列成分として、信号を変数とする多項式の組を計算します。順方向 — 任意の位相リストから得られるユニタリの成分が、次数制限とユニタリ性制約を満たす多項式になること — は簡単な半分です。逆方向 — 許容される多項式の組は すべて 何らかの位相列によって実現されること — こそが、QSP を単なる興味深い現象ではなく設計ツールにしている定理です。そして、多くの論文が手を振って済ませているのもこの定理です。

私たちは両方向の機械検証済み証明を持っています。これは Aria リポジトリ内の Lean 4 ツリー（proofs/lean4/QuantumProofs/QSP.lean）にあり、ファイルは sorry を含みません。

2 つの定理

順定理（qsp_unitary）。 任意の位相リスト φ と、s² = 1 − x² を満たす任意の (x, s) について、QSP の積 U は Uᴴ U = 1 を満たします。これがユニタリ性の要であり、位相リストに関する帰納法で、各回転が不変条件を保つことから証明されます。

逆定理（qsp_converse）。 任意の次数 d と、任意の許容される多項式の組 (A, C) — 許容性とは、偶奇性と次数の条件に加えて Gram 恒等式 A·A⋆ + (1−X²)·C·C⋆ = 1 を満たすこと — について、長さ d の位相リストが存在し、その QSP の積が 大域位相を除いて (A, C) を実現します。この大域位相の但し書きはごまかしではありません。SL₂ に由来する本物の障害であり、定理の主張の中で明示的に述べられています。

逆定理の証明の流れ

逆定理は、「剥がす（peel）」ステップを伴う次数に関する帰納法です。許容される次数 d の組が与えられたら、位相角をひとつ剥がし、次数を 1 下げ、再帰します。これを厳密にすることが作業の大半であり、次の補題の連鎖に分解されます。いずれも証明は完結しています。

• (0,0) における Gram 恒等式 — ユニタリ性の多項式恒等式 A·A⋆ + (1−X²)·C·C⋆ = 1。許容性の代数的な背骨です。
• gram_lead_modulus — この恒等式から、A と C の最高次係数の絶対値が等しいことが従います。
• cancel_angle_exists — 最高次の項を打ち消す角度が存在し、明示的な式で与えられます。
• peel_first_column_drop / peel_degree_drop — ひとつの角度で両方の多項式の次数が下がる。帰納法の各段です。
• parity_coeff_zero — 偶奇性の条件によって偶奇の合わない係数が消えるため、次数は 2 ではなく確実に 1 だけ下がります。
• gram_peel_invariant / realize_step — Gram 恒等式は剥がす操作のもとで保たれるため、再帰は許容集合の中に留まり、実現が再構成できます。
• 基底ケース d = 0, 1（構成的な角度の実現）と、明示的な次数 2 の段（qsp_converse_deg2：絶対値 1 のあらゆる (a, b) は 2 つの位相で実現される）。

これらはいずれも開いて読める名前付きの補題であり、「標準的な議論により」と書かれたコメントではありません。

なぜ逆定理をわざわざ証明するのか

QSP こそが、私たちの回路合成に関する主張の最終的な拠り所だからです。ブロックエンコードされた演算子の多項式変換を位相列へコンパイルするとき、そのコンパイルの正しさは逆定理 そのもの です。偶奇性、次数、Gram 恒等式、大域位相の但し書きまで含めて機械検証されているということは、合成の経路が、私たちが信用している論文ではなく、機械が検証した証明の上に成り立っているということです。

これは証明ツリーの他の部分 — ゲートの恒等式、Grover の限界、QFT/QPE の精度、ノイズチャネル、ブロックエンコーディングの主張 — と並んで、mathlib を用いた Lean 4 で書かれています。QSP のファイルは、その中で最も難しいものです。