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

Formal quantum computing, read alongside Lean

QuantumComputinglib

QuantumComputinglib is the textbook and declaration browser for ASPBE. The current book has two primary parts: State Preparation and Block Encoding. State Preparation is the nested preparation layer used by many broader block-encoding constructions; its certificate remains meaningful on its own. A reverse block-to-state use is a separate downstream theorem with additional input, success, normalization and amplification obligations.

Start with state preparation Study block encoding See the full reading guide →

Choose the problem first

Two parts, one inclusion direction, one shared graph

The main curriculum relation is State Preparation → Block Encoding: PREPARE is a reusable subproblem inside many block-encoding routes. A block-to-state consumer path also exists, but it is not the inclusion relation and it needs extra branch, normalization and amplification hypotheses. Shared foundations are authored once rather than duplicated.

Part I

State preparation

\[U|0^n\rangle=|\psi\rangle\]

Fix a normalized target state, construct a unitary, and prove that its action on the all-zero state gives exactly those amplitudes.

Read the state-preparation route →

Part II

Block encoding

\[\Pi U\Pi^\dagger=A/\alpha\]

Fix an operator, normalization, ancilla convention, and register order; then prove that the projected block of a larger unitary has the requested value.

Read the block-encoding route →

State-preparation workflow

From a target vector to a preparation certificate

Normalization, unitarity, and state action are separate obligations. The first-column identity is the matrix form of the same state-action equation.

State-preparation proof and export flow editable Mermaid source 
flowchart LR
  T["Target state<br/>|ψ⟩"] --> N["Check normalization<br/>⟨ψ|ψ⟩ = 1"]
  N --> C["Choose a circuit<br/>or unitary completion"]
  C --> U["Prove U is unitary"]
  C --> A["Prove the state action<br/>U|0ⁿ⟩ = |ψ⟩"]
  U --> L["Lean state-preparation<br/>certificate"]
  A --> L
  L --> E["Export one certified<br/>finite instance"]

  classDef target fill:#ffffff,stroke:#6b6045,color:#222222,stroke-width:1.5px;
  classDef work fill:#ffffff,stroke:#64747a,color:#222222,stroke-width:1.25px;
  classDef proof fill:#ffffff,stroke:#2f7355,color:#18382b,stroke-width:1.5px;
  class T,N target;
  class C,U,A work;
  class L,E proof;

Block-encoding workflow

From an operator contract to a clean-block certificate

This route introduces choices that state preparation does not need: ancilla count, a clean projector, register layout, normalization \(\alpha\), and an exact or approximate block norm.

Block-encoding proof and export flow editable Mermaid source 
flowchart LR
  T["Target operator A<br/>and scale α"] --> R["Fix ancillas, norm,<br/>and register order"]
  R --> C["Choose a construction<br/>family and unitary U"]
  C --> U["Prove U is unitary"]
  C --> B["Prove the clean block<br/>‖A − α Π U Π†‖ ≤ ε"]
  U --> L["Lean block-encoding<br/>certificate"]
  B --> L
  L --> E["Export and check one<br/>certified finite instance"]

  classDef target fill:#ffffff,stroke:#49677d,color:#1f2e39,stroke-width:1.5px;
  classDef work fill:#ffffff,stroke:#64747a,color:#222222,stroke-width:1.25px;
  classDef proof fill:#ffffff,stroke:#2f7355,color:#18382b,stroke-width:1.5px;
  class T,R target;
  class C,U,B work;
  class L,E proof;

Current checkout

What this build actually certifies

4,524explicit public declarations
2,337source docstrings
395experimental declarations
0explicit incomplete proofs
9guided learning chapters

Compiled means the Lean and test gates passed on commit c681192368c2. A contract record may compile even when a concrete construction route is still partial; the site shows those two statuses separately.

Shared evidence discipline

What happens after either contract is fixed

ASPBE explores candidates, records why routes fail, and lets Lean decide formal promotion. A Qiskit check is useful finite evidence after certification; it does not prove a symbolic family.

Shared certification and feedback loop editable Mermaid source 
flowchart LR
  C["Fixed mathematical<br/>contract"] --> O["Named proof<br/>obligations"]
  O --> P["Candidate routes<br/>with provenance"]
  P --> L{"Lean gate"}
  L -- "proof fails" --> F["Classified failure<br/>and next local lemma"]
  F --> P
  L -- "certificate compiles" --> X["Finite export<br/>and circuit check"]
  X --> D["Documented result<br/>with stated scope"]

  classDef contract fill:#f8f5ee,stroke:#826a32,color:#222222,stroke-width:1.5px;
  classDef process fill:#ffffff,stroke:#64747a,color:#222222,stroke-width:1.25px;
  classDef gate fill:#edf5f1,stroke:#2f7355,color:#18382b,stroke-width:1.5px;
  classDef feedback fill:#fff2ef,stroke:#a44b3f,color:#4a2520,stroke-width:1.25px;
  class C contract;
  class O,P,X,D process;
  class L gate;
  class F feedback;

Use the project

Read, formalize, or submit a construction

The public site is not only a declaration catalog. It keeps the original user-facing task builder, the local-compilation workspace, and the reviewed contribution route beside the textbook.

Read

Learn from a checked chapter

Follow a formula from its physical meaning to the exact Lean declaration.

Open the book map →
Formalize

Compare LaTeX and Lean

Edit a theorem, inspect dependencies, and compile temporary code with the local companion.

Open the workspace →
Run

Build an ASPBE task packet

Describe a target state or operator, choose a harness, and export a reproducible task packet.

Open the task builder →

Project record

News and auditable priority

The dates below are repository milestones. They do not replace the generated proof-status pages.

  1. Statement Seal, evidence memory, and proof digestion.

    QuantumComputinglib now freezes source-facing quantum contracts before proof search, types and salvages failed routes before cleanup, keeps environment/API failures separate from mathematical refutation, defaults routine coordination to deterministic/low-token control in light of local route-ablation evidence, requires distinct uncertainty for parallel Workers, and seals PURIFIED reader explanations against the source and Lean graphs.

  2. Schrödingerisation smooth auxiliary-state preparation: exponential-to-linear in the grid-register width.

    The smooth auxiliary \(p\)-register state required by Jin–Liu–Ma’s PDE Schrödingerisation construction, viewed alongside the smooth-function state-preparation route of Holmes–Matsuura, has exact Hermite–Bernstein/tensor-train structure. ASPBE turns generic \(\Theta(2^{n_p})\) amplitude loading into \(G\le48n_p(2k+6)^3\), hence \(O(n_p)\) gates for fixed \(k\), with \(O(\log k)\) workspace. Open the Lean-verified worked case →

  3. Robin boundary block encoding: a smaller certified primitive.

    For the selected \(n=3\) Robin boundary instance in Guseynov–Huang–Liu, Block encoding by signal processing, ASPBE reduced the audited \(T^{\dagger 3}\) branch from 49 to 30 \(T^{\dagger 3}\) gates and from 52 to 32 CNOTs, with the same five qubits and zero ancillas under the fixed primitive model.

  4. ASPBE and QuantumComputinglib.

    The two application tracks, local workspace, task builder, and contributor review path are presented in one site.

  5. Blueprint and Library Explorer.

    One generated inventory now drives the checked Blueprint catalog and searchable declaration browser.

  6. Public testing preview.

    The site exposed separate State Preparation and Block Encoding directions and the user task builder.

  7. Earliest repository record.

    The initial commit and timestamped manifest begin the public, auditable project history. No earlier date is asserted without evidence.

Reading guide

Follow one application without losing the shared foundations

Part I · State Preparation

Chapters 1–2 are shared foundations authored once and reused by Block Encoding; Chapters 3–4 specialize them to preparation certificates.

01 Vectors, matrices, and basis states Fix the finite matrix model, pointwise equality, dimensions, and resource records used by every later certificate. 02 Gates, unitaries, and circuit meaning Separate gate syntax from matrix evaluation and make register order an explicit part of the semantic boundary. 03 The state-preparation problem Ask one concrete question: which unitary sends the all-zero basis state to the normalized state we want? 04 Reading and reusing a preparation certificate Connect the ket equation to a matrix column, package the proof, and reuse exact preparation where an approximate interface is expected.

Part II · Block Encoding

Block Encoding reuses the same finite-matrix and circuit nodes, then adds projected-block, composition, resource and proof-gated construction obligations.

05 The block-encoding contract State the block contract with normalization, explicit register layout, and a verifier-facing certificate record. 06 Construction routes and composition rules Reuse permutation, one-sparse, LCU, product, dilation, and QSVT interfaces instead of rediscovering each route per benchmark. 07 Certified block-encoding cases Distinguish completed local certificates from paper-facing contract models and historical experiments. 08 Candidate comparison and executable exports Keep formal validity lexicographically ahead of resource quality, then expose accepted candidates to executable tooling. 09 Search control, evidence, and open work Show how typed stages, agent layers, candidate populations, proof gates, and explicit open problems coordinate without overstating evidence.

Audit the source

Explanation, inventory, and checked Blueprint

The chapters teach selected results. The Library Explorer inventories every explicit public declaration. The Verso Blueprint resolves its Lean references during the build.

Implementation map Library Explorer Verso Blueprint Task builder →