Quantum Information

Motivation

This mission develops Chapter 5 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

In the hidden subgroup problem (HSP) on a finite group $G$, an algorithm has black-box access to a function $f : G \to S$, where $S$ is a finite set, promised to hide some unknown subgroup $H \le G$:

$$f(x) = f(y) \iff x^{-1}y \in H \qquad (x, y \in G).$$

The goal is to determine $H$. A deterministic classical algorithm is a decision tree: it queries group elements $g_1, g_2, \dots$ adaptively, each query returning $f(g_\ell) \in S$, and finally outputs a subgroup of $G$. It solves the HSP if, for every subgroup $H \le G$ and every $f$ hiding $H$, its output is $H$. Its query count on input $f$ is the number of queries it makes on $f$.

Theorem. There are an absolute constant $c > 0$ and a threshold $N_0$ such that the following holds for every $N \ge N_0$. Let $G$ be a finite group and $S$ a finite set with $|S| \ge |G|$, and suppose $G$ has a family $\mathcal H$ of $N$ distinct subgroups any two of which have only the identity in common, i.e. $H \cap K = \{1\}$ for all distinct $H, K \in \mathcal H$. Then every deterministic classical algorithm that solves the HSP on $G$ (with values in $S$) makes, on some input $f$ hiding some subgroup of $G$,

$$\#\text{queries}(f) \ge c\sqrt{N}.$$

The theorem shows that the HSP is classically hard whenever the group has many trivially intersecting subgroups (for example Simon's problem), in contrast with efficient quantum algorithms for abelian groups.

Formalization Note The algorithm outputs the subgroup itself rather than a generating set, which changes nothing for a query lower bound. The condition $|S| \ge |G|$ makes every subgroup of $G$ hideable; the proof's adversary labels each new query with a fresh value, and with a very small $S$ (say $|S| = 1$) only $H = G$ can be hidden, so the bound would fail. The constants $c$ and $N_0$ are chosen before the group, the set $S$, the family and the algorithm. The threshold $N_0$ is needed because for the trivial group $N = 1$ and no queries are needed. The phrase "whose only common element is the identity" is read pairwise, as in the section's "trivially intersecting subgroups" and as the proof needs when it counts at most $t(t-1)$ non-identity values $g_j^{-1}g_k$ against $N$ subgroups. Read as $\bigcap \mathcal H = \{1\}$, the theorem is false: in the cyclic group of squarefree order $p_1\cdots p_k$, all $2^k$ subgroups intersect trivially, yet $k+1$ queries determine $H$.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Theorem 5.1: Ω(√N) deterministic classical queries for the HSP with N trivially intersecting subgroups.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Andrew Childs, Lecture Notes on Quantum Algorithms, 17 April 2025. https://www.cs.umd.edu/~amchilds/qa/qa.pdf.

Motivation

This mission develops Chapter 21 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

This is the symmetrization lemma of Minsky and Papert.

Let $p \in \mathbb R[x_1, \dots, x_n]$ be multilinear, meaning that every variable has degree at most $1$ in $p$. For $k \in \{0, 1, \dots, n\}$, let

$$P(k) := \mathbb E_{|x| = k}\,[p(x)] = \binom{n}{k}^{-1} \sum_{x \in \{0,1\}^n,\ |x| = k} p(x),$$

where $|x|$ is the Hamming weight of $x$ (its number of 1s). Then there is a univariate polynomial $Q \in \mathbb R[k]$ with $\deg Q \le \deg p$ (total degree) such that $Q(k) = P(k)$ for every $k \in \{0, 1, \dots, n\}$.

Symmetrization reduces questions about multivariate polynomials that represent symmetric Boolean functions, such as parity or OR, to questions about univariate polynomials. Those questions can then be settled by counting sign changes or by Markov's inequality.

Formalization Note The statement that "$P$ is a polynomial" is formalized as agreement with a univariate polynomial on the points $\{0, \dots, n\}$, the only points where $P$ is defined. For these $k$ the average is taken over a nonempty set.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Lemma 21.1: Polynomial method: the acceptance probability of a t-query algorithm is a polynomial of degree at most 2t.
• Lemma 21.2: Symmetrization: the Hamming-weight average of a multilinear polynomial is a polynomial of no larger degree.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Andrew Childs, Lecture Notes on Quantum Algorithms, 17 April 2025. https://www.cs.umd.edu/~amchilds/qa/qa.pdf.

Motivation

This mission develops Chapter 27 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

Fix integers $N,d\ge 0$. There is a single colouring rule $c$, chosen before the graph, that assigns to an ordered pair of vertices $\alpha,\beta\in\{1,\dots,N\}$ a colour $c\big((\alpha,s(\alpha),L_\alpha),(\beta,s(\beta),L_\beta)\big)\in\mathbb N\times\mathbb N$ that depends only on the two vertices, their sides $s(\alpha),s(\beta)$ of the bipartition, and their neighbour lists $L_\alpha,L_\beta$, with the following property.

Let $G$ be an undirected simple graph on the vertex set $\{1,\dots,N\}$ with a bipartition $s:V\to\{\mathrm{left},\mathrm{right}\}$ (every edge joins the two sides) and maximum degree at most $d$, and let $L_v$ be any duplicate-free list of the neighbours of each vertex $v$. Then the map $\{\alpha,\beta\}\mapsto c\big((\alpha,s(\alpha),L_\alpha),(\beta,s(\beta),L_\beta)\big)$ is a proper edge colouring of $G$:

1. it is symmetric on edges, so each edge receives one colour;
2. two distinct edges sharing a vertex receive distinct colours;
3. the number of distinct colours used on the edges of $G$ satisfies

$$\#\{\,c(\alpha,\beta) : \alpha\beta\in E(G)\,\}\le d^2 .$$

In the source the colour of an edge $\alpha\beta$ with $\alpha$ on the left is $(\mathrm{idx}(\alpha,\beta),\mathrm{idx}(\beta,\alpha))$, where $\mathrm{idx}(\alpha,\beta)$ is the position of $\beta$ in the neighbour list of $\alpha$. The lemma is the colouring step of the simulation of sparse Hamiltonians: the edges of each colour class form a matching, whose Hamiltonian is simulated separately before the pieces are combined by a product formula.

Formalization Note The source's "efficiently computable" has no machine model, so the running time of the rule is not formalized; what is kept is that one rule serves every graph and reads only the two endpoints' local data (two neighbour-list queries per edge). Colours are pairs of natural numbers rather than elements of $[d]\times[d]$ so that the rule is total at $d=0$; the bound $d^2$ is on the colours actually used on edges.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Lemma 27.1: Local d²-edge-colouring of a bipartite graph of maximum degree d.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Andrew Childs, Lecture Notes on Quantum Algorithms, 17 April 2025. https://www.cs.umd.edu/~amchilds/qa/qa.pdf.

Motivation

This mission develops Chapter 9 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

This is the classical post-processing step of period finding over the reals (Childs, Lemma 9.1).

Write $\lfloor x \rceil$ for the integer nearest to the real number $x$. Let $r > 0$ be a real number (the period, possibly irrational), let $N$ be a positive integer (the size of the cyclic group $\mathbb Z_N$ used for Fourier sampling), and let $j, j'$ be relatively prime integers with $1 \le j < r$ and $1 \le j' < r$; Fourier sampling returns the integers $\lfloor jN/r \rceil$ and $\lfloor j'N/r \rceil$. If $N \ge 3r^2$, then:

1. the fraction $j/j'$ is one of the convergents of the continued fraction expansion of the rational number

$$\frac{\lfloor jN/r \rceil}{\lfloor j'N/r \rceil};$$

2. the period is recovered to within one unit:

$$\left| r - \left\lfloor \frac{jN}{\lfloor jN/r \rceil} \right\rceil \right| \le 1.$$

Thus, from two samples with coprime multipliers, one learns $j$ from the continued fraction expansion and then an approximation of $r$ to within $1$.

Formalization Note The nearest-integer function is Mathlib's round (ties rounded up; the source leaves ties unspecified and its proof uses only that the rounding error is at most $1/2$). Convergents are Mathlib's Real.convergent, which coincide with the convergents of the regular continued fraction. The ranges $1 \le j, j' < r$ are those the source's proof uses (they come from $\lfloor jN/r \rceil \in \mathbb Z_N$ and the proof's appeals to $j \ge 1$ and $j' < r$); the proof's "$j < j'$ without loss of generality" is not imposed. Under these hypotheses the denominator $\lfloor j'N/r \rceil$ is at least $3$, so no division by zero occurs.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Lemma 9.1: Period finding over the reals: an irrational period from two Fourier samples.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Andrew Childs, Lecture Notes on Quantum Algorithms, 17 April 2025. https://www.cs.umd.edu/~amchilds/qa/qa.pdf.

Motivation

This mission develops Chapter 6 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

This is the correctness statement of the standard quantum algorithm for the Abelian hidden subgroup problem.

Let $G = \mathbb Z_{N_1}\times\cdots\times\mathbb Z_{N_\ell}$ be a finite Abelian group written additively ($N_i \ge 1$), with characters $\chi_g(h) = \prod_{i=1}^{\ell} \omega_{N_i}^{g_i h_i}$, $\omega_N = e^{2\pi i/N}$, and quantum Fourier transform $F_G = F_{N_1}\otimes\cdots\otimes F_{N_\ell}$, $|k\rangle \mapsto |\chi_k\rangle = |G|^{-1/2}\sum_{g\in G}\chi_k(g)|g\rangle$. Let $S$ be a finite set, $H \le G$ a subgroup, and $f : G \to S$ a function hiding $H$:

$$f(g) = f(g') \iff g + H = g' + H.$$

The standard algorithm starts in $|0\rangle|0\rangle$ (registers of dimensions $|G|$ and $|S|$), prepares $|G|^{-1/2}\sum_{g}|g\rangle|0\rangle$, computes $f$ in superposition with one query, $|g\rangle|0\rangle\mapsto|g\rangle|f(g)\rangle$, (measures the second register,) applies $F_G$ to the first register and measures it. For every $g \in G$ the outcome $g$ occurs with probability

$$\Pr[\text{output } g] = \begin{cases} |H|/|G| & \text{if } \chi_g(h) = 1 \text{ for all } h\in H \ (\text{i.e. } \chi_g \in H^\perp),\\ 0 & \text{otherwise.}\end{cases}$$

Since $|H^\perp| = |G|/|H|$, the algorithm samples uniformly from the labels of the elements of $H^\perp$; each sample gives a linear constraint on $H$, which is how the algorithm generalizes Simon's algorithm, period finding and discrete logarithms.

Formalization Note The finite set $S$ is given an arbitrary additive group structure so that computing $f$ is the unitary $|g,b\rangle\mapsto|g,b+f(g)\rangle$, which maps $|g,0\rangle$ to $|g,f(g)\rangle$ as in the source. The intermediate measurement of the second register (step 4) is omitted: it does not change the distribution of the first register, so the output law is the first-register marginal of the state before the final measurement. The source's claim that $H$ can then be found efficiently from few samples is asserted without proof and is not part of this statement.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• §6.2.2: Abelian HSP: the standard algorithm samples uniformly from H^⊥.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Ronald de Wolf, Quantum Computing: Lecture Notes, 27 August 2026. https://homepages.cwi.nl/~rdewolf/qcnotes.pdf.

Motivation

This mission develops Chapter 4 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

Let $U$ be a unitary matrix acting on a finite-dimensional space, and let $|\psi\rangle$ be a unit eigenvector of $U$ with eigenvalue $e^{2\pi i\varphi}$, where $\varphi\in[0,1)$:

$$U|\psi\rangle=e^{2\pi i\varphi}|\psi\rangle .$$

Fix $n\ge0$, put $N=2^n$, and suppose $\varphi$ can be written exactly with $n$ bits, i.e. $2^n\varphi=k$ for a natural number $k$ (necessarily $k<N$). Run phase estimation: start in $|0^n\rangle|\psi\rangle$, apply the quantum Fourier transform $F_N$ to the first $n$ qubits, apply the controlled power $|j\rangle|\psi\rangle\mapsto|j\rangle U^j|\psi\rangle$, then apply $F_N^{-1}=F_N^{*}$ to the first $n$ qubits and measure them in the computational basis (bit strings read most significant bit first). Then

1. after the controlled power the state is $\big(F_N|k\rangle\big)\otimes|\psi\rangle$, i.e. $\frac{1}{\sqrt N}\sum_{j=0}^{N-1}e^{2\pi i\varphi j}|j\rangle|\psi\rangle=F_N|2^n\varphi\rangle|\psi\rangle$;
2. the measurement of the first register yields the outcome $k=2^n\varphi=\varphi_1\dots\varphi_n$ with probability $1$.

This is the exact case of phase estimation, the subroutine underlying Shor's algorithm, quantum counting and many Hamiltonian algorithms.

Formalization Note The final state is the shared phaseEstimationState, $(F_N^{*}\otimes I)\,\Lambda(U)\,(F_N\otimes I)\,|0^n\rangle|\psi\rangle$ with $\Lambda(U)|j\rangle|\phi\rangle=|j\rangle U^{j}|\phi\rangle$; the probability of outcome $k$ on the first register is the marginal $\sum_b|\langle k,b|\cdot\rangle|^2$. The source's general-case claim (an $n$-bit approximation with additive error $O(2^{-n})$ 'with high probability') supplies no probability constant and is not stated.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• §4.5: The n-qubit QFT has an exact circuit of at most n^2 Hadamard, controlled-R_s and swap gates.
• §4.6: Phase estimation returns an exactly n-bit phase with probability 1.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Ronald de Wolf, Quantum Computing: Lecture Notes, 27 August 2026. https://homepages.cwi.nl/~rdewolf/qcnotes.pdf.

Motivation

This mission develops Chapter 8 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

Let $d$ be a squarefree integer with $d \ge 2$, and let $\mathbb Z[\sqrt d] = \{x + y\sqrt d : x, y \in \mathbb Z\}$. For $\xi \in \mathbb Z[\sqrt d]$ write $\xi\mathbb Z[\sqrt d]$ for the principal ideal generated by $\xi$.

For all $\xi, \zeta \in \mathbb Z[\sqrt d]$,

$$\xi\,\mathbb Z[\sqrt d] = \zeta\,\mathbb Z[\sqrt d] \iff \xi = \zeta\epsilon \text{ for some unit } \epsilon \text{ of } \mathbb Z[\sqrt d].$$

Thus the map $\xi \mapsto \xi\mathbb Z[\sqrt d]$ is multiplicatively periodic, with the units as its periods; this periodicity, with period the fundamental unit, underlies the periodic function used in Hallgren's algorithm for Pell's equation.

Formalization Note $\mathbb Z[\sqrt d]$ is Mathlib's ℤ√d, the principal ideal $\xi\mathbb Z[\sqrt d]$ is Ideal.span {ξ}, and a unit is IsUnit. The statement holds also for $\xi = 0$ (both sides then force $\zeta = 0$), so no nonzero hypothesis is added.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Proposition 8.1: Units of Z[√d] are exactly the elements of norm ±1.
• Proposition 8.2: Principal ideals of Z[√d] coincide iff the generators differ by a unit.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Andrew Childs, Lecture Notes on Quantum Algorithms, 17 April 2025. https://www.cs.umd.edu/~amchilds/qa/qa.pdf.

Motivation

This mission develops Chapter 26 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

Let $n,m\ge0$, $\Sigma=\{0,1\}^m$, and let $W$ be a finite workspace. Consider the Hilbert space with computational basis $|x,z,w,y\rangle$, where $x\in[n]$ is the query input, $z\in\Sigma$ the query output, $w\in W$ the workspace and $y\in(\Sigma\cup\{\perp\})^n$ the oracle register. The compressed phase oracle is

$$\Phi=(I\otimes H^{\otimes m}\otimes I\otimes C^{\otimes n})\,\Lambda\,(I\otimes H^{\otimes m}\otimes I\otimes C^{\otimes n}).$$

Here $H$ is the Hadamard gate, $C$ is the compression unitary of §26.1 (it swaps $|\perp\rangle$ and $|\hat 0\rangle$ and fixes $|\hat y\rangle$ for $y\ne0$), and $\Lambda|x,z,w,y\rangle=|x,z\oplus y_x,w,y\rangle$ (the identity when $y_x=\perp$). Let $P$ be the projection onto the basis states whose oracle register contains a zero, i.e. $y_{x^*}=0^m$ for some $x^*$. Then for every state $|\psi\rangle$ (unit vector),

$$\|P\,\Phi|\psi\rangle\|\;\le\;\|P|\psi\rangle\|+\sqrt{\frac{2}{2^m}} .$$

Iterated over $t$ queries, this shows that the compressed-oracle probability of having recorded a zero is $O(t^2/2^m)$. Combined with Lemma 26.1, this gives the $\Omega(2^{m/2})$ query lower bound for unstructured search against a random oracle.

Formalization Note $|\psi\rangle$ is an arbitrary unit vector of the full space; no reachability condition is imposed, and the proof uses none. The register order is $((x,z),w),y$, as in (26.30).

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Lemma 26.1: Standard vs compressed oracle: √p ≤ √p′ + √(k/2^m).
• Fact 26.2: One compressed phase query raises ‖P ψ‖ by at most √(2/2^m).

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Andrew Childs, Lecture Notes on Quantum Algorithms, 17 April 2025. https://www.cs.umd.edu/~amchilds/qa/qa.pdf.

Motivation

This mission develops Chapter 18 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

This is the impossibility of perfect quantum bit commitment.

In de Wolf's model, a quantum bit-commitment protocol is represented by the two joint pure states $|\phi_0\rangle, |\phi_1\rangle \in \mathbb{C}^{d_A} \otimes \mathbb{C}^{d_B}$ that Alice and Bob share at the end of the commit phase when Alice honestly commits to the bit $b = 0$ or $b = 1$. Here $\mathbb{C}^{d_A}$ is Alice's space and $\mathbb{C}^{d_B}$ is Bob's. Restricting to pure states loses no generality. The protocol is perfectly concealing if Bob's reduced density matrix does not depend on $b$, where $\operatorname{Tr}_A$ is the partial trace over Alice's register.

Let $d_A, d_B \ge 0$ and let $|\phi_0\rangle, |\phi_1\rangle$ be unit vectors in $\mathbb{C}^{d_A} \otimes \mathbb{C}^{d_B}$ with

$$\operatorname{Tr}_A\big(|\phi_0\rangle\langle\phi_0|\big) = \operatorname{Tr}_A\big(|\phi_1\rangle\langle\phi_1|\big).$$

Then there is a unitary $U$ on Alice's space $\mathbb{C}^{d_A}$ such that

$$(U \otimes I)\,|\phi_0\rangle = |\phi_1\rangle.$$

So after committing to $0$, Alice can turn the joint state into the honest commitment to $1$ by acting on her own register only. The protocol is then not binding at all, and no quantum bit-commitment protocol is both perfectly concealing and perfectly binding.

Formalization Note Alice's space is indexed by Fin dA and Bob's by Fin dB. The joint space is indexed by Fin dA × Fin dB with Alice's register first. $\operatorname{Tr}_A(|\phi\rangle\langle\phi|)$ is traceLeft (pureDensity phi), and $U \otimes I$ is Matrix.kronecker U 1 with $U$ in Matrix.unitaryGroup. When $d_A = 0$ or $d_B = 0$ no unit vector exists, so the statement is vacuous in those cases, as in the source.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• §18.4: Perfect quantum bit commitment is impossible: perfect concealing implies no binding.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Ronald de Wolf, Quantum Computing: Lecture Notes, 27 August 2026. https://homepages.cwi.nl/~rdewolf/qcnotes.pdf.

Motivation

This mission develops Chapter 24 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

Let $\mathcal H$ be a finite-dimensional complex inner product space and let $\Pi$ and $\Delta$ be orthogonal projections on $\mathcal H$. Put $U = (2\Pi - I)(2\Delta - I)$, a unitary. For $\omega \ge 0$, let $P_\omega$ be the orthogonal projector onto the span of the eigenvectors of $U$ whose eigenvalues are $e^{i\theta}$ with $|\theta| < \omega$. If $|\phi\rangle \in \mathcal H$ is a unit vector with $\Delta|\phi\rangle = 0$, then

$$\|P_\omega \Pi |\phi\rangle\| \le \frac{\omega}{2}.$$

The lemma is the key step in showing that the phase-estimation algorithm built from a dual adversary solution rejects inputs with $f(x) = 0$: the start state has little weight on eigenvectors of small phase.

Formalization Note $\Pi$ and $\Delta$ are given as the orthogonal projections onto submodules $K$ and $L$; $2P - I$ is Mathlib's reflection through the subspace. The eigenvalue set is $\{e^{i\theta} : \theta \in \mathbb{R}, |\theta| < \omega\}$, which is the same set as with $\theta$ restricted to $(-\pi,\pi]$.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Theorem 24.1: The dual of the general adversary bound.
• Theorem 24.2: Adversary bound of a composed function is at most the product.
• Lemma 24.3: Effective spectral gap lemma.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Andrew Childs, Lecture Notes on Quantum Algorithms, 17 April 2025. https://www.cs.umd.edu/~amchilds/qa/qa.pdf.

Motivation

This mission develops Chapter 12 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

In the setting of Claim 3 (a feasible solution $\{u_{xj}, v_{xj}\}$ of the dual SDP for $\mathrm{ADV}^{\pm}(f)$ with objective value $A > 0$, the states $|t^\pm_x\rangle$, $|\psi_y\rangle$, the projectors $\Lambda$, $\Pi_x$ and the unitary $U_x = (2\Pi_x - I)(2\Lambda - I)$), let $\Theta = 1/(1000A)$. For every $x \in D$ there is a vector $|\varphi\rangle$ in the span of the eigenvectors of $U_x$ whose eigenvalues $e^{i\theta}$, $\theta \in (-\pi, \pi]$, satisfy $|\theta| > \Theta$, such that

$$\big\| |t^-_x\rangle - |\varphi\rangle \big\| \le \frac{1}{20} + \frac{1}{2000A}.$$

Equivalently, the component of $|t^-_x\rangle$ in the eigenspaces of $U_x$ with eigenphase $|\theta| \le \Theta$ has norm at most $1/20 + 1/(2000A)$. Together with Claim 3, this lets phase estimation with precision $\Theta/2$ distinguish $|t^+_x\rangle$ from $|t^-_x\rangle$.

Formalization Note The eigenphase $\theta$ is the principal argument Complex.arg, which takes values in $(-\pi, \pi]$; the span of eigenvectors is the supremum of the eigenspaces of $U_x$ over the eigenvalues with $|\arg \mu| > \Theta$. The informal "close" is pinned to the bound the source's proof establishes, and it is stated for every $A > 0$ (the proof's own hypothesis; the source adds "we may assume $A \ge 1$" only to call the bound small).

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• §12.1, Claim 1: Generalized adversary method: the final progress measure is small.
• §12.1, Claim 2: Generalized adversary method: one query changes the progress measure by at most 2 max_i ‖Γ_i‖.
• §12.1, Theorem 2: Generalized (negative-weights) adversary lower bound.
• §12.3, unnumbered: A dual-adversary solution of value A gives an O(A)-query bounded-error algorithm.
• §12.3, Claim 3: |t⁺_x⟩ is within 0.01 of an eigenvalue-1 eigenvector of U_x.
• §12.3, Claim 4: |t⁻_x⟩ is close to the large-eigenphase part of U_x.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Ronald de Wolf, Quantum Computing: Lecture Notes, 27 August 2026. https://homepages.cwi.nl/~rdewolf/qcnotes.pdf.

Motivation

Kramers–Wannier duality was found in 1941 as a map between the high- and low-temperature phases of the two-dimensional Ising model (Kramers–Wannier 1941). In its quantum form it exchanges the transverse field $X_j$ and the nearest-neighbour coupling $Z_{j-1}Z_j$ of the transverse-field Ising chain, and it fixes the critical point. In conformal field theory it is implemented by a topological defect line (Fröhlich–Fuchs–Runkel–Schweigert 2004), the prototypical non-invertible symmetry: its fusion with itself is a sum of operators, not a single invertible one (Shao, TASI lectures 2023).

On a finite periodic chain the duality cannot be a unitary operator, because it maps the $\mathbb Z_2$-even sector to itself and annihilates the odd sector. Seiberg–Shao 2023 and Seiberg–Seifnashri–Shao 2024 wrote the exact lattice operator $\mathsf D$ on the tensor-product Hilbert space $(\mathbb C^2)^{\otimes L}$. They showed that its algebra closes only after the lattice translation is included: $\mathsf D^2=(1+\eta)T^{-1}$. This is a lattice relation that a fusion category does not describe, since the continuum fusion rule $\mathcal N^2=1+\eta$ appears only at low energy. The same identity drives the LSM-type constraint proved in that paper.

Timeline. 1941: Kramers and Wannier find the duality of the 2D Ising model. 2004: Fröhlich, Fuchs, Runkel and Schweigert realise it as a conformal defect. 2016: Aasen–Mong–Fendley construct the lattice defects. 2023–2024: Seiberg, Seifnashri and Shao find the exact operator algebra on the tensor-product Hilbert space, including the translation factor.

Setting

Fix $L\ge1$ qubits on a ring, with site indices in $\mathbb Z/L$ (Fin L with modular arithmetic). A computational-basis state is labelled by a configuration $s=(s_0,\dots,s_{L-1})\in(\mathbb Z/2)^L$ (Config L). Operators are complex $2^L\times2^L$ matrices indexed by configurations (Op L). Write $\operatorname{sgn}(a)=(-1)^a$.

• Pauli operators. $X_j|s\rangle=|s+e_j\rangle$ flips spin $j$ (pauliX), and $Z_j|s\rangle=(-1)^{s_j}|s\rangle$ (pauliZ).
• $\mathbb Z_2$ symmetry. $\eta=\prod_j X_j$ flips every spin (eta).
• Translation. $T|s\rangle=|s'\rangle$ with $s'_k=s_{k-1}$ (transl), so that $TX_jT^{-1}=X_{j+1}$.
• Kramers–Wannier operator (kwD):

$$\langle t|\,\mathsf D\,|s\rangle \;=\; 2^{-L/2}\,(-1)^{\sum_{k} t_k\,(s_k+s_{k+1})}.$$

This explicit formula is the definition used throughout. Relations (1.5) together with $\mathsf D\eta=\mathsf D$ determine $\mathsf D$ up to a scalar, and (1.4) fixes the scalar up to a sign. Every statement below is invariant under $\mathsf D\mapsto-\mathsf D$, so this is the operator of Seiberg–Seifnashri–Shao in that paper's normalisation (footnote 1). Its equality with their matrix-product presentation (2.64) is not formalised here.

Formalization targets

Goal: the non-invertible fusion rule (eqs. (1.4), (2.65), (F.18))

$$\mathsf D^2=(1+\eta)\,T^{-1}\qquad\text{for every }L\ge1 .$$

Milestones

1. Invertible algebra (eqs. (1.1)–(1.3), (2.10), (2.65)): $\eta^2=1$, $T\eta=\eta T$, $T^L=1$, $TX_jT^{-1}=X_{j+1}$, $TZ_jT^{-1}=Z_{j+1}$, $\eta X_j=X_j\eta$, $\eta Z_j=-Z_j\eta$.
2. Duality on $X$ (eq. (1.5)): $\mathsf D X_j=Z_{j-1}Z_j\,\mathsf D$.
3. Duality on $ZZ$ (eq. (1.5)): $\mathsf D Z_{j-1}Z_j=X_{j-1}\,\mathsf D$.
4. Absorbing $\eta$ (eqs. (1.4), (2.65)): $\mathsf D\eta=\eta\mathsf D=\mathsf D$.
5. Translation and adjoint (eq. (2.65), Table 1): $T\mathsf D=\mathsf DT$ and $\mathsf D^\dagger=\mathsf DT$.
6. Non-invertibility (§1.1): $\mathsf D$ is not a unit, and $\ker\mathsf D\neq0$.

Significance

The result. The goal identity is the defining relation of the lattice Kramers–Wannier symmetry. Together with milestones 4–5 it shows that $\mathsf D/\sqrt2$ restricted to the $\eta$-even sector squares to a translation, so $\mathsf D$ is a square root of $T^{-1}$ there. The paper uses this to derive its LSM-type constraint, and also to show that the lattice symmetry is not a fusion category, because the continuum rule $\mathcal N^2=1+\eta$ only emerges at low energy. Milestones 2–3 are the lattice Kramers–Wannier map on $\mathbb Z_2$-invariant operators, so $\mathsf D$ commutes with the critical Ising Hamiltonian $H=-\sum_j(Z_{j-1}Z_j+X_j)$.

Formalizing it. The identities are proved in the physics literature by tensor-network manipulations ((F.14)–(F.18)) and checked numerically, but none of this is machine-checked. This mission produces a reusable Lean setup for qubit chains: Pauli strings on $(\mathbb Z/2)^L$, $\mathbb Z_2$ and translation symmetries, and an exact non-invertible operator with its full operator algebra for every chain length. No mission on the platform or file in Mathlib currently formalizes a non-invertible lattice symmetry.

Difficulty

Each identity is easy to check for a fixed small $L$ by brute force. The content is that it holds for all $L$ at once, on a $2^L$-dimensional space. The difficulty is bookkeeping with periodic indices: sums over $(\mathbb Z/2)^L$ of characters $(-1)^{\langle t,\,\cdot\rangle}$, reindexing $k\mapsto k\pm1$ in Fin L (including $L=1$, where $k+1=k$, and $L=2$, where $k+1=k-1$), and the exact normalisation $2^{-L/2}$, so that the right-hand side carries no stray factor $2^L$. The goal also involves the matrix inverse $T^{-1}$, so a proof must establish that $T$ is invertible rather than rely on Lean's junk value.

Formalization scope

• Representation. Operators are Matrix (Fin L → ZMod 2) (Fin L → ZMod 2) ℂ; products are matrix products; $T^{-1}$ is Mathlib's matrix inverse (transl L)⁻¹; $\dagger$ is conjTranspose. Every theorem assumes [NeZero L], i.e. $L\ge1$.
• Conventions committed to. $Z_j=(-1)^{s_j}$ on basis states, translation to the right ($s'_k=s_{k-1}$), and $\mathsf D$ normalised by $2^{-L/2}$ as in eqs. (1.4)/(2.65). Other conventions (left translation, unnormalised $\mathsf D$) change the statements to $T$ instead of $T^{-1}$ or add a factor $2^L$; the conventions here reproduce the paper's equations verbatim.
• No trivialisation. kwD is an explicit formula, not a hypothesis. The goal fixes both sides completely, and milestone 1 pins the translation convention against eq. (2.10).
• Out of scope. The defect Hamiltonians, the MPO presentation (2.64) itself, the $\mathbb Z_2$- and duality-twisted operators of §§2.3.3–2.3.4, and the LSM constraint of §4.
• Reusable. Pauli operators, translation and $\eta$ on qubit chains; character-sum lemmas over $(\mathbb Z/2)^L$. Contributions of general Mathlib lemmas on Walsh–Hadamard-type sums are welcome.

Selected references

• H. A. Kramers, G. H. Wannier, Statistics of the Two-Dimensional Ferromagnet. Part I, Phys. Rev. 60, 252–262 (1941). doi:10.1103/PhysRev.60.252
• J. Fröhlich, J. Fuchs, I. Runkel, C. Schweigert, Kramers–Wannier duality from conformal defects, Phys. Rev. Lett. 93, 070601 (2004). arXiv:cond-mat/0404051
• D. Aasen, R. S. K. Mong, P. Fendley, Topological Defects on the Lattice I: The Ising model, J. Phys. A 49, 354001 (2016). arXiv:1601.07185
• N. Seiberg, S.-H. Shao, Majorana chain and Ising model – (non-invertible) translations, anomalies, and emanant symmetries, SciPost Phys. 16, 064 (2024). arXiv:2307.02534
• S.-H. Shao, What's Done Cannot Be Undone: TASI Lectures on Non-Invertible Symmetries (2023). arXiv:2308.00747
• Source: N. Seiberg, S. Seifnashri, S.-H. Shao, Non-invertible symmetries and LSM-type constraints on a tensor product Hilbert space, SciPost Phys. 16, 154 (2024). arXiv:2401.12281

Motivation

Projective measurement is usually taught together with state update: an observable is measured, a value is obtained, and the conditional state is assigned. These are two different questions. The first is the prediction of the outgoing ensemble from the incoming ensemble and the measured observable alone, before the outcome is known; the second is the incorporation of the outcome once it is known. The technical brief by G. Carcassi for the Assumptions of Physics collaboration (AoP technical briefs) isolates the first question and treats the measurement as a black-box process that only relates incoming and outgoing ensembles, without committing to a mechanism.

Within this view the standard prediction, the nonselective (Lüders) post-measurement ensemble, admits several characterizations that come from different traditions: the algebraic pinching map, the long-time limit of a dephasing Lindblad equation (open quantum systems, see Lindblad 1976), and a closest-point principle, either in Hilbert–Schmidt distance or in quantum relative entropy (Umegaki 1962). The brief's Theorem 1 states that these characterizations select the same process.

Setting

Fix a finite index set $n$; the Hilbert space is $\mathbb C^n$ and operators are complex $n\times n$ matrices. A density matrix is a positive semidefinite matrix $\rho$ with $\operatorname{tr}\rho=1$. An observable is a Hermitian matrix $X$ with spectral decomposition

$$X=\sum_{x}x\,P_x ,$$

where $x$ ranges over the distinct eigenvalues of $X$ and $P_x$ is the orthogonal projection onto the $x$-eigenspace.

• The pinching of $\rho$ is $\mathcal P_X(\rho)=\sum_x P_x\rho P_x$.
• The dephasing Lindblad equation with vanishing Hamiltonian and jump operator $X$ is $\dfrac{d\rho}{dt}=X\rho X-\tfrac12\{X^2,\rho\}$, $t\ge0$.
• The Hilbert–Schmidt distance is $\|\rho-\sigma\|_{HS}=\big(\operatorname{tr}(\rho-\sigma)^*(\rho-\sigma)\big)^{1/2}$.
• The relative entropy is $D(\rho\|\sigma)=\operatorname{tr}(\rho\log\rho)-\operatorname{tr}(\rho\log\sigma)$ when $\operatorname{supp}\rho\subseteq\operatorname{supp}\sigma$ and $+\infty$ otherwise; the von Neumann entropy is $S(\rho)=-\operatorname{tr}(\rho\log\rho)$.

The spectral equilibration process $\Phi_X$ is an unknown map on density matrices. The brief's four conditions on it are:

• EQ-MEAS: $\Phi_X(\rho)=\sum_xP_x\rho P_x$.
• EQ-LIND: $\Phi_X(\rho)=\lim_{t\to\infty}\rho(t)$ for the Lindblad evolution with $\rho(0)=\rho$.
• EQ-HS: $\Phi_X(\rho)=\operatorname{argmin}\{\|\rho-\sigma\|_{HS}^2:\ \sigma \text{ a density matrix},\ [\sigma,X]=0\}$.
• EQ-KL: $\Phi_X(\rho)=\operatorname{argmin}\{D(\rho\|\sigma):\ \sigma \text{ a density matrix},\ [\sigma,X]=0\}$.

Formalization targets

Goal: Theorem 1 (finite-dimensional form)

For every Hermitian $X$ and every map $\Phi$,

$$\text{EQ-MEAS}\iff\text{EQ-LIND},\qquad \text{EQ-MEAS}\iff\text{EQ-HS},\qquad \text{EQ-MEAS}\iff\text{EQ-KL}.$$

Milestones

The milestones follow the steps of the brief's proof: the block decomposition $\rho=\sum_{x,y}P_x\rho P_y$ (eq. 2); the blockwise solution $P_x\rho(t)P_y=e^{-\frac t2(x-y)^2}P_x\rho(0)P_y$ (eqs. 4–5); convergence $\rho(t)\to\mathcal P_X(\rho)$ (eqs. 9–10) and EQ-LIND $\Leftrightarrow$ EQ-MEAS; the equivalence $[\sigma,X]=0\iff\mathcal P_X(\sigma)=\sigma$; $\mathcal P_X$ preserves density matrices; the Pythagorean identity (eq. 11) and EQ-HS $\Leftrightarrow$ EQ-MEAS; the relative-entropy chain rule (eq. 12); $D(\rho\|\mathcal P_X\rho)=S(\mathcal P_X\rho)-S(\rho)$ (eq. 13); non-negativity and definiteness of $D$; and EQ-KL $\Leftrightarrow$ EQ-MEAS.

Significance

The result says that "projective measurement" can be specified without reference to wave-function collapse: any of the three dynamical or variational descriptions pins down the same input–output map. Downstream, this justifies treating repeatable measurements as equilibration processes whose outputs are fixed points, and treating the outcome-update step as classical conditioning on a mixture.

The mathematics in finite dimension is classical; this mission asks for a machine-checked proof of the equivalence in Lean 4 with Mathlib. A complete development produces reusable pieces: spectral projections and the pinching map for Hermitian matrices, explicit solutions and asymptotics of a dephasing Lindblad semigroup, and an extended-real relative entropy with Klein's inequality.

Difficulty

The Hilbert–Schmidt part is linear algebra once block-diagonality is in place. The Lindblad part requires uniqueness of solutions of a linear matrix ODE on the closed half-line, to transfer the explicit blockwise formula to an arbitrary solution. The relative-entropy part is the most delicate: it needs the interaction between the functional-calculus logarithm and block structure ($\log\sigma$ is block diagonal when $\sigma$ commutes with $X$), the support conventions that make $D$ take the value $+\infty$, and Klein's inequality with its equality case for matrices, which the development must supply if the library does not already provide it.

Formalization scope

• Finite dimension only. The Hilbert space is $\mathbb C^n$ for a finite type $n$, so all observables are bounded with pure point spectrum and every density matrix has finite entropy. The brief also covers separable infinite-dimensional spaces and unbounded observables (where Condition [B]FINENT is a genuine restriction); that regime is not part of this mission.
• Spectral data. $P_x$ is built from Mathlib's eigen-decomposition of a Hermitian matrix and is defined for every real $x$ (zero when $x$ is not an eigenvalue); the pinching sums over the finite set of distinct eigenvalues.
• Lindblad solutions. A solution is any function $\mathbb R\to M_n(\mathbb C)$ with the given initial value whose derivative within $[0,\infty)$ satisfies the equation for $t\ge0$. EQ-LIND requires existence of a solution and convergence of every solution, so it cannot hold vacuously.
• Argmin. "$\Phi(\rho)=\operatorname{argmin}$" is encoded as "$\Phi(\rho)$ is a feasible minimizer"; uniqueness is a consequence proved by the theorem, not an assumption.
• Logarithm and relative entropy. $\log$ is the continuous functional calculus applied to Real.log (so $\log0=0$, i.e. the logarithm on the support); $D$ takes values in the extended reals and equals $+\infty$ unless $\ker\sigma\subseteq\ker\rho$.
• Convergence is in the entrywise topology, which coincides with the trace-norm and Hilbert–Schmidt topologies in finite dimension.

Contributions of general-purpose lemmas (Klein's inequality, uniqueness for linear ODEs on half-lines, properties of pinching) are welcome as separate theorems.

Selected references

• G. Carcassi (Assumptions of Physics collaboration), Projective measurements are equilibration processes, AoP Technical Brief 017. https://assumptionsofphysics.org/resources/briefs
• G. Lindblad, On the generators of quantum dynamical semigroups, Comm. Math. Phys. 48 (1976) 119–130. https://doi.org/10.1007/BF01608499
• H. Umegaki, Conditional expectation in an operator algebra. IV. Entropy and information, Kodai Math. Sem. Rep. 14 (1962) 59–85. https://doi.org/10.2996/kmj/1138844604

Motivation

The parity function tests whether a shallow quantum circuit can combine information from all input bits. Polynomially many ancillary qubits make the measured-output formulation substantially stronger than a restriction to clean final registers. The pinned manuscript supplies the research context.

Setting

Allowed gates are arbitrary one-qubit unitaries and Toffoli gates with finitely many controls. Gates within a layer have disjoint supports. Inputs occupy the first n qubits, with zero ancillas.

Formalization target

The selected goal is OAI.QAC.parity_lower_bound_polynomial_size. Its central assertion is

$$\exists x\in\{0,1\}^n:\quad P(\mathrm{output}=\mathrm{parity}(x))<2/3.$$

The theorem states that, for any positive integers d, k and C, there is a threshold n₀ such that for every n ≥ n₀ and every total qubit count N with n ≤ N ≤ C(n+1)^k, the following holds. Take any circuit given as a list of at most d physical layers on N qubits, where a layer is a list of gates with pairwise disjoint supports and each gate is either a one-qubit unitary on a single qubit or a Toffoli gate with an arbitrary finite set of control qubits and a target outside that set (flipping the target exactly when all controls are 1). The circuit's matrix is the product of the layer matrices, with the first layer acting first. For every choice of output qubit out among the N qubits, there exists an n-bit input x such that successProbability, the total Born probability over all final computational-basis strings y whose out-th bit equals the parity (sum mod 2) of x, is strictly less than 2/3. Here the input state is x placed on the first n qubits with all remaining qubits set to 0, and the remaining qubits are summed over with no requirement that they be clean. So fixed-depth circuits with polynomially many qubits cannot compute parity with worst-case success probability at least 2/3. The theorem is admitted in the source (proof is sorry).

Significance and status

The published goal fixes success threshold 2/3 and positive integer depth, polynomial exponent and coefficient. It does not state the manuscript's full range of positive advantages. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The bound covers arbitrary gates, all choices of output qubit and polynomially many total qubits. Discarded registers can retain unrestricted garbage.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, Regular trajectories, pruning and quantum parity, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation: the classical capacity of a thermal qubit channel

A quantum channel models how a physical system, used to carry information, is corrupted by its environment. The classical capacity of a channel is the largest rate, in bits per use, at which classical messages can be sent with vanishing error when the sender may encode into arbitrary — possibly entangled — states of many uses and the receiver may measure all outputs jointly. The Holevo–Schumacher–Westmoreland coding theorem (Holevo 1998; Schumacher–Westmoreland 1997) expresses this capacity as a regularized limit of the Holevo information over ever larger blocks of uses. Since Holevo information is not additive in general (Hastings 2009), computing the capacity of any specific channel requires a channel-specific additivity argument, and exact formulas are known only for a few families.

Generalized amplitude damping is the standard model of a qubit relaxing toward a thermal state: it loses or gains an excitation with probabilities set by a damping strength $\gamma$ and a stationary excited population $\nu$, and its coherences decay. It is one of the basic noise models of quantum information theory.

Background timeline

• 1996–1998 — Coding theorems for pure and mixed signals establish the regularized capacity formula (Hausladen et al. 1996; Schumacher–Westmoreland 1997; Holevo 1998).
• 2002 — Additivity for unital qubit channels (King 2002) and for entanglement-breaking channels (Shor 2002) settles some parameter regions of the family; Bennett, Shor, Smolin and Thapliyal describe the two-signal optimization for ordinary amplitude damping (BSST 2002).
• 2005 — Giovannetti and Fazio derive the optimized one-use expression for ordinary amplitude damping (Giovannetti–Fazio 2005); Berry studies qubit channels achieving capacity with two states (Berry 2005).
• 2007 — Hou and Fang characterize the one-use Holevo optimum of the generalized channel (Hou–Fang 2007).
• 2009 — Hastings shows that Holevo information is not additive in general (Hastings 2009).
• 2018 — Leditzky, Kaur, Datta and Wilde note that the unrestricted classical capacity of amplitude damping had not been determined (LKDW 2018).
• 2020 — Khatri, Sharma and Wilde collect upper bounds for the generalized family (KSW 2020).
• 2026 — Tang, Zhu, Bai and Wang prove additivity for qubit channels with a pure output, including ordinary amplitude damping (arXiv:2609.28592); Fang gives a close converse bound for the generalized family (arXiv:2609.14621).
• 2026 — An OpenAI preprint, Classical capacity and entropy inequalities for generalized amplitude damping (OpenAI Math Release, September 24, 2026), claims the capacity for all $(\gamma,\nu)\in[0,1]^2$. The preprint has not been peer reviewed, and its results are not formally verified.

Setting

For $\gamma,\nu\in[0,1]$ the generalized amplitude-damping channel acts on a qubit density matrix by

$$\mathcal A_{\gamma,\nu}\begin{pmatrix}1-q&z\\\bar z&q\end{pmatrix}=\begin{pmatrix}1-t&\sqrt{1-\gamma}\,z\\\sqrt{1-\gamma}\,\bar z&t\end{pmatrix},\qquad t=(1-\gamma)q+\gamma\nu,$$

and $n$ independent uses act as $\mathcal A_{\gamma,\nu}^{\otimes n}$ on $2^n\times2^n$ matrices. With $S(P)=-\operatorname{Tr}P\ln P$, the Holevo information in bits is

$$\chi(\mathcal N)=\frac1{\ln2}\sup_{\{q_a,\rho_a\}}\Bigl\{S\Bigl(\sum_aq_a\mathcal N(\rho_a)\Bigr)-\sum_aq_aS(\mathcal N(\rho_a))\Bigr\},$$

over all finite ensembles of input states (entangled across uses when $\mathcal N=\mathcal A^{\otimes n}$). The classical capacity $C(\mathcal N)$ is the supremum of rates $R$ for which there are $n$-use codes — arbitrary input states for each of $M_n$ equiprobable messages and one joint measurement of all outputs — with average error tending to zero and $\liminf_n n^{-1}\log_2M_n\ge R$; there is no shared entanglement or feedback. Write $h$ for binary entropy in nats, $g(u)=h\bigl((1+\sqrt{1-4u})/2\bigr)$ and $v_{\gamma,\nu}(p)=\gamma\nu(1-\nu)+\gamma(1-\gamma)(p-\nu)^2$.

Formalization targets

Goal: additivity and capacity formula (Theorem 1.1)

For all $\gamma,\nu\in[0,1]$ and every $n\ge1$,

$$\chi(\mathcal A_{\gamma,\nu}^{\otimes n})=n\,\chi(\mathcal A_{\gamma,\nu})=\frac n{\ln 2}\max_{0\le p\le1}\bigl\{h((1-\gamma)p+\gamma\nu)-g(v_{\gamma,\nu}(p))\bigr\},$$

the maximum is attained, $C(\mathcal A_{\gamma,\nu})=\chi(\mathcal A_{\gamma,\nu})$, and for every maximizer $p$ the equiprobable independent products of the two signals $\phi_\pm=\sqrt{1-p}\,|0\rangle\pm\sqrt p\,|1\rangle$ attain $\chi(\mathcal A_{\gamma,\nu}^{\otimes n})$ at every block length. The goal is published on the platform with status Open.

Significance

The result itself. The theorem gives a closed one-variable formula for the classical capacity of every generalized amplitude-damping channel, removing the regularization over block lengths: entangled input signals across uses give no advantage, and a simple product code with two signals per use is optimal. This settles the ordinary amplitude-damping case listed as open by LKDW 2018 and extends beyond the pure-output criterion of Tang et al. to the thermal regime, where the channel has no pure output. The source further proves additivity of Holevo capacity, minimum output entropy and classical capacity when the channel is used in parallel with any finite-dimensional partner channel (Corollary 1.2); that corollary is not part of this goal.

Formalizing it. The goal ties together an operational capacity (codes and error probabilities), an entropic quantity (a supremum over unrestricted ensembles on $2^n$-dimensional matrices), and a scalar optimization. A machine-checked proof would certify both the matrix entropy inequality at the heart of the argument and the converse direction of the coding theorem. Mathlib does not currently contain quantum channel capacity theory, so the definitions here are new infrastructure.

Difficulty

Optimizing a single use gives a lower bound on capacity; the difficulty is the matching upper bound for all $n$ simultaneously, where an input may be entangled across all uses. Holevo additivity is false for general channels, so no abstract argument applies, and for interior thermal occupation $0<\nu<1$ with $\gamma>0$ the channel has no pure output, which rules out the recent pure-output criterion. The proof needs a lower bound on the entropy of the output of an arbitrary entangled block input, i.e. a matrix entropy inequality for $2\times2$ block-structured states that is tight on product inputs. Identifying the capacity with the regularized Holevo quantity also requires the full coding theorem and a Fano-type converse.

Formalization scope

• Matrices are indexed by Fin n → Fin 2; the $n$-use channel is given by tensor products of the four standard Kraus operators of generalized amplitude damping, which reproduce the displayed action exactly.
• Entropy is Tr (cfc negMulLog P) (nats, $0\ln0=0$); Holevo values are divided by $\ln 2$ (bits). holevo γ ν n is the sSup over all finite ensembles of arbitrary $2^n$-dimensional states, with no product or purity restriction.
• capacity is the sSup of operationally achievable rates: codes with any positive number of messages, arbitrary state encodings, an arbitrary POVM decoder, average error tending to $0$, and the liminf rate condition. It is defined operationally, not by regularization, so the identity $C=\chi$ includes the coding theorem.
• The scalar objective uses Real.binEntropy (nats); the maximizer is over $p\in[0,1]$. The final clause also asserts that the phase-product signals are states.
• Parameters range over the closed square $[0,1]^2$, including boundary cases (identity channel at $\gamma=0$, full replacement at $\gamma=1$).
• Needed infrastructure: matrix entropy and its concavity, CPTP maps and Kraus representations, Holevo's bound, Fano's inequality, the HSW coding theorem for finite ensembles, and Fekete-type superadditivity. These are reusable for any quantum Shannon-theory mission.

Selected references

• P. Hausladen, R. Jozsa, B. Schumacher, M. Westmoreland, W. K. Wootters, Classical information capacity of a quantum channel, Phys. Rev. A 54 (1996), 1869–1876. https://doi.org/10.1103/PhysRevA.54.1869
• B. Schumacher and M. D. Westmoreland, Sending classical information via noisy quantum channels, Phys. Rev. A 56 (1997), 131–138. https://doi.org/10.1103/PhysRevA.56.131
• A. S. Holevo, The capacity of the quantum channel with general signal states, IEEE Trans. Inf. Theory 44 (1998), 269–273. https://doi.org/10.1109/18.651037
• C. King, Additivity for unital qubit channels, J. Math. Phys. 43 (2002), 4641–4653. https://doi.org/10.1063/1.1500791
• P. W. Shor, Additivity of the classical capacity of entanglement-breaking quantum channels, J. Math. Phys. 43 (2002), 4334–4340. https://doi.org/10.1063/1.1498000
• C. H. Bennett, P. W. Shor, J. A. Smolin, A. V. Thapliyal, Entanglement-assisted capacity of a quantum channel and the reverse Shannon theorem, IEEE Trans. Inf. Theory 48 (2002), 2637–2655. https://doi.org/10.1109/TIT.2002.802612
• V. Giovannetti and R. Fazio, Information-capacity description of spin-chain correlations, Phys. Rev. A 71 (2005), 032314. https://doi.org/10.1103/PhysRevA.71.032314
• D. W. Berry, Qubit channels that achieve capacity with two states, Phys. Rev. A 71 (2005), 032334. https://doi.org/10.1103/PhysRevA.71.032334
• L.-Z. Hou and M.-F. Fang, The Holevo capacity of a generalized amplitude-damping channel, Chinese Physics 16 (2007), 1843–1847. https://doi.org/10.1088/1009-1963/16/7/006
• M. B. Hastings, Superadditivity of communication capacity using entangled inputs, Nature Physics 5 (2009), 255–257. https://doi.org/10.1038/nphys1224
• F. Leditzky, E. Kaur, N. Datta, M. M. Wilde, Approaches for approximate additivity of the Holevo information of quantum channels, Phys. Rev. A 97 (2018), 012332. https://doi.org/10.1103/PhysRevA.97.012332
• S. Khatri, K. Sharma, M. M. Wilde, Information-theoretic aspects of the generalized amplitude-damping channel, Phys. Rev. A 102 (2020), 012401. https://doi.org/10.1103/PhysRevA.102.012401
• Z. Tang, C. Zhu, G. Bai, X. Wang, Classical capacity and entanglement cost of the amplitude damping channel, arXiv:2609.28592 (2026). https://arxiv.org/abs/2609.28592v1
• K. Fang, A pretty-tight converse on the classical capacity of generalized amplitude-damping channels, arXiv:2609.14621 (2026). https://arxiv.org/abs/2609.14621v1
• OpenAI, Classical capacity and entropy inequalities for generalized amplitude damping, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 3). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Classical-capacity-and-entropy-inequalities-for-generalized-amplitude-damping-September-24-2026/paper.pdf

Motivation

Parity, $\mathrm{PARITY}_n(x)=x_1\oplus\cdots\oplus x_n$, is the standard test of whether a shallow circuit can aggregate information from all of its inputs. Classically, constant-depth circuits with unbounded fan-in AND/OR gates ($\mathsf{AC}^0$) cannot compute it: Furst, Saxe and Sipser (Math. Systems Theory 1984) and Ajtai (APAL 1983) proved superpolynomial lower bounds, and Håstad's switching lemma gave nearly optimal exponential ones (STOC 1986). The quantum analogue $\mathsf{QAC}^0$ allows arbitrary one-qubit unitaries and Toffoli gates of unbounded arity, but gates in one layer must act on disjoint qubits, so a wire cannot control many simultaneous gates. Moore (arXiv:quant-ph/9903046, 1999) showed that coherent parity and quantum fanout are equivalent under Hadamard conjugation, and conjectured that neither is in $\mathsf{QAC}^0$. Because fanout makes constant-depth quantum circuits very powerful (Høyer–Špalek, ToC 2005), whether $\mathrm{PARITY}\notin\mathsf{QAC}^0$ has been a central question about shallow quantum computation.

Background

• 1999 — Moore introduces the quantum circuit classes and the parity/fanout conjecture.
• 2002 — Green, Homer, Moore and Pollett develop quantum counting classes and modular-gate equivalences (QIC 2002).
• 2006 — Fang, Fenner, Green, Homer and Zhang: depth $\Omega(\log(n/(a+1)))$ for exact clean parity with $a$ ancillas (QIC 2006).
• 2020–2021 — Padé, Fenner, Grier and Thierauf rule out exact clean parity at entangling depth two (arXiv:2005.12169); Rosenthal bounds approximate parity unitaries (ITCS 2021).
• 2024–2025 — Pauli-spectrum lower bounds with restricted ancillas (Nadimpalli, Parham, Vasconcelos, Yuen, STOC 2024); no fixed parity advantage with barely superlinear ancillas (Anshu, Dong, Ou, Yao, STOC 2025), extended by Dong, Ou and Yao (arXiv:2510.00593).
• 2026 — Joshi, Tal, Vasconcelos and Wright: exact parity lower bounds at entangling depth three without size restriction (STOC 2026); Gretta, Gupta and Joshi relate the question to Fourier concentration (arXiv:2604.02793).
• September 2026 — Two OpenAI preprints claim the lower bound for every fixed depth and every polynomial number of qubits, by independent arguments: product-projection localization (source) and regular trajectories with pruning (source).

This mission asks for a formal proof of the parity lower bound stated as Theorem 1 of an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Setting

A circuit acts on $N$ qubits, with state space $(\mathbb C^2)^{\otimes N}$ and computational basis indexed by bit strings $y\in\{0,1\}^N$. The allowed gates are arbitrary one-qubit unitaries and generalized Toffoli gates $|z_1,\dots,z_t,b\rangle\mapsto|z_1,\dots,z_t,b\oplus z_1\cdots z_t\rangle$ on distinct control and target qubits. A layer is a set of gates with pairwise disjoint supports, and a depth-$d$ circuit is a product $W=L_d\cdots L_1$ of at most $d$ layers. Gates and their complex entries may depend on $n$ but not on the input.

On input $x\in\{0,1\}^n$ with $n\le N$, the circuit starts in $|x\rangle\otimes|0\rangle^{\otimes(N-n)}$. One designated output qubit is measured in the computational basis; all other qubits are discarded in arbitrary states, and the input need not be preserved. The success probability on $x$ is

$$\Pr[\text{output}=\mathrm{PARITY}_n(x)]=\sum_{y:\ y_{\mathrm{out}}=\mathrm{PARITY}_n(x)}\bigl|\langle y|W|x,0\rangle\bigr|^2 .$$

A circuit computes parity with worst-case advantage $\varepsilon$ if this probability is at least $1/2+\varepsilon$ for every $x$.

Formalization targets

Goal: the parity lower bound (Theorem 1, p. 1)

Fix an integer $d\ge0$, a real $c\ge1$ and $0<\varepsilon\le1/2$. Then for all sufficiently large $n$, for every $N$ with $n\le N\le n^c$, every circuit of depth at most $d$ on $N$ qubits and every choice of output qubit, there is an input $x\in\{0,1\}^n$ with

$$\Pr[\text{output}=\mathrm{PARITY}_n(x)]<\tfrac12+\varepsilon .$$

With $\varepsilon=1/6$ this is the usual bounded-error statement $\mathrm{PARITY}\notin\mathsf{QAC}^0$ in the measured-output model.

Significance

The result itself. It answers Moore's question for every fixed depth and every polynomial bound on the total number of qubits, with arbitrary final garbage and any fixed positive advantage, whereas earlier results fixed the entangling depth or restricted the number of ancillas. Through Hadamard conjugation it also excludes constant-depth polynomial-size coherent fanout. The preprint derives further consequences (Section 7): state-preparation obstructions (Corollary 8, p. 14), a qualitative quantum LMN-type Fourier tail bound (Corollary 9, p. 16), and, via reductions of Xu and Li, lower bounds for majority and other symmetric functions (Corollaries 10–11, pp. 17–18). The structural Theorem 2 (p. 5), localization of conjugated product projections, is of independent interest.

Formalizing it. The statement is elementary (finite matrices, Born probabilities) while the proof is a two-level induction with polynomial approximation, so a formal proof would give a fully checked circuit lower bound in quantum complexity, an area with few machine-checked results. A companion OpenAI preprint gives an independent proof by regular trajectories and pruning.

Difficulty

Light-cone arguments fail at once: a single Toffoli gate may touch every qubit, so after one layer an output can depend on all inputs. Spectral and Pauli-weight methods previously needed ancilla bounds such as $\tilde O(n^{1+2^{-d}})$. The preprint's route controls transitions from a product condition to states with many mismatches, $\bigl\|[M\ge N^t]\,U\,[D=0]\,U^\dagger\,[M=0]\bigr\|\le e^{-N^s}$ for all fixed $0\le s<t$ (Theorem 2, p. 5). The obstacle is that reflection expansions cost exponentially in the projection's support, and low-degree polynomial surrogates for a product projection are accurate only at low mismatch counts; the uncontrolled high-count error is handled by a second induction on thresholds that exchanges the roles of the two counts.

Formalization scope

• Word N := Fin N → Fin 2; operators are complex matrices indexed by words. Gate.local q u is a one-qubit unitary tensored with identities; Gate.toffoli controls target is the permutation matrix flipping the target when all controls are $1$ (an empty control set gives a NOT gate, itself a one-qubit unitary).
• PhysicalLayer N is a list of gates whose supports are pairwise disjoint; its matrix is the product of the gate matrices. physicalCircuitMatrix layers applies the layers in list order (rightmost matrix acts first).
• inputWord x pads $x$ with zeros; successProbability W out x sums $|W_{y,(x,0)}|^2$ over all $y$ whose output bit equals the parity of $x$, so final garbage is unrestricted.
• The output qubit out : Fin N is arbitrary, including an input qubit. The quantifier order is: depth, size bound and advantage fixed first; then a threshold $n_0$; then every $n\ge n_0$, every $N$ in range, every circuit and every output qubit.
• No intermediate measurement, postselection or fanout gate is in the model; the statement is a pure statement about unitary matrices, with no complexity-class machinery.
• ParityStatement takes the size bound as a real exponent: $N\le n^c$ with $c\ge1$ real, $n\le N$, and depth layers.length ≤ d with $d\ge0$, exactly as in Theorem 1. Its conclusion is the negation of "for every $x$, success $\ge 1/2+\varepsilon$".

Welcome contributions: a reusable Lean model of unitary circuits on qubits, spectral projections of commuting count operators, and Chebyshev-type polynomial approximation with coefficient bounds (Lemma 3, p. 6).

Selected references

• OpenAI, Product-projection localization and the QAC0 parity lower bound, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Product-projection-localization-and-the-QAC0-parity-lower-bound-September-24-2026/paper.pdf
• OpenAI, Regular trajectories, pruning and quantum parity, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Regular-trajectories-pruning-and-quantum-parity-September-24-2026/paper.pdf
• C. Moore, Quantum circuits: fanout, parity, and counting, arXiv:quant-ph/9903046 (1999). https://arxiv.org/abs/quant-ph/9903046v3
• M. Furst, J. B. Saxe, M. Sipser, Parity, circuits, and the polynomial-time hierarchy, Math. Systems Theory 17 (1984), 13–27. https://doi.org/10.1007/BF01744431
• M. Ajtai, $\Sigma^1_1$-formulae on finite structures, Ann. Pure Appl. Logic 24 (1983), 1–48. https://doi.org/10.1016/0168-0072(83)90038-6
• J. Håstad, Almost optimal lower bounds for small depth circuits, STOC 1986. https://doi.org/10.1145/12130.12132
• F. Green, S. Homer, C. Moore, C. Pollett, Counting, fanout and the complexity of quantum ACC, QIC 2 (2002). https://doi.org/10.26421/QIC2.1-3
• P. Høyer, R. Špalek, Quantum fan-out is powerful, Theory of Computing 1 (2005). https://doi.org/10.4086/toc.2005.v001a005
• M. Fang, S. Fenner, F. Green, S. Homer, Y. Zhang, Quantum lower bounds for fanout, QIC 6 (2006). https://doi.org/10.26421/QIC6.1-3
• G. Rosenthal, Bounds on the QAC0 complexity of approximating parity, ITCS 2021. https://doi.org/10.4230/LIPIcs.ITCS.2021.32
• S. Nadimpalli, N. Parham, F. Vasconcelos, H. Yuen, On the Pauli spectrum of QAC0, STOC 2024. https://doi.org/10.1145/3618260.3649662
• M. R. Joshi, A. Tal, F. Vasconcelos, J. Wright, Improved lower bounds for QAC0, STOC 2026. https://doi.org/10.1145/3798129.3800922
• L. Gretta, M. Gupta, M. R. Joshi, Parity ∉ QAC0 ⟺ QAC0 is Fourier-concentrated, arXiv:2604.02793 (2026). https://arxiv.org/abs/2604.02793v2