1. Motivation

Wikipedia's pages on open problems are, for many mathematicians, the first contact with a conjecture: a one-paragraph statement, a short history, a list of partial results. The Formal Conjectures library (Google DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the conjectures can be attacked — and, just as importantly, stated unambiguously — by machine.

This mission ports a coherent slice of that material to Prove2Me. It is deliberately a portfolio mission: the goal theorem is the Bateman–Horn conjecture, the strongest single statement in the collection, and the milestone list gathers the other conjectures and the landmark theorems that surround them. Some milestones are genuine steps toward the goal (the Bunyakovsky conjecture is literally the one-polynomial case); most are independent open problems from other fields, grouped here because they share a source, a level of difficulty, and a need for faithful formal statements. A reader should not assume that proving a milestone advances the goal theorem. The mission's value is that every statement in it has been written against the same Mathlib revision, checked to compile, and documented well enough to be attacked.

A rough timeline of the collection's landmarks:

• 1947 — Mills: a real $A>1$ with $\lfloor A^{3^n}\rfloor$ always prime.
• 1962 — Radó: the busy beaver function outgrows every computable function.
• 1971 — Davies: planar Kakeya sets have Hausdorff dimension $2$.
• 1978 — Apéry: $\zeta(3)$ is irrational.
• 1985 — Read (after Enflo, 1981): an operator on $\ell^1$ with no nontrivial closed invariant subspace.
• 2001 — Zudilin: one of $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational.
• 2002 — Mihăilescu: $8$ and $9$ are the only consecutive perfect powers (Catalan's conjecture).
• 2009 / 2021 — Dvir; Bukh–Chao: the finite-field Kakeya bound and its sharp density constant.
• 2021 — Gardam: Kaplansky's unit conjecture is false (its zero-divisor and idempotent companions remain open).
• 2024 — Saito: Mills' constant is irrational; bbchallenge: $\mathrm{BB}(5)=47\,176\,870$.
• 2025 — Wang–Zahl: the Kakeya set conjecture in $\mathbb{R}^3$.

2. Setting

The goal theorem concerns prime values of polynomials. Fix a finite set $S=\{f_1,\dots,f_k\}\subseteq\mathbb{Z}[X]$ of distinct polynomials. Say that $f$ satisfies the Bunyakovsky condition if its leading coefficient is positive, $\deg f\ge 1$, and $f$ is irreducible over $\mathbb{Z}$; say that $S$ satisfies the Schinzel condition if for every prime $p$ there is an integer $n$ with $p\nmid f_1(n)\cdots f_k(n)$ — i.e. no fixed prime divides the product at every argument.

For a prime $p$ let $\omega_p(S)$ be the number of residue classes $n \bmod p$ at which some $f_i$ vanishes, let $D=\prod_i \deg f_i$, and let

$$\pi_S(x)=\#\{\,n\le x : |f_i(n)| \text{ is prime for every } i\,\}.$$

The Bateman–Horn constant is the (conditionally convergent) Euler product

$$C=\lim_{N\to\infty}\ \prod_{p<N}\Big(1-\tfrac1p\Big)^{-k}\Big(1-\tfrac{\omega_p(S)}{p}\Big).$$

The other groups use their own vocabulary, each fixed in a definition item of this mission: Kakeya sets in $\mathbb{R}^n$ and over $\mathbb{F}_q$; Mills' property $\lfloor A^{3^n}\rfloor \in \mathbb{P}$; Wagstaff primes and Catalan–Mersenne numbers; polynomial self-maps and their Jacobian matrix; nontrivial closed invariant subspaces; linear extensions of a finite poset; Catalan's constant; and an explicit two-symbol Turing machine model with its maximum-shifts function $\mathrm{BB}$.

3. Target

The goal theorem is the Bateman–Horn asymptotic: under the Bunyakovsky and Schinzel hypotheses, $C$ exists and is positive and

$$\pi_S(x)\ \sim\ \frac{C}{D}\,\frac{x}{(\log x)^{k}}\qquad (x\to\infty).$$

Weaker statements in the same direction appear as milestones, first of all Bunyakovsky's conjecture: under the same hypotheses with $k=1$, $f$ takes prime values infinitely often. The remaining milestones are listed in the milestone panel and are grouped by subject: Diophantine equations (Brocard, Pillai, Lebesgue–Nagell, Catalan/Mihăilescu), Mersenne-type primality (New Mersenne, infinitude of Mersenne primes, Catalan–Mersenne), prime-representing constants (Mills), geometric measure theory (Kakeya in $\mathbb{R}^n$, Kakeya over $\mathbb{F}_q$, Falconer), operator theory (invariant subspace problem and Read's $\ell^1$ counterexample), group algebras (Kaplansky's zero-divisor and idempotent conjectures), affine algebraic geometry (the two-variable Jacobian conjecture), irrationality and transcendence ($\zeta(5)$, all odd zeta values, Zudilin's theorem, $e+\pi$, $e\pi$, $\gamma$, Catalan's constant), order theory (the $1/3$–$2/3$ conjecture), and computability (Radó's theorem).

4. Significance

The results themselves. Bateman–Horn is the quantitative form of Schinzel's hypothesis H: it contains the twin prime conjecture, the infinitude of primes of the form $n^2+1$, and Bunyakovsky as special cases, and it is the standard heuristic behind prime-counting predictions. The other targets are each the headline question of their area: whether every bounded Hilbert-space operator has an invariant subspace; whether group algebras of torsion-free groups are domains; whether Kakeya sets must have full dimension. The solved milestones (Mihăilescu, Davies, Dvir, Zudilin, Read, Saito, Radó) are landmarks whose formal proofs would be significant library contributions in their own right.

Formalizing them. None of the open statements is expected to fall here; the concrete deliverable is a set of faithful, compiling, reusable statements plus formal proofs of the solved milestones, most of which are not in Mathlib today. Several are realistically in reach: the finite-field Kakeya bound (Dvir's polynomial method is short), the elementary fact that $\pi+e$ and $\pi e$ cannot both be algebraic, and Radó's diagonal argument.

5. Difficulty

For Bateman–Horn, the obstruction is visible already for $k=1$, $\deg f = 2$: sieve methods bound $\pi_S(x)$ from above by a constant times the conjectured main term and produce almost-primes, but the parity problem blocks every known sieve from producing a single prime value of an irreducible quadratic. The conditional convergence of the Euler product is a second, smaller trap: the product over $p<N$ must be taken in order, so any reformulation as an unordered infinite product changes the statement.

Each other group has its own obstruction, and they do not transfer: the parity problem says nothing about Kakeya, where the difficulty is that dimension is not stable under the natural compactness arguments, nor about the invariant subspace problem, where the known counterexamples on $\ell^1$ show that no soft argument can work.

6. Formalization scope

Conventions this mission commits to, all fixed in the definition items:

• Polynomials are elements of ℤ[X]; primality of a polynomial value is primality of its absolute value, and the counting function ranges over natural numbers $n \le \lfloor x\rfloor$.
• The Bateman–Horn constant is the limit of the ordered partial products over $p<N$, not an unordered infinite product.
• Kakeya sets carry no compactness or measurability hypothesis, matching the source; the conjecture is stated as an equality of Hausdorff dimensions in $[0,\infty]$.
• Falconer's hypothesis is written $d < 2\dim_H E$ to avoid division in $[0,\infty]$.
• Torsion-freeness of a group is spelled out as "every element of finite order is the identity", which is the hypothesis the source intends (it is weaker than Mathlib's IsMulTorsionFree).
• Linear extensions are order-preserving bijections onto $\{0,\dots,|P|-1\}$, and probabilities are quotients of set cardinalities in $\mathbb{Q}$.
• The busy beaver model is an explicit $n$-state, $2$-symbol machine with a bi-infinite Boolean tape; $\mathrm{BB}$ counts transitions performed (maximum shifts), the halting transition included, and $\mathrm{BB}(0)=0$.
• Several source statements are phrased as "is $X$ true?" with an unknown answer. Prove2Me statements must be definite, so each such question is recorded in its affirmative form (e.g. "$e+\pi$ is irrational"); a solver who can refute one should submit a disproof. The one question with no statable answer, "what is $\mathrm{BB}(6)$?", is replaced by Radó's growth theorem rather than guessed at.
• Nothing here is vacuous: each hypothesis set is satisfiable (e.g. closed unit balls are Kakeya sets, and $X^2+1$ satisfies the Bunyakovsky and Schinzel conditions).

Contributions welcome: proofs of the solved milestones; sharper variants; and additional faithful statements from the same source library, which contains far more than fits in one mission.

7. Selected references

• P. T. Bateman and R. A. Horn, A heuristic asymptotic formula concerning the distribution of prime numbers, Math. Comp. 16 (1962), 363–367. DOI
• T. Radó, On non-computable functions, Bell System Tech. J. 41 (1962), 877–884. DOI
• R. O. Davies, Some remarks on the Kakeya problem, Math. Proc. Cambridge Philos. Soc. 69 (1971), 417–421. DOI
• C. J. Read, A solution to the invariant subspace problem on the space $\ell_1$, Bull. London Math. Soc. 17 (1985), 305–317. DOI
• K. Falconer, On the Hausdorff dimensions of distance sets, Mathematika 32 (1985), 206–212. DOI
• W. Zudilin, One of the numbers $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational, Russian Math. Surveys 56 (2001), 774–776. DOI
• P. Mihăilescu, Primary cyclotomic units and a proof of Catalan's conjecture, J. reine angew. Math. 572 (2004), 167–195. DOI
• Z. Dvir, On the size of Kakeya sets in finite fields, J. Amer. Math. Soc. 22 (2009), 1093–1097. DOI
• B. Bukh and T.-W. Chao, Sharp density bounds on the finite field Kakeya problem, Discrete Analysis 26 (2021). DOI
• G. Gardam, A counterexample to the unit conjecture for group rings, Ann. of Math. 194 (2021), 967–979. DOI
• K. Saito, Mills' constant is irrational, Mathematika 71 (2025), e70027. arXiv:2404.19461
• H. Wang and J. Zahl, Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions, arXiv:2502.17655
• Google DeepMind, Formal Conjectures, Apache-2.0, github.com/google-deepmind/formal-conjectures

---

Provenance note. The Lean statements in this mission are adaptations of the Formal Conjectures library (Apache-2.0), rewritten to depend only on Mathlib and on this mission's own definition items, and checked to compile against the platform's Mathlib revision. Each draft item carries a read-back; those read-backs are non-blind — they were written by the same agent that drafted the statements, and each says so in its first line. They are documentation, not independent testimony.

Motivation

The $k$-server problem was introduced by Manasse, McGeoch, and Sleator (STOC 1988 / J. Algorithms 1990) as a common generalization of paging, weighted caching, and related sequential decision problems, and their $k$-server conjecture has since become the central open question of competitive analysis. The conjecture asserts that a single ratio — exactly $k$ — governs deterministic online server management on every metric space.

Timeline

• 1985. Sleator and Tarjan introduce competitive analysis — an online algorithm judged against the offline optimum on every input — for list update and paging, and ask for a theory of such guarantees.
• 1988–1990. Manasse, McGeoch, and Sleator introduce the $k$-server problem (STOC 1988; J. Algorithms 1990) and settle its extremes: no deterministic algorithm beats ratio $k$ on any space with more than $k$ points (Corollary 7), two servers admit a $2$-competitive algorithm (Theorem 5, algorithm RES), and $k$ servers on $k+1$ points admit a $k$-competitive one (Theorem 4, algorithm BAL). Section 8 poses the $k$-server conjecture, in the symmetric finite setting of the paper.
• 1990. Fiat, Rabani, and Ravid (FOCS 1990) give the first competitive ratio depending on $k$ alone — exponential in $k$, but finite on every metric space.
• 1991. Chrobak, Karloff, Payne, and Vishwanathan (SIAM J. Discrete Math.) prove the conjecture on the real line via Double Coverage; Chrobak and Larmore (SIAM J. Comput.) extend it to all tree metrics.
• 1995. Koutsoupias and Papadimitriou (J. ACM) prove the Work Function Algorithm is $(2k-1)$-competitive on every metric space — the breakthrough, and still the best general bound. Their Conjecture 1.1 fixes the conjecture's modern form: for every metric space there is an online algorithm with competitive ratio $k$.
• 1996. The same authors verify the conjecture on spaces of $k+2$ points via the dual 2-evader problem (Inf. Process. Lett. 57).
• 2004. Bartal and Koutsoupias prove the WFA itself is $k$-competitive on the line, weighted stars, and all spaces of $k+2$ points.
• 2021. Coester and Koutsoupias (ICALP) give a unifying potential for all known WFA analyses and push the frontier to the circle.
• 2023. Bubeck, Coester, and Rabani (STOC) refute the randomized analogue: no $o(\log^2 k)$-competitive randomized algorithm exists in general. The deterministic conjecture — this mission's goal — survives as the central open question, with the gap between $k$ and $2k-1$ unmoved since 1995.
• 2026. Coester, Koutsoupias, and Zbysiński post The $k$-server conjecture is true (arXiv:2609.15979), a claimed proof of the full conjecture: the Work Function Algorithm itself is $k$-competitive on every metric space, via a matrix representation of work functions and a potential function built on it. The preprint is not yet peer-reviewed; this mission's goal stays open until a machine-checked proof exists.

Setting

Fix a metric space $M$ with distance function $d$, and a number of servers $k \ge 1$. A configuration records where the $k$ servers stand: it is a function $C$ assigning to each server $i \in \{1, \dots, k\}$ a point $C(i) \in M$. Moving the servers from configuration $C$ to configuration $C'$ means server $i$ travels from $C(i)$ to $C'(i)$; the movement cost is the total distance traveled,

$$\mathrm{moveCost}(C, C') \;=\; \sum_{i=1}^{k} d\bigl(C(i),\, C'(i)\bigr).$$

A request sequence is a finite list $\sigma = (r_1, \dots, r_n)$ of points of $M$, presented one at a time; write $\sigma_{\le j} = (r_1, \dots, r_j)$ for the list of the first $j$ requests (so $\sigma_{\le 0}$ is the empty list).

A deterministic online algorithm $A$ is a rule that, for every finite request sequence $\ell$, specifies a configuration $A(\ell)$ — where the servers stand after serving the requests of $\ell$ in order. In particular $A(\text{empty list})$ is the initial configuration, before any request arrives. Two points about this way of modeling an algorithm:

• Online and deterministic, by construction. The configuration after $j$ requests is $A(\sigma_{\le j})$, a function of those first $j$ requests only — the algorithm cannot see the future, and makes no random choices.
• The service constraint. Whenever a request sequence ends with a request $r$, some server must stand at $r$ immediately after: for every list $\ell$ and every point $r$, the configuration reached after serving $\ell$ followed by $r$ places at least one server at the point $r$.

Running $A$ on $\sigma = (r_1, \dots, r_n)$ produces the configurations $A(\sigma_{\le 0}),\, A(\sigma_{\le 1}),\, \dots,\, A(\sigma_{\le n})$, and its cost is the total movement along this trajectory:

$$\mathrm{cost}_A(\sigma) \;=\; \sum_{j=1}^{n} \mathrm{moveCost}\bigl(A(\sigma_{\le j-1}),\, A(\sigma_{\le j})\bigr).$$

For comparison, an offline schedule for $\sigma$ starting at a configuration $C_0$ is any sequence of configurations $S_0 = C_0, S_1, \dots, S_n$ in which $S_j$ places a server at the request $r_j$, for each $j$ — chosen with the whole of $\sigma$ known in advance. The optimal offline cost $\mathrm{OPT}(C_0, \sigma)$ is the infimum, over all such schedules, of the total movement $\sum_{j=1}^{n} \mathrm{moveCost}(S_{j-1}, S_j)$.

Finally, $A$ is $c$-competitive if there is a constant $a$ — depending on the algorithm, hence possibly on the metric space and the initial configuration, but never on the request sequence — with

$$\mathrm{cost}_A(\sigma) \;\le\; c \cdot \mathrm{OPT}\bigl(A(\text{empty list}),\, \sigma\bigr) + a \qquad \text{for every request sequence } \sigma.$$

Formalization targets

Goal — the $k$-server conjecture

$$\text{For every } k \ge 1,\ \text{every metric space } M,\ \text{and every initial configuration } C_0:\ \exists\, A \text{ starting at } C_0 \text{ that is } k\text{-competitive.}$$

The goal fixes no algorithm: any $k$-competitive construction settles it. This is the weakest stable form of the conjecture — it survives every improvement in constants or techniques short of a disproof.

Milestones — the known ladder

The milestones are the classical results between the trivial and the conjectured, each an existence or impossibility statement over the same definitions: the lower bound $c \ge k$ on any space with at least $k+1$ points; the conjecture for $k = 2$; for spaces of exactly $k+1$ points; for the real line; the $(2k-1)$ upper bound of the Work Function Algorithm on every space; the conjecture for spaces of exactly $k+2$ points; the conjecture for three servers in the Manhattan plane $(\mathbb{R}^2, \ell^1)$ — the one settled case over a genuinely two-dimensional continuum (Bein–Chrobak–Larmore 2002; reproved by the unifying potential of Coester–Koutsoupias 2021); Coester–Koutsoupias's 2021 result that the Work Function Algorithm itself — not just some algorithm — is $3$-competitive for three servers on trees, stated over an explicit formalization of the WFA; and the 2023 Bubeck–Coester–Rabani refutation of the randomized analogue: there are $(k+1)$-point spaces on which every randomized algorithm is $\Omega(\log^2 k)$-competitive, stated over a mixed-strategy model of randomized online algorithms.

Significance

A proof of the conjecture would close the founding problem of competitive analysis and pin down the exact power of determinism in online optimization over arbitrary metrics; a disproof would separate general metric spaces from every special class where the ratio $k$ is known tight. Either outcome recalibrates the field's standard model of adversarial request sequences.

None of these results — not even the lower bound — has a machine-checked proof, and online algorithms as a subject are absent from Mathlib. This mission builds the base layer: a faithful model of online service systems (configurations, online algorithms as prefix functions, offline schedules, competitiveness), the classical possibility and impossibility results over it, and, at the top, the Koutsoupias–Papadimitriou bound, whose potential-function argument is self-contained but delicate. The model is reusable for paging, weighted caching, metrical task systems, and the randomized $k$-server problem.

Difficulty

The obvious first idea — the greedy algorithm, moving the nearest server to each request — is not competitive for any constant, already on three points of the line: two nearby points can ping-pong one server forever while a server parked slightly farther away never moves. Every known competitive algorithm must sometimes move a server other than the nearest one, and the whole difficulty of the conjecture is quantifying exactly how much such foresight-free hedging can achieve. The Work Function Algorithm's analysis via a potential over offline work functions loses a factor of two for reasons nobody has been able to remove; on the lower-bound side, no metric space is known where the deterministic ratio exceeds $k$.

Formalization scope

The Lean model commits to: configurations as functions Fin k → M (labeled servers — equivalent in cost to the unlabeled multiset model, since offline can permute labels for free); algorithms as total functions List M → (Fin k → M) with the service constraint, so a step may move several servers (the standard laziness reduction makes this equivalent to one-move-per-request); costs in ℝ via Metric.dist; the offline optimum as an sInf over schedules, which agrees with the attained minimum on finite spaces; and the additive-constant form of competitiveness, quantified as ∃ a, ∀ σ.

Two conventions guard against trivialization. The additive constant is quantified before the request sequence — allowing it to depend on $\sigma$ would make every algorithm $1$-competitive. And the lower-bound milestone requires $k+1$ distinct points (Finset.card = k + 1); on spaces with at most $k$ points the conjecture is trivially true and the lower bound false.

Three further definitional layers extend the model. The work function workFunction C₀ σ C is the sInf of (schedule cost + final move to C) over schedules serving σ from C₀, and the Work Function Algorithm WFA is defined on finite spaces with k ≥ 1 servers: after each request it moves to a configuration containing the request minimizing (movement cost) + (work function of the history including the request), a minimizer existing by finiteness and ties broken by a fixed arbitrary choice — matching the standard definition with its "ties broken arbitrarily" (our fixed choice is one admissible instance). A tree is a finite metric space carrying a tree graph whose weighted path lengths realize the metric — exactly "the set of vertices of a tree" of the sources. A randomized algorithm is a mixed strategy: a probability measure over an index type together with a deterministic algorithm per outcome and measurable per-sequence cost; its expected cost is a lower Lebesgue integral in $[0,\infty]$, and $c$-competitiveness from $C_0$ demands every outcome start at $C_0$ and one additive constant work for all request sequences.

Welcome contributions: proofs of any milestone in any order (the lower bound and the $(k+1)$-point case are the natural entry points); alternative algorithms for milestones already closed; and infrastructure lemmas about moveCost, schedules, and work functions published as reusable platform theorems.

Selected references

• M. Manasse, L. McGeoch, D. Sleator, Competitive algorithms for server problems, J. Algorithms 11 (1990). doi:10.1016/0196-6774(90)90003-W
• A. Fiat, Y. Rabani, Y. Ravid, Competitive k-server algorithms, FOCS 1990. doi:10.1109/FSCS.1990.89566
• M. Chrobak, H. Karloff, T. Payne, S. Vishwanathan, New results on server problems, SIAM J. Discrete Math. 4 (1991). doi:10.1137/0404017
• M. Chrobak, L. Larmore, An optimal on-line algorithm for k servers on trees, SIAM J. Comput. 20 (1991). doi:10.1137/0220008
• E. Koutsoupias, C. Papadimitriou, On the k-server conjecture, J. ACM 42 (1995). doi:10.1145/210118.210128
• E. Koutsoupias, C. Papadimitriou, The 2-evader problem, Inf. Process. Lett. 57(5) (1996), 249–252.
• C. Coester, E. Koutsoupias, Towards the k-server conjecture: a unifying potential, pushing the frontier to the circle, ICALP 2021. arXiv:2102.10474
• S. Bubeck, C. Coester, Y. Rabani, The randomized k-server conjecture is false!, STOC 2023. arXiv:2211.05753
• E. Koutsoupias, The k-server problem (survey), Computer Science Review 3 (2009). doi:10.1016/j.cosrev.2009.04.002

The problem of solving linear inequalities

The linear feasibility problem takes a matrix $A \in \mathbb{R}^{m\times n}$ and a vector $b \in \mathbb{R}^m$ and asks whether the system of $m$ linear inequalities in $n$ real unknowns

$$\{\,x \in \mathbb{R}^n \mid Ax \ge b\,\} \;\ne\; \emptyset$$

has a solution. By linear programming duality, optimizing a linear objective over such a set reduces to feasibility, so this decision problem carries the whole complexity of linear programming.

What "polynomial time" means here depends on the machine. In the bit model the input is a list of rational numbers, its size $L$ counts the bits of all numerators and denominators, and an algorithm is polynomial if it runs in time $\mathrm{poly}(m, n, L)$. In the real-number model the input is a list of $mn + m$ exact real numbers, each arithmetic operation ($+, -, \times, \div$), comparison, or memory move costs one unit, and a running time may only depend on $m$ and $n$. An algorithm polynomial in this second sense is what Smale asks for; the closely related bit-model notion — $\mathrm{poly}(m,n)$ arithmetic operations and polynomially bounded intermediate bit sizes — is called strongly polynomial. This mission fixes the real-number model precisely as a Blum–Shub–Smale (BSS) machine (Blum–Shub–Smale 1989): a finite program of instructions acting on a bi-infinite tape $\mathbb{Z} \to \mathbb{R}$ of real registers — loads of arbitrary real machine constants, exact field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch, and accept/reject — with cost equal to the number of executed instructions. The convention that costs something: the program must be uniform, one finite instruction list serving every $m$, $n$, and every real instance. Uniformity is exactly what separates the question from point-location tricks available to non-uniform families of decision trees.

Why it matters

For optimization, the question is the last gap in the complexity of its central problem. Linear programs with combinatorial structure already admit strongly polynomial algorithms — Tardos (1986) solved every LP whose running time may depend on the entries of $A$ but not on $b$ or $c$, covering network flows and all $\{0,\pm1\}$-constraint problems — and a positive answer for general LP would extend that unification to the whole class, while explaining why simplex-type methods behave so well in practice (Spielman–Teng 2004).

For the theory of computation over the reals, the problem is a benchmark for what unit-cost exact arithmetic can do: it is Problem 9 on Smale's list of mathematical problems for the twenty-first century (Smale 1998), posed in the BSS model as the real-number analogue of the P-versus-NP style questions of that program, and it interacts with polyhedral combinatorics through the polynomial Hirsch conjecture: a polynomial bound on polytope diameters is a necessary condition for any polynomial pivot rule. A problem that calibrates both the practice of optimization and the foundations of real computation is a subject, not a special case.

The question and what is known

$$\textbf{Question (Smale's 9th).}\quad \text{Is there a uniform BSS program deciding } \{x \mid Ax \ge b\} \ne \emptyset \text{ in } \mathrm{poly}(m,n) \text{ steps?}$$

The timeline splits into a negative branch (lower bounds against algorithm classes) and a positive branch (polynomial algorithms in weaker senses).

Lower bounds. Klee–Minty (1972) constructed a deformed cube on which Dantzig's largest-coefficient simplex rule visits all $2^n$ vertices; analogous exponential examples were later found for essentially every deterministic pivot rule, and randomized rules were driven to subexponential lower bounds by Friedmann–Hansen–Zwick (2011) — against upper bounds of $\exp(O(\sqrt{n \log n}))$ from Kalai (1992) and Matoušek–Sharir–Welzl (1996). On the interior-point side, Allamigeon–Benchimol–Gaubert–Joswig (2018) showed by tropical methods that log-barrier path following is not strongly polynomial, and Allamigeon–Gaubert–Vandame (2022) extended this to every self-concordant barrier: no interior-point method of that class can settle the question positively.

Polynomial algorithms in weaker senses. Khachiyan (1979/80) proved LP feasibility is polynomial in the bit model via the ellipsoid method; Karmarkar (1984) and then Renegar (1988) brought interior-point methods to $O(\sqrt{n}\,L)$ iterations. Megiddo (1984) solved LP in linear time for every fixed dimension; Tardos (1986) gave the combinatorial strongly polynomial class; Vavasis–Ye (1996) and Dadush–Huiberts–Natura–Végh (2020) replaced the bit size by condition measures of $A$ alone; Ye (2011) proved policy iteration strongly polynomial for fixed-discount Markov decision processes.

The central difficulty is visible in every positive result: each known iteration count is controlled by a scale-dependent quantity — bit length, condition number, barrier curvature — that is unbounded over the real instances with $m, n$ fixed. The naive plan, "run the ellipsoid method and round", fails at its first step in the real model: the number of iterations needed to separate a feasible system from an infeasible one grows with the thinness of the feasible set, which is not a function of $(m, n)$; no data-independent perturbation $\varepsilon$ exists when the data are arbitrary reals. All results above are proved on paper only; none has a machine-checked proof in the literature. What is already formalized, on this platform, is the substrate this mission builds on: the simplex iteration (mission Introduction to Linear Optimization IV), the ellipsoid method with its volume-halving correctness theorem (XI), interior-point path following (XII), and self-concordance with the barrier method (Convex Optimization VI).

A hierarchy of formalization targets

The mission's milestone list realizes this hierarchy in order; each level states what it deliberately leaves open.

Level 0 — the model works. A uniform BSS program decides one-variable feasibility in linear time:

$$\exists\,P,\,C\ \ \forall m,\ \forall (a,b) \in \mathbb{R}^m \times \mathbb{R}^m:\ P \text{ decides } \{x \in \mathbb{R} \mid a_i x \ge b_i\ \forall i\} \ne \emptyset \text{ within } C(m{+}1) \text{ steps}.$$

It fixes nothing about $n \ge 2$; its role is to certify that the machine model and cost semantics of the goal are non-vacuous.

Level 1 — the classical method is exponential. On the Klee–Minty cube, Dantzig's rule admits a run of

$$2^n - 1 \text{ pivots}$$

from the all-slack basis to the optimum. It leaves open all other pivot rules — extensions to further rules are welcome as strengthenings.

Level 2 — the bit model succeeds. Through the Cramer–Hadamard solution bound $|x_j| \le n!\,U^n$ and the perturbation estimates, Khachiyan's theorem: for integer data bounded by $U$, every admissible ellipsoid run decides feasibility within

$$t^* \le 10^6\,(n{+}2)^4(\log_2 U + n + 2) \text{ iterations}.$$

The generous constants are deliberate — only the polynomial order is load-bearing. This level leaves open exactly the dependence on $\log U$.

Level 3 — the goal (open). A uniform program with data-independent polynomial cost:

$$\exists\,P,\,C,\,d\ \ \forall m, n, A, b:\ P \text{ decides } \{x \mid Ax \ge b\} \ne \emptyset \text{ within } C\,(mn + m + 2)^d \text{ steps}.$$

The statement asserts only the shape of the truth — no hard-coded degree or constant — so it is stable under every future quantitative improvement. These levels do not exhaust the project: Tardos' combinatorial LP theorem, Ye's fixed-discount MDP result, and impossibility statements for restricted program classes in the style of Allamigeon–Gaubert–Vandame are natural later milestones.

Formalization scope

Polyhedra, simplex states, pivots, and ellipsoid runs are the platform's existing LinearOptimization development over Matrix (Fin m) (Fin n) ℝ, with $\{x \mid Ax \ge b\}$ as polyhedron A b; algorithms with data-dependent iteration counts are formalized as run predicates, as in the parent missions. The new SmaleNinth definitions supply what the goal genuinely needs and the run-predicate style cannot express: a concrete inductive type of BSS programs with operational semantics and unit-cost accounting, the Klee–Minty data with Dantzig's rule, and the explicit Khachiyan constants. One convention closes the degenerate escape hatch: the goal quantifies over finite BSSProgram terms under the fixed encodeLP input convention — formalizing "algorithm" as an arbitrary function $\mathbb{R}^{mn+m} \to \mathrm{Bool}$ would make the statement trivially true and is not the theorem. Division is totalized as $x/0 = 0$ and the branch test is $x_i \le 0$; both are benign for the class of programs quantified over.

The machine module is infrastructure beyond this mission — any real-number complexity statement (other Smale problems, sums-of-square-roots, BSS-completeness) can reuse it, as can any pivot-rule lower bound reuse the Klee–Minty module. Formalization forces distinctions the literature leaves informal: which machine variant carries the unit-cost claim, how ties in Dantzig's rule are resolved, and which of the interchangeable Khachiyan constants each estimate actually needs. Welcome contributions include proofs of any milestone, alternative exponential instances for other pivot rules, sharper constants in the Khachiyan module, and ports of the known strongly polynomial special cases.

Selected references

• L. Blum, M. Shub, S. Smale, On a theory of computation and complexity over the real numbers, Bull. AMS 21(1):1–46, 1989. DOI
• S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2):7–15, 1998. DOI
• V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972, pp. 159–175.
• L. G. Khachiyan, Polynomial algorithms in linear programming, USSR Comput. Math. Math. Phys. 20:53–72, 1980. DOI
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4:373–395, 1984. DOI
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Math. Programming 40:59–93, 1988. DOI
• É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Oper. Res. 34(2):250–256, 1986. DOI
• N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. DOI
• G. Kalai, A subexponential randomized simplex algorithm, STOC 1992. DOI
• O. Friedmann, T. D. Hansen, U. Zwick, Subexponential lower bounds for randomized pivoting rules for the simplex algorithm, STOC 2011. DOI
• D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: why the simplex algorithm usually takes polynomial time, J. ACM 51(3):385–463, 2004. DOI
• S. A. Vavasis, Y. Ye, A primal-dual interior point method whose running time depends only on the constraint matrix, Math. Programming 74:79–120, 1996. DOI
• Y. Ye, The simplex and policy-iteration methods are strongly polynomial for the Markov decision problem with a fixed discount rate, Math. Oper. Res. 36(4):593–603, 2011. DOI
• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1):140–178, 2018. DOI
• X. Allamigeon, S. Gaubert, N. Vandame, No self-concordant barrier interior point method is strongly polynomial, STOC 2022. arXiv
• D. Dadush, S. Huiberts, B. Natura, L. A. Végh, A scaling-invariant algorithm for linear programming whose running time depends only on the constraint matrix, STOC 2020. arXiv
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Chapters 3, 8, 9 — formalized in the Introduction to Linear Optimization mission series).
• B. Korte, J. Vygen, Combinatorial Optimization: Theory and Algorithms, 6th ed., Springer, 2018, §4.1–4.5.

Motivation

A linear program asks for a point $x\in\mathbb{R}^d$ minimizing $c^Tx$ subject to $n$ linear inequalities $\sum_{j=1}^d a_{ij}x_j\ge b_i$. Many problems in computational geometry and statistics are linear programs with few variables and very many constraints: separating two point sets by a line or plane, fitting a line in the Chebyshev ($L_\infty$) norm, finding the smallest disk or ball containing a point set (a related convex problem). For these problems the number of variables $d$ is a small constant, and what matters is how the running time grows with $n$.

Nimrod Megiddo showed that for every fixed $d$ the problem can be solved in time $C(d)\cdot n$ (J. ACM 31(1), 1984).

Timeline.

• 1983. Megiddo (SIAM J. Comput. 12) and, independently, Dyer (SIAM J. Comput. 13 (1984)) give linear-time algorithms for $d=2$ and $d=3$.
• 1984. Megiddo extends the method to every fixed $d$, with $C(d)<2^{2^{d+2}}$ (the paper formalized here).
• 1988–1991. Clarkson (J. ACM 42 (1995), conference version 1988) gives a randomized algorithm with expected time $O(d^2n)+d^{O(\sqrt d)}\log n$. Seidel (Discrete Comput. Geom. 6 (1991)) gives a simple randomized $O(d!\,n)$ algorithm.
• 1992–1996. Matoušek, Sharir and Welzl and, independently, Kalai give subexponential randomized bounds. Chazelle and Matoušek derandomize the linear dependence with $C(d)=d^{O(d)}$ (J. Algorithms 21 (1996)).

Setting

Fix $d$. An instance is a matrix $A\in\mathbb{R}^{n\times d}$ and a vector $b\in\mathbb{R}^n$, and its feasible region is the polyhedron $P(A,b)=\{x\in\mathbb{R}^d: Ax\ge b\}$. Here $n$ is the number of constraints and $d$ the number of variables.

The model of computation is the real RAM. A program is a finite list of instructions acting on real registers, integer pointer registers and a memory $\mathbb{Z}\to\mathbb{R}$. It performs exact $+,-,\times,/$ on reals at unit cost, tests the sign of a real, sets, copies, increments, decrements and compares pointers, and loads and stores through pointers. The input is the standard encoding of $(A,b)$ in memory: the numbers $n$ and $d$, then $A$ row by row, then $b$. A program decides an instance within $T$ steps with output $\beta\in\{\text{accept},\text{reject}\}$ if it halts on that output after at most $T$ steps.

Megiddo's method rests on multidimensional search. There is an unknown point $x^*\in\mathbb{R}^d$ and an oracle that, for any hyperplane $\{x: a^Tx=b\}$, answers whether $a^Tx^*<b$, $=b$ or $>b$. Given hyperplanes $H_i=\{a_i^Tx=b_i\}$ with $a_i\ne0$, the question is how many oracle calls determine the position of $x^*$ relative to all of them. A search strategy is a ternary decision tree: inner nodes are hyperplane queries, leaves carry outputs, and the tree is built from the data alone. For linear programming, $x^*$ is an optimal solution, or a minimizer of the infeasibility function $f(x)=\max_i(b_i-a_i^Tx)$ when the system is infeasible. The oracle is implemented by solving problems in $d-1$ variables.

Formalization targets

Goal: linear-time feasibility on the real RAM

$$\forall d\ \exists R\ \exists C\ \forall n\ \forall A\in\mathbb{R}^{n\times d},\,b\in\mathbb{R}^n:\quad R\text{ decides within }C\,(n+1)\text{ steps whether } \{x: Ax\ge b\}\neq\emptyset.$$

The program and the constant depend on $d$ only. No explicit form of $C(d)$ is fixed.

Milestones

1. One query settles half of $n$ hyperplanes on the line ($A(1)=1$, $B(1)=\tfrac12$).
2. $v(\epsilon)=(1,\epsilon,\dots,\epsilon^{d-1})$ is orthogonal to some $a_i$ for at most $n(d-1)$ values of $\epsilon$, so there is a basis in which all $a_{ij}\ne0$.
3. For hyperplanes of opposite slopes in the $(x_1,x_2)$ plane, the answers for $H^{(1)}_{ik}$ and $H^{(2)}_{ik}$ settle one of $H_i$, $H_k$.
4. A linearly dependent pair of opposite slopes has $a_{i1}=a_{k1}=0$, and the middle hyperplane settles one of them.
5. Approach I: $2^{d-1}$ queries settle at least $\lfloor 2^{1-2^d}n\rfloor$ hyperplanes.
6. $C(d)\log n$ queries settle all $n$ hyperplanes.
7. If a hyperplane contains no optimal point, all optimal points lie on one side of it.
8. The oracle, Case I: at an optimum relative to $\{x_d=0\}$, two auxiliary systems decide the side or certify global optimality.
9. The oracle, Case II: at a minimizer of $f$ on $\{x_d=0\}$, systems (1) and (2) decide the side or certify infeasibility.

Significance

The result. For every fixed dimension, linear programming is solvable in time linear in the number of constraints. The algorithm is also strongly polynomial in fixed dimension: its operation count does not depend on the bit size of the data. Deciding whether the optimum is at most $t$ is feasibility of $Ax\ge b$ together with $-c^Tx\ge-t$, so the goal also covers the decision form of optimization. The prune-and-search technique of the paper, which discards a constant fraction of the constraints per round, became a standard tool of computational geometry.

Formalizing it. The result is proved and classical. The platform already has the cases $d=1$ (linear time) and $d=2$ (quadratic time, by Fourier–Motzkin elimination) on the same machine and input encoding (SmaleNinth.real_ram_decides_one_variable_lp_linear, SmaleNinth.real_ram_decides_two_variable_lp_quadratic). No machine-checked proof of the general statement is known. The work consists of the query-complexity layer (milestones 1–6), the convex-analytic correctness of the oracle (milestones 7–9), and a real-RAM implementation with a step count linear in $n$, including linear-time median selection. Alternative proofs, for example through Clarkson's or Seidel's algorithms made deterministic, are welcome for the goal.

Difficulty

The obvious approach is to find the optimum by testing constraints one by one or by eliminating variables. Fourier–Motzkin elimination produces $\Theta(n^2)$ constraints after one step. Pivoting methods have no known bound linear in $n$. The key difficulty is to discard a constant fraction of the constraints using only a constant number of recursive calls in dimension $d-1$, when no single hyperplane test gives information about more than one constraint. The multidimensional search layer gives this, and it is where the pairing of hyperplanes by slope and the degenerate cases (dependent pairs, zero coefficients) have to be handled exactly. At the machine level, the step count must stay linear in $n$ for a fixed program, so every median selection and every recursive call must be implemented within the budget, with the recursion depth depending on $d$ only.

Formalization scope

• Machine and input. The machine is the platform's real RAM SmaleNinth.RAMProgram with RAMDecidesInTime, and the input convention is SmaleNinth.encodeLP (published definitions, reused unchanged). No instruction is added: there is no LP, median, floor or sort primitive. Time is the number of machine steps.
• Quantifier order. $\forall d\ \exists R\ \exists C\ \forall n, A, b$. The bound is $C(n+1)$ in the number $n$ of constraints, so that the machine can halt at $n=0$. The paper's $C(d)<2^{2^{d+2}}$ counts unspecified units of "effort" with an unquantified $\theta(nd)$ term, and it is not transferred to machine steps. Where a milestone's proof fixes a constant exactly, the constant is stated: $2^{d-1}$ queries and $\lfloor n/2^{2^d-1}\rfloor$ settled hyperplanes in milestone 5.
• Feasibility only. The machine outputs accept or reject. Returning an optimizer, "unbounded", or a minimizer of $f$ is not part of the goal. The case $d=0$ is included.
• Query trees. Nodes are queries compare (a ⬝ᵥ x) b and nothing else, leaves hold fixed values, and correctness is required for every $x$. A tree over arbitrary tests of $x$ would make milestones 5 and 6 empty, and it is excluded by the definition.
• Indices. The paper's $x_1,x_2$ are indices 0, 1 of Fin (d + 2), and its $x_d$ is Fin.last d of Fin (d + 1).
• Corrections. Two passages of §4 are stated in corrected form. The Case I auxiliary objective includes the $\pm c_d$ term of the direction. In Case II, feasibility of (1) puts improvement in $\{x_d>0\}$, where the page's last sentence says $\{x_d<0\}$. The pairing claim carries $a_{k1}a_{i2}-a_{k2}a_{i1}\ne0$, the hypothesis its argument uses, since linear independence alone does not give it.
• Not included. Approach II and its bound $O(n(\log n)^{d^2})$, the remarks on slowly growing $d$, the randomized variants, and the applications of §1.
• Reusable parts. The query-tree definition and milestones 1–6 apply to any prune-and-search problem with a hyperplane oracle. The oracle lemmas (7–9) are statements about convex piecewise-linear functions and polyhedra.

Selected references

• N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. https://doi.org/10.1145/2422.322418
• N. Megiddo, Linear-time algorithms for linear programming in $R^3$ and related problems, SIAM J. Comput. 12(4):759–776, 1983. https://doi.org/10.1137/0212052
• M. E. Dyer, Linear time algorithms for two- and three-variable linear programs, SIAM J. Comput. 13(1):31–45, 1984. https://doi.org/10.1137/0213003
• K. L. Clarkson, Las Vegas algorithms for linear and integer programming when the dimension is small, J. ACM 42(2):488–499, 1995. https://doi.org/10.1145/201019.201036
• R. Seidel, Small-dimensional linear programming and convex hulls made easy, Discrete Comput. Geom. 6:423–434, 1991. https://doi.org/10.1007/BF02574699
• B. Chazelle, J. Matoušek, On linear-time deterministic algorithms for optimization problems in fixed dimension, J. Algorithms 21(3):579–597, 1996. https://doi.org/10.1006/jagm.1996.0046

Motivation

Every generalization bound presented so far in this series is for classification, where the error of a prediction is binary (correct or not). Regression asks a different question: predictions are real-valued, and error is measured by the magnitude of the deviation from the true label, via a loss function L. Chapter 11 develops generalization theory for bounded regression, showing that the same two complexity measures used for classification — Rademacher complexity and a VC-dimension analogue — extend naturally, once the loss function itself is folded into the machinery via a Lipschitz-contraction argument (Rademacher route) or a reduction to classification via level-set thresholding (pseudo-dimension route).

Setting

A regression hypothesis h:X→ℝ is scored by a loss L:ℝ×ℝ→ℝ against a joint distribution D on X×ℝ (the stochastic scenario, since regression labels are rarely exactly reproducible); R(h) = E_{(x,y)~D}[L(h(x),y)] (Eq. 11.1) and R̂_S(h) = (1/m)∑L(h(x_i),y_i) (Eq. 11.2). For a finite hypothesis set, Theorem 11.1 gives a Hoeffding/union-bound guarantee directly, the regression analogue of chunk 02-pac's finite-hypothesis bound. For infinite H, §11.2.2 develops a Rademacher-complexity route: Proposition 11.2 shows that if L is µ-Lipschitz in its first (predicted-value) argument, the Rademacher complexity of the loss-composed family G = {(x,y)↦L(h(x),y) : h∈H} is controlled by µ times H's own Rademacher complexity, via Talagrand's contraction lemma (chunk 05-svm's Lemma 5.7); Theorem 11.3 combines this with chunk 03's Theorem 3.3 to give the chapter's headline bound. §11.2.3 develops an independent, purely combinatorial route: pseudo-dimension (Definition 11.5), a real-valued analogue of VC-dimension defined via threshold-witnessed shattering (Definition 11.4, restated via its own Eq. 11.3 as the VC-dimension of a thresholded indicator family); Theorem 11.8 gives a pseudo-dimension generalization bound by reducing regression to a family of classification problems (one per threshold t), using the tail-integral identity Eq. 11.5.

Formalization targets

Theorem 11.1 (milestone). For L bounded by M and H finite: for any δ>0, with probability at least 1-δ, for all h∈H: R(h) ≤ R̂_S(h) + M√((log|H|+log(1/δ))/(2m)).

Proposition 11.2 (milestone). For L non-negative, bounded by M, µ-Lipschitz in its first argument: for any sample S, R̂_S(G) ≤ µR̂_S(H).

Theorem 11.3 — the mission's goal. Under Proposition 11.2's hypotheses on L: for any δ>0, with probability at least 1-δ, for all h∈H: E[L(h(x),y)] ≤ (1/m)∑L(h(x_i),y_i) + 2µR_m(H) + M√(log(1/δ)/(2m)), and also with 2µR̂_S(H) + 3M√(log(2/δ)/(2m)).

Theorem 11.8 (milestone). For Pdim(G)=d, L non-negative bounded by M: for any δ>0, with probability at least 1-δ over a sample of size m, for all h∈H: R(h) ≤ R̂_S(h) + M√(2d log(em/d)/m) + M√(log(1/δ)/(2m)).

Significance

Theorem 11.3 is the chapter's own choice of headline result (§11.2's stated goal is to show "how the Rademacher complexity bounds of theorem 3.3 can be used to derive generalization bounds for regression"), and its proof genuinely reuses two pieces of prior machinery from this series — chunk 03's Theorem 3.3 and chunk 05's Talagrand's-lemma-style contraction — combined via a new observation (Proposition 11.2) specific to loss-composed families, not a restatement of either. Theorem 11.8 is the chapter's second, structurally independent technique: its em/d bound parallels chunk 03's Corollary 3.19 (both ultimately reduce to a VC-dimension-style growth-function argument), but the reduction itself — regression to a continuum of threshold classification problems, via the Lebesgue-integral tail identity Eq. (11.5) applied to |R(h)-R̂_S(h)| — is genuinely new content for this book, and pseudo-dimension has no prior art on the platform or in Mathlib. No prior art exists for this chapter's overall content either: GET /theorems?q=generalization%20bound%20regression and GET /theorems?q=pseudo-dimension both return zero hits.

Difficulty

Proposition 11.2's proof needs Talagrand's contraction lemma applied with the Lipschitz constant taken in the first argument of L only — the predicted value h(x_i), holding the true label y_i fixed — exactly the pitfall BRIEF.md names: a loss Lipschitz in the wrong argument, or in both arguments jointly, would not license this step. Theorem 11.8's proof is the chapter's most involved: it defines, for every h∈H and threshold t≥0, a classifier c(h,t):(x,y)↦1_{L(h(x),y)>t}, bounds |R(h)-R̂_S(h)| by M·sup_{t∈[0,M]}|R(c(h,t))- R̂_S(c(h,t))| via the tail-integral identity, and then applies a VC-dimension-style classification bound (Corollary 3.19) to the family of thresholded classifiers — whose VC-dimension is, by Eq. (11.3), exactly Pdim(G) by construction. A formalization that conflated pseudo-dimension with ordinary VC-dimension, or reused chunk 03's HasVCDim definition by relabeling, would misrepresent this chapter's genuinely different (real-valued, threshold-witnessed) combinatorial notion — precisely the pitfall BRIEF.md flags.

Formalization scope

Y := ℝ throughout (the book's own "Y a measurable subset of ℝ"), a harmless simplification consistent with every hypothesis, loss and Lipschitz condition in this chapter being stated for real-valued scores and labels. EmpiricalRademacherComplexity/ RademacherComplexity restate chunk 03-rademacher-vc's Definitions 3.1/3.2 locally, since a draft item cannot import another chunk's draft module. Shatters/PseudoDim are formalized via the book's own equivalent reformulation (Eq. 11.3, the thresholded-indicator form), rather than the sign-function form of Definition 11.4 directly, since the two coincide except at a measure-zero boundary the book itself does not address; PseudoDim mirrors chunk 03's HasVCDim Prop-valued pattern (does not cover Pdim(G)=+∞; every consuming theorem takes it as an explicit hypothesis) but is a structurally distinct definition built on Shatters, never a relabeling of HasVCDim, per BRIEF.md's pitfall note. Proposition 11.2's and Theorem 11.3's Lipschitz hypothesis (hLlip) is stated with the true label y' universally quantified outside the two-point comparison y1, y2 (the predicted values), matching "for any fixed y' ∈ Y, y ↦ L(y,y') is µ-Lipschitz" exactly — Lipschitzness in the first argument only, per BRIEF.md's pitfall note. RademacherComplexity (Measure.map Prod.fst D) H m gives the book's R_m(H) (H's Rademacher complexity under the marginal sampling distribution of the inputs x, i.e. D's first marginal). No numerical constant is altered from the book in any of the four theorems.

Not formalized: the L_p-loss worked example following Theorem 11.3's proof (an instantiation of the general theorem for a specific loss family, not a separate numbered theorem); Theorem 11.6 and Theorem 11.7 (worked pseudo-dimension examples for hyperplanes and vector spaces, background/illustration rather than the chapter's general machinery — drafting only these examples instead of the general Theorem 11.8 would be this chapter's trivializing formalization); the two-sided variant of Theorem 11.1 mentioned immediately after its proof (an unnumbered remark, not a separately displayed/numbered theorem); and all of §11.3 (linear regression, kernel ridge regression, SVR, Lasso and their online variants), which is applications-heavy per BRIEF.md's chapter restriction to §11.1-11.2.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 11 (§11.1-11.2).
• D. Haussler, "Decision theoretic generalizations of the PAC model for neural net and other learning applications," Information and Computation 100(1), 1992 (pseudo-dimension's origin).
• D. Pollard, Convergence of Stochastic Processes, Springer, 1984 (the tail-integral identity Eq. 11.5's classical antecedent).

Motivation

Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an $O(n\log n)$ bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.

Setting

A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.

An input consists of two bit strings $x,y$ of the same positive length $n$, separated by $\#$. The strings are read most significant bit first, with leading zeros permitted. If $\operatorname{val}(x)$ denotes the represented natural number, the required output is exactly the $2n$-bit binary representation of $\operatorname{val}(x)\operatorname{val}(y)$, padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define $L(n)=\max(\lceil\log_2 n\rceil,1)$.

Target

The full target is

$$\mathrm{IntMul.KappaBound}(0.00012612978530233).$$

This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants $c>0$ and $n_0$ such that every pair of $n$-bit inputs, for $n\ge n_0$ and $n\ge1$, halts within

$$c\,n\,L(n)^{1-0.00012612978530233}$$

steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger $\kappa$ gives a stronger asymptotic saving because $L(n)\ge1$.

Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.

This entry: Jain, round eight

The value

$$\kappa=\frac{12612978530233}{10^{17}}=0.00012612978530233\;(>2^{-13})$$

is the headline conditional witness of S. Jain's integer-mult-kappa, round eight, at revision 5868dc7. It is bound by the complex side ($a_c=3945999/31250000000$).

• Bit side: the frozen round-seven witness (deferred readouts, $V$ leaves, lifted frames and late copies at $h=23$; Avi Eisenberg's producer from PR #62, compiled by eumemic's joint frame compiler), recompiled with opposite bank orders and a stopped interchange after IceKylin (PR #104).
• Complex side: a signed reclaim with completed-core sharing and one fix-up child per group.

The repository states that the claim is conditional: it assumes the full upstream multiplication theorem (the OpenAI manuscript and Colkitt's framework) and that stage two is the complement time-reversal of stage one, and it rests on three further interfaces that are stated but not machine-checked there — IceKylin's normal form for alternating residuals, the cost of binary address adapters for the exterior fix-up children, and the row stock of the stopped bit interchange. Its Lean files check only finite rational statements (moment certificates, the stopped mix and the parameter assembly), not the analytic inequalities or the multiplication theorem. It has not had independent review.

Earlier claims appear as milestones: Harvey–van der Hoeven ($\kappa=0$), OpenAI Theorem 1 ($2^{-182}$), Colkitt's $2^{-30}$ checkpoint, Jain rounds six and seven, and community PR #62. Each is implied by this goal because $L(n)^{1-\kappa}$ decreases in $\kappa$.

Significance

A proof for any positive value would give a strict asymptotic improvement over $n\log n$. Such an improvement would contradict the proposed $\Omega(n\log n)$ lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.

Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.

Difficulty

A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.

Formalization scope

The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.

The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.

Selected references

• D. Harvey and J. van der Hoeven, Integer multiplication in time O(n log n), Annals of Mathematics 193(2), 563–617 (2021). Paper.
• OpenAI, Integer multiplication below n log n, preprint (23 September 2026), pinned manuscript revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source.
• D. Colkitt and community contributors, A sharper exponent for integer multiplication, research repository (2026), revision 56b66d58297deca1d7dd130247d720e960f77a37. Checkpoint and attribution.
• S. Jain, Integer multiplication: a conditional witness above $2^{-13}$ (integer-mult-kappa), research draft (2026), revision 5868dc701a9bec375c9dc5391d992ab3b8c35f3f. Round eight.

Motivation

Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an $O(n\log n)$ bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.

Setting

A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.

An input consists of two bit strings $x,y$ of the same positive length $n$, separated by $\#$. The strings are read most significant bit first, with leading zeros permitted. If $\operatorname{val}(x)$ denotes the represented natural number, the required output is exactly the $2n$-bit binary representation of $\operatorname{val}(x)\operatorname{val}(y)$, padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define $L(n)=\max(\lceil\log_2 n\rceil,1)$.

Target

The full target is

$$\mathrm{IntMul.KappaBound}(0.00006397891967576).$$

This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants $c>0$ and $n_0$ such that every pair of $n$-bit inputs, for $n\ge n_0$ and $n\ge1$, halts within

$$c\,n\,L(n)^{1-0.00006397891967576}$$

steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger $\kappa$ gives a stronger asymptotic saving because $L(n)\ge1$.

Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.

This entry: Jain, round seven

The value

$$\kappa=\frac{799736495947}{12500000000000000}=0.00006397891967576\;(>2^{-14})$$

is the conditional witness of S. Jain's integer-mult-kappa, round seven, at revision c05adfe, with the sharper moment certificate merged there (research/round7-moment-refinement/). The README's headline for the same construction is the slightly smaller $1599247689723/(2.5\cdot10^{16})\approx6.39699\times10^{-5}$; the refinement keeps the frozen round-seven bit network, histogram, complex saving and assembly unchanged, and replaces the reciprocal bound $e^u\le1/(1-u)$ in the moment certificate by a degree-eight Taylor enclosure, which certifies the bit saving $a_b=63983013240044/10^{18}$.

The construction builds on the OpenAI manuscript and on Colkitt's integer-mult-bounds (it uses the PR #62 producer with interval strips and core-aware pair assembly). Its new ingredients are lifted frames with late copies, deferred readouts, and per-use $V$ leaves on the bit side; the complex side is round six's. The repository states that the claim is conditional on the OpenAI manuscript and Colkitt's framework, that stage two (the complement time-reversal of stage one) is assumed rather than machine-checked, and that its Lean files check only finite rational statements (moment certificates and parameter assembly), not the analytic tail inequalities or the multiplication theorem. It has not had independent review.

Earlier claims appear as milestones: Harvey–van der Hoeven ($\kappa=0$), OpenAI Theorem 1 ($2^{-182}$), Colkitt's $2^{-30}$ checkpoint, Jain round six ($3666565558019/10^{17}$) and community PR #62 ($0.000051016920170078$). Each is implied by this goal because $L(n)^{1-\kappa}$ decreases in $\kappa$.

Significance

A proof for any positive value would give a strict asymptotic improvement over $n\log n$. Such an improvement would contradict the proposed $\Omega(n\log n)$ lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.

Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.

Difficulty

A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.

Formalization scope

The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.

The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.

Selected references

• D. Harvey and J. van der Hoeven, Integer multiplication in time O(n log n), Annals of Mathematics 193(2), 563–617 (2021). Paper.
• OpenAI, Integer multiplication below n log n, preprint (23 September 2026), pinned manuscript revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source.
• D. Colkitt and community contributors, A sharper exponent for integer multiplication, research repository (2026), revision 56b66d58297deca1d7dd130247d720e960f77a37. Checkpoint and attribution.
• S. Jain, Integer multiplication: a conditional witness above $2^{-14}$ (integer-mult-kappa), research draft (2026), revision c05adfe1dfe85326dd6dcf12bfd53f435bd49bf3. Round seven and the sharper moment certificate.

Prove that CLIQUE is NP-complete by reducing the existing 3-SAT language, KSat.KSAT 3, to it. An instance consists of a finite simple undirected graph and an input threshold; it asks whether the graph contains a clique of at least that size. (https://prove2.me/theorems/d82e8682-c490-4742-a5e5-dd3a0b870b90). The construction specializes Karp’s SAT-to-CLIQUE reduction to 3-SAT.

References:

• Richard M. Karp. Reducibility Among Combinatorial Problems. Complexity of Computer Computations, 85–103, 1972. Main Theorem, problem 3, p. 94; SAT-to-CLIQUE reduction, p. 97.

Motivation

Every generalization bound in chapters 2-5 is for binary classification. Most real-world classification problems have more than two classes, and the number of classes can itself be in the hundreds or thousands (topic classification, speech recognition). Chapter 9 extends the margin-based generalization theory of chapter 5 (SVMs) to this multi-class, mono-label setting, using the same Rademacher-complexity machinery as chunk 03-rademacher-vc, but with a new combinatorial ingredient — bounding the Rademacher complexity of a family built by taking a pointwise maximum over several hypothesis sets — needed because a multi-class prediction is itself an argmax over per-class scores.

Setting

A multi-class hypothesis is a scoring function $h:X\times Y\to\mathbb R$ with $Y=\{1,\dots,k\}$ (mono-label case); the predicted label is $\arg\max_y h(x,y)$, and the margin $\rho_h(x,y)=h(x,y)-\max_{y'\ne y}h(x,y')$ (p. 215) is negative exactly when $h$ misclassifies $(x,y)$. The empirical margin loss $\hat R_{S,\rho}(h)$ (Eq. 9.5) uses the same margin-loss function $\Phi_\rho$ (Definition 5.5) as chunk 05-svm, restated locally here. $\Pi_1(H) = \{x\mapsto h(x,y):y\in Y,h\in H\}$ (p. 217) projects a multi-class hypothesis set onto ordinary real-valued functions on $X$ — the object the chapter's Rademacher-complexity bound actually controls, since $H\subseteq\mathbb R^{X\times Y}$ has no norm of its own without such a projection. Lemma 9.1 is a purely combinatorial tool: the empirical Rademacher complexity of a family built by taking the pointwise max over $l$ hypothesis sets is bounded by the sum of their individual empirical Rademacher complexities — used to control the argmax structure of a multi-class prediction. Theorem 9.2 combines this with chunk 03's Rademacher-complexity generalization machinery (Theorem 3.3) to give the chapter's margin bound. Proposition 9.3 and Corollary 9.4 specialize this to kernel-based hypotheses, where each class has its own weight vector in a reproducing kernel Hilbert space and the $k$ weight vectors are jointly constrained by an $L^p$-type group norm $\|W\|_{H,p}\le\Lambda$.

Formalization targets

Lemma 9.1 (milestone). For $F_1,\dots,F_l$ hypothesis sets in $\mathbb R^X$, $l\ge1$, and $G=\{\max\{h_1,\dots,h_l\}:h_i\in F_i\}$: $\hat R_S(G)\le\sum_{j=1}^l\hat R_S(F_j)$.

Theorem 9.2 — the mission's goal. For $H\subseteq\mathbb R^{X\times Y}$, $Y=\{1,\dots,k\}$, fix $\rho>0$. For any $\delta>0$, with probability at least $1-\delta$, for all $h\in H$:

$$R(h) \le \hat R_{S,\rho}(h) + \tfrac{4k}\rho R_m(\Pi_1(H)) + \sqrt{\tfrac{\log(1/\delta)} {2m}}.$$

Proposition 9.3 (milestone). For a PDS kernel $K$ with feature map $\Phi$ and $K(x,x)\le r^2$: $R_m(\Pi_1(H_{K,p})) \le \sqrt{r^2\Lambda^2/m}$.

Corollary 9.4 (milestone). Under Proposition 9.3's hypotheses, fix $\rho>0$. For any $\delta>0$, with probability at least $1-\delta$, for all $h\in H_{K,p}$: $R(h) \le \hat R_{S,\rho}(h) + 4k\sqrt{r^2\Lambda^2/\rho^2/m} + \sqrt{\log(1/\delta)/(2m)}$.

Significance

Theorem 9.2 is the multi-class generalization of chunk 05-svm's Theorem 5.8, and its proof is the chapter's genuine new technique rather than a restatement: it needs a $k$-way application of Lemma 9.1 (once for the argmax structure of the margin, once summing over the $k$ possible labels), which is exactly where the $4k$ factor comes from. Corollary 9.4 is the direct theoretical basis for the multi-class SVM algorithm the chapter derives next (§9.3.1): the displayed dual optimization problem literally minimizes the right-hand side of the corollary's bound. No prior art exists on the platform: GET /theorems?q=multi-class%20classification returns zero hits, and chunk 03's Rademacher-complexity machinery (needed by the proof route) is a draft, not reusable, per the "drafts cannot import drafts" rule.

Difficulty

Lemma 9.1's proof is a genuine two-function argument (max as $\tfrac12(h_1+h_2+|h_1-h_2|)$, Talagrand's lemma applied to $|\cdot|$) generalized to $l$ functions by induction, not a one-line consequence of chunk 03's single-hypothesis-set bound. Theorem 9.2's own proof (PDF pp. 234-236) is the chapter's most involved: it introduces an auxiliary margin function $\rho_{\theta,h}$ with a free parameter $\theta$ later fixed to $2\rho$, splits the resulting Rademacher complexity into a "diagonal" term (bounded via a further one-hot decomposition across the $k$ classes, giving the first factor of $k$) and a "off-diagonal" term bounded via Lemma 9.1 (giving the second factor, folded into the same $4k$ constant). A formalization that stated Theorem 9.2 for $H$ itself rather than $\Pi_1(H)$, or that treated $k$ as an unrelated free constant rather than the actual number of classes, would misstate the theorem — precisely the pitfall BRIEF.md names for this chapter. Proposition 9.3's proof is a clean Cauchy-Schwarz/Jensen argument in the RKHS but needs the $L^p$-group-norm hypothesis class $H_{K,p}$ stated with its exact footnote definition (PDF p. 236), not a simplified $p=2$ special case.

Formalization scope

GeneralizationError, EmpiricalRademacherComplexity and RademacherComplexity are restated locally in this chunk's MultiClass namespace (the last two identical in content to chunk 03-rademacher-vc's own copies); MarginLossFunction restates chunk 05-svm's Definition 5.5 (the same function, needed here for this chapter's own EmpiricalMarginLoss); IsPDS restates chunk 06-kernels's PDS-kernel definition. All are duplicated rather than imported since a draft item cannot import another chunk's draft module, and none of 03, 05, 06 is listed as reusable in missions/README.md's "Published definitions" table at the time of this session. GeneralizationError is formalized via the book's own established equivalence "$h$ misclassifies $(x,y)$ iff $\rho_h(x,y)\le0$" (the form Theorem 9.2's own proof displays and works with), rather than via an explicit argmax classifier construction — checked as faithful, not a weakening, since it is exactly the quantity the chapter's proof bounds. MarginFunction's ⨆_{y'≠y} is a real supremum rather than a Finset.sup', avoiding a nonempty-finset side proof at definition time; every consuming theorem supplies 2 ≤ k (Y = Fin k) to guard it against trap 5. MaxFamily's index type is Fintype+Nonempty rather than a Finset-cardinality parameter l, a harmless generalization matching "l ≥ 1 hypothesis sets" via Nonempty. IsPDS's feature map Φ and its defining property K(x,y) = ⟪Φ(x),Φ(y)⟫ are supplied as hypotheses to the two kernel theorems rather than as a separate "feature mapping associated to a kernel" definition — the book itself treats this as a given correspondence, not a construction. No numerical constant is altered: 4k/ρ and log(1/δ) in Theorem 9.2, r²Λ²/m in Proposition 9.3, and 4k and r²Λ²/ρ²/m in Corollary 9.4 are exactly as displayed.

Not formalized: §9.1's discussion of the multi-label case (Eq. 9.2/9.3, the Hamming-distance risk) and Eq. 9.4 (empirical Hamming error) — background for a case this chapter's own generalization-bound section (§9.2) does not cover (the mono-label case only); the multi-class SVM primal/dual optimization problems (§9.3.1, an algorithm derived from Corollary 9.4, not a generalization-theoretic theorem); AdaBoost.MH (§9.3.2, a boosting algorithm, analyzed via a convex-surrogate argument rather than the Rademacher-complexity route this mission formalizes); and the uniform-over-$\rho$ extension mentioned at the end of the Theorem 9.2 proof (an unnumbered remark referencing Theorem 5.9's technique from a different chapter, not restated here). Drafting only the algorithmic consequences (the multi-class SVM's optimization problem) in place of the generalization bounds themselves would be this chapter's trivializing formalization.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 9.
• V. Koltchinskii, D. Panchenko, "Empirical margin distributions and bounding the generalization error of combined classifiers," Annals of Statistics 30(1), 2002 (Lemma 9.1's technique).
• K. Crammer, Y. Singer, "On the algorithmic implementation of multiclass kernel-based vector machines," JMLR 2, 2001 (the multi-class SVM algorithm §9.3.1 derives).

Motivation

Support vector machines were, for two decades, the workhorse of applied classification, and the reason offered for their success was always geometric: SVMs maximize the margin between the two classes. Chapter 3's VC-dimension bound cannot explain why this should help — for linear hypotheses in $\mathbb R^N$ its bound depends on $N+1$ and is uninformative whenever the feature dimension is large relative to the sample size, exactly the regime (kernel-induced or high-dimensional features) where SVMs are most often used. Chapter 5 answers the question this leaves open: a generalization bound for a real-valued hypothesis, stated in terms of its margin on the training sample, that does not depend on the ambient dimension at all. This is also the template every later chapter's margin bound specializes (multi-class classification, ranking, and, indirectly, boosting all reuse the same Rademacher-complexity-of-a-Lipschitz-loss argument developed here).

Setting

A hypothesis here is a real-valued function $h:X\to\mathbb R$, not (as in Chapters 2-3) a function into $\{-1,+1\}$: for a labeled point $(x,y)$ with $y\in\{-1,+1\}$, the sign of $h(x)$ gives the prediction and $|h(x)|$ is read as the classifier's confidence. The confidence margin of $h$ at $(x,y)$ is $y\,h(x)$; it is positive exactly when $h$ classifies $x$ correctly. For $\rho>0$, the $\rho$-margin loss $\Phi_\rho:\mathbb R\to\mathbb R$ (Definition 5.5) is

$$\Phi_\rho(x) = \min\Big(1,\max\Big(0,1-\frac x\rho\Big)\Big),$$

equal to $1$ when $x\le 0$ (misclassified), $0$ when $x\ge\rho$ (classified with confidence at least $\rho$), and interpolating linearly in between; it is $1/\rho$-Lipschitz. The empirical margin loss on a sample $S=(x_1,\dots,x_m)$ with labels $y_1,\dots,y_m$ (Definition 5.6) is $\hat R_{S,\rho}(h) = \frac1m\sum_{i=1}^m\Phi_\rho(y_ih(x_i))$ — the fraction of training points misclassified or classified with confidence below $\rho$, a strictly stronger requirement than plain misclassification. The (population) generalization error is $R(h)=\Pr_{(x,y)\sim D}[y\,h(x)\le 0]$. Rademacher complexity, $\hat R_S(H)$ and $R_m(H)$ (Definitions 3.1-3.2, restated here since chunk 03-rademacher-vc's own copies are still drafts), measure how well a real-valued hypothesis class $H$ correlates with random sign noise on a sample, and are the vehicle through which the margin bound's complexity term is expressed.

Formalization targets

Lemma 5.7 (Talagrand's lemma, milestone). For $l$-Lipschitz $\Phi_1,\dots,\Phi_m:\mathbb R\to\mathbb R$ and any hypothesis set $H$ of real-valued functions,

$$\frac1m\,\mathbb E_\sigma\Big[\sup_{h\in H}\sum_{i=1}^m\sigma_i(\Phi_i\circ h)(x_i)\Big] \le l\,\hat R_S(H).$$

Theorem 5.10 (Rademacher complexity of bounded-norm linear hypotheses, milestone). For $S\subseteq\{x:\|x\|\le r\}$ and $H=\{x\mapsto w\cdot x:\|w\|\le\Lambda\}$,

$$\hat R_S(H) \le \sqrt{r^2\Lambda^2/m}.$$

Corollary 5.11 (margin bound for linear hypotheses, milestone). For the same $H$ and $X\subseteq\{x:\|x\|\le r\}$, fixing $\rho>0$, with probability at least $1-\delta$,

$$R(h) \le \hat R_{S,\rho}(h) + 2\sqrt{\frac{r^2\Lambda^2/\rho^2}{m}} + \sqrt{\frac{\log(1/\delta)}{2m}} \quad\text{for all } h\in H.$$

Theorem 5.8 — the mission's goal. For any set $H$ of real-valued functions and $\rho>0$, with probability at least $1-\delta$, both

$$R(h) \le \hat R_{S,\rho}(h) + \frac2\rho R_m(H) + \sqrt{\frac{\log(1/\delta)}{2m}}$$ $$R(h) \le \hat R_{S,\rho}(h) + \frac2\rho \hat R_S(H) + 3\sqrt{\frac{\log(2/\delta)}{2m}}$$

hold simultaneously for all $h\in H$.

Significance

Theorem 5.8 is genuinely dimension-free: unlike Chapter 3's VC-dimension bound (5.36 in the book, restated from Corollary 3.19), it holds regardless of the ambient feature dimension $N$, depending instead only on the hypothesis class's Rademacher complexity and the chosen margin $\rho$. Specialized to bounded-norm linear hypotheses (Corollary 5.11), this gives the theoretical justification most often cited for SVMs and every other margin-maximization algorithm: whenever the training data admits a large geometric margin, the empirical margin loss at that margin is small (often zero, in the separable case) and the bound is tight regardless of $N$. Every later chapter's own margin bound (multi-class in Chapter 9, ranking in Chapter 10) is a direct structural descendant of Theorem 5.8's proof technique. No prior art on the Prove2Me platform is faithful: GET /theorems?q=support+vector+machine and q=margin+bound return no hits on this book's model (the two q=margin+bound hits found, both from the Aether Catalog, state a different comparison — a VC-type bound is eventually worse than a fixed Rademacher-type bound as a function of dimension — not Theorem 5.8 itself); q=Talagrand and q=contraction+principle return several hits (Ledoux/Talagrand convex-distance concentration, Rudin's Banach-space contraction-mapping theorem, a generic Rademacher-sign contraction lemma for quadratic sums) but every one states either a different mathematical object (metric-space fixed points, Talagrand's concentration inequality on product spaces) or a different idiom (squared vs. linear coordinate sums) from Lemma 5.7's function-composition contraction — none reused. All nine items are drafted fresh.

Not formalized here: Theorem 5.4 (the SVM sparsity/leave-one-out bound). It is listed as a candidate milestone in BRIEF.md, but its statement and proof depend on the primal/dual SVM optimization problem itself (the Lagrangian, KKT conditions, and the resulting definition of a "support vector" as a training point with nonzero dual coefficient) — a materially different, non-margin-based proof technique (leave-one-out stability of the trained hypothesis, via Lemma 5.3) that shares no definitions with the margin-bound family this mission's goal and other milestones are built on. Formalizing it faithfully would require standing up the SVM primal/dual formalism (Lagrangian, complementary slackness, the "support vector" predicate itself) from scratch, which is disproportionate to a single additional milestone within this mission's budget; per the captain brief's guidance to leave out, rather than approximate, a statement that cannot be made faithful in the time available, it is omitted.

Difficulty

The proof of Theorem 5.8 needs the empirical margin loss's zero-one-loss upper bound ($\mathbb 1_{u\le 0}\le\Phi_\rho(u)$) applied before invoking Theorem 3.3's Rademacher generalization bound on the composed class $\tilde{\tilde H}=\{\Phi_\rho\circ f: f\in\tilde H\}$, $\tilde H=\{(x,y)\mapsto y\,h(x):h\in H\}$ — reversing this order (bounding $R(h)$ by a Rademacher complexity computed on the zero-one loss directly) does not work, because the zero-one loss is not Lipschitz. Talagrand's lemma is exactly what lets the $1/\rho$-Lipschitz surrogate $\Phi_\rho$ be pulled outside the Rademacher complexity, at the cost of a factor $1/\rho$ and no worse; its own proof is an induction removing one Rademacher variable at a time, using a two-point supremum argument (fixing $\epsilon>0$, choosing near-optimal $h_1,h_2$) that does not simplify to anything less than genuine care with suprema of non-smooth objects — a formalization attempting to replace this with a naive linearity-of-expectation argument would be proving a false or vacuous statement, since $\sup$ does not commute with linear combinations. Theorem 5.10's bound needs the Cauchy-Schwarz and Jensen inequalities used in the particular order the book uses them (Cauchy-Schwarz on the empirical sup, then Jensen on the expectation of a norm, then the independence of the $\sigma_i$s) — the bound $\hat R_S(H)\le r\Lambda/\sqrt m$ does not follow from either inequality alone.

Formalization scope

EmpiricalRademacherComplexity/RademacherComplexity are restated locally in SVM, byte-identical to chunk 03-rademacher-vc's own copies (a draft item cannot import another chunk's draft module); this duplication collapses once 03-rademacher-vc is uploaded and listed in missions/README.md's "Published definitions" table. MarginGeneralizationError is a new, real-valued-hypothesis specialization of Definition 2.1 (R(h) = P[y h(x) ≤ 0]), distinct from every earlier chunk's {-1,+1}-valued GeneralizationError, since no earlier chunk's own copy matches this chapter's real-valued convention. PhiRho/EmpiricalMarginLoss are new. The goal theorem (margin_bound_binary_classification) states H's own Rademacher complexity computed on the marginal X-distribution (D.map Prod.fst), matching the book's final displayed form — the proof's intermediate step (the lifted class $\tilde H=\{(x,y)\mapsto y h(x)\}$ having the same Rademacher complexity as $H$ itself, since $y\in\{-1,+1\}$) is not separately drafted, only the theorem's statement. Theorem 5.10/Corollary 5.11 generalize the book's ambient $\mathbb R^N$ to an arbitrary real inner-product space X ([NormedAddCommGroup X] [InnerProductSpace ℝ X]), a harmless generalization since the book's proof (Cauchy-Schwarz, Jensen, orthogonality of Rademacher signs) uses only the inner-product structure, never finite dimension; [BorelSpace X] is added to Corollary 5.11's statement to make the measurable structure under which MarginGeneralizationError is well-posed explicit, since every x ↦ ⟨w, x⟩ is automatically Borel-measurable — not a substantive restriction, the book never discusses measurability of linear functionals. No numerical constant in any of the four theorems is altered from the book's own displayed form. A trivializing formalization this mission avoids: stating Theorem 5.8 only for a Finset/finite H (which would make it a disguised instance of Chapter 2's finite-hypothesis bound rather than the chapter's genuinely new, complexity-based argument) — H : Set (X → ℝ) is left fully general, exactly as the book states it.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 5.
• C. Cortes, V. Vapnik, "Support-vector networks," Machine Learning 20(3), 1995, 273-297.
• M. Talagrand, "Sharper bounds for Gaussian and empirical processes," The Annals of Probability 22(1), 1994, 28-76.
• P. Bartlett, S. Mendelson, "Rademacher and Gaussian complexities: risk bounds and structural results," Journal of Machine Learning Research 3, 2002, 463-482.

Motivation

Chapters 2 and 3 bound the estimation error of a hypothesis chosen from a fixed hypothesis set $H$, but the choice of $H$ itself is left open: a richer $H$ lowers the approximation error (how close $H$ comes to the Bayes classifier) at the price of a looser generalization bound, and a poorer $H$ does the reverse. Chapter 4 is the book's answer to this trade-off. It first shows that Empirical Risk Minimization (ERM) alone cannot resolve it — ERM ignores the complexity of $H$ entirely — and then develops Structural Risk Minimization (SRM): decompose a rich hypothesis set into a nested countable union $H=\bigcup_{k\ge1}H_k$ of increasingly complex pieces, and let the learning algorithm balance empirical fit against a complexity penalty for each $H_k$ automatically. The chapter closes by showing how the same balance can be achieved computationally through convex surrogate losses, whose minimization is tractable where minimizing the zero-one loss directly is not.

Setting

For a hypothesis $h$ chosen from $H$, the excess error $R(h)-R^*$ decomposes into an estimation term $R(h)-\inf_{h\in H}R(h)$ and an approximation term $\inf_{h\in H}R(h)-R^*$ (Eq. 4.1). Proposition 4.1 bounds ERM's estimation error by twice the uniform deviation $\sup_{h\in H}|R(h)-\hat R_S(h)|$. For a nested family $(H_k)_{k\ge1}$ and $h\in H$, $k(h)$ denotes the least index with $h\in H_{k(h)}$; SRM selects $h_S^{SRM}$ by minimizing $F_k(h)=\hat R_S(h)+R_m(H_k)+\sqrt{\log k/m}$ jointly over $k\ge1$ and $h\in H_k$, where $R_m(H_k)$ is $H_k$'s Rademacher complexity (Definitions 3.1/3.2, restated locally in this chunk's ModelSelection namespace). Theorem 4.2 is the resulting learning guarantee. Section 4.4 develops a competing model-selection procedure, cross-validation, and Theorem 4.4 directly compares its guarantee to SRM's on a held-out split of the sample. Section 4.7 turns to real-valued scoring functions $h:X\to\mathbb R$ with sign convention $f_h(x)=\mathrm{sign}(h(x))$ and a convex non-decreasing surrogate $\Phi$ of the zero-one loss; the Bayes scoring function $h^*(x)=\eta(x)-\tfrac12$ (Eq. 4.9) and the $\Phi$-loss $L_\Phi$ (Eq. 4.10) let Theorem 4.7 bound the true excess error by a power of the surrogate's own excess loss.

Formalization targets

Proposition 4.1 (ERM bound, milestone). For any sample $S$, $\Pr[R(h_S^{ERM}) - \inf_{h\in H}R(h) > \epsilon] \le \Pr[\sup_{h\in H}|R(h)-\hat R_S(h)| > \epsilon/2]$.

Theorem 4.2 — the mission's goal. For a nested countable union $H=\bigcup_{k\ge1}H_k$ and $h_S^{SRM}$ minimizing $F_k(h)$ over the whole union, for any $\delta>0$, with probability at least $1-\delta$:

$$R(h_S^{SRM}) \le \inf_{h\in H}\Big[R(h)+2R_m(H_{k(h)})+\sqrt{\tfrac{\log k(h)}m}\Big] + \sqrt{\tfrac{2\log(3/\delta)}m}.$$

Theorem 4.4 (Cross-validation versus SRM, milestone). Splitting a sample of size $m$ into $S_1$ (size $(1-\alpha)m$, training) and $S_2$ (size $\alpha m$, validation), for any $\delta>0$, with probability at least $1-\delta$:

$$R(h_S^{CV}) - R(h_{S_1}^{SRM}) \le 2\sqrt{\tfrac{\log\max(k(h_S^{CV}),k(h_{S_1}^{SRM}))}{\alpha m}} + 2\sqrt{\tfrac{\log(4/\delta)}{2\alpha m}}.$$

Theorem 4.7 (Convex-surrogate excess-error bound, milestone). For $\Phi$ convex and non-decreasing with $s\ge1,c>0$ satisfying $|h^*(x)|^s \le c^s(L_\Phi(x,0)-L_\Phi(x,h^*_\Phi(x)))$ for all $x$: $R(h)-R^* \le 2c(L_\Phi(h)-L^*_\Phi)^{1/s}$.

Significance

Theorem 4.2 is the chapter's headline result and the theoretical justification for regularization-based learning: it shows that a single algorithm, without knowing in advance which $H_k$ contains a good hypothesis, achieves a guarantee that is — up to the $\sqrt{\log k(h)/m}$ penalty — as favorable as if an oracle had revealed the best-in-class index in advance (Eq. 4.6). It is also the chapter's genuine new content beyond chunk 03-rademacher-vc's single-hypothesis-set bound: the countable union bound (a 1/k²-weighted union over $k\ge1$ converging to $\pi^2/6$, hence the $\log 3$ appearing in place of $\log 2$) is not a restatement of Theorem 3.3 but a distinct argument, and the goal's inf over the whole nested family is what makes SRM a model-selection method rather than a bound for one fixed $k$. Theorem 4.4 is the chapter's only head-to-head comparison between two competing model-selection procedures, on two genuinely different samples. Theorem 4.7 is the bridge between the learning-theoretic guarantees of chapters 2-4 and the actually-implemented convex optimization problems of chapters 5 (SVM), 6 (kernels) and beyond, all of which minimize a convex surrogate rather than the zero-one loss directly. No prior art exists on the platform: GET /theorems?q=structural%20risk%20minimization and GET /theorems?q=model%20selection both return zero hits.

Difficulty

Theorem 4.2's proof genuinely uses the union bound over a countably infinite family indexed by $k\ge1$ with weight $1/k^2$ converging to $\pi^2/6 < 2$ (Eq. 4.5) — this is the chapter's distinct new technique, not an application of chunk 03's finite/VC-dimension machinery to a single $H_k$; a formalization that stated the bound only for one fixed $k$, or dropped the inf over the whole union in favor of a single best-in-class $h^*$, would be Theorem 4.2's named trivializing formalization (BRIEF.md's pitfall note) rather than the theorem itself. Theorem 4.4 requires keeping two distinct samples ($S_1$, $S_2$, of different, precisely related sizes) and two distinct hypotheses ($h_S^{CV}$, $h_{S_1}^{SRM}$) apart throughout; conflating them collapses the comparison to a tautology. Theorem 4.7's difficulty is in its setup, not its statement: the Bayes scoring function, the $\Phi$-loss, and the pointwise $\Phi$-minimizer $h^*_\Phi$ (which the book allows to take the extended values $\pm\infty$ at the degenerate points $\eta(x)\in\{0,1\}$) all need care to state without silently altering the theorem's content.

Formalization scope

GeneralizationError, EmpiricalError, EmpiricalRademacherComplexity and RademacherComplexity are restated locally in this chunk's ModelSelection namespace (identical in content to chunk 03-rademacher-vc's own copies), since a draft item cannot import another chunk's draft module. LeastIndex H h (k(h)) is Nat.sInf {k | 1 ≤ k ∧ h ∈ H k}; every theorem using it carries the standing hypothesis that h lies in the relevant union, guarding against trap 5 (Nat.sInf of an empty set). Theorem 4.2's hSRM and Proposition 4.1's hERM are hypothesis-supplied functions satisfying the book's optimality property, not constructed via choice over an unconstrained H; H.Nonempty (Proposition 4.1) and (⋃ k ≥ 1, Hk k).Nonempty (Theorem 4.2) guard the outer sInf/inf terms against trap 5. Theorem 4.7's $h^*_\Phi$ is formalized as a real-valued function satisfying the pointwise minimization property for all $x$; the book's own extended-real convention ($h^*_\Phi(x)=\pm\infty$ exactly where $\eta(x)\in\{0,1\}$) is outside this formalization — disclosed here and in MODERATION_NOTES.md — since no real number satisfies the minimizing property at those degenerate points, the theorem as stated applies precisely to the case a real-valued $h^*_\Phi$ can be supplied, which is the book's own generic case. No numerical constant is altered from the book in any of the four theorems: 2 and log(3/δ) in Theorem 4.2, 2 (twice) and log(4/δ) in Theorem 4.4, and 2c and the exponent 1/s in Theorem 4.7 are exactly as displayed.

Not formalized: the discussion of computing $k^*$ via binary search (a computational, not a statistical, result); $n$-fold and leave-one-out cross-validation (Section 4.5, a practical variant of Theorem 4.4's two-sample cross-validation without its own numbered generalization bound); regularization-based algorithms (Section 4.6, the uncountable-union extension of SRM, which the book itself only sketches without a numbered theorem); Lemma 4.5 and Proposition 4.6 (intermediate results establishing that $h^*_\Phi$ induces the same classifier as $h^*$, needed for Theorem 4.7's proof but not part of its statement); and the worked examples for the hinge, exponential and logistic losses (instantiations of Theorem 4.7's $s,c$, not separate theorems). Drafting only these worked instantiations in place of Theorem 4.7's general statement would be a trivializing formalization for this chapter.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 4.
• V. Vapnik, Statistical Learning Theory, Wiley-Interscience, 1998 (structural risk minimization).
• T. Zhang, "Statistical behavior and consistency of classification methods based on convex risk minimization," Annals of Statistics 32(1), 2003 (Theorem 4.7's origin).