All missions

Motivation

Shadow Tomography of Quantum States establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

There are universal constants $C>0$ and $p\in\mathbb N$ and one explicit adaptive measurement constructor with the following property. Let $D,M\ge1$ be integers, let $E_1,\ldots,E_M$ be known two-outcome measurement effects on $\mathbb C^D$ (so $0\preceq E_i\preceq I$), and let $0<\varepsilon,\delta<1$. The constructor depends on these known data and not on the unknown state.

Write $L_D=\max\{1,\log D\}$, $L_M=\max\{1,\log M\}$, $L_\delta=\max\{1,\log(1/\delta)\}$, $L_\varepsilon=\max\{1,\log(1/\varepsilon)\}$, $L_{LM}=\max\{1,\log L_M\}$, and $L_{LD}=\max\{1,\log L_D\}$. The constructed procedure uses $k$ independent copies of the unknown state, with

$$k\le\left\lceil C\varepsilon^{-4}L_\delta L_M^4 L_D(1+L_{LM}+L_{LD}+L_\varepsilon)^p\right\rceil.$$

For every density matrix $\rho$ on $\mathbb C^D$, a run on $\rho^{\otimes k}$ returns numbers $b_1,\ldots,b_M\in[0,1]$ satisfying

$$\Pr\!\left[\forall i\in\{1,\ldots,M\},\ |b_i-\operatorname{Tr}(E_i\rho)|\le\varepsilon\right]\ge1-\delta.$$

Collective measurements, adaptive measurements, temporary ancillas, and unrestricted known-data classical computation are permitted. The procedure composes physical quantum-OR decision programs, the paper's binary gentle search over signed amplified deviation effects, and classical matrix multiplicative weights. This estimates the entire specified list simultaneously without reconstructing the unknown density matrix in trace distance.

Formalization Note The finite adaptive instrument programs carry normalized Kraus families. The constructor supplies actual physical decision programs, not an assumed accuracy contract or a state oracle. The source composition is executed by chunk-local recursive definitions. The logarithm floors extend the asymptotic notation to $D=1$, $M=1$, and other finite boundary regimes; they introduce no additional asymptotic parameter dependence. No computation-time or gate-complexity assertion is made.

Target

Theorem 2 (Shadow Tomography Theorem); Problem 1

There are universal constants $C>0$ and $p\in\mathbb N$ and one explicit adaptive measurement constructor with the following property. Let $D,M\ge1$ be integers, let $E_1,\ldots,E_M$ be known two-outcome measurement effects on $\mathbb C^D$ (so $0\preceq E_i\preceq I$), and let $0<\varepsilon,\delta<1$. The constructor depends on these known data and not on the unknown state.

Write $L_D=\max\{1,\log D\}$, $L_M=\max\{1,\log M\}$, $L_\delta=\max\{1,\log(1/\delta)\}$, $L_\varepsilon=\max\{1,\log(1/\varepsilon)\}$, $L_{LM}=\max\{1,\log L_M\}$, and $L_{LD}=\max\{1,\log L_D\}$. The constructed procedure uses $k$ independent copies of the unknown state, with

$$k\le\left\lceil C\varepsilon^{-4}L_\delta L_M^4 L_D(1+L_{LM}+L_{LD}+L_\varepsilon)^p\right\rceil.$$

For every density matrix $\rho$ on $\mathbb C^D$, a run on $\rho^{\otimes k}$ returns numbers $b_1,\ldots,b_M\in[0,1]$ satisfying

$$\Pr\!\left[\forall i\in\{1,\ldots,M\},\ |b_i-\operatorname{Tr}(E_i\rho)|\le\varepsilon\right]\ge1-\delta.$$

Collective measurements, adaptive measurements, temporary ancillas, and unrestricted known-data classical computation are permitted. The procedure composes physical quantum-OR decision programs, the paper's binary gentle search over signed amplified deviation effects, and classical matrix multiplicative weights. This estimates the entire specified list simultaneously without reconstructing the unknown density matrix in trace distance.

Formalization Note The finite adaptive instrument programs carry normalized Kraus families. The constructor supplies actual physical decision programs, not an assumed accuracy contract or a state oracle. The source composition is executed by chunk-local recursive definitions. The logarithm floors extend the asymptotic notation to $D=1$, $M=1$, and other finite boundary regimes; they introduce no additional asymptotic parameter dependence. No computation-time or gate-complexity assertion is made.

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

• Shadow Tomography of Quantum States, arXiv:1711.01053v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Quantum speedup of Monte Carlo methods establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $A$ be the coherent unitary representation of a randomized or quantum computation on $n=h+k$ qubits, initially in $|0^n\rangle$, with no intermediate measurements and with access to its inverse. Measuring the last $k$ qubits gives a bit string $x$, whose output is the fixed value $\varphi(x)\in[0,1]$. The value-dependent flag rotation is supplied exactly; the source assumes that $\varphi$ is easily computable. Write $\mu=\mathbb E[v(A)]$.

Attach a fresh flag and prepare $|\psi\rangle$ by rotating it to $\sqrt{1-\varphi(x)}|0\rangle+\sqrt{\varphi(x)}|1\rangle$. Set $P=I\otimes|1\rangle\langle1|$, $U=2|\psi\rangle\langle\psi|-I$, and $V=I-2P$. For any positive integer $t$ and $0<\delta<1$, Algorithm 1 applies amplitude estimation independently $r(\delta)=2\lceil100\log(1/\delta)\rceil+1$ times and returns the median $\widetilde\mu$. One run uses uniform control on $\{0,\ldots,t-1\}$, controlled powers of $UV$, the inverse Fourier transform of dimension $t$, and the estimate $\sin^2(\pi j/t)$ for control outcome $j$.

There exist positive universal constants $C,K,D$, chosen before all sampler data and parameters, such that, with $L_\delta=\max\{1,\log(1/\delta)\}$,

$$N_{\mathrm{copies}}\le K L_\delta,\qquad N_U\le KtL_\delta,\qquad \Pr\!\left[|\widetilde\mu-\mu|\le C\left(\frac{\sqrt\mu}{t}+\frac{1}{t^2}\right)\right]\ge1-\delta.$$

Here the actual schedule consumes $r(\delta)$ fresh copies of $A|0^n\rangle$ and $r(\delta)(t-1)$ calls to $U$, counting controlled calls as uses.

For every $0<\varepsilon\le1$:

1. If $\mu>0$, there is a positive integer $t\le D/(\varepsilon\sqrt\mu)$ for which $\Pr[|\widetilde\mu-\mu|\le\varepsilon\mu]\ge1-\delta$.
2. There is a positive integer $t\le D/\varepsilon$ for which $\Pr[|\widetilde\mu-\mu|\le\varepsilon]\ge1-\delta$.

If $\mu=0$, the estimator returns zero with probability one for every positive integer $t$. The bounds hold for every coherent computation, including each instance of any oracle it uses. They quantify copies and reflections separately.

This is the bounded-output mean-estimation subroutine used by the paper's later Monte Carlo algorithms.

Formalization Note The selected result is Theorem 3 on PDF pages 8–9, rather than a later bounded-variance theorem. The printed reciprocal rates at $\varepsilon=0$ supply no finite exact-estimation claim; the reciprocal corollaries therefore use $0<\varepsilon\le1$. The all-confidence bound $L_\delta$ agrees with $O(\log(1/\delta))$ as $\delta$ tends to zero. The unspecified repetition coefficient is fixed to the odd representative above. The theorem asserts no gate-time bound for computing $\varphi$.

Target

Theorem 3, §2.1 (continues on PDF p.9); Algorithm 1

Let $A$ be the coherent unitary representation of a randomized or quantum computation on $n=h+k$ qubits, initially in $|0^n\rangle$, with no intermediate measurements and with access to its inverse. Measuring the last $k$ qubits gives a bit string $x$, whose output is the fixed value $\varphi(x)\in[0,1]$. The value-dependent flag rotation is supplied exactly; the source assumes that $\varphi$ is easily computable. Write $\mu=\mathbb E[v(A)]$.

Attach a fresh flag and prepare $|\psi\rangle$ by rotating it to $\sqrt{1-\varphi(x)}|0\rangle+\sqrt{\varphi(x)}|1\rangle$. Set $P=I\otimes|1\rangle\langle1|$, $U=2|\psi\rangle\langle\psi|-I$, and $V=I-2P$. For any positive integer $t$ and $0<\delta<1$, Algorithm 1 applies amplitude estimation independently $r(\delta)=2\lceil100\log(1/\delta)\rceil+1$ times and returns the median $\widetilde\mu$. One run uses uniform control on $\{0,\ldots,t-1\}$, controlled powers of $UV$, the inverse Fourier transform of dimension $t$, and the estimate $\sin^2(\pi j/t)$ for control outcome $j$.

There exist positive universal constants $C,K,D$, chosen before all sampler data and parameters, such that, with $L_\delta=\max\{1,\log(1/\delta)\}$,

$$N_{\mathrm{copies}}\le K L_\delta,\qquad N_U\le KtL_\delta,\qquad \Pr\!\left[|\widetilde\mu-\mu|\le C\left(\frac{\sqrt\mu}{t}+\frac{1}{t^2}\right)\right]\ge1-\delta.$$

Here the actual schedule consumes $r(\delta)$ fresh copies of $A|0^n\rangle$ and $r(\delta)(t-1)$ calls to $U$, counting controlled calls as uses.

For every $0<\varepsilon\le1$:

1. If $\mu>0$, there is a positive integer $t\le D/(\varepsilon\sqrt\mu)$ for which $\Pr[|\widetilde\mu-\mu|\le\varepsilon\mu]\ge1-\delta$.
2. There is a positive integer $t\le D/\varepsilon$ for which $\Pr[|\widetilde\mu-\mu|\le\varepsilon]\ge1-\delta$.

If $\mu=0$, the estimator returns zero with probability one for every positive integer $t$. The bounds hold for every coherent computation, including each instance of any oracle it uses. They quantify copies and reflections separately.

This is the bounded-output mean-estimation subroutine used by the paper's later Monte Carlo algorithms.

Formalization Note The selected result is Theorem 3 on PDF pages 8–9, rather than a later bounded-variance theorem. The printed reciprocal rates at $\varepsilon=0$ supply no finite exact-estimation claim; the reciprocal corollaries therefore use $0<\varepsilon\le1$. The all-confidence bound $L_\delta$ agrees with $O(\log(1/\delta))$ as $\delta$ tends to zero. The unspecified repetition coefficient is fixed to the odd representative above. The theorem asserts no gate-time bound for computing $\varphi$.

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 speedup of Monte Carlo methods, arXiv:1504.06987v3. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

The Power of Two Bases: Robust and copy-optimal certification of nearly all quantum states with few-qubit measurements establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

There is a single efficient oracle procedure for certifying a pure target state using one copy of an arbitrary mixed lab state. The classical oracle returns the exact amplitudes of the target in the computational basis and in the full-register Hadamard basis, as in Definition 1 of the paper.

More precisely, there exist a polynomial resource bound $p$, a constant $C>0$, a threshold $n_0\ge1$, a nonnegative sequence $\eta_n\to0$, and measurable sets $G_n$ of normalized $n$-qubit target states such that, for all $n\ge n_0$,

$$\Pr_{\psi\sim\mathrm{Haar}_n}[\psi\notin G_n]\le C2^{-n}.$$

For every $\psi\in G_n$ and every density matrix $\rho$ on the same $n$ qubits, write $F(\psi,\rho)=\langle\psi|\rho|\psi\rangle$. The procedure satisfies

$$\Pr[\mathrm{accept}]\ge F(\psi,\rho),\qquad \Pr[\mathrm{reject}]\ge\frac{1-F(\psi,\rho)}{2}-\eta_n.$$

It flips one fair classical bit and measures the first $r=n-k$ qubits either all in the $Z$ basis or all in the $X$ basis, where $k=\min\{n,\lceil2\log_2(\max\{2,n\})\rceil\}$. Given the observed prefix, it reads the $2^k$ oracle amplitudes for that prefix, computes the conditional target, and performs one projector/complement measurement on the fixed suffix of $k$ qubits. In the $X$ branch, the full-Hadamard oracle fiber is transformed by $H^{\otimes k}$ to obtain the physical conditional target. A zero target fiber is always rejected. The executed oracle calls, scalar instructions, and suffix circuit gates are bounded by $p(n)$, uniformly over normalized targets and every branch; the compiled accepting effect is the conditional target projector.

The same good set and error sequence apply simultaneously to all lab density matrices. This provides the paper's constant robustness with only one measurement involving logarithmically many qubits.

Formalization Note The suffix rounding fixes the proof's choice $\gamma=1$. Efficiency is relative to exact complex-answer classical oracle access and ideal scalar operations, with arbitrary one- and two-qubit unitaries for exact synthesis. No finite-precision or oracle-simulation cost is claimed. The Lean statement uses the concrete frozen conditional measurement program and its execution-derived resource counts, and gives the additive soundness of Theorem 1.

Target

Theorem 1

There is a single efficient oracle procedure for certifying a pure target state using one copy of an arbitrary mixed lab state. The classical oracle returns the exact amplitudes of the target in the computational basis and in the full-register Hadamard basis, as in Definition 1 of the paper.

More precisely, there exist a polynomial resource bound $p$, a constant $C>0$, a threshold $n_0\ge1$, a nonnegative sequence $\eta_n\to0$, and measurable sets $G_n$ of normalized $n$-qubit target states such that, for all $n\ge n_0$,

$$\Pr_{\psi\sim\mathrm{Haar}_n}[\psi\notin G_n]\le C2^{-n}.$$

For every $\psi\in G_n$ and every density matrix $\rho$ on the same $n$ qubits, write $F(\psi,\rho)=\langle\psi|\rho|\psi\rangle$. The procedure satisfies

$$\Pr[\mathrm{accept}]\ge F(\psi,\rho),\qquad \Pr[\mathrm{reject}]\ge\frac{1-F(\psi,\rho)}{2}-\eta_n.$$

It flips one fair classical bit and measures the first $r=n-k$ qubits either all in the $Z$ basis or all in the $X$ basis, where $k=\min\{n,\lceil2\log_2(\max\{2,n\})\rceil\}$. Given the observed prefix, it reads the $2^k$ oracle amplitudes for that prefix, computes the conditional target, and performs one projector/complement measurement on the fixed suffix of $k$ qubits. In the $X$ branch, the full-Hadamard oracle fiber is transformed by $H^{\otimes k}$ to obtain the physical conditional target. A zero target fiber is always rejected. The executed oracle calls, scalar instructions, and suffix circuit gates are bounded by $p(n)$, uniformly over normalized targets and every branch; the compiled accepting effect is the conditional target projector.

The same good set and error sequence apply simultaneously to all lab density matrices. This provides the paper's constant robustness with only one measurement involving logarithmically many qubits.

Formalization Note The suffix rounding fixes the proof's choice $\gamma=1$. Efficiency is relative to exact complex-answer classical oracle access and ideal scalar operations, with arbitrary one- and two-qubit unitaries for exact synthesis. No finite-precision or oracle-simulation cost is claimed. The Lean statement uses the concrete frozen conditional measurement program and its execution-derived resource counts, and gives the additive soundness of Theorem 1.

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 Power of Two Bases: Robust and copy-optimal certification of nearly all quantum states with few-qubit measurements, arXiv:2602.11616v1. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Approximate sampling from decoded quantum interferometry via Markov chain Monte Carlo methods establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $p$ be prime, $B\in\mathbb F_p^{m\times n}$, and $F_i\subseteq\mathbb F_p$ satisfy $|F_i|=r$ for every $i$, where $0\le r<p$. For $x\in\mathbb F_p^n$, define the signed objective $f(x)=\sum_{i=1}^m(2\mathbf1_{(Bx)_i\in F_i}-1)$. Let $C^\perp=\{c\in\mathbb F_p^m:B^\mathsf Tc=0\}$ and let $d$ be its minimum nonzero Hamming weight, with $d=+\infty$ when $C^\perp=\{0\}$.

Let $P\in\mathbb R[t]$ have degree $\ell$, satisfy $\sum_xP(f(x))^2=1$, and obey $2\ell+1\le d$. Define $\mathcal P_{\mathrm{DQI}}(x)=P(f(x))^2$ and $\beta_h=[t^h]P(t)^2$. For every nonnegative integer $k$ such that $k+2\ell<d$,

$$\mathbb E_{x\sim\mathcal P_{\mathrm{DQI}}}[f(x)^k] =p^n\mathbb E_{J\sim\operatorname{Binom}(m,r/p)} \left[\sum_{h=0}^{2\ell}\beta_h(2J-m)^{k+h}\right].$$

Equivalently, the right side is

$$p^n\sum_{j=0}^m\binom mj \left(\frac rp\right)^j\left(1-\frac rp\right)^{m-j} \sum_{h=0}^{2\ell}\beta_h(2j-m)^{k+h}.$$

This identity characterizes the low-order moments of the signed score under the DQI distribution through binomial moments.

Formalization Note Expectations are finite real sums. The code and its extended natural minimum distance are computed from $B$ using the frozen field-code definitions. The squared-amplitude weights are the frozen real polynomial weights; for real amplitudes they equal the computational-basis probabilities of the frozen DQI state. No additional normalization denominator is introduced.

Target

Theorem 3, Appendix B, Eq. (B60)

Let $p$ be prime, $B\in\mathbb F_p^{m\times n}$, and $F_i\subseteq\mathbb F_p$ satisfy $|F_i|=r$ for every $i$, where $0\le r<p$. For $x\in\mathbb F_p^n$, define the signed objective $f(x)=\sum_{i=1}^m(2\mathbf1_{(Bx)_i\in F_i}-1)$. Let $C^\perp=\{c\in\mathbb F_p^m:B^\mathsf Tc=0\}$ and let $d$ be its minimum nonzero Hamming weight, with $d=+\infty$ when $C^\perp=\{0\}$.

Let $P\in\mathbb R[t]$ have degree $\ell$, satisfy $\sum_xP(f(x))^2=1$, and obey $2\ell+1\le d$. Define $\mathcal P_{\mathrm{DQI}}(x)=P(f(x))^2$ and $\beta_h=[t^h]P(t)^2$. For every nonnegative integer $k$ such that $k+2\ell<d$,

$$\mathbb E_{x\sim\mathcal P_{\mathrm{DQI}}}[f(x)^k] =p^n\mathbb E_{J\sim\operatorname{Binom}(m,r/p)} \left[\sum_{h=0}^{2\ell}\beta_h(2J-m)^{k+h}\right].$$

Equivalently, the right side is

$$p^n\sum_{j=0}^m\binom mj \left(\frac rp\right)^j\left(1-\frac rp\right)^{m-j} \sum_{h=0}^{2\ell}\beta_h(2j-m)^{k+h}.$$

This identity characterizes the low-order moments of the signed score under the DQI distribution through binomial moments.

Formalization Note Expectations are finite real sums. The code and its extended natural minimum distance are computed from $B$ using the frozen field-code definitions. The squared-amplitude weights are the frozen real polynomial weights; for real amplitudes they equal the computational-basis probabilities of the frozen DQI state. No additional normalization denominator is introduced.

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

• Approximate sampling from decoded quantum interferometry via Markov chain Monte Carlo methods, arXiv:2607.28120v1. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Quantum state tomography via compressed sensing establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $n\ge 0$ be the number of qubits, $d=2^n$, and let $\rho\in\mathbb C^{d\times d}$ be a fixed density matrix (positive semidefinite with trace one) of exact rank $r$. There are absolute constants $a,b,c_0>0$, independent of $n,r,\rho$, such that the following holds for every $c\ge c_0$.

Set $m=\lceil cdr(\ln d)^2\rceil$. Independently sample $m$ unphased Pauli strings $w(A_i)$, uniformly with replacement from all $d^2$ tensor products of $I,X,Y,Z$, including the identity. Suppose their exact expectations $y_i=\operatorname{Tr}(w(A_i)\rho)$ are known. Write $\mathcal O(A,y)$ for the set of minimizers of

$$\min_{\sigma=\sigma^\dagger}\|\sigma\|_{\mathrm{tr}} \quad\text{subject to}\quad \operatorname{Tr}\sigma=1,\qquad \operatorname{Tr}(w(A_i)\sigma)=y_i\quad(1\le i\le m).$$

The trace norm is the sum of the singular values; competitors need not be positive semidefinite and have no rank constraint. Then

$$\Pr_A\!\left[\mathcal O(A,y)\ne\{\rho\}\right]\le a e^{-bc}.$$

Thus this specific convex program attains its minimum uniquely at the unknown state with exponentially small failure probability. The probability is over the design for each fixed state, and $m$ counts exact expectation settings, rather than physical copies or computation time.

Formalization Note Natural logarithms and integer rounding pin down the paper's asymptotic notation using its closing proof on PDF p.3. The sampling law and optimizer set are frozen definitions depending only on public $n,m$, and on the design and supplied data, respectively. For $n=0$, $d=r=1$ and $m=0$; trace one alone gives unique recovery.

Target

Theorem 1 (Low-rank tomography), convex program (1)

Let $n\ge 0$ be the number of qubits, $d=2^n$, and let $\rho\in\mathbb C^{d\times d}$ be a fixed density matrix (positive semidefinite with trace one) of exact rank $r$. There are absolute constants $a,b,c_0>0$, independent of $n,r,\rho$, such that the following holds for every $c\ge c_0$.

Set $m=\lceil cdr(\ln d)^2\rceil$. Independently sample $m$ unphased Pauli strings $w(A_i)$, uniformly with replacement from all $d^2$ tensor products of $I,X,Y,Z$, including the identity. Suppose their exact expectations $y_i=\operatorname{Tr}(w(A_i)\rho)$ are known. Write $\mathcal O(A,y)$ for the set of minimizers of

$$\min_{\sigma=\sigma^\dagger}\|\sigma\|_{\mathrm{tr}} \quad\text{subject to}\quad \operatorname{Tr}\sigma=1,\qquad \operatorname{Tr}(w(A_i)\sigma)=y_i\quad(1\le i\le m).$$

The trace norm is the sum of the singular values; competitors need not be positive semidefinite and have no rank constraint. Then

$$\Pr_A\!\left[\mathcal O(A,y)\ne\{\rho\}\right]\le a e^{-bc}.$$

Thus this specific convex program attains its minimum uniquely at the unknown state with exponentially small failure probability. The probability is over the design for each fixed state, and $m$ counts exact expectation settings, rather than physical copies or computation time.

Formalization Note Natural logarithms and integer rounding pin down the paper's asymptotic notation using its closing proof on PDF p.3. The sampling law and optimizer set are frozen definitions depending only on public $n,m$, and on the design and supplied data, respectively. For $n=0$, $d=r=1$ and $m=0$; trace one alone gives unique recovery.

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 state tomography via compressed sensing, arXiv:0909.3304v4. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Quantum chi-squared tomography and mutual information testing establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

There are absolute constants $C>0$ and $0<\epsilon_0\le 1/2$ with the following property. For every integer dimension $d\ge 1$, supplied integer rank bound $1\le r\le d$, and accuracy $0<\epsilon\le\epsilon_0$, one can choose a copy count $n\ge 0$ and a lawful collective measurement on $n$ independent identical copies of a state, with a density matrix as its classical outcome, such that

$$n\le C\frac{rd}{\epsilon}\left(\ln\frac{d}{\epsilon}\right)^2,\qquad \Pr_{\widehat\rho\sim\mathcal M(\rho^{\otimes n})}\!\left[S(\rho\Vert\widehat\rho)\le\epsilon\right]\ge 0.99.$$

The probability guarantee holds for every unknown positive semidefinite $d\times d$ matrix $\rho$ of trace one and rank at most $r$. The measurement is chosen using only $d,r,\epsilon$, before $\rho$. Here $S$ is Umegaki quantum relative entropy with natural logarithms: $S(\rho\Vert\sigma)=\operatorname{Tr}(\rho\ln\rho-\rho\ln\sigma)$ when $\operatorname{supp}\rho\subseteq\operatorname{supp}\sigma$, and $+\infty$ otherwise; zero-eigenvalue terms use their continuous limits. The estimate may have any rank.

This gives relative entropy tomography with $\widetilde O(rd/\epsilon)$ copies, including singular input states. Larger positive accuracies follow by running at a fixed smaller accuracy. The explicit squared-logarithm bound is stated on PDF p.12 immediately after Theorem 2.34.

Formalization Note The measurement uses the frozen general operator-valued POVM on the space of density matrices, and its output distribution is the Born law on $\rho^{\otimes n}$. The extended divergence uses the frozen kernel-containment support guard.

Target

Corollary 1.8

There are absolute constants $C>0$ and $0<\epsilon_0\le 1/2$ with the following property. For every integer dimension $d\ge 1$, supplied integer rank bound $1\le r\le d$, and accuracy $0<\epsilon\le\epsilon_0$, one can choose a copy count $n\ge 0$ and a lawful collective measurement on $n$ independent identical copies of a state, with a density matrix as its classical outcome, such that

$$n\le C\frac{rd}{\epsilon}\left(\ln\frac{d}{\epsilon}\right)^2,\qquad \Pr_{\widehat\rho\sim\mathcal M(\rho^{\otimes n})}\!\left[S(\rho\Vert\widehat\rho)\le\epsilon\right]\ge 0.99.$$

The probability guarantee holds for every unknown positive semidefinite $d\times d$ matrix $\rho$ of trace one and rank at most $r$. The measurement is chosen using only $d,r,\epsilon$, before $\rho$. Here $S$ is Umegaki quantum relative entropy with natural logarithms: $S(\rho\Vert\sigma)=\operatorname{Tr}(\rho\ln\rho-\rho\ln\sigma)$ when $\operatorname{supp}\rho\subseteq\operatorname{supp}\sigma$, and $+\infty$ otherwise; zero-eigenvalue terms use their continuous limits. The estimate may have any rank.

This gives relative entropy tomography with $\widetilde O(rd/\epsilon)$ copies, including singular input states. Larger positive accuracies follow by running at a fixed smaller accuracy. The explicit squared-logarithm bound is stated on PDF p.12 immediately after Theorem 2.34.

Formalization Note The measurement uses the frozen general operator-valued POVM on the space of density matrices, and its output distribution is the Born law on $\rho^{\otimes n}$. The extended divergence uses the frozen kernel-containment support guard.

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 chi-squared tomography and mutual information testing, arXiv:2305.18519v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Improved quantum data analysis establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

There are a universal constant $C>0$ and a copy-count function $n_{\mathrm{TS}}(m,\varepsilon,\delta)$, depending only on the number of tests $m$ and the accuracy and failure parameters $\varepsilon,\delta$, with the following property. For every integer $m\ge1$ and every $0<\varepsilon,\delta<1/2$, write $L=\log(1/\delta)$. Then

$$n_{\mathrm{TS}}(m,\varepsilon,\delta) \le \left\lceil C\,\frac{((\log m)^2+L)L}{\varepsilon^2}\right\rceil.$$

For every dimension $d\ge1$, there is an online quantum protocol that begins with $n_{\mathrm{TS}}(m,\varepsilon,\delta)$ independent, unentangled copies of an unknown state $\rho\in\mathbb C^{d\times d}$, where $\rho$ is positive semidefinite and $\operatorname{tr}\rho=1$, together with a known ancillary state. Observable/threshold pairs $(A_t,\theta_t)$ are then presented in order, with $0\le A_t\le I$ and $\theta_t\in[0,1]$. The protocol is fixed independently of $\rho$ and the stream, and its decision at stage $t$ depends only on the presented prefix and its retained quantum memory. It either passes or halts and selects the current index $t$. Selection asserts $\operatorname{tr}(\rho A_t)>\theta_t-\varepsilon$; after $m$ passes it asserts $\operatorname{tr}(\rho A_i)\le\theta_i$ for all $i$.

For every such state and stream,

$$\Pr\!\left[ \begin{array}{l} \text{the protocol selects }t\text{ with }\operatorname{tr}(\rho A_t)>\theta_t-\varepsilon,\\ \text{or passes on all }m\text{ pairs with }\operatorname{tr}(\rho A_i)\le\theta_i\text{ for every }i \end{array} \right]\ge1-\delta.$$

The stream may depend on preceding public pass responses. No promise that an expectation exceeds a threshold is required. Both kinds of claim are valid in the overlap $\theta_t-\varepsilon<\operatorname{tr}(\rho A_t)\le\theta_t$.

This theorem bounds the sample cost of online search among quantum observables independently of the state dimension.

Formalization Note Natural logarithms and a ceiling express the source's uniform big-O copy bound. Physical Kraus instruments act on the initial tensor power of $\rho$ and an ancillary state; the model uses only copy access. The selected index is zero-based in Lean.

Target

Theorem 1.1

There are a universal constant $C>0$ and a copy-count function $n_{\mathrm{TS}}(m,\varepsilon,\delta)$, depending only on the number of tests $m$ and the accuracy and failure parameters $\varepsilon,\delta$, with the following property. For every integer $m\ge1$ and every $0<\varepsilon,\delta<1/2$, write $L=\log(1/\delta)$. Then

$$n_{\mathrm{TS}}(m,\varepsilon,\delta) \le \left\lceil C\,\frac{((\log m)^2+L)L}{\varepsilon^2}\right\rceil.$$

For every dimension $d\ge1$, there is an online quantum protocol that begins with $n_{\mathrm{TS}}(m,\varepsilon,\delta)$ independent, unentangled copies of an unknown state $\rho\in\mathbb C^{d\times d}$, where $\rho$ is positive semidefinite and $\operatorname{tr}\rho=1$, together with a known ancillary state. Observable/threshold pairs $(A_t,\theta_t)$ are then presented in order, with $0\le A_t\le I$ and $\theta_t\in[0,1]$. The protocol is fixed independently of $\rho$ and the stream, and its decision at stage $t$ depends only on the presented prefix and its retained quantum memory. It either passes or halts and selects the current index $t$. Selection asserts $\operatorname{tr}(\rho A_t)>\theta_t-\varepsilon$; after $m$ passes it asserts $\operatorname{tr}(\rho A_i)\le\theta_i$ for all $i$.

For every such state and stream,

$$\Pr\!\left[ \begin{array}{l} \text{the protocol selects }t\text{ with }\operatorname{tr}(\rho A_t)>\theta_t-\varepsilon,\\ \text{or passes on all }m\text{ pairs with }\operatorname{tr}(\rho A_i)\le\theta_i\text{ for every }i \end{array} \right]\ge1-\delta.$$

The stream may depend on preceding public pass responses. No promise that an expectation exceeds a threshold is required. Both kinds of claim are valid in the overlap $\theta_t-\varepsilon<\operatorname{tr}(\rho A_t)\le\theta_t$.

This theorem bounds the sample cost of online search among quantum observables independently of the state dimension.

Formalization Note Natural logarithms and a ceiling express the source's uniform big-O copy bound. Physical Kraus instruments act on the initial tensor power of $\rho$ and an ancillary state; the model uses only copy access. The selected index is zero-based in Lean.

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

• Improved quantum data analysis, arXiv:2011.10908v4. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Quantum Tomography via Compressed Sensing: Error Bounds, Sample Complexity, and Efficient Estimators establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

There are positive absolute constants $C,C_0,C_1,C'_0,C'_1$ and a function $\eta:\mathbb N\to[0,1]$ with $\eta(n)\to0$ as $n\to\infty$ such that the following holds. Let $d=2^n$, $1\le r\le d$, and $m\ge1$ satisfy $m\ge Crd(\log d)^6$. Sample $P_1,\ldots,P_m$ independently and uniformly, with replacement, from all $d^2$ unsigned tensor Pauli operators, including the identity. On the real space of Hermitian matrices define $\mathcal A(X)_i=\sqrt{d/m}\,\operatorname{Tr}(P_iX)$ and $\mathcal A^*(v)=\sqrt{d/m}\sum_i v_iP_i$.

With probability at least $1-\eta(n)$ over this sampling, simultaneously for every positive semidefinite matrix $\rho$ (without a trace or rank restriction), every $z\in\mathbb R^m$, and $y=\mathcal A(\rho)+z$, both conclusions below hold. Write $\rho_r$ for the spectral truncation retaining the largest $r$ eigenvalues, and $\rho_c=\rho-\rho_r$. All optimizations range over Hermitian matrices and permit nonunique minimizers.

1. For every $\lambda$ satisfying $\|\mathcal A^*(z)\|\le\lambda$, the problem minimizing $\|X\|_{\mathrm{tr}}$ subject to $\|\mathcal A^*(\mathcal A(X)-y)\|\le\lambda$ has a minimizer. Every such minimizer $\widehat\rho_{\mathrm{DS}}$ satisfies

$$\|\widehat\rho_{\mathrm{DS}}-\rho\|_{\mathrm{tr}}\le C_0r\lambda+C_1\|\rho_c\|_{\mathrm{tr}}.$$

2. For every $\mu>0$ satisfying $\|\mathcal A^*(z)\|\le\mu/2$, the problem minimizing $\frac12\|\mathcal A(X)-y\|_2^2+\mu\|X\|_{\mathrm{tr}}$ has a minimizer. Every such minimizer $\widehat\rho_{\mathrm{Lasso}}$ satisfies

$$\|\widehat\rho_{\mathrm{Lasso}}-\rho\|_{\mathrm{tr}}\le C'_0r\mu+C'_1\|\rho_c\|_{\mathrm{tr}}.$$

Here $\|\cdot\|$ is the operator norm, $\|\cdot\|_2$ is the Euclidean vector norm, and $\|X\|_{\mathrm{tr}}=\operatorname{Tr}\sqrt{X^\dagger X}$ is the full trace norm. The two bounds separate noise from the spectral tail and apply to full-rank inputs as well as exactly low-rank ones.

Formalization Note The paper's qualitative “high probability” is represented by a vanishing failure function uniform in $r,m$. Positive Lasso regularization is an explicit correction of the omitted $\mu=0$ domain; the source's regularized recovery argument requires it. This correction, the interpretation of unnormalized PSD inputs, and the qualitative probability convention require independent moderation.

Target

Theorem 1, §II.C

There are positive absolute constants $C,C_0,C_1,C'_0,C'_1$ and a function $\eta:\mathbb N\to[0,1]$ with $\eta(n)\to0$ as $n\to\infty$ such that the following holds. Let $d=2^n$, $1\le r\le d$, and $m\ge1$ satisfy $m\ge Crd(\log d)^6$. Sample $P_1,\ldots,P_m$ independently and uniformly, with replacement, from all $d^2$ unsigned tensor Pauli operators, including the identity. On the real space of Hermitian matrices define $\mathcal A(X)_i=\sqrt{d/m}\,\operatorname{Tr}(P_iX)$ and $\mathcal A^*(v)=\sqrt{d/m}\sum_i v_iP_i$.

With probability at least $1-\eta(n)$ over this sampling, simultaneously for every positive semidefinite matrix $\rho$ (without a trace or rank restriction), every $z\in\mathbb R^m$, and $y=\mathcal A(\rho)+z$, both conclusions below hold. Write $\rho_r$ for the spectral truncation retaining the largest $r$ eigenvalues, and $\rho_c=\rho-\rho_r$. All optimizations range over Hermitian matrices and permit nonunique minimizers.

1. For every $\lambda$ satisfying $\|\mathcal A^*(z)\|\le\lambda$, the problem minimizing $\|X\|_{\mathrm{tr}}$ subject to $\|\mathcal A^*(\mathcal A(X)-y)\|\le\lambda$ has a minimizer. Every such minimizer $\widehat\rho_{\mathrm{DS}}$ satisfies

$$\|\widehat\rho_{\mathrm{DS}}-\rho\|_{\mathrm{tr}}\le C_0r\lambda+C_1\|\rho_c\|_{\mathrm{tr}}.$$

2. For every $\mu>0$ satisfying $\|\mathcal A^*(z)\|\le\mu/2$, the problem minimizing $\frac12\|\mathcal A(X)-y\|_2^2+\mu\|X\|_{\mathrm{tr}}$ has a minimizer. Every such minimizer $\widehat\rho_{\mathrm{Lasso}}$ satisfies

$$\|\widehat\rho_{\mathrm{Lasso}}-\rho\|_{\mathrm{tr}}\le C'_0r\mu+C'_1\|\rho_c\|_{\mathrm{tr}}.$$

Here $\|\cdot\|$ is the operator norm, $\|\cdot\|_2$ is the Euclidean vector norm, and $\|X\|_{\mathrm{tr}}=\operatorname{Tr}\sqrt{X^\dagger X}$ is the full trace norm. The two bounds separate noise from the spectral tail and apply to full-rank inputs as well as exactly low-rank ones.

Formalization Note The paper's qualitative “high probability” is represented by a vanishing failure function uniform in $r,m$. Positive Lasso regularization is an explicit correction of the omitted $\mu=0$ domain; the source's regularized recovery argument requires it. This correction, the interpretation of unnormalized PSD inputs, and the qualitative probability convention require independent moderation.

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 via Compressed Sensing: Error Bounds, Sample Complexity, and Efficient Estimators, arXiv:1205.2300v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Hamiltonian Simulation by Qubitization establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $N,d\ge 1$ be the system and auxiliary dimensions. Let $U$ be a unitary on $\mathbb C^d\otimes\mathbb C^N$, let $G$ be a unitary on $\mathbb C^d$, and write $|g\rangle=G|0\rangle$. Assume that the computed compression $H=(\langle g|\otimes I)U(|g\rangle\otimes I)$ is Hermitian. Access to controlled $U,G$ and their inverses is by black-box queries; arbitrary single- and two-qubit gates are allowed. For real evolution time $t$ and accuracy $0<\varepsilon<1$, define

$$Q(t,\varepsilon)=\min\left\{q\in\mathbb Z_{>0}:\frac{4|t|^q}{q!\,2^q}\le\varepsilon\right\}.$$

There are positive universal constants $c_{\rm q},C_{\rm q},C_{\rm g},C_{\rm f},C_{\rm s}$ and $\varepsilon_0\in(0,1)$ such that, for every $N,d,t,\varepsilon$, one can choose a circuit independently of the particular $U,G$ that uses at most $\lceil\log_2 N\rceil+\lceil\log_2 d\rceil+2$ qubits. For every such oracle pair with Hermitian compression, its successful system operator $K$, obtained by initializing and postselecting all auxiliary wires to zero, satisfies

$$\|K-J_N e^{-iHt}\|_{\rm op}\le\varepsilon,\qquad 1-\|K\psi\|_2^2\le C_{\rm f}\varepsilon \quad\text{for every }\psi\in\mathbb C^N\text{ with }\|\psi\|_2=1,$$

where $J_N:\mathbb C^N\hookrightarrow(\mathbb C^2)^{\otimes\lceil\log_2 N\rceil}$ is the computational-basis embedding. Thus $K$ includes all possible output amplitudes, even on unused system basis labels. If $T$ is the total number of controlled oracle applications, including inverse applications, and $L_2$ is the number of additional two-qubit gates, the same circuit satisfies

$$c_{\rm q}Q(t,\varepsilon)\le T\le C_{\rm q}Q(t,\varepsilon), \qquad L_2\le C_{\rm g}Q(t,\varepsilon)\log d.$$

For $0<\varepsilon\le\varepsilon_0$, the factorial scale also satisfies

$$Q(t,\varepsilon)\le C_{\rm s}\bigl(|t|+\log(1/\varepsilon)\bigr).$$

This is the paper's standard-form simulation procedure and resource guarantee. Its claimed optimality is a worst-case assertion over oracle encodings, supported by the sparse specialization on p.16; the displayed lower query inequality describes the chosen procedure rather than requiring every simulator of each individual Hamiltonian to use that many calls.

Formalization Note Finite-register oracles are extended by the identity on the orthogonal complement of their computational encodings, so neither dimension must be a power of two. The error is the spectral norm of the successful operator itself. The printed $\tau$ in Eq. (1) is undefined in this model; the exact factorial formula fixes $|t|$. The proof's internal accuracy is rescaled to order $\varepsilon^2$ to recover final error $\varepsilon$, and its odd-term sign is reconciled with the headline's $e^{-iHt}$.

Target

Theorem 1, Eq. (1)

Let $N,d\ge 1$ be the system and auxiliary dimensions. Let $U$ be a unitary on $\mathbb C^d\otimes\mathbb C^N$, let $G$ be a unitary on $\mathbb C^d$, and write $|g\rangle=G|0\rangle$. Assume that the computed compression $H=(\langle g|\otimes I)U(|g\rangle\otimes I)$ is Hermitian. Access to controlled $U,G$ and their inverses is by black-box queries; arbitrary single- and two-qubit gates are allowed. For real evolution time $t$ and accuracy $0<\varepsilon<1$, define

$$Q(t,\varepsilon)=\min\left\{q\in\mathbb Z_{>0}:\frac{4|t|^q}{q!\,2^q}\le\varepsilon\right\}.$$

There are positive universal constants $c_{\rm q},C_{\rm q},C_{\rm g},C_{\rm f},C_{\rm s}$ and $\varepsilon_0\in(0,1)$ such that, for every $N,d,t,\varepsilon$, one can choose a circuit independently of the particular $U,G$ that uses at most $\lceil\log_2 N\rceil+\lceil\log_2 d\rceil+2$ qubits. For every such oracle pair with Hermitian compression, its successful system operator $K$, obtained by initializing and postselecting all auxiliary wires to zero, satisfies

$$\|K-J_N e^{-iHt}\|_{\rm op}\le\varepsilon,\qquad 1-\|K\psi\|_2^2\le C_{\rm f}\varepsilon \quad\text{for every }\psi\in\mathbb C^N\text{ with }\|\psi\|_2=1,$$

where $J_N:\mathbb C^N\hookrightarrow(\mathbb C^2)^{\otimes\lceil\log_2 N\rceil}$ is the computational-basis embedding. Thus $K$ includes all possible output amplitudes, even on unused system basis labels. If $T$ is the total number of controlled oracle applications, including inverse applications, and $L_2$ is the number of additional two-qubit gates, the same circuit satisfies

$$c_{\rm q}Q(t,\varepsilon)\le T\le C_{\rm q}Q(t,\varepsilon), \qquad L_2\le C_{\rm g}Q(t,\varepsilon)\log d.$$

For $0<\varepsilon\le\varepsilon_0$, the factorial scale also satisfies

$$Q(t,\varepsilon)\le C_{\rm s}\bigl(|t|+\log(1/\varepsilon)\bigr).$$

This is the paper's standard-form simulation procedure and resource guarantee. Its claimed optimality is a worst-case assertion over oracle encodings, supported by the sparse specialization on p.16; the displayed lower query inequality describes the chosen procedure rather than requiring every simulator of each individual Hamiltonian to use that many calls.

Formalization Note Finite-register oracles are extended by the identity on the orthogonal complement of their computational encodings, so neither dimension must be a power of two. The error is the spectral norm of the successful operator itself. The printed $\tau$ in Eq. (1) is undefined in this model; the exact factorial formula fixes $|t|$. The proof's internal accuracy is rescaled to order $\varepsilon^2$ to recover final error $\varepsilon$, and its odd-term sign is reconciled with the headline's $e^{-iHt}$.

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

• Hamiltonian Simulation by Qubitization, arXiv:1610.06546v3. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Direct Fidelity Estimation from Few Pauli Measurements establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $n\ge 0$ be an integer, $d=2^n$, and $\rho=|\psi\rangle\langle\psi|$ for a normalized $n$-qubit pure state $|\psi\rangle$. Let $\sigma$ be any density matrix on the same register, possibly mixed. For each phase-free Hermitian Pauli product $W_k\in\{I,X,Y,Z\}^{\otimes n}$, write $\chi_\tau(k)=\operatorname{Tr}(\tau W_k)/\sqrt d$. The source's fidelity convention is $F(\rho,\sigma)=\operatorname{Tr}(\rho\sigma)$, the square of root fidelity.

Fix $\varepsilon>0$ and $0<\delta\le1$. Independently draw exactly $\ell=\lceil1/(\varepsilon^2\delta)\rceil$ settings $k_1,\ldots,k_\ell$ with replacement, each with probability $\chi_\rho(k)^2$. Only settings with nonzero target coefficient are drawn. For each draw, measure $W_{k_i}$ separately on

$$m_i=\left\lceil\frac{2\log(2/\delta)}{d\chi_\rho(k_i)^2\ell\varepsilon^2}\right\rceil$$

fresh independent copies of $\sigma$, obtaining Born-rule outcomes $A_{ij}\in\{-1,+1\}$, independent conditional on the settings. Set

$$\widetilde Y=\frac1\ell\sum_{i=1}^{\ell}\frac{\sum_{j=1}^{m_i}A_{ij}}{m_i\sqrt d\,\chi_\rho(k_i)},\qquad m=\sum_{i=1}^{\ell}m_i.$$

Then

$$\Pr\!\left\{F(\rho,\sigma)\in[\widetilde Y-2\varepsilon,\widetilde Y+2\varepsilon]\right\}\ge1-2\delta,$$

and at most $\ell$ distinct observables are measured. The setting-wise and total expected copy costs satisfy

$$\mathbb E[m_i]=\sum_{k:\chi_\rho(k)\ne0}\chi_\rho(k)^2m_i(k) \le1+\frac{2d}{\ell\varepsilon^2}\log\frac2\delta, \qquad \mathbb E[m]\le1+\frac1{\varepsilon^2\delta}+\frac{2d}{\varepsilon^2}\log\frac2\delta.$$

This protocol estimates the fidelity to an arbitrary known pure target using single-copy Pauli measurements. Its copy cost is random; no efficient classical sampling bound is claimed for general targets.

Formalization Note The finite experiment space fixes exactly $\ell$ setting draws and their setting-dependent numbers of outcomes. Its probability weights are products of the target importance law and conditional Pauli outcome laws. The closed interval is not clipped to $[0,1]$.

Target

Fidelity Estimation, equations (3)–(10)

Let $n\ge 0$ be an integer, $d=2^n$, and $\rho=|\psi\rangle\langle\psi|$ for a normalized $n$-qubit pure state $|\psi\rangle$. Let $\sigma$ be any density matrix on the same register, possibly mixed. For each phase-free Hermitian Pauli product $W_k\in\{I,X,Y,Z\}^{\otimes n}$, write $\chi_\tau(k)=\operatorname{Tr}(\tau W_k)/\sqrt d$. The source's fidelity convention is $F(\rho,\sigma)=\operatorname{Tr}(\rho\sigma)$, the square of root fidelity.

Fix $\varepsilon>0$ and $0<\delta\le1$. Independently draw exactly $\ell=\lceil1/(\varepsilon^2\delta)\rceil$ settings $k_1,\ldots,k_\ell$ with replacement, each with probability $\chi_\rho(k)^2$. Only settings with nonzero target coefficient are drawn. For each draw, measure $W_{k_i}$ separately on

$$m_i=\left\lceil\frac{2\log(2/\delta)}{d\chi_\rho(k_i)^2\ell\varepsilon^2}\right\rceil$$

fresh independent copies of $\sigma$, obtaining Born-rule outcomes $A_{ij}\in\{-1,+1\}$, independent conditional on the settings. Set

$$\widetilde Y=\frac1\ell\sum_{i=1}^{\ell}\frac{\sum_{j=1}^{m_i}A_{ij}}{m_i\sqrt d\,\chi_\rho(k_i)},\qquad m=\sum_{i=1}^{\ell}m_i.$$

Then

$$\Pr\!\left\{F(\rho,\sigma)\in[\widetilde Y-2\varepsilon,\widetilde Y+2\varepsilon]\right\}\ge1-2\delta,$$

and at most $\ell$ distinct observables are measured. The setting-wise and total expected copy costs satisfy

$$\mathbb E[m_i]=\sum_{k:\chi_\rho(k)\ne0}\chi_\rho(k)^2m_i(k) \le1+\frac{2d}{\ell\varepsilon^2}\log\frac2\delta, \qquad \mathbb E[m]\le1+\frac1{\varepsilon^2\delta}+\frac{2d}{\varepsilon^2}\log\frac2\delta.$$

This protocol estimates the fidelity to an arbitrary known pure target using single-copy Pauli measurements. Its copy cost is random; no efficient classical sampling bound is claimed for general targets.

Formalization Note The finite experiment space fixes exactly $\ell$ setting draws and their setting-dependent numbers of outcomes. Its probability weights are products of the target importance law and conditional Pauli outcome laws. The closed interval is not clipped to $[0,1]$.

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

• Direct Fidelity Estimation from Few Pauli Measurements, arXiv:1104.4695v3. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.