Lean-QIT가 이번 논문에서 형식화했다고 밝힌 종점은 세 가지다. Schumacher 양자 소스 부호화 정리, Holevo–Schumacher–Westmoreland(HSW) 고전 용량 정리, 얽힘 보조 고전 용량 정리다. 얽힘 보조 경우에는 일반 용량과 strong-converse capacity가 해당 정보량과 일치하는 끝점도 부록에 제시했다.
이 정리들을 한 틀에 놓기 위해 유한 블록 프로토콜과 해석적 부등식, 점근 극한을 잇는 Lean 4 계층을 설계했다. 상태와 채널, 소스·채널 코드, finite-block 성능 기준, 가설검정, 원샷 양, 점근 rate 구성을 조합 가능한 인터페이스로 제공한다.
핵심 설계 원칙은 operational quantity를 analytic formula와 독립적으로 정의하는 것이다. achievable rate나 capacity를 정의에 미리 넣지 않고, 서로 독립적으로 적은 운용 객체와 정보이론적 특성화의 일치를 정리로 증명한다. Lean kernel이 확인하는 공개 엔드포인트와 그 엔드포인트를 받치는 API도 구분했다.
기반 계층에는 typed state와 CPTP 채널, 부분계·텐서곱, 고전 레지스터·측정, purification, 엔트로피·상호정보량, 샌드위치 Rényi 다이버전스, smooth entropy, 데이터 처리 정리가 포함된다. mutual information과 PSD reference를 쓰는 sandwiched Rényi의 데이터 처리 부등식을 재사용 가능한 정리로 노출했다.
| 형식화 경로 | 운용 객체 | 증명 종점 |
|---|---|---|
| Schumacher 소스 부호화 | 압축 코드·달성 가능 소스 rate | RSch(ρ)=S(ρ) |
| HSW 고전 통신 | 유한 메시지 코드·운용 capacity | C(N)=lim n→∞ (1/n)χ(N⊗n) |
| 얽힘 보조 고전 통신 | EA 코드·rate·strong-converse capacity | CEA(N)=eCEA(N)=I(N) |
자료: STORIUM 정리
논문이 적은 2026년 7월 9일 스냅샷 규모는 Lean 파일 200개 이상, 코드 15만 줄 이상이다. 이는 저자의 저장소 설명이지 별도의 독립 검증 수치는 아니다. AI 보조 형식화와 자동 증명 탐색의 지식 기반으로 쓸 수 있다는 언급도 가능성에 관한 것이며, 이번에 직접 제시된 성과는 kernel-checked 정리와 API다.
범위는 유한차원 양자정보이론이다. quantum·private capacity, channel simulation, reverse Shannon theorem, feedback-assisted tradeoff, resource inequality에는 추가 정보량과 자원 회계 계층이 필요하다고 적었다. Chengkai Zhu 등의 arXiv:2607.09632v1은 QIT 전체의 완결판이 아니라 세 코딩 정리를 공통 기계검증 기반에 올린 인프라 보고다.
저작권자 © STORIUM 무단전재 및 재배포 금지
