Correlations decide a shallow-circuit advantage
Zijian Gong, Zhaobin Lyu, Jingjing Hu, Dengfeng Li, Shuoming An
quant-ph
Oct 3, 2026 · v1
TL;DR
Lean 4/Mathlib formalization of the analytic core: structural lemma, TV chain rule, per-fixing collapse theorem chains, residue-rigidity congruence, with zero sorry.
Abstract
Quantum computers are claimed to produce samples ordinary classical computers cannot reproduce. The sharpest such claim known pits constant-depth quantum circuits, given one entangled state per run, against shallow classical circuits of few-input gates and limited randomness. No efficient test was known that certifies such a claim from classical samples alone. Here we show that what such a test must read is decided by the classical class's pattern of single-bit and pair correlations, not by a distance. The test rests on one inequality: any machine producing the samples sits no further from the target than the fraction it mislabels plus the deviation of its string half, the bits beyond the label, from uniform. A collapse theorem, machine-checked in the Lean 4 proof assistant, confines that second term, one setting of the sampler's random input bits at a time. Four natural checks provably fail; a fifth, reading those same correlations, catches a far-from-target construction they cannot reach, and is exact on the class of few-input gates. The label test is proven and sample-optimal in its own tolerance up to a logarithmic factor; the fifth check is sound, not only effective, on the bounded pinned-residue class, pairwise-uniform samplers whose residue, the string's weight modulo the prime, is pinned by few seeds and whose seed sharing is bounded. What binds an experiment is the $43$-qubit entangled resource state at fidelity near $0.99$, not the readout. What remains are two named open problems; a positive answer to the first would extend the guarantee to the full class.
Problem
Constant-depth quantum circuits with GHZ advice can sample a target distribution (string plus majmod-XOR-parity tag) that shallow classical NC0 samplers cannot. No efficient test was known that certifies such a sampling-advantage claim from classical samples alone.
Approach
A TV chain rule bounds a sampler's distance to the target by its mislabel rate plus the deviation of its string marginal from uniform. This yields a dichotomy verifier: a label test plus a five-door structure test. A per-fixing collapse theorem, obtained via Turán-based seed fixing and character sums, confines the residual case. The structural lemma, chain rule, collapse chains and supporting identities are machine-checked in Lean 4 against Mathlib, using only the standard axioms.
Results
The label test is sample-optimal in its tolerance up to a log factor. The fifth, correlation-reading door is sound on the bounded pinned-residue class and catches constructions that four natural checks miss. Full soundness reduces to two stated open problems, which are deliberately left unformalized.