QuantumComputinglib learn · inspect · formalize
Checked on this commit 2,822 public declarations commit 07559c3d051f Build record
Reading mode Start visually; reveal formalism only when you want it.

Beginner layer · worked examples

A proof is easier to understand when you can watch one basis state travel through the circuit

The case studies are not decoration. Each one freezes a matrix, a register layout, and a circuit, then lets you compare the paper picture, the executable circuit, and the Lean theorem.

Case-study reading order: target → circuit → clean block → resource comparison.
target A construct ULean ✓resource verified BE
  1. FreezeName the exact finite target and normalization.
  2. TraceFollow clean basis inputs through the candidate circuit.
  3. ProvePromote only after unitarity and every clean-block entry are exact.
  4. CompareOnly candidates at the same semantic tier may be compared by resources.

Strict mathematics, after the picture

The equations behind the intuition

\[\Pi U\Pi^\dagger=A/\alpha\]
\[\text{score}=(\text{gates},\text{depth},\text{aux qubits},\text{oracle calls})\]

Every symbol used here is connected below to a compiled declaration or a clearly marked research-source formula.

Learn Lean while learning quantum computing

Lean idea: theorem names are checkpoints

warmRobinFigure4PrimitiveVerifiedBlockEncoding
warmRobinBestVerified

A reader can jump from a diagram directly to the declaration that certifies the same stage.

The full proof-backed declarations for this chapter are shown immediately below.

Block encoding · Chapter 7 of 9

Certified block-encoding cases

Distinguish completed local certificates from paper-facing contract models and historical experiments.

Lean modules used in this chapter
  • QuantumBlockEncoding/ColdStartTransferE1.lean
  • QuantumBlockEncoding/OptimalControl.lean
  • QuantumBlockEncoding/CubicStatePreparation.lean
  • QuantumBlockEncoding/GHL2025.lean
  • QuantumBlockEncoding/GHLHamiltonian.lean
  • QuantumBlockEncoding/Examples/RobinHeat.lean
  • QuantumBlockEncoding/RobinMatrix.lean

Textbook lesson

Build the idea before opening the proof

Case studies show both successful certificates and rejected routes. A refutation is a completed result when it prevents reuse of a false premise.

Accepted cases

\[\text{candidate}\rightarrow\text{unitary proof}\rightarrow\text{clean block}\rightarrow\text{cost}.\]

BE Case 1 uses finite permutation structure. BE Case 2 uses an exact rational Householder completion. Both end at named compiled roots.

Robin audit closure

\[U_{00}\ne\sum_s B_s\quad\text{for the historical H-free target}.\]

The raw symbolic route is not merely slow: the current target is false. Lean proves the contradiction through a concrete coefficient environment.

From one-term operators to the Hamiltonian

\[A=\sum_kA_k,\quad A^\dagger=\sum_kA_k^\dagger,\quad H=S_1\otimes x_\xi+S_2\otimes I_\xi.\]

The paper itself carries this composition through Theorem 4. ASPBE compiles the same A/A-dagger, S1/S2, and H chain and also checks the LCU filler phases rather than treating the displayed matrix equality as self-evident.

A source audit matters

\[e^{i\pi}=e^{-i\pi}=-1.\]

Under a literal full-clean-matrix reading, the printed first S1 LCU phase pair leaves a lower-right -N_A identity filler. Lean records that obstruction and separately proves the phase-balanced correction that yields the intended S1 matrix; S2 closes with the printed zero phases.

The remaining compiler frontier

\[\text{source theorem}\to\text{arbitrary-width primitive gate list}.\]

What remains open is not the Hamiltonian formula: it is a uniform primitive compiler proving all general-width one-term oracle resource bounds at the source paper's gate tier.

Check your understanding

Check both badges: a local theorem may compile while a larger paper route remains experimental.

Mathematical order and conventions adapted from Lin, Lecture Notes on Quantum Algorithms for Scientific Computation. The formal checkpoints and ASPBE status distinctions are specific to this library.

Route at a glance

Where these results sit

Block encoding: Certified block-encoding cases editable Mermaid source 
flowchart LR
  C["Compiled<br/>core contracts"] --> E["Compiled<br/>BE Case 1 and 2"]
  E --> P["Partial route<br/>amplitude oracle"]
  P --> Q["Planned<br/>concrete QSVT"]
  E --> X["Experimental<br/>paper backend"]
  X --> B["Blocked<br/>historical raw fold"]
  B --> F["Finite semantic bridge<br/>and projection proof"]

Selected declarations

Read the mathematics beside the Lean statement

A compiled route means that the reusable theorem or constructor and at least one finite witness compile. Hardware- and problem-specific downstream instantiations are out of scope, not universal claims made by these cards.

Lean result

BE Case 1 block projection

QuantumBlockEncoding.coldE1Candidate_blockProjection
DeclarationCompiled Full routeCompiled
\[\Pi U_{\mathrm{E1}}\Pi^\dagger=A_{\mathrm{E1}}/\alpha.\]

What it says

The selected transfer-operator candidate has the required projected block.

Why it matters

The benchmark closes from a concrete candidate to the exact block identity. It is a compact reproducible example of the complete ASPBE acceptance path.

How the proof goes

Reuse the partial-permutation image certificate and simplify the selected entries.

Uses
QuantumBlockEncoding.coldE1CandidateImage_permutation_certificate; QuantumBlockEncoding.BlockEncodingClassics.partialPermutationCertificate
Still outside this result
None for this local declaration.

Route closure

Natural-language steps and Lean objects

Mathematical stepLean object or step
Certify routed basis images.coldE1CandidateImage_permutation_certificate
Project the clean block.coldE1Candidate_blockProjection
Open the Lean statement and source links 
theorem coldE1Candidate_blockProjection :
    coldE1BlockProjection coldE1CandidateMatrix := by

Local declaration · Verso Blueprint · commit-pinned GitHub source

Lean result

BE Case 2 exact Householder completion

QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract_complete
DeclarationCompiled Full routeCompiled
\[\Pi U_{\mathrm{cubic}}\Pi^\dagger=D_{\mathrm{cubic}}/\alpha.\]

What it says

The cubic diagonal benchmark has a completed exact block-encoding contract through the rational Householder route.

Why it matters

The hard benchmark converges by selecting a library-supported algebraic route, not by expanding a large gate fold. It records a completed alternative to the still-partial amplitude-oracle/QSVT route.

How the proof goes

Complete the input Householder certificate, instantiate rational backend support, and package the cubic target identity.

Uses
QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderInputBEContract_complete; QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalRationalCompletion_backendSupport
Still outside this result
None for this local declaration.

Route closure

Natural-language steps and Lean objects

Mathematical stepLean object or step
Complete the linear input block.linearDiagonalHouseholderInputBEContract_complete
Supply rational backend support.cubicDiagonalRationalCompletion_backendSupport
Assemble the final certificate.cubicDiagonalHouseholderExactBEContract_complete
Open the Lean statement and source links 
theorem cubicDiagonalHouseholderExactBEContract_complete (n : Nat) :
    BlockEncodingClassics.IsRationalOrthogonal
        (cubicDiagonalHouseholderExactBEContract n).exactPayload.U ∧
      Matrix.PointwiseEq
        (cubicDiagonalHouseholderExactBEContract n).exactPayload.clean
        (cubicDiagonalTarget n).operator ∧
      (cubicDiagonalTarget n).normalizer = 1 ∧
      (cubicDiagonalHouseholderExactBEContract n).resource =
        Resource.ofCountsWithDepth 0 0 1 0 1 := by

Local declaration · Verso Blueprint · commit-pinned GitHub source

Lean result

GHL Theorem 4: source-audited LCU composition to the Hamiltonian

QuantumBlockEncoding.GHL2025.Hamiltonian.theorem4_source_lcu_route_closed
DeclarationCompiled Full routeCompiled
\[A=\sum_kA_k,\quad A^\dagger=\sum_kA_k^\dagger,\quad H=S_1\otimes x_\xi+S_2\otimes I_\xi.\]

What it says

The paper's Theorem 4 route is now machine-checked from A and A-dagger through the LCU clean blocks for S1 and S2, then to H, together with the registered normalization, signal-width, and resource expressions.

Why it matters

ASPBE does not silently copy the displayed phases: a literal full-clean-matrix reading of the printed first LCU line leaves a nonzero lower-right filler because exp(i*pi)=exp(-i*pi)=-1. Lean proves that obstruction, then proves a phase-balanced correction gives exactly S1; the printed S2 line closes as written. This is the distinction the public status needs: the Hamiltonian composition is not open, but the source-phase audit and the remaining arbitrary-width primitive compiler must stay visible.

How the proof goes

Assemble A and A-dagger from one-term inputs; audit the controlled-phase filler in the first S1 LCU; use the phase-balanced correction to obtain S1; verify the S2 LCU; then compose the two Hermitian pieces with x_xi and I_xi and attach the paper-facing normalization/resource record.

Uses
QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint_sumTerms; QuantumBlockEncoding.Robin.ComplexLCU.prepareAmplitudeSelectUnprepare_unitary; QuantumBlockEncoding.Robin.ComplexLCU.prepareAmplitudeSelectUnprepare_cleanEntry; QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_ne_S1; QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean_eq_S1; QuantumBlockEncoding.GHL2025.Hamiltonian.eq30Clean_eq_S2
Still outside this result
The source-audited Theorem-4 composition is closed. Uniform arbitrary-width primitive compilation of all Theorem-3 source oracles and their concrete gate/resource realization remains a separate compiler frontier.

Route closure

Natural-language steps and Lean objects

Mathematical stepLean object or step
Assemble A and A-dagger.adjoint_sumTerms / Adagger_eq_sum_term_adjoints
Refute the literal printed filler cancellation.eq29PrintedClean_ne_S1
Close the corrected S1 clean block.eq29PhaseBalancedClean_eq_S1
Close S2 from the printed second LCU line.eq30Clean_eq_S2
Close H plus source metadata.theorem4_source_lcu_route_closed
Open the Lean statement and source links 
theorem theorem4_source_lcu_route_closed [DecidableEq ι] [DecidableEq ξ]
    {η : Type*} [Fintype η]
    (cert : OneDimCompositionCertificate η ι ξ)
    (normalizerA : ℂ) :
    eq29PhaseBalancedClean cert.A cert.B normalizerA = cert.first ∧
    eq30Clean cert.A cert.B normalizerA = cert.second ∧
    cert.H = add (tensor cert.first cert.xXi)
      (tensor cert.second (identity ξ)) ∧
    oneDimHamiltonianClaim.normalization = "O(kappa * ||H||_max)" ∧
    oneDimHamiltonianClaim.resource = oneDimHamiltonianResourceExpr := by

Local declaration · Verso Blueprint · commit-pinned GitHub source

Lean result

Robin raw-fold route is rejected

QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryUnitaryEntry_ne_backendFold_n3
DeclarationCompiled Full routeCompiled
\[U_{00}\ne\sum_{s=0}^{6} B_s.\]

What it says

The historical H-free symbolic entry is proved not equal to the proposed seven-slot backend fold.

Why it matters

The all-one coefficient environment exposes a nonzero selected contribution that the old equality would force to zero. A proved counterexample closes this search branch and prevents future agents from spending budget on a false target.

How the proof goes

Assume the raw fold, convert it to the equivalent backend-expansion statement, and contradict the compiled all-one counterexample.

Uses
QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryBackendExpansionStatement_not_n3; QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryBackendExpansionStatement_equivUnitaryEntryFold_n3
Still outside this result
The rejected branch is closed. Fixed-N8 source circuits and the GHL Theorem-4 A-to-H composition are compiled; arbitrary-width primitive compilers for the general source oracles remain separately scoped.

Route closure

Natural-language steps and Lean objects

Mathematical stepLean object or step
Assume the historical raw equality.intro hFold
Move to the equivalent expansion target.equivUnitaryEntryFold_n3.mpr
Apply the counterexample.BackendExpansionStatement_not_n3
Open the Lean statement and source links 
theorem oneTermRobinGamma3BoundaryUnitaryEntry_ne_backendFold_n3 :
    oneTermRobinGamma3BoundaryProjectionSummationTarget_n3.signalUnitaryEntry ≠
      blockExtractionBranchContributionSum
        oneTermRobinGamma3BoundaryBackendBranchContribution_n3 := by

Local declaration · Verso Blueprint · commit-pinned GitHub source