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.

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.