Theoretical Computer Science

Motivation

The maximum weight matching (MWM) problem asks, for a graph with edge weights, for a set of vertex-disjoint edges of largest total weight. It is a central problem of combinatorial optimization, with applications to transportation, assignment and scheduling, and as a subroutine for shortest paths, planar max cut, Chinese postman tours and metric TSP. Edmonds' blossom algorithm (1965) solves it on general graphs; the fastest implementation, due to Gabow, runs in $O(mn+n^2\log n)$ time, and the scaling algorithm of Gabow and Tarjan (1991) runs in $O(m\sqrt{n\log n}\,\log(nN))$ time on graphs with $n$ vertices, $m$ edges and integer weights of magnitude at most $N$. Applications such as switch scheduling, graph clustering and sparse linear solvers accept a slightly suboptimal matching in exchange for speed. This motivates $(1-\epsilon)$-approximate maximum weight matchings: matchings whose weight is at least a $1-\epsilon$ fraction of the optimum.

Timeline of linear and near-linear time approximation for general graphs (Section 1.3 and Table IV of the paper; the entries below are as the paper attributes them):

• Folklore: the greedy algorithm, which repeatedly takes the heaviest remaining edge, gives a $\tfrac12$-MWM in $O(m\log n)$ time.
• Preis (STACS 1999): a $\tfrac12$-MWM in linear time; Drake and Hougardy (2003) gave a simpler one.
• Drake and Hougardy (2003; journal version Vinkemeier and Hougardy, ACM Trans. Algorithms 2005): a $(\tfrac23-\epsilon)$-MWM in $O(m\epsilon^{-1})$ time; Pettie and Sanders (2004) improved this to $O(m\log\epsilon^{-1})$.
• Duan and Pettie (FOCS 2010) and Hanke and Hougardy (2010): a $(\tfrac34-\epsilon)$-MWM in $O(m\log n\log\epsilon^{-1})$ time.
• Duan and Pettie (2014): a $(1-\epsilon)$-MWM in $O(m\epsilon^{-1}\log\epsilon^{-1})$ time, which is linear for every fixed $\epsilon$.

Setting

Let $G=(V,E)$ be a finite simple graph with integer weights $w:E\to\{1,\dots,N\}$, $N=2^L$. A matching $M$ is a set of vertex-disjoint edges, with weight $w(M)=\sum_{e\in M}w(e)$; a vertex is free if no edge of $M$ touches it. $M$ is a $c$-MWM if $c\cdot w(M')\le w(M)$ for every matching $M'$.

A blossom is built recursively: a single vertex $\{v\}$ is a trivial blossom with $E_{\{v\}}=\emptyset$; an odd number $\ge3$ of disjoint blossoms $A_0,\dots,A_\ell$ joined in a cycle by edges $e_i\in A_i\times A_{i+1}$ form the blossom $B=\bigcup A_i$ with edge set $E_B=\bigcup E_{A_i}\cup\{e_0,\dots,e_\ell\}$. It is full if $|M\cap E_B|=(|B|-1)/2$. The algorithm keeps a laminar set $\Omega$ of full blossoms; a root blossom is a maximal one, and $G/\Omega$ contracts each root blossom to a single vertex.

Dual values $y:V\to\mathbb R$ and $z$ on odd vertex sets give each edge the value

$$yz(u,v)=y(u)+y(v)+\sum_{B\ \text{odd},\ u,v\in B} z(B).$$

The scaling algorithm (Figure 2 of the paper) has parameters $N$ and $\epsilon'=2^{-g}\le\tfrac14$. It runs scales $i=0,\dots,L$ with granularity $\delta_i=\epsilon'N/2^i$ and truncated weights $w_i(e)=\delta_i\lfloor w(e)/\delta_i\rfloor$. Each scale repeats four steps: augment along a maximal set of vertex-disjoint augmenting paths of the eligible graph $G_{\mathrm{elig}}$, shrink a maximal set of new blossoms, adjust the duals by $\pm\delta_i/2$, and dissolve root blossoms whose $z$-value has reached zero. It stops when the free vertices' $y$-values reach a scale-dependent value, which is $0$ at scale $L$. Eligibility is given by Definition 3.2; the linear-time variant keeps the algorithm unchanged and uses Definition 3.10, which additionally ignores an edge $e$ in scales $i>\mathrm{scale}(e)+\log\epsilon'^{-1}$ unless it is a blossom edge.

Formalization targets

Goal: Theorem 3.12, approximation half

For every $\epsilon$ with $\epsilon'\le\epsilon/7$, the algorithm of Figure 2 with Definition 3.10 eligibility has a terminating run, and every terminating run returns a matching $M$ with

$$w(M)\ \ge\ (1-\epsilon)\,w(M')\qquad\text{for every matching } M' \text{ of } G .$$

Milestones, in attack order

• Lemma 2.3: approximate complementary slackness ($yz(e)\ge(1-\epsilon_0)w(e)$ everywhere, $yz(e)\le(1+\epsilon_1)w(e)$ on matched and blossom edges, zero free duals) gives a $(1+\epsilon_1)^{-1}(1-\epsilon_0)$-MWM.
• Section 2 rescaling: rounding real weights to $\lfloor w/\gamma_r\rfloor$, $\gamma_r=\epsilon w_{\max}/n$, loses at most a factor $1-\epsilon/2$.
• Lemma 3.5: with Definition 3.2 the algorithm preserves Property 3.1, which consists of granularity, active blossoms, near domination $yz(e)\ge w_i(e)-\delta_i$, near tightness $yz(e)\le w_i(e)+2(\delta_j-\delta_i)$ for type-$j$ edges, and equal free duals.
• Lemma 3.6: eligible edges searched up to scale $i$ weigh at least $N/2^{i+1}+\delta_i$, and matched edges satisfy $yz(e)\le(1+4\epsilon')w(e)$.
• Lemma 3.7: the output under Definition 3.2 is a $(1-5\epsilon')$-MWM.
• Theorem 3.8: the approximation half of Theorem 3.8, with $\epsilon'\le\epsilon/5$.
• Lemma 3.11: the invariants under Definition 3.10, including $yz(e)>(1-\epsilon')w_i(e)$ and $yz(e)<(1+6\epsilon')w_i(e)$ once $i>\mathrm{scale}(e)+\gamma$.

Significance

The result. Theorem 3.12 gives the first algorithm for $(1-\epsilon)$-approximate maximum weight matching on general graphs that runs in linear time for every fixed $\epsilon$; earlier linear-time algorithms achieved only $\tfrac12$ or $\tfrac23-\epsilon$. Its analysis is a relaxation of Edmonds' complementary slackness conditions that grows weaker over the scales, but not uniformly, and Lemma 2.3 certifies an approximate matching by approximately feasible duals.

Formalizing it. The result is proved in the paper. Mathlib (at the pinned revision) has matchings, alternating walks and Tutte's theorem, but no blossoms, contracted graphs or weighted matching algorithms. A complete development gives a Lean model of blossoms, contraction and augmenting paths through blossoms, a verified primal–dual invariant for a scaling algorithm, and a checked approximate-slackness certificate for matchings. Each of these can be reused to formalize Edmonds' exact algorithm or the Gabow–Tarjan scaling algorithm.

Difficulty

The two halves of the argument pull against each other. Lemma 2.3 needs near domination and near tightness as multiplicative bounds. The algorithm maintains only additive bounds whose slack for an edge of type $j$ is $2(\delta_j-\delta_i)$, and this slack does not shrink as the scales advance. Converting it into a factor $1+O(\epsilon')$ requires a lower bound on the weight of every edge that ever became eligible, which in turn depends on the free vertices' duals following an exact schedule across scales.

For Definition 3.10 the obvious argument breaks down: an edge that is ignored after scale $\mathrm{scale}(e)+\gamma$ may violate near domination and near tightness by an amount that grows with every later dual adjustment. The claim is that the accumulated violation stays within an $O(\epsilon')$ fraction of $w_i(e)$, and establishing this requires tracking every adjustment that can reach an ignored edge.

On the combinatorial side, the Augmentation and Blossom Shrinking steps work in the contracted graph $G/\Omega$. Their correctness uses the classical facts that augmenting paths lift through full blossoms and that blossoms stay full after augmentation (Lemma 2.1), which have to be formalized from scratch.

Formalization scope

Graphs are SimpleGraph V on a Fintype V with decidable equality; edges are Sym2 V; matchings are Finset (Sym2 V) with pairwise vertex-disjoint edges of $G$; weights are $w:\mathrm{Sym2}\,V\to\mathbb N$ with $1\le w(e)\le 2^L$ on edges. Duals, $\delta_i$ and $w_i$ are real numbers. $z$ is a function on all finite vertex sets and $yz$ sums it over the odd sets that contain the edge, as on the page. $N=2^L$ and $\epsilon'=2^{-g}$, $g\ge2$, are given through their exponents. $\mathrm{scale}(e)$ uses the convention $\mu_{-1}=+\infty$. The paper's standing assumption $N\le n^2$ is used only for running time and is omitted.

The algorithm is a nondeterministic relation. A state holds $M$, $\Omega$ with its blossom edge sets, $y$, $z$, a ghost record of the scale in which each edge last entered $M\cup\bigcup_{B\in\Omega}E_B$, and the common free-vertex dual that drives the loop test. The maximal sets of augmenting paths and of new blossoms and the lifts of paths through blossoms are choices. Invariants are stated for states reachable by a run, and the goal asserts both that a terminating run exists and that every terminating run returns a $(1-\epsilon)$-MWM.

The running times $O(m\epsilon^{-1}\log N)$ of Theorem 3.8 and $O(m\epsilon^{-1}\log\epsilon^{-1})$ of Theorem 3.12 are not formalized: the paper fixes no cost model, and its bounds rely on a modified depth-first search and on word-RAM table lookups. The explicit constants $\epsilon'\le\epsilon/5$ (Theorem 3.8) and $\epsilon'\le\epsilon/7$ (Theorem 3.12) are the ones the proofs supply.

The following trivializing formalizations are ruled out: a "matching" that may contain non-edges or repeated edges; a goal about a state only assumed to satisfy Property 3.1 rather than reached by the algorithm; a run relation with no terminating run, which the existence conjunct excludes; eligibility or blossoms chosen freely instead of by the page's rules; and comparison only against matchings of the contracted graph instead of all matchings of $G$.

Welcome contributions include a Lean treatment of blossoms and their contraction (Lemma 2.1, which is not a milestone here), the lift of augmenting paths, Lemmas 3.3 and 3.4 as auxiliary results, and proofs of the milestones in the order listed.

Selected references

• R. Duan and S. Pettie, Linear-Time Approximation for Maximum Weight Matching, Journal of the ACM 61(1), Article 1, 2014. https://doi.org/10.1145/2529989
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B, 125–130, 1965. https://doi.org/10.6028/jres.069B.013
• H. N. Gabow and R. E. Tarjan, Faster scaling algorithms for general graph-matching problems, Journal of the ACM 38(4), 815–853, 1991. https://doi.org/10.1145/115234.115366
• R. Preis, Linear time 1/2-approximation algorithm for maximum weighted matching in general graphs, STACS 1999, LNCS 1563, 259–269 (cited from the bibliography of Duan and Pettie 2014).
• D. E. D. Vinkemeier and S. Hougardy, A linear-time approximation algorithm for weighted matchings in graphs, ACM Transactions on Algorithms 1(1), 107–122, 2005 (cited from the bibliography of Duan and Pettie 2014).
• S. Pettie and P. Sanders, A simpler linear time 2/3 − ϵ approximation to maximum weight matching, Information Processing Letters 91(6), 271–276, 2004 (cited from the bibliography of Duan and Pettie 2014).

Motivation

A sorting network is a sorting procedure whose sequence of comparisons is fixed in advance, independently of the data. Its depth, the number of rounds of simultaneous comparisons on disjoint pairs, is the parallel running time. Sorting networks are used in parallel and hardware sorting, in switching networks, and in cryptography, where a data-independent (oblivious) sequence of operations is required. How small the depth can be as a function of the number of inputs $n$ is a basic question of parallel computation.

Timeline:

• 1968. Batcher's odd-even merge sort and bitonic sort give networks of depth $O((\log n)^2)$ and size $O(n(\log n)^2)$ (K. E. Batcher, Sorting networks and their applications, AFIPS Spring Joint Computer Conference, 1968). For $n$ a power of two they remain the best explicit networks in practice.
• 1973. Knuth's The Art of Computer Programming, Vol. 3, §5.3.4, surveys sorting networks. A simple counting argument gives the lower bound: every sorting network has depth at least $\log_2 n$, since each output depends on at most $2^{\text{depth}}$ inputs.
• 1983. Ajtai, Komlós and Szemerédi construct networks of depth $O(\log n)$ and size $O(n\log n)$ (Combinatorica 3 (1983) 1–19, doi:10.1007/BF02579338), matching the lower bound up to a constant. The constant is not computed in the paper and is known to be very large.
• 1990. Paterson simplifies the construction and gives the first explicit, still very large, depth constant (M. S. Paterson, Improved sorting networks with O(log N) depth, Algorithmica 5 (1990) 75–92, doi:10.1007/BF01840378).
• 2014. Goodrich gives Zig-zag sort, a simpler deterministic data-oblivious sorting algorithm with $O(n\log n)$ comparisons that avoids the AKS machinery but is not of logarithmic depth (arXiv:1403.2777).

Setting

There are $n$ registers $R_1,\dots,R_n$ holding elements of a linearly ordered set. An elementary step (a comparator) $(i,j)$ with $i\neq j$ compares the contents of $R_i$ and $R_j$ and exchanges them if the content of $R_i$ is larger. Afterwards $R_i$ holds the minimum and $R_j$ the maximum of the two, and every other register is unchanged. A parallel step is a set of comparators in which no register occurs twice, so it has at most $n/2$ comparators. A comparator network $N$ is a finite sequence of parallel steps, fixed before the input is seen. Its depth $\operatorname{depth}(N)$ is the number of parallel steps and its size $\operatorname{size}(N)$ the total number of comparators. $N$ sorts if for every input $x=(x_1,\dots,x_n)$ the output $N(x)$ satisfies $N(x)_1\le\cdots\le N(x)_n$.

The construction runs on the tree $T$ of finite $0$-$1$ sequences, whose levels are ordered lexicographically. A chain on level $i$ assigns to every node of that level a set of registers, with the sets pairwise disjoint and of a common size $N(C)$. A ⟨k, ε⟩ expander on ⟨A, B⟩, for disjoint register sets $A$ and $B$, is a bipartite graph between $A$ and $B$ of maximum degree $k$ in which every nonempty $X\subseteq A$ has more than $(1-\varepsilon)\varepsilon^{-1}\min\{|X|,\varepsilon|B|\}$ neighbours, and symmetrically for $B$. The Lean development uses the names ComparatorNetwork, compareExchange, IsChain, chainN, IsExpander, IsLowerSection for these objects.

Formalization targets

Goal: the AKS theorem (Abstract and §1, p. 1)

$$\exists\, c>0\ \ \forall n\ge 2\ \ \exists N:\quad N \text{ sorts},\qquad \operatorname{depth}(N)\le c\log_2 n,\qquad \operatorname{size}(N)\le c\,n\log_2 n .$$

The constant is absolute and is not fixed. Any explicit value would be invalidated by the next improvement, and the paper gives none.

Milestones (the paper's numbered lemmas that hold as stated)

• Lemma 3 (p. 6): for $0<\varepsilon<1$ and $c\ge1$ there is $k(\varepsilon,c)$ such that every pair of disjoint sets with $1/c\le|A|/|B|\le c$ carries a $\langle k,\varepsilon\rangle$ expander.
• Lemma 4 (p. 7): performing every comparator of such an expander once, in any order, from $A$ to $B$ leaves all but an $\varepsilon$-fraction of any lower section $S$ with $|S|\le|A|$ in $A$, and symmetrically for upper sections in $B$:

$$|S\setminus\mathrm{Cont}(A)|\le\varepsilon|S| .$$

• Lemma 1 (pp. 3–4): the splitting $V(C,k)$ of a chain, which moves one register of each leaf set up the tree, produces chains with properties (1.1)–(1.5).
• Lemma 2 (p. 4): chains $W(C,k)$ with $a_k-1\le N(W(C,k))\le a_k$ exist under conditions (2a), (2.b).
• Lemma 12(a) (p. 14): a violation of the order relation $R^\beta_G$ between two nodes of a level is witnessed by two consecutive nodes.

Significance

The result. The AKS theorem settles the asymptotic depth of sorting networks at $\Theta(\log n)$ and their size at $\Theta(n\log n)$. It gives an $O(\log n)$-time sorting algorithm with $n$ processors that performs only data-independent comparisons. It is the standard reference point for oblivious sorting in parallel algorithms, circuit complexity (sorting is in $\mathsf{NC}^1$ via comparators) and oblivious RAM constructions. Lemma 4, the ε-halver property of expander comparisons, is the component that later constructions (Paterson) reuse.

Formalizing it. The theorem has been proved since 1983. No Lean proof of the AKS theorem is known. Mathlib has no expander graphs in the ⟨k, ε⟩ sense and no sorting networks. The mission asks for a formal proof of the headline theorem by any route (the AKS construction or Paterson's variant), and for formal proofs of the paper's verified lemmas as reusable components. The expander lemma needs either an explicit family (Margulis; Gabber–Galil) or a probabilistic existence argument, both substantial on their own.

Difficulty

Every elementary argument stalls at depth $O((\log n)^2)$: recursive merging needs $\log n$ merge rounds, and merging two sorted lists by a comparator network needs depth $\Omega(\log n)$. A depth of $O(\log n)$ therefore cannot come from exact merging. It must come from constant-depth approximate operations (ε-halvers, which require bounded-degree expanders) combined with a mechanism that corrects the errors they leave. In the paper this mechanism is a movement of registers up and down a binary tree, controlled by a family of constants chosen in a fixed order ("$\varepsilon_1\ll q_2\ll1-g\ll q_1\ll 1/c_1\ll1$", p. 2). The accounting that shows the misplaced elements decay geometrically is the hard part. Several intermediate lemmas of the paper are false as printed, so the paper's text is not a checklist to transcribe.

Formalization scope

Conventions committed to in Lean:

• Registers are Fin n, and contents lie in an arbitrary linearly ordered type. A network is a List of layers, each a List (Fin n × Fin n) of comparators with distinct endpoints, and no register occurs twice in a layer. A comparator $(i,j)$ puts the minimum into $i$, and both directions $i<j$ and $i>j$ are allowed. Sorts means the output is monotone for every linearly ordered type and every input, not only for permutations.
• $\log_2 n$ is Real.logb 2 n, and the goal is stated for $n\ge2$. The constant $c$ is quantified before $n$.
• Tree levels are Fin (2^i), with numeric order equal to lexicographic order. A chain is a Fin (2^i) → Finset R.
• Definition 2.2 of the paper, read literally, requires $|\Gamma_\emptyset|>0$, which fails, so no graph would be an expander. The expansion inequalities are imposed on nonempty sets only, and the strict inequality is kept.

Trivializing formalizations are ruled out. The goal is not "for every $n$ there is a network of depth $O(\log n)$" with the constant chosen after $n$, which is true for trivial reasons. Layers without the disjointness condition would let a single layer contain a whole insertion sort. A bound on the number of comparisons alone, with unbounded depth, is a different and much older result; the goal states both the depth and the size bound.

The mission states the AKS theorem and the paper's lemmas that are correct as stated. It does not formalize the AKS algorithm itself ($S^\alpha$, $P^\alpha$, the operations CH1–CH4, IMP) or its intermediate Lemmas 5–11 and 13–15. Those depend on unspecified constants constrained only by "sufficiently small" chains, and Lemmas 5, 10 and 12(b) are false as printed. A solver may of course define the algorithm, with pinned constants, as part of a proof.

Contributions welcome: a library of comparator networks (composition, the 0-1 principle, depth of Batcher's networks), existence of bounded-degree bipartite expanders, the ε-halver lemma, and any complete proof of the goal. The network and expander definitions are independent of this paper and reusable.

Selected references

• M. Ajtai, J. Komlós, E. Szemerédi, Sorting in c log n parallel steps, Combinatorica 3(1) (1983) 1–19. doi:10.1007/BF02579338
• K. E. Batcher, Sorting networks and their applications, Proc. AFIPS Spring Joint Computer Conference 32 (1968) 307–314. doi:10.1145/1468075.1468121
• D. E. Knuth, The Art of Computer Programming, Vol. 3: Sorting and Searching, Addison-Wesley, 1973, §5.3.4.
• G. A. Margulis, Explicit constructions of concentrators, Problems of Information Transmission 9 (1973) 325–332.
• O. Gabber, Z. Galil, Explicit constructions of linear-sized superconcentrators, J. Computer and System Sciences 22(3) (1981) 407–420. doi:10.1016/0022-0000(81)90040-4
• M. S. Paterson, Improved sorting networks with O(log N) depth, Algorithmica 5 (1990) 75–92. doi:10.1007/BF01840378
• M. T. Goodrich, Zig-zag sort: a simple deterministic data-oblivious sorting algorithm running in O(n log n) time, STOC 2014. arXiv:1403.2777

Motivation

A graph records pairs of objects that cannot be chosen together. An independent set is a choice with no conflicting pair. When each vertex has a nonnegative weight, maximum weighted independent set asks for a conflict-free set with the greatest total weight. This model occurs when choices have values and pairwise incompatibilities. On general graphs the optimization problem is difficult; the planar restriction gives a concrete geometric promise under which approximation is possible. Williamson and Shmoys state a polynomial-time approximation scheme for planar maximum independent set as Theorem 10.11 of The Design of Approximation Algorithms, in the author electronic manuscript at PDF/manuscript page 271.

Setting

The instance has vertices labeled by Fin n, an adjacency table edge : Fin n → Fin n → Bool, and a real weight weight i for each vertex. SimpleGraph.fromRel turns the table into an undirected simple graph G. The theorem requires every weight to be nonnegative. A finite set S is feasible when G.IsIndepSet (S : Set (Fin n)) holds. Its value is ∑ i ∈ S, weight i.

Planarity is expressed by HasPlanarDrawing G: vertices are placed at distinct points of the real plane, and every edge is represented by a continuous simple arc. An arc has no vertex in its interior, and distinct edges can meet only at endpoints. This is a concrete local drawing convention for the planar graph promise. The drawing witnesses the hypothesis; it is not passed as part of the algorithm's input.

The computational model is a fixed finite unit-cost RAM program. Its input includes the vertex count, an integer accuracy parameter, a complete adjacency table, and the real weights in named memory cells. Its instructions include natural-number and real addition and subtraction, exact comparisons, random-access loads and stores, branches, jumps, and halt. The machine starts with the instance preloaded and produces a bitmap after the adjacency table. This precise instruction set is a formalization convention: the book states an arithmetic-operation running time but does not specify a machine language.

Formalization targets

For every real $\varepsilon>0$, let $k=\max(1,\lceil1/\varepsilon\rceil)$. The goal asserts that a single finite program and fixed positive natural constants $C,d$ work for every planar instance and every vector of nonnegative real weights. The program must halt after a number $t$ of operations satisfying

$$t+1\le C\,2^{dk}(n+1)^2.$$

Its bitmap must represent an independent set $A$, and for every independent set $S$,

$$(1-\varepsilon)\sum_{i\in S}w_i\le\sum_{i\in A}w_i.$$

Comparison with every feasible $S$ includes an optimal solution. The same program and constants precede all accuracy and instance quantifiers. The $(n+1)^2$ form includes the empty graph without imposing zero running time. The result corresponds to the $O(2^{O(1/\varepsilon)}n^2)$ bound in Theorem 10.11; the formal statement makes the constants and accuracy parameter explicit.

Significance

The result supplies an accuracy-time tradeoff for planar weighted independent set: any fixed positive accuracy has a quadratic dependence on graph size in this operation model, while the accuracy dependence is exponential. It separates the planar setting from the general graph problem. The finite instruction set and input layout make the computational claim inspectable, including what information the program receives and what counts as an operation.

The cited result is known in the textbook. This mission asks for a Lean proof of the packaged statement; the theorem currently has sorry, and no machine construction or correctness proof is claimed. The original local statement was compiled and source reviewed before packaging. That prior result establishes statement validity in its source workspace, while the upload payload is checked separately.

Difficulty

A high-quality independent set in each planar region does not immediately give a high-quality global set: edges across regions can create conflicts, and discarding boundary vertices can lose weight. A proof must coordinate the approximation inequality with a uniform operation bound for one program across all graph sizes, accuracies, and real weight vectors. It must also show the computed bitmap is always independent and that execution reaches an explicit halt instruction within the bound. These requirements rule out treating an optimizer, an embedding, or a best solution as preloaded input.

Formalization scope

The goal uses finite labeled graphs, nonnegative arbitrary real weights, exact real arithmetic, and the concrete drawing predicate above. It does not claim a bit-complexity bound for encoded reals. The RAM starts from a complete adjacency table and weight vector, with no supplied drawing or optimum. Its step function is deterministic; an invalid program counter is stuck, so the theorem explicitly requires a halt instruction. Outputs are bits in designated natural memory cells and are checked for validity before their weighted value is compared.

The packaged definitions are the drawing predicate, instruction type, state, transition, iteration, input layout, and output decoder. They contain no proof axioms or optimization oracle. The rational-input polynomial bit-time fragment in the source workspace is a separate statement and is outside this goal. A complete contribution would construct the finite program and prove its running time and approximation guarantee in the specified model.

Selected references

• David P. Williamson and David B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011, author electronic manuscript, Theorem 10.11, PDF/manuscript p. 271; weighted independent-set setting p. 269 and context pp. 270–272. DOI.

Motivation

Many approximation problems resist the standard PCP toolkit: the best known NP-hardness factors for Max-Cut, Vertex-Cover and approximate graph colouring are far from the best known polynomial-time algorithms. To explain this gap, Khot (CCC 2002) proposed the Unique-Games Conjecture and the family of $d$-to-1 Games Conjectures. The $d$-to-1 conjectures assert perfect completeness: the hard instances are either fully satisfiable, or satisfiable only to a vanishing extent. Perfect completeness is what makes these conjectures usable for colouring problems, where a "yes" instance must be genuinely $3$-colourable rather than almost so.

A line of work culminating in Khot–Minzer–Safra and Dinur–Khot–Kindler–Minzer–Safra established the almost-perfect completeness version for $2$-to-1 games: for every $\varepsilon>0$ there is an alphabet bound $r$ such that distinguishing value $\ge 1-\varepsilon$ from value $\le\varepsilon$ is NP-hard. Their route goes through Håstad's hardness for linear equations, which cannot have perfect completeness, so the loss is intrinsic to the technique. The source paper of this mission removes that loss for $d = 4$.

Setting

A label-cover instance $\Psi$ (Definition 1.1 of the source) consists of a bipartite graph $G = (L \sqcup R, E)$, two finite alphabets $\Sigma_L, \Sigma_R$, and for each edge $e = (u,v)$ a constraint $\Phi_e \subseteq \Sigma_L \times \Sigma_R$. The constraint is a projection constraint if there is $\varphi_e : \Sigma_L \to \Sigma_R$ with $\Phi_e = \{(\sigma, \varphi_e(\sigma))\}$, and a $d$-to-1 constraint if in addition $|\varphi_e^{-1}(\sigma)| = d$ for every $\sigma \in \Sigma_R$. Given assignments $A_L : L \to \Sigma_L$ and $A_R : R \to \Sigma_R$, the fraction of satisfied edges is $\mathrm{val}_\Psi(A_L, A_R)$, and

$$\mathrm{val}(\Psi) \;=\; \max_{A_L, A_R} \mathrm{val}_\Psi(A_L, A_R).$$

An instance all of whose constraints are $d$-to-1 is a $d$-to-1 game.

For $0 < s < c \le 1$, $\mathrm{Gap\text{-}}d\mathrm{\text{-}to\text{-}}1_r(c,s)$ is the promise problem: given a $d$-to-1 game with both alphabets of size at most $r$, distinguish $\mathrm{val}(\Psi) \ge c$ from $\mathrm{val}(\Psi) \le s$. Writing $\mathrm{GapPLC}_r(c,s)$ for the same promise problem over all projection instances, the PCP theorem together with the parallel repetition theorem gives that $\mathrm{GapPLC}_{r}(1,\varepsilon)$ is NP-hard for a suitable $r = r(\varepsilon)$ (Theorem 1.2 of the source); this mission takes that statement as an external input.

Formalization targets

Goal — Theorem 1.6 of the source

$$\forall \varepsilon > 0 \ \exists r \in \mathbb{N}^{+} : \quad \mathrm{Gap\text{-}4\text{-}to\text{-}1}_r(1,\varepsilon) \text{ is NP-hard.}$$

In Lean this is stated as a polynomial-time gap-preserving reduction: for every $\varepsilon > 0$ there is a soundness threshold $s \in (0,1)$ such that for every source alphabet bound $r_0$ there is a target alphabet bound $r$ and a polynomial-time computable map sending projection label-cover instances with alphabets of size at most $r_0$ and value $1$ to $4$-to-1 games with alphabets of size at most $r$ and value $1$, and instances of value at most $s$ to $4$-to-1 games of value at most $\varepsilon$. Combined with the NP-hardness of $\mathrm{GapPLC}_{r_0}(1,s)$, this is exactly Theorem 1.6.

Supporting targets

The milestone list follows the source's own numbering: the hardness of approximate colouring of $3$-uniform hypergraphs that starts the construction (Theorem 3.1), the two Grassmann decoding theorems the inner PCP rests on (Theorems 3.2 and 3.3), the sunflower bound on zoom-outs (Lemma 3.8), and the linear-algebraic layer connecting NAE-satisfying bilinear forms with their tensor decompositions (Propositions 4.13, 4.14 and Corollary 4.15).

Significance

Theorem 1.6 confirms the $4$-to-1 Games Conjecture, the first of Khot's $d$-to-1 conjectures to be settled with perfect completeness. Via known reductions it yields: for every $k$, it is NP-hard to $k$-colour a $3$-colourable graph (previously known for $k = 5$); for every $\delta>0$, it is NP-hard to find an independent set of relative size $\delta$ in a $2$-colourable $3$-uniform hypergraph; and hardness results for low-rank matrix completion.

None of this material is formalized today. Mathlib has no label cover, no PCP machinery, no Grassmann graph and no complexity classes beyond the computability layer. A complete development therefore contributes reusable infrastructure — finite two-prover games and their value, gap-preserving reductions, the Grassmann graph over $\mathbb{F}_2$ and its agreement tests — well beyond this single theorem.

Difficulty

The obvious attempt is to redo the $2$-to-1 construction with a perfectly complete outer PCP, namely hardness of systems of quadratic equations over $\mathbb{F}_2$ in place of linear ones. This fails at composition: the Grassmann agreement test, the only known device that produces $d$-to-1 constraints, is a test for linear functions and cannot certify quadratic constraints. Linearizing the quadratic equations by a low-rank test destroys the covering property of the outer PCP, which is what makes the composed soundness analysis work. The source paper's answer is a three-layer construction (outer, middle and inner PCP) with a lazy parallel repetition in the middle layer and an inner PCP based on a tensor of the standard Grassmann encoding with Golowich's low-rank variant.

Formalization scope

All objects are finite and explicit. A label-cover instance carries left vertices $\{0,\dots,n_L-1\}$, right vertices $\{0,\dots,n_R-1\}$, alphabets $\{0,\dots,|\Sigma_L|-1\}$ and $\{0,\dots,|\Sigma_R|-1\}$, a finite edge set, and a projection map for every pair of vertices; only projection instances are representable, as in Definition 1.1. The value is the supremum over all pairs of assignments of the fraction of satisfied edges, taken in $\mathbb{R}$; when there are no edges, or no assignments at all, the convention gives value $0$. A tripled set (Definition 4.1) is modelled as $\iota \times \{0,1,2\}$, with the triple indexed by $i$ being $\{(i,0),(i,1),(i,2)\}$. The Grassmann objects live in $\mathbb{F}_2^n$ modelled as $\mathrm{Fin}\,n \to \mathbb{Z}/2$, and all probabilities are ratios of cardinalities of finite sets of subspaces, with the convention that an empty denominator gives $0$.

Hardness is not stated as "NP-hard" — no notion of NP is available — but as the existence of a reduction. This matters: a reduction required only to preserve the gap, with no computability condition, would be trivially satisfiable by a map that inspects the value of its input and returns one of two fixed instances. The formalization therefore requires the reduction map to be computed by a Turing machine within a polynomial time bound, using Mathlib's Turing.TM2ComputableInPolyTime together with an explicit binary encoding of instances. The NP-hardness of the source problem $\mathrm{GapPLC}_{r_0}(1,s)$ (Theorem 1.2, i.e. the PCP theorem plus parallel repetition) is an external input and is not part of this mission.

Contributions of intermediate infrastructure are welcome: the games of Sections 4–6 (Game1a, Game1b, Game2a, Game2b, Game2c, Game3) and their completeness and soundness lemmas are the natural next layer of milestones, as are the covering properties of Appendix C and the list-decoding bounds of Appendix E.

Selected references

• Yumou Fei, Dor Minzer, Shuo Wang, On the Hardness of 4-to-1 Games with Perfect Completeness, ECCC TR26-179 (2026), https://eccc.weizmann.ac.il/report/2026/179/
• Subhash Khot, On the power of unique 2-prover 1-round games, STOC 2002, https://doi.org/10.1145/509907.509985
• Irit Dinur, Subhash Khot, Guy Kindler, Dor Minzer, Muli Safra, Towards a proof of the 2-to-1 games conjecture?, STOC 2018, https://doi.org/10.1145/3188745.3188804
• Subhash Khot, Dor Minzer, Muli Safra, Pseudorandom sets in Grassmann graph have near-perfect expansion, FOCS 2018, https://doi.org/10.1109/FOCS.2018.00062
• Louis Golowich, New Explicit Constant-Degree Lossless Expanders, FOCS 2023, https://arxiv.org/abs/2306.07551

Motivation

Quantum query algorithms are known to beat classical ones on problems with algebraic structure -- period finding, hidden subgroups, forrelation. No such speedup is known for a problem with no structure at all. Aaronson and Ambainis proposed making that observation into a theorem, and reduced it to a question with no quantum content: a statement about bounded low-degree polynomials on the Boolean cube (Aaronson--Ambainis 2009).

The question has resisted since. A timeline of what is actually established:

• 2009. Aaronson and Ambainis state the conjecture and prove that it implies almost-everywhere classical simulation of quantum query algorithms.
• 2012. Montanaro settles the case of block-multilinear forms whose coefficients all have the same magnitude.
• 2016. O'Donnell and Zhao reduce the general conjecture to a restricted class, the one-block decoupled polynomials.
• 2019. Aaronson surveys a decade of partial progress (retrospective).
• 2022. Bansal, Sinha and de Wolf prove the conjecture for completely bounded degree-$d$ block-multilinear forms, obtaining influence $1/\mathrm{poly}(d)$ at constant variance (arXiv:2203.00212).
• 2024. The conjecture is established for a non-negligible fraction of random restrictions (arXiv:2402.13952).

The cases that are settled are settled under structural hypotheses -- block-multilinearity, complete boundedness, symmetry, Boolean range. The general statement is open.

Setting

Let $N$ be a positive integer. The Boolean cube is $\{0,1\}^N$, carrying the uniform distribution; a point $x$ is identified with the $0/1$ real vector it names, so a real multivariate polynomial $p$ in $N$ variables has a value $p(x)$ at each cube point. For a function $f$ on the cube write

$$\mathbb{E}[f]=2^{-N}\sum_{x\in\{0,1\}^N}f(x).$$

The variance of $p$ is $\operatorname{Var}[p]=\mathbb{E}\big[(p-\mathbb{E}[p])^2\big]$. Writing $x^{\oplus i}$ for $x$ with its $i$-th bit flipped, the influence of coordinate $i$ on $p$ is

$$\operatorname{Inf}_i[p]=\mathbb{E}\big[(p(x)-p(x^{\oplus i}))^2\big].$$

These are the combinatorial forms of both quantities, as used in the source; no Fourier--Walsh expansion is required to state anything below. The degree of $p$ is its total degree as a polynomial. Call $p$ bounded when $0\le p(x)\le 1$ at every cube point -- a condition imposed only on the cube, not on all of $\mathbb{R}^N$.

Target

The goal is the conjecture in the shape stated by its authors: there is an absolute constant $C$ such that for all $N$, all $d$, every polynomial $p$ of degree at most $d$ that is bounded on the cube, and every $\varepsilon>0$ with $\operatorname{Var}[p]\ge\varepsilon$, some coordinate $i$ satisfies

$$\operatorname{Inf}_i[p]\;\ge\;\Big(\frac{\varepsilon}{d}\Big)^{C}.$$

The constant $C$ is quantified outermost and may depend on nothing. That uniformity is the entire content: bounds that degrade exponentially in $d$ are already known, and a goal naming a specific exponent would be superseded by the next improvement.

Significance

The result itself. Aaronson and Ambainis prove that the conjecture implies that the acceptance probability of any bounded-error $T$-query quantum algorithm on a Boolean input can be approximated, to small error on all but a small fraction of inputs, by a classical algorithm making $\mathrm{poly}(T)$ queries. Quantum speedups would then require structure in a precise sense. The conjecture also has purely classical content, asserting that boundedness plus low degree forces variance to concentrate on some single coordinate rather than spread across all $N$. Without it, no such concentration is known at any rate polynomial in $1/d$.

Formalizing it. The conjecture is open, so this mission does not formalize a known proof of the goal. What it produces is a machine-checked statement of the conjecture together with formalizations of the partial results above, each currently existing only on paper. The milestone chain also yields reusable infrastructure for analysis of Boolean functions, of which Mathlib currently contains none: no Fourier--Walsh expansion, no influence, no variance on the cube.

Difficulty

The elementary bound is the Poincare inequality on the cube, $4\operatorname{Var}[p]\le\sum_i\operatorname{Inf}_i[p]$, which yields a coordinate with influence at least $4\varepsilon/N$. This is tight for the dictator $p(x)=x_1$ and depends on $N$, so it says nothing: the conjecture demands a bound free of $N$ entirely.

The natural repair is the route available when $p$ takes only the values $0$ and $1$. A Boolean-valued polynomial of degree $d$ depends on boundedly many coordinates, which immediately produces an influential one. That argument does not survive relaxing the range to the interval $[0,1]$: a bounded real-valued polynomial of low degree need not depend on boundedly many coordinates, and every known substitute loses a factor exponential in $d$. Closing the gap between exponential and polynomial dependence on $d$ is the difficulty, and it is where all of the partial results stop.

Formalization scope

Polynomials are MvPolynomial (Fin N) ℝ and degree is Mathlib's totalDegree, so the statement needs no bespoke notion of degree. Expectation is a finite sum scaled by $2^{-N}$ rather than a measure-theoretic integral, keeping every definition elementary. Bit flipping is Function.update x i (!x i). Boundedness is asserted at cube points only. Variance and influence are the combinatorial definitions above, published as the definition AaronsonAmbainis.

Three points close off degenerate readings. The exponent $O(1)$ of the source is rendered as an existentially quantified natural number with no leading multiplicative constant, since admitting one weakens the claim. Taking that exponent to be $0$ would demand influence at least $1$ and is therefore not a trivializing choice, while larger exponents only weaken the bound; the content is that some fixed exponent suffices for all $N$ and $d$ at once. The hypothesis $\deg p\le d$ is universally quantified over $d$, which is equivalent to the source's exact-degree form because the smallest admissible $d$ gives the strongest conclusion. The cases $N=0$ and $d=0$ are vacuous, since $0<\varepsilon\le\operatorname{Var}[p]$ fails for a constant polynomial.

A complete development needs, beyond the published definitions, a Fourier--Walsh layer with Parseval's identity, the level-$k$ machinery used by the partial results, and -- for the completely bounded case -- operator-space norms on multilinear forms. All of the Boolean-analysis material is reusable well beyond this mission. Contributions of any milestone are welcome, as are alternative formalizations of the definitions in function-level rather than polynomial-level form.

Out of scope: the quantum simulation consequence is not formalized here. Stating it requires a formal quantum query model, which no Lean library currently provides.

Selected references

• S. Aaronson, A. Ambainis, The Need for Structure in Quantum Speedups, Theory of Computing 10 (2014) 133--166; arXiv:0911.0996. Conjecture 6.
• N. Bansal, M. Sinha, R. de Wolf, Influence in Completely Bounded Block-multilinear Forms and Classical Simulation of Quantum Algorithms, CCC 2022; arXiv:2203.00212.
• Aaronson--Ambainis Conjecture Is True For Random Restrictions, 2024; arXiv:2402.13952.
• S. Aaronson, The Aaronson-Ambainis Conjecture (2008-2019), blog retrospective.
• S. Arunachalam, J. Briet, C. Palazuelos, Quantum query algorithms are completely bounded forms, SIAM J. Comput. 48 (2019); arXiv:1711.07285.
• AIM problem list, Analysis on the hypercube with applications to quantum computing, aimpl.org/hypercubequantum.

Why estimate a mean with a quantum algorithm?

Many computational tasks produce a real number by running a randomized procedure once, then estimate its expected value by running that procedure repeatedly. The number of repetitions needed for a given additive accuracy depends on the output variance. Montanaro's Quantum speedup of Monte Carlo methods studies the same estimation problem when the procedure can be run coherently as a quantum algorithm and its unitary part can also be inverted. The bounded-variance result gives an estimator whose dependence on the requested accuracy is approximately linear in $1/\epsilon$, compared with the quadratic dependence of ordinary sampling, up to logarithmic factors and the paper's model-specific operation counts. The exact asymptotic claims are in Theorem 5 of the pinned preprint, p. 12.

This mission concentrates on the probability and accuracy claim of that theorem. It includes the mean-estimation result for a nonnegative output from Lemma 4, because Algorithm 3 invokes that estimator twice after centering a general real output. The underlying amplitude-estimation theorem is a separate, already posed result, QAmpEst.Est.theorem_12; this mission uses the accuracy guarantee stated in Montanaro's Theorem 3 as the interface to that subroutine.

Outputs, truncations, and estimates

Let $X=v(\mathcal A)$ denote the real output of a quantum algorithm $\mathcal A$ under one run, and let $P$ be its probability law. The mean is $\mathbb E[X]$, and the variance is $\operatorname{Var}(X)=\mathbb E[(X-\mathbb E[X])^2]$. The result assumes a known $\sigma>0$ with $\operatorname{Var}(X)\le\sigma^2$. Although the paper describes a circuit that prepares and measures $X$, its accuracy statements depend on the distribution of $X$; the Lean interface therefore represents a run as a measurable real random variable on a probability space.

For real thresholds $a<b$, the truncation $X_{[a,b)}$ returns $X$ when $a\le X<b$ and zero otherwise. The variants $X_{<a}$ and $X_{\ge b}$ retain the output below $a$ and at or above $b$, respectively. They do not clip a value to a threshold. The $L^2$ size is $\|X\|_2=\sqrt{\mathbb E[X^2]}$. These are the output transformations defined in §2.2, p. 9, and used in Lemma 4, pp. 10–11.

Algorithm 2 estimates a nonnegative mean using the base interval $[0,1)$ and the half-open bands $[2^{\ell-1},2^\ell)$ for $1\le\ell\le k$. It sets $k=\lceil\log_2(1/\epsilon)\rceil$ and $t_0=\lceil D\sqrt{\log_2(1/\epsilon)}/\epsilon\rceil$, then adds the base estimate to $2^\ell$ times each band estimate. A successful Algorithm 1 call means that its estimate of a $[0,1]$-valued output $Y$ differs from $\mathbb E[Y]$ by at most $C(\sqrt{\mathbb E[Y]}/t+1/t^2)$, the accuracy bound of Theorem 3, pp. 8–9.

Algorithm 3 rescales $X$ by $\sigma$, draws one sample $m$ from $X/\sigma$, and centers the rescaled output at $m$. It feeds the negative and nonnegative parts, each divided by four, to Algorithm 2 at accuracy $\epsilon/(32\sigma)$ and recombines their estimates. The two calls are specified to fail with probability at most $1/9$ each; the paper describes boosting Algorithm 2's initial success probability for this use on p. 11.

Formalization targets

Lemma 4: nonnegative mean accuracy

When every Algorithm 1 call satisfies its accuracy bound and $0<\epsilon<1/2$, the output $\widetilde\mu$ of Algorithm 2 obeys

$$|\widetilde\mu-\mathbb E[X]|\le\epsilon(\|X\|_2+1)^2.$$

The constant $D>0$ is chosen once for a fixed positive universal constant $C$ from Theorem 3. It is independent of $X$ and $\epsilon$.

Theorem 5: bounded-variance accuracy

For $\operatorname{Var}(X)\le\sigma^2$, $\sigma>0$, and $0<\epsilon<4\sigma$, Algorithm 3 returns $\widehat\mu$ with

$$\Pr\bigl(|\widehat\mu-\mathbb E[X]|\le\epsilon\bigr)\ge\frac23.$$

This is the mission goal. Its probability is over the preliminary sample and both subsequent estimation runs. The milestone list follows the exact displayed statements used in Lemma 4 and the proof of Theorem 5, with their source pages.

What the result supplies

Theorem 5 turns an estimator for nonnegative outputs with finite second moment into one that handles signed outputs whose variance is bounded, without assuming a bound on the magnitude or mean of the output. That extension matters when the quantity being averaged can be negative or has a large offset: a second-moment bound on $X$ itself would then be much stronger than the paper's variance hypothesis. The stated error and success probability are the mathematical guarantee on which the paper's resource comparison rests; the comparison itself includes quantum operations absent from the measure-theoretic statement.

The formal development supplies reusable definitions of truncations, dyadic estimates, and the centered positive and negative parts, together with precisely quantified probability claims. It leaves Lemma 4 and Theorem 5 as open Lean proof targets. The amplitude-estimation statement behind Theorem 3 is already posed separately on Prove2Me, while the composed bounded-variance result and the displayed intermediate claims are the new targets here.

Where the difficulty lies

A bound for one $[0,1]$-valued call does not directly bound the mean of a signed, unbounded output. Truncating after finitely many bands leaves a tail, and the sum of errors over the retained bands can grow with their weights. The theorem must control both effects while keeping $D$ independent of the output distribution. For the signed case, the initial sample is random; its deviation, the two later failures, and the scale of the centered output all contribute to the final probability. Replacing that sample by the exact mean would remove a substantive part of the claim.

Formalization scope

Lean uses probability measures and measurable real outputs for the laws of $v(\mathcal A)$ and Algorithm 3's preliminary sample. The law of that sample is fixed to the image law of $X/\sigma$, so it cannot be selected arbitrarily. The successful-call predicate names the actual truncated outputs and the paper's $k$ and $t_0$ formulas; it does not assume Lemma 4's final error bound. The sample space carrying the later estimates is allowed to encode their joint dependence on the preliminary sample. Events are measured with extended nonnegative real values.

The $L^2$ hypotheses state that the second moment is finite. In Mathlib the real-valued variance and the integral can return a default value on a nonintegrable input, which would make a bare variance inequality or a bare $\|X\|_2$ bound misleading. The paper implicitly uses finite variance where those quantities occur. The condition $0<\epsilon$ makes the divisions and logarithms in the algorithm parameters meaningful. The natural-number expression $\ell-1$ occurs only on bands indexed by $\ell\ge1$.

The quantum circuit for Algorithm 1, the construction of an inverse unitary, and the $O(\cdot)$ copy and operation counts are outside the formal statements. Their interface is Theorem 3's numerical accuracy event. Contributions to the dyadic inequalities, the finite-variance probability bound, and their composition into the final event are in scope. The definitions are also useful for other mean estimators that split a real output into bounded pieces.

Selected references

• Ashley Montanaro, Quantum speedup of Monte Carlo methods, arXiv:1504.06987v3 [quant-ph], 2017, especially §§2.1–2.3, pp. 8–12. Pinned preprint.
• Gilles Brassard, Peter Høyer, Michele Mosca, and Alain Tapp, Quantum Amplitude Amplification and Estimation, Contemporary Mathematics 305, 2002. arXiv preprint.

Motivation

Decoded quantum interferometry (DQI) is a quantum algorithm, introduced by Jordan, Shutty, Wootters, Zalcman, Schmidhuber, King, Isakov, Khattar and Babbush (arXiv:2408.08292), that turns an approximate optimization problem over a finite field into a decoding problem for a linear code. It applies to max-LINSAT: given linear constraints over $\mathbb F_p$, satisfy as many of them as possible. For structured instances such as optimal polynomial intersection the authors find DQI reaching approximation ratios that no known polynomial-time classical algorithm reaches, which makes it one of the few concrete candidates for a quantum advantage in optimization.

Whether DQI is useful on an instance depends on one number: the expected fraction of constraints satisfied by the string it outputs. Theorem 4.1 of the paper computes this number, in the limit of many constraints, for the best DQI state of a given degree. Every comparison of DQI with classical algorithms in the paper (simulated annealing, Prange's algorithm, the OPI and max-XORSAT benchmarks) is a comparison against this formula, and the follow-up analysis of imperfect decoders (Theorem 10.1) is a perturbation of it.

Setting

Fix a prime $p$. A max-LINSAT instance is a matrix $B\in\mathbb F_p^{m\times n}$ with rows $\mathbf b_1,\dots,\mathbf b_m$ and subsets $F_1,\dots,F_m\subseteq\mathbb F_p$; constraint $i$ asks that $\mathbf b_i\cdot\mathbf x\in F_i$ (Definition 2.1). Throughout, $m>n$ and every $F_i$ has the same size $r\in\{1,\dots,p-1\}$. Put $f_i(a)=+1$ if $a\in F_i$ and $-1$ otherwise, and

$$f(\mathbf x)=\sum_{i=1}^m f_i(\mathbf b_i\cdot\mathbf x),\qquad s(\mathbf x)=\#\{i:\mathbf b_i\cdot\mathbf x\in F_i\}.$$

For a real polynomial $P$ of degree at most $\ell$, the DQI state is $|P(f)\rangle=\sum_{\mathbf x\in\mathbb F_p^n}P(f(\mathbf x))|\mathbf x\rangle$, normalized so that $\sum_{\mathbf x}P(f(\mathbf x))^2=1$. Measuring it in the computational basis returns $\mathbf x$ with probability $P(f(\mathbf x))^2$, so the expected number of satisfied constraints is

$$\langle s\rangle=\sum_{\mathbf x}P(f(\mathbf x))^2\,s(\mathbf x),$$

and $\langle s^{(m,\ell)}\rangle_{\rm opt}$ is its supremum over all such $P$.

The dual code is $C^\perp=\{\mathbf d\in\mathbb F_p^m:B^T\mathbf d=0\}$ and $d^\perp$ is the least Hamming weight of a nonzero codeword. The condition $2\ell+1<d^\perp$ says that syndromes of errors of weight up to $\ell$ (and a little more) determine the error.

The analysis passes through rescaled constraint functions $g_i=(f_i-\bar f)/\varphi$ with Fourier transforms $\tilde g_i$, the elementary symmetric polynomials $P^{(k)}$ evaluated at the $g_i(\mathbf b_i\cdot\mathbf x)$, and the $(\ell+1)\times(\ell+1)$ symmetric tridiagonal matrix $A^{(m,\ell,d)}$ with diagonal $0,d,2d,\dots,\ell d$ and off-diagonal entries $a_k=\sqrt{k(m-k+1)}$, at $d=(p-2r)/\sqrt{r(p-r)}$.

Formalization targets

Goal: Theorem 4.1 (the semicircle law)

Fix $p$, $r$ and $\mu\ge0$. For any sequence of instances with $m\to\infty$, $\ell/m\to\mu$ and $2\ell+1<d^\perp$, writing $\rho=r/p$,

$$\lim\frac{\langle s^{(m,\ell)}\rangle_{\rm opt}}{m}=\begin{cases}\big(\sqrt{\mu(1-\rho)}+\sqrt{\rho(1-\mu)}\big)^2,&\rho\le1-\mu,\\ 1,&\text{otherwise.}\end{cases}$$

For $\rho=\tfrac12$ the curve is $\tfrac12+\sqrt{\mu(1-\mu)}$, a semicircle, which gives the theorem its name.

Milestones

1. The normalization of the rescaled $g_i$, (37)–(40).
2. Lemma A.1: under a common quadratic identity, $P(x_1+\dots+x_m)$ is a fixed linear combination of elementary symmetric polynomials.
3. The counting identity (68), $\sum_{|\mathbf y|=k}|\tilde g(\mathbf y)|^2=\binom mk$, and the Fourier picture (65) of the DQI state.
4. Lemma 9.1 (norm $=\|\mathbf w\|^2$ when $2\ell<d^\perp$) and Lemma 9.2 (the expected count is $\frac{mr}p+\frac{\sqrt{r(p-r)}}p\mathbf w^TA^{(m,\ell,d)}\mathbf w$ when $2\ell+1<d^\perp$).
5. The finite-size identity (131): $\langle s^{(m,\ell)}\rangle_{\rm opt}/m=\rho+\sqrt{\rho(1-\rho)}\,\lambda_{\max}^{(m,\ell,d)}/m$.
6. Lemma 9.3, $\lambda_{\max}^{(m,\ell,d)}/m\to\mu d+2\sqrt{\mu(1-\mu)}$, with its lower half (114) and the Gershgorin bound (129).
7. The algebra (132) and (136)–(137) that produce the closed form.

Significance

The result. Theorem 4.1 makes DQI's performance a closed-form function of two numbers, $r/p$ and $\ell/m$, and moves every question about an instance into coding theory: how large a $d^\perp$ the instance's dual code has, and whether it can be decoded efficiently up to $\ell$ errors. The OPI advantage claim of the paper, the comparison with Prange's algorithm on max-XORSAT, and the imperfect-decoding bound of Theorem 10.1 all start from this formula. The finite-size identity (131) is also useful on its own: it gives the exact optimum for any instance, not only in the limit.

Formalizing it. The theorem is proved in the paper; to our knowledge no part of it has been machine-checked. A formalization would check the Fourier bookkeeping of §8.2.1 and §9 (normalizations $\sqrt{p^{n-k}\binom mk}$, character sums over $\mathbb F_p$), the claim that every degree-$\ell$ DQI state is a combination of the $|P^{(k)}\rangle$ and conversely, and the eigenvalue asymptotics of the tridiagonal matrix. Two points of the printed text need care and are stated correctly here: Lemma 9.2 writes its decomposition in the $f_i$ where the normalization requires the rescaled $g_i$, and the "otherwise $=1$" branch of Theorem 4.1 is argued only briefly on p. 34.

Difficulty

The algebraic steps are finite but long, and every one carries a normalization that a careless formalization gets wrong. The asymptotic step is the main obstacle. Lemma 9.3 needs a lower bound on $\lambda_{\max}$ from a test vector of growing width and a matching upper bound from Gershgorin's theorem, and the upper bound holds only under $d\ge-(m-2\ell)/\sqrt{\ell(m-\ell)}$, which is exactly the regime $\rho\le1-\mu$. In the other regime that hypothesis fails and the Gershgorin bound overshoots, so the limit $1$ needs a separate argument; the observation that $\langle s\rangle_{\rm opt}$ "increases in $r$", printed on p. 34, does not give it at fixed $p$ and $r$. A second difficulty is that $\langle s\rangle_{\rm opt}$ is a supremum over polynomials, while Lemma 9.2 is a statement about weight vectors $\mathbf w$; identifying the two needs both directions of Lemma A.1's correspondence and the normalization of Lemma 9.1.

Formalization scope

All objects live in the namespace DQI.Semicircle and one definitions file. $\mathbb F_p$ is ZMod p with [Fact p.Prime]; vectors are Fin n → ZMod p; constraints are indexed by Fin m from $0$. $\omega_p^a=\exp(2\pi i\,a/p)$ is computed from the representative of $a$ in $\{0,\dots,p-1\}$. Polynomials are real with natDegree ≤ ℓ; weight vectors are real. The optimum $\langle s\rangle_{\rm opt}$ is the real supremum over exactly the normalized polynomials of degree at most $\ell$ evaluated at $f(\mathbf x)$; its set is nonempty (constant polynomials) and bounded by $m$. The dual-distance condition is "every nonzero $\mathbf d$ with $B^T\mathbf d=0$ has weight $>t$"; $d^\perp$ is never an infimum, and $m>n$ (the paper's standing assumption) guarantees a nonzero codeword, so the condition forces $2\ell<m$. $\lambda_{\max}$ is the supremum of the real spectrum. The limit "$m\to\infty$ with $\ell/m$ fixed" is any sequence of instances with $m_j\to\infty$ and $\ell_j/m_j\to\mu$, with $p$ and $r$ fixed along it. Convergence of the ratio includes irrational $\mu$ with integer sizes.

Added hypotheses, all disclosed in the items: Lemma 9.2 decomposes in the $g_i$ rather than the printed $f_i$; (129) assumes $\ell\ge1$ to avoid dividing by $\sqrt0$; Lemma 9.3 imposes its hypothesis on $d$ only when $\ell_j\ge1$; (114) is stated as a $\liminf$ with an explicit $\varepsilon$.

A formalization that replaces $\langle s\rangle_{\rm opt}$ by a supremum over all states (which gives $1$), drops "nonzero" from the distance condition (which makes it unsatisfiable), or states the goal at a single $m$ is not this theorem and is ruled out by the definitions above.

Needed infrastructure: Fourier analysis on $\mathbb F_p^n$ (character orthogonality, Parseval), elementary symmetric polynomials and their reduction modulo a quadratic, Rayleigh quotients and Gershgorin discs for real symmetric matrices, and elementary limits. The tridiagonal-matrix bounds and the quadratic-reduction lemma are reusable beyond DQI. Proofs of any milestone, alternative arguments for the "otherwise" branch, and sharper finite-$m$ bounds on $\lambda_{\max}$ are welcome.

Selected references

• S. P. Jordan, N. Shutty, M. Wootters, A. Zalcman, A. Schmidhuber, R. King, S. V. Isakov, T. Khattar, R. Babbush, Optimization by Decoded Quantum Interferometry, arXiv:2408.08292v5, 2025. https://arxiv.org/abs/2408.08292
• S. Gershgorin, Über die Abgrenzung der Eigenwerte einer Matrix, Izv. Akad. Nauk SSSR, Ser. Fiz.-Mat. 6, 749–754, 1931.
• R. G. Gallager, Low-Density Parity-Check Codes, IRE Trans. Inform. Theory 8(1), 21–28, 1962. https://doi.org/10.1109/TIT.1962.1057683

Motivation

A firm that fills a fixed number of positions from a pool of applicants faces uncertainty at every stage: applicants differ in value, and an offer may be declined. When offers must go out at once, as in a recruiting season with a common deadline, the firm decides a single offer set and lives with however many candidates accept. Sending too few offers leaves positions empty; sending too many hires beyond capacity at a cost. This trade-off is the same as overbooking in revenue management (airline seats, hotel rooms), with the difference that candidates are heterogeneous in both value and acceptance probability.

Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024) study three hiring-pipeline models through linear programming relaxations. This mission formalizes their lower bound for the third model, Simultaneous Offering (§3.3 and §6 of the paper). The question it answers is practical: how much is lost if the firm restricts itself to value-ordered policies, which send offers to the $m$ most valuable candidates for some $m$, instead of searching over all $2^n$ offer sets? Value-ordered policies are natural, because a firm rarely wants to withhold offers from its best candidates, and the optimal one is computable by a short dynamic program. The paper shows (Example 1, p. 25) that they can be arbitrarily bad in general, and that they are provably good when every candidate's value is bounded below.

Setting

An instance $I=(k,n,p,v)$ has $k$ positions and $n$ candidates, $1\le k\le n$. Candidate $i$ accepts an offer independently with probability $p_i\in[0,1]$ and then contributes value $v_i\ge0$. Candidates are labelled so that $v_1\ge v_2\ge\dots\ge v_n$. The firm chooses an offer set $S\subseteq[n]$; with $A\subseteq S$ the random set of acceptances, the reward is

$$\sum_{i\in A}v_i-\big[\,|A|-k\,\big]^+,$$

the cost per candidate hired beyond capacity being normalised to $1$. $\mathrm{OPT}_{\mathrm{sim}}(I)$ is the best expected reward over offer sets. For $\tau>0$ the instance is $\tau$-bounded, $I\in\mathcal I^\tau_{\mathrm{sim}}$, if $v_i\ge\tau$ for all $i$; the interesting range is $\tau\in(0,1)$, since for $\tau\ge1$ offering to everyone is optimal.

The benchmark is the LP relaxation

$$\mathrm{LP}_{\mathrm{sim}}(I)=\max_{y,z}\ \sum_{i}v_ip_iy_i+z\quad\text{s.t.}\quad z\le k-\sum_ip_iy_i,\ \ z\le0,\ \ 0\le y_i\le1,$$

which charges the overage cost on the expected number of hires. Write $V_{\mathrm{high}}=\{i:v_i>1\}$ and $P_{\mathrm{high}}=\sum_{i\in V_{\mathrm{high}}}p_i$.

The algorithm $\mathrm{ALG}^s_{\mathrm{sim}}$, for $s\in[0,1]$, takes an optimal LP solution $y$, scales its total mass $\sum_iy_ip_i$ by $s$ to $\kappa$, and fills mass $\kappa$ from the most valuable candidate down: $y'_i=1$ while the prefix mass $\sum_{l\le i}p_l$ stays at most $\kappa$, one fractional entry, then zeros. Offers are then sent independently with probabilities $y'_i$, so the algorithm randomises between two value-ordered policies. Its expected reward is $R_{\mathrm{ALG}^s_{\mathrm{sim}}}(I)$.

The guarantee involves the truncated Poisson mean $\mathbb E[\min\{\mathrm{Pois}(\lambda),k\}]=\sum_{j\ge0}\min\{j,k\}e^{-\lambda}\lambda^j/j!$ and

$$\alpha^\tau_k=\sup_{0\le s\le1}\Big(s-\frac{s}{\tau}+\frac{\mathbb E[\min\{\mathrm{Pois}(sk),k\}]}{\tau k}\Big).$$

Formalization targets

Goal: Theorem 3 (p. 30)

For $\tau\in(0,1)$, every $I\in\mathcal I^\tau_{\mathrm{sim}}$, every optimal solution of $\mathrm{LP}_{\mathrm{sim}}(I)$ and a maximiser $s^*\in[0,1]$ of the objective defining $\alpha^\tau_k$,

$$R_{\mathrm{ALG}^{s^*}_{\mathrm{sim}}}(I)\ \ge\ \alpha^\tau_k\,\mathrm{LP}_{\mathrm{sim}}(I).$$

Milestones

• Lemma 10 (p. 27): $\mathrm{LP}_{\mathrm{sim}}(I)\ge\mathrm{OPT}_{\mathrm{sim}}(I)$.
• Lemma 11 (p. 27): some optimal LP solution is a filled prefix $y=(1,\dots,1,y_j,0,\dots,0)$ with $y_j>0$.
• Lemma 12 (p. 28): the total mass of such a solution is $P_{\mathrm{high}}$ if $P_{\mathrm{high}}>k$ and $\min\{k,P_{\mathrm{total}}\}$ otherwise (posed under the disclosed hypothesis $v_i>0$, $v_i\ne1$, $p_i>0$).
• Monotonicity (App. D.5, p. ec16): $\mathbb E[\min\{\mathrm{Pois}(x),k\}]/x$ is decreasing in $x$.
• Proposition EC.2 (p. ec3): $\mathbb E[\min\{\mathrm{Pois}(k),k\}]=k(1-e^{-k}k^k/k!)$.
• Lemma 13 (p. 29): if $P_{\mathrm{high}}\le k$, then $R_{\mathrm{ALG}^s_{\mathrm{sim}}}(I)\ge\big(s-s/\tau+\mathbb E[\min\{\mathrm{Pois}(sk),k\}]/(\tau k)\big)\mathrm{LP}_{\mathrm{sim}}(I)$ for every $s\in[0,1]$.
• The $\mathrm{ALG}^1$ bound (p. 30): on every $\tau$-bounded instance, $R_{\mathrm{ALG}^1_{\mathrm{sim}}}(I)\ge(1-e^{-k}k^k/(k!\tau))\,\mathrm{LP}_{\mathrm{sim}}(I)$.
• Lemma 14 (p. 29): if $P_{\mathrm{high}}>k$, deflating the acceptance probabilities to an instance with $P_{\mathrm{high}}=k$ does not increase the ratio $R_{\mathrm{ALG}^{s^*}_{\mathrm{sim}}}/\mathrm{LP}_{\mathrm{sim}}$ (posed under the disclosed hypothesis $v_i\ne1$).

Significance

Theorem 3 makes value-ordered policies an $\alpha^\tau_k$-approximation on $\tau$-bounded instances, through Lemma 10. The factor tends to $1$ as $k\to\infty$ for fixed $\tau$: at $s=1$ it is at least $1-e^{-k}k^k/(k!\tau)=1-O(1/\sqrt k)$ (Corollary 4). The paper's Theorem 4, the subject of the companion mission in this series, shows that no value-ordered policy beats the same expression with the supremum over $s\ge0$, so the analysis is tight wherever the two suprema coincide. The interpretation of $\tau$ is how soft the capacity is: the bound degrades exactly as the overage cost dominates candidate values.

The result is proved in the paper; nothing in this mission is open mathematics. To our knowledge none of it has been machine-checked. A complete development would give the platform an overbooking-type stochastic selection model with an exact expected reward, an LP benchmark, and the truncated-Poisson constant that recurs in prophet-inequality and online-matching analyses (the $k$-uniform correlation gap of Yan 2011). Proposition EC.2 and the monotonicity of $\mathbb E[\min\{\mathrm{Pois}(x),k\}]/x$ are reusable on their own.

Difficulty

The obvious argument compares the algorithm's random number of hires with the LP's expected number and loses everything to the overage term: the LP pays $[\mathbb E|A|-k]^+$, the algorithm pays $\mathbb E[|A|-k]^+$, and Jensen's inequality points the wrong way. The gap must be controlled by a sum of independent Bernoulli variables against a Poisson variable of the same mean, uniformly over how the mass is spread across candidates. A second difficulty is the regime $P_{\mathrm{high}}>k$, where the LP optimum deliberately exceeds capacity; a direct bound there does not reduce to the first case, and the paper's reduction (Lemma 14) changes the instance rather than the algorithm. Tie cases $v_i=1$ make the LP optimum non-unique, which the formal statements must handle explicitly.

Formalization scope

Candidates are Fin n (0-based), all quantities are real. The sorted labelling $v_1\ge\dots\ge v_n$ is part of instance validity (Antitone I.v), as the paper assumes after relabelling; ties may be ordered arbitrarily. Every expectation is an explicit finite sum over the $2^n$ hire sets with independent probabilities $y'_ip_i$; there is no measure theory. The truncated Poisson mean is the series of the Poisson pmf. $\mathrm{LP}_{\mathrm{sim}}(I)$ is the supremum of the objective over the feasible set, which is the LP value; $\alpha^\tau_k$ is the supremum over $[0,1]$. $s^*$ is any maximiser of the $\alpha^\tau_k$ objective over $[0,1]$; one exists by continuity. A candidate with $p_i=0$ receives $y'_i=0$, which changes no reward.

The algorithm's reward is the exact expected reward of the run with independent offers, never the bound produced in the paper's proof, and the comparison is with the LP value at an optimal solution, not with the objective at an arbitrary feasible point; $\alpha^\tau_k$ is the supremum of the specific Poisson expression, not a free constant.

Two statements carry disclosed hypotheses, because the printed versions fail at ties: Lemma 12 assumes $v_i>0$, $v_i\ne1$, $p_i>0$, and Lemma 14 assumes $v_i\ne1$. Counterexamples are in the items' Formalization Notes. Theorem 3 and Lemma 13 need neither and hold for every optimal LP solution.

A complete development needs Poisson series manipulations (the closed form, concavity of $\lambda\mapsto\mathbb E[\min\{\mathrm{Pois}(\lambda),k\}]$), a Bernoulli-to-Poisson comparison for $\mathbb E\min\{\sum_iD_i,k\}$, and fractional-knapsack structure for the LP. Contributions of alternative proofs of any milestone, and of the Poisson facts as standalone results, are welcome.

Selected references

• B. Epstein, W. Ma, Selection and Ordering Policies for Hiring Pipelines via Linear Programming, arXiv:2210.04059v3 (2023); Operations Research (2024). https://arxiv.org/abs/2210.04059
• Q. Yan, Mechanism Design via Correlation Gap, Proceedings of SODA 2011, 710–719. https://doi.org/10.1137/1.9781611973082.56
• M. T. Goodrich, R. Tamassia, Algorithm Design: Foundations, Analysis, and Internet Examples, Wiley, 2001, Chapter 5 (fractional knapsack).