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?
Off-policy evaluation (OPE) asks for the long-run value of a target decision policy, using only data collected under a different policy. It arises wherever running the target policy is expensive or unsafe: a new treatment rule in medicine, a new recommendation or pricing rule, a candidate controller in reinforcement learning. Importance-sampling estimators reweight whole trajectories. Their variance grows exponentially with the horizon, the curse of horizon (Liu et al. 2018, arXiv:1810.12429).
Kallus and Uehara (arXiv:1909.05850, Operations Research 2022) treat infinite-horizon discounted OPE as a semiparametric estimation problem. They derive the efficiency bound under three models: non-Markov, time-varying Markov and time-invariant Markov (MDP). They then propose double reinforcement learning (DRL), an estimator that combines a q-function estimate with an estimate of the ratio between the discounted state visitation of the target policy and the state distribution of the data. In the MDP model it attains the efficiency bound. This mission formalizes the transition-sampling version of that result, Theorem 6.
Timeline:
States lie in a measurable space and actions in a measurable space . A time-invariant MDP is a transition kernel and a reward kernel with rewards in . A policy is a kernel from to . Fix a discount , a known target policy with known initial law , and a behavior policy .
The estimand is the normalized discounted value
The q-function is , and . The discounted visitation is , where is the law of .
Transition sampling. The data are i.i.d. observations with law : , , and, given , independently and . The law of may differ from that of .
The density ratios are and . For candidate nuisances , with , the estimating function is
The cross-fitted estimator splits the sample into two folds. It fits on fold and averages over all observations, each evaluated at the nuisances of the other fold. The efficient influence function is , and the efficiency bound is .
Assume the following:
Then
No rate exponent or learner class is fixed. Only the product rate enters.
Theorem 6 shows that, in a Markov model, a -consistent and efficient OPE estimator exists whose variance scales with the number of observed transitions, not trajectories. It requires no complexity (Donsker or entropy) restriction on the nuisance estimators, only a product rate. Any black-box learners with , which allows two subparametric rates, give asymptotically valid confidence intervals at the efficiency bound. The mixed-bias identities (Eqs. (5)–(8)) and Lemma 1 are the same ingredients used by later minimax and adversarial estimators of and .
The result is proved in the paper; nothing here is presented as open. As far as is known, none of it has a machine-checked proof: no off-policy evaluation, density-ratio characterization or cross-fitting asymptotics exists in Mathlib or on the platform. Formalizing it checks the appendix argument, which is short and contains errors (below). It also produces a reusable layer: kernel-based discounted MDPs on general measurable spaces, discounted visitation measures, and the cross-fitting plus Slutsky template that other double-machine-learning results share.
The obvious route is "the estimator equals the oracle average plus negligible terms, then apply the CLT". Two of its steps are not routine.
First, the negligible terms are random functions evaluated at random data. The empirical-process term (28) is controlled only conditionally on the other fold, through a conditional Chebyshev argument that needs the independence structure of the split. Treating as fixed functions loses exactly this.
Second, the bias term (30) is second order only because of the mixed-bias structure. That structure rests on Lemma 1, a change-of-measure identity between the discounted visitation of and the data distribution. The printed constants are wrong. The Jensen step fails when is large: with one state, uniform on two actions and a point mass, the left side is and the right side is . The bound by is not a valid inequality for a triple product. Both need a bound , which the mission adds.
Kernel.rnDeriv). The MDP, the policies and the observation law are Mathlib kernels and measures. The paper's base measures are not used.toReal of Radon–Nikodym derivatives, not free functions satisfying an identity. Overlap (, ) is a standing assumption.TendstoInDistribution with TendstoInMeasure) and Mathlib's i.i.d. CLT tendstoInDistribution_inv_sqrt_mul_sum_sub. The occupancy and Lemma 1 layer and the cross-fitting template are reusable beyond this mission. Proofs of any milestone, and helper lemmas on kernel powers and discounted sums, are welcome.Mean-variance analysis (Markowitz, 1952) tells an investor which portfolio to hold once the mean vector and covariance matrix of asset returns are known. In practice both are estimated from a finite window of past returns, and the portfolio built from the estimates (the plug-in portfolio) performs badly out of sample: its weights are noisy and its realized utility is often far below the theoretical optimum. A long literature asks how to choose portfolio rules that take this estimation risk into account; Kan and Zhou (2007) treat the case with a risk-free asset.
Kan, Wang and Zhou (2022) study the case without a risk-free asset, where the investor must be fully invested in risky assets. There the optimal portfolio splits into the global minimum-variance (GMV) portfolio plus a scaled zero-investment portfolio, and estimation errors enter the two parts very differently. Their §2 derives the exact expected out-of-sample utility of the family of rules that rescale the estimated zero-investment part, and the coefficient that maximizes it. This mission formalizes that derivation.
An investor chooses weights with to maximize the mean-variance utility
where is the risk-aversion coefficient and is positive definite. The population quantities that matter are the GMV variance , the GMV mean , and the squared slope of the asymptote of the minimum-variance frontier, .
The returns of an estimation window of length are independent and identically distributed . The maximum-likelihood estimators are and . From them come the sample GMV portfolio and the sample zero-investment portfolio
with . For a constant combining coefficient the paper considers
is the plug-in rule. The expected out-of-sample utility evaluates at the true , and averages over the sample. The five random quantities , , , and determine it.
For and , with
the coefficient is the unique maximizer of over , and , with when .
For and every constant ,
together with the first and second moments of the auxiliary variables , of Proposition 1 that the proof of Lemma 1 uses.
The result gives a closed-form, implementable-in-principle correction to the plug-in rule: since , the investor should always under-weight the estimated zero-investment portfolio, by a factor that depends only on , and . Replacing by an adjusted estimator gives the paper's feasible rules (§2.4, §3), which are compared empirically in §4. The moment formulas (A9)–(A13) are of independent use: they give the exact out-of-sample mean and variance of the sample GMV and zero-investment portfolios, which recur in the shrinkage literature (for instance Lassance, Martín-Utrera and Simaan, 2024, who build on this paper's Proposition 1).
The result is proved in the paper, but the proof rests on Proposition 1, a stochastic representation of the out-of-sample moments whose detailed proof is in an online appendix. No machine-checked proof exists. On Prove2Me, Proposition 1 is posed (Open) as RiskEU.OOSUVar.kan_representation in Lassance et al.'s restatement, together with special cases (eq_IA60, eq_IA49) of the combinations and of the portfolio variance for and . The closed-form vertex of the quadratic (17) is already proved there (RiskEU.RobustShrink.proposition_IA_1_3). What this mission adds is the statement about the actual expectation over the Gaussian sample, for all real , under the paper's own threshold , with uniqueness of the maximizer.
Once Lemma 1 is available, the goal is the vertex of a concave quadratic. The difficulty is Lemma 1 itself: computing expectations of quadratic forms in and in the normalized vector . The weights are ratios of dependent random quantities, so linearity of expectation does not apply directly, and inverse-Wishart moment formulas alone do not cover the ratio in . The threshold is Lemma 1's hypothesis; the factor in the denominator of (A12) shows that it is what keeps the expected variance of the estimated zero-investment portfolio finite, so integrability is part of the content.
The model is the published definition RiskEU.OOSUVar.Setting: Market N carries , , ; sigmaG2, muG, psi2, U, sampleMean, sampleCov (divided by ), wHatG, wHatZ and IsGaussianSample are the objects above (that setting calls the window ; here it is ). The auxiliary family of Proposition 1 and , come from the published RiskEU.OOSUVar.KanRepresentation. The mission's own definitions (KanCombine.Optimal.Model) add the standing assumptions, the combining portfolio, the five sample moments, the expected utility, and .
Conventions committed to:
The goal is about the integral over the Gaussian sample. Stating it about the closed-form right-hand side of (17) would reduce it to the vertex of a quadratic, which is already proved, and is ruled out. The hypotheses are satisfiable: , , , , meets them with the product Gaussian sample, and gives .
A complete development needs Wishart and inverse-Wishart theory (the Bartlett decomposition, moments of chi-squared ratios) and a formal version of Proposition 1. These are reusable well beyond this mission; contributions proving (A9)–(A13) by any route, including directly from inverse-Wishart moments, are welcome.
A provable quantum advantage for approximate optimization via decoded quantum interferometry establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix a rational rate . An admissible block count satisfies for an integer , and , where , and . Work over the publicly represented characteristic-two field , with a fixed public primitive element . Put and . A promised instance consists of arbitrary sets with , accessed only through separately callable fixed-block XOR membership oracles. Each call chooses its block classically and may query a superposition of whole symbols.
A coefficient vector represents the polynomial , including the zero polynomial. Its score is
Define
The construction uses the conventional unfolded scalar GRS dual syndrome decoder at cutoff , strictly below half its scalar minimum distance, the explicit top-window layer weights, and synthesis accuracy . Its polynomial resource bounds and classical circuit constructor are independent of the acceptance sets.
The probability is over the same sampled acceptance sets and independent algorithm randomness. Computation between queries and arbitrary finite advice are unrestricted, provided the description and advice are fixed before sampling.
This result separates the approximation scores attainable through the same whole-symbol membership interface. The quantum assertion is an expectation guarantee for every promised oracle; the classical assertions are distributional.
Formalization Note A fixed effective polynomial-basis binary field representation and uniform compilation over make the implicit public representation and polynomial runtime concrete. The DQI state, its coefficient output wires and its query count are tied to one circuit. The sampled probabilities are finite uniform averages of normalized classical output laws.
Fix a rational rate . An admissible block count satisfies for an integer , and , where , and . Work over the publicly represented characteristic-two field , with a fixed public primitive element . Put and . A promised instance consists of arbitrary sets with , accessed only through separately callable fixed-block XOR membership oracles. Each call chooses its block classically and may query a superposition of whole symbols.
A coefficient vector represents the polynomial , including the zero polynomial. Its score is
Define
The construction uses the conventional unfolded scalar GRS dual syndrome decoder at cutoff , strictly below half its scalar minimum distance, the explicit top-window layer weights, and synthesis accuracy . Its polynomial resource bounds and classical circuit constructor are independent of the acceptance sets.
The probability is over the same sampled acceptance sets and independent algorithm randomness. Computation between queries and arbitrary finite advice are unrestricted, provided the description and advice are fixed before sampling.
This result separates the approximation scores attainable through the same whole-symbol membership interface. The quantum assertion is an expectation guarantee for every promised oracle; the classical assertions are distributional.
Formalization Note A fixed effective polynomial-basis binary field representation and uniform compilation over make the implicit public representation and polynomial runtime concrete. The DQI state, its coefficient output wires and its query count are tied to one circuit. The sampled probabilities are finite uniform averages of normalized classical output laws.
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.
An Optimal Quantum Linear Systems Algorithm establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Consider the quantum linear systems problem for an invertible, complex, -sparse matrix , with , , and , where these are operator norms and is known. For a nonzero vector , a supplied preparation circuit prepares . The solver must output a success flag of probability at least and, conditioned on success, a normalized reduced density matrix within trace distance of , where . Both and have reversible row-location and XOR entry-value oracles; the locations listed in each row are distinct, cover all nonzeros, and may include zeros. Only matrix-oracle calls count, including inverse and controlled calls. Supplied preparation operations and known quantum operations are free.
Let be the supremum over positive dimensions and public finite exact entry encodings of the least natural worst-case matrix-query budget of a solver correct for every compatible promised input and oracle completion. Solvers are chosen before the hidden matrix, vector, and oracle completions. Empty sets of feasible budgets and unbounded suprema retain . There exist absolute constants , , , and such that, for every , , and ,
This gives matching upper and worst-case lower bounds jointly in sparsity, inverse-norm bound, and precision. The constants and thresholds are independent of dimension, encoding, and input.
Formalization Note Complexity is represented in using the frozen OptimalQLSP.queryComplexity. General matrices and general positive dimensions are retained; the Hermitian reduction and power-of-two registers used inside the proof do not restrict the headline.
Consider the quantum linear systems problem for an invertible, complex, -sparse matrix , with , , and , where these are operator norms and is known. For a nonzero vector , a supplied preparation circuit prepares . The solver must output a success flag of probability at least and, conditioned on success, a normalized reduced density matrix within trace distance of , where . Both and have reversible row-location and XOR entry-value oracles; the locations listed in each row are distinct, cover all nonzeros, and may include zeros. Only matrix-oracle calls count, including inverse and controlled calls. Supplied preparation operations and known quantum operations are free.
Let be the supremum over positive dimensions and public finite exact entry encodings of the least natural worst-case matrix-query budget of a solver correct for every compatible promised input and oracle completion. Solvers are chosen before the hidden matrix, vector, and oracle completions. Empty sets of feasible budgets and unbounded suprema retain . There exist absolute constants , , , and such that, for every , , and ,
This gives matching upper and worst-case lower bounds jointly in sparsity, inverse-norm bound, and precision. The constants and thresholds are independent of dimension, encoding, and input.
Formalization Note Complexity is represented in using the frozen OptimalQLSP.queryComplexity. General matrices and general positive dimensions are retained; the Hermitian reduction and power-of-two registers used inside the proof do not restrict the headline.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Sample-optimal learning of stabilizer states 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 the allowed failure probability. An unknown normalized pure stabilizer state is provided as identical copies. Let be the least number of copies with which one quantum procedure can identify every such state with probability at least . The minimum permits arbitrary collective measurements, ancillas, internal randomness and adaptivity. Identification means outputting a valid tableau of independent signed Pauli generators whose common eigenspace is the input state; global phase and the choice of generators are irrelevant. Then
Furthermore, for every such and , there is a quantum learner receiving at most copies and retaining them through adaptive operations, which identifies every input stabilizer state with failure probability at most . There are absolute constants and , independent of , and the input state, such that this learner has computational time
Time counts elementary quantum gates, measurements, fair coins and Boolean operations, including classical and reversible arithmetic, finite-precision rotation synthesis and tableau reconstruction. The sample and success bounds have no asymptotic threshold. This determines the leading sample coefficient to be one and attains the bound with an efficient learner.
Formalization Note The minimum is represented in , with an empty feasible set assigned ; the upper bound implies finiteness. The lower inequality is written as to avoid natural subtraction. The theorem's printed statement leaves the qubit domain implicit; follows the lower-bound proof on PDF p.7, since the zero-qubit state requires zero copies.
Let be the number of qubits and let be the allowed failure probability. An unknown normalized pure stabilizer state is provided as identical copies. Let be the least number of copies with which one quantum procedure can identify every such state with probability at least . The minimum permits arbitrary collective measurements, ancillas, internal randomness and adaptivity. Identification means outputting a valid tableau of independent signed Pauli generators whose common eigenspace is the input state; global phase and the choice of generators are irrelevant. Then
Furthermore, for every such and , there is a quantum learner receiving at most copies and retaining them through adaptive operations, which identifies every input stabilizer state with failure probability at most . There are absolute constants and , independent of , and the input state, such that this learner has computational time
Time counts elementary quantum gates, measurements, fair coins and Boolean operations, including classical and reversible arithmetic, finite-precision rotation synthesis and tableau reconstruction. The sample and success bounds have no asymptotic threshold. This determines the leading sample coefficient to be one and attains the bound with an efficient learner.
Formalization Note The minimum is represented in , with an empty feasible set assigned ; the upper bound implies finiteness. The lower inequality is written as to avoid natural subtraction. The theorem's printed statement leaves the qubit domain implicit; follows the lower-bound proof on PDF p.7, since the zero-qubit state requires zero copies.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Efficient Exact Quantum Sampling from the Sun-Wootters Distribution for Optimal Polynomial Intersection establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be prime, , and let be distinct public evaluation points. Every hidden set has the same known cardinality , with . Put , for , and . A coefficient vector represents the polynomial ; its satisfaction ratio is . Access is through the indexed XOR oracle , with arbitrary full unitary behavior on invalid encodings.
For an integer cutoff , set , , and . Define , , and . On its positive-denominator domain the Sun–Wootters law is
Write , , , and . Suppose and the target denominator is positive. For every complete duplicate-free canonical shell list, padded to the same slots for every syndrome, the ideal attempt prepares , reversibly indexes and erases the error, applies to the index, and postselects using a match flag. It then applies the positive-character Fourier transform on the syndrome. Its success and conditional law satisfy
This finite identity preserves cancellation within fibers and asserts no running-time bound for an arbitrary unpriced list. For normalized ideal and implemented full-register states, ideal success at least , vector error at most , and final Fourier operator error at most , implemented success is at least and conditional total variation error is at most .
Now consider public parameter families with , , and . Constants, programs and preprocessing are uniform over all sets of the promised cardinality and every supplied membership oracle. Let , using natural logarithms and , and define
All denominators in these ratios must be nonzero and all entropy arguments must belong to . Fix , a positive rational , and in that domain with and . Put . Eventually the target is well defined, complete canonical lists admit one polynomial common padding length, and ideal success is at least . For every , a uniform quantum algorithm with time polynomial in satisfies
For every fixed default vector, the defaulted law has total variation distance at most from and expected score at least , for some nonnegative independent of the hidden sets; here on . Preprocessing, synthesized gates, queries, measurements, reversible/classical work, and capped restarts are counted.
The two balanced consequences are retained:
These conclusions turn the Sun–Wootters distributional improvement into efficient worst-case quantum optimization.
Formalization Note Theorem 7.1's printed “For each family member” is clarified to an eventual guarantee, matching its proof's positivity and decoder-feasibility bounds. This is an explicit proof-based scope clarification awaiting independent moderation. The finite exact identity is separate from the approximate universal-gate implementation. The paper's operator called inverse QFT has positive character and equals the frozen positive-sign QFT convention.
Correction to the printed source.
Printed: For each family member put ... and define Pu,m by equations (11) to (13) with largest active weight ell_m. Then ... there is a uniform bounded-error quantum algorithm.
Corrected: The finite target is defined on its positive-denominator and cutoff-at-least-three domain, and the sampling guarantees hold for every sufficiently large public parameter-family member.
Reason: Theorem 7.1 itself invokes the finite Johnson inequality and postselection estimate only for all sufficiently large m. Lemmas 3.2 and 6.4 are eventual, while equation (11) uses log log ell; early undefined targets cannot be normalized by total division.
Let be prime, , and let be distinct public evaluation points. Every hidden set has the same known cardinality , with . Put , for , and . A coefficient vector represents the polynomial ; its satisfaction ratio is . Access is through the indexed XOR oracle , with arbitrary full unitary behavior on invalid encodings.
For an integer cutoff , set , , and . Define , , and . On its positive-denominator domain the Sun–Wootters law is
Write , , , and . Suppose and the target denominator is positive. For every complete duplicate-free canonical shell list, padded to the same slots for every syndrome, the ideal attempt prepares , reversibly indexes and erases the error, applies to the index, and postselects using a match flag. It then applies the positive-character Fourier transform on the syndrome. Its success and conditional law satisfy
This finite identity preserves cancellation within fibers and asserts no running-time bound for an arbitrary unpriced list. For normalized ideal and implemented full-register states, ideal success at least , vector error at most , and final Fourier operator error at most , implemented success is at least and conditional total variation error is at most .
Now consider public parameter families with , , and . Constants, programs and preprocessing are uniform over all sets of the promised cardinality and every supplied membership oracle. Let , using natural logarithms and , and define
All denominators in these ratios must be nonzero and all entropy arguments must belong to . Fix , a positive rational , and in that domain with and . Put . Eventually the target is well defined, complete canonical lists admit one polynomial common padding length, and ideal success is at least . For every , a uniform quantum algorithm with time polynomial in satisfies
For every fixed default vector, the defaulted law has total variation distance at most from and expected score at least , for some nonnegative independent of the hidden sets; here on . Preprocessing, synthesized gates, queries, measurements, reversible/classical work, and capped restarts are counted.
The two balanced consequences are retained:
These conclusions turn the Sun–Wootters distributional improvement into efficient worst-case quantum optimization.
Formalization Note Theorem 7.1's printed “For each family member” is clarified to an eventual guarantee, matching its proof's positivity and decoder-feasibility bounds. This is an explicit proof-based scope clarification awaiting independent moderation. The finite exact identity is separate from the approximate universal-gate implementation. The paper's operator called inverse QFT has positive character and equals the frozen positive-sign QFT convention.
Correction to the printed source.
Printed: For each family member put ... and define Pu,m by equations (11) to (13) with largest active weight ell_m. Then ... there is a uniform bounded-error quantum algorithm.
Corrected: The finite target is defined on its positive-denominator and cutoff-at-least-three domain, and the sampling guarantees hold for every sufficiently large public parameter-family member.
Reason: Theorem 7.1 itself invokes the finite Johnson inequality and postselection estimate only for all sufficiently large m. Lemmas 3.2 and 6.4 are eventual, while equation (11) uses log log ell; early undefined targets cannot be normalized by total division.
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.
Worst-Case Quantum Algorithm for Optimal Polynomial Intersection Beyond Decoded Quantum Interferometry establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Consider a growing public parameter family , where is prime, , , , and . Put . Assume eventually for fixed and . Each has its standard effective polynomial-basis binary representation, specified by its characteristic, extension degree and irreducible modulus. Fix a target and assume one of these two eventual regimes, with a common fixed margin :
Here , with .
Let tend to zero. There exist a uniform quantum oracle solver, a polynomial and an index such that, for every , every tuple of distinct evaluation points , and every hidden subset family satisfying
the solver outputs a polynomial for which
Its classical constructor receives only the public field description, , the evaluation points and the integer target . The sets are accessed through their individual quantum XOR membership oracles. Work counts queries, standard Clifford+T gates, measurements, preparations, classical control, workspace and coefficient decoding; constructor time and space are polynomial in . The constants and threshold are uniform over evaluation points and hidden sets, and probability refers to internal coins and measurements.
This gives an algorithm on every promised instance, including exact perfect satisfaction in the first branch. No random-instance assumption, efficient-decoder hypothesis, or pre-existing-solution hypothesis is imposed.
Formalization Note The asymptotic reading makes the bound and high-rate constant margin explicit using Theorem 6.1 and Remark 6.2. The printed informal high-rate sentence omits them. Unequal densities are retained under footnote 3. Rates tending to one and are retained through constructive dimension reduction. These bridges require independent mathematical moderation.
Consider a growing public parameter family , where is prime, , , , and . Put . Assume eventually for fixed and . Each has its standard effective polynomial-basis binary representation, specified by its characteristic, extension degree and irreducible modulus. Fix a target and assume one of these two eventual regimes, with a common fixed margin :
Here , with .
Let tend to zero. There exist a uniform quantum oracle solver, a polynomial and an index such that, for every , every tuple of distinct evaluation points , and every hidden subset family satisfying
the solver outputs a polynomial for which
Its classical constructor receives only the public field description, , the evaluation points and the integer target . The sets are accessed through their individual quantum XOR membership oracles. Work counts queries, standard Clifford+T gates, measurements, preparations, classical control, workspace and coefficient decoding; constructor time and space are polynomial in . The constants and threshold are uniform over evaluation points and hidden sets, and probability refers to internal coins and measurements.
This gives an algorithm on every promised instance, including exact perfect satisfaction in the first branch. No random-instance assumption, efficient-decoder hypothesis, or pre-existing-solution hypothesis is imposed.
Formalization Note The asymptotic reading makes the bound and high-rate constant margin explicit using Theorem 6.1 and Remark 6.2. The printed informal high-rate sentence omits them. Unequal densities are retained under footnote 3. Rates tending to one and are retained through constructive dimension reduction. These bridges require independent mathematical 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 Decoded Quantum Interferometry for General Pauli Hamiltonians establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let and be integers. Let be a classically known Hamiltonian on qubits, where and the are distinct canonical Hermitian Pauli operators that commute pairwise. Let be a real polynomial of degree exactly , and assume . Write for the matrix whose columns are the symplectic labels of the , with the coordinates preceding the coordinates. Assume there exists a unitary decoder on the -qubit label register and the -qubit syndrome register satisfying
Here is Hamming weight and is the zero-string reference coefficient defined below. The zero-branch guarantee is required only when ; when , that decoder input is unrestricted. All other decoder inputs are unrestricted.
There is an exact quantum preparation circuit, chosen from the known Hamiltonian and polynomial before choosing the decoder, that works for every decoder with these guarantees and prepares
It starts with zeroed registers, uses exactly one plain forward application of , and uses no adjoint or controlled decoder calls. The output is the reduced density matrix after discarding the other registers, with no postselection or success-probability qualification.
For clarity, define the real reference coefficients and their normalization by
The reference is constructed by the algorithm, rather than supplied as input. In particular,
where ; both and have unit norm.
The circuit includes a concrete classical arithmetic program that computes and all boundary and local-matrix entries of the reference MPS from the coefficients alone. It may introduce only the numeric constants , and the entries of its quantum gates are obtained from that program's results. There exist an absolute , a polynomial with nonnegative integer coefficients, and thresholds and , all independent of sizes, Pauli terms, coefficients, and decoder, such that
Here classical cost counts actual arithmetic and memory instructions, and quantum cost counts the circuit's gate and oracle steps plus initialization of its qubits. This is the paper's ideal model with unit-cost real arithmetic and exact arbitrary one- and two-qubit unitary gates.
This result supplies an exact polynomial-filtered density matrix using a perfect decoder even for general real commuting Pauli coefficients, without assuming the reference state has already been prepared.
Formalization Note. The proof's convention replaces the theorem display's . Real polynomial coefficients, the nonzero condition, and the decoder's zero-branch guarantee for an occupied reference branch are explicit corrections needed for normalization and coherence. The conditional zero-branch guarantee strengthens literal Eq. (7) only when and is not inferred from it. Pauli-product phases are retained through the Bell basis change and its inverse. The ordinary positive- regime is explicit; nonzero constant polynomials are included, and asymptotic bounds are applied only above their stated thresholds.
Correction to the printed source.
Printed: Theorem 5 displays j=1,...,l, does not explicitly type a_j or exclude P(H)=0, and refers to Eq.(7), which specifies decoder action only for 1<=|y|<=l. The proof suppresses Pauli-product phases in its Bell-basis display.
Corrected: Use the proof convention j=0,...,l with real polynomial coefficients; require P(H)!=0; retain Eq.(7) and require D|0,0>=|0,0> only if the Eq.(10) coefficient w_0 is nonzero. Preserve product phases under the coherent Bell transform and its inverse.
Reason: The proof and MPS boundaries include a_0. Real coefficients and P(H)!=0 make P(H)^2/Tr[P(H)^2] a density matrix. Eq.(7) leaves an occupied zero branch uncontrolled; fixing only that occupied branch restores coherent erasure without excluding H=I,P=x, whose w_0 vanishes and whose positive-weight decoder necessarily moves |0,0>. A linear Bell transform must preserve Pauli-product signs.
Let and be integers. Let be a classically known Hamiltonian on qubits, where and the are distinct canonical Hermitian Pauli operators that commute pairwise. Let be a real polynomial of degree exactly , and assume . Write for the matrix whose columns are the symplectic labels of the , with the coordinates preceding the coordinates. Assume there exists a unitary decoder on the -qubit label register and the -qubit syndrome register satisfying
Here is Hamming weight and is the zero-string reference coefficient defined below. The zero-branch guarantee is required only when ; when , that decoder input is unrestricted. All other decoder inputs are unrestricted.
There is an exact quantum preparation circuit, chosen from the known Hamiltonian and polynomial before choosing the decoder, that works for every decoder with these guarantees and prepares
It starts with zeroed registers, uses exactly one plain forward application of , and uses no adjoint or controlled decoder calls. The output is the reduced density matrix after discarding the other registers, with no postselection or success-probability qualification.
For clarity, define the real reference coefficients and their normalization by
The reference is constructed by the algorithm, rather than supplied as input. In particular,
where ; both and have unit norm.
The circuit includes a concrete classical arithmetic program that computes and all boundary and local-matrix entries of the reference MPS from the coefficients alone. It may introduce only the numeric constants , and the entries of its quantum gates are obtained from that program's results. There exist an absolute , a polynomial with nonnegative integer coefficients, and thresholds and , all independent of sizes, Pauli terms, coefficients, and decoder, such that
Here classical cost counts actual arithmetic and memory instructions, and quantum cost counts the circuit's gate and oracle steps plus initialization of its qubits. This is the paper's ideal model with unit-cost real arithmetic and exact arbitrary one- and two-qubit unitary gates.
This result supplies an exact polynomial-filtered density matrix using a perfect decoder even for general real commuting Pauli coefficients, without assuming the reference state has already been prepared.
Formalization Note. The proof's convention replaces the theorem display's . Real polynomial coefficients, the nonzero condition, and the decoder's zero-branch guarantee for an occupied reference branch are explicit corrections needed for normalization and coherence. The conditional zero-branch guarantee strengthens literal Eq. (7) only when and is not inferred from it. Pauli-product phases are retained through the Bell basis change and its inverse. The ordinary positive- regime is explicit; nonzero constant polynomials are included, and asymptotic bounds are applied only above their stated thresholds.
Correction to the printed source.
Printed: Theorem 5 displays j=1,...,l, does not explicitly type a_j or exclude P(H)=0, and refers to Eq.(7), which specifies decoder action only for 1<=|y|<=l. The proof suppresses Pauli-product phases in its Bell-basis display.
Corrected: Use the proof convention j=0,...,l with real polynomial coefficients; require P(H)!=0; retain Eq.(7) and require D|0,0>=|0,0> only if the Eq.(10) coefficient w_0 is nonzero. Preserve product phases under the coherent Bell transform and its inverse.
Reason: The proof and MPS boundaries include a_0. Real coefficients and P(H)!=0 make P(H)^2/Tr[P(H)^2] a density matrix. Eq.(7) leaves an occupied zero branch uncontrolled; fixing only that occupied branch restores coherent erasure without excluding H=I,P=x, whose w_0 vanishes and whose positive-weight decoder necessarily moves |0,0>. A linear Bell transform must preserve Pauli-product signs.
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.
Multivariate Decoded Quantum Interferometry for Weighted Optimization establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be prime and . Let with , and let have cardinality . Define on and otherwise. Partition into nonempty blocks , write , and assign positive weights . Put and , where is row of and .
Fix an exact degree ratio , with integer , and assume , where is the minimum nonzero Hamming weight in (infinite when this kernel is zero). Let be the supremum of over complex multivariate polynomials of total degree at most such that has unit norm. This supremum is attained by an admissible polynomial.
Write , , , and define
For each fixed , there are and an integer , chosen before all other instance data and , such that every admissible instance with satisfies
Along any admissible family with fixed , unbounded , and eventually bounded , the residual tends to zero. No convergence of block proportions is required.
This characterizes the asymptotically optimal signed weighted objective among multivariate DQI states. It does not impose decoder access or a preparation complexity bound.
Formalization Note The range is explicitly recalled by Appendix A (PDF p.30) and is carried as a standing assumption although omitted from the printed theorem sentence. Exact integer pairs are used; no rounding convention is added.
Let be prime and . Let with , and let have cardinality . Define on and otherwise. Partition into nonempty blocks , write , and assign positive weights . Put and , where is row of and .
Fix an exact degree ratio , with integer , and assume , where is the minimum nonzero Hamming weight in (infinite when this kernel is zero). Let be the supremum of over complex multivariate polynomials of total degree at most such that has unit norm. This supremum is attained by an admissible polynomial.
Write , , , and define
For each fixed , there are and an integer , chosen before all other instance data and , such that every admissible instance with satisfies
Along any admissible family with fixed , unbounded , and eventually bounded , the residual tends to zero. No convergence of block proportions is required.
This characterizes the asymptotically optimal signed weighted objective among multivariate DQI states. It does not impose decoder access or a preparation complexity bound.
Formalization Note The range is explicitly recalled by Appendix A (PDF p.30) and is carried as a standing assumption although omitted from the printed theorem sentence. Exact integer pairs are used; no rounding convention is added.
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.
Randomized and quantum approximate matrix multiplication establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix a classical exact-arithmetic matrix multiplication implementation with achievable exponent . Let , , and let be arbitrary matrices. Write , where . Given absolute accuracy and failure probability , there are fixed input-taking classical and quantum circuit families, with classical preprocessing time , which return classical matrices and satisfying
Apart from input/output and preprocessing overhead, their running times are respectively
The soft factors include the confidence logarithms and are uniform over dimensions, factors, matrix entries, accuracy, and confidence; constants may depend on the chosen multiplication implementation. Real numbers are represented exactly, and fixed-position retrieval and arithmetic are charged in both models. The quantum output is an ordinary classical matrix. No efficiently addressable classical or quantum memory is required.
The case returns the input matrix exactly. For and , both families return zero; this includes every zero factor. These branches still pay for the input and classical output. The displayed online scales are clamped below by , and the formal total bound includes explicitly. This result compares approximate products in two different error norms under the same circuit access model.
Formalization Note Lean uses interfaces and computes during charged classical preprocessing. Rounded, confidence-dependent sample budgets select members of circuit families fixed before the matrices. The classical law is computed from one fixed list of exact-real arithmetic, random-coin and comparison instructions, with each comparison writing a 0/1 register value and every instruction charged; quantum probabilities and work are computed from the frozen exact-real mean-estimation circuit language. No approximation guarantee or arbitrary runtime number is assumed as a field of an algorithm.
Fix a classical exact-arithmetic matrix multiplication implementation with achievable exponent . Let , , and let be arbitrary matrices. Write , where . Given absolute accuracy and failure probability , there are fixed input-taking classical and quantum circuit families, with classical preprocessing time , which return classical matrices and satisfying
Apart from input/output and preprocessing overhead, their running times are respectively
The soft factors include the confidence logarithms and are uniform over dimensions, factors, matrix entries, accuracy, and confidence; constants may depend on the chosen multiplication implementation. Real numbers are represented exactly, and fixed-position retrieval and arithmetic are charged in both models. The quantum output is an ordinary classical matrix. No efficiently addressable classical or quantum memory is required.
The case returns the input matrix exactly. For and , both families return zero; this includes every zero factor. These branches still pay for the input and classical output. The displayed online scales are clamped below by , and the formal total bound includes explicitly. This result compares approximate products in two different error norms under the same circuit access model.
Formalization Note Lean uses interfaces and computes during charged classical preprocessing. Rounded, confidence-dependent sample budgets select members of circuit families fixed before the matrices. The classical law is computed from one fixed list of exact-real arithmetic, random-coin and comparison instructions, with each comparison writing a 0/1 register value and every instruction charged; quantum probabilities and work are computed from the frozen exact-real mean-estimation circuit language. No approximation guarantee or arbitrary runtime number is assumed as a field of an algorithm.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Fast Convex Optimization with Quantum Gradient Methods establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be closed, bounded and convex, let , and let be convex and ambient -Lipschitz in the stated norm. Assume an attained constrained optimum , and . Both branches use coherent binary evaluations on sufficiently fine finite translated hypergrids: every grid index is preserved, the encoded value has error strictly below , and calls to the unitary and its adjoint are counted. The algorithm construction is fixed before the objective, optimum and oracle values; only geometry and supplied numerical scale bounds enter its construction.
A sufficient scale is a small absolute constant times
This retains both noise terms; a sufficient positive precision takes the minimum of the lemma guard and small absolute multiples of and .
In either branch the classical output is the average of the first iterates, and
The query costs are , with absolute constants common to all data, yielding and , respectively. Quantum arithmetic uses gates, with binary word length and inverse precision exposed as polynomial arithmetic factors. Supplied geometric operations cost at most and , respectively. All bounds apply on positive-probability branches. Conditional per-call failure control suffices; independence is not assumed.
Zero-dimensional, constant-objective, zero-radius, singleton, or already-accurate regimes return the feasible start with zero queries before divisions. In particular, a start is already accurate if , or in the Euclidean branch, or in the mirror branch.
The result shows that quantum zeroth-order methods attain the corresponding first-order nonsmooth query rates. Formalization Note: This uses the formal appendix scope, including ambient Lipschitz control, rather than the informal “on ” access description. The Euclidean precision corrects B.3's omitted independent ; its printed denominator follows in the domain-radius regime , which is not implied by an initial distance. The mirror radius is computed from the Bregman divergence, not introduced by an arbitrary equality. The finite-grid compilation and adaptive execution definitions are submitted for local definition review.
Let be closed, bounded and convex, let , and let be convex and ambient -Lipschitz in the stated norm. Assume an attained constrained optimum , and . Both branches use coherent binary evaluations on sufficiently fine finite translated hypergrids: every grid index is preserved, the encoded value has error strictly below , and calls to the unitary and its adjoint are counted. The algorithm construction is fixed before the objective, optimum and oracle values; only geometry and supplied numerical scale bounds enter its construction.
A sufficient scale is a small absolute constant times
This retains both noise terms; a sufficient positive precision takes the minimum of the lemma guard and small absolute multiples of and .
In either branch the classical output is the average of the first iterates, and
The query costs are , with absolute constants common to all data, yielding and , respectively. Quantum arithmetic uses gates, with binary word length and inverse precision exposed as polynomial arithmetic factors. Supplied geometric operations cost at most and , respectively. All bounds apply on positive-probability branches. Conditional per-call failure control suffices; independence is not assumed.
Zero-dimensional, constant-objective, zero-radius, singleton, or already-accurate regimes return the feasible start with zero queries before divisions. In particular, a start is already accurate if , or in the Euclidean branch, or in the mirror branch.
The result shows that quantum zeroth-order methods attain the corresponding first-order nonsmooth query rates. Formalization Note: This uses the formal appendix scope, including ambient Lipschitz control, rather than the informal “on ” access description. The Euclidean precision corrects B.3's omitted independent ; its printed denominator follows in the domain-radius regime , which is not implied by an initial distance. The mirror radius is computed from the Bregman divergence, not introduced by an arbitrary equality. The finite-grid compilation and adaptive execution definitions are submitted for local definition review.
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 Signal Processing and Quantum Singular Value Transformation on establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be an integer and let be an matrix of complex polynomials, with . Each entry has degree at most and parity : . Suppose
Let be positive finite input, output, and signal registers, and fix known isometric computational-basis embeddings and . The mixing register has qubits, with fixed embeddings of the input labels and output labels in its basis states; unused rows and columns are zero padded. An admissible oracle is any unitary on with exact unscaled block .
There are known unitary mixers on the mixing register enlarged by one flag qubit, and a fixed identification of the flag and mixing registers, chosen from and the known embeddings before or is supplied. The resulting synthesis circuit alternates these known operations with exactly uncontrolled oracle calls . A mixer acts conditioned on the known input signal projector at even stages and the known output signal projector at odd stages. For every admissible oracle and every family of input vectors , the entire flag-zero component of its output is
Here the input is , and for even and for odd . Writing , the singular-value transforms are
All remaining amplitude lies in flag one. This simultaneously block-encodes the whole polynomial matrix at normalization one and error zero, without a positive success-probability guarantee. The formula includes the input kernel in the even case, where the constant coefficient acts as a multiple of the identity. Singular , rectangular and , zero , and are permitted. A normalized joint input gives a physical state, while the equality itself is linear and holds for all vectors.
This theorem supplies coherent matrix-valued singular-value synthesis under a single matrix contraction condition. No Hermiticity, invertibility, determinant constraint, finite gate set, or classical synthesis-time estimate is imposed.
Formalization Note The printed Theorem 10 omits the degree and common-parity requirements used by its proof; these are explicit here. The output signal zero register and the orientation of the singular-vector decomposition are corrected according to Eqs. (1) and (31)–(35). The printed claim and these corrections are recorded separately in the audit notes. Known embeddings express the all-zero signal-ancilla subspaces in register-independent coordinates.
Let be an integer and let be an matrix of complex polynomials, with . Each entry has degree at most and parity : . Suppose
Let be positive finite input, output, and signal registers, and fix known isometric computational-basis embeddings and . The mixing register has qubits, with fixed embeddings of the input labels and output labels in its basis states; unused rows and columns are zero padded. An admissible oracle is any unitary on with exact unscaled block .
There are known unitary mixers on the mixing register enlarged by one flag qubit, and a fixed identification of the flag and mixing registers, chosen from and the known embeddings before or is supplied. The resulting synthesis circuit alternates these known operations with exactly uncontrolled oracle calls . A mixer acts conditioned on the known input signal projector at even stages and the known output signal projector at odd stages. For every admissible oracle and every family of input vectors , the entire flag-zero component of its output is
Here the input is , and for even and for odd . Writing , the singular-value transforms are
All remaining amplitude lies in flag one. This simultaneously block-encodes the whole polynomial matrix at normalization one and error zero, without a positive success-probability guarantee. The formula includes the input kernel in the even case, where the constant coefficient acts as a multiple of the identity. Singular , rectangular and , zero , and are permitted. A normalized joint input gives a physical state, while the equality itself is linear and holds for all vectors.
This theorem supplies coherent matrix-valued singular-value synthesis under a single matrix contraction condition. No Hermiticity, invertibility, determinant constraint, finite gate set, or classical synthesis-time estimate is imposed.
Formalization Note The printed Theorem 10 omits the degree and common-parity requirements used by its proof; these are explicit here. The output signal zero register and the orientation of the singular-vector decomposition are corrected according to Eqs. (1) and (31)–(35). The printed claim and these corrections are recorded separately in the audit notes. Known embeddings express the all-zero signal-ancilla subspaces in register-independent coordinates.
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 speedups for stochastic optimization establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let and let be differentiable and globally convex. Suppose attains its global minimum at a point with , where are public bounds. For every query point , the stochastic gradient is drawn from a measurable probability law satisfying
Assume coherent unitary access to this gradient law, preserving the query point and allowing arbitrary garbage, and access to the inverse oracle. The implementation uses normalized zero registers, Born measurement laws, and known Gaussian preparation and reordering operations that construct the smoothed oracle with one gradient-oracle call. These operations and the mean-estimation routine are fixed before the unknown objective and oracle. The mean-estimation interface cited on p.8 is realized, rather than assumed as a convergence hypothesis: for any sampling oracle with variance at most , requested error , and , its execution has total probability one and finite expected calls, and its estimate is within Euclidean distance of the mean with probability at least .
For any , run Algorithm 3 with fresh Algorithm 2 gradient estimates. In the nontrivial case and , its parameters are
It starts from . At iteration , set , , and . Use Algorithm 2 on the Gaussian-smoothed gradient law at , then use the printed ball-constrained update
The returned point is . The same execution, including its classical randomness and quantum measurements, has total probability one and satisfies
Here counts every call to the original gradient oracle and its inverse. Its expectation is finite; the positive geometric level in Algorithm 2 allows an unbounded query count. Explicitly, there are absolute constants , an integer , and a threshold , all independent of the dimension, bounds, accuracy, objective, probability laws, and register realization, such that whenever ,
If , , or , the implementation returns with no queries and retains the expected-accuracy guarantee. The minimizing point is used only to express the guarantee and is not supplied to the algorithm. This result gives the expected-query speedup of the paper's quantum accelerated stochastic approximation method; it asserts no gate-complexity or fixed-confidence output bound.
Formalization Note The real iteration budget on p.13 is rounded upward to define a finite loop. The statement preserves the proximal center and all other displayed constants. The p.13/p.15 pointwise gradient assertion is incompatible with the stated second-moment hypothesis; the proof also contains an extra factor , a reversed optimum-gap sign, and a constant gap in its use of Lemma 5. These are disclosed proof gaps, not additional hypotheses or silent changes to Algorithm 3. No directional-mean definition is imported or reconstructed.
Let and let be differentiable and globally convex. Suppose attains its global minimum at a point with , where are public bounds. For every query point , the stochastic gradient is drawn from a measurable probability law satisfying
Assume coherent unitary access to this gradient law, preserving the query point and allowing arbitrary garbage, and access to the inverse oracle. The implementation uses normalized zero registers, Born measurement laws, and known Gaussian preparation and reordering operations that construct the smoothed oracle with one gradient-oracle call. These operations and the mean-estimation routine are fixed before the unknown objective and oracle. The mean-estimation interface cited on p.8 is realized, rather than assumed as a convergence hypothesis: for any sampling oracle with variance at most , requested error , and , its execution has total probability one and finite expected calls, and its estimate is within Euclidean distance of the mean with probability at least .
For any , run Algorithm 3 with fresh Algorithm 2 gradient estimates. In the nontrivial case and , its parameters are
It starts from . At iteration , set , , and . Use Algorithm 2 on the Gaussian-smoothed gradient law at , then use the printed ball-constrained update
The returned point is . The same execution, including its classical randomness and quantum measurements, has total probability one and satisfies
Here counts every call to the original gradient oracle and its inverse. Its expectation is finite; the positive geometric level in Algorithm 2 allows an unbounded query count. Explicitly, there are absolute constants , an integer , and a threshold , all independent of the dimension, bounds, accuracy, objective, probability laws, and register realization, such that whenever ,
If , , or , the implementation returns with no queries and retains the expected-accuracy guarantee. The minimizing point is used only to express the guarantee and is not supplied to the algorithm. This result gives the expected-query speedup of the paper's quantum accelerated stochastic approximation method; it asserts no gate-complexity or fixed-confidence output bound.
Formalization Note The real iteration budget on p.13 is rounded upward to define a finite loop. The statement preserves the proximal center and all other displayed constants. The p.13/p.15 pointwise gradient assertion is incompatible with the stated second-moment hypothesis; the proof also contains an extra factor , a reversed optimum-gap sign, and a constant gap in its use of Lemma 5. These are disclosed proof gaps, not additional hypotheses or silent changes to Algorithm 3. No directional-mean definition is imported or reconstructed.
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 Quantum Esscher Transform establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let , , , and be public parameters. Set
where . The input is an -qubit trace-one density operator whose eigenvalues lie in . Each is Hermitian with . Purified access is a unitary on qubits preparing a purification of , with the ancillary qubits first. Let be the exact block-encoding supplied by the purification construction of Proposition 12. For each , supplied is a block-encoding of ; ordinary, adjoint and controlled signal access are available.
There are universal constants , a nonnegative integer , and a universal threshold such that, for every admissible public parameter choice with , a QEsscher circuit can be selected before . This circuit is the logarithm transformation, coefficient state-preparation pair, padded linear combination, and exponential transformation of Algorithm 1. It works for every admissible hidden input and oracle completion. With and , its unitary satisfies
Its oracle counts, including ordinary, adjoint and controlled calls, obey
The logarithm of a positive matrix is defined by applying to its eigenvalues; is the natural matrix exponential. The constants, exponent and threshold are independent of all public parameters, hidden matrices and oracle implementations.
This supplies the subnormalized transform as a block-encoding, useful as an operator primitive. The query count is for ; each such call can be implemented with a constant number of purification-oracle calls. The actual is retained in the footprint; the source's is a family convention, and no gate-time conclusion is asserted.
Source corrections and limitation. Algorithm 1 and Step 3 print , although their coefficients require . The box prints the divisor ; the statement uses proof Step 5's explicit . The printed error schedule is retained. The claim that its numeral 8 ensures Eq. (III.2) has an unresolved quantitative degree-bound gap; accuracy remains the theorem's conclusion, without adding that bound as an assumption.
Let , , , and be public parameters. Set
where . The input is an -qubit trace-one density operator whose eigenvalues lie in . Each is Hermitian with . Purified access is a unitary on qubits preparing a purification of , with the ancillary qubits first. Let be the exact block-encoding supplied by the purification construction of Proposition 12. For each , supplied is a block-encoding of ; ordinary, adjoint and controlled signal access are available.
There are universal constants , a nonnegative integer , and a universal threshold such that, for every admissible public parameter choice with , a QEsscher circuit can be selected before . This circuit is the logarithm transformation, coefficient state-preparation pair, padded linear combination, and exponential transformation of Algorithm 1. It works for every admissible hidden input and oracle completion. With and , its unitary satisfies
Its oracle counts, including ordinary, adjoint and controlled calls, obey
The logarithm of a positive matrix is defined by applying to its eigenvalues; is the natural matrix exponential. The constants, exponent and threshold are independent of all public parameters, hidden matrices and oracle implementations.
This supplies the subnormalized transform as a block-encoding, useful as an operator primitive. The query count is for ; each such call can be implemented with a constant number of purification-oracle calls. The actual is retained in the footprint; the source's is a family convention, and no gate-time conclusion is asserted.
Source corrections and limitation. Algorithm 1 and Step 3 print , although their coefficients require . The box prints the divisor ; the statement uses proof Step 5's explicit . The printed error schedule is retained. The claim that its numeral 8 ensures Eq. (III.2) has an unresolved quantitative degree-bound gap; accuracy remains the theorem's conclusion, without adding that bound as an assumption.
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.
Explicit decoders using fixed-point amplitude amplification based on QSVT establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be any channel on finite registers of positive dimensions , with fixed computational bases. The registers copy , and copies , including their bases. Choose any Stinespring isometry and a compatible unitary with and . Write for the complementary channel derived from this same isometry, for the normalized computational-basis maximally entangled state, and . Define and let be its smallest strictly positive eigenvalue.
Suppose there is a density state such that . For every and every odd positive integer satisfying
there are phases for the explicit generalized Yoshida–Kitaev decoder of Eq. (44), with preprocessing (35) and the real two-projector QSVT (49)–(53), such that
The channel acts as the identity on the untouched reference and shared register in the expression for . The same choice of phases admits an exact circuit using arbitrary single- and two-qubit unitary gates with universal positive constants such that
Here the standing circuit model of Section 2.1 permits only polynomially many ancillary qubits. One polynomial allowance is chosen before all dimensions, channels and dilations. With , is the minimum exact gate count for the chosen dilation unitary within an added-ancilla budget , including its input and output basis layout; the displayed denotes this cost under the common chosen allowance. Both constants are independent of the channel, dimensions, chosen dilation, errors and . The decoder acts only on the receiver's systems and locally prepared ancillas. This supplies an explicit recovery circuit whenever decoupling holds, including unassisted communication (), exact decoupling (), and rank-deficient states.
Formalization Note Finite registers are embedded in qubits by the frozen finite-register embedding; no power-of-two dimension assumption is added. The full trace norm is used for decoupling and half that norm for recovery. The logarithm in the degree threshold is natural, as in the proof's Lambert-W estimate; qubit resource logarithms are base two. The compatible dimension identity makes the resource logarithm nonnegative. When it vanishes, the recovered register is one-dimensional and discarding the input uses zero gates and added ancillas.
Let be any channel on finite registers of positive dimensions , with fixed computational bases. The registers copy , and copies , including their bases. Choose any Stinespring isometry and a compatible unitary with and . Write for the complementary channel derived from this same isometry, for the normalized computational-basis maximally entangled state, and . Define and let be its smallest strictly positive eigenvalue.
Suppose there is a density state such that . For every and every odd positive integer satisfying
there are phases for the explicit generalized Yoshida–Kitaev decoder of Eq. (44), with preprocessing (35) and the real two-projector QSVT (49)–(53), such that
The channel acts as the identity on the untouched reference and shared register in the expression for . The same choice of phases admits an exact circuit using arbitrary single- and two-qubit unitary gates with universal positive constants such that
Here the standing circuit model of Section 2.1 permits only polynomially many ancillary qubits. One polynomial allowance is chosen before all dimensions, channels and dilations. With , is the minimum exact gate count for the chosen dilation unitary within an added-ancilla budget , including its input and output basis layout; the displayed denotes this cost under the common chosen allowance. Both constants are independent of the channel, dimensions, chosen dilation, errors and . The decoder acts only on the receiver's systems and locally prepared ancillas. This supplies an explicit recovery circuit whenever decoupling holds, including unassisted communication (), exact decoupling (), and rank-deficient states.
Formalization Note Finite registers are embedded in qubits by the frozen finite-register embedding; no power-of-two dimension assumption is added. The full trace norm is used for decoupling and half that norm for recovery. The logarithm in the degree threshold is natural, as in the proof's Lambert-W estimate; qubit resource logarithms are base two. The compatible dimension identity makes the resource logarithm nonnegative. When it vanishes, the recovered register is one-dimensional and discarding the input uses zero gates and added ancillas.
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.
Amplitude Estimation from Quantum Signal Processing establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be an unknown amplitude in the completed two-dimensional Grover space. Choose an orthonormal pair , set , and write and . The endpoint states are understood as rays. Define and . A complex polynomial is Pellian if there is a polynomial of the opposite fixed parity such that for every . A real polynomial is semi-Pellian if it is the coefficientwise real part of a Pellian polynomial.
There is an absolute constant such that, for every Pellian or semi-Pellian polynomial , an oracle instrument can be chosen independently of and of the orthonormal basis. Given one copy of any of the four states and its known classical label, the instrument outputs a bit satisfying
It also returns a classical label for a retained signal state. For each joint outcome of probability , the unnormalized signal density matrix is exactly , with . This includes both sampled-bit outcomes. The total number of oracle calls, including the oracle-assisted final basis measurement, is at most for every input label. Pellian sampling uses arbitrary-angle rotations , with the controlled measurement access used in the proof. Semi-Pellian sampling uses the distinct primitives for each basis. Ancilla preparation and known ancilla gates are free in this query model.
The retained-state guarantee allows successive polynomial samples from the same signal system, without requiring that each invocation restore the original state.
Formalization Note The completed Grover-space model includes and uses density matrices to ignore global phase. The asymptotic query claim is expressed with a uniform additive degree-zero allowance. Controlled access for the Pellian basis measurement is the operational convention of the source's proof; it is not derived from a strictly uncontrolled black box.
Let be an unknown amplitude in the completed two-dimensional Grover space. Choose an orthonormal pair , set , and write and . The endpoint states are understood as rays. Define and . A complex polynomial is Pellian if there is a polynomial of the opposite fixed parity such that for every . A real polynomial is semi-Pellian if it is the coefficientwise real part of a Pellian polynomial.
There is an absolute constant such that, for every Pellian or semi-Pellian polynomial , an oracle instrument can be chosen independently of and of the orthonormal basis. Given one copy of any of the four states and its known classical label, the instrument outputs a bit satisfying
It also returns a classical label for a retained signal state. For each joint outcome of probability , the unnormalized signal density matrix is exactly , with . This includes both sampled-bit outcomes. The total number of oracle calls, including the oracle-assisted final basis measurement, is at most for every input label. Pellian sampling uses arbitrary-angle rotations , with the controlled measurement access used in the proof. Semi-Pellian sampling uses the distinct primitives for each basis. Ancilla preparation and known ancilla gates are free in this query model.
The retained-state guarantee allows successive polynomial samples from the same signal system, without requiring that each invocation restore the original state.
Formalization Note The completed Grover-space model includes and uses density matrices to ignore global phase. The asymptotic query claim is expressed with a uniform additive degree-zero allowance. Controlled access for the Pellian basis measurement is the operational convention of the source's proof; it is not derived from a strictly uncontrolled black box.
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.
Single-shot decoding of good quantum LDPC codes establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix code parameters and decoder parameters . For all sufficiently large degrees (with the threshold depending only on these fixed parameters), let be a finite group with symmetric generating sets of size , whose left and right Cayley graphs are Ramanujan in the paper's sense: their second largest adjacency eigenvalue is at most . Let the binary local codes have exact rates , respectively. Each of has distance at least , and both dual tensor codes and are -product-expanding.
Construct the quadripartite quantum Tanner code on , with qubits, X checks from at and Z checks from at . Let be its actual CSS distance. Let be an X error and a binary error on the vertex-labelled Z checks. Write and let count vertices with at least one nonzero syndrome-error bit. Define
If
then Algorithm 1, receiving only and parameter , terminates and every lawful output satisfies
Local minimum-weight choices are fixed consistently before the input; infeasible local syndromes use the zero fallback. Algorithm 2 starts with zero accumulators, uses the stated weight-decrease test and minimum column/row decomposition, and halts only at zero mismatch or when no permitted move exists. Algorithm 1 returns .
This is the quantitative adversarial single-shot guarantee for the sequential Tanner decoder. With , the residual is a stabilizer, rather than necessarily the zero vector.
Formalization Note The printed theorem leaves decoder domains implicit; the range above is inherited from pp.14 and 22. The distance is an extended natural minimum; when both logical-error sets are empty it is infinite, and the threshold uses only . Termination is represented by existence of a terminal execution together with the bound for every lawful terminal execution. No stochastic residual support law is asserted.
Fix code parameters and decoder parameters . For all sufficiently large degrees (with the threshold depending only on these fixed parameters), let be a finite group with symmetric generating sets of size , whose left and right Cayley graphs are Ramanujan in the paper's sense: their second largest adjacency eigenvalue is at most . Let the binary local codes have exact rates , respectively. Each of has distance at least , and both dual tensor codes and are -product-expanding.
Construct the quadripartite quantum Tanner code on , with qubits, X checks from at and Z checks from at . Let be its actual CSS distance. Let be an X error and a binary error on the vertex-labelled Z checks. Write and let count vertices with at least one nonzero syndrome-error bit. Define
If
then Algorithm 1, receiving only and parameter , terminates and every lawful output satisfies
Local minimum-weight choices are fixed consistently before the input; infeasible local syndromes use the zero fallback. Algorithm 2 starts with zero accumulators, uses the stated weight-decrease test and minimum column/row decomposition, and halts only at zero mismatch or when no permitted move exists. Algorithm 1 returns .
This is the quantitative adversarial single-shot guarantee for the sequential Tanner decoder. With , the residual is a stabilizer, rather than necessarily the zero vector.
Formalization Note The printed theorem leaves decoder domains implicit; the range above is inherited from pp.14 and 22. The distance is an extended natural minimum; when both logical-error sets are empty it is infinite, and the threshold uses only . Termination is represented by existence of a terminal execution together with the bound for every lawful terminal execution. No stochastic residual support law is asserted.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Fast Estimation of Sparse Quantum Noise establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix a sparsity exponent . There are positive constants and a threshold , depending only on this fixed exponent and public design/code choices, and a public construction of the subsampling and peeling protocol for every and integer .
The labels of the phase-free -qubit Paulis are . Let be uniform among the size- subsets of these labels. For each possible , assign arbitrary nonnegative rates with total mass one, support exactly , and on . This assignment is independent of the protocol's public randomness and observation noise. The associated channel is , and its eigenvalues are
The observed eigenvalue vector has independent centered Gaussian errors of variance , with , independent of the support and the public design. Repeated reads use the same indexed observation and are counted as queries.
The construction chooses bins with , constantly many subsampling groups, and offsets. Random offsets and binary hash matrices are sampled independently and uniformly before the hidden input. Coded offsets use a full-rank binary linear code with positive constant relative distance and a public, query-free, linear-time decoder. The decoder's realization, correction property and time bound are conclusions of the construction. Assume
Algorithms 2–4 produce a list of distinct labels with support exactly and estimated rates , zero off the reported support, satisfying
The probability averages over the uniform support, public design, Gaussian observations, and any internal decoder randomness. Every execution uses at most eigenvalue reads and classical arithmetic/indexing instructions. The computed conditional success probabilities are measurable.
This result recovers both the locations and values of sparse Pauli errors from noisy eigenvalues. It does not assert a quantum measurement sample complexity.
Formalization Note The frozen, independently reviewed program composition is used directly. It separates the ordinary -bit WHT from the symplectic -bit label pairing, resolves the printed dimensional inconsistencies as approved in the definition review, and retires peeled bins according to the graph description. The theorem does not assume successful bin detection, favorable graph events, accuracy, runtime, or independence of overlapping bin errors.
Fix a sparsity exponent . There are positive constants and a threshold , depending only on this fixed exponent and public design/code choices, and a public construction of the subsampling and peeling protocol for every and integer .
The labels of the phase-free -qubit Paulis are . Let be uniform among the size- subsets of these labels. For each possible , assign arbitrary nonnegative rates with total mass one, support exactly , and on . This assignment is independent of the protocol's public randomness and observation noise. The associated channel is , and its eigenvalues are
The observed eigenvalue vector has independent centered Gaussian errors of variance , with , independent of the support and the public design. Repeated reads use the same indexed observation and are counted as queries.
The construction chooses bins with , constantly many subsampling groups, and offsets. Random offsets and binary hash matrices are sampled independently and uniformly before the hidden input. Coded offsets use a full-rank binary linear code with positive constant relative distance and a public, query-free, linear-time decoder. The decoder's realization, correction property and time bound are conclusions of the construction. Assume
Algorithms 2–4 produce a list of distinct labels with support exactly and estimated rates , zero off the reported support, satisfying
The probability averages over the uniform support, public design, Gaussian observations, and any internal decoder randomness. Every execution uses at most eigenvalue reads and classical arithmetic/indexing instructions. The computed conditional success probabilities are measurable.
This result recovers both the locations and values of sparse Pauli errors from noisy eigenvalues. It does not assert a quantum measurement sample complexity.
Formalization Note The frozen, independently reviewed program composition is used directly. It separates the ordinary -bit WHT from the symplectic -bit label pairing, resolves the printed dimensional inconsistencies as approved in the definition review, and retires peeled bins according to the graph description. The theorem does not assume successful bin detection, favorable graph events, accuracy, runtime, or independence of overlapping bin errors.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Provably efficient machine learning for quantum many-body problems establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix a finite spatial dimension , bounds on the number and geometric radius of sites in each Hamiltonian term, a local-term density bound , a spectral gap , an observable locality bound , and a confidence parameter . Consider -qubit Hamiltonians , smoothly parametrized by . Each term is Hermitian, obeys , and has directional derivative of operator norm at most one in every Euclidean unit parameter direction. These properties hold throughout the cube; smoothness at its boundary uses a local smooth extension. Every Hamiltonian has an excited energy and a gap at least above its entire ground eigenspace. Let be the normalized projector onto that eigenspace, allowing degeneracy.
For a fixed Hermitian observable , each term supported on at most qubits (not necessarily neighboring), choose a norm budget satisfying . A smaller norm budget may be replaced by one. There are uniform positive constants, depending only on the fixed physical bounds, , and , such that for every fixed mean-squared error tolerance and all sufficiently large , public sample counts, cutoffs, and actual classical arithmetic/RAM programs can be selected before the unknown Hamiltonian family, training draw, observable entries, and test parameter. The training set consists of independent uniform parameter draws, with one fresh-copy randomized Pauli snapshot at each point. Pauli axes are independently uniform; the joint measurement outcomes obey the Born law.
The named predictor is
For each observable fixed before the training draw,
with and computed classical training and prediction work . The compact representation stores real parameter words and six-valued labels, encodable in bits. The programs read and store those data and compute the observable value; they do not materialize the represented matrix. Ground-state preparation and data generation are excluded from this classical work.
For every fixed subsystem of at most qubits, separately with confidence at least ,
Thus taking gives the informal constant trace-norm error on a fixed few-body reduced matrix. This conversion uses the finite Pauli expansion and allocates confidence to its coefficients; it leaves the polynomial-in-, linear-in- conclusion intact at fixed accuracy and locality.
This result describes generalization in population average for the source's compact shadow predictor. It asserts neither pointwise error nor simultaneous accuracy on all observables or subsystems, and does not require the predicted representation to be positive or trace one.
Formalization Note Theorem 3 on PDF pp.29–30 explicitly identifies itself as the detailed restatement of Theorem 1. Its Eq. (F3) prints exact ground-state labels, whereas its premise and Eqs. (2), (E3), and (F27) specify shadow labels; the latter determine the model above. This discrepancy and the nonperiodic-boundary gap in Lemma 2 are recorded for independent source moderation, without adding periodicity or a gradient bound as hypotheses.
Fix a finite spatial dimension , bounds on the number and geometric radius of sites in each Hamiltonian term, a local-term density bound , a spectral gap , an observable locality bound , and a confidence parameter . Consider -qubit Hamiltonians , smoothly parametrized by . Each term is Hermitian, obeys , and has directional derivative of operator norm at most one in every Euclidean unit parameter direction. These properties hold throughout the cube; smoothness at its boundary uses a local smooth extension. Every Hamiltonian has an excited energy and a gap at least above its entire ground eigenspace. Let be the normalized projector onto that eigenspace, allowing degeneracy.
For a fixed Hermitian observable , each term supported on at most qubits (not necessarily neighboring), choose a norm budget satisfying . A smaller norm budget may be replaced by one. There are uniform positive constants, depending only on the fixed physical bounds, , and , such that for every fixed mean-squared error tolerance and all sufficiently large , public sample counts, cutoffs, and actual classical arithmetic/RAM programs can be selected before the unknown Hamiltonian family, training draw, observable entries, and test parameter. The training set consists of independent uniform parameter draws, with one fresh-copy randomized Pauli snapshot at each point. Pauli axes are independently uniform; the joint measurement outcomes obey the Born law.
The named predictor is
For each observable fixed before the training draw,
with and computed classical training and prediction work . The compact representation stores real parameter words and six-valued labels, encodable in bits. The programs read and store those data and compute the observable value; they do not materialize the represented matrix. Ground-state preparation and data generation are excluded from this classical work.
For every fixed subsystem of at most qubits, separately with confidence at least ,
Thus taking gives the informal constant trace-norm error on a fixed few-body reduced matrix. This conversion uses the finite Pauli expansion and allocates confidence to its coefficients; it leaves the polynomial-in-, linear-in- conclusion intact at fixed accuracy and locality.
This result describes generalization in population average for the source's compact shadow predictor. It asserts neither pointwise error nor simultaneous accuracy on all observables or subsystems, and does not require the predicted representation to be positive or trace one.
Formalization Note Theorem 3 on PDF pp.29–30 explicitly identifies itself as the detailed restatement of Theorem 1. Its Eq. (F3) prints exact ground-state labels, whereas its premise and Eqs. (2), (E3), and (F27) specify shadow labels; the latter determine the model above. This discrepancy and the nonperiodic-boundary gap in Lemma 2 are recorded for independent source moderation, without adding periodicity or a gradient bound as hypotheses.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Foundations for learning from noisy quantum experiments establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix a positive finite dimension and finite labelled sets of preparation actions, dynamics actions, measurement actions, and measurement outcomes. Let be any set of world models on : every preparation is a density matrix, every dynamics action is a CPTP map, and each measurement is a POVM. The model class may be uncountable and may contain equivalent descriptions.
Suppose every is universal: some preparation is pure; some finite collection of dynamics actions implements exact unitary channels whose representatives generate a dense subgroup of ; and some measurement effect is not proportional to the identity. These witnessing actions and their physical descriptions are unknown and may vary between worlds. Mathematical inverses enter the generated subgroup; physical access to inverse actions is not assumed.
Then there exists a fixed family of finite classical experimental procedures, chosen before the unknown world. Each procedure adaptively chooses experiments that freshly prepare , apply a finite word of the available dynamics actions, and measure one of the available POVMs. Its description output is denoted . For every , every , and every , there exists such that for all there is one unitary or anti-unitary gauge satisfying
Here is computed from the experimental outcome probabilities and internal classical randomization of . A unitary gauge has the form ; an anti-unitary gauge has the form . The same gauge is fixed outside all three collections of probability clauses. Both norms are unhalved. The output estimates need not themselves be lawful quantum objects.
The result establishes learnability of all labelled operations from untrusted experiments under universality. It gives eventual accuracy for each world, with no uniform sample bound, polynomial complexity guarantee, or certified accuracy-based stopping rule.
Formalization Note The finite-action scope is explicit in Theorem D.1 (PDF p.21), although the main-text Theorem 2 does not explicitly restrict the action sets. The stage-indexed interpretation follows the precision-halving procedure in D.2 (p.23) and D.7 (p.33).
Fix a positive finite dimension and finite labelled sets of preparation actions, dynamics actions, measurement actions, and measurement outcomes. Let be any set of world models on : every preparation is a density matrix, every dynamics action is a CPTP map, and each measurement is a POVM. The model class may be uncountable and may contain equivalent descriptions.
Suppose every is universal: some preparation is pure; some finite collection of dynamics actions implements exact unitary channels whose representatives generate a dense subgroup of ; and some measurement effect is not proportional to the identity. These witnessing actions and their physical descriptions are unknown and may vary between worlds. Mathematical inverses enter the generated subgroup; physical access to inverse actions is not assumed.
Then there exists a fixed family of finite classical experimental procedures, chosen before the unknown world. Each procedure adaptively chooses experiments that freshly prepare , apply a finite word of the available dynamics actions, and measure one of the available POVMs. Its description output is denoted . For every , every , and every , there exists such that for all there is one unitary or anti-unitary gauge satisfying
Here is computed from the experimental outcome probabilities and internal classical randomization of . A unitary gauge has the form ; an anti-unitary gauge has the form . The same gauge is fixed outside all three collections of probability clauses. Both norms are unhalved. The output estimates need not themselves be lawful quantum objects.
The result establishes learnability of all labelled operations from untrusted experiments under universality. It gives eventual accuracy for each world, with no uniform sample bound, polynomial complexity guarantee, or certified accuracy-based stopping rule.
Formalization Note The finite-action scope is explicit in Theorem D.1 (PDF p.21), although the main-text Theorem 2 does not explicitly restrict the action sets. The stage-indexed interpretation follows the precision-halving procedure in D.2 (p.23) and D.7 (p.33).
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Robust shadow estimation establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Consider Protocol 1 of Chen, Yu, Zeng and Flammia on qubits, with Hilbert space dimension . The same completely positive, trace-preserving noise channel acts after each ideal global Clifford gate; fixed computational-basis measurement noise is absorbed into . Calibration perfectly prepares . The full Clifford group modulo global phase is sampled uniformly and calibration shots are independent and identically distributed.
Let and . Define the Z-basis average fidelity by , and suppose . Set
The printed sample scale in Theorem 7 is . Interpret its real-valued batch parameters operationally as positive integers and , with actual calibration count .
For each recorded ideal Clifford and noisy outcome , compute . Let be the median of the means of batches of such scores. The estimated inverse sends an operator to . Let , where removes off-diagonal computational-basis entries, and let .
With probability at least over calibration records, and the subsequent single-shot retrieval expectation satisfies, simultaneously for every Hermitian observable and every density matrix ,
Here is the operator norm, and the expectation is conditional on the calibration result. This guarantee controls the systematic, asymptotic bias of robust shadow retrieval; it applies to all observables and states on the same successful calibration event.
Formalization Note The statement retains the printed factor. The source proof's substitution instead gives from the stated variance bound; this discrepancy and the integer rounding interpretation remain subject to independent source moderation. The product of rounded batch parameters is not asserted to equal, or be bounded above by the ceiling of, the printed total scale. The frozen calibration probability law, overlap scores, median and retrieval expectation compute the named protocol directly.
Consider Protocol 1 of Chen, Yu, Zeng and Flammia on qubits, with Hilbert space dimension . The same completely positive, trace-preserving noise channel acts after each ideal global Clifford gate; fixed computational-basis measurement noise is absorbed into . Calibration perfectly prepares . The full Clifford group modulo global phase is sampled uniformly and calibration shots are independent and identically distributed.
Let and . Define the Z-basis average fidelity by , and suppose . Set
The printed sample scale in Theorem 7 is . Interpret its real-valued batch parameters operationally as positive integers and , with actual calibration count .
For each recorded ideal Clifford and noisy outcome , compute . Let be the median of the means of batches of such scores. The estimated inverse sends an operator to . Let , where removes off-diagonal computational-basis entries, and let .
With probability at least over calibration records, and the subsequent single-shot retrieval expectation satisfies, simultaneously for every Hermitian observable and every density matrix ,
Here is the operator norm, and the expectation is conditional on the calibration result. This guarantee controls the systematic, asymptotic bias of robust shadow retrieval; it applies to all observables and states on the same successful calibration event.
Formalization Note The statement retains the printed factor. The source proof's substitution instead gives from the stated variance bound; this discrepancy and the integer rounding interpretation remain subject to independent source moderation. The product of rounded batch parameters is not asserted to equal, or be bounded above by the ceiling of, the printed total scale. The frozen calibration probability law, overlap scores, median and retrieval expectation compute the named protocol directly.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
A Grand Unification of Quantum Algorithms establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix a nonnegative integer , put , and choose real phases . There are complex polynomials , depending only on these phases and , with , , and respective parities and modulo , such that
For every finite quantum register, every pair of normalized pure states in that register, and every unitary with a real nonzero amplitude , define the available exact rank-one phase shifts and for real . Then
The product is written in increasing from left to right, and its rightmost acts first. Normalization and unitarity imply ; the endpoints are allowed. Parity means and .
This construction applies one uniform polynomial to a privileged transition amplitude and connects amplitude amplification with quantum signal processing.
Formalization Note The finite register is a Euclidean space over an arbitrary finite basis type. The frozen positive-sign rank-one phase shifts and sequence encode Eq. (13) exactly. The complementary polynomial is existentially quantified with before the register, states, unitary and amplitude. The zero polynomial is allowed as , including when .
Fix a nonnegative integer , put , and choose real phases . There are complex polynomials , depending only on these phases and , with , , and respective parities and modulo , such that
For every finite quantum register, every pair of normalized pure states in that register, and every unitary with a real nonzero amplitude , define the available exact rank-one phase shifts and for real . Then
The product is written in increasing from left to right, and its rightmost acts first. Normalization and unitarity imply ; the endpoints are allowed. Parity means and .
This construction applies one uniform polynomial to a privileged transition amplitude and connects amplitude amplification with quantum signal processing.
Formalization Note The finite register is a Euclidean space over an arbitrary finite basis type. The frozen positive-sign rank-one phase shifts and sequence encode Eq. (13) exactly. The complementary polynomial is existentially quantified with before the register, states, unitary and amplitude. The zero polynomial is allowed as , including when .
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Quantum Expander Codes establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix positive integer degrees and positive real constants , with . There are a deterministic classical decoder, a constant , and an integer , all chosen before the graph sizes and inputs, with the following properties.
Let be any finite simple bipartite graph with , left degree and right degree . For every with , require , where denotes its neighboring vertices. Require the corresponding right expansion for every with .
Form the self hypergraph-product CSS code on the tagged coordinates , of length . Write for the binary incidence matrix with rows and columns , and set , . Let and be their respective binary row spaces.
On every syndrome input, the decoder terminates and realizes the Section 3 small-set-flip algorithm, treating the two components independently. Each step flips a nonempty subset of an opposite generator's support, strictly reduces syndrome weight, and maximizes the decrease divided by the number of flipped coordinates. The deterministic implementation fixes its choices among the finitely many tied candidates. A zero syndrome returns the accumulated correction; a nonzero syndrome with no improving flip returns failure. Whenever , its total uniform-cost word-machine instruction count, together with the cost of loading its adjacency-list and syndrome input, is at most .
For every binary error pair on , let count coordinates on which at least one component is nonzero. If
then on the exact syndrome the decoder returns a correction satisfying
Correctness holds at every admissible finite size. This is an exact adversarial decoding guarantee for the associated quantum code, with linear classical runtime when degrees are fixed.
Formalization Note The positive-degree, nonempty-part convention used in the paper's proof is explicit. Equation (6)'s mixed coordinate names are read as the supports of the rows fixed by Equation (1) and the incidence formulas. These source clarifications are disclosed for independent moderation; the strict threshold and all constants in it are unchanged. Runtime and realization are conclusions about an executable classical machine; no progress or minimum-distance assertion is a hypothesis.
Fix positive integer degrees and positive real constants , with . There are a deterministic classical decoder, a constant , and an integer , all chosen before the graph sizes and inputs, with the following properties.
Let be any finite simple bipartite graph with , left degree and right degree . For every with , require , where denotes its neighboring vertices. Require the corresponding right expansion for every with .
Form the self hypergraph-product CSS code on the tagged coordinates , of length . Write for the binary incidence matrix with rows and columns , and set , . Let and be their respective binary row spaces.
On every syndrome input, the decoder terminates and realizes the Section 3 small-set-flip algorithm, treating the two components independently. Each step flips a nonempty subset of an opposite generator's support, strictly reduces syndrome weight, and maximizes the decrease divided by the number of flipped coordinates. The deterministic implementation fixes its choices among the finitely many tied candidates. A zero syndrome returns the accumulated correction; a nonzero syndrome with no improving flip returns failure. Whenever , its total uniform-cost word-machine instruction count, together with the cost of loading its adjacency-list and syndrome input, is at most .
For every binary error pair on , let count coordinates on which at least one component is nonzero. If
then on the exact syndrome the decoder returns a correction satisfying
Correctness holds at every admissible finite size. This is an exact adversarial decoding guarantee for the associated quantum code, with linear classical runtime when degrees are fixed.
Formalization Note The positive-degree, nonempty-part convention used in the paper's proof is explicit. Equation (6)'s mixed coordinate names are read as the supports of the rows fixed by Equation (1) and the incidence formulas. These source clarifications are disclosed for independent moderation; the strict threshold and all constants in it are unchanged. Runtime and realization are conclusions about an executable classical machine; no progress or minimum-distance assertion is a hypothesis.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Simulating Hamiltonian dynamics with a truncated Taylor series establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let , let be known coefficients, and let and . For any unitary matrices on a -dimensional system whose sum is Hermitian, count coherent signed controlled selection and its inverse as the access operations. Set , , and .
There are absolute constants , , and , chosen before all instance data, for which the following holds. Choose the least nonnegative truncation order satisfying . From alone one can construct the paper's segmented Taylor simulator, before choosing the term oracle or the input state. The simulator uses segments of duration and the remaining positive duration as its final segment. Each segment uses the Taylor LCU, the normalization ancilla, and robust oblivious amplification , with fresh zero ancillas that are subsequently discarded.
If is the standard isometric embedding of the -dimensional system into qubits, denotes the implemented unconditional channel, and is any unit vector, then
Every segment's truncated operator differs from its exact evolution by at most in spectral norm. The same construction also approximates the padded Hamiltonian on every normalized state of the full qubit register. The number of signed-selector calls is at most ; the number of other elementary gates is at most ; and peak ancillary qubits, treating the selector as the primitive access operation, are at most .
For and , the order and counted access cost satisfy
If a signed-selector implementation has elementary gates and clean workspace qubits, there are elementary segment circuits implementing the same simulator, returning that workspace to zero, with total gate count at most . In the special case in which the padded terms are tensor products of single-qubit Pauli matrices, such circuits exist with total gate count at most and peak ancillary qubits at most .
This gives the paper's time-independent simulation cost without requiring commuting, self-inverse, Hermitian individual terms or a bound on .
Formalization Note The paper does not name the reduced-state norm. Trace norm without the factor is used to make its discard-ancillas and error-accumulation argument precise. Eq. (10)'s failure coefficient, Eq. (16)'s partial trace of a ket, and the printed order-register amplitude are corrected as recorded in the audit. Arbitrary one- and two-qubit gates are used, with exact rotations and inverses; finite-gate-set synthesis overhead is outside the claim.
Let , let be known coefficients, and let and . For any unitary matrices on a -dimensional system whose sum is Hermitian, count coherent signed controlled selection and its inverse as the access operations. Set , , and .
There are absolute constants , , and , chosen before all instance data, for which the following holds. Choose the least nonnegative truncation order satisfying . From alone one can construct the paper's segmented Taylor simulator, before choosing the term oracle or the input state. The simulator uses segments of duration and the remaining positive duration as its final segment. Each segment uses the Taylor LCU, the normalization ancilla, and robust oblivious amplification , with fresh zero ancillas that are subsequently discarded.
If is the standard isometric embedding of the -dimensional system into qubits, denotes the implemented unconditional channel, and is any unit vector, then
Every segment's truncated operator differs from its exact evolution by at most in spectral norm. The same construction also approximates the padded Hamiltonian on every normalized state of the full qubit register. The number of signed-selector calls is at most ; the number of other elementary gates is at most ; and peak ancillary qubits, treating the selector as the primitive access operation, are at most .
For and , the order and counted access cost satisfy
If a signed-selector implementation has elementary gates and clean workspace qubits, there are elementary segment circuits implementing the same simulator, returning that workspace to zero, with total gate count at most . In the special case in which the padded terms are tensor products of single-qubit Pauli matrices, such circuits exist with total gate count at most and peak ancillary qubits at most .
This gives the paper's time-independent simulation cost without requiring commuting, self-inverse, Hermitian individual terms or a bound on .
Formalization Note The paper does not name the reduced-state norm. Trace norm without the factor is used to make its discard-ancillas and error-accumulation argument precise. Eq. (10)'s failure coefficient, Eq. (16)'s partial trace of a ket, and the printed order-register amplitude are corrected as recorded in the audit. Arbitrary one- and two-qubit gates are used, with exact rotations and inverses; finite-gate-set synthesis overhead is outside the claim.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Quantum algorithm for systems of linear equations with exponentially improved dependence on precision establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let , let be Hermitian and invertible with , and let be a supplied upper bound on its condition number. Let , and write and . The coherent preparation procedure prepares in polynomial time in on the -qubit state register; its inverse is available. Put , with .
There are absolute positive constants and fixed asymptotic thresholds, chosen before all public parameters and hidden inputs, with the following two conclusions.
The reduction outputs a success flag with probability at least . Conditional on success, its system output is the pure state whose vector representative is the normalized action of the actually simulated Fourier block on , and
This representative is fixed by the Fourier block; the error is not minimized over global phases. Failure output is unrestricted.
The sum counts the two matrix-oracle operations separately and then adds them. Short columns may be padded with zero entries, the location lists need not be sorted, and injectivity of each in-place location map is required. Entries use a public ordinary signed binary complex-number format. This is the exact-entry branch of the paper's access model; sufficiently accurate finite-precision access is covered through the simulator error budget. No controlled access to the input black boxes is assumed. External gates exclude internal implementations of and ; inlining either subroutine adds its per-call gate cost times its corresponding number of calls.
The bounds establish logarithmic dependence on output precision for quantum state preparation. The number of calls is bounded in the worst case using a finite capped amplification routine.
Formalization Note The Lean conclusion includes both clauses in one theorem and fixes the reduction and sparse circuits before quantifying over hidden inputs. The preparation-time polynomial and binary format are public parameters. Successful output is represented by a subnormalized pure density matrix together with its explicitly specified vector representative and direct vector error. Invalid qubit padding cannot count as successful output.
Correction to the printed source.
Printed: Page 8 says a worst-case amplification guarantee needs an 'upper bound on the probability q'; page 15 writes 'τ := y_J y_K'.
Corrected: Use a known positive lower bound on q for capped amplification, as Corollary 10 does, and read the maximum evolution time as y_J z_K.
Reason: The required amplification work grows when q decreases; Corollary 10 provides q bounded below using known coefficient mass. The Fourier times are y_j z_k in (18), (31), (52); y_K is not the defined z cutoff.
Let , let be Hermitian and invertible with , and let be a supplied upper bound on its condition number. Let , and write and . The coherent preparation procedure prepares in polynomial time in on the -qubit state register; its inverse is available. Put , with .
There are absolute positive constants and fixed asymptotic thresholds, chosen before all public parameters and hidden inputs, with the following two conclusions.
The reduction outputs a success flag with probability at least . Conditional on success, its system output is the pure state whose vector representative is the normalized action of the actually simulated Fourier block on , and
This representative is fixed by the Fourier block; the error is not minimized over global phases. Failure output is unrestricted.
The sum counts the two matrix-oracle operations separately and then adds them. Short columns may be padded with zero entries, the location lists need not be sorted, and injectivity of each in-place location map is required. Entries use a public ordinary signed binary complex-number format. This is the exact-entry branch of the paper's access model; sufficiently accurate finite-precision access is covered through the simulator error budget. No controlled access to the input black boxes is assumed. External gates exclude internal implementations of and ; inlining either subroutine adds its per-call gate cost times its corresponding number of calls.
The bounds establish logarithmic dependence on output precision for quantum state preparation. The number of calls is bounded in the worst case using a finite capped amplification routine.
Formalization Note The Lean conclusion includes both clauses in one theorem and fixes the reduction and sparse circuits before quantifying over hidden inputs. The preparation-time polynomial and binary format are public parameters. Successful output is represented by a subnormalized pure density matrix together with its explicitly specified vector representative and direct vector error. Invalid qubit padding cannot count as successful output.
Correction to the printed source.
Printed: Page 8 says a worst-case amplification guarantee needs an 'upper bound on the probability q'; page 15 writes 'τ := y_J y_K'.
Corrected: Use a known positive lower bound on q for capped amplification, as Corollary 10 does, and read the maximum evolution time as y_J z_K.
Reason: The required amplification work grows when q decreases; Corollary 10 provides q bounded below using known coefficient mass. The Fourier times are y_j z_k in (18), (31), (52); y_K is not the defined z cutoff.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.