ASPBE
State preparation, block encoding, finite circuit semantics, construction routes, resource records, automation, and certified cases.
Quantum Lean ecosystem
One reading map, honest dependency boundaries
QuantumComputinglib brings ASPBE declarations, selected external quantum-formalization references, and textbook explanations into one map. “Indexed” does not mean “imported”: every row states how the source is used.
Libraries represented in QuantumComputinglib
Built here
Mathlib
Finite types, matrices, algebra, norms, finite sums, and proof infrastructure used by the local Lean package.
quantum-computing-lean
Named states, gates, projectors, gate actions, decompositions, and compact finite-dimensional module organization.
Lean-QuantumInfo
Finite-dimensional quantum and classical information, channels, distributions, entropy, and capacity.
lean-quantum
Quantum states, channels, qudits, operator conventions, and higher-level quantum-information semantics.
How an external result enters the library
- Reference. Record the upstream repository, license, module, and exact declaration.
- Adapter. State the narrow ASPBE bridge without copying incompatible APIs.
- Compile. Import or prove the adapter under the pinned toolchain.
- Teach. Add the formula, plain-language reading, assumptions, and source link.
This prevents a survey entry or theorem card from appearing as a locally compiled result.