All missions

Motivation

Multivariate Decoded Quantum Interferometry for Weighted Optimization establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $p$ be prime and $1\le r<p$. Let $B\in\mathbb F_p^{m\times n}$ with $m>0$, and let $L_i\subseteq\mathbb F_p$ have cardinality $r$. Define $f_i(y)=1$ on $L_i$ and $f_i(y)=-1$ otherwise. Partition $[m]$ into nonempty blocks $S_1,\ldots,S_N$, write $m_t=|S_t|$, and assign positive weights $g_t$. Put $F_t(x)=\sum_{i\in S_t}f_i(b_i\cdot x)$ and $F_g(x)=\sum_t g_tF_t(x)$, where $b_i$ is row $i$ of $B$ and $x\in\mathbb F_p^n$.

Fix an exact degree ratio $\mu=\ell/m\in(0,1/2)$, with integer $\ell$, and assume $2\ell+1<d^\perp$, where $d^\perp$ is the minimum nonzero Hamming weight in $\ker B^\top$ (infinite when this kernel is zero). Let $E_{\mathrm{opt}}$ be the supremum of $\sum_x|\psi_P(x)|^2F_g(x)$ over complex multivariate polynomials of total degree at most $\ell$ such that $\psi_P(x)=P(F_1(x),\ldots,F_N(x))$ has unit norm. This supremum is attained by an admissible polynomial.

Write $\bar f=2r/p-1$, $\sigma=2\sqrt{r(p-r)}/p$, $\kappa=(p-2r)/\sqrt{r(p-r)}$, and define

$$\Gamma_{g,m,\kappa}(\mu)=\sup_{\substack{0\le\alpha_t\le1\ (1\le t\le N)\\\sum_t(m_t/m)\alpha_t\le\mu}}\sum_t\frac{m_t}{m}g_t\left(\kappa\alpha_t+2\sqrt{\alpha_t(1-\alpha_t)}\right).$$

For each fixed $\kappa$, there are $C_\kappa>0$ and an integer $m_0$, chosen before all other instance data and $\mu$, such that every admissible instance with $m\ge m_0$ satisfies

$$\frac{E_{\mathrm{opt}}}{m}=\bar f\sum_t\frac{g_tm_t}{m}+\sigma\Gamma_{g,m,\kappa}(\mu)+R, \qquad |R|\le\frac{C_\kappa}{m}\sum_tg_tm_t^{3/4}.$$

Along any admissible family with fixed $\kappa,\mu,N$, unbounded $m$, and eventually bounded $\max_tg_t$, the residual $R$ tends to zero. No convergence of block proportions is required.

This characterizes the asymptotically optimal signed weighted objective among multivariate DQI states. It does not impose decoder access or a preparation complexity bound.

Formalization Note The range $1\le r<p$ is explicitly recalled by Appendix A (PDF p.30) and is carried as a standing assumption although omitted from the printed theorem sentence. Exact integer pairs $(\ell,m)$ are used; no rounding convention is added.

Target

Theorem 2 (Asymptotically Optimal Expectation Value), equations (9)–(10)

Let $p$ be prime and $1\le r<p$. Let $B\in\mathbb F_p^{m\times n}$ with $m>0$, and let $L_i\subseteq\mathbb F_p$ have cardinality $r$. Define $f_i(y)=1$ on $L_i$ and $f_i(y)=-1$ otherwise. Partition $[m]$ into nonempty blocks $S_1,\ldots,S_N$, write $m_t=|S_t|$, and assign positive weights $g_t$. Put $F_t(x)=\sum_{i\in S_t}f_i(b_i\cdot x)$ and $F_g(x)=\sum_t g_tF_t(x)$, where $b_i$ is row $i$ of $B$ and $x\in\mathbb F_p^n$.

Fix an exact degree ratio $\mu=\ell/m\in(0,1/2)$, with integer $\ell$, and assume $2\ell+1<d^\perp$, where $d^\perp$ is the minimum nonzero Hamming weight in $\ker B^\top$ (infinite when this kernel is zero). Let $E_{\mathrm{opt}}$ be the supremum of $\sum_x|\psi_P(x)|^2F_g(x)$ over complex multivariate polynomials of total degree at most $\ell$ such that $\psi_P(x)=P(F_1(x),\ldots,F_N(x))$ has unit norm. This supremum is attained by an admissible polynomial.

Write $\bar f=2r/p-1$, $\sigma=2\sqrt{r(p-r)}/p$, $\kappa=(p-2r)/\sqrt{r(p-r)}$, and define

$$\Gamma_{g,m,\kappa}(\mu)=\sup_{\substack{0\le\alpha_t\le1\ (1\le t\le N)\\\sum_t(m_t/m)\alpha_t\le\mu}}\sum_t\frac{m_t}{m}g_t\left(\kappa\alpha_t+2\sqrt{\alpha_t(1-\alpha_t)}\right).$$

For each fixed $\kappa$, there are $C_\kappa>0$ and an integer $m_0$, chosen before all other instance data and $\mu$, such that every admissible instance with $m\ge m_0$ satisfies

$$\frac{E_{\mathrm{opt}}}{m}=\bar f\sum_t\frac{g_tm_t}{m}+\sigma\Gamma_{g,m,\kappa}(\mu)+R, \qquad |R|\le\frac{C_\kappa}{m}\sum_tg_tm_t^{3/4}.$$

Along any admissible family with fixed $\kappa,\mu,N$, unbounded $m$, and eventually bounded $\max_tg_t$, the residual $R$ tends to zero. No convergence of block proportions is required.

This characterizes the asymptotically optimal signed weighted objective among multivariate DQI states. It does not impose decoder access or a preparation complexity bound.

Formalization Note The range $1\le r<p$ is explicitly recalled by Appendix A (PDF p.30) and is carried as a standing assumption although omitted from the printed theorem sentence. Exact integer pairs $(\ell,m)$ are used; no rounding convention is added.

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

• Multivariate Decoded Quantum Interferometry for Weighted Optimization, arXiv:2605.10666v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Randomized and quantum approximate matrix multiplication establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Fix a classical exact-arithmetic matrix multiplication implementation with achievable exponent $\omega\ge 2$. Let $n\ge1$, $K\ge1$, and let $A_1,\ldots,A_K\in\mathbb R^{n\times n}$ be arbitrary matrices. Write $F=\prod_{j=1}^K\|A_j\|_F$, where $\|A\|_F=(\sum_{i,j}A_{ij}^2)^{1/2}$. Given absolute accuracy $\varepsilon>0$ and failure probability $0<\delta<1$, there are fixed input-taking classical and quantum circuit families, with classical preprocessing time $\widetilde O(Kn^2)$, which return classical matrices $C_{\rm cl}$ and $C_{\rm q}$ satisfying

$$\Pr\!\left[\|C_{\rm cl}-A_1\cdots A_K\|_F\le\varepsilon\right]\ge1-\delta, \qquad \Pr\!\left[\max_{i,j}|(C_{\rm q}-A_1\cdots A_K)_{ij}|\le\varepsilon\right]\ge1-\delta.$$

Apart from input/output and preprocessing overhead, their running times are respectively

$$\widetilde O\!\left(n^2\left(\frac{3^K F^2}{\varepsilon^2}\right)^{\omega-2}\right), \qquad \widetilde O\!\left(n^2\frac{3^K F}{\varepsilon}\right).$$

The soft factors include the confidence logarithms and are uniform over dimensions, factors, matrix entries, accuracy, and confidence; constants may depend on the chosen multiplication implementation. Real numbers are represented exactly, and fixed-position retrieval and arithmetic are charged in both models. The quantum output is an ordinary classical matrix. No efficiently addressable classical or quantum memory is required.

The case $K=1$ returns the input matrix exactly. For $K>1$ and $F\le\varepsilon$, both families return zero; this includes every zero factor. These branches still pay for the input and classical output. The displayed online scales are clamped below by $n^2$, and the formal total bound includes $Kn^2$ explicitly. This result compares approximate products in two different error norms under the same circuit access model.

Formalization Note Lean uses $k=K-1$ interfaces and computes $F^2$ during charged classical preprocessing. Rounded, confidence-dependent sample budgets select members of circuit families fixed before the matrices. The classical law is computed from one fixed list of exact-real arithmetic, random-coin and comparison instructions, with each comparison writing a 0/1 register value and every instruction charged; quantum probabilities and work are computed from the frozen exact-real mean-estimation circuit language. No approximation guarantee or arbitrary runtime number is assumed as a field of an algorithm.

Target

Theorem 1.3 (continues on p.6); Theorems 4.10–4.11, pp.21–23

Fix a classical exact-arithmetic matrix multiplication implementation with achievable exponent $\omega\ge 2$. Let $n\ge1$, $K\ge1$, and let $A_1,\ldots,A_K\in\mathbb R^{n\times n}$ be arbitrary matrices. Write $F=\prod_{j=1}^K\|A_j\|_F$, where $\|A\|_F=(\sum_{i,j}A_{ij}^2)^{1/2}$. Given absolute accuracy $\varepsilon>0$ and failure probability $0<\delta<1$, there are fixed input-taking classical and quantum circuit families, with classical preprocessing time $\widetilde O(Kn^2)$, which return classical matrices $C_{\rm cl}$ and $C_{\rm q}$ satisfying

$$\Pr\!\left[\|C_{\rm cl}-A_1\cdots A_K\|_F\le\varepsilon\right]\ge1-\delta, \qquad \Pr\!\left[\max_{i,j}|(C_{\rm q}-A_1\cdots A_K)_{ij}|\le\varepsilon\right]\ge1-\delta.$$

Apart from input/output and preprocessing overhead, their running times are respectively

$$\widetilde O\!\left(n^2\left(\frac{3^K F^2}{\varepsilon^2}\right)^{\omega-2}\right), \qquad \widetilde O\!\left(n^2\frac{3^K F}{\varepsilon}\right).$$

The soft factors include the confidence logarithms and are uniform over dimensions, factors, matrix entries, accuracy, and confidence; constants may depend on the chosen multiplication implementation. Real numbers are represented exactly, and fixed-position retrieval and arithmetic are charged in both models. The quantum output is an ordinary classical matrix. No efficiently addressable classical or quantum memory is required.

The case $K=1$ returns the input matrix exactly. For $K>1$ and $F\le\varepsilon$, both families return zero; this includes every zero factor. These branches still pay for the input and classical output. The displayed online scales are clamped below by $n^2$, and the formal total bound includes $Kn^2$ explicitly. This result compares approximate products in two different error norms under the same circuit access model.

Formalization Note Lean uses $k=K-1$ interfaces and computes $F^2$ during charged classical preprocessing. Rounded, confidence-dependent sample budgets select members of circuit families fixed before the matrices. The classical law is computed from one fixed list of exact-real arithmetic, random-coin and comparison instructions, with each comparison writing a 0/1 register value and every instruction charged; quantum probabilities and work are computed from the frozen exact-real mean-estimation circuit language. No approximation guarantee or arbitrary runtime number is assumed as a field of an algorithm.

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

• Randomized and quantum approximate matrix multiplication, arXiv:2510.08509v1. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Fast Convex Optimization with Quantum Gradient Methods establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $X\subseteq\mathbb R^d$ be closed, bounded and convex, let $x_1\in X$, and let $f:\mathbb R^d\to\mathbb R$ be convex and ambient $G$-Lipschitz in the stated norm. Assume an attained constrained optimum $x^\star$, and $0<\varepsilon<1$. Both branches use coherent binary evaluations on sufficiently fine finite translated hypergrids: every grid index is preserved, the encoded value has error strictly below $\theta$, and calls to the unitary and its adjoint are counted. The algorithm construction is fixed before the objective, optimum and oracle values; only geometry and supplied numerical scale bounds enter its construction.

1. Euclidean branch. Set $R=\|x_1-x^\star\|_2$, $K=\operatorname{diam}_2(X)$, $T=\max\{1,\lceil(3GR/\varepsilon)^2\rceil\}$, $r_1=\varepsilon/(6G\sqrt d)$, $\rho=1/(3T)$, and $\eta=R/(G\sqrt T)$. QPSM uses the actual Jordan subgradient-output law of Lemma A.1 at each current center, followed by the supplied exact Euclidean projection. For positive $d,G,R,\theta$, impose $\theta\le r_1dG/\rho$ and the independent-diameter precision budget

$$23^4\frac{\theta d^4R}{\sqrt T\,\rho r_1} +(23d)^2K\sqrt{\frac{\theta G}{\rho r_1}}\le\frac{\varepsilon}{3}.$$

A sufficient scale is a small absolute constant times

$$\min\left\{\frac{\varepsilon^3}{G^2R^2d^{9/2}}, \frac{\varepsilon^5}{G^4R^2K^2d^{9/2}}, \frac{r_1dG}{\rho}\right\}.$$

2. Mirror branch. Fix $p\in[1,\infty]$, $p\ne2$, and its Hölder-conjugate exponent. Let $P$ be open convex, $X\subseteq\overline P$, $X\cap P\ne\varnothing$, and $x_1,x^\star\in X\cap P$. The supplied mirror map $\Phi$ is strictly convex and differentiable on $P$, its gradient takes every dual value and diverges at the boundary, and it is $\mu$-strongly convex on $X\cap P$ in the chosen norm, with $\mu>0$. Exact inverse-gradient operations and attained Bregman projections are supplied. Define $R=\sqrt{D_\Phi(x^\star,x_1)}$, $K=\operatorname{diam}_p(X)$, $T=\max\{1,\lceil(6GR/(\sqrt\mu\varepsilon))^2\rceil\}$, $r_1=\varepsilon/(6G\vartheta)$, $\rho=1/(3T)$, and $\eta=(R/G)\sqrt{\mu/T}$. Here $1\le\vartheta,\vartheta_\star\le d$, $\vartheta\vartheta_\star\le d$, $\|v\|_p\le\vartheta\|v\|_\infty$, and $\|g\|_\star\le\vartheta_\star\|g\|_\infty$. Require $\theta\le r_1dG/\rho$ and

$$\frac{2GR}{\sqrt{\mu T}} +23^2\vartheta_\star K\sqrt{\frac{\theta d^3G}{\rho r_1}} +2G\vartheta r_1 +23^4\vartheta_\star^2\frac{R}{\sqrt{\mu T}}\frac{\theta d^3}{\rho r_1} \le\varepsilon.$$

This retains both noise terms; a sufficient positive precision takes the minimum of the lemma guard and small absolute multiples of $\mu\varepsilon^5/(G^4R^2K^2\vartheta_\star^2\vartheta d^3)$ and $\mu\varepsilon^3/(G^2R^2\vartheta_\star^2\vartheta d^3)$.

In either branch the classical output is the average of the first $T$ iterates, and

$$\Pr[\bar x\in X,\ f(\bar x)-f(x^\star)\le\varepsilon]\ge2/3.$$

The query costs are $O(T\max\{1,\log(3dT)\})$, with absolute constants common to all data, yielding $\widetilde O((GR/\varepsilon)^2)$ and $\widetilde O((GR/(\sqrt\mu\varepsilon))^2)$, respectively. Quantum arithmetic uses $\widetilde O(dT)$ gates, with binary word length and inverse precision exposed as polynomial arithmetic factors. Supplied geometric operations cost at most $T(T_\Pi+1)$ and $TT_{\rm next}$, respectively. All bounds apply on positive-probability branches. Conditional per-call failure control suffices; independence is not assumed.

Zero-dimensional, constant-objective, zero-radius, singleton, or already-accurate regimes return the feasible start with zero queries before divisions. In particular, a start is already accurate if $\varepsilon\ge GK$, or $\varepsilon\ge GR$ in the Euclidean branch, or $\varepsilon\ge GR\sqrt{2/\mu}$ in the mirror branch.

The result shows that quantum zeroth-order methods attain the corresponding first-order nonsmooth query rates. Formalization Note: This uses the formal appendix scope, including ambient Lipschitz control, rather than the informal “on $X$” access description. The Euclidean precision corrects B.3's omitted independent $K$; its printed $R^4$ denominator follows in the domain-radius regime $K\le2R$, which is not implied by an initial distance. The mirror radius is computed from the Bregman divergence, not introduced by an arbitrary equality. The finite-grid compilation and adaptive execution definitions are submitted for local definition review.

Target

Theorem 2.1; formal Theorems B.3 and C.1

Let $X\subseteq\mathbb R^d$ be closed, bounded and convex, let $x_1\in X$, and let $f:\mathbb R^d\to\mathbb R$ be convex and ambient $G$-Lipschitz in the stated norm. Assume an attained constrained optimum $x^\star$, and $0<\varepsilon<1$. Both branches use coherent binary evaluations on sufficiently fine finite translated hypergrids: every grid index is preserved, the encoded value has error strictly below $\theta$, and calls to the unitary and its adjoint are counted. The algorithm construction is fixed before the objective, optimum and oracle values; only geometry and supplied numerical scale bounds enter its construction.

1. Euclidean branch. Set $R=\|x_1-x^\star\|_2$, $K=\operatorname{diam}_2(X)$, $T=\max\{1,\lceil(3GR/\varepsilon)^2\rceil\}$, $r_1=\varepsilon/(6G\sqrt d)$, $\rho=1/(3T)$, and $\eta=R/(G\sqrt T)$. QPSM uses the actual Jordan subgradient-output law of Lemma A.1 at each current center, followed by the supplied exact Euclidean projection. For positive $d,G,R,\theta$, impose $\theta\le r_1dG/\rho$ and the independent-diameter precision budget

$$23^4\frac{\theta d^4R}{\sqrt T\,\rho r_1} +(23d)^2K\sqrt{\frac{\theta G}{\rho r_1}}\le\frac{\varepsilon}{3}.$$

A sufficient scale is a small absolute constant times

$$\min\left\{\frac{\varepsilon^3}{G^2R^2d^{9/2}}, \frac{\varepsilon^5}{G^4R^2K^2d^{9/2}}, \frac{r_1dG}{\rho}\right\}.$$

2. Mirror branch. Fix $p\in[1,\infty]$, $p\ne2$, and its Hölder-conjugate exponent. Let $P$ be open convex, $X\subseteq\overline P$, $X\cap P\ne\varnothing$, and $x_1,x^\star\in X\cap P$. The supplied mirror map $\Phi$ is strictly convex and differentiable on $P$, its gradient takes every dual value and diverges at the boundary, and it is $\mu$-strongly convex on $X\cap P$ in the chosen norm, with $\mu>0$. Exact inverse-gradient operations and attained Bregman projections are supplied. Define $R=\sqrt{D_\Phi(x^\star,x_1)}$, $K=\operatorname{diam}_p(X)$, $T=\max\{1,\lceil(6GR/(\sqrt\mu\varepsilon))^2\rceil\}$, $r_1=\varepsilon/(6G\vartheta)$, $\rho=1/(3T)$, and $\eta=(R/G)\sqrt{\mu/T}$. Here $1\le\vartheta,\vartheta_\star\le d$, $\vartheta\vartheta_\star\le d$, $\|v\|_p\le\vartheta\|v\|_\infty$, and $\|g\|_\star\le\vartheta_\star\|g\|_\infty$. Require $\theta\le r_1dG/\rho$ and

$$\frac{2GR}{\sqrt{\mu T}} +23^2\vartheta_\star K\sqrt{\frac{\theta d^3G}{\rho r_1}} +2G\vartheta r_1 +23^4\vartheta_\star^2\frac{R}{\sqrt{\mu T}}\frac{\theta d^3}{\rho r_1} \le\varepsilon.$$

This retains both noise terms; a sufficient positive precision takes the minimum of the lemma guard and small absolute multiples of $\mu\varepsilon^5/(G^4R^2K^2\vartheta_\star^2\vartheta d^3)$ and $\mu\varepsilon^3/(G^2R^2\vartheta_\star^2\vartheta d^3)$.

In either branch the classical output is the average of the first $T$ iterates, and

$$\Pr[\bar x\in X,\ f(\bar x)-f(x^\star)\le\varepsilon]\ge2/3.$$

The query costs are $O(T\max\{1,\log(3dT)\})$, with absolute constants common to all data, yielding $\widetilde O((GR/\varepsilon)^2)$ and $\widetilde O((GR/(\sqrt\mu\varepsilon))^2)$, respectively. Quantum arithmetic uses $\widetilde O(dT)$ gates, with binary word length and inverse precision exposed as polynomial arithmetic factors. Supplied geometric operations cost at most $T(T_\Pi+1)$ and $TT_{\rm next}$, respectively. All bounds apply on positive-probability branches. Conditional per-call failure control suffices; independence is not assumed.

Zero-dimensional, constant-objective, zero-radius, singleton, or already-accurate regimes return the feasible start with zero queries before divisions. In particular, a start is already accurate if $\varepsilon\ge GK$, or $\varepsilon\ge GR$ in the Euclidean branch, or $\varepsilon\ge GR\sqrt{2/\mu}$ in the mirror branch.

The result shows that quantum zeroth-order methods attain the corresponding first-order nonsmooth query rates. Formalization Note: This uses the formal appendix scope, including ambient Lipschitz control, rather than the informal “on $X$” access description. The Euclidean precision corrects B.3's omitted independent $K$; its printed $R^4$ denominator follows in the domain-radius regime $K\le2R$, which is not implied by an initial distance. The mirror radius is computed from the Bregman divergence, not introduced by an arbitrary equality. The finite-grid compilation and adaptive execution definitions are submitted for local definition review.

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

• Fast Convex Optimization with Quantum Gradient Methods, arXiv:2503.17356v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Quantum Signal Processing and Quantum Singular Value Transformation on $U(N)$ establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $d\geq 0$ be an integer and let $P=(P_{kj})$ be an $r\times c$ matrix of complex polynomials, with $r,c\geq 1$. Each entry has degree at most $d$ and parity $d$: $P_{kj}(-x)=(-1)^dP_{kj}(x)$. Suppose

$$I_c-P(x)^\dagger P(x)\succeq 0\qquad\text{for every }x\in[-1,1].$$

Let $\mathcal I,\mathcal O,\mathcal K$ be positive finite input, output, and signal registers, and fix known isometric computational-basis embeddings $\iota:\mathcal I\hookrightarrow\mathcal K$ and $\omega:\mathcal O\hookrightarrow\mathcal K$. The mixing register has $q$ qubits, with fixed embeddings of the $c$ input labels and $r$ output labels in its $2^q$ basis states; unused rows and columns are zero padded. An admissible oracle is any unitary $U$ on $\mathcal K$ with exact unscaled block $A=U[\omega,\iota]:\mathcal I\to\mathcal O$.

There are $d+1$ known unitary mixers on the mixing register enlarged by one flag qubit, and a fixed identification of the flag and mixing registers, chosen from $P,d$ and the known embeddings before $U$ or $A$ is supplied. The resulting synthesis circuit alternates these known operations with exactly $d$ uncontrolled oracle calls $U,U^\dagger,U,U^\dagger,\ldots$. A mixer acts conditioned on the known input signal projector at even stages and the known output signal projector at odd stages. For every admissible oracle and every family of input vectors $\phi_j\in\mathcal I$, the entire flag-zero component of its output is

$$|0\rangle_{\mathrm{flag}}\sum_{k=1}^{r}|k\rangle_{\mathrm{mix}}\,\iota_d\!\left(\sum_{j=1}^{c}P_{kj}^{(\mathrm{SV})}(A)\phi_j\right).$$

Here the input is $|0\rangle_{\mathrm{flag}}\sum_{j=1}^{c}|j\rangle_{\mathrm{mix}}\,\iota(\phi_j)$, and $\iota_d=\iota$ for even $d$ and $\iota_d=\omega$ for odd $d$. Writing $P_{kj}(x)=\sum_a p_{kj,a}x^a$, the singular-value transforms are

$$P_{kj}^{(\mathrm{SV})}(A)= \begin{cases} \displaystyle\sum_{a=0}^{\lfloor d/2\rfloor}p_{kj,2a}(A^\dagger A)^a,&d\text{ even},\\[4pt] \displaystyle\sum_{a=0}^{\lfloor d/2\rfloor}p_{kj,2a+1}A(A^\dagger A)^a,&d\text{ odd}. \end{cases}$$

All remaining amplitude lies in flag one. This simultaneously block-encodes the whole polynomial matrix at normalization one and error zero, without a positive success-probability guarantee. The formula includes the input kernel in the even case, where the constant coefficient acts as a multiple of the identity. Singular $A$, rectangular $A$ and $P$, zero $P$, and $d=0$ are permitted. A normalized joint input gives a physical state, while the equality itself is linear and holds for all vectors.

This theorem supplies coherent matrix-valued singular-value synthesis under a single matrix contraction condition. No Hermiticity, invertibility, determinant constraint, finite gate set, or classical synthesis-time estimate is imposed.

Formalization Note The printed Theorem 10 omits the degree and common-parity requirements used by its proof; these are explicit here. The output signal zero register and the orientation of the singular-vector decomposition are corrected according to Eqs. (1) and (31)–(35). The printed claim and these corrections are recorded separately in the audit notes. Known embeddings express the all-zero signal-ancilla subspaces in register-independent coordinates.

Target

Theorem 10 (U(N)-QSVT, backward), §2.3, Eq. (38), pp. 7–8

Let $d\geq 0$ be an integer and let $P=(P_{kj})$ be an $r\times c$ matrix of complex polynomials, with $r,c\geq 1$. Each entry has degree at most $d$ and parity $d$: $P_{kj}(-x)=(-1)^dP_{kj}(x)$. Suppose

$$I_c-P(x)^\dagger P(x)\succeq 0\qquad\text{for every }x\in[-1,1].$$

Let $\mathcal I,\mathcal O,\mathcal K$ be positive finite input, output, and signal registers, and fix known isometric computational-basis embeddings $\iota:\mathcal I\hookrightarrow\mathcal K$ and $\omega:\mathcal O\hookrightarrow\mathcal K$. The mixing register has $q$ qubits, with fixed embeddings of the $c$ input labels and $r$ output labels in its $2^q$ basis states; unused rows and columns are zero padded. An admissible oracle is any unitary $U$ on $\mathcal K$ with exact unscaled block $A=U[\omega,\iota]:\mathcal I\to\mathcal O$.

There are $d+1$ known unitary mixers on the mixing register enlarged by one flag qubit, and a fixed identification of the flag and mixing registers, chosen from $P,d$ and the known embeddings before $U$ or $A$ is supplied. The resulting synthesis circuit alternates these known operations with exactly $d$ uncontrolled oracle calls $U,U^\dagger,U,U^\dagger,\ldots$. A mixer acts conditioned on the known input signal projector at even stages and the known output signal projector at odd stages. For every admissible oracle and every family of input vectors $\phi_j\in\mathcal I$, the entire flag-zero component of its output is

$$|0\rangle_{\mathrm{flag}}\sum_{k=1}^{r}|k\rangle_{\mathrm{mix}}\,\iota_d\!\left(\sum_{j=1}^{c}P_{kj}^{(\mathrm{SV})}(A)\phi_j\right).$$

Here the input is $|0\rangle_{\mathrm{flag}}\sum_{j=1}^{c}|j\rangle_{\mathrm{mix}}\,\iota(\phi_j)$, and $\iota_d=\iota$ for even $d$ and $\iota_d=\omega$ for odd $d$. Writing $P_{kj}(x)=\sum_a p_{kj,a}x^a$, the singular-value transforms are

$$P_{kj}^{(\mathrm{SV})}(A)= \begin{cases} \displaystyle\sum_{a=0}^{\lfloor d/2\rfloor}p_{kj,2a}(A^\dagger A)^a,&d\text{ even},\\[4pt] \displaystyle\sum_{a=0}^{\lfloor d/2\rfloor}p_{kj,2a+1}A(A^\dagger A)^a,&d\text{ odd}. \end{cases}$$

All remaining amplitude lies in flag one. This simultaneously block-encodes the whole polynomial matrix at normalization one and error zero, without a positive success-probability guarantee. The formula includes the input kernel in the even case, where the constant coefficient acts as a multiple of the identity. Singular $A$, rectangular $A$ and $P$, zero $P$, and $d=0$ are permitted. A normalized joint input gives a physical state, while the equality itself is linear and holds for all vectors.

This theorem supplies coherent matrix-valued singular-value synthesis under a single matrix contraction condition. No Hermiticity, invertibility, determinant constraint, finite gate set, or classical synthesis-time estimate is imposed.

Formalization Note The printed Theorem 10 omits the degree and common-parity requirements used by its proof; these are explicit here. The output signal zero register and the orientation of the singular-vector decomposition are corrected according to Eqs. (1) and (31)–(35). The printed claim and these corrections are recorded separately in the audit notes. Known embeddings express the all-zero signal-ancilla subspaces in register-independent coordinates.

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 Signal Processing and Quantum Singular Value Transformation on $U(N)$, arXiv:2408.01439v4. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Quantum speedups for stochastic optimization establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $d\ge 1$ and let $f:\mathbb R^d\to\mathbb R$ be differentiable and globally convex. Suppose $f$ attains its global minimum at a point $x_\star$ with $\|x_\star\|_2\le R$, where $L,R\ge0$ are public bounds. For every query point $x$, the stochastic gradient is drawn from a measurable probability law satisfying

$$\mathbb E[g(x)]=\nabla f(x),\qquad \mathbb E\|g(x)\|_2^2\le L^2.$$

Assume coherent unitary access to this gradient law, preserving the query point and allowing arbitrary garbage, and access to the inverse oracle. The implementation uses normalized zero registers, Born measurement laws, and known Gaussian preparation and reordering operations that construct the smoothed oracle with one gradient-oracle call. These operations and the mean-estimation routine are fixed before the unknown objective and oracle. The mean-estimation interface cited on p.8 is realized, rather than assumed as a convergence hypothesis: for any sampling oracle with variance at most $L^2$, requested error $0<\eta\le L$, and $0<\delta<1$, its execution has total probability one and finite expected calls, and its estimate is within Euclidean distance $\eta$ of the mean with probability at least $1-\delta$.

For any $\epsilon>0$, run Algorithm 3 with fresh Algorithm 2 gradient estimates. In the nontrivial case $L,R>0$ and $\epsilon<LR$, its parameters are

$$T=\left\lceil4d^{1/4}LR/\epsilon\right\rceil,\quad \widehat\sigma=\frac{d^{1/8}}8\sqrt{\frac{L\epsilon}{R}},\quad r=\frac{\epsilon}{4\sqrt d L},\quad \gamma=\frac{R\sqrt{6L/r}}{(T+2)^{3/2}\widehat\sigma}.$$

It starts from $x_1=x_1^{\mathrm{ag}}=0$. At iteration $t$, set $\beta_t=(t+1)/2$, $\gamma_t=(t+1)\gamma/2$, and $x_t^{\mathrm{md}}=\beta_t^{-1}x_t+(1-\beta_t^{-1})x_t^{\mathrm{ag}}$. Use Algorithm 2 on the Gaussian-smoothed gradient law at $x_t^{\mathrm{md}}$, then use the printed ball-constrained update

$$x_{t+1}=\operatorname*{arg\,min}_{\|z\|_2\le R} \left\{\gamma_t\langle\widetilde g_t,z-x_t^{\mathrm{md}}\rangle+ \frac L{2r}\|x_t^{\mathrm{md}}-z\|_2^2\right\},\qquad x_{t+1}^{\mathrm{ag}}=\beta_t^{-1}x_{t+1}+(1-\beta_t^{-1})x_t^{\mathrm{ag}}.$$

The returned point is $x_{\mathrm{out}}=x_{T+1}^{\mathrm{ag}}$. The same execution, including its classical randomness and quantum measurements, has total probability one and satisfies

$$\mathbb E[f(x_{\mathrm{out}})-f(x_\star)]\le\epsilon,\qquad \mathbb E[Q]=\widetilde O\!\left(d^{5/8}(LR/\epsilon)^{3/2}\right).$$

Here $Q$ counts every call to the original gradient oracle and its inverse. Its expectation is finite; the positive geometric level in Algorithm 2 allows an unbounded query count. Explicitly, there are absolute constants $C>0$, an integer $p\ge0$, and a threshold $a\ge1$, all independent of the dimension, bounds, accuracy, objective, probability laws, and register realization, such that whenever $LR/\epsilon\ge a$,

$$\mathbb E[Q]\le C d^{5/8}(LR/\epsilon)^{3/2} \max\{1,\log(2+d)+|\log\epsilon|+|\log L|+|\log R|\}^{p}.$$

If $L=0$, $R=0$, or $\epsilon\ge LR$, the implementation returns $0$ with no queries and retains the expected-accuracy guarantee. The minimizing point $x_\star$ is used only to express the guarantee and is not supplied to the algorithm. This result gives the expected-query speedup of the paper's quantum accelerated stochastic approximation method; it asserts no gate-complexity or fixed-confidence output bound.

Formalization Note The real iteration budget on p.13 is rounded upward to define a finite loop. The statement preserves the proximal center and all other displayed constants. The p.13/p.15 pointwise gradient assertion is incompatible with the stated second-moment hypothesis; the proof also contains an extra factor $1/r$, a reversed optimum-gap sign, and a constant gap in its use of Lemma 5. These are disclosed proof gaps, not additional hypotheses or silent changes to Algorithm 3. No directional-mean definition is imported or reconstructed.

Target

Theorem 5 (Formal version of Theorem 1, Part 1)

Let $d\ge 1$ and let $f:\mathbb R^d\to\mathbb R$ be differentiable and globally convex. Suppose $f$ attains its global minimum at a point $x_\star$ with $\|x_\star\|_2\le R$, where $L,R\ge0$ are public bounds. For every query point $x$, the stochastic gradient is drawn from a measurable probability law satisfying

$$\mathbb E[g(x)]=\nabla f(x),\qquad \mathbb E\|g(x)\|_2^2\le L^2.$$

Assume coherent unitary access to this gradient law, preserving the query point and allowing arbitrary garbage, and access to the inverse oracle. The implementation uses normalized zero registers, Born measurement laws, and known Gaussian preparation and reordering operations that construct the smoothed oracle with one gradient-oracle call. These operations and the mean-estimation routine are fixed before the unknown objective and oracle. The mean-estimation interface cited on p.8 is realized, rather than assumed as a convergence hypothesis: for any sampling oracle with variance at most $L^2$, requested error $0<\eta\le L$, and $0<\delta<1$, its execution has total probability one and finite expected calls, and its estimate is within Euclidean distance $\eta$ of the mean with probability at least $1-\delta$.

For any $\epsilon>0$, run Algorithm 3 with fresh Algorithm 2 gradient estimates. In the nontrivial case $L,R>0$ and $\epsilon<LR$, its parameters are

$$T=\left\lceil4d^{1/4}LR/\epsilon\right\rceil,\quad \widehat\sigma=\frac{d^{1/8}}8\sqrt{\frac{L\epsilon}{R}},\quad r=\frac{\epsilon}{4\sqrt d L},\quad \gamma=\frac{R\sqrt{6L/r}}{(T+2)^{3/2}\widehat\sigma}.$$

It starts from $x_1=x_1^{\mathrm{ag}}=0$. At iteration $t$, set $\beta_t=(t+1)/2$, $\gamma_t=(t+1)\gamma/2$, and $x_t^{\mathrm{md}}=\beta_t^{-1}x_t+(1-\beta_t^{-1})x_t^{\mathrm{ag}}$. Use Algorithm 2 on the Gaussian-smoothed gradient law at $x_t^{\mathrm{md}}$, then use the printed ball-constrained update

$$x_{t+1}=\operatorname*{arg\,min}_{\|z\|_2\le R} \left\{\gamma_t\langle\widetilde g_t,z-x_t^{\mathrm{md}}\rangle+ \frac L{2r}\|x_t^{\mathrm{md}}-z\|_2^2\right\},\qquad x_{t+1}^{\mathrm{ag}}=\beta_t^{-1}x_{t+1}+(1-\beta_t^{-1})x_t^{\mathrm{ag}}.$$

The returned point is $x_{\mathrm{out}}=x_{T+1}^{\mathrm{ag}}$. The same execution, including its classical randomness and quantum measurements, has total probability one and satisfies

$$\mathbb E[f(x_{\mathrm{out}})-f(x_\star)]\le\epsilon,\qquad \mathbb E[Q]=\widetilde O\!\left(d^{5/8}(LR/\epsilon)^{3/2}\right).$$

Here $Q$ counts every call to the original gradient oracle and its inverse. Its expectation is finite; the positive geometric level in Algorithm 2 allows an unbounded query count. Explicitly, there are absolute constants $C>0$, an integer $p\ge0$, and a threshold $a\ge1$, all independent of the dimension, bounds, accuracy, objective, probability laws, and register realization, such that whenever $LR/\epsilon\ge a$,

$$\mathbb E[Q]\le C d^{5/8}(LR/\epsilon)^{3/2} \max\{1,\log(2+d)+|\log\epsilon|+|\log L|+|\log R|\}^{p}.$$

If $L=0$, $R=0$, or $\epsilon\ge LR$, the implementation returns $0$ with no queries and retains the expected-accuracy guarantee. The minimizing point $x_\star$ is used only to express the guarantee and is not supplied to the algorithm. This result gives the expected-query speedup of the paper's quantum accelerated stochastic approximation method; it asserts no gate-complexity or fixed-confidence output bound.

Formalization Note The real iteration budget on p.13 is rounded upward to define a finite loop. The statement preserves the proximal center and all other displayed constants. The p.13/p.15 pointwise gradient assertion is incompatible with the stated second-moment hypothesis; the proof also contains an extra factor $1/r$, a reversed optimum-gap sign, and a constant gap in its use of Lemma 5. These are disclosed proof gaps, not additional hypotheses or silent changes to Algorithm 3. No directional-mean definition is imported or reconstructed.

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 speedups for stochastic optimization, arXiv:2308.01582v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

The Quantum Esscher Transform establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $d\ge1$, $n,a,n_\rho\ge0$, $\theta\in\mathbb R^d$, and $\kappa>1$ be public parameters. Set

$$\beta=\sum_{j=1}^d|\theta_j|+2(1+\log_2(2\kappa)),\qquad L=\log_2(1/\varepsilon),\qquad \varepsilon_{\rm BE}=\left(\frac{\varepsilon}{8L}\right)^2,$$

where $0<\varepsilon<2^{-\beta}$. The input $\rho$ is an $n$-qubit trace-one density operator whose eigenvalues lie in $[1/\kappa,1]$. Each $H_j$ is Hermitian with $\|H_j\|_{\rm op}\le1$. Purified access is a unitary $O_\rho$ on $n_\rho+n$ qubits preparing a purification of $\rho$, with the $n_\rho$ ancillary qubits first. Let $U_\rho$ be the exact $(1,n+n_\rho,0)$ block-encoding supplied by the purification construction of Proposition 12. For each $j$, supplied $U_j$ is a $(1,a,\varepsilon_{\rm BE})$ block-encoding of $H_j$; ordinary, adjoint and controlled signal access are available.

There are universal constants $C_\rho,C_{\rm obs}>0$, a nonnegative integer $p$, and a universal threshold $0<\varepsilon_0<1$ such that, for every admissible public parameter choice with $\varepsilon\le\varepsilon_0$, a QEsscher circuit can be selected before $\rho,H_j,O_\rho,U_j$. This circuit is the logarithm transformation, coefficient state-preparation pair, padded linear combination, and exponential transformation of Algorithm 1. It works for every admissible hidden input and oracle completion. With $b=\lceil\log_2(d+1)\rceil$ and $a_{\rm out}=\max(a,n+n_\rho)+b+4$, its unitary $U_{\rm out}$ satisfies

$$\left\|\sigma-(\langle0^{a_{\rm out}}|\otimes I_n)U_{\rm out}(|0^{a_{\rm out}}\rangle\otimes I_n)\right\|_{\rm op}\le\varepsilon, \qquad \sigma=\frac{\exp\!\left(\sum_{j=1}^d\theta_jH_j+\log_2\rho\right)}{4e^\beta}.$$

Its oracle counts, including ordinary, adjoint and controlled calls, obey

$$q_\rho\le C_\rho\kappa L^2\max\!\left(1,\log_2(2+\kappa L^2)\right)^p, \qquad q_j\le C_{\rm obs}L\quad(j\in[d]).$$

The logarithm of a positive matrix is defined by applying $\log_2$ to its eigenvalues; $\exp$ is the natural matrix exponential. The constants, exponent and threshold are independent of all public parameters, hidden matrices and oracle implementations.

This supplies the subnormalized transform as a block-encoding, useful as an operator primitive. The query count is for $U_\rho$; each such call can be implemented with a constant number of purification-oracle calls. The actual $n_\rho$ is retained in the footprint; the source's $n_\rho=\operatorname{poly}(n)$ is a family convention, and no gate-time conclusion is asserted.

Source corrections and limitation. Algorithm 1 and Step 3 print $b=\lceil\log_2d\rceil$, although their $d+1$ coefficients require $b=\lceil\log_2(d+1)\rceil$. The box prints the divisor $e^\beta$; the statement uses proof Step 5's explicit $4e^\beta$. The printed error schedule is retained. The claim that its numeral 8 ensures Eq. (III.2) has an unresolved quantitative degree-bound gap; accuracy remains the theorem's conclusion, without adding that bound as an assumption.

Target

Theorem 5 (Algorithm 1 and proof, pp.6–7)

Let $d\ge1$, $n,a,n_\rho\ge0$, $\theta\in\mathbb R^d$, and $\kappa>1$ be public parameters. Set

$$\beta=\sum_{j=1}^d|\theta_j|+2(1+\log_2(2\kappa)),\qquad L=\log_2(1/\varepsilon),\qquad \varepsilon_{\rm BE}=\left(\frac{\varepsilon}{8L}\right)^2,$$

where $0<\varepsilon<2^{-\beta}$. The input $\rho$ is an $n$-qubit trace-one density operator whose eigenvalues lie in $[1/\kappa,1]$. Each $H_j$ is Hermitian with $\|H_j\|_{\rm op}\le1$. Purified access is a unitary $O_\rho$ on $n_\rho+n$ qubits preparing a purification of $\rho$, with the $n_\rho$ ancillary qubits first. Let $U_\rho$ be the exact $(1,n+n_\rho,0)$ block-encoding supplied by the purification construction of Proposition 12. For each $j$, supplied $U_j$ is a $(1,a,\varepsilon_{\rm BE})$ block-encoding of $H_j$; ordinary, adjoint and controlled signal access are available.

There are universal constants $C_\rho,C_{\rm obs}>0$, a nonnegative integer $p$, and a universal threshold $0<\varepsilon_0<1$ such that, for every admissible public parameter choice with $\varepsilon\le\varepsilon_0$, a QEsscher circuit can be selected before $\rho,H_j,O_\rho,U_j$. This circuit is the logarithm transformation, coefficient state-preparation pair, padded linear combination, and exponential transformation of Algorithm 1. It works for every admissible hidden input and oracle completion. With $b=\lceil\log_2(d+1)\rceil$ and $a_{\rm out}=\max(a,n+n_\rho)+b+4$, its unitary $U_{\rm out}$ satisfies

$$\left\|\sigma-(\langle0^{a_{\rm out}}|\otimes I_n)U_{\rm out}(|0^{a_{\rm out}}\rangle\otimes I_n)\right\|_{\rm op}\le\varepsilon, \qquad \sigma=\frac{\exp\!\left(\sum_{j=1}^d\theta_jH_j+\log_2\rho\right)}{4e^\beta}.$$

Its oracle counts, including ordinary, adjoint and controlled calls, obey

$$q_\rho\le C_\rho\kappa L^2\max\!\left(1,\log_2(2+\kappa L^2)\right)^p, \qquad q_j\le C_{\rm obs}L\quad(j\in[d]).$$

The logarithm of a positive matrix is defined by applying $\log_2$ to its eigenvalues; $\exp$ is the natural matrix exponential. The constants, exponent and threshold are independent of all public parameters, hidden matrices and oracle implementations.

This supplies the subnormalized transform as a block-encoding, useful as an operator primitive. The query count is for $U_\rho$; each such call can be implemented with a constant number of purification-oracle calls. The actual $n_\rho$ is retained in the footprint; the source's $n_\rho=\operatorname{poly}(n)$ is a family convention, and no gate-time conclusion is asserted.

Source corrections and limitation. Algorithm 1 and Step 3 print $b=\lceil\log_2d\rceil$, although their $d+1$ coefficients require $b=\lceil\log_2(d+1)\rceil$. The box prints the divisor $e^\beta$; the statement uses proof Step 5's explicit $4e^\beta$. The printed error schedule is retained. The claim that its numeral 8 ensures Eq. (III.2) has an unresolved quantitative degree-bound gap; accuracy remains the theorem's conclusion, without adding that bound as an assumption.

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

• The Quantum Esscher Transform, arXiv:2401.07561v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.