All missions

Motivation

Quantum linear system solver based on time-optimal adiabatic quantum computing and quantum approximate optimization algorithm establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $n\in\mathbb N$, $N=2^n$, and let $A\in\mathbb C^{N\times N}$ be Hermitian positive definite with $\|A\|_2=1$. Let $b\in\mathbb C^N$ be a unit vector. Here $\|\cdot\|_2$ denotes the operator norm for matrices and the Euclidean norm for vectors. Write

$$\kappa=\|A\|_2\|A^{-1}\|_2,\qquad x=\frac{A^{-1}b}{\|A^{-1}b\|_2},\qquad \widetilde x=|0\rangle\otimes x.$$

The condition number is the actual value determined by $A$, and satisfies $\kappa\ge1$.

Set $Q_b=I-|b\rangle\langle b|$ and

$$H_0=\begin{pmatrix}0&Q_b\\Q_b&0\end{pmatrix},\qquad H_1=\begin{pmatrix}0&AQ_b\\Q_bA&0\end{pmatrix}.$$

For $p>0$, AQC($p$) uses the schedule $f_p:[0,1]\to[0,1]$ specified by

$$f_p'(s)=c_p(1-f_p(s)+f_p(s)/\kappa)^p,\quad f_p(0)=0,\qquad c_p=\int_0^1(1-u+u/\kappa)^{-p}\,du.$$

Thus $f_p(1)=1$. The schedule is $f_p(s)=s$ when $\kappa=1$; when $\kappa>1$ and $p=1$, it is $\kappa(1-\kappa^{-s})/(\kappa-1)$; otherwise it is the closed formula in Eq. (6). For positive runtime $T$, the normalized evolution $\psi_T:[0,1]\to\mathbb C^{2N}$ solves

$$\psi_T'(s)=-iT[(1-f_p(s))H_0+f_p(s)H_1]\psi_T(s),\qquad \psi_T(0)=|0\rangle\otimes b.$$

For every fixed $p\in(1,2)$ there is a constant $C_p>0$, independent of $n,A,b,\kappa,T$ and the requested accuracy, such that this evolution exists for every $T>0$ and every solution satisfies

$$\bigl\||\psi_T(1)\rangle\langle\psi_T(1)| -|\widetilde x\rangle\langle\widetilde x|\bigr\|_2 \le \frac{C_p\kappa}{T}.$$

Consequently, for every $\epsilon>0$ there exists a successful positive runtime $T\le C_p\kappa/\epsilon$: the evolution exists at this runtime and every solution has the displayed error at most $\epsilon$.

For each endpoint $p\in\{1,2\}$ there are constants $C_p>0$ and $\kappa_{0,p}\ge2$, independent of all input data and accuracy, such that whenever $\kappa\ge\kappa_{0,p}$ and $\epsilon>0$, there exists a positive runtime with

$$T\le \frac{C_p\kappa\log\kappa}{\epsilon}$$

at which the evolution exists and every solution has operator norm error at most $\epsilon$.

This result establishes the runtime and accuracy guarantee for the continuous AQC($p$) linear-system solver with positive definite matrices.

Formalization Note The error compares density matrices on the full $2N$-dimensional register. The endpoint big-O clause is asymptotic in $\kappa$; the threshold avoids interpreting $\kappa\log\kappa=0$ at $\kappa=1$ as an upper bound on a positive runtime. The frozen condition-number range binder is automatic on the stated input class.

Target

Theorem 1, Section 3, Eq. (7)

Let $n\in\mathbb N$, $N=2^n$, and let $A\in\mathbb C^{N\times N}$ be Hermitian positive definite with $\|A\|_2=1$. Let $b\in\mathbb C^N$ be a unit vector. Here $\|\cdot\|_2$ denotes the operator norm for matrices and the Euclidean norm for vectors. Write

$$\kappa=\|A\|_2\|A^{-1}\|_2,\qquad x=\frac{A^{-1}b}{\|A^{-1}b\|_2},\qquad \widetilde x=|0\rangle\otimes x.$$

The condition number is the actual value determined by $A$, and satisfies $\kappa\ge1$.

Set $Q_b=I-|b\rangle\langle b|$ and

$$H_0=\begin{pmatrix}0&Q_b\\Q_b&0\end{pmatrix},\qquad H_1=\begin{pmatrix}0&AQ_b\\Q_bA&0\end{pmatrix}.$$

For $p>0$, AQC($p$) uses the schedule $f_p:[0,1]\to[0,1]$ specified by

$$f_p'(s)=c_p(1-f_p(s)+f_p(s)/\kappa)^p,\quad f_p(0)=0,\qquad c_p=\int_0^1(1-u+u/\kappa)^{-p}\,du.$$

Thus $f_p(1)=1$. The schedule is $f_p(s)=s$ when $\kappa=1$; when $\kappa>1$ and $p=1$, it is $\kappa(1-\kappa^{-s})/(\kappa-1)$; otherwise it is the closed formula in Eq. (6). For positive runtime $T$, the normalized evolution $\psi_T:[0,1]\to\mathbb C^{2N}$ solves

$$\psi_T'(s)=-iT[(1-f_p(s))H_0+f_p(s)H_1]\psi_T(s),\qquad \psi_T(0)=|0\rangle\otimes b.$$

For every fixed $p\in(1,2)$ there is a constant $C_p>0$, independent of $n,A,b,\kappa,T$ and the requested accuracy, such that this evolution exists for every $T>0$ and every solution satisfies

$$\bigl\||\psi_T(1)\rangle\langle\psi_T(1)| -|\widetilde x\rangle\langle\widetilde x|\bigr\|_2 \le \frac{C_p\kappa}{T}.$$

Consequently, for every $\epsilon>0$ there exists a successful positive runtime $T\le C_p\kappa/\epsilon$: the evolution exists at this runtime and every solution has the displayed error at most $\epsilon$.

For each endpoint $p\in\{1,2\}$ there are constants $C_p>0$ and $\kappa_{0,p}\ge2$, independent of all input data and accuracy, such that whenever $\kappa\ge\kappa_{0,p}$ and $\epsilon>0$, there exists a positive runtime with

$$T\le \frac{C_p\kappa\log\kappa}{\epsilon}$$

at which the evolution exists and every solution has operator norm error at most $\epsilon$.

This result establishes the runtime and accuracy guarantee for the continuous AQC($p$) linear-system solver with positive definite matrices.

Formalization Note The error compares density matrices on the full $2N$-dimensional register. The endpoint big-O clause is asymptotic in $\kappa$; the threshold avoids interpreting $\kappa\log\kappa=0$ at $\kappa=1$ as an upper bound on a positive runtime. The frozen condition-number range binder is automatic on the stated input class.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• Quantum linear system solver based on time-optimal adiabatic quantum computing and quantum approximate optimization algorithm, arXiv:1909.05500v3. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Quantum entanglement and the communication complexity of the inner product function (Cleve, van Dam, Nielsen, Tapp) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

This is the entanglement-assisted lower bound of Cleve, van Dam, Nielsen and Tapp, a consequence of Holevo's theorem.

Consider a two-party qubit protocol in which Alice holds an input $x\in\{0,1\}^n$ on $n$ of her qubits. All other qubits start in $|0\rangle$, except for a block of qubits in an arbitrary shared state $|\Phi\rangle$ (fixed before the input, its qubits distributed between Alice and Bob in any way). The protocol is a fixed sequence of steps, each of which is a unitary applied by one party to qubits it currently holds, or the sending of one qubit to the other party. Let $n_{AB}$ be the number of qubits Alice sends to Bob; the number $n_{BA}$ of qubits Bob sends to Alice is unrestricted. At the end Bob performs a measurement (a POVM) acting only on the qubits he holds.

1. If Bob's measurement, with outcomes in $\{0,1\}^n$, returns $x$ with probability $1$ for every input $x$, then

$$n_{AB}\ \ge\ \left\lceil \tfrac{n}{2}\right\rceil.$$

2. More generally, let $X$ be uniformly distributed on $\{0,1\}^n$ and $Y$ the outcome of any measurement of Bob. For every natural number $m$, if $I(X:Y)\ge m$ (mutual information in bits), then $n_{AB}\ge\lceil m/2\rceil$.

The bound holds regardless of the prior entanglement and of the communication from Bob to Alice. It is the information-theoretic ingredient of the paper's linear lower bounds on the communication complexity of the inner product function.

Formalization Note The protocol model is the shared TwoPartyProtocol (pure shared state; mixed states and intermediate measurements are simulated with ancillas, as the paper notes on p.13). The ceiling $\lceil k/2\rceil$ is written as natural-number division $(k+1)/2$. In clause 1 the outcome set is $\{0,1\}^n$ itself; a measurement with another outcome set followed by a decoding map is a coarse-grained measurement of this form, and clause 2 covers arbitrary outcome sets.

Target

Theorem 1

This is the entanglement-assisted lower bound of Cleve, van Dam, Nielsen and Tapp, a consequence of Holevo's theorem.

Consider a two-party qubit protocol in which Alice holds an input $x\in\{0,1\}^n$ on $n$ of her qubits. All other qubits start in $|0\rangle$, except for a block of qubits in an arbitrary shared state $|\Phi\rangle$ (fixed before the input, its qubits distributed between Alice and Bob in any way). The protocol is a fixed sequence of steps, each of which is a unitary applied by one party to qubits it currently holds, or the sending of one qubit to the other party. Let $n_{AB}$ be the number of qubits Alice sends to Bob; the number $n_{BA}$ of qubits Bob sends to Alice is unrestricted. At the end Bob performs a measurement (a POVM) acting only on the qubits he holds.

1. If Bob's measurement, with outcomes in $\{0,1\}^n$, returns $x$ with probability $1$ for every input $x$, then

$$n_{AB}\ \ge\ \left\lceil \tfrac{n}{2}\right\rceil.$$

2. More generally, let $X$ be uniformly distributed on $\{0,1\}^n$ and $Y$ the outcome of any measurement of Bob. For every natural number $m$, if $I(X:Y)\ge m$ (mutual information in bits), then $n_{AB}\ge\lceil m/2\rceil$.

The bound holds regardless of the prior entanglement and of the communication from Bob to Alice. It is the information-theoretic ingredient of the paper's linear lower bounds on the communication complexity of the inner product function.

Formalization Note The protocol model is the shared TwoPartyProtocol (pure shared state; mixed states and intermediate measurements are simulated with ancillas, as the paper notes on p.13). The ceiling $\lceil k/2\rceil$ is written as natural-number division $(k+1)/2$. In clause 1 the outcome set is $\{0,1\}^n$ itself; a measurement with another outcome set followed by a decoding map is a coarse-grained measurement of this form, and clause 2 covers arbitrary outcome sets.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• Quantum entanglement and the communication complexity of the inner product function (Cleve, van Dam, Nielsen, Tapp), arXiv:quant-ph/9708019v3. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Quantum tomography using state-preparation unitaries (van Apeldoorn, Cornelissen, Gilyén, Nannicini) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

This is the $\ell_\infty$ pure-state tomography result of van Apeldoorn, Cornelissen, Gilyén and Nannicini (arXiv:2207.08800, Proposition 22), cited in Nannicini's lecture notes as Theorem 5.17.

Let $d\ge 1$ and $n=\lceil\log_2 d\rceil$. Let $|\psi\rangle=\sum_{j=0}^{d-1}\alpha_j|j\rangle$ be a pure state, so $\alpha\in\mathbb C^d$ and $\|\alpha\|_2=1$. It is stored on $n$ qubits, with basis states $|j\rangle$ for $j\ge d$ having amplitude $0$. Let $U$ be an $n$-qubit unitary with $U|0\rangle=|\psi\rangle$. The algorithm can apply $U$ and $U^\dagger$, possibly controlled, but sees $U$ only through these applications. The gate set has all single-qubit gates, CNOT, and the indexed-SWAP gate

$$\text{indexed-SWAP}\,|i\rangle|j\rangle|x_1\rangle\cdots|x_D\rangle=|i\rangle|j\rangle\,\mathrm{SWAP}_{i,j}(|x_1\rangle\cdots|x_D\rangle).$$

There are absolute constants $C>0$ and $c\in\mathbb N$ such that the following holds for every $d\ge1$, $\varepsilon>0$ and $\delta\in(0,1)$. Write $L=\log(2+d)+\log(2+1/\varepsilon)+\log(2+1/\delta)$.

1. There is a quantum algorithm, fixed before $U$, with the following resources:

   • at most $C\,\frac{\sqrt d}{\varepsilon}\log(2+d/\delta)$ applications of $U$ and $U^\dagger$;
   • at most $C\,\frac{\sqrt d}{\varepsilon}\log(2+d/\delta)\log(2+d/\varepsilon)$ indexed-SWAP gates, each acting on a memory of $d$ qubits;
   • at most $C\,(d+\sqrt d/\varepsilon)L^c$ additional gates (single-qubit gates and CNOTs).

   For every such $\psi$ and $U$, with probability at least $1-\delta$ it outputs $\tilde\alpha\in\mathbb R^d$ with

$$\|\mathrm{Re}(\alpha)-\tilde\alpha\|_\infty\le\varepsilon.$$

2. If $\varepsilon\ge1/\sqrt d$, there is such an algorithm with at most $C\,L^c/\varepsilon^2$ applications of $U$ and $U^\dagger$ and at most $C\,L^c/\varepsilon^4$ gates in total, with the same guarantee.

The result reaches the optimal $\sqrt d/\varepsilon$ dependence for $\ell_\infty$-estimation of the amplitudes. Combined with the paper's $\ell_\infty$-to-$\ell_q$ conversion, it yields the $\ell_q$ tomography bounds (Theorem 23 of the paper; Corollary 5.18 in Nannicini).

Formalization Note Both clauses use the coherent-circuit model: one oracle circuit over the paper's gate set, started in $|0\rangle$ and measured once, with classical post-processing (medians, rescaling) in a read-out function. The paper allows adaptive classical control. The adaptive algorithm of clause 2 is simulated by deferred measurement, and the paper's convention of counting classical computation up to polylog factors absorbs the cost. The logarithms $\log(d/\delta)$ and $\log(d/\varepsilon)$ are written $\log(2+\cdot)$ so the bounds do not vanish in the degenerate corner $d=1$, $\delta\to1$. The $\tilde O$ factors are $L^c$. On index values $\ge D$, which the paper leaves unspecified, the indexed-SWAP gate acts as the identity.

Target

Proposition 22

This is the $\ell_\infty$ pure-state tomography result of van Apeldoorn, Cornelissen, Gilyén and Nannicini (arXiv:2207.08800, Proposition 22), cited in Nannicini's lecture notes as Theorem 5.17.

Let $d\ge 1$ and $n=\lceil\log_2 d\rceil$. Let $|\psi\rangle=\sum_{j=0}^{d-1}\alpha_j|j\rangle$ be a pure state, so $\alpha\in\mathbb C^d$ and $\|\alpha\|_2=1$. It is stored on $n$ qubits, with basis states $|j\rangle$ for $j\ge d$ having amplitude $0$. Let $U$ be an $n$-qubit unitary with $U|0\rangle=|\psi\rangle$. The algorithm can apply $U$ and $U^\dagger$, possibly controlled, but sees $U$ only through these applications. The gate set has all single-qubit gates, CNOT, and the indexed-SWAP gate

$$\text{indexed-SWAP}\,|i\rangle|j\rangle|x_1\rangle\cdots|x_D\rangle=|i\rangle|j\rangle\,\mathrm{SWAP}_{i,j}(|x_1\rangle\cdots|x_D\rangle).$$

There are absolute constants $C>0$ and $c\in\mathbb N$ such that the following holds for every $d\ge1$, $\varepsilon>0$ and $\delta\in(0,1)$. Write $L=\log(2+d)+\log(2+1/\varepsilon)+\log(2+1/\delta)$.

1. There is a quantum algorithm, fixed before $U$, with the following resources:

   • at most $C\,\frac{\sqrt d}{\varepsilon}\log(2+d/\delta)$ applications of $U$ and $U^\dagger$;
   • at most $C\,\frac{\sqrt d}{\varepsilon}\log(2+d/\delta)\log(2+d/\varepsilon)$ indexed-SWAP gates, each acting on a memory of $d$ qubits;
   • at most $C\,(d+\sqrt d/\varepsilon)L^c$ additional gates (single-qubit gates and CNOTs).

   For every such $\psi$ and $U$, with probability at least $1-\delta$ it outputs $\tilde\alpha\in\mathbb R^d$ with

$$\|\mathrm{Re}(\alpha)-\tilde\alpha\|_\infty\le\varepsilon.$$

2. If $\varepsilon\ge1/\sqrt d$, there is such an algorithm with at most $C\,L^c/\varepsilon^2$ applications of $U$ and $U^\dagger$ and at most $C\,L^c/\varepsilon^4$ gates in total, with the same guarantee.

The result reaches the optimal $\sqrt d/\varepsilon$ dependence for $\ell_\infty$-estimation of the amplitudes. Combined with the paper's $\ell_\infty$-to-$\ell_q$ conversion, it yields the $\ell_q$ tomography bounds (Theorem 23 of the paper; Corollary 5.18 in Nannicini).

Formalization Note Both clauses use the coherent-circuit model: one oracle circuit over the paper's gate set, started in $|0\rangle$ and measured once, with classical post-processing (medians, rescaling) in a read-out function. The paper allows adaptive classical control. The adaptive algorithm of clause 2 is simulated by deferred measurement, and the paper's convention of counting classical computation up to polylog factors absorbs the cost. The logarithms $\log(d/\delta)$ and $\log(d/\varepsilon)$ are written $\log(2+\cdot)$ so the bounds do not vanish in the degenerate corner $d=1$, $\delta\to1$. The $\tilde O$ factors are $L^c$. On index values $\ge D$, which the paper leaves unspecified, the indexed-SWAP gate acts as the identity.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• Quantum tomography using state-preparation unitaries (van Apeldoorn, Cornelissen, Gilyén, Nannicini), arXiv:2207.08800v1. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Quantum singular value transformation and beyond: exponential improvements for quantum matrix arithmetics (Gilyén, Su, Low, Wiebe) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

This is the polynomial eigenvalue transformation theorem of Gilyén, Su, Low and Wiebe, which removes the parity constraint of quantum singular value transformation at the price of a factor $1/2$.

For an $s$-qubit operator $A$, real numbers $\alpha>0$, $\varepsilon\ge 0$ and $a\in\mathbb N$, an $(a+s)$-qubit unitary $U$ is an $(\alpha,a,\varepsilon)$-block-encoding of $A$ if

$$\big\|A-\alpha\,(\langle 0|^{\otimes a}\otimes I)\,U\,(|0\rangle^{\otimes a}\otimes I)\big\|\le\varepsilon ,$$

where $\|\cdot\|$ is the operator norm and the ancilla register comes first.

There is an absolute constant $C>0$ such that the following holds. Let $s,a,d\in\mathbb N$, let $\delta\ge 0$, and let $P\in\mathbb R[x]$ be a polynomial of degree at most $d$ with $|P(x)|\le \tfrac12$ for all $x\in[-1,1]$. Then there exist $w\in\mathbb N$ and a quantum circuit $\tilde U$ on $(a+2)+s+w$ qubits, built from one- and two-qubit gates and calls to a black box $U$ on $a+s$ qubits, with

1. at most $d$ uncontrolled applications of $U$ or $U^\dagger$,
2. at most one controlled application of the black box,
3. at most $C(a+1)\max(d,1)$ other gates,

such that for every $\alpha>0$, $\varepsilon\ge 0$, every Hermitian $s$-qubit matrix $A$ with $\|A\|\le\alpha$ and every $(\alpha,a,\varepsilon)$-block-encoding $U$ of $A$, the circuit $\tilde U$ (with the last $w$ qubits as clean ancillas, started and returned exactly in $|0\rangle$) implements a unitary $V$ on $(a+2)+s$ qubits that is a

$$\Big(1,\;a+2,\;4d\sqrt{\varepsilon/\alpha}+\delta\Big)\text{-block-encoding of } P(A/\alpha).$$

This theorem is the workhorse for implementing smooth functions of Hermitian matrices (Hamiltonian simulation, matrix inversion, Gibbs sampling) through block-encodings.

Formalization Note The circuit is chosen before $\alpha,\varepsilon,A,U$, so it depends only on $s,a,d,P,\delta$. The source's $O((a+1)d)$ is encoded with $\max(d,1)$ since a constant polynomial still needs a few gates. The source's last sentence (classical computability of the circuit description in time $\mathrm{poly}(d,\log(1/\delta))$) is not formalized, because the source fixes no bit model for the real coefficients of $P$. The controlled query may be controlled-$U$ or controlled-$U^\dagger$. The hypothesis $\|A\|\le\alpha$ corrects the printed statement: the source's proof uses Lemma 22, which needs $\|A/\alpha\|\le 1$, and without it the printed statement fails (e.g. $A=[2]$, $U=[1]$, $\alpha=\varepsilon=1$, $P=T_8/2$, $d=8$).

Correction to the printed source.

Printed: Suppose that U is an (α, a, ε)-encoding of a Hermitian matrix A (no condition ‖A‖ ≤ α; Definition 43 only forces ‖A‖ ≤ α + ε).

Corrected: Added the hypothesis specNorm A ≤ α, i.e. ‖A/α‖ ≤ 1.

Reason: The proof (p.49) applies Lemma 22 (p.23), which requires both matrices to have operator norm at most 1. Without it the statement is false: s = a = 0, α = ε = 1, A = [2], U = [1] is a (1, 0, 1)-encoding of A; with P = T_8/2, d = 8, δ = 0 one gets P(A/α) = T_8(2)/2 ≈ 9408, while every block of a unitary has norm ≤ 1 and the claimed error is 32.

Target

Theorem 56

This is the polynomial eigenvalue transformation theorem of Gilyén, Su, Low and Wiebe, which removes the parity constraint of quantum singular value transformation at the price of a factor $1/2$.

For an $s$-qubit operator $A$, real numbers $\alpha>0$, $\varepsilon\ge 0$ and $a\in\mathbb N$, an $(a+s)$-qubit unitary $U$ is an $(\alpha,a,\varepsilon)$-block-encoding of $A$ if

$$\big\|A-\alpha\,(\langle 0|^{\otimes a}\otimes I)\,U\,(|0\rangle^{\otimes a}\otimes I)\big\|\le\varepsilon ,$$

where $\|\cdot\|$ is the operator norm and the ancilla register comes first.

There is an absolute constant $C>0$ such that the following holds. Let $s,a,d\in\mathbb N$, let $\delta\ge 0$, and let $P\in\mathbb R[x]$ be a polynomial of degree at most $d$ with $|P(x)|\le \tfrac12$ for all $x\in[-1,1]$. Then there exist $w\in\mathbb N$ and a quantum circuit $\tilde U$ on $(a+2)+s+w$ qubits, built from one- and two-qubit gates and calls to a black box $U$ on $a+s$ qubits, with

1. at most $d$ uncontrolled applications of $U$ or $U^\dagger$,
2. at most one controlled application of the black box,
3. at most $C(a+1)\max(d,1)$ other gates,

such that for every $\alpha>0$, $\varepsilon\ge 0$, every Hermitian $s$-qubit matrix $A$ with $\|A\|\le\alpha$ and every $(\alpha,a,\varepsilon)$-block-encoding $U$ of $A$, the circuit $\tilde U$ (with the last $w$ qubits as clean ancillas, started and returned exactly in $|0\rangle$) implements a unitary $V$ on $(a+2)+s$ qubits that is a

$$\Big(1,\;a+2,\;4d\sqrt{\varepsilon/\alpha}+\delta\Big)\text{-block-encoding of } P(A/\alpha).$$

This theorem is the workhorse for implementing smooth functions of Hermitian matrices (Hamiltonian simulation, matrix inversion, Gibbs sampling) through block-encodings.

Formalization Note The circuit is chosen before $\alpha,\varepsilon,A,U$, so it depends only on $s,a,d,P,\delta$. The source's $O((a+1)d)$ is encoded with $\max(d,1)$ since a constant polynomial still needs a few gates. The source's last sentence (classical computability of the circuit description in time $\mathrm{poly}(d,\log(1/\delta))$) is not formalized, because the source fixes no bit model for the real coefficients of $P$. The controlled query may be controlled-$U$ or controlled-$U^\dagger$. The hypothesis $\|A\|\le\alpha$ corrects the printed statement: the source's proof uses Lemma 22, which needs $\|A/\alpha\|\le 1$, and without it the printed statement fails (e.g. $A=[2]$, $U=[1]$, $\alpha=\varepsilon=1$, $P=T_8/2$, $d=8$).

Correction to the printed source.

Printed: Suppose that U is an (α, a, ε)-encoding of a Hermitian matrix A (no condition ‖A‖ ≤ α; Definition 43 only forces ‖A‖ ≤ α + ε).

Corrected: Added the hypothesis specNorm A ≤ α, i.e. ‖A/α‖ ≤ 1.

Reason: The proof (p.49) applies Lemma 22 (p.23), which requires both matrices to have operator norm at most 1. Without it the statement is false: s = a = 0, α = ε = 1, A = [2], U = [1] is a (1, 0, 1)-encoding of A; with P = T_8/2, d = 8, δ = 0 one gets P(A/α) = T_8(2)/2 ≈ 9408, while every block of a unitary has norm ≤ 1 and the claimed error is 32.

Corollary 62

This is the robust block-Hamiltonian simulation result of Gilyén, Su, Low and Wiebe (Corollary 62 of arXiv:1806.01838v1, Corollary 63 in the published version).

Block-encodings are as in Definition 43: an $(a+s)$-qubit unitary $U$ is an $(\alpha,a,\eta)$-block-encoding of an $s$-qubit operator $H$ if $\|H-\alpha(\langle0|^{\otimes a}\otimes I)U(|0\rangle^{\otimes a}\otimes I)\|\le\eta$ in operator norm.

There is an absolute constant $C>0$ such that the following holds. Let $s,a\in\mathbb N$, $t\in\mathbb R$, $\varepsilon\in(0,1)$ and $\alpha>0$. Then there exist $w\le C$ and a circuit on $(a+2)+s+w$ qubits, made of two-qubit gates and calls to a black box $U$ on $a+s$ qubits, using

1. at most $6\alpha|t|+9\ln(12/\varepsilon)$ uncontrolled applications of $U$ or $U^\dagger$,
2. at most $3$ applications of controlled-$U$ or its inverse,
3. at most $C(a+1)\big(\alpha|t|+\ln(2/\varepsilon)\big)$ two-qubit gates,

such that for every Hermitian $s$-qubit matrix $H$ and every $(\alpha,a,\varepsilon/|2t|)$-block-encoding $U$ of $H$, the circuit (with its last $w$ qubits as clean ancillas) implements a unitary $V$ that is a

$$(1,\;a+2,\;\varepsilon)\text{-block-encoding of } e^{itH}.$$

This gives Hamiltonian simulation with additive query complexity in $\alpha|t|$ and $\log(1/\varepsilon)$, robust to an imprecise block-encoding of the Hamiltonian.

Formalization Note The circuit may depend on $s,a,t,\varepsilon,\alpha$ but not on $H$ or $U$. The source's gate bound $O(a(\cdots))$ is encoded as $O((a+1)(\cdots))$, since the two new ancillas need gates even when $a=0$. At $t=0$ the source's $\varepsilon/|2t|$ is undefined; in Lean $\varepsilon/0=0$, so there the hypothesis is an exact block-encoding.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• Quantum singular value transformation and beyond: exponential improvements for quantum matrix arithmetics (Gilyén, Su, Low, Wiebe), arXiv:1806.01838v1. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Optimizing quantum optimization algorithms via faster quantum gradient computation (Gilyén, Arunachalam, Wiebe) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

This is the conversion of a probability oracle into an approximate phase oracle (Gilyén–Arunachalam–Wiebe, Theorem 14).

Let $X$ be a finite set and $\mathcal H$ the Hilbert space with orthonormal basis $\{|x\rangle : x\in X\}$. A probability oracle for $p : X\to[0,1]$ with an $n$-qubit auxiliary register is a unitary $U_p$ on $\mathcal H\otimes\mathbb C^{2^n}$ with

$$U_p|x\rangle|0\rangle^{\otimes n} = |x\rangle\otimes\Big(\sqrt{p(x)}\,|\psi_{\mathrm{good}}(x)\rangle|1\rangle + \sqrt{1-p(x)}\,|\psi_{\mathrm{bad}}(x)\rangle|0\rangle\Big)$$

for some normalized states $\psi_{\mathrm{good}}(x),\psi_{\mathrm{bad}}(x)$ (the flag is the last qubit). A phase oracle for $p$ on an auxiliary register is a unitary $O_p$ with $O_p|x\rangle|0\rangle = e^{ip(x)}|x\rangle|0\rangle$ for all $x\in X$.

There is an absolute constant $C>0$ such that for every $\varepsilon\in(0,1/3)$, every finite $X$ and every $n\ge1$ there are a number $a\le C\log\log(1/\varepsilon)$ of extra qubits and a quantum circuit $O$ on $\mathcal H\otimes\mathbb C^{2^{n+a}}$, built from input-independent unitaries and at most $C\log(1/\varepsilon)$ (uncontrolled) applications of $U_p$ and $U_p^\dagger$, such that for every $p$, every probability oracle $U_p$ for $p$, every phase oracle $O_p$ for $p$ on $n+a$ auxiliary qubits, and every unit vector $|\psi\rangle\in\mathcal H$,

$$\big\| O|\psi\rangle|0\rangle^{\otimes(n+a)} - O_p|\psi\rangle|0\rangle^{\otimes(n+a)}\big\| \le \varepsilon .$$

This shows that the probability oracles arising from parametrized quantum circuits can be used wherever a phase oracle is needed, at only logarithmic overhead in the precision.

Formalization Note The circuit is fixed before $p$ and $U_p$; the source's $n$-qubit auxiliary register is written $n=m+1$. The source's "for all $|\psi\rangle\in\mathcal H$" is read for unit vectors, as in the proof.

Target

Theorem 14

This is the conversion of a probability oracle into an approximate phase oracle (Gilyén–Arunachalam–Wiebe, Theorem 14).

Let $X$ be a finite set and $\mathcal H$ the Hilbert space with orthonormal basis $\{|x\rangle : x\in X\}$. A probability oracle for $p : X\to[0,1]$ with an $n$-qubit auxiliary register is a unitary $U_p$ on $\mathcal H\otimes\mathbb C^{2^n}$ with

$$U_p|x\rangle|0\rangle^{\otimes n} = |x\rangle\otimes\Big(\sqrt{p(x)}\,|\psi_{\mathrm{good}}(x)\rangle|1\rangle + \sqrt{1-p(x)}\,|\psi_{\mathrm{bad}}(x)\rangle|0\rangle\Big)$$

for some normalized states $\psi_{\mathrm{good}}(x),\psi_{\mathrm{bad}}(x)$ (the flag is the last qubit). A phase oracle for $p$ on an auxiliary register is a unitary $O_p$ with $O_p|x\rangle|0\rangle = e^{ip(x)}|x\rangle|0\rangle$ for all $x\in X$.

There is an absolute constant $C>0$ such that for every $\varepsilon\in(0,1/3)$, every finite $X$ and every $n\ge1$ there are a number $a\le C\log\log(1/\varepsilon)$ of extra qubits and a quantum circuit $O$ on $\mathcal H\otimes\mathbb C^{2^{n+a}}$, built from input-independent unitaries and at most $C\log(1/\varepsilon)$ (uncontrolled) applications of $U_p$ and $U_p^\dagger$, such that for every $p$, every probability oracle $U_p$ for $p$, every phase oracle $O_p$ for $p$ on $n+a$ auxiliary qubits, and every unit vector $|\psi\rangle\in\mathcal H$,

$$\big\| O|\psi\rangle|0\rangle^{\otimes(n+a)} - O_p|\psi\rangle|0\rangle^{\otimes(n+a)}\big\| \le \varepsilon .$$

This shows that the probability oracles arising from parametrized quantum circuits can be used wherever a phase oracle is needed, at only logarithmic overhead in the precision.

Formalization Note The circuit is fixed before $p$ and $U_p$; the source's $n$-qubit auxiliary register is written $n=m+1$. The source's "for all $|\psi\rangle\in\mathcal H$" is read for unit vectors, as in the proof.

Lemma 16

This is the conversion of a phase oracle into a probability oracle (Gilyén–Arunachalam–Wiebe, Lemma 16).

Let $X$ be a finite set, $\mathcal H$ the Hilbert space with orthonormal basis $\{|x\rangle : x\in X\}$, and let $O_p$ be a phase oracle for $p : X\to\mathbb R$ on $\mathcal H\otimes\mathbb C^{2^w}$, i.e. a unitary with $O_p|x\rangle|0\rangle^{\otimes w}=e^{ip(x)}|x\rangle|0\rangle^{\otimes w}$ for all $x\in X$.

There is an absolute constant $C>0$ such that for all $\varepsilon,\delta\in(0,1/2)$, every finite $X$ and every $w$ there are $k$ and a quantum circuit $U_p$ on $\mathcal H\otimes\mathbb C^{2^{k+1}}$, built from input-independent unitaries and at most $C\log(1/\varepsilon)/\delta$ invocations of $O_p$, $O_p^\dagger$ or their controlled versions, such that for every $p : X\to[\delta,1-\delta]$, every phase oracle $O_p$ for $p$ and every $x\in X$ there are $p'(x)\in[0,1]$ and a unit vector $|\Phi^\perp\rangle$ with

$$U_p|x\rangle|0\rangle^{\otimes k}|0\rangle = |x\rangle\otimes\Big(\sqrt{p'(x)}\,|0\rangle^{\otimes k}|0\rangle + \sqrt{1-p'(x)}\,|\Phi^\perp\rangle|1\rangle\Big), \qquad \big|\sqrt{p'(x)}-\sqrt{p(x)}\big|\le\varepsilon .$$

Together with Theorem 14 this shows that phase and probability oracles are interconvertible with logarithmic overhead in the precision when the probabilities are bounded away from $0$ and $1$.

Formalization Note The register $|0\rangle^{\otimes k}$ consists of the $w$ auxiliary qubits of $O_p$ and $a$ further qubits ($k=w+a$); the last qubit is the flag. The source's "for every $x\in\mathbb R^n$" is read as $x\in X$, the domain of $p$.

Theorem 23

This is the higher-order gradient algorithm of Gilyén–Arunachalam–Wiebe (Theorem 23).

Let $f : [-R,R]^d\to\mathbb R$ be accessed through fractional phase queries: for a finite set of query points $X\subseteq[-R,R]^d$ chosen by the algorithm, and every $r\in[-1,1]$, a unitary $O_f^r$ with $O_f^r|x\rangle|0\rangle=e^{irf(x)}|x\rangle|0\rangle$ for $x\in X$; each application of some $O_f^r$ counts as one query. For $x\ne0$ write $\partial_r^{k}f(x)=\frac{d^k}{d\tau^k}f(x+\tau r)\big|_{\tau=0}$ (taken within the cube) with $r=x/\|x\|$, $\|\cdot\|$ the Euclidean norm.

There is an absolute constant $C>0$ such that for all $d$, $m\in\mathbb Z_+$, $R>0$, $B\ge0$, $\varepsilon>0$, $\rho\in(0,1)$ and every a-priori gradient bound $M>0$ there is a quantum algorithm (query points, start state, circuit and classical post-processing of the final measurement, all independent of $f$) using at most

$$C\left(\max\left(\frac{\sqrt d}{\varepsilon}\Big(\frac{B\sqrt d}{\varepsilon}\Big)^{1/(2m)},\ \frac{m}{\varepsilon R}\right)\log(2m)+m\right)\big(1+\log(d/\rho)\big)$$

phase queries with the following property: for every $f$ that is $(2m+1)$-times differentiable on $[-R,R]^d$, satisfies $|\partial_r^{2m+1}f(x)|\le B$ for all $x\in[-R,R]^d\setminus\{0\}$, $r=x/\|x\|$, and $\|\nabla f(0)\|_\infty\le M$, and for every fractional phase oracle for $f$, the output $g$ satisfies

$$\Pr\big[\|g-\nabla f(0)\|_\infty\le\varepsilon\big]\ge1-\rho .$$

The bound shows that higher-degree central difference formulas reduce the query cost of Jordan's gradient algorithm, exponentially in $d$ for low-degree polynomials.

Formalization Note The known gradient bound $M$ is the hypothesis of Theorem 21 that the proof uses (the query count is independent of $M$). The factor $\log(d/\rho)$ is written $1+\log(d/\rho)$, the proof's repetition count $\lceil C\log(d/\rho)\rceil\ge1$. Queries are uncontrolled and non-adjoint, as the proof applies them.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• Optimizing quantum optimization algorithms via faster quantum gradient computation (Gilyén, Arunachalam, Wiebe), arXiv:1711.00465v3. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Quantum algorithms for escaping from saddle points establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Fix positive smoothness bounds $\ell,\rho$, confidence $0<\delta<1$, and a nonnegative starting gap $\Delta$. Let $f:\mathbb R^n\to\mathbb R$ be twice differentiable, with globally $\ell$-Lipschitz gradient in Euclidean norm and globally $\rho$-Lipschitz Hessian in operator norm. Assume $f$ attains its finite global minimum $f^*$, and let the public initial point $x_0$ satisfy $f(x_0)-f^*=\Delta$. For $0<\varepsilon\le\ell^2/\rho$, set $g=\Delta(\log n)^2\varepsilon^{-7/4}$.

There are $C>0$, a nonnegative integer $a$, and thresholds $n_0\ge2$, $g_0\ge1$, depending only on the fixed public parameters. In the regime $n\ge n_0$ and $g\ge g_0$, a quantum evaluation-query program can be chosen using $n,\varepsilon,x_0$ and those public parameters before $f$ and its oracle. For every coherent value-output unitary satisfying $U_f|x,0,0\rangle=|x,f(x),0\rangle$, its joint output and evaluation-call law obeys

$$\Pr\!\left[\|\nabla f(x)\|_2\le\varepsilon,\quad\lambda_{\min}(\nabla^2f(x))\ge-\sqrt{\rho\varepsilon},\quad Q\le Cg\max\{1,\log g\}^{a}\right]\ge1-\delta.$$

Here $Q$ counts forward and inverse evaluation-oracle applications. There are no free gradient, Hessian or simulation queries. If $\Delta=0$, the program returns $x_0$ without queries, including in dimension one. Positive-gap small dimensions and scales are outside this asymptotic statement.

This is the authors' ideal-oracle existence claim, with the displayed $\log^2 n$ and $\varepsilon^{-7/4}$ dependence and their broad convention $\widetilde O(g)=O(g\,\mathrm{poly}(\log g))$. The formal counterpart combines Theorem 4, Eq. (66), pages 18–19, Remark 2 on page 20, and the accelerated evaluation-only extension asserted after Theorem 5 and in Remark 3 on page 24. It does not assert an exact local minimum or correctness of a specific finite-accuracy implementation.

Formalization Note The frozen ideal real-label register and adaptive evaluation-program semantics provide the joint law. The Hessian lower bound is its equivalent quadratic-form inequality on every real vector. Measurability is concluded for the chosen program, and the gap is computed from an attained minimum. The action of the oracle on dirty value registers is left unrestricted.

Target

Theorem 1 (Main result, informal)

Fix positive smoothness bounds $\ell,\rho$, confidence $0<\delta<1$, and a nonnegative starting gap $\Delta$. Let $f:\mathbb R^n\to\mathbb R$ be twice differentiable, with globally $\ell$-Lipschitz gradient in Euclidean norm and globally $\rho$-Lipschitz Hessian in operator norm. Assume $f$ attains its finite global minimum $f^*$, and let the public initial point $x_0$ satisfy $f(x_0)-f^*=\Delta$. For $0<\varepsilon\le\ell^2/\rho$, set $g=\Delta(\log n)^2\varepsilon^{-7/4}$.

There are $C>0$, a nonnegative integer $a$, and thresholds $n_0\ge2$, $g_0\ge1$, depending only on the fixed public parameters. In the regime $n\ge n_0$ and $g\ge g_0$, a quantum evaluation-query program can be chosen using $n,\varepsilon,x_0$ and those public parameters before $f$ and its oracle. For every coherent value-output unitary satisfying $U_f|x,0,0\rangle=|x,f(x),0\rangle$, its joint output and evaluation-call law obeys

$$\Pr\!\left[\|\nabla f(x)\|_2\le\varepsilon,\quad\lambda_{\min}(\nabla^2f(x))\ge-\sqrt{\rho\varepsilon},\quad Q\le Cg\max\{1,\log g\}^{a}\right]\ge1-\delta.$$

Here $Q$ counts forward and inverse evaluation-oracle applications. There are no free gradient, Hessian or simulation queries. If $\Delta=0$, the program returns $x_0$ without queries, including in dimension one. Positive-gap small dimensions and scales are outside this asymptotic statement.

This is the authors' ideal-oracle existence claim, with the displayed $\log^2 n$ and $\varepsilon^{-7/4}$ dependence and their broad convention $\widetilde O(g)=O(g\,\mathrm{poly}(\log g))$. The formal counterpart combines Theorem 4, Eq. (66), pages 18–19, Remark 2 on page 20, and the accelerated evaluation-only extension asserted after Theorem 5 and in Remark 3 on page 24. It does not assert an exact local minimum or correctness of a specific finite-accuracy implementation.

Formalization Note The frozen ideal real-label register and adaptive evaluation-program semantics provide the joint law. The Hessian lower bound is its equivalent quadratic-form inequality on every real vector. Measurability is concluded for the chosen program, and the gap is computed from an attained minimum. The action of the oracle on dirty value registers is left unrestricted.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• Quantum algorithms for escaping from saddle points, arXiv:2007.10253v3. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.