New reading rule

Every case now follows the same theorem-first path

Why would a quantum algorithm need this state or operator?
How should you read the circuit?
What is the exact theorem statement?
What is the proof idea in human mathematics?
Only then, optionally open the Lean checkpoints.
If ASPBE improves a circuit, the comparison theorem appears after correctness.

Reproducible reading paths

Case studies, from equation to circuit

Each case begins with the operator or target state, fixes the acceptance contract, and then shows the circuit and resource trace. “Certified” means a named Lean root compiled in this checkout. Qiskit and other fast backends may screen and prioritize routes; a floating-point match alone is not the final exact proof.

How to read a score

The tuple is ordered lexicographically as (gate count, parallel depth, auxiliary qubits, oracle calls). A page says “strictly better” only when it links the corresponding Lean betterThan theorem. Routes at different semantic tiers are not compared.

State preparation

Preparing the basis state |1>

The smallest complete state-preparation certificate: target normalization, unitary matrix, exact state action, and resource tuple.

X|0\rangle=|1\rangle,\qquad X=\begin{pmatrix}0&1\\1&0\end{pmatrix}.

Lean certifiedexact one-qubit circuit

State preparation

Preparing the equal superposition |+>

A familiar quantum gate becomes a complete exact certificate rather than a numerical statevector check.

H|0\rangle=|+\rangle=\frac{|0\rangle+|1\rangle}{\sqrt 2},\qquad H=\frac1{\sqrt2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}.

Lean certifiedexact one-qubit circuit

Block encoding

BE Case 1: finite transfer operator

A concrete non-unitary transfer is embedded in a permutation unitary and improved from (6,5,1,0) to (4,2,1,0).

E_1=|0\rangle\!\langle1|_{\mathrm{time}}\otimes|0\rangle\!\langle1|_{\mathrm{type}}\otimes I_2,\qquad \langle0|_aU|0\rangle_a=E_1.

Lean certifiedexact finite logical reversible circuit

Block encoding

BE Case 1: isolated cold reconstruction

An isolated route closes the same mathematical contract with its own exact permutation and score (5,5,1,0).

E_1=|0\rangle\!\langle1|_{\mathrm{time}}\otimes|0\rangle\!\langle1|_{\mathrm{type}}\otimes I_2,\qquad \langle0|_aU_{\mathrm{cold}}|0\rangle_a=E_1.

Lean certifiedexact finite logical reversible circuit

Block encoding

BE Case 2: cubic diagonal family, cold route

A symbolic exact family theorem replaces finite numerical acceptance with rational Householder certificates for every n.

D_n=\operatorname{diag}_{0\le j<2^n}\!\left(\frac{j}{2^n}\right)^3,\qquad \Pi U_n\Pi^\dagger=D_n.

Lean certifiedsymbolic exact rational family

Block encoding

BE Case 2: cubic diagonal family, hinted route

A direct hint becomes a short formal route with separate exact Lean roots for the input and output blocks.

O_0=\sum_{j=0}^{2^n-1}x_j|j\rangle\!\langle j|,\quad x_j=\frac{j}{2^n},\qquad D_n=O_0^3=\sum_jx_j^3|j\rangle\!\langle j|.

Lean certifiedsymbolic exact rational family

Block encoding

GHL Eq. (9) benchmark at N=8 (A1=B1=0)

Lean block-encodes the dimensionless A1=B1=0 specialization of GHL Eq. (9), explicitly distinguishes it from the physical Delta x^{-2} matrix, closes both source realizations and the evolved candidate at the exact primitive level, and certifies the candidate's same-tier improvement.

A_{\mathrm{GHL}}^{(9)}=\Delta x^{-2}\,\widetilde A(A_1\Delta x,B_1\Delta x),\qquad \widetilde A_0:=\widetilde A(0,0)=\frac1{12}\begin{pmatrix}-30&32&-2&0&0&0&0&0\\16&-31&16&-1&0&0&0&0\\-1&16&-30&16&-1&0&0&0\\0&-1&16&-30&16&-1&0&0\\0&0&-1&16&-30&16&-1&0\\0&0&0&-1&16&-30&16&-1\\0&0&0&0&-1&16&-31&16\\0&0&0&0&0&-2&32&-30\end{pmatrix},\qquad \Pi U\Pi^\dagger=\frac{\widetilde A_0}{56/3}=\frac{M}{224},\quad M=12\widetilde A_0.

Lean certifiedExact primitive source reproductions and certified same-tier winner

Contribute a checked variant

Generated drafts are welcome. Public retrieval begins only after review, a repository declaration, and the advertised gates pass.

Share a State Preparation example Share a Block Encoding example