For the 15 two-qubit Pauli observables, any classical Mealy machine reproducing the quantum predictions (Ia) repeatability and (II) context product rules requires exactly log2(5) ≈ 2.32 bits of memory. Upper bound: an explicit five-state machine, verified including the intervening-measurement form of (Ia). Lower bound: machine-certified unsatisfiability at four states (three independent encodings × three SAT solvers; DRUP proof checked by drat-trim; byte-reproducible formula; preregistrations externally timestamped before computation). This closes the gap [log2 4, log2 6] left open in arXiv:2506.06869. A verified note documents 338 pairwise-inequivalent optimal machines collapsing to 19 output-atlas orbits under the target-preserving affine symmetry group of order 23,040. Verification: unzip the deposit, run python3 verifier3.py (537 assertions, ~30 s, stdlib only), then drat-trim E2_n4.cnf E2_n4_unsat_glucose.drup (prints s VERIFIED).
For the 15 two-qubit Pauli observables, any classical Mealy machine reproducing the quantum predictions (Ia) repeatability and (II) context product rules requires exactly log2(5) ≈ 2.32 bits of memory. Upper bound: an explicit five-state machine, verified including the intervening-measurement form of (Ia). Lower bound: machine-certified unsatisfiability at four states (three independent encodings × three SAT solvers; DRUP proof checked by drat-trim; byte-reproducible formula; preregistrations externally timestamped before computation). This closes the gap [log2 4, log2 6] left open in arXiv:2506.06869. A verified note documents 338 pairwise-inequivalent optimal machines collapsing to 19 output-atlas orbits under the target-preserving affine symmetry group of order 23,040. Verification: unzip the deposit, run python3 verifier3.py (537 assertions, ~30 s, stdlib only), then drat-trim E2_n4.cnf E2_n4_unsat_glucose.drup (prints s VERIFIED).
Classically simulating the quantum contextual correlations produced by sequences of ideal measurements of compatible observables requires the measured system to have an internal memory. Computing the minimum amount of memory needed is, in general, challenging. Here, building upon the work of Kleinmann et al. [New J. Phys. 13, 113011 (2011)], we prove that the memory cost for simulating the contextuality produced by the 10 three-qubit observables of Mermin's pentagram is only log2(5)≈2.32 bits, but the memory cost for simulating the contextuality produced by all 15 two-qubit Pauli observables is, at least, log2(6)≈2.58 bits, thus exceeding the classical capacity of the system on which the measurements are performed. We also add results on the memory for simulating some subsets of quantum predictions.
How much memory does it take to apply the same quantum channel many times, when each output must be released before the next input arrives and every retained qubit counts? One-use invariants do not decide it. Two explicit channels on dimension 1664 have identical normalized Choi spectra (32 eigenvalues 1/32), the same maximal complementary entropy 5, and zero asymptotic purity cost. At the same optimal exchange rate, one is implemented exactly with five memory qubits for any number of uses, while the other needs Omega(n^(1/(2 log_2(107)+2))) memory qubits for n uses, at every fixed error at most 1/16 and whatever purity is available; memory O(n^(1/3) log^(4/3) n) suffices for it. The hard channel is built from Houghton's group H_3. Behind the example is a general theory: the achievable exchange and purity rates, the purity cost kappa, which vanishes exactly on the closure of finite tracial factorizations, and memory bounds from how well a channel's environment is approximated by finite ones, and, for channels built from finite presentations, from the approximation profile of the group. Version 1.1 adds where the expensive channels lie: on the relative boundary of the closure; any fixed depolarizing admixture brings them down to polylogarithmic memory at the rank rate; on a face containing the Houghton channel a single moment of a trace on the group decides expense; and one free fermion per site already forces polynomial memory. Version 1.1.1 adds a map of what the main separation depends on (published inputs, companion results and new arguments), sets finite-budget and asymptotic-rate statements side by side, cites the companion papers at their published versions, pins the tested software versions, and makes every check refuse to run under optimized Python. The mathematical results are unchanged. Version 1.1.2 corrects attributions and makes two headline statements precise. The separation of Theorem A is stated at the exchange budget 5n/2, and the channels that need polynomial memory at every exchange rate are those with purity limited to O(log n). Credits added or corrected: Bisio, D'Ariano, Perinotti and Chiribella, and Bisio, D'Ariano, Perinotti and Sedlak; Boes et al. for the square-root dephasing construction; Lie, Son, Boes, Ng and Wilming for the exact case of the tracialization lemma; Faist, Berta and Brandao for the relation to the thermodynamic capacity; Haagerup, Musat and Rordam for the moment criteria; Thoma, Johnson, Watrous, Horodecki-Oppenheim-Winter and Lie-Jeong; Cornulier for the Baumslag-Solitar bound. Known results are moved out of numbered statements. The mathematical results and the numbering are unchanged. All operational bounds use complete-experiment error against adaptive observers with quantum references. The general rate-region achievability result uses a cited closed-device theorem; the explicit separation does not. This preprint archive includes the PDF, TeX source, finite verification scripts, and scoped Lean arithmetic proofs. The artifacts do not formally verify the entire manuscript; their scope and external dependencies are documented in verification/README.md.
Quantum estimates of molecular energy require repeated state preparation and measurement. We bound the minimum repetition count for given measurements and processing rules from above with a practical schedule and from below with independently verified inequalities. For an H4 chain at H-H distances of 0.90 and 1.80 Åwith 2 per cent uniform noise in the ground state, entangling Clifford measurements, which map Pauli products onto one another, cut leading-order repetitions by at least 65.9 and 61.0 per cent, respectively, relative to any schedule using only single-qubit Pauli measurements and Hamiltonian terms. With 69 unaltered measurement settings, each a basis change followed by qubit readout, processing further observables saves at least 12.04 and 6.70 per cent. For four lanthanide and actinide Hamiltonians with depolarized Hartree-Fock covariances, reducing the sum of absolute Hamiltonian coefficients does not proportionally reduce sampling. The bounds cover linear unbiased estimates from independent batches at small error.
Preprint v0.3, not peer reviewed; the proofs were written with AI assistance and are AI-refereed (same model family), not formally verified. For n-qubit Pauli observables closed under products of commuting pairs we prove the operator identity A^2 = NI + 2K - 4V. For W(2n-1,2) and both quadric types, the spectral lower bound on the contextuality degree is attained exactly when some assignment is violation-regular with a simple (Kramers-simple) top eigenvalue; for n >= 2 this happens exactly for W(5,2), Q+(7,2), Q-(3,2) and Q-(5,2) (three by exact computation). For the four-qubit elliptic quadric, a hyperplane completion violates 378 - <sigma, h(X)> outside lines, h(X) being read off a Gram operator. With computer assistance, an odd count forces Gram rank 8, and Gram rank 2 forces counts divisible by 4. That every completion minimum is a multiple of 4 is false (computer-certified counterexamples, not proof-checked). Data are committed by SHA-256.
We show that the algorithmic complexity of any classical algorithm written in a Turing-complete programming language polynomially bounds the number of quantum bits that are required to run and even symbolically execute the algorithm on a quantum computer. In particular, we show that any classical algorithm A that runs in O(f(n)) time and O(g(n)) space requires no more than O(f(n)⋅g(n)) quantum bits to execute, even symbolically, on a quantum computer. With O(1)≤O(g(n))≤O(f(n)) for all n, the quantum bits required to execute A may therefore not exceed O(f(n)2) and may come down to O(f(n)) if memory consumption by A is bounded by a constant. Our construction works by encoding symbolic execution of machine code in a finite state machine over the satisfiability-modulo-theory (SMT) of bitvectors, for modeling CPU registers, and arrays of bitvectors, for modeling main memory. The FSM is linear in the size of the code, independent of execution time and space, and represents the reachable machine states for any given input. The FSM may be explored by bounded model checkers using SMT and SAT solvers as backend. However, for the purpose of this paper, we focus on quantum computing by unrolling and bit-blasting the FSM into (1)~satisfiability-preserving quadratic unconstrained binary optimization (QUBO) models targeting adiabatic forms of quantum computing such as quantum annealing, and (2)~semantics-preserving quantum circuits (QCs) targeting gate-model quantum computers. With our compact QUBOs, real quantum annealers can now execute simple but real code even symbolically, yet only with potential but no guarantee for exponential speedup, and with our QCs as oracles, Grover's algorithm applies to symbolic execution of arbitrary code, guaranteeing at least in theory a quadratic speedup.
The noise threshold below which the qubit depolarizing channel retains positive quantum capacity has been studied since 1996. The classic constructions come with exact finite formulae, but in every reported threshold to date -- most recently the record of Agarwal et al. -- the final step, the sign of the coherent information at the reported point, is a floating-point evaluation. We give the first exact-arithmetic, independently machine-checkable positivity proofs in this regime: an explicit 45-copy rank-two input state A, published as a 1,472-byte witness, with certified Ic>0 at the exact rational p=16239/250000=0.064956 (per-Pauli convention; total error rate 3p=0.194868) -- beyond both the best value printed in the Agarwal et al. paper (0.064657) and the strongest state in the same authors' public repository (≈0.064911), both numerical. Because the depolarizing family is a semigroup under composition, fixed-input coherent information is nonincreasing in p on [0,1/4], so a single certified point extends to the entire interval below it. The same machinery confines the positivity boundaries of A and of the strongest public state of Agarwal et al. to disjoint rational intervals separated by more than 1/25000 -- to our knowledge the first proven ordering of the positivity boundaries of two explicit competing code states. Every computational claim in the paper reduces to a finite list of big-integer comparisons, checkable by a dependency-free few-hundred-line verifier whose soundness rests on three self-contained half-page lemmas. Payloads, certificates, and verifier accompany the paper as a supplementary artifact.