Motivation

Ranking is the learning problem behind search engines, recommendation systems and fraud-alert triage: what matters is not a single classification decision but the relative order the system assigns to a set of items, because a user or analyst can only act on the very top of a ranked list. Chapter 10 develops margin-based generalization theory for the score-based ranking setting, transplanting chunk 05-svm's single-sample Rademacher-complexity machinery to a genuinely two-sample structure: a ranking example is a pair of points, one drawn from each of two positions, and the chapter's bound must therefore control two marginal complexities rather than one. It also introduces RankBoost, the ranking analogue of AdaBoost, with a boosting-style empirical-error guarantee proved by the same normalization-factor telescoping argument as chunk 07's AdaBoost bound, adapted to RankBoost's own pairwise per-round quantities.

Setting

A ranking example is a pair (x,x') drawn from a distribution D over X×X, labeled by a preference function f; restricted to {-1,+1} labels (the simplification §10.2 adopts), a scoring function h:X→ℝ misranks (x,x') when f(x,x')(h(x')-h(x)) ≤ 0 (Eq. 10.1/10.2). The empirical margin loss R̂_{S,ρ}(h) (Eq. 10.3) uses the same Φ_ρ (Definition 5.5) as chunk 05-svm, restated locally here. Writing S1, S2 for the two coordinate projections of a pair sample S, and D1, D2 for the corresponding marginals of D, R_m^{D1}(H) and R_m^{D2}(H) are the Rademacher complexities of H under each marginal (p. 241). Theorem 10.1 bounds R(h) in terms of these two Rademacher-complexity terms, both in their population form (R_m^{D1}, R_m^{D2}) and their empirical form (R̂_{S1}, R̂_{S2}), via chunk 03's Theorem 3.3 applied through an auxiliary hypothesis family H̃ = {((x,x'),y) ↦ y[h(x')-h(x)]}. Corollary 10.2 specializes this to kernel-based linear scoring hypotheses; §10.4 introduces RankBoost (Figure 10.1), whose per-round weighted pairwise-outcome fractions ε_t^+, ε_t^- (Eq. 10.11) play the role AdaBoost's single ε_t plays in chunk 07, and Theorem 10.3 bounds RankBoost's empirical error in terms of them. Corollary 10.4 combines Theorem 10.1 with Lemma 7.4 (the convex hull of H has the same empirical Rademacher complexity as H, restated as a standing fact of the boosting series) to give RankBoost's own margin-based guarantee.

Formalization targets

Theorem 10.1 — the mission's goal. For H a set of real-valued functions, ρ>0, δ>0, with probability at least 1-δ, for all h∈H:

$$R(h) \le \hat R_{S,\rho}(h) + \tfrac2\rho(R_m^{D_1}(H)+R_m^{D_2}(H)) + \sqrt{\tfrac{\log(1/\delta)}{2m}}$$ $$R(h) \le \hat R_{S,\rho}(h) + \tfrac2\rho(\hat R_{S_1}(H)+\hat R_{S_2}(H)) + 3\sqrt{\tfrac{\log(2/\delta)}{2m}}.$$

Corollary 10.2 (milestone). For a PDS kernel K with r an upper bound on K(x,x), feature map Φ, and H = {x↦w·Φ(x) : ‖w‖≤Λ}, fixed ρ>0: R(h) ≤ R̂_{S,ρ}(h) + 4√(r²Λ²/ρ²/m) + √(log(1/δ)/(2m)).

Theorem 10.3 (milestone). RankBoost's empirical error verifies R̂_S(f) ≤ exp(-2∑_t((ε_t^+-ε_t^-)/2)²), and ≤ exp(-2γ²T) if the edge is uniformly at least γ>0.

Corollary 10.4 (milestone). Theorem 10.1's first bound, applied to h∈conv(H).

Significance

Theorem 10.1's proof is the chapter's genuine new technique, not a restatement of chunk 05's Theorem 5.8: the two-sample decomposition (splitting the supremum over H̃ into a term on x' alone and a term on x alone, each bounded by the Rademacher complexity under its own marginal) is what the 2/ρ · (R_m^{D1}+R_m^{D2}) structure expresses, and collapsing it to a single-sample bound would either be false or silently assume D1=D2 (which only holds for a symmetric D, an assumption the theorem does not make). Corollary 10.2 is the direct theoretical basis for the ranking SVM algorithm §10.3 derives. Theorem 10.3 mirrors chunk 07-boosting's Theorem 7.2 almost line for line in its proof technique (the same telescoping product of normalization factors Z_t), but with genuinely different per-round quantities (ε_t^+, ε_t^- rather than a single ε_t) that must not be conflated with AdaBoost's own, per BRIEF.md's pitfall note. Corollary 10.4 is what makes RankBoost's output (a linear, not convex, combination — normalized by ‖α‖_1) provably generalize independently of the number of boosting rounds T, the ranking analogue of chunk 07's Corollary 7.5. No prior art exists on the platform: GET /theorems?q=ranking%20loss returns zero hits.

Difficulty

Theorem 10.1's proof needs the two-sample structure carried through explicitly: H̃'s Rademacher complexity splits, via the sub-additivity of sup and the fact that y_iσ_i and σ_i have the same distribution, into a term on S2 alone and a term on S1 alone — treating a ranking sample as an ordinary single sample (chunk 03's single-hypothesis-set machinery applied naively) would drop this structure entirely and is exactly the pitfall BRIEF.md names. Theorem 10.3's proof requires Z_t = ε_t^0 + 2√(ε_t^+ε_t^-) be bounded via the identity 4ε_t^+ε_t^- = (1-ε_t^0)^2 - (ε_t^+-ε_t^-)^2 and the inequality 1-x ≤ e^{-x} — the same telescoping-normalizer technique as AdaBoost's Theorem 7.2, but RankBoost's own D_t, ε_t^+, ε_t^- genuinely differ (they are defined via pairwise outcomes y_i(h(x'_i)-h(x_i)) ∈ {-1,0,+1}, not a single-point disagreement h(x_i)≠y_i) and must be modeled as their own recursively-defined algorithm state, not obtained by substitution into chunk 07's AdaBoost Lean.

Formalization scope

MarginLossFunction restates chunk 05-svm's Definition 5.5; EmpiricalRademacherComplexity/ RademacherComplexity restate chunk 03-rademacher-vc's Definitions 3.1/3.2; IsPDS restates chunk 06-kernels's PDS-kernel definition; ConvHull restates chunk 07-boosting's convex-hull definition — all duplicated rather than imported since a draft item cannot import another chunk's draft module, and none is listed as reusable in missions/README.md's "Published definitions" table at the time of this session. D1, D2 are computed directly as Measure.map Prod.fst D/Measure.map Prod.snd D rather than posited via a separate marginal hypothesis, so the theorem statement itself pins down that they are genuinely the marginals of the sampling distribution D, not independent parameters. Corollary 10.2's r is an explicit upper bound on K(x,x) (hrK : ∀ x, K x x ≤ r) rather than a literal sSup, per BRIEF.md's pitfall note about the possibly-infinite supremum — the theorem's conclusion is monotonic in r, so this is not a weakening. RankBoost's D_t, ε_t^+, ε_t^-, α_t, Z_t and returned function f are modeled as their own recursively-defined algorithm state (mirroring chunk 07's AdaBoostDist/AdaBoostEpsilon/AdaBoostEnsemble pattern exactly, but built from RankBoost's own pairwise-outcome quantities, never by substituting into the AdaBoost Lean, per BRIEF.md's pitfall note) — RankBoostEpsilonPlus/RankBoostEpsilonMinus are already tied to RankBoost's own D_t and selected base ranker, so Theorem 10.3 needs no separate hypothesis connecting them (the same trivialization guard chunk 07's own Theorem 7.2 documents). No numerical constant is altered from the book in any of the four theorems.

Not formalized: §10.3's ranking-SVM primal/dual optimization problems (an algorithm derived from Corollary 10.2, not a generalization-theoretic result); §10.4.2 (RankBoost as coordinate descent, an algorithmic-equivalence argument, not a generalization bound); §10.5 (bipartite ranking, its own distinct problem formulation with a different generalization error, Eq. 10.20, explicitly out of scope per BRIEF.md); §10.6-10.7 (preference-based ranking, other criteria), out of scope per BRIEF.md. The uniform-over-ρ extension mentioned after both Theorem 10.1's and Corollary 10.2's proofs (referencing Theorem 5.9's technique from a different chapter) is not drafted, matching chunk 09-multiclass's identical scope decision for the analogous remark.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 10 (§10.1-10.4).
• Y. Freund, R. Iyer, R. E. Schapire, Y. Singer, "An efficient boosting algorithm for combining preferences," JMLR 4, 2003 (RankBoost's origin).
• C. Cortes, M. Mohri, "AUC optimization vs. error rate minimization," NeurIPS 2003 (the ranking-SVM connection §10.3 develops).

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

Chapter 2's finite-hypothesis-set learning bound is uninformative the moment $H$ is infinite — $\log|H|$ diverges — yet most hypothesis sets used in practice (linear separators, neural networks, decision trees) are infinite. Chapter 3 answers the question the previous chapter's own worked example (axis-aligned rectangles, Example 2.4) leaves open: is efficient learning from a finite sample still possible for an infinite hypothesis set, and can this be shown in general rather than case by case? The chapter's answer runs through two complementary notions of complexity — Rademacher complexity, a data-dependent measure of how well a function family correlates with random noise, and the VC-dimension, a purely combinatorial measure of the number of distinct labelings a hypothesis set can realize on a finite point set — connected by Massart's lemma and Sauer's lemma, and culminating in a generalization bound that replaces $\log|H|$ with the VC-dimension $d$.

Setting

For a family $G$ of functions $Z\to[0,1]$ and a sample $S=(z_1,\dots,z_m)$, the empirical Rademacher complexity $\hat R_S(G) = \mathbb E_\sigma[\sup_{g\in G}\frac1m\sum_i\sigma_i g(z_i)]$ (Definition 3.1) measures how well $G$ fits random sign noise $\sigma$ on $S$; the Rademacher complexity $R_m(G) = \mathbb E_{S\sim D^m}[\hat R_S(G)]$ (Definition 3.2) averages this over samples. Theorem 3.3 converts a Rademacher-complexity bound directly into a generalization bound via McDiarmid's inequality. For binary hypothesis sets $H\subseteq(X\to\{-1,+1\})$, the growth function $\Pi_H(m)$ (Definition 3.6) counts the maximum number of distinct dichotomies $H$ realizes on $m$ points, and the VC-dimension $\mathrm{VCdim}(H)$ (Definition 3.10) is the largest $m$ for which $\Pi_H(m)=2^m$ (i.e. $H$ shatters some set of $m$ points). Massart's lemma (Theorem 3.7) is the purely combinatorial tool bounding the expected maximum of a sum of signed vector components by $\sqrt{\log|A|}$, and Sauer's lemma (Theorem 3.17) bounds the growth function itself, by induction on $m+d$, whenever the VC-dimension is finite.

Formalization targets

Theorem 3.3 (Rademacher generalization bound, milestone). For $G:Z\to[0,1]$ and any $\delta>0$, with probability at least $1-\delta$ over an i.i.d. sample $S$ of size $m$, for all $g\in G$: $\mathbb E[g(z)] \le \frac1m\sum_i g(z_i) + 2R_m(G) + \sqrt{\log(1/\delta)/(2m)}$.

Theorem 3.7 (Massart's lemma, milestone). For a finite $A\subseteq\mathbb R^m$ with $r=\max_{x\in A}\|x\|_2$: $\mathbb E_\sigma[\frac1m\sup_{x\in A}\sum_i\sigma_i x_i] \le r\sqrt{2\log|A|/m}$.

Theorem 3.17 (Sauer's lemma, milestone). For $H$ with $\mathrm{VCdim}(H)=d$, for all $m\in\mathbb N$: $\Pi_H(m) \le \sum_{i=0}^d\binom{m}{i}$.

Corollary 3.19 — the mission's goal. For $H\subseteq(X\to\{-1,+1\})$ with $\mathrm{VCdim}(H)=d$ and any $\delta>0$, with probability at least $1-\delta$, for all $h\in H$:

$$R(h) \le \hat R_S(h) + \sqrt{\frac{2d\log(em/d)}{m}} + \sqrt{\frac{\log(1/\delta)}{2m}}.$$

Significance

Corollary 3.19 is the chapter's answer to the question chapter 2 leaves open: it is Theorem 2.13's direct infinite-hypothesis-set generalization, replacing $\log|H|$ (undefined for infinite $H$) with the VC-dimension $d$ (finite even for many infinite hypothesis sets, such as halfspaces in $\mathbb R^k$, which have VC-dimension $k+1$). It is also the template every later margin bound in the book specializes (Chapters 5, 9, 10's SVM, multi-class and ranking margin bounds all replace this bound's uniform $\log|H|$/VC-dimension term with a scale-sensitive complexity measure derived from the same Rademacher-complexity machinery), and Sauer's lemma is independently one of the most cited results in learning theory and extremal combinatorics. No prior art on the Prove2Me platform is faithful to any of this chapter's content: RademacherSymmetrization.radS_chernoff (Aether Catalog) proves a different, Massart-optimized Chernoff bound for the empirical Rademacher complexity of a finite class — a different object (empirical vs. population) with a different bound form from Theorem 3.3/3.5 — and sauerShelah_full proves only the trivial identity sauerShelahBound k k = 2^k, not Sauer's lemma itself. A further hit, sauer_shelah (Aether Catalog, Algebra/SauerShelah.lean), does state the Sauer-Shelah bound itself (F.card ≤ ∑_{i≤d} C(n,i) for a family F of subsets of Fin n shattering no set larger than d) — checked and not reused: it is a different idiom from Theorem 3.17 as this chunk needs it, a fixed finite ambient domain Fin n with F a Finset of its subsets directly, rather than the book's own growth function Π_H(m) (a supremum over point-tuples drawn from an arbitrary, possibly infinite X, Definition 3.6) that this chunk's other items and the goal (Corollary 3.19) are built on; reusing it would require either abandoning GrowthFunction/HasVCDim (needed faithfully by the goal itself) or a nontrivial reduction lemma this mission's budget does not include, so sauer_lemma is drafted fresh against this chunk's own GrowthFunction/HasVCDim. All ten items are drafted fresh.

Difficulty

Sauer's lemma's proof is a genuine two-parameter induction (on $m+d$) with a real combinatorial construction: restricting $H$ to a sample $S$ of size $m$, then splitting the restricted family into $G_1$ (its restriction to the first $m-1$ points) and $G_2$ (the concepts whose membership in $G$ changes with the addition of the $m$-th point), with $|G_1|+|G_2|=|G|$ and $\mathrm{VCdim}(G_2) \le \mathrm{VCdim}(G)-1$ — a genuinely combinatorial argument, not a statement that unfolds by simp; a weaker restatement using only the trivial bound $\Pi_H(m)\le 2^d$ would be true but is explicitly not what Theorem 3.17 states (BRIEF.md's named trivializing formalization for this chapter). Massart's lemma needs the expectation of a supremum over a finite set of $2^m$-many sign patterns kept as an honest average, not silently replaced by a looser union bound. Corollary 3.19's own $em/d$ term inside the logarithm needs the side condition $d\le m$ carried through explicitly — Corollary 3.18's own domain restricts to $m\ge d$, and the bound is false, not merely unproved, without it (at $m<d$, $em/d$ can be smaller than $1$, making the logarithm negative).

Formalization scope

GeneralizationError/EmpiricalError are restated locally in this chunk's RademacherVC namespace (byte-identical in content to chunk 02-pac's own copies), since a draft item cannot import another chunk's draft module; this duplication is expected and will collapse once 02-pac is moderated, uploaded and listed as reusable in missions/README.md's "Published definitions" table. EmpiricalRademacherComplexity/Massart's lemma model the Rademacher signs σ as ranging over the finite type Fin m → Bool rather than a measure-theoretic i.i.d. process, so the "expectation over σ" in both is the exact finite uniform average over its 2^m outcomes — faithful and simpler than a MeasureTheory construction, since σ's distribution really is uniform on a finite set of outcomes for every finite m. GrowthFunction takes a tuple of m points (Fin m → X) rather than a size-m subset of X, a harmless generalization (repeated points never increase the dichotomy count) documented in the item's own docstring. HasVCDim is a Prop parametrized by the candidate dimension rather than a total ℕ/ℕ∞-valued function, so it does not cover the book's VCdim(H)=+\infty case (Examples 3.15-3.16); every theorem using it takes HasVCDim H d as an explicit hypothesis, matching the book's own "let H... with VCdim(H)=d." Theorem 3.3 adds an explicit measurability hypothesis on G (hGm) beyond the book's own displayed statement, needed to keep the Bochner integral ∫ z, g z ∂D from silently evaluating to 0 for a non-measurable g — this is the book's own standing assumption (footnote 3, p. 30) made an explicit hypothesis rather than an implicit one. No numerical constant in any of the four theorems is altered from the book's own; Corollary 3.19's side condition d ≤ m is kept explicit, per BRIEF.md's pitfall note.

Not formalized: Lemma 3.4 and Theorem 3.5 (the binary-classification specialization of Theorem 3.3 via the zero-one-loss identity $\hat R_S(G)=\frac12\hat R_{S_X}(H)$), Corollary 3.8 and Corollary 3.9 (the intermediate Rademacher-to-growth-function and growth-function generalization bounds), and Corollary 3.18 (the VC-dimension bound on the growth function, $\Pi_H(m)\le(em/d)^d$ for $m\ge d$) — five intermediate results in the proof chain Theorem 3.3 → Theorem 3.5 → Corollary 3.8/3.9 → Sauer's lemma → Corollary 3.18 → Corollary 3.19 that are not independently drafted as milestones, per the budget guidance to keep a chunk to a goal plus its most load-bearing 3-8 milestones rather than every numbered result on the page; the three drafted milestones (Theorem 3.3, Massart's lemma, Sauer's lemma) are the chain's three genuinely distinct proof techniques (McDiarmid's inequality, a probabilistic-maximum bound, and a combinatorial induction), and the goal theorem's own statement is Corollary 3.19 exactly as displayed, not a restatement of any intermediate corollary. Radon's theorem (Theorem 3.13, background for the hyperplane VC-dimension example) and the worked VC-dimension examples (intervals, hyperplanes, rectangles, convex polygons, sine functions) are illustrations, not general results, and are not formalized — drafting only the example computations (e.g. VCdim(hyperplanes) = d+1) instead of the general finite-H machinery is exactly the trivializing formalization this mission avoids.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 3.
• V. Vapnik, A. Chervonenkis, "On the uniform convergence of relative frequencies of events to their probabilities," Theory of Probability and its Applications 16(2), 1971, 264-280.
• N. Sauer, "On the density of families of sets," Journal of Combinatorial Theory, Series A 13(1), 1972, 145-147.

Motivation

How many labeled examples does a learning algorithm need to see before its output generalizes well to unseen data? Chapter 2 of Foundations of Machine Learning answers this question for the simplest nontrivial setting — a finite hypothesis set — and in doing so introduces the book's central object, the Probably Approximately Correct (PAC) learning framework: a distribution-free, high-probability guarantee relating a learner's sample size to the accuracy and confidence of its output. Every later chapter's generalization bound (VC-based, Rademacher-based, margin-based) is a variant of the same "probability of a bad event is small" argument this chapter proves in its most elementary form, so getting the chapter's core definitions and its two bracketing theorems (consistent and inconsistent finite-$H$) right is the foundation the rest of the book's guarantees build on.

Setting

A learner sees a sample $S = (x_1,\dots,x_m)$ drawn i.i.d. from a fixed but unknown distribution $D$ on an instance space $X$, labeled by an unknown target concept $c$ drawn from a concept class $C$; a hypothesis $h$ from a fixed hypothesis set $H$ is judged by its generalization error $R(h) = \Pr_{x\sim D}[h(x)\ne c(x)]$ (Definition 2.1) against its empirical error $\hat R_S(h) = \frac1m\sum_i \mathbb 1_{h(x_i)\ne c(x_i)}$ (Definition 2.2) on the observed sample. A concept class is PAC-learnable (Definition 2.3) if some algorithm, given a polynomially-bounded number of samples, returns a hypothesis whose generalization error is at most $\epsilon$ with probability at least $1-\delta$, for every accuracy $\epsilon$ and confidence $\delta$ and every distribution $D$ — the "distribution-free" and "for all target concepts" character of the definition is what makes it a genuine worst-case learning guarantee rather than an average-case one tailored to a particular data-generating process.

Formalization targets

Theorem 2.5 (consistent case, milestone). If $H$ is finite and algorithm $A$ always returns a hypothesis consistent with the target concept on the training sample ($\hat R_S(h_S)=0$), then $\Pr_{S\sim D^m}[R(h_S)\le\epsilon]\ge1-\delta$ whenever $m \ge \frac1\epsilon(\log|H|+\log\frac1\delta)$.

Corollary 2.11 (single-hypothesis Hoeffding bound, milestone). For a fixed hypothesis $h:X\to\{0,1\}$ and any $\delta>0$, with probability at least $1-\delta$, $R(h) \le \hat R_S(h) + \sqrt{\log(2/\delta)/(2m)}$.

Theorem 2.13 (inconsistent case, goal). For a finite hypothesis set $H$ and any $\delta>0$, with probability at least $1-\delta$, simultaneously for every $h\in H$,

$$R(h) \le \hat R_S(h) + \sqrt{\frac{\log|H|+\log(2/\delta)}{2m}}.$$

Significance

Theorem 2.13 is the chapter's capstone because it removes Theorem 2.5's consistency requirement — the typical case in practice, where no hypothesis in $H$ perfectly fits the training data — while paying only an additive $\log|H|$ price inside the square root, via a union bound over $H$ applied to Corollary 2.11's per-hypothesis concentration bound. It is also the template every later generalization bound in the book refines: Chapter 3 replaces $\log|H|$ with the growth function / VC-dimension to handle infinite hypothesis sets, and Chapter 3's Rademacher-complexity bound is the direct machine-independent generalization of the same argument. No prior art on the Prove2Me platform is faithful to this chapter's PAC-learning content (GET /theorems?q=PAC-learnable returns no hits), so all six items are drafted fresh.

Difficulty

Theorem 2.13's own proof is a short combination of two ideas already present in the chapter (Corollary 2.11's Hoeffding bound plus a union bound over $|H|$ hypotheses), but each ingredient carries its own faithfulness burden. Corollary 2.11 needs the sample $S$ and the target hypothesis $h$ kept in the right relationship — $h$ fixed, $S$ random — for the bound to be Hoeffding's inequality and not a vacuous statement about a random hypothesis. Theorem 2.13 needs the $\forall h\in H$ quantifier placed inside the probability event (a single sample $S$ must work for every $h$ at once), not outside it (which would only assert each $h$'s bound holds with high probability for a sample chosen depending on $h$) — the difference between a uniform convergence bound and $|H|$ separate, weaker statements. Definition 2.3's "polynomial function $\mathrm{poly}(\cdot,\cdot,\cdot,\cdot)$" is a genuine formalization judgment call, addressed below.

Formalization scope

GeneralizationError/EmpiricalError are typed generally over $X, Y$ (matching Definition 2.1/2.2's own general statement, "$h : X\to Y$"), since Theorem 2.5 itself is stated for general $Y$, not just $Y=\mathrm{Bool}$; Corollary 2.11 and Theorem 2.13 specialize to $h : X\to\mathrm{Bool}$, matching their own explicit "$h:X\to\{0,1\}$" (Corollary 2.11) and the surrounding inconsistent-case section's restriction to binary classification. The i.i.d. sample $S\sim D^m$ is modeled as the identity random variable on the product-measure space $(\mathrm{Fin}\ m \to X,\ \mathrm{Measure.pi}(\lambda\_.\ D))$ in both Corollary 2.11 and Theorem 2.13, matching the book's own $S\sim D^m$ notation exactly. IsPACLearnable (Definition 2.3) makes "polynomial function" precise as a function bounded above by $K\cdot(a+b+n+s+1)^k$ for some constants $K>0$, $k\in\mathbb N$, uniform in its (nonnegative) arguments — the standard reading of "polynomial in its arguments" in the absence of a ready-made multivariate polynomial-growth predicate in Mathlib; dropping this constraint entirely (stating only "there is some threshold function") would silently weaken Definition 2.3 to a strictly easier notion of learnability, since virtually any finite or well-behaved concept class admits some (possibly super-polynomial) sample-complexity threshold — this is exactly the distinction Example 2.7 (the universal concept class) uses to demonstrate a class that is not PAC-learnable despite admitting a consistent hypothesis set. No numerical constant in Theorem 2.5, Corollary 2.11 or Theorem 2.13 is altered from the book's own; no upper bound on $\delta$ is added anywhere the book itself leaves it unrestricted (the theorems remain true, if vacuous, for $\delta>1$). Not formalized: the "efficiently PAC-learnable" running-time clause of Definition 2.3 (a second, independent polynomial-time condition on $A$ not needed by either milestone or the goal); Corollary 2.10 (the raw two-sided Hoeffding statement Corollary 2.11 is immediately derived from by solving for $\epsilon$, making it redundant with Corollary 2.11 as a formalization target); the axis-aligned-rectangles worked example (Example 2.4–2.9), which illustrates the framework rather than proving a new general result, and the trivializing formalization this chapter invites — reusing Mathlib's rectangle machinery to encode only the specific two-dimensional geometric argument rather than the general finite-$H$ theorems — is exactly what this mission avoids by drafting Theorems 2.5 and 2.13 in their general, hypothesis-set-agnostic form.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 2.
• W. Hoeffding, "Probability inequalities for sums of bounded random variables," Journal of the American Statistical Association 58(301), 1963, 13-30.

Algorithmic Game Theory III: Arrow and Gibbard–Satterthwaite

Motivation

Before a mechanism can pay anyone, it must decide something — and the impossibility theorems of social choice say that deciding honestly is already hard. Arrow's theorem (1951) showed that any method of aggregating individual rankings into a social ranking that respects unanimity and independence of irrelevant alternatives must be a dictatorship; Gibbard (1973) and Satterthwaite (1975) showed the voting analogue: any non-dictatorial voting rule onto three or more candidates can be strategically manipulated. These two results frame all of mechanism design — they are the reason Chapter 9 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), this mission's source, introduces money and quasilinear utilities immediately after proving them: without transfers, incentive compatibility is an impossibility, not a design constraint.

A timeline: Arrow proved the aggregation impossibility in his 1951 monograph Social Choice and Individual Values; Gibbard (1973) established the manipulability of non-dictatorial voting schemes via game forms, Satterthwaite (1975) independently via a direct argument; the derivation of Gibbard–Satterthwaite as a corollary of Arrow's theorem, which the book follows and this mission adopts as its attack path, is standard since the 1970s.

Setting

Fix a finite set $A$ of alternatives (candidates) and a finite set $\iota$ of voters. A preference is a strict total order on $A$; we write the relation as $r(a,b)$, read "$a$ is strictly preferred to $b$" (the book writes $b \prec a$). A preference profile assigns a preference to each voter. A social welfare function $F$ maps profiles to a social preference; a social choice function $f$ maps profiles to a single chosen alternative (Definition 9.1).

The properties at stake (Definitions 9.2, 9.4, 9.5, 9.7):

• $F$ satisfies unanimity if on every profile where all voters hold the identical preference $r$, the social preference is $r$.
• $F$ satisfies independence of irrelevant alternatives (IIA) if the social preference between $a$ and $b$ depends only on the voters' preferences between $a$ and $b$.
• Voter $i$ is a dictator in $F$ if the social preference always equals $i$'s; in $f$, if $f$ always elects $i$'s top alternative.
• $f$ is incentive compatible if no voter, by misreporting, can obtain an outcome they strictly prefer (under their true preference) to the truthful outcome; $f$ is monotone if whenever a single voter's change of vote moves the outcome from $a$ to $a' \ne a$, that voter ranked $a$ above $a'$ before and $a'$ above $a$ after.
• $f$ is onto if every alternative is elected on some profile.

Formalization targets

Goal (capstone) — Theorem 9.8, Gibbard–Satterthwaite

$$|A| \ge 3,\ f \text{ incentive compatible and onto } A \implies f \text{ is a dictatorship.}$$

Theorem 9.3 — Arrow

$$|A| \ge 3,\ F \text{ a social welfare function satisfying unanimity and IIA} \implies F \text{ is a dictatorship.}$$

Proposition 9.6 — incentive compatibility = monotonicity

$$f \text{ is incentive compatible} \iff f \text{ is monotone},$$

with no cardinality or finiteness assumptions: the two properties are quantifier-for-quantifier the same data viewed twice.

Significance

These are the two foundational impossibility theorems of social choice, and the pivot of the whole mechanism-design part of this series: the VCG mission that follows exists because Gibbard–Satterthwaite closes the door on non-trivial strategyproof choice without money. The chapter derives Gibbard–Satterthwaite from Arrow through the top-set extension (Definition 9.9, Lemmas 9.10–9.11), so a solver of the capstone gets Arrow as a stepping stone, not a detour.

Formalizing them produces the platform's first social-choice library: preference profiles as strict total orders, the aggregation vocabulary, and the impossibility pair. Arrow's theorem has been formalized before in other proof assistants (Nipkow's Isabelle formalization, 2009; a Mizar formalization by Wiedijk), which is evidence the statement shapes here are the standard ones — but no Lean 4/mathlib formalization exists, and none on this platform.

Difficulty

The proofs are short on paper and famously slippery in the details. Arrow's proof (the book gives Geanakoplos's pairwise-neutrality route) is a sequence of profile surgeries: each step swaps one voter's ranking of a pair and tracks the social outcome through IIA; the formal cost is constructing the intermediate profiles and proving they remain strict total orders — pure bookkeeping, but a lot of it. The hybrid-profile argument needs, over three or more alternatives, custom orders placing chosen pairs at chosen positions; building these on an abstract finite type is where most of the work lies. For the capstone, the book's route through the top-set extension $\prec^S$ (move $S$ to the top, Definition 9.9) requires proving the extension is again a strict total order (Lemma 9.10) and inherits unanimity, IIA, and non-dictatorship (Lemma 9.11); a solver may equally take any direct proof of Gibbard–Satterthwaite — the statement fixes no route. Proposition 9.6 is a genuine warm-up: unfolding both definitions and rearranging quantifiers.

Formalization scope

Preferences are relations A → A → Prop carrying IsStrictTotalOrder; r a b means "$a$ is strictly preferred to $b$", the reverse of the book's $\prec$ — every definition's docstring states this orientation. Aggregators are total functions on all relation-valued profiles; every property quantifies only over genuine preference profiles, so behavior on invalid inputs is irrelevant, and nothing can be smuggled through junk inputs. Unanimity is the book's identical-profile form (Definition 9.2), which together with IIA yields the pairwise form used in proofs. Both alternatives and voters are finite types; |A| ≥ 3 enters as 2 < Fintype.card A. Arrow's theorem carries Nonempty ι, matching the book's setting of $n \ge 1$ voters; it is not needed for truth — with zero voters the identical-profile unanimity is already unsatisfiable over three or more alternatives, so that case is vacuous either way. Gibbard–Satterthwaite deliberately omits it: with zero voters ontoness onto three alternatives is unsatisfiable, and the statement holds vacuously. Dictatorship for choice functions is Definition 9.7 exactly: whenever some alternative is the dictator's unique maximum, it is elected.

Selected references

• K. J. Arrow, Social Choice and Individual Values, Wiley, 1951 (2nd ed. 1963). Link
• A. Gibbard, Manipulation of voting schemes: a general result, Econometrica 41 (1973), 587–601. DOI
• M. A. Satterthwaite, Strategy-proofness and Arrow's conditions, Journal of Economic Theory 10 (1975), 187–217. DOI
• J. Geanakoplos, Three brief proofs of Arrow's impossibility theorem, Economic Theory 26 (2005), 211–215. DOI
• T. Nipkow, Social choice theory in HOL: Arrow and Gibbard–Satterthwaite, J. Automated Reasoning 43 (2009), 289–304. DOI
• N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 9, §9.2. DOI

Motivation

Equilibrium concepts are static; play is dynamic. The bridge between the two is regret minimization: simple adaptive rules that, against arbitrary — even adversarial — opponents, perform nearly as well as the best fixed alternative in hindsight. The subject begins with Hannan (1957) and Blackwell (1956), whose consistency theorems predate most of computational learning theory; the modern multiplicative-weights style bounds are due to Littlestone–Warmuth (1994) and Freund–Schapire (1997); the reduction from external to swap regret, and with it the algorithmic route to correlated equilibria, is Blum–Mansour (2005), following Foster–Vohra (1997) and Hart–Mas-Colell (2000). Chapter 4 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), written by Blum and Mansour, is the source text of this mission.

The punchline of the chapter, and of this mission, is that a computationally trivial form of rationality — each player privately running a no-swap-regret algorithm — drives the empirical play of any finite game into an approximate correlated equilibrium (Aumann, 1974). No coordination, no knowledge of the game, no fixed-point computation: the equilibrium concept that Chapter 1 of the series defines through a correlating device is reached by decentralized learning.

Setting

The online model (§4.2): there are $N$ actions. At each time $t$ an online algorithm selects a distribution $p^t$ over actions, as a function of the loss vectors observed so far; then the adversary reveals a loss vector $\ell^t \in [0,1]^N$ and the algorithm suffers $\sum_i p^t_i \ell^t_i$. Cumulatively, $L_H^T = \sum_{t \le T} \sum_i p^t_i \ell^t_i$ and $L_k^T = \sum_{t \le T} \ell^t_k$ for a fixed action $k$. The external regret of $H$ is $L_H^T - \min_k L_k^T$. A modification rule $F : \{1,\dots,N\} \to \{1,\dots,N\}$ rewires the algorithm's play, giving the modified loss $L_{H,F}^T = \sum_t \sum_i p^t_i\, \ell^t_{F(i)}$; the swap regret is $L_H^T - \min_F L_{H,F}^T$ over all $N^N$ rules.

A finite game (the vocabulary of Mission I of this series, in loss form): players $\iota$, finite action sets $S_i$, cost functions $c_i : \prod_j S_j \to \mathbb{R}$. A joint distribution $Q$ on action vectors is an $\varepsilon$-correlated equilibrium (Definition 4.11) if for every player $i$ and every switching rule $F : S_i \to S_i$,

$$\mathbb{E}_{s \sim Q}\big[c_i(s)\big] \;\le\; \mathbb{E}_{s \sim Q}\big[c_i(F(s_i), s_{-i})\big] + \varepsilon.$$

Formalization targets

Goal (capstone) — Corollary 4.16, explicit form

$$\forall N, T\ \exists H:\quad \text{swap regret of } H \text{ on every } [0,1]\text{-loss sequence} \;\le\; 2N\sqrt{T \ln N}.$$

An online algorithm with vanishing per-round swap regret, with the constant the chapter's own route produces.

Theorem 4.6 — Polynomial Weights

$$L_{PW}^T \;\le\; L_k^T + \eta\, Q_k^T + \frac{\ln N}{\eta}, \qquad Q_k^T = \sum_{t\le T} (\ell^t_k)^2, \quad 0 < \eta \le \tfrac12.$$

Theorem 4.9 — external regret in constant-sum games

A player with external regret $R$ over $T$ rounds has average loss at most $v_i + R/T$, where $v_i$ is the game value — no-regret play guarantees the minimax value against any opponent.

Theorem 4.15 — external-to-swap reduction

Any algorithm with external regret $\le R$ on all $[0,1]$-loss sequences yields one with swap regret $\le N R$.

Theorem 4.12 — swap regret bounds distance from correlated equilibrium

If every player's swap regret over $T$ steps of mixed play is at most $R$, the empirical joint distribution is an $(R/T)$-correlated equilibrium.

Theorem 4.3 — deterministic algorithms fail

Every deterministic algorithm has a $\{0,1\}$-loss sequence forcing loss $T$ while some action loses at most $\lfloor T/N \rfloor$: randomization is necessary, not a convenience.

Significance

Correlated equilibrium is the equilibrium concept with a defensible dynamic foundation: Nash equilibria are PPAD-hard to find, but the capstone plus Theorem 4.12 exhibit polynomial-time decentralized dynamics whose empirical play is an $\varepsilon$-correlated equilibrium after $T = O(N^2 \ln N / \varepsilon^2)$ rounds. Later missions in this series lean on this machinery: the price-of-anarchy chapters bound the cost of no-regret play (not just of exact equilibria), and the routing-game chapter uses precisely the convergence result formalized here.

Formalizing it produces the platform's first online-learning library: the adversarial protocol, regret in both external and swap forms, the multiplicative-weights analysis, and correlated equilibria. The regret vocabulary is directly reusable for the bandit-flavored missions already on the platform. All results are classical, with textbook proofs; the work requested is machine-checked proof, not new mathematics.

Difficulty

The Polynomial Weights bound is a potential-function argument: the total weight $W^t$ falls geometrically with the algorithm's loss and is bounded below by the weight of action $k$; the formal work is inequalities for $\ln(1-x)$ on $[0, 1/2]$ and careful bookkeeping of the recursion. The reduction (Theorem 4.15) is the structurally interesting step: the master algorithm runs $N$ copies of the external-regret procedure, feeds copy $i$ the true losses scaled by the master's own probability $p^t_i$, and — the crux — plays the stationary distribution $p^t = p^t Q^t$ of the column-stochastic matrix assembled from the copies' outputs. Existence of that fixed point is exactly the existence of a stationary distribution of a finite Markov chain, available on this platform as the goal of Markov Chains and Mixing Times I — or provable directly. Theorem 4.12 is an averaging argument, deliberately easy; Theorem 4.3 is an adversary construction; Theorem 4.9 combines the regret bound with the security level the minimax theorem of Mission I supplies, through the opponent's empirical mixture. The capstone is the composition of 4.6 (tuned at $\eta = \min\{\sqrt{\ln N / T}, 1/2\}$) with 4.15, plus the arithmetic that turns $N \cdot 2\sqrt{T \ln N}$ into the stated bound.

Formalization scope

An online algorithm is a deterministic function from the observed history (the list of past loss vectors) to the mixed action played next — the standard formal reading of the full-information model; randomization lives in the mixed action, and losses are expected losses. Boundedness of losses ($[0,1]$) is a hypothesis on theorems, never part of a definition. The Polynomial Weights algorithm is defined concretely by its weight recursion, and its learning rate carries the hypothesis $0 < \eta \le 1/2$: the book writes only $\eta \le 1/2$, but at $\eta = 0$ the bound's $\ln N / \eta$ term degenerates and the claim is false, so positivity is explicit. Action sets are Fin (n+1), keeping them nonempty. The number of steps $T$ is a known parameter (the book's convention; guess-and-double is out of scope). Correlated equilibria use the switching-rule form of Definition 4.11, over the game vocabulary (IsLottery, IsMixedProfile, profileProb) published with Mission I of this series. In Theorem 4.12 the empirical distribution is the average of product distributions of the played profiles, $T \ge 1$ is required (at $T = 0$ there is no empirical distribution), and costs are not assumed bounded — the averaging is scale-free.

Trivializing readings are ruled out: the existential algorithms in Theorem 4.15 and the capstone are quantified before the loss sequence and the modification rule, so a witness must work uniformly against every adversary — nothing may be chosen with hindsight.

Selected references

• A. Blum, Y. Mansour, From external to internal regret, JMLR 8 (2007), 1307–1324. Link
• N. Littlestone, M. K. Warmuth, The weighted majority algorithm, Information and Computation 108 (1994), 212–261. DOI
• D. P. Foster, R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997), 40–55. DOI
• S. Hart, A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68 (2000), 1127–1150. DOI
• N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 4. DOI

Motivation

Ramsey theory asks for the smallest number $R(k)$ such that every graph on $R(k)$ vertices contains either a clique of size $k$ or an independent set of size $k$. Beyond being one of the oldest problems in extremal combinatorics, Ramsey numbers sit at the junction of combinatorics, probability, and computer science: the two-coloring of edges they quantify is exactly the distinction between a graph and its complement, and their growth controls constructions used in derandomization and in the theory of Boolean functions.

This mission formalizes the paper that started the probabilistic method as a systematic tool: Erdős's 1947 proof that $R(k) > 2^{k/2}$. It is also the natural companion to the platform's Sipser–Gács–Lautemann mission: the union-bound argument formalized here is the same counting technique that drives the Lautemann lemma used to place $\mathsf{BPP}$ in $\Sigma_2^p$.

Timeline. Ramsey proved in 1928 that $R(k)$ is finite; Erdős and Szekeres gave the first upper bounds in 1935; Erdős's 1947 paper supplied the exponential lower bound $R(k) > 2^{k/2}$ by a one-page counting argument, introducing the probabilistic method. Better constants for specific regimes followed (Lovász local lemma 1975, Spencer 1977), but no general lower bound beyond $2^{(1+o(1))k/2}$ is known today.

Setting

Fix an integer $k \ge 3$ and put $N = 2^{\lfloor k/2 \rfloor}$. A graph is a pair $(V,E)$ with $E$ an irreflexive symmetric relation on $V$; here vertices are labeled $0, \dots, N-1$. A subset $s \subseteq V$ of size $k$ is a clique if every two distinct vertices of $s$ are adjacent, and an independent set if every two distinct vertices of $s$ are non-adjacent. A $k$-set that is either a clique or an independent set is monochromatic: it is monochromatic in the two-coloring of the complete graph on $V$ in which an edge is colored by the graph (present) or its complement (absent).

The ambient probability space is the uniform distribution over all graphs on $N$ labeled vertices — equivalently, each of the $\binom{N}{2}$ possible edges is present independently with probability $1/2$. This space has exactly $2^{\binom{N}{2}}$ elements.

A graph with no monochromatic $k$-set is a graph with neither a $k$-clique nor an independent $k$-set. The mission's goal, "the Ramsey number satisfies $R(k) > 2^{k/2}$", is formalized as the bare existence of such a graph on $N = 2^{\lfloor k/2 \rfloor}$ vertices, without defining the Ramsey number itself.

Formalization targets

Goal: the probabilistic lower bound

$$R(k) > 2^{k/2}, \qquad k \ge 3$$

i.e. there exists a graph on $N = 2^{\lfloor k/2 \rfloor}$ labeled vertices that contains no monochromatic $k$-set.

Stronger: the three steps of the proof, as separate targets

1. Count estimate. For $k \ge 3$ and $N = 2^{\lfloor k/2 \rfloor}$,

$$\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1, \qquad \text{equivalently} \quad \binom{N}{k} \cdot 2 < 2^{\binom{k}{2}}.$$

2. Union-bound principle. In any finite outcome space, if the total number of outcomes ruled out by all bad events together is less than the number of outcomes, some outcome avoids every bad event:

$$\sum_i \left| \{\omega : \mathrm{bad}\ i\ \omega\} \right| < |\Omega| \implies \exists\, \omega, \ \forall i,\ \neg \mathrm{bad}\ i\ \omega.$$

3. Pair-count bound. Over all graphs on $N$ vertices, the total number of pairs $(G, s)$ with $s$ a monochromatic $k$-set in $G$ is at most

$$\binom{N}{k} \cdot 2^{1+\binom{N}{2}-\binom{k}{2}}.$$

The goal follows by combining the three steps: the pair count is the sum over bad events in the union-bound principle, and the count estimate makes that sum smaller than the $2^{\binom{N}{2}}$ graphs.

Significance

The result. The lower bound $R(k) > 2^{k/2}$ is exponential, matching (up to the constant in the exponent) the best known upper bound $R(k) < 4^k$ from Erdős–Szekeres. It shows that the Ramsey function, despite being finite, grows genuinely fast — and the proof's method became more influential than the bound: the probabilistic method now permeates combinatorics, graph theory, and theoretical computer science (random graphs, discrepancy, property testing, derandomization).

Formalizing it. Mathlib currently contains no Ramsey theory at all: no definition of a Ramsey number and no lower bound. This mission closes that gap with the foundational result, in a way that is deliberately elementary — no measure theory, no randomness: the "probabilistic" argument is re-expressed as exact counting, which is why the statements are fully formalizable in Mathlib today. The union-bound principle (target 2) is a reusable lemma for future probabilistic-method formalizations, and the monochromatic-set infrastructure (targets 1 and 3) is the natural base layer for a future definition of the Ramsey number $R(k)$.

Difficulty

The central difficulty is that the bad events — "the $k$-set $s$ is monochromatic" — overlap heavily: a typical graph contains many monochromatic $k$-sets, so the union bound must be crude enough to survive the overlap. Concretely, the estimate $\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1$ holds for $N = 2^{\lfloor k/2 \rfloor}$ but fails for $N = 2^{\lfloor k/2 \rfloor+1}$; the naive "take one vertex more" step is where the argument breaks. A solver who tries to strengthen the bound will find the exponent is tight.

A second difficulty is purely formal: the uniform distribution over graphs has to be eliminated. The mission's statements do this by counting graphs with a fixed monochromatic $k$-set ($2^{1+\binom{N}{2}-\binom{k}{2}}$ of them) and applying the union-bound principle, so no probability theory enters the formalization.

Formalization scope

Representation. Graphs are SimpleGraph (Fin N): a relation on $N$ labeled vertices. A candidate set is a Finset (Fin N) of cardinality $k$; "monochromatic" is IsClique ∨ IsIndepSet on the graph; "no monochromatic $k$-set" is the predicate NoMonoK. All counting is cardinality of finite sets; monoCount N k G is the number of monochromatic $k$-sets of $G$.

Conventions. $N = 2^{\lfloor k/2 \rfloor}$ uses natural-number division, so for odd $k$ the graph lives on $2^{(k-1)/2}$ vertices — the standard reading of $R(k) > 2^{k/2}$. The hypothesis $k \ge 3$ is explicit. The theorem quantifies existence over all graphs; it does not define the Ramsey number $R(k)$ (a definition item for it, with the re-stated bound $R(k) > 2^{k/2}$, is a natural follow-up contribution).

Reusability. The union-bound principle, the monochromatic-$k$-set machinery, and the pair-count bound are all reusable beyond this mission. Welcome contributions: defining ramseyNumber and restating the bound as $R(k) > 2^{\lfloor k/2 \rfloor}$; the Erdős–Szekeres upper bound $R(k) \le 4^k$ as a companion mission; applications of the same principle elsewhere.

Selected references

• Paul Erdős, Some remarks on the theory of graphs, Bulletin of the American Mathematical Society 53(4), 1947, pp. 292–294. https://doi.org/10.1090/S0002-9904-1947-08785-X — the source paper: main construction proving $R(k) > 2^{k/2}$.
• Noga Alon, Joel H. Spencer, The Probabilistic Method, 4th ed., Wiley, 2016 — Chapter 1 (the Erdős lower bound) and Chapter 3 (Lovász local lemma); standard exposition of the technique.
• Stanisław Radziszowski, Small Ramsey Numbers, Electronic Journal of Combinatorics, Dynamic Survey DS1 — survey of Ramsey number bounds and history.

Context: where this sits in the formalization landscape

This mission is not a duplicate of existing platform content, and the choice of target is deliberate:

• Mathlib gap. The pinned environment (mathlib 0df444a) contains no Ramsey-number theory at all — nothing in Combinatorics/SimpleGraph, no ramseyNumber-style definition. This mission seeds that subfield with reusable infrastructure: the monochromatic-set model, the finite union-bound (probabilistic-method) principle, and the double-counting bound are all general-purpose lemmas, not one-off steps.
• Existing Ramsey content is a different quantity. The platform's fully-proved Erdos183 mission concerns multicolour triangle Ramsey numbers $R(3,\dots,3)$ and is driven by recursive palette constructions — a different Ramsey parameter and a different technique. The classical 2-colour diagonal bound formalized here appears nowhere on the platform as a proved statement.
• Directly load-bearing for a live open problem. The public open problem diagonal_ramsey_asymptotics (same environment 0df444a) asks, eventually in $k$, for $2^{\lfloor k/2 \rfloor} \le R(k,k) \le 4^k$; its upper half is already proved as ramsey_theory_upper_bound. The lower half is exactly what this mission's goal supplies: once ramsey_lower_bound is proved, closing that open problem reduces to a translation between the graph formulation used here (SimpleGraph / NoMonoK) and the edge-colouring formulation (ramseyDiag) used there, plus the eventual-quantifier wrapper.
• Formalization convention. The bound is stated on $N = 2^{\lfloor k/2 \rfloor}$ vertices (natural-number division), matching the exponent convention of the existing platform open problem above. For even $k$ this is exactly Erdős's $2^{k/2}$; for odd $k$ it is the standard floor form, equivalent to the classical asymptotic reading $R(k)^{1/k} \ge \sqrt{2}$.

The model

Fix $m \ge 1$ machines and $n$ jobs arriving one at a time in the order $0, \dots, n-1$. Job $i$ carries a whole vector of nonnegative loads $\tilde p(i,j)$, one per machine, with no assumed relationship between the entries — the same job may be cheap on one machine and unplaceable on another. This is the unrelated machines model. When job $i$ arrives its load vector becomes visible, and the algorithm must commit it to a single machine immediately and irrevocably, knowing nothing about the jobs still to come. A machine's load is the sum of $\tilde p(i,j)$ over the jobs assigned to it.

The setting formalized here is one normalized phase: loads are already scaled by a guessed makespan, so machine $j$ counts as eligible for job $i$ exactly when $\tilde p(i,j) \le 1$. The phase is allowed to give up rather than assign badly — it fails if an arriving job has no eligible machine, or if an internal weight grows past $1$.

The algorithm and the guarantee

The algorithm keeps a weight $x(j)$ per machine, initialized to $1/(2m)$. Job $i$ goes to the eligible machine $\ell$ minimizing $\tilde p(i,\ell)\, x(\ell)$; that machine's weight is then scaled by $1 + \tilde p(i,\ell)/2$, so a machine becomes exponentially unattractive as it fills. The weights are the primal variables of the covering LP

$$\min \sum_j x(j) + \sum_i z(i) \quad \text{s.t.} \quad \tilde p(i,j)\,x(j) + z(i) \ge 1 \ \text{ for every eligible pair } (i,j),$$

and each assignment raises one dual variable $y(i,\ell)$ to $1$. The guarantee follows from weak duality rather than a bespoke potential argument, which is the point of the primal-dual method.

The goal theorem states that if the dual admits a feasible solution putting unit total mass on every job — the certificate that the guessed makespan was large enough — then the phase does not fail, every job is assigned, and every machine ends with load

$$\sum_{i \,\text{assigned to}\, j} \tilde p(i,j) \ \le\ \frac{\ln(3m)}{\ln(3/2)}.$$

The source states this as $O(\log m)$; the explicit constant is what its proof yields.

Note that the load bound alone is not the theorem: it holds vacuously when the phase assigns nothing, and the milestones state it that way deliberately. The content is the conjunction of succeeded, assigns all, and the bound.

Scope

The doubling wrapper — guess a makespan, run a phase, double the guess and restart on failure — is what turns this phase into an $O(\log m)$-competitive online algorithm. It is outside this mission; the guarantee proved here is the conditional single-phase statement. The milestones break the argument into weak duality for finite LPs, the load bound, primal feasibility at each prefix, the primal objective identity, and the failure certificate.

Source

Niv Buchbinder and Joseph (Seffi) Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009, Chapter 8, pp. 193–196 (Theorem 8.1). PDF · doi:10.1561/0400000024

Motivation

Set cover is the standard worked example of the primal-dual method, and Chapter 2 of Buchbinder's thesis uses it that way: it is where the machinery of §2.1 is first turned on a concrete NP-hard problem. Two analyses appear. The greedy algorithm, analysed by dual fitting, buys the set with the best cost-per-newly-covered-element ratio and charges the price to the elements it covers; the resulting element prices form an infeasible dual that becomes feasible after scaling by $H_n$. The primal-dual algorithm instead raises the price of an uncovered element until some set's constraint goes tight, buys that set, and repeats; the resulting dual is feasible, and each bought set is paid for by elements of frequency at most $f$, giving an $f$-approximation.

Both analyses have the same shape, and it is the shape that matters for the rest of the series: the algorithm never sees the optimum. It maintains a dual solution, and the approximation ratio falls out of comparing the primal it built against the dual it accumulated.

Setting

An instance consists of a finite type $E$ of elements, a finite type $S$ indexing available sets, an assignment $s \mapsto A_s \subseteq E$, and a nonnegative cost $c : S \to \mathbb{R}$. Every element is assumed to lie in at least one available set; the source leaves this implicit, and without it no cover exists and the approximation statements are vacuous. The covering LP and its packing dual are

$$(P)\quad \min \sum_{s} c_s x_s \ \text{ s.t. } \sum_{s : e \in A_s} x_s \ \ge\ 1 \ \ (\forall e \in E), \quad x \ge 0,$$ $$(D)\quad \max \sum_{e} y_e \ \text{ s.t. } \sum_{e \in A_s} y_e \ \le\ c_s \ \ (\forall s \in S), \quad y \ge 0.$$

The frequency of an element is the number of sets containing it, and $f$ denotes the maximum frequency over all elements.

The two standing assumptions — nonnegative costs, and every element lying in some available set — are carried by a bundled SetCoverInstance, not passed as loose hypotheses. Every source-facing statement in the mission takes such an instance and reads those facts off its fields, so none of them can be instantiated at data violating either. The two indicator lemmas are the exceptions and are labelled as generalized assisting results: one has no cost function in scope at all, and the other's hypothesis that a given $C$ covers is strictly stronger than coverability of the family.

Costs are permitted to be zero and the ground type is permitted to be empty. No Nonempty E hypothesis appears anywhere; when $E$ is empty, $f = 0$ and the $f$-approximation bound reads $\mathrm{cost}(C) \le 0$, which the certificate's tightness clause forces to be $0 \le 0$ rather than anything false.

Formalization targets

The results are stated about certificates, not about executable algorithms. This is the central modelling decision of the mission and it is deliberate: the mathematical content of the source's proofs is entirely a statement about the invariants the output satisfies, and separating that from the question of whether a particular procedure produces such output keeps each half provable on its own.

A primal-dual certificate is a pair $(C, y)$ where $C \subseteq S$ covers $E$, $y$ is dual-feasible, and every $s \in C$ has a tight dual constraint, $\sum_{e \in A_s} y_e = c_s$.

Goal — the primal-dual $f$-approximation

For any primal-dual certificate $(C,y)$ and any fractional cover $x$,

$$\sum_{s \in C} c_s \ \le\ f \cdot \sum_{s \in S} c_s x_s .$$

Since this holds against every fractional cover, it holds in particular against an optimal one, so the cover $C$ costs at most $f$ times the fractional optimum and a fortiori at most $f$ times the integral optimum.

The double-counting step

The one substantive step of the goal is split out as its own target: for a primal-dual certificate,

$$\sum_{s \in C} c_s \ \le\ f \cdot \sum_{e \in E} y_e .$$

Tightness rewrites the cover's cost as a double sum over chosen sets and their elements; exchanging the order groups it by element, each charged at most $f$ times. With this and weak duality, the goal is two lines.

The greedy bound

A greedy certificate at ratio $\rho$ is a cover $C$ and a nonnegative $y$ with $\sum_{s \in C} c_s = \sum_{e} y_e$ and $\sum_{e \in A_s} y_e \le \rho\, c_s$ for every $s$. For such a certificate and any fractional cover $x$,

$$\sum_{s \in C} c_s \ \le\ \rho \cdot \sum_{s} c_s x_s .$$

Instantiating $\rho = H_n$ is what recovers the source's greedy guarantee; the harmonic bound itself is already in Mathlib.

Set-cover weak duality and LP attainment

Every dual packing is bounded by every fractional cover, $\sum_e y_e \le \sum_s c_s x_s$; the fractional optimum is at most the integral optimum; and both optima are attained, not merely bounded below. Attainment of the fractional optimum is a genuine linear-programming fact and is the hardest supporting item in the mission.

Significance

This is where the series first converts a dual-feasibility invariant into an approximation ratio on a concrete combinatorial problem, and the two certificate predicates are reused verbatim by the online covering missions later in the series. Set cover approximation has, as far as we can determine, no prior formalization in Mathlib or in any public Lean library: there is no set-cover problem statement, no greedy analysis, and no $f$-approximation result to build on.

Difficulty

The two certificate bounds are finite-summation arguments of moderate length — the work is in a double-counting step that reindexes a sum over chosen sets into a sum over elements, weighted by frequency. Attainment of the fractional optimum is different in kind: it needs a compactness or vertex argument about the covering polytope and is the item most likely to need real work. Zero-cost sets are permitted throughout, so any later algorithm definition that divides by a cost must handle that case explicitly.

Formalization scope

Definitions cover §2.2 of the source, excluding §2.2.2 (randomized rounding), which is deferred to a separate mission because its expected-cost and failure-probability analysis is measure-theoretic and shares no infrastructure with the deterministic results.

Two theorems are not in this mission: that the greedy algorithm produces a greedy certificate, and that the primal-dual algorithm produces a primal-dual certificate. Those require defining the algorithms and proving termination and coverage, and are planned as a second wave. Until that wave lands, the source's Theorems 2.4 and 2.6 should not be described as fully formalized — what this mission establishes is the certificate-to-ratio half of each.

Selected references

• Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008, §2.2, pp. 10–14. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
• Vijay V. Vazirani, Approximation Algorithms, Springer, 2001, Chapters 2 and 15 — the standard treatment of the greedy and primal-dual set-cover analyses.

Motivation

An online algorithm must commit to decisions before it knows the rest of its input, and it is judged by competitive analysis: the ratio between its cost and the cost of an optimal solution computed with full knowledge of the input. A recurring obstacle in this area is that each problem seems to need its own ad hoc potential-function argument. Buchbinder's thesis develops a single method that replaces those arguments — formulate the offline problem as a covering linear program, let the online algorithm raise the dual variables of its packing dual, and read the competitive ratio off the ratio between the primal and dual increments. The same recipe then yields algorithms for online set cover, weighted caching, ad-auction revenue, routing, and load balancing.

This mission formalizes the chapter where the method is introduced on its smallest example, the ski-rental problem. A customer needs skis for an unknown number of days: renting costs $1$ per day and buying costs $B$ once. The customer must decide, each morning, whether to rent again or buy, without knowing how many ski days remain. Despite its size the problem is the canonical rent-or-buy dilemma, and it has two classical tight results: a deterministic $2$-competitive algorithm, and a randomized algorithm whose competitive ratio tends to $e/(e-1)$, due to Karlin, Manasse, McGeoch and Owicki (1994). The primal-dual derivation of both is the content of Chapter 3.

Setting

An instance is a pair $(B, k)$: the purchase price $B$, a positive integer, and the number $k \ge 0$ of ski days, which the online algorithm does not know. An offline solution either buys at once, paying $B$, or rents on every day, paying $k$; so the offline optimum is

$$\mathrm{OPT}(B,k) \;=\; \min(B, k).$$

Chapter 3 casts this as a linear program (Figure 3.1, p. 18). The primal is a covering program with one buy variable $x$ and one rent variable $z_j$ per day $j$:

$$\text{minimize } \; B x + \sum_{j=1}^{k} z_j \quad \text{subject to} \quad x + z_j \ge 1 \ \text{ for each day } j.$$

Its dual is a packing program with one variable $y_j$ per day:

$$\text{maximize } \; \sum_{j=1}^{k} y_j \quad \text{subject to} \quad \sum_{j=1}^{k} y_j \le B, \qquad 0 \le y_j \le 1 .$$

The online structure enters in a single way: a new ski day appends a new covering constraint to the primal and a new variable to the dual, and previously raised primal variables may never be decreased. That monotonicity is what "previous decisions cannot be regretted" means formally.

The fractional primal-dual algorithm maintains $x$, initially $0$. On each new day, while $x < 1$ it sets $z_j \leftarrow 1 - x$, then raises

$$x \;\leftarrow\; x\left(1 + \tfrac{1}{B}\right) + \tfrac{1}{cB},$$

and sets $y_j \leftarrow 1$; once $x$ has reached $1$ it does nothing further. The free parameter $c$ is then pinned to the value that makes $x$ reach exactly $1$ after $B$ days,

$$c \;=\; \left(1 + \tfrac{1}{B}\right)^{B} - 1 .$$

Formalization targets

Goal — the fractional algorithm's competitive ratio at finite $B$

$$B\,x_k + \sum_{j=0}^{k-1} z_j \;\le\; \left(1 + \frac{1}{\left(1 + \frac{1}{B}\right)^{B} - 1}\right) \cdot \min(B, k) \qquad \text{for every } B \ge 1, \ k \ge 0 .$$

The coefficient is the exact finite-$B$ ratio $1 + 1/c$, left in closed form rather than replaced by a constant. This is deliberate: $\left(1+\frac1B\right)^B$ increases to $e$, so $c < e - 1$ and therefore $1 + 1/c > e/(e-1)$ for every finite $B$. A goal asserting $e/(e-1)$-competitiveness at finite $B$ would be false, and a goal asserting some rounded constant would be invalidated by any sharpening. The closed-form coefficient is the weakest statement that is stable under improvement.

Asymptotic companion — where $e/(e-1)$ actually lives

$$\lim_{B \to \infty} \left(1 + \frac{1}{\left(1 + \frac{1}{B}\right)^{B} - 1}\right) \;=\; \frac{e}{e-1} \;\approx\; 1.5819767 .$$

The classical constant is recorded here, as a limit of the coefficient sequence, and nowhere else.

Parallel target — the deterministic algorithm

$$\mathrm{detCost}(B,k) \;\le\; 2 \cdot \min(B,k), \qquad \mathrm{detCost}(B,k) = \begin{cases} k & k < B \\ 2B & k \ge B\end{cases}$$

Chapter 3's other result, independent of the fractional development.

Significance

The ski-rental bounds themselves are classical and tight, and nothing here is mathematically open. What the chapter contributes, and what this mission captures, is the derivation: it is the template instantiated by every later chapter of the thesis, so the artifacts built here — a covering/packing LP pair, its weak-duality instance, a monotone online variable with a closed-form growth law, and the primal-to-dual increment ratio as the source of the competitive factor — are the vocabulary in which the rest of the series will be stated.

On status: the mathematics is proved, published, and standard. It is not, to the best of a search of Mathlib at revision 0df444a, formalized — that revision contains no competitive-analysis or online-algorithm framework, no ski-rental development, and no general linear-programming weak-duality theorem. So the work this mission asks for is formalization of a known proof, not new mathematics, and the reusable output is infrastructure that does not currently exist in the library.

Difficulty

The offline problem is trivial, and a newcomer's first move — prove $\min(B,k)$ is the optimum and stop — solves the wrong problem. The content is entirely in the online constraint. Three specific places where the obvious argument stalls:

The optimum is never observed. The algorithm's cost must be compared against $\min(B,k)$ without $k$ being available to it. The comparison is routed through the dual instead: the dual objective the algorithm accumulates is a lower bound on every feasible primal solution, hence on the optimum, and the algorithm's own primal cost is a fixed multiple of that dual objective.

The growth law is piecewise. The update fires only while $x < 1$. Summing the per-day increments therefore does not telescope uniformly: days before $x$ reaches $1$ contribute $1 + 1/c$ each and later days contribute nothing, and the index at which the switch happens is exactly $B$ — which is a theorem about the recurrence, not an assumption.

The constant is forced, not chosen. $c = (1+1/B)^B - 1$ is not a free tuning parameter; it is the unique value for which the geometric sequence $x_j = \bigl((1+1/B)^j - 1\bigr)/c$ hits $1$ at $j = B$, which is in turn what makes the dual solution feasible ($\sum_j y_j \le B$). Dual feasibility and the choice of $c$ are the same fact.

Formalization scope

Conventions this development commits to. The purchase price is a natural number $B$ with $0 < B$, because Chapter 3 uses $B$ simultaneously as a price, as a day index ("buy skis on the $B$th day"), and as the exponent in $(1+1/B)^B$; costs are real numbers, with $B$ and $k$ coerced. Days are indexed from $0$, so day $j+1$ of the prose is index $j$, and Fin k indexes the $k$ days. Real division is total, so $1/0 = 0$; the hypothesis $0 < B$ is what keeps every reciprocal in the development genuine, and without it $c$ would evaluate to $0$ and the recurrence would collapse to the constant zero sequence. The algorithm's x < 1 guard is part of the formalized definition, not an informal aside: without it the cost would keep growing past day $B$.

A documented discrepancy in the source. The prose on p. 17 relaxes the integer program by letting $x$ and each $z_j$ range over $[0,1]$; Figure 3.1 on p. 18 prints only $x \ge 0$, $z_j \ge 0$. This mission takes the prose version, $0 \le x \le 1$ and $0 \le z_j \le 1$, as the canonical fractional program, and also records the nonnegativity-only region exactly as printed. Two separate theorems establish that both have least value $\min(B,k)$, so the discrepancy is resolved inside the mission rather than silently chosen. Solvers should note which of the two predicates a given statement uses.

Ruling out a trivializing formalization. The offline optimum is defined independently, as $\min(B,k)$, and is not derived from the algorithm's own behaviour; a separate theorem certifies that this value really is the least attainable objective value of the canonical program, so the goal cannot be satisfied by redefining the benchmark. The goal inequality is also tight — both sides are equal to $(1+1/c)$ times the number of days on which $x < 1$ — so it cannot be weakened into vacuity without becoming false.

Infrastructure, and what is reusable. The development needs only Mathlib big operators over Fin k, basic real analysis for the limit, and IsLeast. Two items are explicitly infrastructure rather than ski-rental content: the specialized weak-duality theorem for this covering/packing pair, and the Figure 3.1 optimum. Both are candidates for generalization by the later mission on Chapter 2's general linear-programming duality, and a solver who proves the general form there should expect this instance to be derivable from it rather than duplicated.

Out of scope here. The final paragraph of p. 19 rounds the fractional solution into a randomized algorithm by sampling a threshold $\alpha \in [0,1]$ uniformly and buying on the day whose increment of $x$ contains $\alpha$. That step needs a probability space and an expectation argument, and is deferred to the immediate follow-up mission, Primal-Dual Online Algorithms II: Randomized Rounding for Ski Rental. Contributions here should not anticipate it.

Selected references

• Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008. Chapter 3, pp. 17–19. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
• Niv Buchbinder and Joseph (Seffi) Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009. https://doi.org/10.1561/0400000024
• Anna R. Karlin, Mark S. Manasse, Lyle A. McGeoch and Susan Owicki, Competitive randomized algorithms for nonuniform problems, Algorithmica 11(6), 1994, 542–571. https://doi.org/10.1007/BF01294260
• Allan Borodin and Ran El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998.

Comparing undecidable problems

Computability theory studies which questions admit algorithms and how the unsolvable questions compare with one another. A decision problem can be represented by a set of natural numbers: the question on input $n$ is whether $n$ belongs to the set. Even when there is no algorithm that always answers this question, there may be an algorithm that eventually recognizes every positive instance. Understanding the relative difficulty of such problems is the setting of the Friedberg–Muchnik theorem.

The original paper by Richard M. Friedberg appeared in 1957 under the title Two recursively enumerable sets of incomparable degrees of unsolvability (solution of Post's problem, 1944). It supplies the historical paper source for this formalization. A. A. Muchnik's independent contribution appeared in Russian in 1956. Friedberg, PNAS 43(2), 236–238; Muchnik, Math-Net bibliography, 1956 entry.

Sets, enumeration, and oracle access

A set $A\subseteq\mathbb N$ is computably enumerable, abbreviated c.e., if membership has a semidecision procedure: on input $n$, the procedure halts exactly when $n\in A$. The older terminology is recursively enumerable, abbreviated r.e. The Lean predicate CEnumerable A uses Mathlib's REPred for this property. A computable set has a decision procedure that terminates on every input and answers membership correctly; this is expressed separately by ComputableSet A using ComputablePred.

For each set $A$, define its characteristic function by

$$\chi_A(n)=\begin{cases}1&n\in A,\\0&n\notin A.\end{cases}$$

An oracle for $A$ answers requests for this function's values. It always supplies an answer, even if membership in $A$ cannot be computed without an oracle. The declaration setOracle A represents this total function inside Mathlib's type of partial functions from natural numbers to natural numbers.

Write $A\le_T B$ when an algorithm with access to the membership oracle for $B$ computes $\chi_A$ on every input. This is Turing reducibility, expressed by SetTuringReducible A B. The algorithm may make several queries, with later queries depending on earlier answers. Incomparability requires both $A\not\le_T B$ and $B\not\le_T A$; it is stronger than saying the two sets merely have different degrees. These conventions specify the mathematical reading of the supplied Lean definitions.

Formalization target

The goal is the following unconditional existence statement:

$$\exists A,B\subseteq\mathbb N,\qquad A\text{ is c.e.}\ \land\ B\text{ is c.e.}\ \land\ A\not\le_T B\ \land\ B\not\le_T A.$$

Its Lean name is Computability.friedberg_muchnik. No enumeration, pair of sets, or oracle program is supplied as a hypothesis. Both sets must be obtained as witnesses to the conclusion. The statement matches Theorem 26.2 in Arnold W. Miller's Lecture notes in Recursion Theory, Section 26, with the theorem on page 51 and its proof on pages 51–54. Miller, December 3, 2008 version.

Mathematical and formal significance

The target establishes that the c.e. problems have incomparable levels of computational difficulty. Its witnesses cannot be computable: a computable membership procedure would also work in the presence of any other oracle simply by making no queries, contradicting the required nonreducibility. The stronger historical consequence is a positive solution of Post's problem: a c.e. degree can lie strictly between the computable degree and the halting degree. Miller records this consequence separately as Corollary 26.3 on page 54. Miller, Section 26.

The mathematical theorem is established; the work requested here is its Lean 4 formalization. A completed development must construct witnesses, prove their computable enumerability, and exclude oracle computations in each direction using Mathlib's actual reducibility relation. The provided goal currently ends in sorry. Successful compilation of this statement checks its formulation and imports; it does not constitute a proof of the existence result.

Difficulty of simultaneous requirements

The main obstacle is preserving decisions about oracle computations while both sets are still being enumerated. An additional element in one set can change an oracle answer used by an earlier computation, undermining the attempt to separate the other set from it. There are infinitely many candidate programs in both directions. Thus a formal treatment has to justify the eventual stability of the relevant computations as well as the effectiveness of the enumeration. This is the setting of the finite injury argument developed in Miller's proof of Theorem 26.2. Miller, pages 51–54.

Formalization scope

The sets are arbitrary Set ℕ, including the natural number zero in their ambient domain. The oracle answers use natural numbers, with one for membership and zero for nonmembership. Classical reasoning is used to define the oracle for an arbitrary set; it supplies no assertion that this function is computable. Each oracle is nevertheless total. Replacing it with a partial membership recognizer would change the meaning of the target.

The foundation consists of Mathlib.Computability.RE and Mathlib.Computability.TuringDegree, together with the supplied definitions in namespace Computability. SetTuringEquivalent records reducibility in both directions. degreeOfSet maps a characteristic-function oracle to its Turing degree, and CEnumerableDegree says that a degree has a c.e. representative. These additional definitions are retained as useful interfaces, while the root theorem itself is expressed directly with sets and TuringIncomparable.

A complete proof will need representations of effective finite stages and oracle computations, and lemmas relating those representations to the imported predicates. Such infrastructure can support later formalizations involving oracle use, computable enumerations, and priority constructions. Contributions should establish these connections with Mathlib's definitions and finish the unconditional target. The theorem must not be replaced by mere degree inequality, weakened reducibility, or a conditional assertion that assumes the required incomparable sets already exist.

Selected references

• Richard M. Friedberg, Two recursively enumerable sets of incomparable degrees of unsolvability (solution of Post's problem, 1944), Proceedings of the National Academy of Sciences of the USA 43(2), 236–238, 1957. DOI; free archived paper.
• A. A. Muchnik, On the unsolvability of the problem of reducibility in the theory of algorithms (Russian: Неразрешимость проблемы сводимости теории алгоритмов), Doklady Akademii Nauk SSSR 108(2), 194–197, 1956. Math-Net bibliography, 1956 entry.
• Arnold W. Miller, Lecture notes in Recursion Theory, University of Wisconsin–Madison, version dated December 3, 2008, Section 26, Theorem 26.2, pages 51–54. Author-hosted PDF.