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?
Single-shot decoding of good quantum LDPC codes establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix code parameters and decoder parameters . For all sufficiently large degrees (with the threshold depending only on these fixed parameters), let be a finite group with symmetric generating sets of size , whose left and right Cayley graphs are Ramanujan in the paper's sense: their second largest adjacency eigenvalue is at most . Let the binary local codes have exact rates , respectively. Each of has distance at least , and both dual tensor codes and are -product-expanding.
Construct the quadripartite quantum Tanner code on , with qubits, X checks from at and Z checks from at . Let be its actual CSS distance. Let be an X error and a binary error on the vertex-labelled Z checks. Write and let count vertices with at least one nonzero syndrome-error bit. Define
If
then Algorithm 1, receiving only and parameter , terminates and every lawful output satisfies
Local minimum-weight choices are fixed consistently before the input; infeasible local syndromes use the zero fallback. Algorithm 2 starts with zero accumulators, uses the stated weight-decrease test and minimum column/row decomposition, and halts only at zero mismatch or when no permitted move exists. Algorithm 1 returns .
This is the quantitative adversarial single-shot guarantee for the sequential Tanner decoder. With , the residual is a stabilizer, rather than necessarily the zero vector.
Formalization Note The printed theorem leaves decoder domains implicit; the range above is inherited from pp.14 and 22. The distance is an extended natural minimum; when both logical-error sets are empty it is infinite, and the threshold uses only . Termination is represented by existence of a terminal execution together with the bound for every lawful terminal execution. No stochastic residual support law is asserted.
Fix code parameters and decoder parameters . For all sufficiently large degrees (with the threshold depending only on these fixed parameters), let be a finite group with symmetric generating sets of size , whose left and right Cayley graphs are Ramanujan in the paper's sense: their second largest adjacency eigenvalue is at most . Let the binary local codes have exact rates , respectively. Each of has distance at least , and both dual tensor codes and are -product-expanding.
Construct the quadripartite quantum Tanner code on , with qubits, X checks from at and Z checks from at . Let be its actual CSS distance. Let be an X error and a binary error on the vertex-labelled Z checks. Write and let count vertices with at least one nonzero syndrome-error bit. Define
If
then Algorithm 1, receiving only and parameter , terminates and every lawful output satisfies
Local minimum-weight choices are fixed consistently before the input; infeasible local syndromes use the zero fallback. Algorithm 2 starts with zero accumulators, uses the stated weight-decrease test and minimum column/row decomposition, and halts only at zero mismatch or when no permitted move exists. Algorithm 1 returns .
This is the quantitative adversarial single-shot guarantee for the sequential Tanner decoder. With , the residual is a stabilizer, rather than necessarily the zero vector.
Formalization Note The printed theorem leaves decoder domains implicit; the range above is inherited from pp.14 and 22. The distance is an extended natural minimum; when both logical-error sets are empty it is infinite, and the threshold uses only . Termination is represented by existence of a terminal execution together with the bound for every lawful terminal execution. No stochastic residual support law is asserted.
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.
Fast Estimation of Sparse Quantum Noise establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix a sparsity exponent . There are positive constants and a threshold , depending only on this fixed exponent and public design/code choices, and a public construction of the subsampling and peeling protocol for every and integer .
The labels of the phase-free -qubit Paulis are . Let be uniform among the size- subsets of these labels. For each possible , assign arbitrary nonnegative rates with total mass one, support exactly , and on . This assignment is independent of the protocol's public randomness and observation noise. The associated channel is , and its eigenvalues are
The observed eigenvalue vector has independent centered Gaussian errors of variance , with , independent of the support and the public design. Repeated reads use the same indexed observation and are counted as queries.
The construction chooses bins with , constantly many subsampling groups, and offsets. Random offsets and binary hash matrices are sampled independently and uniformly before the hidden input. Coded offsets use a full-rank binary linear code with positive constant relative distance and a public, query-free, linear-time decoder. The decoder's realization, correction property and time bound are conclusions of the construction. Assume
Algorithms 2–4 produce a list of distinct labels with support exactly and estimated rates , zero off the reported support, satisfying
The probability averages over the uniform support, public design, Gaussian observations, and any internal decoder randomness. Every execution uses at most eigenvalue reads and classical arithmetic/indexing instructions. The computed conditional success probabilities are measurable.
This result recovers both the locations and values of sparse Pauli errors from noisy eigenvalues. It does not assert a quantum measurement sample complexity.
Formalization Note The frozen, independently reviewed program composition is used directly. It separates the ordinary -bit WHT from the symplectic -bit label pairing, resolves the printed dimensional inconsistencies as approved in the definition review, and retires peeled bins according to the graph description. The theorem does not assume successful bin detection, favorable graph events, accuracy, runtime, or independence of overlapping bin errors.
Fix a sparsity exponent . There are positive constants and a threshold , depending only on this fixed exponent and public design/code choices, and a public construction of the subsampling and peeling protocol for every and integer .
The labels of the phase-free -qubit Paulis are . Let be uniform among the size- subsets of these labels. For each possible , assign arbitrary nonnegative rates with total mass one, support exactly , and on . This assignment is independent of the protocol's public randomness and observation noise. The associated channel is , and its eigenvalues are
The observed eigenvalue vector has independent centered Gaussian errors of variance , with , independent of the support and the public design. Repeated reads use the same indexed observation and are counted as queries.
The construction chooses bins with , constantly many subsampling groups, and offsets. Random offsets and binary hash matrices are sampled independently and uniformly before the hidden input. Coded offsets use a full-rank binary linear code with positive constant relative distance and a public, query-free, linear-time decoder. The decoder's realization, correction property and time bound are conclusions of the construction. Assume
Algorithms 2–4 produce a list of distinct labels with support exactly and estimated rates , zero off the reported support, satisfying
The probability averages over the uniform support, public design, Gaussian observations, and any internal decoder randomness. Every execution uses at most eigenvalue reads and classical arithmetic/indexing instructions. The computed conditional success probabilities are measurable.
This result recovers both the locations and values of sparse Pauli errors from noisy eigenvalues. It does not assert a quantum measurement sample complexity.
Formalization Note The frozen, independently reviewed program composition is used directly. It separates the ordinary -bit WHT from the symplectic -bit label pairing, resolves the printed dimensional inconsistencies as approved in the definition review, and retires peeled bins according to the graph description. The theorem does not assume successful bin detection, favorable graph events, accuracy, runtime, or independence of overlapping bin errors.
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.
Provably efficient machine learning for quantum many-body problems establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix a finite spatial dimension , bounds on the number and geometric radius of sites in each Hamiltonian term, a local-term density bound , a spectral gap , an observable locality bound , and a confidence parameter . Consider -qubit Hamiltonians , smoothly parametrized by . Each term is Hermitian, obeys , and has directional derivative of operator norm at most one in every Euclidean unit parameter direction. These properties hold throughout the cube; smoothness at its boundary uses a local smooth extension. Every Hamiltonian has an excited energy and a gap at least above its entire ground eigenspace. Let be the normalized projector onto that eigenspace, allowing degeneracy.
For a fixed Hermitian observable , each term supported on at most qubits (not necessarily neighboring), choose a norm budget satisfying . A smaller norm budget may be replaced by one. There are uniform positive constants, depending only on the fixed physical bounds, , and , such that for every fixed mean-squared error tolerance and all sufficiently large , public sample counts, cutoffs, and actual classical arithmetic/RAM programs can be selected before the unknown Hamiltonian family, training draw, observable entries, and test parameter. The training set consists of independent uniform parameter draws, with one fresh-copy randomized Pauli snapshot at each point. Pauli axes are independently uniform; the joint measurement outcomes obey the Born law.
The named predictor is
For each observable fixed before the training draw,
with and computed classical training and prediction work . The compact representation stores real parameter words and six-valued labels, encodable in bits. The programs read and store those data and compute the observable value; they do not materialize the represented matrix. Ground-state preparation and data generation are excluded from this classical work.
For every fixed subsystem of at most qubits, separately with confidence at least ,
Thus taking gives the informal constant trace-norm error on a fixed few-body reduced matrix. This conversion uses the finite Pauli expansion and allocates confidence to its coefficients; it leaves the polynomial-in-, linear-in- conclusion intact at fixed accuracy and locality.
This result describes generalization in population average for the source's compact shadow predictor. It asserts neither pointwise error nor simultaneous accuracy on all observables or subsystems, and does not require the predicted representation to be positive or trace one.
Formalization Note Theorem 3 on PDF pp.29–30 explicitly identifies itself as the detailed restatement of Theorem 1. Its Eq. (F3) prints exact ground-state labels, whereas its premise and Eqs. (2), (E3), and (F27) specify shadow labels; the latter determine the model above. This discrepancy and the nonperiodic-boundary gap in Lemma 2 are recorded for independent source moderation, without adding periodicity or a gradient bound as hypotheses.
Fix a finite spatial dimension , bounds on the number and geometric radius of sites in each Hamiltonian term, a local-term density bound , a spectral gap , an observable locality bound , and a confidence parameter . Consider -qubit Hamiltonians , smoothly parametrized by . Each term is Hermitian, obeys , and has directional derivative of operator norm at most one in every Euclidean unit parameter direction. These properties hold throughout the cube; smoothness at its boundary uses a local smooth extension. Every Hamiltonian has an excited energy and a gap at least above its entire ground eigenspace. Let be the normalized projector onto that eigenspace, allowing degeneracy.
For a fixed Hermitian observable , each term supported on at most qubits (not necessarily neighboring), choose a norm budget satisfying . A smaller norm budget may be replaced by one. There are uniform positive constants, depending only on the fixed physical bounds, , and , such that for every fixed mean-squared error tolerance and all sufficiently large , public sample counts, cutoffs, and actual classical arithmetic/RAM programs can be selected before the unknown Hamiltonian family, training draw, observable entries, and test parameter. The training set consists of independent uniform parameter draws, with one fresh-copy randomized Pauli snapshot at each point. Pauli axes are independently uniform; the joint measurement outcomes obey the Born law.
The named predictor is
For each observable fixed before the training draw,
with and computed classical training and prediction work . The compact representation stores real parameter words and six-valued labels, encodable in bits. The programs read and store those data and compute the observable value; they do not materialize the represented matrix. Ground-state preparation and data generation are excluded from this classical work.
For every fixed subsystem of at most qubits, separately with confidence at least ,
Thus taking gives the informal constant trace-norm error on a fixed few-body reduced matrix. This conversion uses the finite Pauli expansion and allocates confidence to its coefficients; it leaves the polynomial-in-, linear-in- conclusion intact at fixed accuracy and locality.
This result describes generalization in population average for the source's compact shadow predictor. It asserts neither pointwise error nor simultaneous accuracy on all observables or subsystems, and does not require the predicted representation to be positive or trace one.
Formalization Note Theorem 3 on PDF pp.29–30 explicitly identifies itself as the detailed restatement of Theorem 1. Its Eq. (F3) prints exact ground-state labels, whereas its premise and Eqs. (2), (E3), and (F27) specify shadow labels; the latter determine the model above. This discrepancy and the nonperiodic-boundary gap in Lemma 2 are recorded for independent source moderation, without adding periodicity or a gradient bound as hypotheses.
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.
Foundations for learning from noisy quantum experiments establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix a positive finite dimension and finite labelled sets of preparation actions, dynamics actions, measurement actions, and measurement outcomes. Let be any set of world models on : every preparation is a density matrix, every dynamics action is a CPTP map, and each measurement is a POVM. The model class may be uncountable and may contain equivalent descriptions.
Suppose every is universal: some preparation is pure; some finite collection of dynamics actions implements exact unitary channels whose representatives generate a dense subgroup of ; and some measurement effect is not proportional to the identity. These witnessing actions and their physical descriptions are unknown and may vary between worlds. Mathematical inverses enter the generated subgroup; physical access to inverse actions is not assumed.
Then there exists a fixed family of finite classical experimental procedures, chosen before the unknown world. Each procedure adaptively chooses experiments that freshly prepare , apply a finite word of the available dynamics actions, and measure one of the available POVMs. Its description output is denoted . For every , every , and every , there exists such that for all there is one unitary or anti-unitary gauge satisfying
Here is computed from the experimental outcome probabilities and internal classical randomization of . A unitary gauge has the form ; an anti-unitary gauge has the form . The same gauge is fixed outside all three collections of probability clauses. Both norms are unhalved. The output estimates need not themselves be lawful quantum objects.
The result establishes learnability of all labelled operations from untrusted experiments under universality. It gives eventual accuracy for each world, with no uniform sample bound, polynomial complexity guarantee, or certified accuracy-based stopping rule.
Formalization Note The finite-action scope is explicit in Theorem D.1 (PDF p.21), although the main-text Theorem 2 does not explicitly restrict the action sets. The stage-indexed interpretation follows the precision-halving procedure in D.2 (p.23) and D.7 (p.33).
Fix a positive finite dimension and finite labelled sets of preparation actions, dynamics actions, measurement actions, and measurement outcomes. Let be any set of world models on : every preparation is a density matrix, every dynamics action is a CPTP map, and each measurement is a POVM. The model class may be uncountable and may contain equivalent descriptions.
Suppose every is universal: some preparation is pure; some finite collection of dynamics actions implements exact unitary channels whose representatives generate a dense subgroup of ; and some measurement effect is not proportional to the identity. These witnessing actions and their physical descriptions are unknown and may vary between worlds. Mathematical inverses enter the generated subgroup; physical access to inverse actions is not assumed.
Then there exists a fixed family of finite classical experimental procedures, chosen before the unknown world. Each procedure adaptively chooses experiments that freshly prepare , apply a finite word of the available dynamics actions, and measure one of the available POVMs. Its description output is denoted . For every , every , and every , there exists such that for all there is one unitary or anti-unitary gauge satisfying
Here is computed from the experimental outcome probabilities and internal classical randomization of . A unitary gauge has the form ; an anti-unitary gauge has the form . The same gauge is fixed outside all three collections of probability clauses. Both norms are unhalved. The output estimates need not themselves be lawful quantum objects.
The result establishes learnability of all labelled operations from untrusted experiments under universality. It gives eventual accuracy for each world, with no uniform sample bound, polynomial complexity guarantee, or certified accuracy-based stopping rule.
Formalization Note The finite-action scope is explicit in Theorem D.1 (PDF p.21), although the main-text Theorem 2 does not explicitly restrict the action sets. The stage-indexed interpretation follows the precision-halving procedure in D.2 (p.23) and D.7 (p.33).
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.
Robust shadow estimation establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Consider Protocol 1 of Chen, Yu, Zeng and Flammia on qubits, with Hilbert space dimension . The same completely positive, trace-preserving noise channel acts after each ideal global Clifford gate; fixed computational-basis measurement noise is absorbed into . Calibration perfectly prepares . The full Clifford group modulo global phase is sampled uniformly and calibration shots are independent and identically distributed.
Let and . Define the Z-basis average fidelity by , and suppose . Set
The printed sample scale in Theorem 7 is . Interpret its real-valued batch parameters operationally as positive integers and , with actual calibration count .
For each recorded ideal Clifford and noisy outcome , compute . Let be the median of the means of batches of such scores. The estimated inverse sends an operator to . Let , where removes off-diagonal computational-basis entries, and let .
With probability at least over calibration records, and the subsequent single-shot retrieval expectation satisfies, simultaneously for every Hermitian observable and every density matrix ,
Here is the operator norm, and the expectation is conditional on the calibration result. This guarantee controls the systematic, asymptotic bias of robust shadow retrieval; it applies to all observables and states on the same successful calibration event.
Formalization Note The statement retains the printed factor. The source proof's substitution instead gives from the stated variance bound; this discrepancy and the integer rounding interpretation remain subject to independent source moderation. The product of rounded batch parameters is not asserted to equal, or be bounded above by the ceiling of, the printed total scale. The frozen calibration probability law, overlap scores, median and retrieval expectation compute the named protocol directly.
Consider Protocol 1 of Chen, Yu, Zeng and Flammia on qubits, with Hilbert space dimension . The same completely positive, trace-preserving noise channel acts after each ideal global Clifford gate; fixed computational-basis measurement noise is absorbed into . Calibration perfectly prepares . The full Clifford group modulo global phase is sampled uniformly and calibration shots are independent and identically distributed.
Let and . Define the Z-basis average fidelity by , and suppose . Set
The printed sample scale in Theorem 7 is . Interpret its real-valued batch parameters operationally as positive integers and , with actual calibration count .
For each recorded ideal Clifford and noisy outcome , compute . Let be the median of the means of batches of such scores. The estimated inverse sends an operator to . Let , where removes off-diagonal computational-basis entries, and let .
With probability at least over calibration records, and the subsequent single-shot retrieval expectation satisfies, simultaneously for every Hermitian observable and every density matrix ,
Here is the operator norm, and the expectation is conditional on the calibration result. This guarantee controls the systematic, asymptotic bias of robust shadow retrieval; it applies to all observables and states on the same successful calibration event.
Formalization Note The statement retains the printed factor. The source proof's substitution instead gives from the stated variance bound; this discrepancy and the integer rounding interpretation remain subject to independent source moderation. The product of rounded batch parameters is not asserted to equal, or be bounded above by the ceiling of, the printed total scale. The frozen calibration probability law, overlap scores, median and retrieval expectation compute the named protocol directly.
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.
A Grand Unification of Quantum Algorithms establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix a nonnegative integer , put , and choose real phases . There are complex polynomials , depending only on these phases and , with , , and respective parities and modulo , such that
For every finite quantum register, every pair of normalized pure states in that register, and every unitary with a real nonzero amplitude , define the available exact rank-one phase shifts and for real . Then
The product is written in increasing from left to right, and its rightmost acts first. Normalization and unitarity imply ; the endpoints are allowed. Parity means and .
This construction applies one uniform polynomial to a privileged transition amplitude and connects amplitude amplification with quantum signal processing.
Formalization Note The finite register is a Euclidean space over an arbitrary finite basis type. The frozen positive-sign rank-one phase shifts and sequence encode Eq. (13) exactly. The complementary polynomial is existentially quantified with before the register, states, unitary and amplitude. The zero polynomial is allowed as , including when .
Fix a nonnegative integer , put , and choose real phases . There are complex polynomials , depending only on these phases and , with , , and respective parities and modulo , such that
For every finite quantum register, every pair of normalized pure states in that register, and every unitary with a real nonzero amplitude , define the available exact rank-one phase shifts and for real . Then
The product is written in increasing from left to right, and its rightmost acts first. Normalization and unitarity imply ; the endpoints are allowed. Parity means and .
This construction applies one uniform polynomial to a privileged transition amplitude and connects amplitude amplification with quantum signal processing.
Formalization Note The finite register is a Euclidean space over an arbitrary finite basis type. The frozen positive-sign rank-one phase shifts and sequence encode Eq. (13) exactly. The complementary polynomial is existentially quantified with before the register, states, unitary and amplitude. The zero polynomial is allowed as , including when .
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 Expander Codes establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix positive integer degrees and positive real constants , with . There are a deterministic classical decoder, a constant , and an integer , all chosen before the graph sizes and inputs, with the following properties.
Let be any finite simple bipartite graph with , left degree and right degree . For every with , require , where denotes its neighboring vertices. Require the corresponding right expansion for every with .
Form the self hypergraph-product CSS code on the tagged coordinates , of length . Write for the binary incidence matrix with rows and columns , and set , . Let and be their respective binary row spaces.
On every syndrome input, the decoder terminates and realizes the Section 3 small-set-flip algorithm, treating the two components independently. Each step flips a nonempty subset of an opposite generator's support, strictly reduces syndrome weight, and maximizes the decrease divided by the number of flipped coordinates. The deterministic implementation fixes its choices among the finitely many tied candidates. A zero syndrome returns the accumulated correction; a nonzero syndrome with no improving flip returns failure. Whenever , its total uniform-cost word-machine instruction count, together with the cost of loading its adjacency-list and syndrome input, is at most .
For every binary error pair on , let count coordinates on which at least one component is nonzero. If
then on the exact syndrome the decoder returns a correction satisfying
Correctness holds at every admissible finite size. This is an exact adversarial decoding guarantee for the associated quantum code, with linear classical runtime when degrees are fixed.
Formalization Note The positive-degree, nonempty-part convention used in the paper's proof is explicit. Equation (6)'s mixed coordinate names are read as the supports of the rows fixed by Equation (1) and the incidence formulas. These source clarifications are disclosed for independent moderation; the strict threshold and all constants in it are unchanged. Runtime and realization are conclusions about an executable classical machine; no progress or minimum-distance assertion is a hypothesis.
Fix positive integer degrees and positive real constants , with . There are a deterministic classical decoder, a constant , and an integer , all chosen before the graph sizes and inputs, with the following properties.
Let be any finite simple bipartite graph with , left degree and right degree . For every with , require , where denotes its neighboring vertices. Require the corresponding right expansion for every with .
Form the self hypergraph-product CSS code on the tagged coordinates , of length . Write for the binary incidence matrix with rows and columns , and set , . Let and be their respective binary row spaces.
On every syndrome input, the decoder terminates and realizes the Section 3 small-set-flip algorithm, treating the two components independently. Each step flips a nonempty subset of an opposite generator's support, strictly reduces syndrome weight, and maximizes the decrease divided by the number of flipped coordinates. The deterministic implementation fixes its choices among the finitely many tied candidates. A zero syndrome returns the accumulated correction; a nonzero syndrome with no improving flip returns failure. Whenever , its total uniform-cost word-machine instruction count, together with the cost of loading its adjacency-list and syndrome input, is at most .
For every binary error pair on , let count coordinates on which at least one component is nonzero. If
then on the exact syndrome the decoder returns a correction satisfying
Correctness holds at every admissible finite size. This is an exact adversarial decoding guarantee for the associated quantum code, with linear classical runtime when degrees are fixed.
Formalization Note The positive-degree, nonempty-part convention used in the paper's proof is explicit. Equation (6)'s mixed coordinate names are read as the supports of the rows fixed by Equation (1) and the incidence formulas. These source clarifications are disclosed for independent moderation; the strict threshold and all constants in it are unchanged. Runtime and realization are conclusions about an executable classical machine; no progress or minimum-distance assertion is 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.
Simulating Hamiltonian dynamics with a truncated Taylor series establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let , let be known coefficients, and let and . For any unitary matrices on a -dimensional system whose sum is Hermitian, count coherent signed controlled selection and its inverse as the access operations. Set , , and .
There are absolute constants , , and , chosen before all instance data, for which the following holds. Choose the least nonnegative truncation order satisfying . From alone one can construct the paper's segmented Taylor simulator, before choosing the term oracle or the input state. The simulator uses segments of duration and the remaining positive duration as its final segment. Each segment uses the Taylor LCU, the normalization ancilla, and robust oblivious amplification , with fresh zero ancillas that are subsequently discarded.
If is the standard isometric embedding of the -dimensional system into qubits, denotes the implemented unconditional channel, and is any unit vector, then
Every segment's truncated operator differs from its exact evolution by at most in spectral norm. The same construction also approximates the padded Hamiltonian on every normalized state of the full qubit register. The number of signed-selector calls is at most ; the number of other elementary gates is at most ; and peak ancillary qubits, treating the selector as the primitive access operation, are at most .
For and , the order and counted access cost satisfy
If a signed-selector implementation has elementary gates and clean workspace qubits, there are elementary segment circuits implementing the same simulator, returning that workspace to zero, with total gate count at most . In the special case in which the padded terms are tensor products of single-qubit Pauli matrices, such circuits exist with total gate count at most and peak ancillary qubits at most .
This gives the paper's time-independent simulation cost without requiring commuting, self-inverse, Hermitian individual terms or a bound on .
Formalization Note The paper does not name the reduced-state norm. Trace norm without the factor is used to make its discard-ancillas and error-accumulation argument precise. Eq. (10)'s failure coefficient, Eq. (16)'s partial trace of a ket, and the printed order-register amplitude are corrected as recorded in the audit. Arbitrary one- and two-qubit gates are used, with exact rotations and inverses; finite-gate-set synthesis overhead is outside the claim.
Let , let be known coefficients, and let and . For any unitary matrices on a -dimensional system whose sum is Hermitian, count coherent signed controlled selection and its inverse as the access operations. Set , , and .
There are absolute constants , , and , chosen before all instance data, for which the following holds. Choose the least nonnegative truncation order satisfying . From alone one can construct the paper's segmented Taylor simulator, before choosing the term oracle or the input state. The simulator uses segments of duration and the remaining positive duration as its final segment. Each segment uses the Taylor LCU, the normalization ancilla, and robust oblivious amplification , with fresh zero ancillas that are subsequently discarded.
If is the standard isometric embedding of the -dimensional system into qubits, denotes the implemented unconditional channel, and is any unit vector, then
Every segment's truncated operator differs from its exact evolution by at most in spectral norm. The same construction also approximates the padded Hamiltonian on every normalized state of the full qubit register. The number of signed-selector calls is at most ; the number of other elementary gates is at most ; and peak ancillary qubits, treating the selector as the primitive access operation, are at most .
For and , the order and counted access cost satisfy
If a signed-selector implementation has elementary gates and clean workspace qubits, there are elementary segment circuits implementing the same simulator, returning that workspace to zero, with total gate count at most . In the special case in which the padded terms are tensor products of single-qubit Pauli matrices, such circuits exist with total gate count at most and peak ancillary qubits at most .
This gives the paper's time-independent simulation cost without requiring commuting, self-inverse, Hermitian individual terms or a bound on .
Formalization Note The paper does not name the reduced-state norm. Trace norm without the factor is used to make its discard-ancillas and error-accumulation argument precise. Eq. (10)'s failure coefficient, Eq. (16)'s partial trace of a ket, and the printed order-register amplitude are corrected as recorded in the audit. Arbitrary one- and two-qubit gates are used, with exact rotations and inverses; finite-gate-set synthesis overhead is outside the claim.
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 algorithm for systems of linear equations with exponentially improved dependence on precision establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let , let be Hermitian and invertible with , and let be a supplied upper bound on its condition number. Let , and write and . The coherent preparation procedure prepares in polynomial time in on the -qubit state register; its inverse is available. Put , with .
There are absolute positive constants and fixed asymptotic thresholds, chosen before all public parameters and hidden inputs, with the following two conclusions.
The reduction outputs a success flag with probability at least . Conditional on success, its system output is the pure state whose vector representative is the normalized action of the actually simulated Fourier block on , and
This representative is fixed by the Fourier block; the error is not minimized over global phases. Failure output is unrestricted.
The sum counts the two matrix-oracle operations separately and then adds them. Short columns may be padded with zero entries, the location lists need not be sorted, and injectivity of each in-place location map is required. Entries use a public ordinary signed binary complex-number format. This is the exact-entry branch of the paper's access model; sufficiently accurate finite-precision access is covered through the simulator error budget. No controlled access to the input black boxes is assumed. External gates exclude internal implementations of and ; inlining either subroutine adds its per-call gate cost times its corresponding number of calls.
The bounds establish logarithmic dependence on output precision for quantum state preparation. The number of calls is bounded in the worst case using a finite capped amplification routine.
Formalization Note The Lean conclusion includes both clauses in one theorem and fixes the reduction and sparse circuits before quantifying over hidden inputs. The preparation-time polynomial and binary format are public parameters. Successful output is represented by a subnormalized pure density matrix together with its explicitly specified vector representative and direct vector error. Invalid qubit padding cannot count as successful output.
Correction to the printed source.
Printed: Page 8 says a worst-case amplification guarantee needs an 'upper bound on the probability q'; page 15 writes 'τ := y_J y_K'.
Corrected: Use a known positive lower bound on q for capped amplification, as Corollary 10 does, and read the maximum evolution time as y_J z_K.
Reason: The required amplification work grows when q decreases; Corollary 10 provides q bounded below using known coefficient mass. The Fourier times are y_j z_k in (18), (31), (52); y_K is not the defined z cutoff.
Let , let be Hermitian and invertible with , and let be a supplied upper bound on its condition number. Let , and write and . The coherent preparation procedure prepares in polynomial time in on the -qubit state register; its inverse is available. Put , with .
There are absolute positive constants and fixed asymptotic thresholds, chosen before all public parameters and hidden inputs, with the following two conclusions.
The reduction outputs a success flag with probability at least . Conditional on success, its system output is the pure state whose vector representative is the normalized action of the actually simulated Fourier block on , and
This representative is fixed by the Fourier block; the error is not minimized over global phases. Failure output is unrestricted.
The sum counts the two matrix-oracle operations separately and then adds them. Short columns may be padded with zero entries, the location lists need not be sorted, and injectivity of each in-place location map is required. Entries use a public ordinary signed binary complex-number format. This is the exact-entry branch of the paper's access model; sufficiently accurate finite-precision access is covered through the simulator error budget. No controlled access to the input black boxes is assumed. External gates exclude internal implementations of and ; inlining either subroutine adds its per-call gate cost times its corresponding number of calls.
The bounds establish logarithmic dependence on output precision for quantum state preparation. The number of calls is bounded in the worst case using a finite capped amplification routine.
Formalization Note The Lean conclusion includes both clauses in one theorem and fixes the reduction and sparse circuits before quantifying over hidden inputs. The preparation-time polynomial and binary format are public parameters. Successful output is represented by a subnormalized pure density matrix together with its explicitly specified vector representative and direct vector error. Invalid qubit padding cannot count as successful output.
Correction to the printed source.
Printed: Page 8 says a worst-case amplification guarantee needs an 'upper bound on the probability q'; page 15 writes 'τ := y_J y_K'.
Corrected: Use a known positive lower bound on q for capped amplification, as Corollary 10 does, and read the maximum evolution time as y_J z_K.
Reason: The required amplification work grows when q decreases; Corollary 10 provides q bounded below using known coefficient mass. The Fourier times are y_j z_k in (18), (31), (52); y_K is not the defined z cutoff.
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 Ramsey number R(5,5) has remained open since the 1960s. The best known bounds are 43 ≤ R(5,5) ≤ 48, where the lower bound was first established by Exoo (1989) via computational search. This mission formalizes an independent verification using novel GF(p) polynomial seeding.
The Ramsey number R(s,t) is the smallest n such that every 2-coloring of the complete graph K_n contains either a red K_s or a blue K_t.
Goal: R(5,5) ≥ 43
Established by exhibiting an explicit 2-coloring of K₄₂ with no monochromatic K₅.
This mission produces a machine-verified certificate of R(5,5) ≥ 43 via the first formalized GF(p) polynomial construction for Ramsey colorings.
The central difficulty is scale: verifying zero violations requires checking all C(42,5) = 850,668 five-element subsets.
Quantum algorithms for zero-sum games establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be positive integers and let be the payoff matrix of a zero-sum game. Alice maximizes the payoff and Bob minimizes it. Let denote the probability simplexes and let
For and , run the fixed-accuracy branch of Algorithm 1 for
completed updates. Starting with zero accumulators , each update independently draws with probabilities proportional to and with probabilities proportional to , then adds to and to . The final accumulators are normalized to give .
There is a classical randomized implementation, chosen independently of the entries of , whose output distribution is exactly the distribution of these normalized updates. Every update makes exactly entry queries and uses numerical work; initialization and final normalization also use work and make no entry queries. The constants and dimension threshold in these work bounds are universal. In particular, the implementation makes exactly entry queries and satisfies the joint guarantee
This result supplies the classical dense-entry implementation and equilibrium guarantee for Algorithm 1.
Formalization Note Numerical work uses the ideal arithmetic and finite-distribution sampling model of the proof: exponential evaluation, array operations and linear sampling passes are charged explicitly. This is not a finite-bit running-time claim. The integer iteration count is taken from the fixed-accuracy clause of Lemma 1, which Lemma 3 invokes. Updates are indexed by their number of completed steps, resolving Algorithm 1's initialization/indexing discrepancy.
Let be positive integers and let be the payoff matrix of a zero-sum game. Alice maximizes the payoff and Bob minimizes it. Let denote the probability simplexes and let
For and , run the fixed-accuracy branch of Algorithm 1 for
completed updates. Starting with zero accumulators , each update independently draws with probabilities proportional to and with probabilities proportional to , then adds to and to . The final accumulators are normalized to give .
There is a classical randomized implementation, chosen independently of the entries of , whose output distribution is exactly the distribution of these normalized updates. Every update makes exactly entry queries and uses numerical work; initialization and final normalization also use work and make no entry queries. The constants and dimension threshold in these work bounds are universal. In particular, the implementation makes exactly entry queries and satisfies the joint guarantee
This result supplies the classical dense-entry implementation and equilibrium guarantee for Algorithm 1.
Formalization Note Numerical work uses the ideal arithmetic and finite-distribution sampling model of the proof: exponential evaluation, array operations and linear sampling passes are charged explicitly. This is not a finite-bit running-time claim. The integer iteration count is taken from the fixed-accuracy clause of Lemma 1, which Lemma 3 invokes. Updates are indexed by their number of completed steps, resolving Algorithm 1's initialization/indexing discrepancy.
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.
Convex optimization using quantum oracles establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let , let be convex, and let be convex. Assume , , , and . On this closed cube, assume that is -Lipschitz in the Euclidean norm. Suppose finite binary quantum value-oracle access is available on a sufficiently fine hypergrid of this cube: the standard unitary preserves the query index and adds a fixed-point value within of . Its inverse is also available.
There is a quantum algorithm, fixed from the known parameters, grid and encoding before the unknown function and oracle, whose output satisfies, with probability at least , simultaneously for every ,
The total number of forward and inverse oracle calls is , with an absolute constant uniform over all parameters, domains, functions, encodings, precision and oracle implementations. Precisely, there are absolute and such that this count is at most when ; a successful finite algorithm exists throughout the admissible parameter range.
The same conclusion and query bound hold for a relational unitary -approximator: on each clean query input it preserves the input and yields a value within with probability at least , with arbitrary normalized conditional garbage. Access to its inverse is allowed.
This result supplies a uniformly valid approximate supporting hyperplane without assuming differentiability or a smoothness bound on the objective.
Formalization Note The sufficiently fine access condition is explicit geometric coverage of compatible finite-difference and uniform-center grids and translated/scaled Definition-13 midpoint grids. An existential positive resolution threshold allows arbitrarily small mesh and radius-rounding budgets. Known-parameter arithmetic guards preserve the printed constants; neither local near-linearity nor small curvature is an input hypothesis. Grid indices remain exact finite labels under their known affine embedding. The real extension of outside is immaterial. No gate bound or convex-set oracle reduction is asserted.
Let , let be convex, and let be convex. Assume , , , and . On this closed cube, assume that is -Lipschitz in the Euclidean norm. Suppose finite binary quantum value-oracle access is available on a sufficiently fine hypergrid of this cube: the standard unitary preserves the query index and adds a fixed-point value within of . Its inverse is also available.
There is a quantum algorithm, fixed from the known parameters, grid and encoding before the unknown function and oracle, whose output satisfies, with probability at least , simultaneously for every ,
The total number of forward and inverse oracle calls is , with an absolute constant uniform over all parameters, domains, functions, encodings, precision and oracle implementations. Precisely, there are absolute and such that this count is at most when ; a successful finite algorithm exists throughout the admissible parameter range.
The same conclusion and query bound hold for a relational unitary -approximator: on each clean query input it preserves the input and yields a value within with probability at least , with arbitrary normalized conditional garbage. Access to its inverse is allowed.
This result supplies a uniformly valid approximate supporting hyperplane without assuming differentiability or a smoothness bound on the objective.
Formalization Note The sufficiently fine access condition is explicit geometric coverage of compatible finite-difference and uniform-center grids and translated/scaled Definition-13 midpoint grids. An existential positive resolution threshold allows arbitrarily small mesh and radius-rounding budgets. Known-parameter arithmetic guards preserve the printed constants; neither local near-linearity nor small curvature is an input hypothesis. Grid indices remain exact finite labels under their known affine embedding. The real extension of outside is immaterial. No gate bound or convex-set oracle reduction is asserted.
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.
Predicting Many Properties of a Quantum System from Very Few Measurements establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let , , and let be any density matrix on an -qubit system. Fix a tomographically complete measurement primitive: a probability ensemble of unitary matrices, whose averaged measurement channel is invertible. A shot samples , measures in the computational basis with Born outcome , and forms the snapshot . The ensemble may be continuous and need not be uniform.
Fix Hermitian observables , independently of the sampled outcomes, and , . For a Hermitian matrix , define
Set , , and . Here is natural logarithm. Draw exactly independent snapshots in batches of shots. Let be the median of the batch means of , using the lower median for even . Then
This is the paper's simultaneous linear-prediction guarantee, with observable-dependent sample size and no purity, locality, positivity, operator-norm, or computational-cost restriction on the observables.
Formalization Note The printed zero endpoints in (S13) are undefined and are excluded. Integer counts are rounded upward and each batch has at least one sample, including scalar observables with . Lean concludes positivity of the constructed counts instead of assuming it. Real parts of traces express the real expectations of Hermitian observables.
Let , , and let be any density matrix on an -qubit system. Fix a tomographically complete measurement primitive: a probability ensemble of unitary matrices, whose averaged measurement channel is invertible. A shot samples , measures in the computational basis with Born outcome , and forms the snapshot . The ensemble may be continuous and need not be uniform.
Fix Hermitian observables , independently of the sampled outcomes, and , . For a Hermitian matrix , define
Set , , and . Here is natural logarithm. Draw exactly independent snapshots in batches of shots. Let be the median of the batch means of , using the lower median for even . Then
This is the paper's simultaneous linear-prediction guarantee, with observable-dependent sample size and no purity, locality, positivity, operator-norm, or computational-cost restriction on the observables.
Formalization Note The printed zero endpoints in (S13) are undefined and are excluded. Integer counts are rounded upward and each batch has at least one sample, including scalar observables with . Lean concludes positivity of the constructed counts instead of assuming it. Real parts of traces express the real expectations of Hermitian observables.
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 LDPC codes with positive rate and minimum distance proportional to n^{1/2} establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let have linearly independent rows, where , and let . Write for the minimum Hamming weight of a nonzero word of , with when . Form the two parity-check matrices
The qubit coordinates are the disjoint union , explicitly reindexed as for . Set and . Then , , and , so these matrices define a valid CSS code. Its parameters are
Here is the CSS coding subspace, denotes Hamming weight, and an empty minimum is infinity. For every row index and column index , the exact check weights are
Consequently, if every row of has weight at most and every column has weight at most , every row of either constructed check matrix has weight at most . Bounds independent of blocklength therefore preserve the LDPC property; no regularity or self-orthogonality of the input code is required.
This construction transfers the classical code's minimum distance to a quantum CSS code while giving the exact logical dimension and preserving sparse checks.
Let have linearly independent rows, where , and let . Write for the minimum Hamming weight of a nonzero word of , with when . Form the two parity-check matrices
The qubit coordinates are the disjoint union , explicitly reindexed as for . Set and . Then , , and , so these matrices define a valid CSS code. Its parameters are
Here is the CSS coding subspace, denotes Hamming weight, and an empty minimum is infinity. For every row index and column index , the exact check weights are
Consequently, if every row of has weight at most and every column has weight at most , every row of either constructed check matrix has weight at most . Bounds independent of blocklength therefore preserve the LDPC property; no regularity or self-orthogonality of the input code is required.
This construction transfers the classical code's minimum distance to a quantum CSS code while giving the exact logical dimension and preserving sparse checks.
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 SDP Solvers: Large Speed-ups, Optimality, and Applications to Quantum Learning establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let , let , and let for . Let be positive semidefinite, and set
Assume and , with , , and .
Oracle D.1 and its inverse write exact binary representations of both component traces at initialized answer registers. Oracle D.2 and its inverse jointly prepare arbitrary normalized purifications of when that trace is nonzero. At trace zero they prepare arbitrary normalized states, whose zero-weight contributions are ignored. All other finite-register actions, purification phases, and actions on unused qubit labels are arbitrary. Each source tensor factor is separately encoded in binary, in the displayed source order. The actual supplied qubit oracles must restrict to these finite-register unitaries; a known identity extension or controlled black-box operation is not assumed.
There are absolute and such that, for each public and binary trace format, a sampler and workspace can be chosen before the hidden PSD matrices and before all compatible oracle unitaries. It terminates almost surely, has a summable unconditional output density , and satisfies
Here counts one- and two-qubit gates, preparations and measurements, and counts actual oracle or inverse calls. Finite classical draws are free in this model. The same bound holds with any in place of .
Printed / changed / why. Lemma 12 prints . The corrected elementary-gate statement includes to charge preparation of an indexed-oracle address, and excludes empty support to avoid a literal zero-cost maximally mixed state. Zero components are retained according to the paper's own application on p.29; the arbitrary-state convention completes the otherwise undefined normalized quotient without changing any nonzero component. Precision uses the unhalved trace norm in Eqs. (F.15)–(F.17); expected repetition is stated on p.33.
Correction to the printed source.
Printed: For S subset [m], Lemma 12 gives |S| * poly(log n, r_K, B_K, epsilon inverse) quantum gates and D.1/D.2 queries; D.2 writes A_j^sign / Tr(A_j^sign) without a zero-trace convention.
Corrected: Require S nonempty and include an elementary address-cost factor 1 + log m in both the |S| bound and its Phi corollary. Permit arbitrary normalized D.2 outputs for zero PSD components and arbitrary unitary completions on unused qubit labels, preserving the promises on every nonzero component.
Reason: The all-zero initialized elementary-gate model must prepare an m-valued address: for singleton S at a distant index this requires Omega(log m) one- or two-qubit gates, while the printed bound has no m dependence. Empty S makes the printed bound zero although K=0 has Gibbs state I/n, which is mixed for n>1. The paper explicitly applies Lemma 12 with zero components on p.29, and Lemma 11 assigns them zero selection probability; excluding them drops source cases. No nonzero quotient, Gibbs target, rank/trace bound, oracle count, accuracy, or quantifier order is changed.
Let , let , and let for . Let be positive semidefinite, and set
Assume and , with , , and .
Oracle D.1 and its inverse write exact binary representations of both component traces at initialized answer registers. Oracle D.2 and its inverse jointly prepare arbitrary normalized purifications of when that trace is nonzero. At trace zero they prepare arbitrary normalized states, whose zero-weight contributions are ignored. All other finite-register actions, purification phases, and actions on unused qubit labels are arbitrary. Each source tensor factor is separately encoded in binary, in the displayed source order. The actual supplied qubit oracles must restrict to these finite-register unitaries; a known identity extension or controlled black-box operation is not assumed.
There are absolute and such that, for each public and binary trace format, a sampler and workspace can be chosen before the hidden PSD matrices and before all compatible oracle unitaries. It terminates almost surely, has a summable unconditional output density , and satisfies
Here counts one- and two-qubit gates, preparations and measurements, and counts actual oracle or inverse calls. Finite classical draws are free in this model. The same bound holds with any in place of .
Printed / changed / why. Lemma 12 prints . The corrected elementary-gate statement includes to charge preparation of an indexed-oracle address, and excludes empty support to avoid a literal zero-cost maximally mixed state. Zero components are retained according to the paper's own application on p.29; the arbitrary-state convention completes the otherwise undefined normalized quotient without changing any nonzero component. Precision uses the unhalved trace norm in Eqs. (F.15)–(F.17); expected repetition is stated on p.33.
Correction to the printed source.
Printed: For S subset [m], Lemma 12 gives |S| * poly(log n, r_K, B_K, epsilon inverse) quantum gates and D.1/D.2 queries; D.2 writes A_j^sign / Tr(A_j^sign) without a zero-trace convention.
Corrected: Require S nonempty and include an elementary address-cost factor 1 + log m in both the |S| bound and its Phi corollary. Permit arbitrary normalized D.2 outputs for zero PSD components and arbitrary unitary completions on unused qubit labels, preserving the promises on every nonzero component.
Reason: The all-zero initialized elementary-gate model must prepare an m-valued address: for singleton S at a distant index this requires Omega(log m) one- or two-qubit gates, while the printed bound has no m dependence. Empty S makes the printed bound zero although K=0 has Gibbs state I/n, which is mixed for n>1. The paper explicitly applies Lemma 12 with zero components on p.29, and Lemma 11 assigns them zero selection probability; excluding them drops source cases. No nonzero quotient, Gibbs target, rank/trace bound, oracle count, accuracy, or quantifier order is changed.
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.
Shadow Tomography of Quantum States establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
There are universal constants and and one explicit adaptive measurement constructor with the following property. Let be integers, let be known two-outcome measurement effects on (so ), and let . The constructor depends on these known data and not on the unknown state.
Write , , , , , and . The constructed procedure uses independent copies of the unknown state, with
For every density matrix on , a run on returns numbers satisfying
Collective measurements, adaptive measurements, temporary ancillas, and unrestricted known-data classical computation are permitted. The procedure composes physical quantum-OR decision programs, the paper's binary gentle search over signed amplified deviation effects, and classical matrix multiplicative weights. This estimates the entire specified list simultaneously without reconstructing the unknown density matrix in trace distance.
Formalization Note The finite adaptive instrument programs carry normalized Kraus families. The constructor supplies actual physical decision programs, not an assumed accuracy contract or a state oracle. The source composition is executed by chunk-local recursive definitions. The logarithm floors extend the asymptotic notation to , , and other finite boundary regimes; they introduce no additional asymptotic parameter dependence. No computation-time or gate-complexity assertion is made.
There are universal constants and and one explicit adaptive measurement constructor with the following property. Let be integers, let be known two-outcome measurement effects on (so ), and let . The constructor depends on these known data and not on the unknown state.
Write , , , , , and . The constructed procedure uses independent copies of the unknown state, with
For every density matrix on , a run on returns numbers satisfying
Collective measurements, adaptive measurements, temporary ancillas, and unrestricted known-data classical computation are permitted. The procedure composes physical quantum-OR decision programs, the paper's binary gentle search over signed amplified deviation effects, and classical matrix multiplicative weights. This estimates the entire specified list simultaneously without reconstructing the unknown density matrix in trace distance.
Formalization Note The finite adaptive instrument programs carry normalized Kraus families. The constructor supplies actual physical decision programs, not an assumed accuracy contract or a state oracle. The source composition is executed by chunk-local recursive definitions. The logarithm floors extend the asymptotic notation to , , and other finite boundary regimes; they introduce no additional asymptotic parameter dependence. No computation-time or gate-complexity assertion is made.
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 speedup of Monte Carlo methods establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be the coherent unitary representation of a randomized or quantum computation on qubits, initially in , with no intermediate measurements and with access to its inverse. Measuring the last qubits gives a bit string , whose output is the fixed value . The value-dependent flag rotation is supplied exactly; the source assumes that is easily computable. Write .
Attach a fresh flag and prepare by rotating it to . Set , , and . For any positive integer and , Algorithm 1 applies amplitude estimation independently times and returns the median . One run uses uniform control on , controlled powers of , the inverse Fourier transform of dimension , and the estimate for control outcome .
There exist positive universal constants , chosen before all sampler data and parameters, such that, with ,
Here the actual schedule consumes fresh copies of and calls to , counting controlled calls as uses.
For every :
If , the estimator returns zero with probability one for every positive integer . The bounds hold for every coherent computation, including each instance of any oracle it uses. They quantify copies and reflections separately.
This is the bounded-output mean-estimation subroutine used by the paper's later Monte Carlo algorithms.
Formalization Note The selected result is Theorem 3 on PDF pages 8–9, rather than a later bounded-variance theorem. The printed reciprocal rates at supply no finite exact-estimation claim; the reciprocal corollaries therefore use . The all-confidence bound agrees with as tends to zero. The unspecified repetition coefficient is fixed to the odd representative above. The theorem asserts no gate-time bound for computing .
Let be the coherent unitary representation of a randomized or quantum computation on qubits, initially in , with no intermediate measurements and with access to its inverse. Measuring the last qubits gives a bit string , whose output is the fixed value . The value-dependent flag rotation is supplied exactly; the source assumes that is easily computable. Write .
Attach a fresh flag and prepare by rotating it to . Set , , and . For any positive integer and , Algorithm 1 applies amplitude estimation independently times and returns the median . One run uses uniform control on , controlled powers of , the inverse Fourier transform of dimension , and the estimate for control outcome .
There exist positive universal constants , chosen before all sampler data and parameters, such that, with ,
Here the actual schedule consumes fresh copies of and calls to , counting controlled calls as uses.
For every :
If , the estimator returns zero with probability one for every positive integer . The bounds hold for every coherent computation, including each instance of any oracle it uses. They quantify copies and reflections separately.
This is the bounded-output mean-estimation subroutine used by the paper's later Monte Carlo algorithms.
Formalization Note The selected result is Theorem 3 on PDF pages 8–9, rather than a later bounded-variance theorem. The printed reciprocal rates at supply no finite exact-estimation claim; the reciprocal corollaries therefore use . The all-confidence bound agrees with as tends to zero. The unspecified repetition coefficient is fixed to the odd representative above. The theorem asserts no gate-time bound for computing .
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 Power of Two Bases: Robust and copy-optimal certification of nearly all quantum states with few-qubit measurements establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
There is a single efficient oracle procedure for certifying a pure target state using one copy of an arbitrary mixed lab state. The classical oracle returns the exact amplitudes of the target in the computational basis and in the full-register Hadamard basis, as in Definition 1 of the paper.
More precisely, there exist a polynomial resource bound , a constant , a threshold , a nonnegative sequence , and measurable sets of normalized -qubit target states such that, for all ,
For every and every density matrix on the same qubits, write . The procedure satisfies
It flips one fair classical bit and measures the first qubits either all in the basis or all in the basis, where . Given the observed prefix, it reads the oracle amplitudes for that prefix, computes the conditional target, and performs one projector/complement measurement on the fixed suffix of qubits. In the branch, the full-Hadamard oracle fiber is transformed by to obtain the physical conditional target. A zero target fiber is always rejected. The executed oracle calls, scalar instructions, and suffix circuit gates are bounded by , uniformly over normalized targets and every branch; the compiled accepting effect is the conditional target projector.
The same good set and error sequence apply simultaneously to all lab density matrices. This provides the paper's constant robustness with only one measurement involving logarithmically many qubits.
Formalization Note The suffix rounding fixes the proof's choice . Efficiency is relative to exact complex-answer classical oracle access and ideal scalar operations, with arbitrary one- and two-qubit unitaries for exact synthesis. No finite-precision or oracle-simulation cost is claimed. The Lean statement uses the concrete frozen conditional measurement program and its execution-derived resource counts, and gives the additive soundness of Theorem 1.
There is a single efficient oracle procedure for certifying a pure target state using one copy of an arbitrary mixed lab state. The classical oracle returns the exact amplitudes of the target in the computational basis and in the full-register Hadamard basis, as in Definition 1 of the paper.
More precisely, there exist a polynomial resource bound , a constant , a threshold , a nonnegative sequence , and measurable sets of normalized -qubit target states such that, for all ,
For every and every density matrix on the same qubits, write . The procedure satisfies
It flips one fair classical bit and measures the first qubits either all in the basis or all in the basis, where . Given the observed prefix, it reads the oracle amplitudes for that prefix, computes the conditional target, and performs one projector/complement measurement on the fixed suffix of qubits. In the branch, the full-Hadamard oracle fiber is transformed by to obtain the physical conditional target. A zero target fiber is always rejected. The executed oracle calls, scalar instructions, and suffix circuit gates are bounded by , uniformly over normalized targets and every branch; the compiled accepting effect is the conditional target projector.
The same good set and error sequence apply simultaneously to all lab density matrices. This provides the paper's constant robustness with only one measurement involving logarithmically many qubits.
Formalization Note The suffix rounding fixes the proof's choice . Efficiency is relative to exact complex-answer classical oracle access and ideal scalar operations, with arbitrary one- and two-qubit unitaries for exact synthesis. No finite-precision or oracle-simulation cost is claimed. The Lean statement uses the concrete frozen conditional measurement program and its execution-derived resource counts, and gives the additive soundness of Theorem 1.
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.
Approximate sampling from decoded quantum interferometry via Markov chain Monte Carlo methods establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be prime, , and satisfy for every , where . For , define the signed objective . Let and let be its minimum nonzero Hamming weight, with when .
Let have degree , satisfy , and obey . Define and . For every nonnegative integer such that ,
Equivalently, the right side is
This identity characterizes the low-order moments of the signed score under the DQI distribution through binomial moments.
Formalization Note Expectations are finite real sums. The code and its extended natural minimum distance are computed from using the frozen field-code definitions. The squared-amplitude weights are the frozen real polynomial weights; for real amplitudes they equal the computational-basis probabilities of the frozen DQI state. No additional normalization denominator is introduced.
Let be prime, , and satisfy for every , where . For , define the signed objective . Let and let be its minimum nonzero Hamming weight, with when .
Let have degree , satisfy , and obey . Define and . For every nonnegative integer such that ,
Equivalently, the right side is
This identity characterizes the low-order moments of the signed score under the DQI distribution through binomial moments.
Formalization Note Expectations are finite real sums. The code and its extended natural minimum distance are computed from using the frozen field-code definitions. The squared-amplitude weights are the frozen real polynomial weights; for real amplitudes they equal the computational-basis probabilities of the frozen DQI state. No additional normalization denominator is introduced.
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 state tomography via compressed sensing establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be the number of qubits, , and let be a fixed density matrix (positive semidefinite with trace one) of exact rank . There are absolute constants , independent of , such that the following holds for every .
Set . Independently sample unphased Pauli strings , uniformly with replacement from all tensor products of , including the identity. Suppose their exact expectations are known. Write for the set of minimizers of
The trace norm is the sum of the singular values; competitors need not be positive semidefinite and have no rank constraint. Then
Thus this specific convex program attains its minimum uniquely at the unknown state with exponentially small failure probability. The probability is over the design for each fixed state, and counts exact expectation settings, rather than physical copies or computation time.
Formalization Note Natural logarithms and integer rounding pin down the paper's asymptotic notation using its closing proof on PDF p.3. The sampling law and optimizer set are frozen definitions depending only on public , and on the design and supplied data, respectively. For , and ; trace one alone gives unique recovery.
Let be the number of qubits, , and let be a fixed density matrix (positive semidefinite with trace one) of exact rank . There are absolute constants , independent of , such that the following holds for every .
Set . Independently sample unphased Pauli strings , uniformly with replacement from all tensor products of , including the identity. Suppose their exact expectations are known. Write for the set of minimizers of
The trace norm is the sum of the singular values; competitors need not be positive semidefinite and have no rank constraint. Then
Thus this specific convex program attains its minimum uniquely at the unknown state with exponentially small failure probability. The probability is over the design for each fixed state, and counts exact expectation settings, rather than physical copies or computation time.
Formalization Note Natural logarithms and integer rounding pin down the paper's asymptotic notation using its closing proof on PDF p.3. The sampling law and optimizer set are frozen definitions depending only on public , and on the design and supplied data, respectively. For , and ; trace one alone gives unique recovery.
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 chi-squared tomography and mutual information testing establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
There are absolute constants and with the following property. For every integer dimension , supplied integer rank bound , and accuracy , one can choose a copy count and a lawful collective measurement on independent identical copies of a state, with a density matrix as its classical outcome, such that
The probability guarantee holds for every unknown positive semidefinite matrix of trace one and rank at most . The measurement is chosen using only , before . Here is Umegaki quantum relative entropy with natural logarithms: when , and otherwise; zero-eigenvalue terms use their continuous limits. The estimate may have any rank.
This gives relative entropy tomography with copies, including singular input states. Larger positive accuracies follow by running at a fixed smaller accuracy. The explicit squared-logarithm bound is stated on PDF p.12 immediately after Theorem 2.34.
Formalization Note The measurement uses the frozen general operator-valued POVM on the space of density matrices, and its output distribution is the Born law on . The extended divergence uses the frozen kernel-containment support guard.
There are absolute constants and with the following property. For every integer dimension , supplied integer rank bound , and accuracy , one can choose a copy count and a lawful collective measurement on independent identical copies of a state, with a density matrix as its classical outcome, such that
The probability guarantee holds for every unknown positive semidefinite matrix of trace one and rank at most . The measurement is chosen using only , before . Here is Umegaki quantum relative entropy with natural logarithms: when , and otherwise; zero-eigenvalue terms use their continuous limits. The estimate may have any rank.
This gives relative entropy tomography with copies, including singular input states. Larger positive accuracies follow by running at a fixed smaller accuracy. The explicit squared-logarithm bound is stated on PDF p.12 immediately after Theorem 2.34.
Formalization Note The measurement uses the frozen general operator-valued POVM on the space of density matrices, and its output distribution is the Born law on . The extended divergence uses the frozen kernel-containment support guard.
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.
Improved quantum data analysis establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
There are a universal constant and a copy-count function , depending only on the number of tests and the accuracy and failure parameters , with the following property. For every integer and every , write . Then
For every dimension , there is an online quantum protocol that begins with independent, unentangled copies of an unknown state , where is positive semidefinite and , together with a known ancillary state. Observable/threshold pairs are then presented in order, with and . The protocol is fixed independently of and the stream, and its decision at stage depends only on the presented prefix and its retained quantum memory. It either passes or halts and selects the current index . Selection asserts ; after passes it asserts for all .
For every such state and stream,
The stream may depend on preceding public pass responses. No promise that an expectation exceeds a threshold is required. Both kinds of claim are valid in the overlap .
This theorem bounds the sample cost of online search among quantum observables independently of the state dimension.
Formalization Note Natural logarithms and a ceiling express the source's uniform big-O copy bound. Physical Kraus instruments act on the initial tensor power of and an ancillary state; the model uses only copy access. The selected index is zero-based in Lean.
There are a universal constant and a copy-count function , depending only on the number of tests and the accuracy and failure parameters , with the following property. For every integer and every , write . Then
For every dimension , there is an online quantum protocol that begins with independent, unentangled copies of an unknown state , where is positive semidefinite and , together with a known ancillary state. Observable/threshold pairs are then presented in order, with and . The protocol is fixed independently of and the stream, and its decision at stage depends only on the presented prefix and its retained quantum memory. It either passes or halts and selects the current index . Selection asserts ; after passes it asserts for all .
For every such state and stream,
The stream may depend on preceding public pass responses. No promise that an expectation exceeds a threshold is required. Both kinds of claim are valid in the overlap .
This theorem bounds the sample cost of online search among quantum observables independently of the state dimension.
Formalization Note Natural logarithms and a ceiling express the source's uniform big-O copy bound. Physical Kraus instruments act on the initial tensor power of and an ancillary state; the model uses only copy access. The selected index is zero-based in Lean.
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 via Compressed Sensing: Error Bounds, Sample Complexity, and Efficient Estimators establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
There are positive absolute constants and a function with as such that the following holds. Let , , and satisfy . Sample independently and uniformly, with replacement, from all unsigned tensor Pauli operators, including the identity. On the real space of Hermitian matrices define and .
With probability at least over this sampling, simultaneously for every positive semidefinite matrix (without a trace or rank restriction), every , and , both conclusions below hold. Write for the spectral truncation retaining the largest eigenvalues, and . All optimizations range over Hermitian matrices and permit nonunique minimizers.
Here is the operator norm, is the Euclidean vector norm, and is the full trace norm. The two bounds separate noise from the spectral tail and apply to full-rank inputs as well as exactly low-rank ones.
Formalization Note The paper's qualitative “high probability” is represented by a vanishing failure function uniform in . Positive Lasso regularization is an explicit correction of the omitted domain; the source's regularized recovery argument requires it. This correction, the interpretation of unnormalized PSD inputs, and the qualitative probability convention require independent moderation.
There are positive absolute constants and a function with as such that the following holds. Let , , and satisfy . Sample independently and uniformly, with replacement, from all unsigned tensor Pauli operators, including the identity. On the real space of Hermitian matrices define and .
With probability at least over this sampling, simultaneously for every positive semidefinite matrix (without a trace or rank restriction), every , and , both conclusions below hold. Write for the spectral truncation retaining the largest eigenvalues, and . All optimizations range over Hermitian matrices and permit nonunique minimizers.
Here is the operator norm, is the Euclidean vector norm, and is the full trace norm. The two bounds separate noise from the spectral tail and apply to full-rank inputs as well as exactly low-rank ones.
Formalization Note The paper's qualitative “high probability” is represented by a vanishing failure function uniform in . Positive Lasso regularization is an explicit correction of the omitted domain; the source's regularized recovery argument requires it. This correction, the interpretation of unnormalized PSD inputs, and the qualitative probability convention require independent moderation.
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.
Hamiltonian Simulation by Qubitization establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be the system and auxiliary dimensions. Let be a unitary on , let be a unitary on , and write . Assume that the computed compression is Hermitian. Access to controlled and their inverses is by black-box queries; arbitrary single- and two-qubit gates are allowed. For real evolution time and accuracy , define
There are positive universal constants and such that, for every , one can choose a circuit independently of the particular that uses at most qubits. For every such oracle pair with Hermitian compression, its successful system operator , obtained by initializing and postselecting all auxiliary wires to zero, satisfies
where is the computational-basis embedding. Thus includes all possible output amplitudes, even on unused system basis labels. If is the total number of controlled oracle applications, including inverse applications, and is the number of additional two-qubit gates, the same circuit satisfies
For , the factorial scale also satisfies
This is the paper's standard-form simulation procedure and resource guarantee. Its claimed optimality is a worst-case assertion over oracle encodings, supported by the sparse specialization on p.16; the displayed lower query inequality describes the chosen procedure rather than requiring every simulator of each individual Hamiltonian to use that many calls.
Formalization Note Finite-register oracles are extended by the identity on the orthogonal complement of their computational encodings, so neither dimension must be a power of two. The error is the spectral norm of the successful operator itself. The printed in Eq. (1) is undefined in this model; the exact factorial formula fixes . The proof's internal accuracy is rescaled to order to recover final error , and its odd-term sign is reconciled with the headline's .
Let be the system and auxiliary dimensions. Let be a unitary on , let be a unitary on , and write . Assume that the computed compression is Hermitian. Access to controlled and their inverses is by black-box queries; arbitrary single- and two-qubit gates are allowed. For real evolution time and accuracy , define
There are positive universal constants and such that, for every , one can choose a circuit independently of the particular that uses at most qubits. For every such oracle pair with Hermitian compression, its successful system operator , obtained by initializing and postselecting all auxiliary wires to zero, satisfies
where is the computational-basis embedding. Thus includes all possible output amplitudes, even on unused system basis labels. If is the total number of controlled oracle applications, including inverse applications, and is the number of additional two-qubit gates, the same circuit satisfies
For , the factorial scale also satisfies
This is the paper's standard-form simulation procedure and resource guarantee. Its claimed optimality is a worst-case assertion over oracle encodings, supported by the sparse specialization on p.16; the displayed lower query inequality describes the chosen procedure rather than requiring every simulator of each individual Hamiltonian to use that many calls.
Formalization Note Finite-register oracles are extended by the identity on the orthogonal complement of their computational encodings, so neither dimension must be a power of two. The error is the spectral norm of the successful operator itself. The printed in Eq. (1) is undefined in this model; the exact factorial formula fixes . The proof's internal accuracy is rescaled to order to recover final error , and its odd-term sign is reconciled with the headline's .
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.
Direct Fidelity Estimation from Few Pauli Measurements establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be an integer, , and for a normalized -qubit pure state . Let be any density matrix on the same register, possibly mixed. For each phase-free Hermitian Pauli product , write . The source's fidelity convention is , the square of root fidelity.
Fix and . Independently draw exactly settings with replacement, each with probability . Only settings with nonzero target coefficient are drawn. For each draw, measure separately on
fresh independent copies of , obtaining Born-rule outcomes , independent conditional on the settings. Set
Then
and at most distinct observables are measured. The setting-wise and total expected copy costs satisfy
This protocol estimates the fidelity to an arbitrary known pure target using single-copy Pauli measurements. Its copy cost is random; no efficient classical sampling bound is claimed for general targets.
Formalization Note The finite experiment space fixes exactly setting draws and their setting-dependent numbers of outcomes. Its probability weights are products of the target importance law and conditional Pauli outcome laws. The closed interval is not clipped to .
Let be an integer, , and for a normalized -qubit pure state . Let be any density matrix on the same register, possibly mixed. For each phase-free Hermitian Pauli product , write . The source's fidelity convention is , the square of root fidelity.
Fix and . Independently draw exactly settings with replacement, each with probability . Only settings with nonzero target coefficient are drawn. For each draw, measure separately on
fresh independent copies of , obtaining Born-rule outcomes , independent conditional on the settings. Set
Then
and at most distinct observables are measured. The setting-wise and total expected copy costs satisfy
This protocol estimates the fidelity to an arbitrary known pure target using single-copy Pauli measurements. Its copy cost is random; no efficient classical sampling bound is claimed for general targets.
Formalization Note The finite experiment space fixes exactly setting draws and their setting-dependent numbers of outcomes. Its probability weights are products of the target importance law and conditional Pauli outcome laws. The closed interval is not clipped to .
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.