Tools, libraries, and project boundaries

Formalization stack

• Lean and Mathlib provide the proof language and mathematical library.
• Verso and Verso Blueprint build the checked Blueprint pages.
• Mermaid renders editable dependency diagrams; MathJax renders mathematics.
• Qiskit is used only where an executable validation route requests it; it is not a substitute for Lean.

Content boundary

This site is tailored to ASPBE state preparation, block encoding, circuit semantics, resource evaluation, and automation records. It does not import unrelated application terminology or status data from reference documentation.

External textbook memory

ATLAS v1, by Ahmad Rammal, Niket Patel, Fabian Gloeckle, Amaury Hayat, Julia Kempe, Remi Munos, Charles Arnal, and Vivien Cabannes, is indexed locally as a pinned external theorem-retrieval surface. Its source and generated theorem text remain under its CC BY-NC 4.0 and no-training terms; they are not copied into ASPBE MIT tree. Upstream compilation or evaluation does not replace an ASPBE adapter and Lean gate.

Interface inspiration

StatsMLlib demonstrates a useful textbook organization: a persistent book map, selected formulas, natural-language readings, source locations, organizers, and a visible contribution path. QuantumComputinglib uses independently written templates, CSS, JavaScript, diagrams, and quantum-computing content.

The local-compiler boundary and reviewed LaTeX-to-Lean workspace follow the proven design used by Auto-Bandit-RL-Proof-In-Sleep: the public site is static, while a loopback-only companion server may invoke the pinned Lean toolchain on temporary snippets. No bandit chapters, declarations, statuses, or theorem data are copied into QuantumComputinglib.