Motivation

The group Steiner tree problem generalizes the ordinary Steiner tree problem: given a rooted tree and several groups of vertices, find a minimum-cost subtree that connects at least one vertex of each group to the root. It is a canonical instance of the generalized-connectivity family this survey studies in Chapter 11 — a family that also contains the online set-cover problem (Chapter 5 of this series) as a special case. Buchbinder and Naor's chapter shows how to convert the celebrated offline randomized-rounding algorithm of Garg, Konjevod and Ravi [56] into an online one, by imitating its per-edge coupling structure one iteration at a time as the online fractional solution (obtained from this survey's own Chapter 4 framework) evolves. This mission formalizes that online rounding scheme's three defining probabilistic guarantees and the resulting competitive-ratio theorem.

Setting

Fix a rooted tree T = (V, E, r) with non-negative edge costs c : E → ℝ, and k groups g₁, …, g_k ⊆ V, each request (r, gᵢ) arriving online. An online covering algorithm (from Chapter 4's framework, applied to the LP relaxation of this connectivity problem) maintains a monotonically increasing fractional weight w : E → ℝ on the edges, reinterpreted so that wₑ is the maximum flow that can be routed through e to any vertex of its subtree — a technical substitution needed so weights are monotone non-increasing along any root-to-leaf path, the property the rounding algorithm requires. At the end of each iteration in which some weights are augmented from w to w' = w + δ, the rounding algorithm processes every edge e with δₑ > 0, in topological order starting from the root, and randomly decides whether to add it to a growing random edge-cover C ⊆ E: deterministically, if w'ₑ > 1; via a single coin flip, if e is incident to the root or its parent edge's inclusion in C is already certain; via a coin flip conditional on the parent edge already being in C, otherwise. Because a coin is only ever flipped for a child once its parent is (or is already known to be) in C, C always induces a connected subtree containing the root.

Formalization targets

Theorem 11.4 (the goal, p. 231): there is a randomized online algorithm for the group Steiner problem in trees with competitive ratio O(log²n log k), where n is the number of leaves. It is built by running T independent trials of the rounding scheme in parallel and taking the union of the resulting covers, for T chosen (this mission's own explicit derivation — the book gives only the narrative "we run O(log k log N) independent trials... using simple probabilistic analysis") so that every group fails to be covered with probability at most 1/(2k), while the union's expected cost stays at T · log(n) · OPT.

Three milestones, in attack order, each stated exactly as the book states it (p. 230-231), with the book's own caveat "we state the main lemmas and omit the proofs" preserved — no in-source proof exists for any of the three beyond the algorithm's own description, so each is left sorry with no invented proof strategy:

• Lemma 11.1: at the end of an iteration, ℙ[e ∈ C] = w'ₑ for every edge, and ℙ[e ∈ C] = 1 whenever wₑ > 1 already.
• Lemma 11.2: the expected cost of C is at most ∑_{e∈T} cₑ w'ₑ (linearity of expectation applied to Lemma 11.1).
• Lemma 11.3: for a group g of size at most N with total routable flow wg ≥ 1, the probability some vertex of g is covered is Ω(1/log N).

Significance

This is the survey's most involved application of the primal-dual framework: unlike Chapters 5, 9, 10 and 13, which round a single scalar decision per online step, the group Steiner algorithm must couple an entire iteration's worth of edge decisions so that the resulting random set stays a connected subtree — the coin-flip probabilities in the Algorithm box are exactly the minimal adjustment needed to keep marginal probabilities matching the fractional solution while preserving this connectivity invariant online. No formal development of the group Steiner problem (online or offline) was found on the platform as of 2026-09-20; this mission is the first.

Difficulty

Two distinct obstacles. First, faithfully representing "the probability that e ∈ C" for an online, coupled random process without assuming its proof: the mission represents the algorithm's random cover as an abstract finite probability distribution RandomCover E and states each lemma as an implication from the Algorithm box's three coupling rules (transcribed as hypotheses on marginal and conditional probabilities) to the claimed marginal or expected-value conclusion — capturing exactly what the book asserts without proof, rather than either assuming the conclusion trivially or constructing a full multi-iteration coupled process (which the source's own "we omit the proofs" indicates is genuinely nontrivial, citing [56]). Second, Theorem 11.4's own competitive ratio is stated in the book only asymptotically, with a purely narrative derivation ("we run O(log k log N) independent trials... we get a competitive ratio of O(log n log k log N)... probability at least 1 − 1/k") and no displayed formula anywhere in the chapter. Per this series' explicit-constants rule, this mission supplies its own explicit closed form for the number of trials T and the resulting bounds via a standard Chernoff/union-bound argument applied to Lemma 11.3's constant α; this derivation is the mission's own (documented below), not a transcription, since none exists in the source to transcribe.

Formalization scope

RandomCover E is a finite pmf p : Finset E → ℝ (Finset E itself finite since E is Fintype), with marg, condProb and expectedCost/probHits derived from it by ordinary Finset sums — no measure theory, since the sample space is always finite. RoundedTree E bundles parent : E → Option E (e(p)) and a non-negative cost. Lemma 11.3's wg (the flow routable to a group's vertices simultaneously) is left as hypothesis-supplied data rather than defined via an explicit max-flow formalization, which this mission's scope does not require (welcome contribution). Theorem 11.4's number of trials is the explicit closed form T = ⌈(log N · log(2k)) / α⌉, α the (existentially quantified, uniform) constant from Lemma 11.3; its coverage guarantee is 1 − 1/(2k) per group (this mission's own union-bound derivation), not the book's stated 1 − 1/k — the book reaches the stronger bound via an additional shortest-path fallback mechanism for any group the trials miss, which is out of scope here (welcome contribution, along with completing any of the four sorrys and formalizing Theorem 11.5's extension to general graphs via HST embedding, out of scope since it depends on an external embedding result not proved in this book).

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024
• N. Garg, G. Konjevod, R. Ravi. A polylogarithmic approximation algorithm for the group Steiner tree problem. Journal of Algorithms, 37(1):66-84, 2000 (cited as [56] in the survey).
• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor. A general approach to online network optimization problems. ACM Transactions on Algorithms, 2(4):640-660, 2006 (cited as [4], the source of this chapter's results per the Notes, p. 231).

Motivation

Section 4 of this survey derives a simple randomized $O(\log m \log n)$-competitive algorithm for the online set-cover problem, by rounding the fractional solution the online packing-covering framework produces. An intriguing question the survey poses next: can the same guarantee be achieved deterministically? The standard tool for removing randomness, the method of conditional expectations, requires finding a pessimistic estimator — a potential function whose value the algorithm can track and whose behavior certifies the randomized algorithm's guarantee step by step. Chapter 5 constructs exactly this potential function for the weighted online set-cover problem, and shows that greedily minimizing it online reproduces the randomized algorithm's competitive ratio with no randomness at all. This mission formalizes that construction: the potential function itself (Lemma 5.1) and the correctness guarantee it buys (Theorem 5.2).

Setting

Fix a finite universe of elements $E$ and a finite family of sets $T$ with positive costs $c_s$, both known to the algorithm in advance (only which elements will actually need covering, and in what order, is unknown). A monotonically increasing assignment $w : T \to \mathbb{R}$ of fractional weights to sets is produced online by a fractional subroutine (any $O(\log m)$- competitive online fractional algorithm — the survey's own Section 4.2 supplies one). An element's weight is $w_e := \sum_{s \mid e \in s} w_s$. Given a target $\alpha \ge c(C_{OPT})$ (a guessed upper bound on the optimal integral cover's cost — the survey handles an unknown optimum by doubling this guess across phases, outside this chapter's own scope), the algorithm maintains a chosen cover $C \subseteq T$ and the potential

where $n = |E|$ and $\chi_C$ is $C$'s characteristic function. Whenever a set $s$'s weight increases, the algorithm computes $\Phi$ both with and without adding $s$ to $C$ and chooses whichever keeps $\Phi$ from exceeding its value before the step (failing only if neither does, which Lemma 5.1 shows cannot happen when $\alpha \ge c(C_{OPT})$).

Formalization targets

Theorem 5.2 (goal, p. 139): given the invariant $\Phi < n^2$ that Lemma 5.1 maintains throughout a run, (i) every element of weight $\ge 1$ is covered, and (ii) the chosen cover costs at most $\alpha \cdot O(\log m \log n)$.

Lemma 5.1 (milestone, p. 137): the potential function never increases in expectation across a weight-augmenting step, under the algorithm's own randomized choice of whether to add the augmented set to the cover (the internal argument — via the method of conditional expectations — that certifies the deterministic algorithm's choice rule never fails).

Significance

This chapter answers, for the online set-cover problem specifically, a question that recurs throughout online algorithm design: when can a randomized guarantee be derandomized online? The potential-function technique here is the survey's own template for the answer (it recurs, per the chapter's Notes section, in the routing algorithm of Chapter 9 and the ad-auctions algorithm of Chapter 10, both formalized as separate missions in this series) — a self-contained, reusable instance of "derandomization via an explicit pessimistic estimator" in the online setting, distinct from the offline set-cover primal-dual and dual-fitting algorithms of this book's own Chapter 2, already on the platform (PrimalDualOnline.SetCover.*, checked below: a static instance with no arrival order and no potential function, a genuinely different model).

Difficulty

The central formalization challenge is that Lemma 5.1's own statement, "$\Phi_{end} \le \Phi_{start}$", denotes the potential's value in expectation under the algorithm's randomized choice — not a single deterministic before/after pair — since the lemma is proved via a probabilistic argument (adding $s$ to the cover with probability $1 - n^{-2\delta_s}$) whose role is purely internal to justifying the deterministic algorithm's rule (choose whichever of the two options controls $\Phi$). Stating the lemma as a bare inequality between two potential values, without the mixture, would either be false (the "add $s$" branch alone can increase $\Phi$) or would silently smuggle in the derandomized choice as a hypothesis rather than proving it is always available. This mission states the expectation explicitly as a probability-weighted average of the two branch potentials, matching the actual analytic content of the book's proof (equations 5.1-5.6) rather than its final one-line restatement.

Formalization scope

SetCoverInstance E T bundles elemSets : E → Finset T (the sets containing an element) and positive costs c. elementWeight and coveredBy are literal transcriptions of $w_e$ and "$e \in \bar C$". potential transcribes $\Phi$'s displayed formula verbatim, with n cast from Fintype.card E. potential_nonincreasing (Lemma 5.1) is the expectation inequality described above. algorithm_correctness (Theorem 5.2) takes the potential invariant Φ < n² as a hypothesis (the state Lemma 5.1, applied repeatedly from the initial value $\Phi < n^2$, is what the book's own proof shows every reachable state satisfies) together with an explicit ratio β standing for "the fractional solution is O(log m)-competitive" (∑ wₛcₛ ≤ βα) — the book imports this fact from Section 4 as a black-box subroutine rather than re-deriving a specific numeric constant in this chapter, and this mission does the same rather than re-deriving Chapter 4's own constant under the (different) $d \to m$ substitution the book's prose glosses over. The conclusion is then the fully explicit α · log n · (3β + 2), matching the book's own derivation (displayed inequality, p. 139-140) with O(log m) replaced by the parameter β. This correctly rules out the trivializing formalization in which the O(log m log n) bound is left as an unquantified existential constant, or in which Φ's invariant is assumed directly as an unmotivated free hypothesis rather than the fact Lemma 5.1 is what actually establishes. Reals throughout; Real.log, Real.exp, Real.rpow (via the ^ notation on reals) for the book's own log, exp and n^{2w_e}. Nothing here is reused from 04-framework (concurrent draft; per this series' own rule, drafts do not import drafts) even though this chapter's fractional subroutine is conceptually the same online covering framework — restated here only as the abstract ratio β, not as a Lean dependency. Welcome contributions: completing the two sorrys, and formalizing the doubling-across-phases wrapper (Section 5.1's "Obtaining a Deterministic Algorithm" discussion) that removes the need to know α ≥ c(C_OPT) in advance.

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024
• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor. The online set cover problem. STOC 2003 / SIAM J. Comput. 39(2), 2009 (cited by this book's Chapter 5 Notes as [3]).

Motivation

Reinforcement learning formalizes a scenario supervised learning cannot: an agent that actively interacts with an environment, choosing actions that change both the state it observes next and the reward it receives, rather than passively receiving an i.i.d. labeled sample. Every practical treatment of this scenario — from classical dynamic programming to modern deep reinforcement learning — is built on the Markov decision process (MDP), a model in which the effect of an action depends only on the current state, not on the full history that led to it. Two questions define the theory this mission covers: given a fixed way of acting (a policy), what value does it obtain, and how is that value actually computed rather than merely characterized as the solution of a fixed-point equation? Mohri, Rostamizadeh and Talwalkar's chapter 17 answers both for the stationary, infinite-horizon discounted case, and this mission targets its two central results: that a fixed policy's value is not just characterized but uniquely determined by a linear system with an explicit closed-form solution (Theorem 17.10), and that the optimal value function — obtained instead by choosing the best action at every state — can be computed by an iterative algorithm guaranteed to converge regardless of where it starts (Theorem 17.11).

Setting

A (finite) Markov decision process consists of a finite set of states $S$, a finite set of actions $A$, a transition kernel $P[s'\mid s,a]$ giving the distribution over the next state $s'$ after taking action $a$ at state $s$, and an expected reward $\mathbb E[r(s,a)]$ for that transition. A (stationary) policy $\pi:S\to\Delta(A)$ assigns each state a distribution over actions — possibly, but not necessarily, a point mass on a single action. Fixing $\pi$ turns the MDP into an ordinary Markov chain on $S$: at each step the agent is at some state $s$, draws $a\sim\pi(s)$, receives (expected) reward $\mathbb E[r(s,a)]$, and moves to a state drawn from $P[\cdot\mid s,a]$. For a discount factor $\gamma\in[0,1)$, the value of $\pi$ at $s$ is the expected discounted sum of future rewards starting from $s$,

and the state-action value function $Q_\pi(s,a)$ is the analogous quantity for taking $a$ at $s$ and then following $\pi$. Marginalizing the raw kernel and reward over the mixed action $\pi(s)$ gives the induced transition matrix $P_{s,s'}=P[s'\mid s,\pi(s)]=\sum_a \pi(s)(a) P[s'\mid s,a]$ and induced reward vector $R_s=\mathbb E[r(s,\pi(s))]=\sum_a\pi(s)(a)\,\mathbb E[r(s,a)]$ — the objects that turn $\pi$'s value into a genuinely linear-algebraic quantity. A policy $\pi^*$ is optimal if $V_{\pi^*}(s)\ge V_\pi(s)$ for every policy $\pi$ and every state $s$; write $V^*$ for its value function.

Formalization targets

Theorem 17.10 (goal). For a finite MDP and a fixed policy $\pi$, the matrix $I-\gamma P$ (with $P$ the policy-induced transition matrix) is invertible, and $\pi$'s value function is the unique solution of the Bellman equations, given in closed form by

Proposition 17.9 (milestone). The value function itself satisfies the linear system that Theorem 17.10 solves:

Theorem 17.7 (milestone). A policy $\pi$ is optimal if and only if it places probability only on $Q_\pi$-maximizing actions: for every $(s,a)$ with $\pi(s)(a)>0$, $a\in \operatorname{argmax}_{a'} Q_\pi(s,a')$.

Theorem 17.11 (milestone). The Bellman optimality operator $\Phi$, $[\Phi(V)](s)=\max_{a} \{\mathbb E[r(s,a)]+\gamma\sum_{s'}P[s'\mid s,a]V(s')\}$, is a $\gamma$-contraction for $\lVert\cdot\rVert_\infty$; consequently, for any starting vector $V_0$, the value-iteration sequence $V_{n+1}=\Phi(V_n)$ converges to a fixed point of $\Phi$.

Significance

Theorem 17.10 is what makes policy evaluation on a finite MDP an exact, finite computation rather than an infinite limit: instead of summing an infinite discounted series or solving an implicit fixed-point equation numerically, a single $|S|\times|S|$ matrix inversion gives the policy's value at every state simultaneously. It is also the base case every planning algorithm in the chapter builds on: policy iteration alternates optimizing a policy with exactly this evaluation step. Theorem 17.11 gives the complementary guarantee for the harder problem of finding the optimal value function directly, without fixing a policy first: value iteration converges from any starting point, with a convergence rate ($O(\log(1/\epsilon))$ iterations for $\epsilon$-accuracy) that follows from the same contraction argument. Together, the two results are the mathematical content behind why dynamic-programming planning for finite MDPs is tractable at all — the discount factor $\gamma<1$, not any structural assumption on rewards or transitions, is what buys both the uniqueness in Theorem 17.10 and the convergence in Theorem 17.11. Formalizing them requires reproducing this linear-algebraic and metric content precisely, not just asserting the conclusions: an invertibility claim asserted without the operator-norm argument, or a convergence claim without the contraction property, would state something true by fiat rather than the book's actual result. No faithful prior art exists on the platform for this exact model (see Formalization scope).

Difficulty

The obvious shortcut for Theorem 17.10 is to assert $I-\gamma P$ is invertible without proof — true, but not what the book does, and not informative about why it holds. The genuine content is that $P$, being row-stochastic (every row of $P$ sums to exactly $1$, since $\pi(s)$ and $P[\cdot\mid s,a]$ are both proper distributions), has operator norm $\lVert P\rVert_\infty=1$ exactly, so $\lVert\gamma P\rVert_\infty=\gamma<1$ strictly; this rules out $1$ as an eigenvalue of $\gamma P$, which is exactly what invertibility of $I-\gamma P$ requires. The same $\gamma<1$ fact, applied differently, drives Theorem 17.11: showing $\Phi$ is $\gamma$-Lipschitz requires bounding $\Phi(V)(s)-\Phi(U)(s)$ by comparing the maximizing action for $V$ against the same action's value under $U$ (not $U$'s own maximizer), since the two suprema need not be attained at the same action — a step easy to state incorrectly as a direct comparison of two maxima. Both theorems fail if $\gamma=1$ is allowed: the discounted setting's central asset, a strict contraction, disappears exactly at that boundary.

Formalization scope

States and actions are modeled as finite types (Fintype S, Fintype A); the raw kernel and reward P : S → A → S → ℝ, Er : S → A → ℝ are unconstrained functions, with IsTransitionKernel asserting the required distribution property explicitly rather than assuming it silently. A policy is π : S → A → ℝ with IsPolicy π asserting π s is a distribution over A for every s — deliberately not π : S → A or a PMF-valued function, since Theorem 17.7's own quantifier ("for any pair (s,a) with π(s)(a) > 0") requires treating π(s) as a genuine mixture. PolicyValue is defined as the actual infinite discounted expectation (via an explicit state-occupation-distribution recursion), not as the Bellman fixed point — so that Proposition 17.9 (the value function satisfies the linear system) and Theorem 17.10 (that system has a unique, invertible-matrix solution) are both non-vacuous claims about the same object, rather than one being definitionally true of the other. The trivializing formalization this rules out is asserting IsUnit (1 - γ • P) as a bare hypothesis, or defining V_π as (1-γP)⁻¹R and calling the resulting identity a theorem; both would erase the mission's actual content. Two platform modules model related MDPs (BertsekasSSPModel, a stochastic-shortest-path model with a termination-probability deficit rather than exact row-stochasticity, and FoundationsRL.RLBasics, a finite-horizon episodic model indexed by layer) — neither specializes exactly to this chapter's stationary, always-continuing, infinite-horizon discounted convention, so every definition here is drafted fresh rather than imported. This chunk covers §17.2–17.4.2 (the MDP model, policy value, Bellman's equations, value and policy iteration); §17.4.3 (the linear-programming formulation) and §17.5 (stochastic-approximation learning algorithms — TD(0), Q-learning, SARSA) are out of scope, since they require a stochastic-approximation convergence substrate this mission does not build.

Selected references

• Mohri, M., Rostamizadeh, A., and Talwalkar, A. Foundations of Machine Learning, 2nd ed., chapter 17. MIT Press, 2018.
• Bellman, R. Dynamic Programming. Princeton University Press, 1957.
• Puterman, M. L. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, 1994.

Motivation

The spectral gap of a quantum many-body Hamiltonian is the difference between the energy of its ground state and the energy of its first excited state, in the limit of infinitely many particles. Whether a given microscopic interaction produces a gapped or a gapless system decides much of the macroscopic physics: gapped systems have exponentially decaying correlations and well-defined quantum phases, gapless systems sit at critical points and can display algebraically decaying correlations. Several long-standing questions — the Haldane conjecture for antiferromagnetic spin chains, the existence of gapped topological spin liquids, and the Yang–Mills mass gap — are instances of the question "given the interaction, is the system gapped?".

Cubitt, Pérez-García and Wolf proved that this question, posed for families of two-dimensional translationally invariant nearest-neighbour spin models, admits no algorithmic answer: the spectral gap problem is undecidable (Nature 528, 207–211 (2015); full version: Forum of Mathematics, Pi 10:e14 (2022), also arXiv:1502.04573).

Timeline of the ingredients the proof rests on: Turing's undecidability of the halting problem (1936); Berger's undecidability of the domino problem (1966) and Robinson's aperiodic tile set (Inventiones 12, 177–209 (1971)); Feynman's and Kitaev's circuit-to-Hamiltonian constructions, which turn a computation into a ground state; Gottesman and Irani's translationally invariant one-dimensional Hamiltonians encoding computation (FOCS 2009); and Bitansky–Vadhan-style quantum Turing machine engineering from Bernstein and Vazirani (SIAM J. Comput. 26, 1411–1473 (1997)). The 2015 result was later sharpened to one-dimensional chains by Bausch, Cubitt, Lucia and Pérez-García (PRX 10, 031038 (2020)).

Setting

Fix a local dimension $d$ and, for each side length $L$, the square lattice $\Lambda(L)=\{1,\dots,L\}^2$ with open boundary conditions. Each site carries a copy of $\mathbb{C}^d$, so the state space of the lattice has the standard product basis indexed by assignments of a level in $\{1,\dots,d\}$ to each site. A model is specified by three Hermitian matrices: an on-site term $h_1$ of size $d\times d$, and two interactions $h_{\mathrm{row}},h_{\mathrm{col}}$ of size $d^2\times d^2$ acting on horizontally and vertically adjacent pairs. The Hamiltonian of the finite lattice is

the same three matrices being used at every edge and every site, which is what translational invariance means here. The quantity $\max\{\|h_1\|,\|h_{\mathrm{row}}\|,\|h_{\mathrm{col}}\|\}$ is the local interaction strength.

Write $\lambda_0(H^{\Lambda(L)})\le\lambda_1(H^{\Lambda(L)})\le\cdots$ for the eigenvalues and $\Delta(H^{\Lambda(L)})=\lambda_1-\lambda_0$ for the finite-size gap. The family $\{H^{\Lambda(L)}\}_L$ is

• gapped (Definition 1 of the source) if there are $\gamma>0$ and $L_0$ such that for all $L>L_0$ the ground state of $H^{\Lambda(L)}$ is non-degenerate and $\Delta(H^{\Lambda(L)})\ge\gamma$;
• gapless (Definition 2 of the source) if there is $c>0$ such that for every $\varepsilon>0$ there is an $L_0$ with: for all $L>L_0$, every point of $[\lambda_0,\lambda_0+c]$ lies within $\varepsilon$ of the spectrum of $H^{\Lambda(L)}$.

These two conditions are not negations of each other; the construction guarantees that every instance falls into one of them. The ground state energy density is $E_\rho=\lim_{L\to\infty}\lambda_0(H^{\Lambda(L)})/L^2$.

Formalization targets

Goal — Theorem 3 of the source

For a fixed universal machine and every $n$, one explicit family of interactions, built from fixed integer-valued matrices $A,A',B,C,D,D'$, a diagonal projector $\Pi$, a rational $\beta>0$ that may be taken arbitrarily small, and an algebraic $\alpha(n)\le 2\beta$,

with $\varphi=\varphi(n)$ the rational whose binary expansion after the point is the binary expansion of $n$ reversed, satisfies: the local interaction strength is at most $1$; if the machine halts on input $n$ the family is gapped with gap at least $1$; and if it does not halt the family is gapless. Since halting is undecidable, no algorithm decides gappedness, even with the promise that exactly one of the two alternatives holds and even at fixed local dimension $d$.

Milestones

The milestone list follows the numbering of the full version: Lemma 8 and Theorem 9 (reduction of halting to ground state energy and to arbitrary low-energy properties), Corollary 7 (the same undecidability for unconstrained local dimension, with rational interactions), Proposition 53 and Corollary 54 (the diverging ground state energy and its promise version), and Theorem 5 (undecidability of the ground state energy density).

Significance

The result rules out a general algorithm — and therefore any complete general method — for deciding gappedness from the interaction matrices, however much computing power is available; the property genuinely depends on arbitrarily large system sizes. It also implies, via the standard link between undecidability and independence, that there are concrete finite-dimensional models whose gap is independent of the axioms of any consistent recursively axiomatized formal system (Corollary 4 of the source), and it transfers to other low-energy properties such as the existence of algebraically decaying ground-state correlations.

The theorem is proved; none of it is formalized. This mission produces the machine-checked version. The reusable infrastructure it forces into existence is substantial on its own: a formal model of translationally invariant lattice Hamiltonians and their thermodynamic-limit spectral behaviour, the tiling layer, and computational-history-state Hamiltonians. Each milestone is a self-contained statement that can be attacked without the others.

Difficulty

The obvious approach — encode a halting computation as an energy penalty — gives the ground state energy of a finite lattice, not a property of the limit; this is exactly what Lemma 8 achieves, and it is not enough, because a gap is a statement about the sequence of spectra as $L\to\infty$ and is insensitive to any single lattice size. The construction must make the halting information visible at all sufficiently large sizes at once while a fixed finite local dimension carries every instance $n$. That forces three separate difficulties: an aperiodic (Robinson) tiling to create squares of every size $2^n$ inside one translationally invariant model; a quantum phase-estimation Turing machine whose transition amplitudes encode $n$ in a single phase $e^{i\pi\varphi(n)}$, so that the instance index does not inflate the local dimension; and a history-state Hamiltonian whose low-energy spectrum can be controlled well enough that a positive energy density in the halting case turns into a genuine spectral gap, and a vanishing one into a dense spectrum above the ground state.

Formalization scope

The development commits to the following conventions, all of which are visible in the definition items of this mission.

1. Lattices are finite: sites are pairs of indices in $\{0,\dots,L-1\}$, edges are consecutive pairs within a row or a column (open boundary conditions; the periodic case of Section 6.3 of the source is out of scope).
2. Operators are complex matrices indexed by product-basis configurations; the interactions are embedded by acting as the given matrix on the two sites of an edge and as the identity elsewhere.
3. The spectrum is taken as the set of real numbers in the matrix spectrum, and $\lambda_0$ is its infimum; every statement carries the Hermiticity hypotheses that make this the usual spectrum. Multiplicities are dimensions of eigenspaces, which is how the "identity of spectra as multisets" of Theorem 9 is expressed.
4. Gapped, gapless and the energy density are properties of the whole family $\{H^{\Lambda(L)}\}_L$ generated by a fixed triple of matrices, exactly as in Definitions 1 and 2.
5. Operator norms are $\ell_2$ operator norms; the local interaction strength is the maximum of the three.
6. Machines are represented by partial recursive codes: "halts on input $n$" is definedness of the evaluation, and "has not halted after $L$ steps" is the step-bounded evaluation returning nothing. The explicit local-dimension bounds of Lemma 8 and Theorem 9, which are stated in the source in terms of the number of internal states and the alphabet size of a Turing machine, are replaced by the existence of a finite local dimension.

Degenerate readings are excluded: a zero local dimension satisfies none of the statements, since a non-degenerate ground state requires a one-dimensional eigenspace and the gapless condition requires a non-empty spectrum; and every existential statement fixes the matrices before quantifying over all instances $n$ and all lattice sizes $L$.

Contributions are welcome at any milestone, and also on the infrastructure the milestones need — Wang tilings and the Robinson tile set, Gottesman–Irani history-state Hamiltonians, and quantum Turing machines in the Bernstein–Vazirani sense — which are needed for Theorem 6 and Lemma 47 of the source and are not yet part of this mission's item list.

Selected references

• T. S. Cubitt, D. Pérez-García, M. M. Wolf, Undecidability of the Spectral Gap (full version), Forum of Mathematics, Pi 10:e14, 1–102 (2022). https://doi.org/10.1017/fmp.2021.15 — the version all statements of this mission are formalized against; preprint: https://arxiv.org/abs/1502.04573
• T. S. Cubitt, D. Pérez-García, M. M. Wolf, Undecidability of the spectral gap, Nature 528, 207–211 (2015). https://doi.org/10.1038/nature16059
• R. M. Robinson, Undecidability and nonperiodicity for tilings of the plane, Inventiones Mathematicae 12, 177–209 (1971). https://doi.org/10.1007/BF01418780
• D. Gottesman, S. Irani, The quantum and classical complexity of translationally invariant tiling and Hamiltonian problems, FOCS 2009. https://arxiv.org/abs/0905.2419
• E. Bernstein, U. Vazirani, Quantum complexity theory, SIAM J. Comput. 26, 1411–1473 (1997). https://doi.org/10.1137/S0097539796300921
• J. Bausch, T. S. Cubitt, A. Lucia, D. Pérez-García, Undecidability of the spectral gap in one dimension, Phys. Rev. X 10, 031038 (2020). https://doi.org/10.1103/PhysRevX.10.031038

Motivation

Mission III of this series ends at an impossibility: without money, incentive compatibility over three or more alternatives means dictatorship. This mission formalizes the classical escape route — quasilinear utilities and payments — and the exact price of it. Vickrey (1961) discovered that a second-price auction makes truth-telling dominant; Clarke (1971) and Groves (1973) generalized the idea to arbitrary social choice: welfare-maximizing rules can always be made truthful by the right payments. The converse program — which choice rules are implementable at all — runs through Rochet (1987) and Myerson (1981) to Saks–Yu (2005): weak monotonicity characterizes implementability on convex domains, and on single-parameter domains the characterization is complete and elementary — monotone rules with critical-value payments. Chapter 9, §§9.3 and 9.5 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), written by Nisan, is the source text.

Setting

A set $A$ of alternatives and a finite set $\iota$ of players. Player $i$ holds a private valuation $v_i : A \to \mathbb{R}$ from a publicly known domain $V_i \subseteq \mathbb{R}^A$; utilities are quasilinear: choosing $a$ and charging $p_i$ gives $i$ utility $v_i(a) - p_i$. A (direct revelation) mechanism is a social choice function $f$ from valuation profiles to $A$ together with payment functions $p_i$ (Definition 9.14). The mechanism is incentive compatible if no unilateral misreport from the domain ever beats the truth (Definition 9.15).

A VCG mechanism (Definition 9.16) has $f$ maximizing social welfare $\sum_i v_i(a)$ and payments of the Groves form $p_i = h_i(v_{-i}) - \sum_{j\ne i} v_j(f(v))$; the Clarke pivot rule takes $h_i(v_{-i}) = \max_b \sum_{j \ne i} v_j(b)$. A rule is weakly monotone (Definition 9.28) if a unilateral change of valuation that moves the outcome from $a$ to $b$ satisfies $v_i'(b) - v_i'(a) \ge v_i(b) - v_i(a)$. A single-parameter domain (Definition 9.33) is given by a win set $W_i \subseteq A$ per player and bids $t \in [t_0, t_1]$: the valuation is $t$ on $W_i$ and $0$ elsewhere.

Formalization targets

Goal (capstone) — Theorem 9.36

A normalized mechanism (losers pay 0) on a single-parameter domain is incentive compatible iff the rule is monotone and every winning bid pays the critical value — the threshold below which the bid loses.

Theorem 9.17 — VCG is truthful

Every VCG mechanism is incentive compatible.

Lemma 9.20 — Clarke pivot

With Clarke pivot payments, a welfare-maximizing rule makes no positive transfers, and is individually rational when valuations are nonnegative.

Theorem 9.29 — weak monotonicity

Necessity: incentive compatibility forces WMON, on any domain. Sufficiency: on convex domains, WMON rules admit implementing payments (Saks–Yu).

Significance

These are the working theorems of every later mechanism-design mission: the approximation mechanisms of Chapter 12, the profit-maximization results of Chapter 13, and the sponsored-search analysis of Chapter 28 all argue through Theorem 9.36's monotonicity-plus-critical-value normal form, and VCG is the benchmark they approximate. Formalizing the cluster produces the platform's quasilinear-mechanism vocabulary — domains, truthfulness, Groves payments, weak monotonicity, single-parameter settings — on top of the social-choice layer of Mission III.

The capstone and Theorem 9.17 are textbook results with complete proofs in the source; the Saks–Yu half of Theorem 9.29 is stated but not proved in the book ("quite involved"), so that milestone carries a genuinely hard formalization with a published paper proof. None have prior Lean formalizations.

Difficulty

Theorem 9.17 is a three-line inequality chase once the Groves form is unfolded — a deliberate warm-up. Lemma 9.20 adds the attained maximum over a finite alternative set. The necessity half of 9.29 is a two-application argument; the sufficiency half is the hard point of the mission: the known proofs walk two-cycle inequalities into a path-integral construction of payments on a convex domain, and nothing of the kind exists in Mathlib. For the capstone, the delicate part is the critical value: the book defines it as a supremum that "is undefined" when the player always wins, and the honest formal rendering — a constant payment c that is a least upper bound of the losing bids whenever losing bids exist — makes the case split explicit; the equivalence proof must thread monotonicity, the threshold structure of the winning set, and normalization through both directions.

Formalization scope

Valuations are functions A → ℝ; domains are sets V i : Set (A → ℝ); mechanisms are total functions with every property quantified only over profiles from the domain, so behavior on invalid inputs carries no content. The Groves term hᵢ is a function of the full profile constrained to be invariant under changes of coordinate i — the standard rendering of "depends only on $v_{-i}$". The Clarke payment uses a Finset.sup' over a finite nonempty A, so no junk supremum arises. In the single-parameter setting the valuation induced by a bid is Set.indicator, bids live in Set.Icc t0 t1 with t0 ≤ t1, and the critical value is characterized by IsLUB guarded by nonemptiness of the losing set — the book's "undefined" caveat made precise without a junk sSup. Weak monotonicity's sufficiency half carries Convex ℝ (V i) and finite A (the Saks–Yu setting); the necessity half deliberately carries no hypotheses beyond incentive compatibility itself.

Selected references

• W. Vickrey, Counterspeculation, auctions, and competitive sealed tenders, J. Finance 16 (1961), 8–37. DOI
• E. H. Clarke, Multipart pricing of public goods, Public Choice 11 (1971), 17–33. DOI
• T. Groves, Incentives in teams, Econometrica 41 (1973), 617–631. DOI
• M. Saks, L. Yu, Weak monotonicity suffices for truthfulness on convex domains, Proc. 6th ACM EC (2005), 286–293. DOI
• N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 9, §§9.3, 9.5. DOI

AI generated, I think it's correct

Motivation

The matrix-multiplication exponent measures the asymptotic arithmetic cost of multiplying square matrices. A bound $\omega<c$ means that, over the field under consideration, $n\times n$ matrices can be multiplied in $O(n^{c+\varepsilon})$ field operations for every $\varepsilon>0$. Matrix multiplication is a central benchmark in algebraic complexity and a basic subroutine in linear algebra, graph algorithms, and symbolic computation.

The Coppersmith--Winograd tensor and the laser method produced the strongest bounds on $\omega$ for several decades. The 1990 tensor-square analysis gave $\omega<2.375477$. Later analyses of larger powers improved the numerical bound, but they organized their recursion through values assigned independently to constituent tensors. Duan, Wu, and Zhou identified a loss in that organization: several fine constituents that can coexist inside one coarse block may be counted as though they had to be selected independently. Their asymmetric-hashing framework partially compensates for this combination loss. The paper's full second-power specialization improves the best bound obtainable from the square of the Coppersmith--Winograd tensor to $\omega<2.374631$; see Section 6.3 and its parameter Table 2 in Duan--Wu--Zhou.

This mission isolates that second-power result. It is smaller than the paper's record-setting eighth-power calculation, but it contains the genuinely new asymmetric-hashing and hole-repair mechanisms in their first complete form. It therefore provides a focused bridge from the existing formalization of the classical $2.375477$ square analysis to later combination-loss methods.

Setting

For a field $K$, the matrix-multiplication tensor

encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix. A restriction applies one linear map to each tensor leg, while a degeneration permits polynomial families of such maps and takes their first nonzero coefficient. A degeneration from the diagonal tensor $I_r$ gives a border-rank upper bound of $r$.

The Coppersmith--Winograd tensor with parameter $q$ is

It has border rank at most $q+2$. Its coordinate partition has six supported types, and the square $CW_q^{\otimes2}$ has fifteen coarse constituent types $(i,j,k)$ with $i+j+k=4$. A large tensor power contains many blocks with prescribed joint and marginal type distributions. The laser method retains blocks whose variables are disjoint and interprets their direct sum through Schönhage's asymptotic sum inequality.

Duan--Wu--Zhou refine this organization by also retaining a split distribution for the fine indices inside each coarse constituent. Coarse $X$- and $Y$-blocks are made unique, while compatible coarse triples may initially share a $Z$-block. The resulting partially damaged constituent tensors are described as broken copies of a standard-form tensor. The formal target uses $q=6$, the full Section 6 construction, and the paper's released second-power parameters.

Formalization targets

Goal: the full second-power asymmetric-hashing bound

For every field $K$,

The source reports the stronger numerical endpoint $2.374631$, so the displayed rational inequality has strict slack. The Lean declaration has exactly the same field quantification and uses exactly the same matMulExp definition as the existing Coppersmith--Winograd $2.376$ mission; only the theorem name and rational endpoint change.

Source-level milestones

The mission first isolates the available-block shuffling interface extracted from Definitions 5.3--5.5 and Claims 5.8--5.10, then formalizes the finite covering core of the Hole Lemma 5.6. The subsequent tensor realization by zeroing and identification, the multiple-copy Corollary 5.11, the compatibility-rate identity of Lemma 6.7, the probabilistic part of Claim 6.8, and the global restricted-splitting value inequality in Equation (25) remain visible structural leaves rather than being hidden inside scalar assumptions. The numerical milestone instantiates Equation (25) with the exact $q=6$ data of Section 6.3 and Table 2 and checks a strict value surplus at $\tau=23747/30000$. The structural proof must also make explicit the conversion from the paper's six-symmetrized value to a direct HasTauValueAtLeast witness for the mode-symmetric CW square. The final bridge applies the existing tau-value/rank machinery and transfers the Strassen-preorder exponent bound to matMulExp.

Significance

The mathematical result gives the first improvement over the classical Coppersmith--Winograd number while continuing to use only the tensor square. It separates improvement of the tensor analysis from improvement obtained merely by moving to a much higher tensor power. The same standard-form and restricted-splitting language is then reused by the paper's higher-power algorithm, which reports $\omega<2.371866$.

For formalization, the mission adds reusable infrastructure for nested tensor partitions. Existing CW-square work records coarse support types and actual matrix-multiplication restrictions. This mission extends that layer with fine split distributions, compatibility between levels, broken-block bookkeeping, and repair of holes without replacing tensor statements by unverified scalar values. Those definitions are prerequisites for later asymmetric-hashing, complete-split, and more-asymmetry analyses.

The bound is known mathematically and was published at FOCS 2023. The open work is a machine-checked reconstruction. The underlying CW tensor, border-rank certificate, canonical tensor-square grading, Salem--Spencer sets, direct-sum tau-value notion, asymptotic sum inequality, and exponent equivalence already exist on Prove2Me. The new frontier is the cross-level combination-loss analysis and its exact numerical specialization.

Difficulty

The central difficulty is that coarse and fine decompositions cannot be optimized independently. Two coarse triples may share a $Z$-block, and a fine $Z$-block can be useful for one triple, compatible with several, or removed by a collision. Counting all locally valuable fine constituents therefore does not certify a direct sum. Conversely, requiring every coarse $Z$-block to be unique discards precisely the combinations that produce the improvement.

The Hole Lemma must also preserve the actual tensor. A broken copy lacks some fine variable blocks; combining several such copies is useful only when a degeneration covers every required block with controlled loss and does not duplicate monomials. On the numerical side, the same-marginal maximum-entropy term and restricted-splitting values must be bounded with certified real inequalities. Floating-point output from MATLAB is evidence for a witness, not a Lean proof.

Formalization scope

The mission uses the existing TensorObj, MMObj, restriction, degeneration, asymptotic-rank, HasTauValueAtLeast, matMulExp_strassen, and matMulExp declarations in environment 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e. Top-level results quantify over an arbitrary field. Finite supports and block indices are represented by finite types; probability and split distributions are nonnegative real functions of total mass one; entropy and numerical optimization live in the reals.

The formalization is restricted to $CW_6^{\otimes2}$ for the capstone, although generic definitions and source lemmas may quantify over levels and finite index types. A valid proof must connect scalar rate inequalities to witnessed restrictions or degenerations yielding direct sums of concrete matrix-multiplication tensors. A constant-valued surrogate for the restricted-splitting value, a hypothesis that already assumes the desired exponent bound, or a certificate definition containing its own conclusion is outside scope.

Contributions are welcome for standard-form tensor encodings, finite permutation arguments, hole repair, type and split counting, entropy maximization certificates, certified logarithm and power inequalities, and the final tau-value/rank assembly. Statements should identify the corresponding definition, lemma, claim, equation, or table in the source.

Selected references

• Ran Duan, Hongxun Wu, and Renfei Zhou, Faster Matrix Multiplication via Asymmetric Hashing, 64th IEEE Symposium on Foundations of Computer Science (FOCS), 2023. arXiv:2210.10173 and released verification code.
• Don Cop persmith and Shmuel Winograd, Matrix Multiplication via Arithmetic Progressions, Journal of Symbolic Computation 9, 1990, pp. 251--280. DOI 10.1016/S0747-7171(08)80013-2.
• Arnold Schönhage, Partial and Total Matrix Multiplication, SIAM Journal on Computing 10(3), 1981, pp. 434--455. DOI 10.1137/0210032.

A continuous piecewise linear (CPWL) function is one assembled from finitely many flat pieces glued along flat seams. Every ReLU network computes such a function, and every such function is computed by some ReLU network. Questions about how deep a network must be are therefore questions about the internal structure of CPWL functions.

In 1993 Breiman built such functions from hinges: maxima of two affine maps. Sums of hinges approximate anything, but from two dimensions up they fail to represent most CPWL functions exactly. Wang and Sun (2005) widened the maxima, proving that every CPWL function on ℝⁿ is a signed sum of maxima of at most n+1 affine maps. Twenty years on it remains the workhorse structural fact, reducing any question about a network to a question about a single max gate and underpinning every known upper bound on the depth of exact representation.

That includes the newest one: at STOC 2026, Bakaev et al disproved the short standing conjecture that ⌈log₂(n+1)⌉ hidden layers are necessary, showing ⌈log₃(n−1)⌉+1 suffice. In this mission we deliver a machine-checked proof of the Wang and Sun theorem so future formalizations of network expressivity can invoke it rather than reprove it. Note that we take as given the lattice representation of Tarela and Martínez, independently proved by Ovchinnikov, which writes any CPWL function as a max of mins of its affine pieces. That is the one external ingredient the argument consumes, and our definition of CPWL builds it in.

Nearly every measure of Boolean function complexity was known to be equivalent — except sensitivity. Proving the conjecture unified the whole picture.

Motivation

A polynomial threshold function makes a Boolean decision by evaluating a real polynomial and keeping only its sign. Its average sensitivity measures how often that decision changes after one uniformly chosen input coordinate is reversed, summed over all coordinate choices. This is a basic quantitative question in the analysis of Boolean functions: how much can a low-degree decision rule vary across the edges of the Boolean cube?

The result collected here is a uniform bound with an explicit coefficient. The OpenAI weighted-grading development supplies a complete coefficient-eight construction. Lagdive, Aglave and Damre sharpen its probability estimate and obtain the sufficient coefficient 3.83. The present fixed-source development formalizes the refined estimate, extracts the coefficient 3.762, and connects it to the full polynomial-threshold statement.

This mission organizes that completed result and its reusable supporting theorems. Its goal and both milestones already have accepted Lean proofs. It does not present the coefficient as optimal, and it makes no claim of exhaustive historical priority.

Setting

Let $n,d$ be positive integers, and let $p$ be a real polynomial in $n$ variables with total degree at most $d$. Choose an input $x$ uniformly from the sign cube $\{-1,1\}^n$. For a coordinate $i$, write $x^{\oplus i}$ for the same input with coordinate $i$ negated. The threshold convention is

In particular, a zero of the polynomial is assigned the positive sign. The average sensitivity is

For the scalar supporting statements, let $B_n$ have the symmetric binomial distribution with parameters $n$ and $1/2$. Its mean absolute deviation is

The accompanying definition module fixes this finite sum and the normalized central coefficient $c_k=4^{-k}\binom{2k}{k}$. These definitions contain no estimates or unproved hypotheses.

Formalization targets

Goal — the coefficient 3.762 for arbitrary real polynomials

For every $n,d\ge1$ and every real polynomial of total degree at most $d$, prove

The goal is the published theorem AverageSensitivity.polynomial_bound_3762_general. It has no multilinearity hypothesis and no requirement that $d\le n$. The narrower range $1\le d\le n$ used by the Big O board is therefore included. The goal's fixed coefficient records this particular verified result; a future sharper coefficient would be a separate statement.

Milestone 1 — the refined finite one-sided coupling estimate

Let a finite set carry nonnegative probability weights $w$, and let real functions $U,V$ have identical weighted distributions. Let $m$ be any real centre and let $a\ge0$. If $V-U\le a$ on the support of the weights, prove

This is the finite form of the first estimate in Lemma 2 of Lagdive, Aglave and Damre. The centre is arbitrary; independence, exchangeability and a two-sided displacement bound are not hypotheses. Its published formalization is already proved.

Milestone 2 — exact extraction of the universal coefficient

For positive integers $n,d$ and a real number $A$, prove the scalar implication

This is AverageSensitivity.extract_constant. Its statement is independent of the polynomial and matrix constructions. It records the coefficient extraction proved in this development, rather than attributing 3.762 to the earlier paper.

Significance and current status

The result gives one coefficient that works simultaneously for every positive dimension and degree. Such uniformity distinguishes it from estimates that hold only for a fixed degree or only as the dimension tends to infinity. It also preserves the stated convention at polynomial zeros, so the class of threshold functions is unchanged at the boundary.

The formal contribution is a complete connection from the polynomial and the actual finite cube to the numerical bound. The final theorem does not assume the existence of a grading, an energy bound, a coupling estimate or a small-dimension certificate. Those mathematical components are discharged inside the proof chain. The two supporting milestones are independently importable results, and the live dependency graph records both as actual prerequisites of the goal's accepted reduction.

All three theorem nodes are currently Proved. The closed repository proof was rebuilt with Lean 4.33.1 and the platform's Mathlib revision, and an independent Linux build also passed. The final theorem's axiom dependencies are exactly propext, Classical.choice and Quot.sound. These checks establish the formal result under the displayed definitions; they do not establish optimality of the coefficient or independent human peer review.

Difficulty

A one-sided bound on the difference of two variables does not by itself bound the difference in the opposite direction. The equal-distribution condition is therefore essential to the coupling milestone. Omitting it would change the problem into a false assertion. In the polynomial application, the relevant distributions also have to come from the actual block masses of the constructed grading; treating those masses or the grading properties as free assumptions would omit the central analytic work.

The constant extraction must cover all admissible dimension-degree pairs. A calculation for finitely many dimensions cannot establish the universal statement, while an asymptotic first-moment estimate can leave uncontrolled small dimensions or degree-dependent errors. The formal target includes both the infinite range and every exceptional finite case. Numerical optimization and floating-point experiments are not premises of the accepted result.

Formalization scope

Cube vertices are functions Fin n → Bool, interpreted coordinatewise as signs. A coordinate flip is an explicit function update, and each probability is a finite cardinality divided by $2^n$. The polynomial is a Mathlib MvPolynomial (Fin n) ℝ; the degree bound refers to its total degree. General polynomial inputs are included through a proved value-preserving, degree-nonincreasing multilinearization. Positive dimensions ensure the normalizing denominator is nonzero. Degree zero and dimension zero are outside the displayed goal's quantifiers.

The two definition references provide the original cube/threshold interface and the exact scalar moment interface. The coupling milestone uses finite weighted sums, so equality of distributions is stated for every real test function without additional measurability assumptions. The scalar milestone quantifies over an arbitrary real $A$ satisfying its two explicit upper bounds. The main goal has no analogous auxiliary assumptions.

This is a Research Paper mission for a completed fixed-source development, with the main theorem and both milestones linked by their existing identities. It creates no duplicate theorem statements. Alternative proofs and subsequent sharper bounds can reuse these interfaces, but they are not claimed as completed by this mission. The construction and earlier probability refinement remain attributed to their original sources. Proof development and source preparation used OpenAI Codex.

Selected references

• OpenAI, Average sensitivity of polynomial threshold functions, preprint and Lean source, 2026. Fixed Lean development.
• Prathmesh Lagdive, Vaibhav Aglave and Suraj Damre, An elementary improvement of the average sensitivity bound for polynomial threshold functions, 2026, Lemma 2 and the dimension-degree estimate. Fixed manuscript source.
• Anchen0823, Average sensitivity: a Lean proof with coefficient 3.762, source development, 2026. Verified source revision. Prove2Me accepted main submission: 0f539328-c783-4509-a78e-a86ac777468c.

Why offer sets with overbooking matter

A firm with $k$ open positions often cannot interview and offer sequentially: hiring seasons are short, and offers go out in one batch. Some recipients decline, so the firm overbooks, sending more offers than it has positions, and pays for every hire beyond capacity. The same trade-off appears in airline and hotel overbooking and in university admissions. Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024) study this Simultaneous Offering problem as one of three hiring-pipeline models, and analyse the natural class of value-ordered policies, which offer to the best candidates first. Their Theorem 3 shows that a value-ordered policy built from a linear-programming relaxation guarantees a fraction $\alpha^\tau_k$ of the optimum when every value is at least $\tau$. This mission formalizes the converse, Theorem 4: no value-ordered policy can guarantee more than $\beta^\tau_k$.

Setting

An instance has $k \ge 1$ positions and $n \ge k$ candidates. Candidate $i$ accepts an offer with probability $p_i \in [0,1]$, independently of the others, and then adds value $v_i \ge 0$. The firm chooses a set $S$ of candidates and sends all offers at once. If $A \subseteq S$ is the random set of acceptances, the reward is

so each hire beyond capacity costs $1$ (the paper rescales values so that this cost is $1$). Write $R(I, S)$ for the expected reward of offering to $S$, and $\mathrm{OPT}_{\mathrm{sim}}(I) = \max_S R(I, S)$ for the best expected reward; randomizing over offer sets cannot do better.

Candidates are labelled so that $v_1 \ge v_2 \ge \cdots \ge v_n$. A value-ordered policy with parameter $m \in [n]$ offers to $\{1, \dots, m\}$. An instance is $\tau$-bounded, $I \in \mathcal{I}^\tau_{\mathrm{sim}}$, if $v_i \ge \tau$ for all $i$. Without such a bound value-ordered policies can be arbitrarily poor (§6.1); $\tau$ measures how soft the capacity is, from nearly hard ($\tau$ close to $0$) to nearly compensated by any hire ($\tau$ close to $1$), and both theorems take $\tau \in (0,1)$.

For $\lambda \ge 0$ let $\mathbb{E}[\min\{\mathrm{Pois}(\lambda), k\}]$ be the mean of a Poisson variable truncated at $k$, and