QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit ab8f277c5704 Build record

Papers · Block Encoding

Block Encoding papers

Block-encoding examples and papers: clean-block semantics, oracle access, source constructions, and same-target circuit improvements. A finite benchmark, a resource lemma, and a full paper reproduction remain distinct statuses.

Source-facing queue

Paper → numbered source anchor → public formalization boundary

Reproduced fixed benchmark

Quantum Framework for Simulating Linear PDEs with Robin Boundary Conditions

Nikita Guseynov, Xiajie Huang, Nana Liu · 2025

Source anchors. Eq. (9), Theorem 3, Theorem 4, Fig. 4

Formalized now. Theorem 3/4 are mapped to explicit Lean scope. The fixed N=8 Robin benchmark closes source normal forms, an exact XOR four-slot winner, and same-tier resource comparisons; the arbitrary-width primitive compiler remains a separate frontier.

Remaining paper-wide scope. See the full reproduction page for the exact boundary.

Read reproduction Source paper ↗