Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Fixed-point quantum search with an optimal number of queries establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be integers, , and . Let be a unitary on qubits, , and let be a unit vector with . The supplied target oracle is
where flips the additional qubit: flips it on and acts identically on the orthogonal complement.
Define for , and for . For , set
With , , and , define ; the empty product is .
There is an absolute constant such that, for each , a single circuit template chosen before implements up to a global phase on every data vector, returning its one ancillary qubit to . It uses exactly plain queries and total calls to or , no controlled oracle calls, and at most elementary gates from arbitrary single-qubit unitaries and CNOT. Preparation of the supplied input is outside these counts. Oracle calls are charged separately from elementary gates.
Writing for the Chebyshev polynomial of the first kind, both the constructed sequence and this physical circuit have target success probability
In particular,
The guaranteed interval gives fixed-point amplitude amplification with an adjustable failure tolerance and exactly target-oracle queries. The endpoints , , , and are included.
Formalization Note The joint overlap with is the physical success probability because the ancillary qubit is returned clean. The endpoint uses the continuous limiting polynomial confirmed on PDF p.4, rather than division by zero.
Let be integers, , and . Let be a unitary on qubits, , and let be a unit vector with . The supplied target oracle is
where flips the additional qubit: flips it on and acts identically on the orthogonal complement.
Define for , and for . For , set
With , , and , define ; the empty product is .
There is an absolute constant such that, for each , a single circuit template chosen before implements up to a global phase on every data vector, returning its one ancillary qubit to . It uses exactly plain queries and total calls to or , no controlled oracle calls, and at most elementary gates from arbitrary single-qubit unitaries and CNOT. Preparation of the supplied input is outside these counts. Oracle calls are charged separately from elementary gates.
Writing for the Chebyshev polynomial of the first kind, both the constructed sequence and this physical circuit have target success probability
In particular,
The guaranteed interval gives fixed-point amplitude amplification with an adjustable failure tolerance and exactly target-oracle queries. The endpoints , , , and are included.
Formalization Note The joint overlap with is the physical success probability because the ancillary qubit is returned clean. The endpoint uses the continuous limiting polynomial confirmed on PDF p.4, rather than division by zero.
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.
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.
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.
Generalized Quantum Signal Processing establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let and let be prescribed ordinary complex polynomials. For real angles define
For any positive integer and any unitary matrix , put , with the control qubit as the first tensor factor, and
When , this is just the initial rotation tensored with . There exist real vectors and a real , chosen independently of and , such that
if and only if
Here and denote polynomial evaluation at the matrix , and the stars leave the second-column blocks unspecified. The zero polynomial satisfies the degree bound.
This theorem characterizes exactly the polynomial pairs synthesized by forward signal applications and rotations; it imposes no real-coefficient or parity restriction.
Formalization Note Universal finite-dimensional unitary realization expresses the polynomial identity used by the proof; in particular, it includes every scalar unitary . The rotation is the matrix printed in equation (6), without a determinant-one constraint.
Let and let be prescribed ordinary complex polynomials. For real angles define
For any positive integer and any unitary matrix , put , with the control qubit as the first tensor factor, and
When , this is just the initial rotation tensored with . There exist real vectors and a real , chosen independently of and , such that
if and only if
Here and denote polynomial evaluation at the matrix , and the stars leave the second-column blocks unspecified. The zero polynomial satisfies the degree bound.
This theorem characterizes exactly the polynomial pairs synthesized by forward signal applications and rotations; it imposes no real-coefficient or parity restriction.
Formalization Note Universal finite-dimensional unitary realization expresses the polynomial identity used by the proof; in particular, it includes every scalar unitary . The rotation is the matrix printed in equation (6), without a determinant-one constraint.
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.
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.
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.
Few Single-Qubit Measurements Suffice to Certify Any Quantum State (Gupta, He, O'Donnell) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the one-copy certification theorem of Gupta, He and O'Donnell.
Access model. For qubits, the algorithm accesses a pure hypothesis state , , only through queries of Definition 15: for single-qubit projectors on (each , the identity allowed), the query returns . It also flips fair coins, and it touches its single copy of the unknown -qubit mixed state (positive semidefinite, trace one) only by projective measurements of one qubit at a time in an orthonormal basis ; the qubit, the basis, the queries and the coins may all depend adaptively on everything seen so far.
Theorem. There exist such an algorithm for every and a constant , chosen before and , such that for every , every run of makes at most query, coin and measurement steps, and for every and , writing ,
Repeating this test times and applying a Chernoff bound gives the paper's Main Theorem: certification of every pure state with single-qubit measurements on copies.
Formalization Note The output probability is computed on subnormalized post-measurement states (Lüders rule without renormalization). The running time is modelled by the number of query, coin and measurement steps on every execution path; classical post-processing between steps is not charged, which matches the source's per-step cost only up to this modelling choice.
This is the one-copy certification theorem of Gupta, He and O'Donnell.
Access model. For qubits, the algorithm accesses a pure hypothesis state , , only through queries of Definition 15: for single-qubit projectors on (each , the identity allowed), the query returns . It also flips fair coins, and it touches its single copy of the unknown -qubit mixed state (positive semidefinite, trace one) only by projective measurements of one qubit at a time in an orthonormal basis ; the qubit, the basis, the queries and the coins may all depend adaptively on everything seen so far.
Theorem. There exist such an algorithm for every and a constant , chosen before and , such that for every , every run of makes at most query, coin and measurement steps, and for every and , writing ,
Repeating this test times and applying a Chernoff bound gives the paper's Main Theorem: certification of every pure state with single-qubit measurements on copies.
Formalization Note The output probability is computed on subnormalized post-measurement states (Lüders rule without renormalization). The running time is modelled by the number of query, coin and measurement steps on every execution path; classical post-processing between steps is not charged, which matches the source's per-step cost only up to this modelling choice.
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.
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.
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.
Quantum Approximate Counting, Simplified (Aaronson, Rall) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the main theorem of Aaronson and Rall: approximate counting with the optimal query complexity, using Grover iterations only (no quantum Fourier transform).
Let be a nonempty set of marked items and . The algorithm (AR p.4) pads the list with unmarked items, giving items. Let be the membership (phase) oracle, the uniform superposition over the items, and . The only quantum operation is: prepare for an odd and measure it in the computational basis, at a cost of queries.
The theorem has three parts.
The function and the constants are fixed before , , and . The result matches the BHMT query complexity for approximate counting, and it is the basis of QFT-free amplitude estimation.
Formalization Note The theorem is stated for the paper's concrete algorithm (the frozen definitions acEventProb, acStep1Exit, acStep2), with every shot count "at least " taken as exactly and Mathlib's round used for the rotation lemma's roundings (the paper allows any tie-breaking). The sentence "fewer than queries whenever the estimate is accurate" is formalized as the joint event of accuracy and fewer than queries, which is what the proof establishes. That event implies the accuracy claim. The -bound is uniform in and as .
This is the main theorem of Aaronson and Rall: approximate counting with the optimal query complexity, using Grover iterations only (no quantum Fourier transform).
Let be a nonempty set of marked items and . The algorithm (AR p.4) pads the list with unmarked items, giving items. Let be the membership (phase) oracle, the uniform superposition over the items, and . The only quantum operation is: prepare for an odd and measure it in the computational basis, at a cost of queries.
The theorem has three parts.
The function and the constants are fixed before , , and . The result matches the BHMT query complexity for approximate counting, and it is the basis of QFT-free amplitude estimation.
Formalization Note The theorem is stated for the paper's concrete algorithm (the frozen definitions acEventProb, acStep1Exit, acStep2), with every shot count "at least " taken as exactly and Mathlib's round used for the rotation lemma's roundings (the paper allows any tie-breaking). The sentence "fewer than queries whenever the estimate is accurate" is formalized as the joint event of accuracy and fewer than queries, which is what the proof establishes. That event implies the accuracy claim. The -bound is uniform in and as .
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.
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.
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.
Learning stabilizer states by Bell sampling (Montanaro) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is Montanaro's theorem on learning stabilizer states by Bell sampling.
A stabilizer state of qubits is a unit vector for which there is a commuting subgroup of the -qubit Pauli group, not containing , with and for all . A learner proceeds in rounds; each round takes some fresh copies of the unknown state together with ancilla qubits in , applies a circuit of gates from whose gates may be switched on or off by bits computed (by Boolean circuits) from the outcomes of earlier rounds, and measures all its qubits in the computational basis. At the end a Boolean circuit maps all outcomes to a stabilizer tableau , i.e. signed Pauli strings , whose associated projector is . The time of the learner is the total number of quantum gates, ancilla qubits and classical Boolean gates.
There are constants , and such that for every there is a single learner , fixed independently of the unknown state, with the following properties:
The paper's Algorithm 1 achieves this with copies (Bell sampling on pairs, then single-copy Pauli measurements to fix the signs) and failure probability at most . The copy count matches the information-theoretic lower bound while acting on only two copies at a time.
Formalization Note Identification is up to global phase, as in the source: success is equality of the projector of the output tableau with . The learner family over is not required to be uniformly generated, since the theorem names no uniformity notion.
This is Montanaro's theorem on learning stabilizer states by Bell sampling.
A stabilizer state of qubits is a unit vector for which there is a commuting subgroup of the -qubit Pauli group, not containing , with and for all . A learner proceeds in rounds; each round takes some fresh copies of the unknown state together with ancilla qubits in , applies a circuit of gates from whose gates may be switched on or off by bits computed (by Boolean circuits) from the outcomes of earlier rounds, and measures all its qubits in the computational basis. At the end a Boolean circuit maps all outcomes to a stabilizer tableau , i.e. signed Pauli strings , whose associated projector is . The time of the learner is the total number of quantum gates, ancilla qubits and classical Boolean gates.
There are constants , and such that for every there is a single learner , fixed independently of the unknown state, with the following properties:
The paper's Algorithm 1 achieves this with copies (Bell sampling on pairs, then single-copy Pauli measurements to fix the signs) and failure probability at most . The copy count matches the information-theoretic lower bound while acting on only two copies at a time.
Formalization Note Identification is up to global phase, as in the source: success is equality of the projector of the output tableau with . The learner family over is not required to be uniformly generated, since the theorem names no uniformity notion.
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.
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.
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.
Iterative Quantum Amplitude Estimation (Grinko, Gacon, Zoufal, Woerner) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be a unitary on qubits such that
where is unknown and are unit vectors (not necessarily orthogonal); the last qubit is the flag qubit. Let , so , and let with and .
Run Iterative Quantum Amplitude Estimation (Algorithm 1 with the subroutine FindNextK, ) with Clopper–Pearson confidence intervals at per-round level , where ; each iteration measures the flag qubit of a number of times and updates a confidence interval for . Fix , a target accuracy , and an integer number of shots , where
Then:
This is the Clopper–Pearson variant of the correctness theorem of IQAE: amplitude estimation without phase estimation, with a quadratic speedup over Monte Carlo up to a double-logarithmic factor and explicit small constants.
Formalization Note The algorithm is a Markov chain on its classical state; shot counts are binomial with the exact quantum probability of the flag outcome. The chain is run for steps (the last step only evaluates the loop condition) and every reachable state must be halted. Two corrections of the page: the Clopper–Pearson bounds are used in their standard orientation (the paper prints and swapped in (C5)–(C6) and Alg. 1), and is assumed, since for the printed algorithm has while its loop still runs.
Let be a unitary on qubits such that
where is unknown and are unit vectors (not necessarily orthogonal); the last qubit is the flag qubit. Let , so , and let with and .
Run Iterative Quantum Amplitude Estimation (Algorithm 1 with the subroutine FindNextK, ) with Clopper–Pearson confidence intervals at per-round level , where ; each iteration measures the flag qubit of a number of times and updates a confidence interval for . Fix , a target accuracy , and an integer number of shots , where
Then:
This is the Clopper–Pearson variant of the correctness theorem of IQAE: amplitude estimation without phase estimation, with a quadratic speedup over Monte Carlo up to a double-logarithmic factor and explicit small constants.
Formalization Note The algorithm is a Markov chain on its classical state; shot counts are binomial with the exact quantum probability of the flag outcome. The chain is run for steps (the last step only evaluates the loop condition) and every reachable state must be halted. Two corrections of the page: the Clopper–Pearson bounds are used in their standard orientation (the paper prints and swapped in (C5)–(C6) and Alg. 1), and is assumed, since for the printed algorithm has while its loop still runs.
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.
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.
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.
Optimization by Decoded Quantum Interferometry (Jordan, Shutty, Wootters, Zalcman, Schmidhuber, King, Isakov, Khattar, Babbush) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the semicircle law of decoded quantum interferometry (DQI) with perfect decoding.
Let be a prime and . A max-LINSAT instance consists of a matrix with rows and subsets ; constraint is for . Put on and off it, and . For a polynomial with complex coefficients the DQI state is . Let be the supremum, over all of degree at most with , of the expected number of satisfied constraints when is measured in the computational basis (outcome with probability ). Let be the minimum Hamming weight of a nonzero codeword of .
Fix and write . Consider instances with for all , , and . Then, as ,
uniformly over such instances: for every there is such that every such instance with has within of the right-hand side.
The theorem converts any decoding guarantee for the code out to errors into an approximation guarantee for max-LINSAT, and it is the basis of the paper's comparison of DQI with classical optimizers (e.g. on Optimal Polynomial Intersection).
Formalization Note The source's limit over an arbitrary sequence of instances is stated in the equivalent uniform – form, with chosen after and before the instance. The hypothesis is taken from Lemma 9.2, on which the source's proof of the theorem rests. The optimum is over polynomials of degree at most (as in the proof, which optimizes over all unit coefficient vectors ); is required exactly, so values of for which is never an integer make the statement vacuous, as in the source.
This is the semicircle law of decoded quantum interferometry (DQI) with perfect decoding.
Let be a prime and . A max-LINSAT instance consists of a matrix with rows and subsets ; constraint is for . Put on and off it, and . For a polynomial with complex coefficients the DQI state is . Let be the supremum, over all of degree at most with , of the expected number of satisfied constraints when is measured in the computational basis (outcome with probability ). Let be the minimum Hamming weight of a nonzero codeword of .
Fix and write . Consider instances with for all , , and . Then, as ,
uniformly over such instances: for every there is such that every such instance with has within of the right-hand side.
The theorem converts any decoding guarantee for the code out to errors into an approximation guarantee for max-LINSAT, and it is the basis of the paper's comparison of DQI with classical optimizers (e.g. on Optimal Polynomial Intersection).
Formalization Note The source's limit over an arbitrary sequence of instances is stated in the equivalent uniform – form, with chosen after and before the instance. The hypothesis is taken from Lemma 9.2, on which the source's proof of the theorem rests. The optimum is over polynomials of degree at most (as in the proof, which optimizes over all unit coefficient vectors ); is required exactly, so values of for which is never an integer make the statement vacuous, as in the source.
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.
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.
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.
Performance guarantees of light-cone variational quantum algorithms for the maximum cut problem establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be any family of finite nonempty connected undirected unweighted simple cubic graphs, with . For each graph, choose a root and construct the one-round lightcone-ZY schedule by recursive BFS, resolving unspecified ties by vertex labels. Each schedule starts in and uses one gate per directed edge, with a common real angle. Let be the expected cut computed by the isolated-boundary 0-local prescription, the attained maximum cut, , and . Let count the zero-in-degree vertices and put
For every , there is such that for all ,
and every arbitrary one-round orientation and gate order on with satisfies
Thus the lightcone schedule attains the asymptotically optimal edge-count certificate at its source count. The pointwise guarantee gives the corresponding worst-case guarantee over graph classes. Source density need not converge. Optimality concerns this certificate; it does not identify the full-circuit ratio with the certificate.
Let be any family of finite nonempty connected undirected unweighted simple cubic graphs, with . For each graph, choose a root and construct the one-round lightcone-ZY schedule by recursive BFS, resolving unspecified ties by vertex labels. Each schedule starts in and uses one gate per directed edge, with a common real angle. Let be the expected cut computed by the isolated-boundary 0-local prescription, the attained maximum cut, , and . Let count the zero-in-degree vertices and put
For every , there is such that for all ,
and every arbitrary one-round orientation and gate order on with satisfies
Thus the lightcone schedule attains the asymptotically optimal edge-count certificate at its source count. The pointwise guarantee gives the corresponding worst-case guarantee over graph classes. Source density need not converge. Optimality concerns this certificate; it does not identify the full-circuit ratio with the certificate.
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.
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.
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.
Quantum versus Classical Learnability (Servedio, Gortler) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be a class of concepts . Write for the classical sample complexity of exact learning from membership queries: the least such that some randomized algorithm (a probability distribution over adaptive query trees) asking at most membership queries outputs the target with probability at least , for every . For , and let , and for put
There are absolute constants , independent of and , such that for every and every class :
That is, , and . These are the classical bounds that, combined with their quantum analogues, show that quantum and classical exact learning from membership queries are polynomially equivalent in query complexity.
Formalization Note is the frozen gammaParam, which is only meaningful for ; that hypothesis is explicit. In (2) the cases are harmless since in Lean. The query bound is required on every input string rather than only on targets in ; the resulting complexities coincide.
Let be a class of concepts . Write for the classical sample complexity of exact learning from membership queries: the least such that some randomized algorithm (a probability distribution over adaptive query trees) asking at most membership queries outputs the target with probability at least , for every . For , and let , and for put
There are absolute constants , independent of and , such that for every and every class :
That is, , and . These are the classical bounds that, combined with their quantum analogues, show that quantum and classical exact learning from membership queries are polynomially equivalent in query complexity.
Formalization Note is the frozen gammaParam, which is only meaningful for ; that hypothesis is explicit. In (2) the cases are harmless since in Lean. The query bound is required on every input string rather than only on targets in ; the resulting complexities coincide.
A Blum integer is with -bit primes, . Assume that no polynomial-time classical randomized algorithm factors a uniformly random Blum integer with non-negligible success probability: for every such algorithm and every polynomial , for all sufficiently large ,
Then there is a concept class , a set of Boolean functions on , such that:
This shows that the information-theoretic equivalence of quantum and classical PAC learning does not extend to computationally efficient learning, under a standard cryptographic assumption.
Formalization Note and with integers , and polynomials in are polynomials in ; this is equivalent up to polynomial factors. As in the source, the quantum learner is a non-uniform family of networks while the classical learner is a uniform machine.
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.
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.
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.
Optimal polynomial based quantum eigenstate filtering with application to solving quantum linear systems (Lin, Tong) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the eigenstate filtering theorem of Lin and Tong.
An -qubit unitary is an -block-encoding of an -qubit operator if
where is the operator norm and the ancilla qubits form the first register. For a Hermitian -qubit matrix and a real number , let be the orthogonal projector onto the -eigenspace of (which may be degenerate).
There are absolute constants and such that the following holds. For all and all reals , , and , there is a quantum circuit on qubits, built from two-qubit gates and black-box applications (possibly controlled, possibly inverted) of an -qubit unitary , which uses
and such that for every Hermitian and every -block-encoding of for which is an eigenvalue of with every other eigenvalue satisfying , the unitary is a -block-encoding of .
Applied to an initial state with overlap with the -eigenspace, this prepares the target eigenstate with logarithmic dependence on the precision; the paper uses it to solve the quantum linear systems problem with near-optimal query complexity.
Formalization Note The circuit depends only on the known data , not on or . Primitive gates are taken to be arbitrary two-qubit unitaries (the source does not fix a gate set and assumes exact phase factors). The printed gate bound is stated with in place of : at the printed bound would force zero gates, while the source's own Theorem 1' gives gates.
This is the eigenstate filtering theorem of Lin and Tong.
An -qubit unitary is an -block-encoding of an -qubit operator if
where is the operator norm and the ancilla qubits form the first register. For a Hermitian -qubit matrix and a real number , let be the orthogonal projector onto the -eigenspace of (which may be degenerate).
There are absolute constants and such that the following holds. For all and all reals , , and , there is a quantum circuit on qubits, built from two-qubit gates and black-box applications (possibly controlled, possibly inverted) of an -qubit unitary , which uses
and such that for every Hermitian and every -block-encoding of for which is an eigenvalue of with every other eigenvalue satisfying , the unitary is a -block-encoding of .
Applied to an initial state with overlap with the -eigenspace, this prepares the target eigenstate with logarithmic dependence on the precision; the paper uses it to solve the quantum linear systems problem with near-optimal query complexity.
Formalization Note The circuit depends only on the known data , not on or . Primitive gates are taken to be arbitrary two-qubit unitaries (the source does not fix a gate set and assumes exact phase factors). The printed gate bound is stated with in place of : at the printed bound would force zero gates, while the source's own Theorem 1' gives gates.
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.
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.
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.
Quantum Tanner codes (Leverrier, Zemor) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the main technical theorem behind quantum Tanner codes.
Setting. Let be a finite group and , with , satisfying the Total No-Conjugacy condition for all , , . The left-right Cayley complex has vertices , , and squares , the 4-sets . For a vertex the squares incident to are in bijection with , so the restriction of to the squares at is an array. Let , be the bipartite double covers of and ; we require both to be Ramanujan: connected, and every adjacency eigenvalue other than has absolute value at most .
For codes , , the tensor code consists of arrays whose columns lie in and whose rows lie in . The dual tensor code is . It is -robust if every codeword of weight vanishes outside for some , with and , where are the minimum distances. It is -robust with -resistance to puncturing if, for all , with and , the dual tensor code of the punctured codes , is -robust. The quantum Tanner code is
Theorem. Fix , and . There is , depending only on , such that the following holds for every and every complex as above. Suppose every nonzero codeword of and of has weight at least , and the dual tensor code is -robust with -resistance to puncturing. Let . Then for every with
there are a vertex and a tensor codeword such that the word that equals on the squares at and is elsewhere lies in and satisfies .
Applied repeatedly, the theorem shows that low-weight codewords of lie in , which gives the linear minimum distance of quantum Tanner codes. It also recovers the local testability of the Dinur et al. code.
Formalization Note The paper says "there exists an infinite family of square complexes". The formal statement instead holds for every left-right Cayley complex that satisfies the hypotheses the proof uses (TNC, Ramanujan double covers). The infinite family is the cited [DEL+21] construction. Minimum distances are taken in , and the bounds are written as .
This is the main technical theorem behind quantum Tanner codes.
Setting. Let be a finite group and , with , satisfying the Total No-Conjugacy condition for all , , . The left-right Cayley complex has vertices , , and squares , the 4-sets . For a vertex the squares incident to are in bijection with , so the restriction of to the squares at is an array. Let , be the bipartite double covers of and ; we require both to be Ramanujan: connected, and every adjacency eigenvalue other than has absolute value at most .
For codes , , the tensor code consists of arrays whose columns lie in and whose rows lie in . The dual tensor code is . It is -robust if every codeword of weight vanishes outside for some , with and , where are the minimum distances. It is -robust with -resistance to puncturing if, for all , with and , the dual tensor code of the punctured codes , is -robust. The quantum Tanner code is
Theorem. Fix , and . There is , depending only on , such that the following holds for every and every complex as above. Suppose every nonzero codeword of and of has weight at least , and the dual tensor code is -robust with -resistance to puncturing. Let . Then for every with
there are a vertex and a tensor codeword such that the word that equals on the squares at and is elsewhere lies in and satisfies .
Applied repeatedly, the theorem shows that low-weight codewords of lie in , which gives the linear minimum distance of quantum Tanner codes. It also recovers the local testability of the Dinur et al. code.
Formalization Note The paper says "there exists an infinite family of square complexes". The formal statement instead holds for every left-right Cayley complex that satisfies the hypotheses the proof uses (TNC, Ramanujan double covers). The infinite family is the cited [DEL+21] construction. Minimum distances are taken in , and the bounds are written as .
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.
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.
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.
Decoding quantum Tanner codes (Leverrier, Zemor) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the correctness and iteration bound of the sequential decoder for quantum Tanner codes (Leverrier–Zémor, Theorem 13 with the bound established in its proof).
Fix and constants . There is (depending only on ) such that the following holds for every . Let be a finite group with self-inverse subsets , of size such that the left Cayley graph and the right Cayley graph are connected, non-bipartite ( is not an adjacency eigenvalue) and Ramanujan (every adjacency eigenvalue has ). Let , be linear codes with , such that , , , all have minimum distance at least , and both dual tensor codes and are -product-expanding (every codeword is with , counting nonzero columns of and nonzero rows of ). Let be the set of squares of the quadripartite left-right Cayley complex, , and let be the quantum Tanner code.
Let be a -type error with
For each let be any minimum-weight local vector on with the same local syndrome as , and let be the mismatch. Consider any run of the sequential mismatch decomposition (Algorithm 2 with parameter , with any of its choices of vertex and nonzero local dual tensor codeword with and minimal, updating , , ), started from , , after iterations. Then:
This is the paper's linear-time decoding guarantee: quantum Tanner codes built from Ramanujan left-right Cayley complexes and robust local codes admit a sequential decoder correcting every error of weight linear in the code length.
Formalization Note The squares are indexed injectively by ; vertices are with the paper's labelling (p.10). Algorithm 2 is a nondeterministic step relation, so the statement quantifies over all runs and over all choices of the . Only the case is stated, as in the paper's proof (the case is symmetric). The group ranges over Type (universe 0).
This is the correctness and iteration bound of the sequential decoder for quantum Tanner codes (Leverrier–Zémor, Theorem 13 with the bound established in its proof).
Fix and constants . There is (depending only on ) such that the following holds for every . Let be a finite group with self-inverse subsets , of size such that the left Cayley graph and the right Cayley graph are connected, non-bipartite ( is not an adjacency eigenvalue) and Ramanujan (every adjacency eigenvalue has ). Let , be linear codes with , such that , , , all have minimum distance at least , and both dual tensor codes and are -product-expanding (every codeword is with , counting nonzero columns of and nonzero rows of ). Let be the set of squares of the quadripartite left-right Cayley complex, , and let be the quantum Tanner code.
Let be a -type error with
For each let be any minimum-weight local vector on with the same local syndrome as , and let be the mismatch. Consider any run of the sequential mismatch decomposition (Algorithm 2 with parameter , with any of its choices of vertex and nonzero local dual tensor codeword with and minimal, updating , , ), started from , , after iterations. Then:
This is the paper's linear-time decoding guarantee: quantum Tanner codes built from Ramanujan left-right Cayley complexes and robust local codes admit a sequential decoder correcting every error of weight linear in the code length.
Formalization Note The squares are indexed injectively by ; vertices are with the paper's labelling (p.10). Algorithm 2 is a nondeterministic step relation, so the statement quantifies over all runs and over all choices of the . Only the case is stated, as in the paper's proof (the case is symmetric). The group ranges over Type (universe 0).
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.
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.
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.
Near-optimal ground state preparation (Lin, Tong) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the ground state preparation theorem of Lin and Tong for the case where an upper bound on the ground energy is known.
Let and let be Hermitian with eigenvalues and a ground state (a unit eigenvector for ). Access is through two unitary oracles: an -block-encoding of , i.e. an -qubit unitary with , and an -qubit unitary preparing . For known parameters , , , the promises are
There are absolute constants such that for every and every there is a quantum circuit of one- and two-qubit gates with oracle calls (plain, inverse or controlled) to and , on qubits started in , together with a set of accepted outcomes of its ancilla qubits, such that
and, for every instance satisfying (P1) and (P2), measuring the ancillas gives an accepted outcome with probability at least , and for every accepted outcome the post-measurement state of the system register has fidelity .
The circuit depends only on the known parameters, not on the instance. The query cost is logarithmic in the inverse precision, which the paper shows to be essentially optimal in and .
Formalization Note The source writes qubits and gates; these are stated with and , since at (resp. ) the literal bound is zero while the construction needs ancillas and Hadamard gates (the paper's own Theorem 1 gives gates). The constant success probability is the proof's reading of the theorem ("the procedure succeeds with some constant probability"). Fidelity is , as in the paper's footnote 1.
This is the ground state preparation theorem of Lin and Tong for the case where an upper bound on the ground energy is known.
Let and let be Hermitian with eigenvalues and a ground state (a unit eigenvector for ). Access is through two unitary oracles: an -block-encoding of , i.e. an -qubit unitary with , and an -qubit unitary preparing . For known parameters , , , the promises are
There are absolute constants such that for every and every there is a quantum circuit of one- and two-qubit gates with oracle calls (plain, inverse or controlled) to and , on qubits started in , together with a set of accepted outcomes of its ancilla qubits, such that
and, for every instance satisfying (P1) and (P2), measuring the ancillas gives an accepted outcome with probability at least , and for every accepted outcome the post-measurement state of the system register has fidelity .
The circuit depends only on the known parameters, not on the instance. The query cost is logarithmic in the inverse precision, which the paper shows to be essentially optimal in and .
Formalization Note The source writes qubits and gates; these are stated with and , since at (resp. ) the literal bound is zero while the construction needs ancillas and Hadamard gates (the paper's own Theorem 1 gives gates). The constant success probability is the proof's reading of the theorem ("the procedure succeeds with some constant probability"). Fidelity is , as in the paper's footnote 1.
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.
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.
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.
Product Decomposition of Periodic Functions in Quantum Signal Processing (Haah) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the product-decomposition theorem underlying quantum signal processing.
For an integer let be the set of Laurent polynomials with coefficients such that for every with . Such an has degree if or . Let consist of those whose exponents lie in , i.e. for every odd . For a rank-one orthogonal projector on the primitive matrix is
Then:
as Laurent polynomials. 3. If and is decomposed as in 2, then the last projector is
The theorem characterizes exactly which polynomial functions are achievable by alternating controlled- and controlled- with single-qubit rotations, and item 3 gives the peeling step of the classical algorithm that computes the rotation sequence.
Formalization Note The source's is "a unitary"; because and on the unit circle, any unitary in such a decomposition has determinant 1, so ranging over is equivalent. Uniqueness is of the whole ordered tuple. The projector is the factor at index of a -indexed family. That (so the trace is nonzero) is a fact the source proves, not a hypothesis.
This is the product-decomposition theorem underlying quantum signal processing.
For an integer let be the set of Laurent polynomials with coefficients such that for every with . Such an has degree if or . Let consist of those whose exponents lie in , i.e. for every odd . For a rank-one orthogonal projector on the primitive matrix is
Then:
as Laurent polynomials. 3. If and is decomposed as in 2, then the last projector is
The theorem characterizes exactly which polynomial functions are achievable by alternating controlled- and controlled- with single-qubit rotations, and item 3 gives the peeling step of the classical algorithm that computes the rotation sequence.
Formalization Note The source's is "a unitary"; because and on the unit circle, any unitary in such a decomposition has determinant 1, so ranging over is equivalent. Uniqueness is of the whole ordered tuple. The projector is the factor at index of a -indexed family. That (so the trace is nonzero) is a fact the source proves, not a hypothesis.
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.
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.
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.
The Optimal Sample Complexity of PAC Learning (Hanneke) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the optimal sample complexity of realizable PAC learning (Hanneke, Theorem 2 and Corollary 3).
Let be a nonempty measurable space (the instance space) and let be a set of measurable classifiers with and finite VC dimension . For a probability measure on , a target and a classifier , write . For the sample complexity is the smallest for which some (possibly randomized) learning algorithm , given the i.i.d. -distributed points labelled by , outputs a measurable classifier with for every and every (and if no works). Let . Assume, as the paper does, that the events of the uniform convergence bound for sample-consistent classifiers are measurable.
Then there are numerical constants, independent of and (in particular of ):
This removes the logarithmic factor from the classical upper bound of Vapnik and Blumer et al., matching the lower bounds of Blumer et al. and Ehrenfeucht et al. up to constants.
Formalization Note takes values in (ℕ∞); part 2 is stated for finite values only, the infinite case being trivially true. Randomized algorithms use an arbitrary probability space independent of the sample. The PAC failure probability is the measure of the failure set (its outer measure if that set is not measurable).
This is the optimal sample complexity of realizable PAC learning (Hanneke, Theorem 2 and Corollary 3).
Let be a nonempty measurable space (the instance space) and let be a set of measurable classifiers with and finite VC dimension . For a probability measure on , a target and a classifier , write . For the sample complexity is the smallest for which some (possibly randomized) learning algorithm , given the i.i.d. -distributed points labelled by , outputs a measurable classifier with for every and every (and if no works). Let . Assume, as the paper does, that the events of the uniform convergence bound for sample-consistent classifiers are measurable.
Then there are numerical constants, independent of and (in particular of ):
This removes the logarithmic factor from the classical upper bound of Vapnik and Blumer et al., matching the lower bounds of Blumer et al. and Ehrenfeucht et al. up to constants.
Formalization Note takes values in (ℕ∞); part 2 is stated for finite values only, the infinite case being trivially true. Randomized algorithms use an arbitrary probability space independent of the sample. The PAC failure probability is the measure of the failure set (its outer measure if that set is not measurable).
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.
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.
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.
Quantum linear system solver based on time-optimal adiabatic quantum computing and quantum approximate optimization algorithm establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let , , and let be Hermitian positive definite with . Let be a unit vector. Here denotes the operator norm for matrices and the Euclidean norm for vectors. Write
The condition number is the actual value determined by , and satisfies .
Set and
For , AQC() uses the schedule specified by
Thus . The schedule is when ; when and , it is ; otherwise it is the closed formula in Eq. (6). For positive runtime , the normalized evolution solves
For every fixed there is a constant , independent of and the requested accuracy, such that this evolution exists for every and every solution satisfies
Consequently, for every there exists a successful positive runtime : the evolution exists at this runtime and every solution has the displayed error at most .
For each endpoint there are constants and , independent of all input data and accuracy, such that whenever and , there exists a positive runtime with
at which the evolution exists and every solution has operator norm error at most .
This result establishes the runtime and accuracy guarantee for the continuous AQC() linear-system solver with positive definite matrices.
Formalization Note The error compares density matrices on the full -dimensional register. The endpoint big-O clause is asymptotic in ; the threshold avoids interpreting at as an upper bound on a positive runtime. The frozen condition-number range binder is automatic on the stated input class.
Let , , and let be Hermitian positive definite with . Let be a unit vector. Here denotes the operator norm for matrices and the Euclidean norm for vectors. Write
The condition number is the actual value determined by , and satisfies .
Set and
For , AQC() uses the schedule specified by
Thus . The schedule is when ; when and , it is ; otherwise it is the closed formula in Eq. (6). For positive runtime , the normalized evolution solves
For every fixed there is a constant , independent of and the requested accuracy, such that this evolution exists for every and every solution satisfies
Consequently, for every there exists a successful positive runtime : the evolution exists at this runtime and every solution has the displayed error at most .
For each endpoint there are constants and , independent of all input data and accuracy, such that whenever and , there exists a positive runtime with
at which the evolution exists and every solution has operator norm error at most .
This result establishes the runtime and accuracy guarantee for the continuous AQC() linear-system solver with positive definite matrices.
Formalization Note The error compares density matrices on the full -dimensional register. The endpoint big-O clause is asymptotic in ; the threshold avoids interpreting at as an upper bound on a positive runtime. The frozen condition-number range binder is automatic on the stated input class.
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.
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.
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.
Quantum entanglement and the communication complexity of the inner product function (Cleve, van Dam, Nielsen, Tapp) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the entanglement-assisted lower bound of Cleve, van Dam, Nielsen and Tapp, a consequence of Holevo's theorem.
Consider a two-party qubit protocol in which Alice holds an input on of her qubits. All other qubits start in , except for a block of qubits in an arbitrary shared state (fixed before the input, its qubits distributed between Alice and Bob in any way). The protocol is a fixed sequence of steps, each of which is a unitary applied by one party to qubits it currently holds, or the sending of one qubit to the other party. Let be the number of qubits Alice sends to Bob; the number of qubits Bob sends to Alice is unrestricted. At the end Bob performs a measurement (a POVM) acting only on the qubits he holds.
The bound holds regardless of the prior entanglement and of the communication from Bob to Alice. It is the information-theoretic ingredient of the paper's linear lower bounds on the communication complexity of the inner product function.
Formalization Note The protocol model is the shared TwoPartyProtocol (pure shared state; mixed states and intermediate measurements are simulated with ancillas, as the paper notes on p.13). The ceiling is written as natural-number division . In clause 1 the outcome set is itself; a measurement with another outcome set followed by a decoding map is a coarse-grained measurement of this form, and clause 2 covers arbitrary outcome sets.
This is the entanglement-assisted lower bound of Cleve, van Dam, Nielsen and Tapp, a consequence of Holevo's theorem.
Consider a two-party qubit protocol in which Alice holds an input on of her qubits. All other qubits start in , except for a block of qubits in an arbitrary shared state (fixed before the input, its qubits distributed between Alice and Bob in any way). The protocol is a fixed sequence of steps, each of which is a unitary applied by one party to qubits it currently holds, or the sending of one qubit to the other party. Let be the number of qubits Alice sends to Bob; the number of qubits Bob sends to Alice is unrestricted. At the end Bob performs a measurement (a POVM) acting only on the qubits he holds.
The bound holds regardless of the prior entanglement and of the communication from Bob to Alice. It is the information-theoretic ingredient of the paper's linear lower bounds on the communication complexity of the inner product function.
Formalization Note The protocol model is the shared TwoPartyProtocol (pure shared state; mixed states and intermediate measurements are simulated with ancillas, as the paper notes on p.13). The ceiling is written as natural-number division . In clause 1 the outcome set is itself; a measurement with another outcome set followed by a decoding map is a coarse-grained measurement of this form, and clause 2 covers arbitrary outcome sets.
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.
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.
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.
Quantum tomography using state-preparation unitaries (van Apeldoorn, Cornelissen, Gilyén, Nannicini) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the pure-state tomography result of van Apeldoorn, Cornelissen, Gilyén and Nannicini (arXiv:2207.08800, Proposition 22), cited in Nannicini's lecture notes as Theorem 5.17.
Let and . Let be a pure state, so and . It is stored on qubits, with basis states for having amplitude . Let be an -qubit unitary with . The algorithm can apply and , possibly controlled, but sees only through these applications. The gate set has all single-qubit gates, CNOT, and the indexed-SWAP gate
There are absolute constants and such that the following holds for every , and . Write .
There is a quantum algorithm, fixed before , with the following resources:
For every such and , with probability at least it outputs with
The result reaches the optimal dependence for -estimation of the amplitudes. Combined with the paper's -to- conversion, it yields the tomography bounds (Theorem 23 of the paper; Corollary 5.18 in Nannicini).
Formalization Note Both clauses use the coherent-circuit model: one oracle circuit over the paper's gate set, started in and measured once, with classical post-processing (medians, rescaling) in a read-out function. The paper allows adaptive classical control. The adaptive algorithm of clause 2 is simulated by deferred measurement, and the paper's convention of counting classical computation up to polylog factors absorbs the cost. The logarithms and are written so the bounds do not vanish in the degenerate corner , . The factors are . On index values , which the paper leaves unspecified, the indexed-SWAP gate acts as the identity.
This is the pure-state tomography result of van Apeldoorn, Cornelissen, Gilyén and Nannicini (arXiv:2207.08800, Proposition 22), cited in Nannicini's lecture notes as Theorem 5.17.
Let and . Let be a pure state, so and . It is stored on qubits, with basis states for having amplitude . Let be an -qubit unitary with . The algorithm can apply and , possibly controlled, but sees only through these applications. The gate set has all single-qubit gates, CNOT, and the indexed-SWAP gate
There are absolute constants and such that the following holds for every , and . Write .
There is a quantum algorithm, fixed before , with the following resources:
For every such and , with probability at least it outputs with
The result reaches the optimal dependence for -estimation of the amplitudes. Combined with the paper's -to- conversion, it yields the tomography bounds (Theorem 23 of the paper; Corollary 5.18 in Nannicini).
Formalization Note Both clauses use the coherent-circuit model: one oracle circuit over the paper's gate set, started in and measured once, with classical post-processing (medians, rescaling) in a read-out function. The paper allows adaptive classical control. The adaptive algorithm of clause 2 is simulated by deferred measurement, and the paper's convention of counting classical computation up to polylog factors absorbs the cost. The logarithms and are written so the bounds do not vanish in the degenerate corner , . The factors are . On index values , which the paper leaves unspecified, the indexed-SWAP gate acts as the identity.
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.
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.
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.
Quantum singular value transformation and beyond: exponential improvements for quantum matrix arithmetics (Gilyén, Su, Low, Wiebe) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the polynomial eigenvalue transformation theorem of Gilyén, Su, Low and Wiebe, which removes the parity constraint of quantum singular value transformation at the price of a factor .
For an -qubit operator , real numbers , and , an -qubit unitary is an -block-encoding of if
where is the operator norm and the ancilla register comes first.
There is an absolute constant such that the following holds. Let , let , and let be a polynomial of degree at most with for all . Then there exist and a quantum circuit on qubits, built from one- and two-qubit gates and calls to a black box on qubits, with
such that for every , , every Hermitian -qubit matrix with and every -block-encoding of , the circuit (with the last qubits as clean ancillas, started and returned exactly in ) implements a unitary on qubits that is a
This theorem is the workhorse for implementing smooth functions of Hermitian matrices (Hamiltonian simulation, matrix inversion, Gibbs sampling) through block-encodings.
Formalization Note The circuit is chosen before , so it depends only on . The source's is encoded with since a constant polynomial still needs a few gates. The source's last sentence (classical computability of the circuit description in time ) is not formalized, because the source fixes no bit model for the real coefficients of . The controlled query may be controlled- or controlled-. The hypothesis corrects the printed statement: the source's proof uses Lemma 22, which needs , and without it the printed statement fails (e.g. , , , , ).
Correction to the printed source.
Printed: Suppose that U is an (α, a, ε)-encoding of a Hermitian matrix A (no condition ‖A‖ ≤ α; Definition 43 only forces ‖A‖ ≤ α + ε).
Corrected: Added the hypothesis specNorm A ≤ α, i.e. ‖A/α‖ ≤ 1.
Reason: The proof (p.49) applies Lemma 22 (p.23), which requires both matrices to have operator norm at most 1. Without it the statement is false: s = a = 0, α = ε = 1, A = [2], U = [1] is a (1, 0, 1)-encoding of A; with P = T_8/2, d = 8, δ = 0 one gets P(A/α) = T_8(2)/2 ≈ 9408, while every block of a unitary has norm ≤ 1 and the claimed error is 32.
This is the polynomial eigenvalue transformation theorem of Gilyén, Su, Low and Wiebe, which removes the parity constraint of quantum singular value transformation at the price of a factor .
For an -qubit operator , real numbers , and , an -qubit unitary is an -block-encoding of if
where is the operator norm and the ancilla register comes first.
There is an absolute constant such that the following holds. Let , let , and let be a polynomial of degree at most with for all . Then there exist and a quantum circuit on qubits, built from one- and two-qubit gates and calls to a black box on qubits, with
such that for every , , every Hermitian -qubit matrix with and every -block-encoding of , the circuit (with the last qubits as clean ancillas, started and returned exactly in ) implements a unitary on qubits that is a
This theorem is the workhorse for implementing smooth functions of Hermitian matrices (Hamiltonian simulation, matrix inversion, Gibbs sampling) through block-encodings.
Formalization Note The circuit is chosen before , so it depends only on . The source's is encoded with since a constant polynomial still needs a few gates. The source's last sentence (classical computability of the circuit description in time ) is not formalized, because the source fixes no bit model for the real coefficients of . The controlled query may be controlled- or controlled-. The hypothesis corrects the printed statement: the source's proof uses Lemma 22, which needs , and without it the printed statement fails (e.g. , , , , ).
Correction to the printed source.
Printed: Suppose that U is an (α, a, ε)-encoding of a Hermitian matrix A (no condition ‖A‖ ≤ α; Definition 43 only forces ‖A‖ ≤ α + ε).
Corrected: Added the hypothesis specNorm A ≤ α, i.e. ‖A/α‖ ≤ 1.
Reason: The proof (p.49) applies Lemma 22 (p.23), which requires both matrices to have operator norm at most 1. Without it the statement is false: s = a = 0, α = ε = 1, A = [2], U = [1] is a (1, 0, 1)-encoding of A; with P = T_8/2, d = 8, δ = 0 one gets P(A/α) = T_8(2)/2 ≈ 9408, while every block of a unitary has norm ≤ 1 and the claimed error is 32.
This is the robust block-Hamiltonian simulation result of Gilyén, Su, Low and Wiebe (Corollary 62 of arXiv:1806.01838v1, Corollary 63 in the published version).
Block-encodings are as in Definition 43: an -qubit unitary is an -block-encoding of an -qubit operator if in operator norm.
There is an absolute constant such that the following holds. Let , , and . Then there exist and a circuit on qubits, made of two-qubit gates and calls to a black box on qubits, using
such that for every Hermitian -qubit matrix and every -block-encoding of , the circuit (with its last qubits as clean ancillas) implements a unitary that is a
This gives Hamiltonian simulation with additive query complexity in and , robust to an imprecise block-encoding of the Hamiltonian.
Formalization Note The circuit may depend on but not on or . The source's gate bound is encoded as , since the two new ancillas need gates even when . At the source's is undefined; in Lean , so there the hypothesis is an exact block-encoding.
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.
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.
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.
Optimizing quantum optimization algorithms via faster quantum gradient computation (Gilyén, Arunachalam, Wiebe) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the conversion of a probability oracle into an approximate phase oracle (Gilyén–Arunachalam–Wiebe, Theorem 14).
Let be a finite set and the Hilbert space with orthonormal basis . A probability oracle for with an -qubit auxiliary register is a unitary on with
for some normalized states (the flag is the last qubit). A phase oracle for on an auxiliary register is a unitary with for all .
There is an absolute constant such that for every , every finite and every there are a number of extra qubits and a quantum circuit on , built from input-independent unitaries and at most (uncontrolled) applications of and , such that for every , every probability oracle for , every phase oracle for on auxiliary qubits, and every unit vector ,
This shows that the probability oracles arising from parametrized quantum circuits can be used wherever a phase oracle is needed, at only logarithmic overhead in the precision.
Formalization Note The circuit is fixed before and ; the source's -qubit auxiliary register is written . The source's "for all " is read for unit vectors, as in the proof.
This is the conversion of a probability oracle into an approximate phase oracle (Gilyén–Arunachalam–Wiebe, Theorem 14).
Let be a finite set and the Hilbert space with orthonormal basis . A probability oracle for with an -qubit auxiliary register is a unitary on with
for some normalized states (the flag is the last qubit). A phase oracle for on an auxiliary register is a unitary with for all .
There is an absolute constant such that for every , every finite and every there are a number of extra qubits and a quantum circuit on , built from input-independent unitaries and at most (uncontrolled) applications of and , such that for every , every probability oracle for , every phase oracle for on auxiliary qubits, and every unit vector ,
This shows that the probability oracles arising from parametrized quantum circuits can be used wherever a phase oracle is needed, at only logarithmic overhead in the precision.
Formalization Note The circuit is fixed before and ; the source's -qubit auxiliary register is written . The source's "for all " is read for unit vectors, as in the proof.
This is the conversion of a phase oracle into a probability oracle (Gilyén–Arunachalam–Wiebe, Lemma 16).
Let be a finite set, the Hilbert space with orthonormal basis , and let be a phase oracle for on , i.e. a unitary with for all .
There is an absolute constant such that for all , every finite and every there are and a quantum circuit on , built from input-independent unitaries and at most invocations of , or their controlled versions, such that for every , every phase oracle for and every there are and a unit vector with
Together with Theorem 14 this shows that phase and probability oracles are interconvertible with logarithmic overhead in the precision when the probabilities are bounded away from and .
Formalization Note The register consists of the auxiliary qubits of and further qubits (); the last qubit is the flag. The source's "for every " is read as , the domain of .
This is the higher-order gradient algorithm of Gilyén–Arunachalam–Wiebe (Theorem 23).
Let be accessed through fractional phase queries: for a finite set of query points chosen by the algorithm, and every , a unitary with for ; each application of some counts as one query. For write (taken within the cube) with , the Euclidean norm.
There is an absolute constant such that for all , , , , , and every a-priori gradient bound there is a quantum algorithm (query points, start state, circuit and classical post-processing of the final measurement, all independent of ) using at most
phase queries with the following property: for every that is -times differentiable on , satisfies for all , , and , and for every fractional phase oracle for , the output satisfies
The bound shows that higher-degree central difference formulas reduce the query cost of Jordan's gradient algorithm, exponentially in for low-degree polynomials.
Formalization Note The known gradient bound is the hypothesis of Theorem 21 that the proof uses (the query count is independent of ). The factor is written , the proof's repetition count . Queries are uncontrolled and non-adjoint, as the proof applies them.
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.
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.
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.
Quantum algorithms for escaping from saddle points establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix positive smoothness bounds , confidence , and a nonnegative starting gap . Let be twice differentiable, with globally -Lipschitz gradient in Euclidean norm and globally -Lipschitz Hessian in operator norm. Assume attains its finite global minimum , and let the public initial point satisfy . For , set .
There are , a nonnegative integer , and thresholds , , depending only on the fixed public parameters. In the regime and , a quantum evaluation-query program can be chosen using and those public parameters before and its oracle. For every coherent value-output unitary satisfying , its joint output and evaluation-call law obeys
Here counts forward and inverse evaluation-oracle applications. There are no free gradient, Hessian or simulation queries. If , the program returns without queries, including in dimension one. Positive-gap small dimensions and scales are outside this asymptotic statement.
This is the authors' ideal-oracle existence claim, with the displayed and dependence and their broad convention . The formal counterpart combines Theorem 4, Eq. (66), pages 18–19, Remark 2 on page 20, and the accelerated evaluation-only extension asserted after Theorem 5 and in Remark 3 on page 24. It does not assert an exact local minimum or correctness of a specific finite-accuracy implementation.
Formalization Note The frozen ideal real-label register and adaptive evaluation-program semantics provide the joint law. The Hessian lower bound is its equivalent quadratic-form inequality on every real vector. Measurability is concluded for the chosen program, and the gap is computed from an attained minimum. The action of the oracle on dirty value registers is left unrestricted.
Fix positive smoothness bounds , confidence , and a nonnegative starting gap . Let be twice differentiable, with globally -Lipschitz gradient in Euclidean norm and globally -Lipschitz Hessian in operator norm. Assume attains its finite global minimum , and let the public initial point satisfy . For , set .
There are , a nonnegative integer , and thresholds , , depending only on the fixed public parameters. In the regime and , a quantum evaluation-query program can be chosen using and those public parameters before and its oracle. For every coherent value-output unitary satisfying , its joint output and evaluation-call law obeys
Here counts forward and inverse evaluation-oracle applications. There are no free gradient, Hessian or simulation queries. If , the program returns without queries, including in dimension one. Positive-gap small dimensions and scales are outside this asymptotic statement.
This is the authors' ideal-oracle existence claim, with the displayed and dependence and their broad convention . The formal counterpart combines Theorem 4, Eq. (66), pages 18–19, Remark 2 on page 20, and the accelerated evaluation-only extension asserted after Theorem 5 and in Remark 3 on page 24. It does not assert an exact local minimum or correctness of a specific finite-accuracy implementation.
Formalization Note The frozen ideal real-label register and adaptive evaluation-program semantics provide the joint law. The Hessian lower bound is its equivalent quadratic-form inequality on every real vector. Measurability is concluded for the chosen program, and the gap is computed from an attained minimum. The action of the oracle on dirty value registers is left unrestricted.
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.
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.
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.
Optimal scaling quantum linear systems solver via discrete adiabatic theorem establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be a complete complex Hilbert space and an integer. Write for unitary walk operators on , for . Choose at each step a spectral band and its complement . For each valid window , with , enclose the two bands in disjoint closed proper arcs of the unit circle. Use compatible choices in which shorter-window arcs lie in the corresponding longer-window arcs. Let be their minimum angular separation, in radians. The choices may be loose: these quantities need not equal the actual spectral gap.
Define when , when , and . Let . For nonnegative bounds , possibly dependent on , suppose
Set , with value zero if this set is empty, and assume at every grid index .
Let be the spectral projection onto and . Construct , and . Define the chronological evolutions by , , and . Then for every integer ,
Here is the full operator norm and empty sums equal zero. This quantitative discrete adiabatic estimate retains the dependence on the first two forward differences and the chosen angular gaps.
Formalization Note The frozen spectral-window structure encodes compatible nested arc choices and ; spectral projections use continuous functional calculus. Finite ordinal intervals encode exactly the displayed integer summation ranges, including and . The chronological product and neighboring minimum follow the proof's conventions where the introductory indexing and the appendix's word “maximum” are misprinted.
Let be a complete complex Hilbert space and an integer. Write for unitary walk operators on , for . Choose at each step a spectral band and its complement . For each valid window , with , enclose the two bands in disjoint closed proper arcs of the unit circle. Use compatible choices in which shorter-window arcs lie in the corresponding longer-window arcs. Let be their minimum angular separation, in radians. The choices may be loose: these quantities need not equal the actual spectral gap.
Define when , when , and . Let . For nonnegative bounds , possibly dependent on , suppose
Set , with value zero if this set is empty, and assume at every grid index .
Let be the spectral projection onto and . Construct , and . Define the chronological evolutions by , , and . Then for every integer ,
Here is the full operator norm and empty sums equal zero. This quantitative discrete adiabatic estimate retains the dependence on the first two forward differences and the chosen angular gaps.
Formalization Note The frozen spectral-window structure encodes compatible nested arc choices and ; spectral projections use continuous functional calculus. Finite ordinal intervals encode exactly the displayed integer summation ranges, including and . The chronological product and neighboring minimum follow the proof's conventions where the introductory indexing and the appendix's word “maximum” are misprinted.
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.
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.
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.
Error mitigation for short-depth quantum circuits establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be a finite family of known implementable completely positive trace-preserving maps on an -qubit device. Maps may include noisy initialization and need not be unitary or unital. Let be a length- word in a fixed finite unitary gate family, with composite unitary . Assume a supplied exact quasi-probability representation, fixed before all experimental outcomes:
where , is a probability distribution on length- noisy words, , and . Each experiment starts from a fresh and ends with ideal computational-basis measurement of every qubit. Let with . Set and .
Conditioned on any noisy word, the readout has mean and variance at most . Moreover,
For a full trial, first draw , then draw its fresh conditional readout and report . This gives , and . For every positive integer , perform independent full trials and compute the paper's estimator
The product trial law has total mass one, and
The computed experiment uses exactly noisy-circuit runs and channel applications, all on the same -qubit register. For every , the rounded Eq. (9) budget is positive and satisfies
These universal numerical bounds witness the paper's bounded-variance, Monte Carlo precision and run-overhead claims. The overhead describes a sufficient sampling budget relative to the noiseless scale, without claiming optimality for every observable.
Formalization Note The theorem uses the supplied QPR distribution directly and makes no classical runtime claim; the paper's efficient sampling and computable-sign premises concern its implementation. Locality and depth preservation require the chosen QPR construction and are not inferred from the decomposition alone. The displayed tail bound spells out “ w.h.p.”: choosing a sufficiently large fixed makes the failure small, but fixed does not imply a failure probability vanishing with .
Let be a finite family of known implementable completely positive trace-preserving maps on an -qubit device. Maps may include noisy initialization and need not be unitary or unital. Let be a length- word in a fixed finite unitary gate family, with composite unitary . Assume a supplied exact quasi-probability representation, fixed before all experimental outcomes:
where , is a probability distribution on length- noisy words, , and . Each experiment starts from a fresh and ends with ideal computational-basis measurement of every qubit. Let with . Set and .
Conditioned on any noisy word, the readout has mean and variance at most . Moreover,
For a full trial, first draw , then draw its fresh conditional readout and report . This gives , and . For every positive integer , perform independent full trials and compute the paper's estimator
The product trial law has total mass one, and
The computed experiment uses exactly noisy-circuit runs and channel applications, all on the same -qubit register. For every , the rounded Eq. (9) budget is positive and satisfies
These universal numerical bounds witness the paper's bounded-variance, Monte Carlo precision and run-overhead claims. The overhead describes a sufficient sampling budget relative to the noiseless scale, without claiming optimality for every observable.
Formalization Note The theorem uses the supplied QPR distribution directly and makes no classical runtime claim; the paper's efficient sampling and computable-sign premises concern its implementation. Locality and depth preservation require the chosen QPR construction and are not inferred from the decomposition alone. The displayed tail bound spells out “ w.h.p.”: choosing a sufficiently large fixed makes the failure small, but fixed does not imply a failure probability vanishing with .
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.
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.
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.
Efficient quantum tomography establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be integers and let be an arbitrary complex density matrix, including a singular one. Write for its decreasingly sorted spectrum. On independent copies , perform weak Schur sampling and then Keyl's normalized highest-weight POVM in the Schur module of the observed partition. The first outcome is a partition of with at most rows and has distribution . Conditional on any positive-probability partition, the second outcome has law . Put , padding the rows by zeros, and report . Then
where . The measurement is fixed by before the unknown input state is supplied. This is the paper's expected-risk guarantee for the named estimator.
Formalization Note The theorem also certifies a lawful continuous-outcome POVM, chosen before , whose Born law is the frozen computed joint law. The nonnegative risk is a Lebesgue integral in ; the finite bound ensures finiteness. The joint density relative to counting measure on partitions and probability Haar measure is , combining source equations (8), (9), and (11). This removes division by a zero Schur probability without excluding singular states.
Let be integers and let be an arbitrary complex density matrix, including a singular one. Write for its decreasingly sorted spectrum. On independent copies , perform weak Schur sampling and then Keyl's normalized highest-weight POVM in the Schur module of the observed partition. The first outcome is a partition of with at most rows and has distribution . Conditional on any positive-probability partition, the second outcome has law . Put , padding the rows by zeros, and report . Then
where . The measurement is fixed by before the unknown input state is supplied. This is the paper's expected-risk guarantee for the named estimator.
Formalization Note The theorem also certifies a lawful continuous-outcome POVM, chosen before , whose Born law is the frozen computed joint law. The nonnegative risk is a Lebesgue integral in ; the finite bound ensures finiteness. The joint density relative to counting measure on partitions and probability Haar measure is , combining source equations (8), (9), and (11). This removes division by a zero Schur probability without excluding singular states.
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.
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.
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.
Sample-optimal tomography of quantum states establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be integers. Let be the partitions of with at most rows, let , and let be the projector onto the full Schur–Weyl summand of . Write for the Schur character polynomial, so .
Independently of the unknown state, there exists a lawful continuous collective POVM with outcomes , reference measure given by counting measure on times normalized Haar measure on , and density
Its reported density matrix is .
For every positive semidefinite matrix with , the Born outcome law on the input is a probability measure. Writing , for every it satisfies
This is the original finite-copy fidelity guarantee for the equation-(10) measurement. The same measurement works for every unknown state and automatically gives the bound corresponding to its actual rank.
Let be integers. Let be the partitions of with at most rows, let , and let be the projector onto the full Schur–Weyl summand of . Write for the Schur character polynomial, so .
Independently of the unknown state, there exists a lawful continuous collective POVM with outcomes , reference measure given by counting measure on times normalized Haar measure on , and density
Its reported density matrix is .
For every positive semidefinite matrix with , the Born outcome law on the input is a probability measure. Writing , for every it satisfies
This is the original finite-copy fidelity guarantee for the equation-(10) measurement. The same measurement works for every unknown state and automatically gives the bound corresponding to its actual rank.
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.
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.
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.