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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
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 Angel problem asks whether bounded movement can overcome an adversary that destroys one square per turn on an infinite chessboard. It is a question about strategies for arbitrarily long play, rather than about finding a path through one fixed configuration. The Devil may act anywhere on the board, including far ahead of the Angel. The movement range therefore has to be compared with a changing obstacle set and with an opponent that observes earlier moves.
This mission collects the complete classification for natural-number powers in one formal development. The power-one loss is the known Berlekamp king-capture result described in Kutz's 2004 thesis, Section 1.1. The power-two win is Mathe's Theorem 4.6 (2007). Higher powers and the exact threshold are consequences of these published results and the movement rules. This is formalization of known mathematics; it does not propose a new solution to an open problem.
A square is a point of the integer lattice . The Angel starts at the origin. Its power is a natural number , including zero. A legal jump changes each coordinate by at most in absolute value. Intermediate squares impose no restriction, and zero-length moves are allowed. Thus power one has the movement range of a chess king, while power zero cannot change position.
The ordinary Devil moves first in every round. It chooses at most one square to burn, or passes. A burned square remains burned. Repeated choices are allowed and do not destroy additional squares. Naming the Angel's currently occupied square is permitted; the loss condition is checked at the Angel's subsequent landing. The Angel loses if its destination is burned or its displacement exceeds its power.
A strategy uses only the finite history available at the time of the move. A Devil strategy receives the visited positions. An Angel strategy receives these positions and the Devil actions, including the action just taken in the current round. Every pair of strategies defines a play by recursion. Write when all rounds of this play have legal, unburned landings, and define
The mission's main theorem is the exact classification
Its two principal outcomes are
and
The first statement supplies one Devil strategy defeating every power-one Angel, rather than an opponent chosen separately after seeing a complete Angel play. Likewise, the Angel's winning strategy is chosen before the opposing Devil strategy. All these statements use the same game definition.
The source milestones retain the original Nice Devil reduction and escape theorem, add Mathe's power-two theorem explicitly, and include the king-capture result from Kutz Section 1.1. A Nice Devil protects the origin and every square within movement range of any visited position other than the most recent position. The corresponding Angel objective includes leaving every finite box. This restricted opponent is an intermediate target; the headline classification concerns the ordinary, unrestricted Devil. Monotonicity and the higher-power corollary are available in the linked theorem dependency graph without attributing invented theorem numbers to either source.
The classification identifies the exact integer threshold: one square of movement in each coordinate is insufficient, whereas two suffice. It distinguishes unlimited survival from success for a fixed number of rounds. The lower endpoint is covered as well, because the formal parameter is a natural number rather than a strictly positive integer.
The formal development makes the quantifier order, observation rules, and geometric assumptions inspectable. The classification and both principal outcomes already have machine-checked proofs. The repository audit records 228 checked local theorems and six accepted extension submissions. Its classification dependency graph contains 37 nodes, 66 edges, and zero open leaves. These are verification results, not independent peer review or a new mathematical publication. The mission now presents this completed body of work as one navigable result.
A finite simulation cannot establish survival against every opponent forever. Conversely, failure of several candidate Angel strategies does not establish a uniform winning Devil strategy. Finite and infinite play must be related without reversing the strategic quantifiers. The geometric statements also have to constrain the evolving play, rather than describe only a static drawing. For the king-capture result, local boundary restrictions must remain valid after every legal move; for the power-two result, the source's confinement and escape assertions must refer to the same operational game.
The implementation uses integer pairs, finite histories, optional Devil actions, finite sets, and recursion on natural numbers. Lean 4.33.1 and the pinned Mathlib revision match the platform environment. The closed local entry point is Solutions.PowerClassification; Solutions.Completed retains the original Mathe assembly. The definitions do not assume a winning strategy or restrict the headline game to a finite board.
The king-capture implementation uses deliberately loose radius-100 constants for an internal confinement argument. It does not claim an optimal capture time or a formalization of the smallest board illustrated by the source. Fractional speeds and Devils burning multiple squares per turn are outside this mission. Reusable material includes finite-game determinacy, finite-survival compactness, journey reduction, connected-square boundary estimates, and strategy monotonicity. Independent reproduction and documentation improvements are welcome; there is no remaining open proof obligation for the stated classification. Platform reference mirrors containing sorry are kept separate from the closed local proof library, whose audited dependencies contain only the standard Lean axioms.
A graph homomorphism sends vertices of one graph to another while preserving adjacency. Requiring this map to be continuous makes graph coloring sensitive to topology: each color must occupy an open and closed region. For integer lattice actions, the resulting questions connect finite graph structure with continuous dynamics. The results considered here give an algebraic sufficient condition on a finite target graph that works in every finite lattice dimension. They are Theorem 1.4 and Proposition 7.1 of Ruijun Wang's Continuous graph homomorphisms of higher dimensional abelian group actions, a 2026 research preprint.
Fix an integer . The integer lattice is , with standard generators . Each generator has one coordinate equal to one and all other coordinates zero. An action of on a space assigns maps satisfying and . A continuous action uses the discrete topology on . It is free when implies .
A Polish space has a topology induced by a complete separable metric. It is zero-dimensional when its topology has a basis of clopen sets, meaning sets that are both open and closed. The standard Schreier graph on joins to for each generator, with adjacency understood symmetrically.
Let be a finite simple graph on a vertex set , equipped with the discrete topology. A continuous homomorphism is a continuous function such that
Write when such a map exists for every free continuous lattice action on every zero-dimensional Polish space.
A closed walk starts and ends at the same vertex, and its length counts edges. Repetitions are allowed. The reduced homotopy group identifies based closed walks under cancellation of a spur and cancellation of a closed four-walk, with these relations compatible with concatenation. Its identity is the constant walk. These conventions agree with Section 2.
Theorem 1.4 assumes an odd closed walk whose reduced class has trivial square:
The source statement appears in Section 1.
The main target, Proposition 7.1, permits any finite order:
Here is a positive integer; it need not be the least exponent. The square-trivial case follows by taking . The stronger statement is given in Section 7.1.
These results turn one finite algebraic witness into a conclusion covering all the spaces, actions, and positive dimensions specified above. Once a graph satisfies the hypothesis, an individual action requires no additional dynamical condition beyond the stated assumptions. The conclusion concerns finite discrete targets and the standard generating set.
Both results are established in the cited paper. Complete local Lean proofs now cover their full universal statements. The local project build and kernel audit have passed, and the final declarations use only Lean's standard logical axioms. Prove2Me has accepted the complete uploaded proof dependency graph. Both original headline theorem identities now have status Proved.
The completed development supplies reusable statements and checked infrastructure for lattice actions, reduced graph walks, finite probability distributions, and continuous graph homomorphisms. These components support inspection and reuse beyond the two headline results.
Choosing a homomorphism separately on each orbit does not ensure continuity across nearby points of the space. Freeness identifies each orbit with a lattice once an origin has been chosen, but does not supply continuously chosen origins across all orbits. A proof must therefore establish continuity of the resulting vertex map itself. Restricting attention to one action, one dimension, or an orbitwise map would leave the stated universal conclusion unresolved.
The lattice is represented by , actions use additive notation, and standard adjacency includes both orientations of each generator edge. Reduced homotopy is an inductively generated relation on genuine Mathlib graph walks; powers are repeated concatenations. The target vertex type is arbitrary and finite, with its discrete topology.
Source spaces and target vertex types have independent universe parameters. Empty source spaces are allowed. No connectivity assumption is imposed on the target, and no separate nonemptiness hypothesis is added. The odd-walk witness already forces target nonemptiness. Neither a carrier-construction assumption nor an approximation condition appears in either final theorem.
Finite order refers to the class of the walk, rather than its length. An odd walk can revisit vertices and traverse edges repeatedly, so the hypothesis does not require an embedded cycle. All four-walk relations are included, including those with repeated vertices. The conclusion asserts existence of a continuous adjacency-preserving function; it asserts neither uniqueness nor injectivity. These distinctions matter when comparing a formal declaration with the source: replacing arbitrary closed walks by simple cycles or adding connectedness would change the objects quantified over. The recorded statements retain the wider walk convention used in the paper.
Further contributions can reuse the infrastructure or establish related variants while preserving these conventions. Any changed statement should distinguish its additional hypotheses and its altered conclusion from the two results recorded here.
Ruijun Wang, Continuous graph homomorphisms of higher dimensional abelian group actions, arXiv preprint arXiv:2609.39824v1, 2026. Version and source; Theorem 1.4; definitions; Proposition 7.1.
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.
Fixed-point quantum search with an optimal number of queries establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be integers, , and . Let be a unitary on qubits, , and let be a unit vector with . The supplied target oracle is
where flips the additional qubit: flips it on and acts identically on the orthogonal complement.
Define for , and for . For , set
With , , and , define ; the empty product is .
There is an absolute constant such that, for each , a single circuit template chosen before implements up to a global phase on every data vector, returning its one ancillary qubit to . It uses exactly plain queries and total calls to or , no controlled oracle calls, and at most elementary gates from arbitrary single-qubit unitaries and CNOT. Preparation of the supplied input is outside these counts. Oracle calls are charged separately from elementary gates.
Writing for the Chebyshev polynomial of the first kind, both the constructed sequence and this physical circuit have target success probability
In particular,
The guaranteed interval gives fixed-point amplitude amplification with an adjustable failure tolerance and exactly target-oracle queries. The endpoints , , , and are included.
Formalization Note The joint overlap with is the physical success probability because the ancillary qubit is returned clean. The endpoint uses the continuous limiting polynomial confirmed on PDF p.4, rather than division by zero.
Let be integers, , and . Let be a unitary on qubits, , and let be a unit vector with . The supplied target oracle is
where flips the additional qubit: flips it on and acts identically on the orthogonal complement.
Define for , and for . For , set
With , , and , define ; the empty product is .
There is an absolute constant such that, for each , a single circuit template chosen before implements up to a global phase on every data vector, returning its one ancillary qubit to . It uses exactly plain queries and total calls to or , no controlled oracle calls, and at most elementary gates from arbitrary single-qubit unitaries and CNOT. Preparation of the supplied input is outside these counts. Oracle calls are charged separately from elementary gates.
Writing for the Chebyshev polynomial of the first kind, both the constructed sequence and this physical circuit have target success probability
In particular,
The guaranteed interval gives fixed-point amplitude amplification with an adjustable failure tolerance and exactly target-oracle queries. The endpoints , , , and are included.
Formalization Note The joint overlap with is the physical success probability because the ancillary qubit is returned clean. The endpoint uses the continuous limiting polynomial confirmed on PDF p.4, rather than division by zero.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Generalized Quantum Signal Processing establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let and let be prescribed ordinary complex polynomials. For real angles define
For any positive integer and any unitary matrix , put , with the control qubit as the first tensor factor, and
When , this is just the initial rotation tensored with . There exist real vectors and a real , chosen independently of and , such that
if and only if
Here and denote polynomial evaluation at the matrix , and the stars leave the second-column blocks unspecified. The zero polynomial satisfies the degree bound.
This theorem characterizes exactly the polynomial pairs synthesized by forward signal applications and rotations; it imposes no real-coefficient or parity restriction.
Formalization Note Universal finite-dimensional unitary realization expresses the polynomial identity used by the proof; in particular, it includes every scalar unitary . The rotation is the matrix printed in equation (6), without a determinant-one constraint.
Let and let be prescribed ordinary complex polynomials. For real angles define
For any positive integer and any unitary matrix , put , with the control qubit as the first tensor factor, and
When , this is just the initial rotation tensored with . There exist real vectors and a real , chosen independently of and , such that
if and only if
Here and denote polynomial evaluation at the matrix , and the stars leave the second-column blocks unspecified. The zero polynomial satisfies the degree bound.
This theorem characterizes exactly the polynomial pairs synthesized by forward signal applications and rotations; it imposes no real-coefficient or parity restriction.
Formalization Note Universal finite-dimensional unitary realization expresses the polynomial identity used by the proof; in particular, it includes every scalar unitary . The rotation is the matrix printed in equation (6), without a determinant-one constraint.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Few Single-Qubit Measurements Suffice to Certify Any Quantum State (Gupta, He, O'Donnell) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the one-copy certification theorem of Gupta, He and O'Donnell.
Access model. For qubits, the algorithm accesses a pure hypothesis state , , only through queries of Definition 15: for single-qubit projectors on (each , the identity allowed), the query returns . It also flips fair coins, and it touches its single copy of the unknown -qubit mixed state (positive semidefinite, trace one) only by projective measurements of one qubit at a time in an orthonormal basis ; the qubit, the basis, the queries and the coins may all depend adaptively on everything seen so far.
Theorem. There exist such an algorithm for every and a constant , chosen before and , such that for every , every run of makes at most query, coin and measurement steps, and for every and , writing ,
Repeating this test times and applying a Chernoff bound gives the paper's Main Theorem: certification of every pure state with single-qubit measurements on copies.
Formalization Note The output probability is computed on subnormalized post-measurement states (Lüders rule without renormalization). The running time is modelled by the number of query, coin and measurement steps on every execution path; classical post-processing between steps is not charged, which matches the source's per-step cost only up to this modelling choice.
This is the one-copy certification theorem of Gupta, He and O'Donnell.
Access model. For qubits, the algorithm accesses a pure hypothesis state , , only through queries of Definition 15: for single-qubit projectors on (each , the identity allowed), the query returns . It also flips fair coins, and it touches its single copy of the unknown -qubit mixed state (positive semidefinite, trace one) only by projective measurements of one qubit at a time in an orthonormal basis ; the qubit, the basis, the queries and the coins may all depend adaptively on everything seen so far.
Theorem. There exist such an algorithm for every and a constant , chosen before and , such that for every , every run of makes at most query, coin and measurement steps, and for every and , writing ,
Repeating this test times and applying a Chernoff bound gives the paper's Main Theorem: certification of every pure state with single-qubit measurements on copies.
Formalization Note The output probability is computed on subnormalized post-measurement states (Lüders rule without renormalization). The running time is modelled by the number of query, coin and measurement steps on every execution path; classical post-processing between steps is not charged, which matches the source's per-step cost only up to this modelling choice.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Quantum Approximate Counting, Simplified (Aaronson, Rall) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the main theorem of Aaronson and Rall: approximate counting with the optimal query complexity, using Grover iterations only (no quantum Fourier transform).
Let be a nonempty set of marked items and . The algorithm (AR p.4) pads the list with unmarked items, giving items. Let be the membership (phase) oracle, the uniform superposition over the items, and . The only quantum operation is: prepare for an odd and measure it in the computational basis, at a cost of queries.
The theorem has three parts.
The function and the constants are fixed before , , and . The result matches the BHMT query complexity for approximate counting, and it is the basis of QFT-free amplitude estimation.
Formalization Note The theorem is stated for the paper's concrete algorithm (the frozen definitions acEventProb, acStep1Exit, acStep2), with every shot count "at least " taken as exactly and Mathlib's round used for the rotation lemma's roundings (the paper allows any tie-breaking). The sentence "fewer than queries whenever the estimate is accurate" is formalized as the joint event of accuracy and fewer than queries, which is what the proof establishes. That event implies the accuracy claim. The -bound is uniform in and as .
This is the main theorem of Aaronson and Rall: approximate counting with the optimal query complexity, using Grover iterations only (no quantum Fourier transform).
Let be a nonempty set of marked items and . The algorithm (AR p.4) pads the list with unmarked items, giving items. Let be the membership (phase) oracle, the uniform superposition over the items, and . The only quantum operation is: prepare for an odd and measure it in the computational basis, at a cost of queries.
The theorem has three parts.
The function and the constants are fixed before , , and . The result matches the BHMT query complexity for approximate counting, and it is the basis of QFT-free amplitude estimation.
Formalization Note The theorem is stated for the paper's concrete algorithm (the frozen definitions acEventProb, acStep1Exit, acStep2), with every shot count "at least " taken as exactly and Mathlib's round used for the rotation lemma's roundings (the paper allows any tie-breaking). The sentence "fewer than queries whenever the estimate is accurate" is formalized as the joint event of accuracy and fewer than queries, which is what the proof establishes. That event implies the accuracy claim. The -bound is uniform in and as .
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.