양자 신호 처리의 형식화: Lean 4로 증명한 역정리

양자 신호 처리(Quantum Signal Processing, QSP)는 QSVT, 블록 인코딩, 해밀토니안 시뮬레이션을 받치는 근간입니다. 고정된 신호 연산자와 번갈아 배치된 단일 큐비트 회전들의 곱은 그 행렬 성분으로 신호에 대한 다항식 쌍을 계산합니다. 정방향 — 어떤 위상 목록이든 그 성분이 유니터리 제약을 만족하는 차수 제한 다항식인 유니터리를 만든다는 것 — 은 쉬운 절반입니다. 역방향 — 모든 허용 가능한 다항식 쌍이 어떤 위상 열로 실현된다는 것 — 은 QSP를 단순한 호기심거리가 아닌 설계 도구로 만드는 정리입니다. 동시에 대부분의 논문이 대충 넘어가는 부분이기도 합니다.

우리는 두 방향 모두에 대한 기계 검증 증명을 갖고 있습니다. Aria 저장소 안의 Lean 4 트리(proofs/lean4/QuantumProofs/QSP.lean)에 있으며, 이 파일에는 sorry가 없습니다.

두 정리

정방향 (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을 더한 것 — 에 대해, QSP 곱이 전역 위상을 제외하고 (A, C)를 실현하는 길이 d의 위상 목록이 존재합니다. 전역 위상 조건은 허술함이 아닙니다. 실제 SL₂ 장애물이며, 정리 서술에 명시적으로 이름을 붙여 두었습니다.

역정리는 어떻게 증명되는가

역정리는 “벗겨내기(peel)” 단계를 가진 차수 귀납법입니다. 허용 가능한 차수 d 쌍이 주어지면 위상 각도 하나를 벗겨내 차수를 하나 낮추고 재귀합니다. 이를 엄밀하게 만드는 것이 작업의 대부분이며, 모두 닫힌 보조정리들의 연쇄로 분해됩니다.

• (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 — 패리티 조건이 패리티에 맞지 않는 계수를 0으로 강제하므로, 차수가 2가 아니라 정확히 1만큼 떨어진다는 것.
• gram_peel_invariant / realize_step — 벗겨내기 아래에서 Gram 항등식이 보존되므로 재귀가 허용 가능한 집합 안에 머물고 실현이 다시 조립된다는 것.
• 기저 사례 d = 0, 1(구성적 각도 실현)과 명시적인 차수 2 단(qsp_converse_deg2: 절댓값이 1인 모든 (a, b)는 두 위상으로 실현됨).

이들 각각은 열어서 읽을 수 있는 이름 붙은 보조정리이며, “표준적인 논증에 의해”라고 적힌 주석이 아닙니다.

왜 굳이 역정리를 증명하는가

QSP가 우리의 회로 합성 주장이 최종적으로 기대는 지점이기 때문입니다. 블록 인코딩된 연산자의 다항식 변환을 위상 열로 컴파일할 때, 그 컴파일의 정확성이 곧 역정리입니다. 패리티, 차수, Gram 항등식, 전역 위상 조건까지 모두 기계 검증되어 있다는 것은, 합성 경로가 우리가 믿는 논문이 아니라 기계가 확인한 증명 위에 서 있다는 뜻입니다.

이 증명은 증명 트리의 나머지 부분과 나란히 놓여 있습니다. 게이트 항등식, Grover 한계, QFT/QPE 정확도, 잡음 채널, 그리고 mathlib을 사용한 Lean 4 블록 인코딩 명제들입니다. 그중 QSP 파일이 가장 어렵습니다.