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

Part IV · Planned

Quantum Algorithms for Scientific Computation

Lin–Wiebe's scientific-computing progression reuses Part II Block Encoding and adds transforms, simulation, estimation and application contracts.

Read the curriculum anchor →

Truth boundary

Placement is not proof

This catalog is a textbook placement map. A listed source, upstream Lean cluster, or extended chapter is not a local ASPBE theorem unless an exact compiled declaration is linked separately.

OpenAI Math boundary. Audited clusters are pinned source or adapter inputs. Their upstream Lean 4.34.1 results are not local Lean 4.33.0 declarations until separately ported and compiled. Lean 4.33.0 is the migration target; this reader release preserves the published proof tree and records its actual version in the build evidence.

Graph-driven chapter map

Shared foundations first, source-specific consumers later

qsc-foundations

Probability, channels, query models, perturbation and statistics

Share QIT states/channels/distances and make query construction, precision and readout costs explicit.

Planned
Inspect pinned upstream memory (2 routes)

OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0. Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.

  • oai-entanglement

    InformationTheory/Entanglement

    candidate foundational QIT spine; declaration-by-declaration admission only

    Upstream evidence: lean-present-not-single-comparator-audited. adapter-backed. Not local admission.

    Next boundary: A local semantic adapter and independent publication review are still required.

  • oai-randomized-quantum-query-separation

    preprints/A-Nearly-Quartic-Separation-Between-Randomized-and-Quantum-Query-Complexity-October-5-2026

    quantum query-complexity frontier

    Upstream evidence: manuscript-only-in-current-audit. benchmark-only. Not local admission.

    Next boundary: locate exact formalization/comparator mapping before any Lean-status claim; then connect to query/oracle complexity graph

qsc-transforms

Amplification, qubitization, QSP and QSVT

Separate polynomial/signal-transform correctness from phase synthesis and finite-gate compilation.

Planned

qsc-simulation

Hamiltonian simulation and dynamics

Compose access, block/qubitization suppliers, approximation and successful execution under one resource tier.

Planned

qsc-fourier-estimation

Fourier transforms, phase estimation and amplitude estimation

Use the Comparator-backed exact Fourier route as an external resource theorem after circuit-model adaptation; it does not itself certify QPE.

Planned
Inspect pinned upstream memory (1 routes)

OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0. Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.

  • oai-exact-fourier

    Computability/FourierCircuit

    exact Fourier-circuit construction and resource theorem; supplier to Fourier/QPE chapters after circuit-model adaptation

    Upstream evidence: comparator-backed. source-route. Not local admission.

    Next boundary: compare circuit ordering, gate set and cost tuple with the local circuit/resource API; do not present the Fourier result as a block encoding or QPE certificate

qsc-eigen-ground

Eigenvalue and ground-state algorithms

Charge trial-state preparation, overlap, gap, precision, amplification and final classical output.

Planned

qsc-linear-open

Linear systems, differential equations and open systems

Reuse block/channel nodes and expose input, condition-number, success and readout assumptions rather than hiding them in an oracle.

Planned
Inspect pinned upstream memory (1 routes)

OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0. Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.

  • oai-amplitude-damping

    InformationTheory/AmplitudeDamping

    quantum channel, entropy, Holevo information, and operational capacity

    Upstream evidence: comparator-backed. source-route. Not local admission.

    Next boundary: A local semantic adapter and independent publication review are still required.

qsc-compiler-complexity

Extended chapter: compilers, synthesis and circuit lower bounds

Exact factoring, shallow-circuit parity and oracle-assisted unitary synthesis extend the computing curriculum without counting as SP/BE successes.

Planned
Inspect pinned upstream memory (3 routes)

OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0. Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.

  • oai-quantum-circuit

    InformationTheory/QuantumCircuit

    Candidate circuit-model and resource adapter.

    Upstream evidence: comparator-backed. adapter-backed. Not local admission.

    Next boundary: A local semantic adapter and independent publication review are still required.

  • oai-exact-quantum-factoring

    Computability/QuantumFactoring

    full quantum algorithm/circuit/compiler route with arithmetic, oracle and resource semantics

    Upstream evidence: comparator-backed. source-route. Not local admission.

    Next boundary: mine circuit/compiler/resource primitives that can share with ASPBE before exposing the factoring endpoint

  • oai-unitary-synthesis-boolean-oracle

    preprints/Polynomial-Time-Unitary-Synthesis-from-a-Boolean-Oracle-October-5-2026

    oracle-assisted unitary synthesis frontier directly relevant to ASPBE synthesis semantics

    Upstream evidence: manuscript-only-in-current-audit. benchmark-only. Not local admission.

    Next boundary: compare target/operator/oracle/resource contract with the ASPBE synthesis API before formal route creation

qsc-many-body-models

Extended chapter: many-body model targets

The Comparator-backed Laughlin route is a model-side spectral target and reusable mathematical substrate, not evidence of a quantum algorithm or simulator.

Planned
Inspect pinned upstream memory (1 routes)

OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0. Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.

  • oai-laughlin

    Analysis/Laughlin

    many-body model-side mathematical target; not a quantum-algorithm or simulator certificate

    Upstream evidence: comparator-backed. source-route. Not local admission.

    Next boundary: A local semantic adapter and independent publication review are still required.

Search across all four textbooks →