All missions

Motivation

Stochastic fictitious play is a basic model of learning in repeated games. Each period every player best responds to the empirical frequencies of the opponents' past play, after the player's payoffs have been hit by a fresh random shock. It was introduced by Fudenberg and Kreps (1993), is a standard object in the theory of learning in games (Fudenberg and Levine, The Theory of Learning in Games, 1998), and underlies the quantal-response and logit-learning models used in experimental economics and multi-agent reinforcement learning. The question is whether the players' beliefs settle down, and on what.

Potential games, in which all players receive the same payoff, cover pure coordination games and, after the usual payoff transformations, congestion games and weighted potential games. For them Hofbauer and Sandholm (Econometrica 70, 2002) proved that stochastic fictitious play converges almost surely, and that under a generic regularity condition the limit is a single linearly stable rest point of the perturbed best response dynamic.

Timeline. Fudenberg and Kreps (1993) and Kaniovski and Young (1995) established convergence in 2×2 games. Benaïm and Hirsch (1999) related the process to its mean ordinary differential equation and proved convergence in some $p$ player, two strategy games. Hofbauer (2000) and Hofbauer and Hopkins (2000) constructed Lyapunov functions for the deterministically perturbed dynamics. Hofbauer and Sandholm (2002) combined these with a representation theorem for random utility models and with Pemantle's (1990) nonconvergence theorem to obtain the result formalized here.

Setting

A $p$ player game has finite strategy sets $S^\alpha = \{0,\dots,n^\alpha-1\}$ and utilities $u^\alpha : S \to \mathbb R$ on pure profiles $S = \prod_\beta S^\beta$. The game is a potential game if $u^\alpha(s) = u^\beta(s)$ for all players and all profiles. Mixed profiles form $\Sigma = \prod_\alpha \Delta S^\alpha$, and player $\alpha$'s payoff vector is $U^\alpha_i(x^{-\alpha}) = \sum_{s:\,s^\alpha=i} u^\alpha(s)\prod_{\beta\ne\alpha}x^\beta_{s^\beta}$.

Player $\alpha$'s payoffs are perturbed by a random vector $\varepsilon^\alpha$ with a strictly positive density $f^\alpha$ on $\mathbb R^{n^\alpha}$. The choice function is $C^\alpha_i(\pi) = P(\arg\max_j \pi_j + \varepsilon^\alpha_j = i)$, assumed continuously differentiable, and the perturbed best response is $\tilde B^\alpha(x^{-\alpha}) = C^\alpha(U^\alpha(x^{-\alpha}))$.

In standard stochastic fictitious play, shocks $\varepsilon^\alpha_t$ are independent over time and across players. From an arbitrary initial pure profile, at time $t+1$ each player plays a maximizer of $U^\alpha_k(Z_t^{-\alpha}) + (\varepsilon^\alpha_t)_k$, where the beliefs are the time averages

$$Z_t = \frac1t\sum_{u=1}^t \zeta_u .$$

The mean dynamic of this process is the perturbed best response dynamic

$$(P)\qquad \dot x^\alpha = \tilde B^\alpha(x^{-\alpha}) - x^\alpha .$$

A rest point $x^*$ of (P) is hyperbolic if every eigenvalue of $DF(x^*)$ restricted to the tangent space $\prod_\alpha \mathbb R^{n^\alpha}_0$ of $\Sigma$ has nonzero real part, and linearly stable if every such eigenvalue has negative real part. $RP(P)$ and $LS(P)$ denote the rest points and the linearly stable rest points.

By Theorem 2.1 of the paper, $C^\alpha(\pi) = \arg\max_{y\in\operatorname{int}\Delta}(y\cdot\pi - V^\alpha(y))$ for an admissible deterministic perturbation $V^\alpha$, so (P) coincides with the deterministically perturbed dynamic (PV), in which the argmax replaces $C^\alpha$.

Formalization targets

Goal: Theorem 6.1(iii)

For every potential game, every family of densities meeting the conditions above, every probability space, independent shock family and initial profile:

1. if the shocks are smooth enough that the $V^\alpha$ are $C^N$, $N = \sum_\alpha(n^\alpha-1)$, then

$$P\big(\omega(Z_t)\text{ is a connected subset of } RP(P)\big) = 1;$$

2. if every rest point of (P) is hyperbolic and the field of (P) is $C^2$, then

$$P\Big(\lim_{t\to\infty} Z_t \text{ exists and lies in } LS(P)\Big) = 1.$$

Milestones

In attack order: Theorem 2.1 (the representation), Proposition 4.1 (the function $\Pi(x) = \sum_s u^1(s)\prod_\alpha x^\alpha_{s^\alpha} - \sum_\alpha V^\alpha(x^\alpha)$ is a strict Lyapunov function for (PV)), the identification of the critical points of $\Pi$ with the rest points of (PV), Proposition 4.2 ($CR(PV) = RP(PV)$ under $C^N$ smoothness), Proposition 4.3 (under hyperbolicity $RP(PV)$ is finite and equals $CR(PV)$), and Lemmas A.5 and A.4 (a uniform nondegeneracy condition for the noise of the process).

Significance

The result. Theorem 6.1(iii) says that decentralised, boundedly rational learning in common-interest games does not cycle or wander: beliefs converge to a rest point of the perturbed dynamic, and generically to one that is linearly stable, hence a local maximizer of the perturbed potential $\Pi$. Rest points approximate Nash equilibria as the noise vanishes (Proposition 3.1 of the paper), so the theorem is a selection result for equilibria reached by learning. It is also a template for the stochastic-approximation analysis of learning algorithms whose mean dynamic has a Lyapunov function.

Formalizing it. The theorem is proved in the paper, but none of its ingredients is machine-checked: the random utility representation, chain recurrence of flows, Lyapunov arguments for (PV), and the stochastic-approximation step (Benaïm–Hirsch, Benaïm, Pemantle) are all absent from Mathlib and from this platform. A complete development produces a reusable stochastic-approximation layer, not only this theorem.

Difficulty

The obvious argument, "(P) has a strict Lyapunov function, so the process converges to its rest points", fails twice. First, a strict Lyapunov function does not by itself make every chain recurrent point a rest point (the paper cites counterexamples of Akin and of Benaïm); the step needs either Sard's theorem for a $C^N$ function or finiteness of the rest points, and the stochastic-approximation theory controls the process only through the chain recurrent set. Second, convergence to linearly stable points requires showing that the process avoids unstable rest points. This rests on Pemantle's theorem, whose nondegeneracy hypothesis must be verified uniformly over states and directions (Lemma A.4). Neither step follows from the ODE alone: the theorem is about the random process $Z_t$.

Formalization scope

Players are Fin p with p ≥ 2, strategies Fin (n α) with n α ≥ 1, and mixed profiles live in the ambient space (α : Fin p) → Fin (n α) → ℝ, on which every vector field is defined. Choice probabilities are probabilities of strict argmax events under volume.withDensity (f α). The process $Z_t$ is defined pathwise from the shocks, ties broken by the smallest index (a null event), and the theorem quantifies over every probability space and every independent shock family with the given laws. Derivatives of $V^\alpha$ are those of $V^\alpha$ composed with the projection onto the plane $\sum_i y_i = 1$. Eigenvalues are the complex roots of the characteristic polynomial of the derivative restricted to the tangent space of $\Sigma$. Solutions of a dynamic are differentiable curves on $[0,\infty)$ that stay in $\Sigma$, and chain recurrence uses $\varepsilon$-chains with times $t_i \ge 1$.

A formalization about the ODE (P) in place of the process $Z_t$, a fixed noise law such as logit, or convergence to $RP(P)$ in place of $LS(P)$ would prove a different and weaker statement. These are excluded.

Needed infrastructure: the random utility representation (mission I of this series), flows and chain recurrence of $C^1$ vector fields on compact sets, Sard's theorem for real-valued $C^N$ functions, and the stochastic-approximation theorems of Benaïm–Hirsch (1999, Thm 3.3), Benaïm (1999, Props. 5.3 and 6.4) and Pemantle (1990, Thm 1). The last three are reusable well beyond this mission, and contributions of any of them are welcome.

Selected references

• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70(6), 2265–2294, 2002. https://doi.org/10.1111/1468-0262.00376
• M. Benaïm and M. W. Hirsch, Mixed Equilibria and Dynamical Systems Arising from Fictitious Play in Perturbed Games, Games and Economic Behavior 29, 36–72, 1999. https://doi.org/10.1006/game.1999.0717
• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, 1–68, 1999. https://doi.org/10.1007/BFb0096509
• R. Pemantle, Nonconvergence to Unstable Points in Urn Models and Stochastic Approximations, Annals of Probability 18(2), 698–712, 1990. https://doi.org/10.1214/aop/1176990853
• D. Fudenberg and D. M. Kreps, Learning Mixed Equilibria, Games and Economic Behavior 5, 320–367, 1993. https://doi.org/10.1006/game.1993.1021
• J. Hofbauer and E. Hopkins, Learning in Perturbed Asymmetric Games, Games and Economic Behavior 52, 133–152, 2005. https://doi.org/10.1016/j.geb.2004.06.006

Motivation

Chapter 6 built lift-and-project (L&P) cuts from a cut-generating LP, and Chapter 7 surveyed alternative nonlinear constructions reaching the same integer hull. This chapter asks a sharper question: how do L&P cuts relate, coefficient for coefficient, to older, more classical cutting planes — simple disjunctive cuts and mixed integer Gomory cuts, derived directly from a simplex tableau rather than from an auxiliary LP? The answer is an exact correspondence: every L&P cut from a basic solution of the cut-generating LP is equivalent to a specific simple disjunctive cut from a specific tableau basis, and conversely. This correspondence is not merely of theoretical interest — it converts a question about an infinite family of cuts into a finite, countable one (bases of a linear system), and it is what lets the chapter's capstone result, Theorem 8.7, establish a uniform rank bound of $p$ (the number of 0-1 variables) across four cut families at once, by proving it for one and transporting the proof to the other three.

Setting

$(CGLP)_k$ (eq. (8.1)) is the cut-generating LP for the disjunction $-x_k \ge 0 \lor x_k \ge 1$, with an added normalization constraint $ue+u_0+ve+v_0=1$ that makes its feasible polytope bounded — so a "basic solution" can be identified with an extreme point of that polytope. Given a basic solution with $u_0,v_0>0$ and basic $u/v$-components indexed by $M_1,M_2$ (Lemma 8.1-8.2), the $n\times n$ submatrix $\hat A$ of $\tilde A$ indexed by $J:=M_1\cup M_2$ is nonsingular, giving a simplex tableau in which $x_k$ is expressed as $x_k = \bar a_{k0} - \sum_{j\in J}\bar a_{kj}x_j$ (eq. (8.5)). The simple disjunctive cut from $x_k\le 0 \lor x_k\ge 1$ applied to this row has coefficients $\pi_j := \max\{\pi^1_j,\pi^2_j\}$, $\pi_0 := \bar a_{k0}(1-\bar a_{k0})$ (eq. (8.7)-(8.8)).

Formalization targets

Theorem 8.7 (goal) — a uniform rank bound across four cut families

The rank of the LP relaxation $P$ with respect to (a) unstrengthened L&P cuts, (b) simple disjunctive cuts, (c) strengthened L&P cuts, (d) mixed integer Gomory cuts (equivalently, strengthened simple disjunctive cuts) is at most $p$, the number of 0-1 variables.

The chain of results building toward it

Lemma 8.1 (basicness forces $u_0,v_0>0$), Lemma 8.2 (a basic solution's index sets give a nonsingular submatrix), Lemma 8.3 ($0<\bar a_{k0}<1$), Theorem 8.4A (a basic L&P cut equals a simple disjunctive cut), Theorem 8.4B (the converse: every simple disjunctive cut from a valid basis equals some basic L&P cut), and Theorem 8.5 (the same correspondence, strengthened).

Significance

The results themselves. Theorems 8.4A/8.4B are, in the book's own words, an "exact correspondence between lift-and-project cuts for a mixed 0-1 program and earlier cuts from the literature" — placing L&P cuts, simple disjunctive cuts, and (via Theorem 8.5) mixed integer Gomory cuts on the same logical footing, all generated by choosing a basis of one underlying linear system. Theorem 8.7 is the payoff: a single uniform bound covering four cut families that the literature had previously bounded (if at all) by separate arguments, and by contrast to the unbounded rank of pure-integer fractional Gomory cuts, exhibiting a case where the mixed 0-1 structure yields much stronger guarantees.

Formalizing it. No object in this mission exists on the platform prior to it or in Mathlib. This mission restates 06-lift-project-cuts's $(CGLP)$ apparatus and Theorem 6.4's strengthened cut formula locally, per the series convention that a draft mission cannot import another draft mission's definitions, adapted throughout to this chapter's normalized $(CGLP)_k$ and its disjunction on a single fixed coordinate $k$.

Difficulty

Formalizing "basic solution" required a genuine choice: unlike Chapter 6, $(CGLP)_k$'s normalization constraint makes its feasible set a bounded polytope, so this mission identifies "basic solution" with an extreme point of that polytope (Set.extremePoints) for Lemma 8.1 (whose own statement has no reference to specific index sets), while Lemmas 8.2 onward take the basic index sets $M_1,M_2$ directly as hypothesis data, matching how those theorems are themselves phrased ("let the basic components... be indexed by $M_1$ and $M_2$"). Theorem 8.7's rank bound required designing one generic HasRankAtMost predicate, parametrized by an abstract cut-closure operator, applicable uniformly to all four families — mirroring the book's own proof structure, which establishes the bound for one family and transports it to the other three via Theorems 8.4A/8.4B and 8.5, rather than arguing each part from scratch.

Formalization scope

The row/variable identification gap (see MODERATION_NOTES.md). The book's own eq. (8.4)- (8.5) identifies certain rows of the augmented, $m+p+n$-row matrix $\tilde A$ (those that are bound constraints $x_j\ge 0$) with the variables they bound, so that a chosen nonbasic row set $J$ doubles as a set of "nonbasic variables." This mission's abstract row type does not track that identification (matching the abstraction already used throughout 06-lift-project-cuts and 07-higher-dim): Surplus instead defines the tableau row's nonbasic quantities directly as the slack expression $s_j := (\tilde Ax)_j - \tilde b_j$, a genuine affine function of $x$ for every row, which reduces to $x_j$ itself exactly when row $j$ is that bound constraint — mathematically equivalent to the book's own substitution, stated without needing the row-to-variable lookup. Eq. (8.10)'s "$j\in J\cap N'$" strengthening-eligibility test has the same gap; this mission takes the row-positions eligible for strengthening as an explicit Finset parameter rather than deriving membership from row identity.

Corollary 8.6 is out of scope for this mission — see HARD.md. Its facet-counting bound depends on the same row/variable identification (the printed bound is $\binom{m+p+n-1}{n}$, excluding row $k$ specifically because it is $x_k$'s own bound row) and would additionally require a general notion of "number of facets of a polyhedron" that this mission's abstraction, and Mathlib, do not provide; it does not feed Theorem 8.7's own proof, which cites only Theorems 8.4A/8.4B and 8.5.

Theorem 8.7 is stated via one generic HasRankAtMost predicate applied to SplitConvexify (part a) and three closure operators (SimpleDisjClosureOfSet, StrengthenedLPClosureOfSet, MIGClosureOfSet, parts b-d) defined by intersecting a represented polyhedron with every cut of the corresponding family, then lifted to bare sets by quantifying over every linear representation — since, unlike the split-convexification closure, these three cut families are defined via an explicit basis or CGLP solution and so genuinely need some concrete representation of the current polyhedron at each step of the recursion (the same representation-dependence Theorem 7.5's Lovász-Schrijver iteration required in 07-higher-dim).

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 8.
• E. Balas, M. Perregaard, A precise correspondence between lift-and-project cuts, simple disjunctive cuts, and mixed integer Gomory cuts for 0-1 programming, Mathematical Programming B 94 (2003), 221–245 (cited in the text as [33], the origin of Lemma 8.2 and Theorems 8.4A/8.4B).
• E. Balas, M. Perregaard, Lift-and-project for mixed 0-1 programming: recent progress, Discrete Applied Mathematics 123 (2002), 129–154 (cited in the text as [32], the origin of Theorem 8.5's strengthened-cut coefficient identification).
• F. Eisenbrand, A. Schulz, Bounds on the Chvátal rank of polytopes in the 0-1 cube, in Integer Programming and Combinatorial Optimization (IPCO 7), LNCS 1610 (1999), 137–150 (cited in the text as [73], the source of the unbounded pure-integer Gomory rank result this chapter's Theorem 8.7 contrasts with).

Motivation

The random walk Metropolis algorithm is one of the most widely used Markov chain Monte Carlo methods for sampling from a density known up to a constant. Its one tuning parameter is the variance of the Gaussian proposal. If the variance is too small, the chain accepts almost every move but barely moves. If it is too large, it proposes long jumps that are almost always rejected. Practitioners need a rule for choosing it, and the rule has to work in high dimension, where both failure modes are severe.

Roberts, Gelman and Gilks (Ann. Appl. Probab. 7(1), 1997) gave the first rigorous answer for product targets. As the dimension grows, one coordinate of the suitably speeded-up chain converges to a Langevin diffusion. The speed of that diffusion is an explicit function of the proposal scale, and maximising it gives the rule "tune the proposal so that about 23% of proposals are accepted". This rule, and the 2.38/√I scaling behind it, is now standard advice in applied Bayesian statistics.

Setting

Let $f:\mathbb R\to\mathbb R$ be a target density: positive, $C^2$, integrating to one, with $f'/f$ Lipschitz, and satisfying the moment conditions (A1) $\mathbb E_f[(f'/f)^8]<\infty$ and (A2) $\mathbb E_f[(f''/f)^4]<\infty$. Here $\mathbb E_f[g(X)]=\int g(x)f(x)\,dx$. In dimension $n\ge2$ the target is the product density $\pi_n(x)=\prod_{i=1}^n f(x_i)$ on $\mathbb R^n$.

Fix a scale $l>0$ and set $\sigma_n^2=l^2/(n-1)$. The random walk Metropolis chain $X^n=(X^n_0,X^n_1,\dots)$ moves as follows. From $X^n_{m-1}$ it proposes $Y\sim N(X^n_{m-1},\sigma_n^2I_n)$. It sets $X^n_m=Y$ with probability $\alpha(X^n_{m-1},Y)=1\wedge\pi_n(Y)/\pi_n(X^n_{m-1})$, and $X^n_m=X^n_{m-1}$ otherwise. The chain starts from $\pi_n$, which is stationary for it. The speeded-up first coordinate is $U^n_t=X^n_{\lfloor nt\rfloor,1}$ for $t\ge0$.

Let $\Phi$ be the standard normal distribution function, and define the roughness $I=\mathbb E_f[(f'(X)/f(X))^2]$. The speed and the limiting acceptance rate are

$$h(l)=2l^2\,\Phi\!\Big(-\frac{l\sqrt I}{2}\Big),\qquad a(l)=2\,\Phi\!\Big(-\frac{l\sqrt I}{2}\Big).$$

The Langevin generator is $GV(x)=h(l)\big[\tfrac12V''(x)+\tfrac12(\log f)'(x)V'(x)\big]$. It generates the Langevin diffusion $dU_t=h(l)^{1/2}dB_t+h(l)\frac{f'(U_t)}{2f(U_t)}dt$.

Formalization targets

Goal: Theorem 1.1

As $n\to\infty$,

$$U^n\Rightarrow U,$$

where $\Rightarrow$ denotes weak convergence in the Skorokhod topology, $U_0$ has density $f$, and $U$ is the Langevin diffusion with speed $h(l)$. The limit is asserted to exist. No constants appear in the statement beyond those the model defines.

Milestones: the proof

1. Lemma 2.1. The stationary chain stays in the sets $F_n=\{|R_n-I|<n^{-1/8}\}\cap\{|S_n-I|<n^{-1/8}\}$ up to time $t$ with probability tending to one. Here $R_n$ and $S_n$ are the empirical averages of $((\log f)')^2$ and $-(\log f)''$ over coordinates $2,\dots,n$.
2. Proposition 2.2. $|1\wedge e^x-1\wedge e^y|\le|x-y|$.
3. Lemma 2.3. $\sup_{x\in F_n}\mathbb E|W_n|\to0$, where $W_n$ is the second-order part of the log acceptance ratio.
4. Proposition 2.4. $\mathbb E[1\wedge e^A]=\Phi(\mu/\sigma)+e^{\mu+\sigma^2/2}\Phi(-\sigma-\mu/\sigma)$ for $A\sim N(\mu,\sigma^2)$.
5. Lemma 2.5. $\limsup_n\sup_{x_1}n|\mathbb E[V(Y_1)-V(x_1)]|<\infty$ for $V\in C_c^\infty$.
6. Lemma 2.6. The discrete generator $G_nV(x)=n\,\mathbb E[(V(Y)-V(x))\alpha(x,Y)]$ converges to $GV$ uniformly on $F_n$, for $V\in C_c^\infty$ a function of the first coordinate (stated with bounded $(\log f)'''$, the assumption its proof uses).

Milestones: the optimal-scaling corollary

7. Corollary 1.2 (i). $a_n(l)=\iint\pi_n(x)\alpha(x,y)q_n(x,y)\,dx\,dy\to a(l)$.
8. Corollary 1.2 (ii). $h$ is maximised at $\hat l=2.38/\sqrt I$, with $a(\hat l)=0.23$ and $h(\hat l)=1.3/I$, to the printed precision.

Significance

Theorem 1.1 shows that, run for $n$ times as many steps, the chain in dimension $n$ looks like a fixed one-dimensional diffusion. The algorithm's cost therefore grows linearly in dimension, and its efficiency is measured by the single number $h(l)$. Corollary 1.2 turns this into the 0.234 acceptance-rate heuristic and the $2.38/\sqrt I$ scaling. The same diffusion-limit method has since been applied to the Metropolis-adjusted Langevin algorithm, to Hamiltonian Monte Carlo and to non-product targets.

The theorem is proved on paper; it has no machine-checked proof. A formal development would give the first verified diffusion limit of an MCMC algorithm. It would also yield reusable components: the Metropolis chain on $\mathbb R^n$ as a measurable random mapping, a martingale-problem characterisation of one-dimensional diffusions, and a Gaussian computation (Proposition 2.4) that recurs throughout the optimal-scaling literature.

Difficulty

The obvious approach, a Taylor expansion of the log acceptance ratio, gives a sum of $n-1$ terms of size $1/n$. That sum does not concentrate uniformly over the state space, since the coordinates $2,\dots,n$ are arbitrary. The expansion is controlled only on the sets $F_n$, where the empirical averages $R_n$ and $S_n$ are close to $I$. The limit therefore holds only after showing that the chain rarely leaves $F_n$ over a time horizon of $nt$ steps. A pointwise law of large numbers is not enough for that, because the bound has to survive a union over $nt$ steps. Passing from generator convergence on a set of high probability to weak convergence of processes requires the Ethier–Kurtz convergence theory: a core for the limit generator, and convergence of processes that are not themselves Markov. None of this theory is in Mathlib.

Formalization scope

All declarations live in the namespace Roberts1997.RWM. The following conventions are fixed.

• Vectors are Fin n → ℝ, and the paper's first coordinate $x_1$ is index 0. Its coordinates $2,\dots,n$ are the indices i ≠ 0.
• $\sigma_n^2=l^2/(n-1)$ is computed in $\mathbb R$. All statements concern $n\ge2$ or large $n$.
• $l>0$ is assumed. The paper leaves it implicit, but $h(-l)\ne h(l)$.
• "$f$ is a density" is read as $\int f=1$. The moment conditions are read as integrability of $(f'/f)^8f$ and $(f''/f)^4f$. The standing assumption "$f'/f$ is Lipschitz" (p. 111) is carried by every statement.
• The chain is built as a random mapping on an explicit probability space: $x_0\sim\pi_n$, with i.i.d. standard normal innovations and uniform acceptance variables. Theorem 1.1's initial condition (components i.i.d. $f$, shared across dimensions) is read as "the $n$-th chain starts from $\pi_n$", since weak convergence depends only on the law of each $U^n$.
• "$U$ satisfies the Langevin SDE" is read as "the law of $U$ solves the martingale problem for $G$ on $C_c^\infty$, with continuous paths and initial law $f(x)\,dx$". This is equivalent by Ethier–Kurtz (1986), Ch. 5, Prop. 3.1 and Thm 3.3, and follows the platform definition EthierKurtz_IsContinuousDiffusionLaw.
• "$U^n\Rightarrow U$" is read as the existence of an almost-sure coupling in which càdlàg copies of the $U^n$ converge to a continuous Langevin path uniformly on compact time intervals. For a continuous limit this is equivalent to weak convergence in $D_{\mathbb R}[0,\infty)$, by Skorokhod's representation theorem and Ethier–Kurtz Ch. 3, Thm 1.8, Prop. 5.3 and Prop. 7.1. It follows the platform encoding of Ethier–Kurtz Theorem 7.4.1.
• "$\sup\to0$" and "$\limsup\sup<\infty$" are stated as eventual uniform bounds. This avoids real suprema, whose value on an unbounded set is a default.
• In Lemma 2.6, "as $d\to\infty$" is a misprint for $n\to\infty$, and "$2f(Ut)$" in (1.2) is read as $2f(U_t)$.
• Corollary 1.2 (ii) is stated for an arbitrary constant $I>0$. "To two decimal places" is read as explicit rounding intervals: $1.3$ is read to one decimal, and all maximisers over $l>0$ are covered.

The goal cannot be satisfied trivially. The limit law $Q$ must exist, and it must be a probability measure whose initial marginal is $f(x)\,dx$, so the zero measure is excluded. The coupled copies must carry exactly the laws of the paths $U^n$, not an arbitrary process with the same one-time marginals.

The statements carry the paper's hypotheses, with one exception. The printed proof of Lemma 2.6 bounds $\sup_z|(\log f)'''(z)|$, which Theorem 1.1 does not assume, and under $C^2$ alone the uniform convergence over $F_n$ claimed by Lemma 2.6 fails (narrow spikes of $(\log f)''$ far out let a positive fraction of the coordinates shift the log acceptance ratio by a constant while $R_n$ and $S_n$ stay close to $I$). Lemma 2.6 is therefore stated with the proof's own assumption, $f\in C^3$ with $(\log f)'''$ bounded, named as an addition. Theorem 1.1 and the other results keep the paper's hypotheses.

A complete development needs several pieces not yet available: path spaces and the Skorokhod topology (or the coupling reading), the martingale problem and its well-posedness for Lipschitz drift, and the Ethier–Kurtz theorem on convergence of generators on sets of high probability. Proofs of the Gaussian milestones (Propositions 2.2 and 2.4, Lemma 2.5) and of Corollary 1.2 (ii) are independent of this infrastructure and are welcome contributions.

Selected references

• G. O. Roberts, A. Gelman, W. R. Gilks, Weak convergence and optimal scaling of random walk Metropolis algorithms, Ann. Appl. Probab. 7(1), 110–120, 1997. https://doi.org/10.1214/aoap/1034625254
• S. N. Ethier, T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658
• A. Gelman, G. O. Roberts, W. R. Gilks, Efficient Metropolis jumping rules, Bayesian Statistics 5, Oxford University Press, 599–607, 1996.
• G. O. Roberts, J. S. Rosenthal, Optimal scaling for various Metropolis–Hastings algorithms, Statistical Science 16(4), 351–367, 2001. https://doi.org/10.1214/ss/1015346320

Why smooth-region boundary diffusions matter

Diffusion models in a bounded region need a rule for what happens when a path reaches the boundary. Two standard mechanisms are absorption, where the boundary kills the generator contribution, and oblique reflection, where a prescribed vector field pushes the process back into the region. Ethier and Kurtz treat these mechanisms as neighboring variants of the same uniformly elliptic model in Chapter 8, Section 1 of Markov Processes: Characterization and Convergence. The distinction is structural: the interior differential operator is shared, but its admissible generator graph changes with the boundary condition. This mission formalizes Theorems 1.4 and 1.5, retaining oblique reflection as the capstone and absorbed diffusion as the required related result.

The setting

Let $\Omega\subset\mathbb R^d$ be bounded, open, and connected, with $d\ge 2$. Its boundary is locally represented in orthogonal coordinates as the graph of a scalar function. The formal predicate C²,μ boundary regularity requires one positive chart radius valid at every boundary point, a connected local boundary patch, and a graphing function whose second partial derivatives satisfy the source's componentwise Hölder oscillation condition. The exponent obeys $0<\mu\le 1$.

The diffusion coefficients are a symmetric positive-semidefinite matrix field $a(x)$ and a drift field $b(x)$. Their entries satisfy the same local componentwise Hölder convention. Uniform ellipticity means that one $\varepsilon>0$ satisfies

$$\varepsilon\le \sum_{i,j}\theta_i a_{ij}(x)\theta_j$$

for every $x\in\Omega$ and every unit vector $\theta$. For smooth $f$, the interior operator is

$$Gf(x)=\frac12\sum_{i,j}a_{ij}(x)\,\partial_{ij}f(x) +Df(x)[b(x)].$$

Functions live on the compact closure $\overline\Omega$ as bounded continuous functions. Their ambient extensions are differentiated only at interior points. The second coordinate of each graph is itself continuous on the closure, so it records the boundary trace of $Gf$ rather than assigning an arbitrary value after differentiation.

Formalization targets

Goal: obliquely reflected diffusion generation

Theorem 1.5 adds a reflection field $c$ whose components have C¹,μ boundary regularity. An outward unit normal $n(x)$ is oriented by a local defining function that is negative precisely inside $\Omega$. Uniform obliqueness is the global lower bound

$$\varepsilon\le c(x)\cdot n(x),\qquad x\in\partial\Omega,$$

for one positive $\varepsilon$. The reflected graph requires a continuous derivative trace $J$ that agrees with $Df$ in the interior and satisfies

$$J_x(c(x))=0,\qquad x\in\partial\Omega.$$

The target asserts that the uniform closure of this graph is single-valued and is exactly the full generator of a positive strongly continuous contraction semigroup preserving the constant function one. The generator condition is a biconditional derivative limit, so it identifies the complete domain rather than only a convenient operator restriction.

Related target: absorbed diffusion generation

Theorem 1.4 keeps the same smooth-region and ellipticity assumptions but uses the absorbed graph. Its continuous operator trace satisfies $Gf=0$ on the boundary. It has the same full generation conclusion: graph single-valuedness, a positive strongly continuous contraction semigroup, preservation of one, and exact identification of the generator. The absorbed zero trace is not imported into the reflected theorem, and the oblique derivative condition is not imposed on the absorbed graph.

Significance

These results connect a local elliptic expression and a geometric boundary condition to a global Markov evolution on continuous functions over the closed region. The conclusions contain more than existence of a semigroup: they determine the whole infinitesimal generator, ensure positivity and contraction, and retain the conservative convention used by Ethier and Kurtz. The paired statements make the effect of the boundary mechanism explicit while holding the interior model fixed.

The formal contribution is a machine-checkable statement layer, not a proof of the source theorems. It records the componentwise Hölder convention, uniform boundary charts, ellipticity, normal orientation, continuous derivative trace, the two distinct generator graphs, and every semigroup clause. These definitions can support later work on reflected processes, elliptic boundary problems, and martingale formulations without rebuilding the geometric conventions.

Where the difficulty lies

The main difficulty is simultaneous control of interior regularity, boundary geometry, and the closed generator domain. Pointwise obliqueness is insufficient: the source requires a uniform positive lower bound over the whole compact boundary. Likewise, merely writing $Df(c)=0$ for an arbitrary ambient extension would not supply a well-defined boundary derivative. The graph therefore carries a continuous derivative trace agreeing with the interior derivative. Replacing the biconditional generator equality by a one-way inclusion, or silently imposing the absorbed zero trace on the reflected graph, would weaken or change the source result.

Formalization scope and conventions

The state space is EuclideanSpace ℝ (Fin (n + 1)) with 2 ≤ n + 1. Connectedness supplies nonemptiness. Matrix positive semidefiniteness supplies symmetry and nonnegative quadratic forms; a separate hypothesis gives strict uniform ellipticity. Local oscillation bounds apply within connected components of small intersections and do not compare different components.

The absorbed and reflected graphs use bounded continuous functions on closure Ω. The arbitrary zero extension outside the closure is never differentiated at a boundary point. The reflected boundary equation uses a continuous field of linear derivative maps, while the absorbed equation uses the continuous second graph coordinate. No vacuous region, pointwise-only ellipticity or obliqueness, weakened generator inclusion, proof-only theorem dependency, or synthetic theorem combining the two boundary mechanisms is admitted.

Selected references

• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 8, Section 1, Theorems 1.4–1.5 and equations (1.13)–(1.20). Wiley DOI
• Stewart N. Ethier and Thomas G. Kurtz, same volume, Chapter 1 for strongly continuous contraction semigroups and generators, and Chapter 4 for the conservative Feller convention. Wiley DOI

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

Random matrices with independent rows are the workhorse of high-dimensional statistics and compressed sensing: sample covariance matrices, sub-sampled measurement operators, and randomized sketches are all of this form. A basic question about such a matrix $A$ is how close $\|Ax\|_2$ stays to its typical size $\mathbb E\|Ax\|_2\approx\sqrt m\|x\|_2$ — not just for one fixed $x$, but simultaneously for every $x$ in some set $T$ of interest (a sphere, a cone, the difference set of a data cloud). A bound that holds only pointwise in $x$ is of limited use, since most applications need to reason about the worst case over an entire geometric set at once.

This chapter proves such a uniform bound — the matrix deviation inequality — for matrices with independent, isotropic, sub-gaussian rows, controlling the deviation by a single geometric parameter of $T$, its Gaussian complexity. The result is a direct descendant of the chaining machinery of Chapter 8 (via Talagrand's comparison inequality, Chapter 8.6) and, in this book's own account, subsumes several results proved earlier by other methods — two-sided bounds on random matrices, the Johnson-Lindenstrauss lemma for infinite sets — while also yielding two new consequences central to high-dimensional convex geometry: the $M^*$ bound and the Escape theorem, both controlling how a random subspace intersects a fixed geometric set.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$. A random vector $X$ in $\mathbb R^n$ is isotropic if its covariance matrix is the identity, $\Sigma(X)=\mathbb E[XX^\top]=I_n$ — equivalently (the book's own Lemma 3.2.3), $\mathbb E\langle X,x\rangle^2=\|x\|_2^2$ for every $x\in\mathbb R^n$. The sub-gaussian norm of a random vector $X$ is $\|X\|_{\psi_2}:=\sup_{x\in S^{n-1}}\|\langle X,x\rangle\|_{\psi_2}$, the supremum over the unit sphere of the scalar sub-gaussian (Orlicz $\psi_2$) norm of its one-dimensional marginals; $X$ is sub-gaussian when this is finite.

Fix a standard Gaussian random vector $g\sim N(0,I_n)$ in $\mathbb R^n$ (a vector whose coordinates in any orthonormal basis are independent standard normal). For a subset $T\subseteq\mathbb R^n$, the Gaussian width and Gaussian complexity of $T$ are

$$w(T) := \mathbb E\sup_{x\in T}\langle g,x\rangle, \qquad \gamma(T) := \mathbb E\sup_{x\in T}|\langle g,x\rangle|,$$

two closely related measures of the geometric size of $T$ — "cousins" that agree up to a factor of $2$ whenever $T$ contains the origin, and agree exactly when $T$ is origin-symmetric.

Formalization targets

Goal (Theorem 9.1.1, Matrix deviation inequality)

$$\exists\,C>0:\quad \mathbb E\sup_{x\in T}\bigl|\,\|Ax\|_2-\sqrt m\|x\|_2\,\bigr| \;\le\; CK^2\gamma(T)$$

for every $m\times n$ matrix $A$ whose rows $A_1,\dots,A_m$ are independent, isotropic, sub-gaussian random vectors with $K:=\max_i\|A_i\|_{\psi_2}$, and every $T\subseteq\mathbb R^n$ (whenever $\gamma(T)$ is finite). $C$ is the book's own unnamed absolute constant, hard-coded to no numeral — the weakest stable form of the claim.

Milestone (Theorem 9.4.2, the $M^*$ bound)

$$\mathbb E\,\mathrm{diam}(T\cap\ker A) \;\le\; \frac{CK^2w(T)}{\sqrt m}$$

for the same class of matrices $A$ and any bounded $T\subseteq\mathbb R^n$, where $\ker A$ is the (random) kernel of $A$, a subspace of codimension at most $m$. A direct one-paragraph consequence of the goal theorem (apply it to $T-T$, then restrict to $\ker A$, where $\|Ax-Ay\|_2$ vanishes).

Significance

The matrix deviation inequality converts a purely algebraic quantity — how close $\|Ax\|_2$ stays to $\sqrt m\|x\|_2$ — into a single geometric parameter of the index set $T$, letting it subsume, via specializations of $T$, results that were previously proved by separate ad hoc arguments: two-sided singular value bounds on random matrices ($T$ a sphere), Johnson-Lindenstrauss-type embeddings for possibly infinite point sets ($T$ a difference set), and covariance estimation. The $M^*$ bound is one of the two classical consequences the book develops fresh from the inequality (the other, the Escape theorem, is outside this mission's scope): it answers, quantitatively, how large a random affine section of a fixed convex body typically is, a question at the heart of the local theory of Banach spaces and of compressed sensing's recovery guarantees (Chapter 10 builds directly on this chapter's machinery). Both results have long-standing, well-understood classical proofs; this mission formalizes their statements, not open research.

Difficulty

The natural first idea — bound $\|Ax\|_2-\sqrt m\|x\|_2$ pointwise for a fixed $x$ using concentration of the norm of a sub-gaussian random vector, then take a union bound over $T$ — only works when $T$ is finite, and gives a bound that scales with $\log|T|$ rather than with the actual geometric size of $T$. The book's actual route treats $X_x:=\|Ax\|_2-\sqrt m\|x\|_2$, indexed by $x\in\mathbb R^n$, as a genuine random process and shows it has sub-gaussian increments ($\|X_x-X_y\|_{\psi_2}\le CK^2\|x-y\|_2$) — itself a nontrivial fact proved in stages (first for a single unit vector via concentration of the norm, Theorem 3.1.1; then for a pair of unit vectors via a squared-process argument; only then in full generality) — and then invokes Talagrand's comparison inequality (a consequence of the chaining machinery of Chapter 8) to pass from sub-gaussian increments directly to a bound in terms of Gaussian complexity, without ever performing a union bound over $T$ itself.

Formalization scope

A is represented by its rows, A : Fin m → Ω → EuclideanSpace ℝ (Fin n), with ‖Ax‖₂ recovered as Real.sqrt (∑ i, ⟨Aᵢ,x⟩²) rather than constructing A as a Matrix/LinearMap — this matches the book's own row-by-row hypotheses exactly and is what both theorems' own proofs use directly. IsIsotropic is formalized via the book's basis-free Lemma 3.2.3 characterization (E⟨X,x⟩² = ‖x‖² for every x) rather than the matrix equation Σ(X)=Iₙ, avoiding a fixed-basis covariance-matrix construction the rest of this chunk's definitions do not otherwise need. SubgaussianVectorNorm reuses the published scalar subgaussianNorm. GaussianWidth and GaussianComplexity realize the standard Gaussian vector g ∼ N(0,Iₙ) as the identity map on Mathlib's own standard Gaussian measure on a finite-dimensional inner product space (ProbabilityTheory.stdGaussian), and both, together with the goal's own left-hand side, use a locally-defined finite-marginal expected-supremum convention (ExpSup, EReal-valued) matching the book's own footnote-3 convention (Section 7.2), reused throughout the series. Both theorems' right-hand sides presuppose their respective geometric parameter ($\gamma(T)$ or $w(T)$) is a finite real number; since both are EReal-valued in general, each theorem takes an explicit real witness together with a proof that it equals the true value — the same finiteness-disclosure pattern 07-chaining's Dudley inequality uses for its own right-hand integral, needed here for exactly the same reason (the book's own display does not spell out why the quantity is finite, true whenever $T$ is bounded, as in every application). $C$ (and, in the milestone, the same $C$ again — the two are not asserted equal, matching that the book states them as two separate "absolute constants") is existentially quantified before every type, instance and hypothesis it is uniform over. The $M^*$ bound milestone (m_star_bound) additionally carries the hypothesis $m > 0$: its conclusion divides by $\sqrt m$, and without this hypothesis Lean's real-division convention ($x/0=0$) makes the right-hand side $0$ at $m=0$ regardless of $C, K, w(T)$ — false whenever $T$ has positive diameter, not merely a weaker or vacuous claim. The book's own proof ("Dividing by $\sqrt m$ yields …", p. 241) already implicitly assumes $m \ge 1$, matching every other use of $m$ in the chapter as a positive count of measurement rows.

A trivializing formalization would fix $T$ to be a finite set, collapsing the goal to the elementary union-bound case the book explicitly contrasts its own more general statement against (Section 9.1's opening paragraph: "we may choose an arbitrary subset $T\subseteq\mathbb R^n$"); this mission's goal quantifies over an arbitrary Set (EuclideanSpace ℝ (Fin n)) to rule that out.

This mission covers Theorem 9.1.1 and Theorem 9.4.2 only; Theorem 9.4.7 (the Escape theorem) and Theorem 9.2.4 (covariance estimation for lower-dimensional distributions), both named as candidate milestones, are left out for lack of session time given the substantial shared infrastructure this chapter needed from scratch. ExpSup, IsIsotropic, SubgaussianVectorNorm, GaussianWidth and GaussianComplexity are reusable by any later chapter needing an isotropic or sub-gaussian random vector, or a Gaussian-width-type quantity (Chapters 4, 10, 11 of this same book series all use one or more of these notions). Solvers' contributions are welcome on: Theorem 9.1.3 (the sub-gaussian increments of the deviation process, the technical heart of the goal's proof), Talagrand's comparison inequality itself (outside this mission, in 07-chaining's companion chapter), and the one-paragraph reduction from the goal to the $M^*$ bound.

Selected references

• S. Mendelson, A. Pajor, N. Tomczak-Jaegermann, Reconstruction and subgaussian operators in asymptotic geometric analysis, Geometric and Functional Analysis 17 (2007), 1248–1282. https://doi.org/10.1007/s00039-007-0618-7
• V. D. Milman, A new proof of A. Dvoretzky's theorem on cross-sections of convex bodies, Funkcional. Anal. i Priložen. 5 (1971), 28–37.
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 9. https://doi.org/10.1017/9781108231596

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).

The set

For a complex parameter $c$, iterate the quadratic map

$$f_c(z) = z^2 + c$$

starting at the critical point $z = 0$. The Mandelbrot set is the set of parameters for which this orbit stays bounded:

$$M = \{\, c \in \mathbb{C} \ : \ \sup_{k \in \mathbb{N}} \left| f_c^{\,k}(0) \right| < \infty \,\}.$$

Equivalently -- and this is the first milestone of the mission -- $c \in M$ if and only if $|f_c^{\,k}(0)| \le 2$ for every $k$, which exhibits $M$ as a compact subset of the plane.

$M$ is the parameter-space picture of the simplest non-trivial family in complex dynamics, and it acts as a dictionary: the shape of $M$ near a parameter $c$ encodes the dynamics of $f_c$ on its Julia set, so structural questions about $M$ are questions about the whole quadratic family at once. Douady and Hubbard proved in 1982 that $M$ is connected, by exhibiting a conformal isomorphism

$$\Phi : \mathbb{C} \setminus M \longrightarrow \mathbb{C} \setminus \overline{\mathbb{D}}$$

between the complement of $M$ and the exterior of the closed unit disk.

The question

MLC conjecture. $M$ is locally connected: every point of $M$ has a neighbourhood basis, in the subspace topology, consisting of connected sets.

By Caratheodory's theorem, MLC is equivalent to the statement that $\Phi^{-1}$ extends continuously to the unit circle. That extension would deliver a complete combinatorial description of $M$ -- the pinched disk model of Douady and Thurston -- in which every boundary point is labelled by the external rays landing on it. Two headline consequences follow: the density of hyperbolicity in the quadratic family (Fatou's conjecture: every quadratic polynomial can be perturbed to one with an attracting cycle), and zero area for $\partial M$.

MLC has been open since the early 1980s and is regarded as the central problem of one-dimensional complex dynamics.

Timeline

• 1982 -- Douady and Hubbard prove that $M$ is connected, via the Boettcher uniformisation of its complement, and formulate MLC.
• 1984/85 -- The Orsay notes develop the combinatorics of external rays and the pinched-disk model, and show that MLC implies the density of hyperbolicity in the quadratic family.
• 1990 -- Yoccoz proves MLC at every finitely renormalizable parameter without an indifferent periodic point, introducing the Yoccoz puzzle and the rigidity techniques that dominate later work.
• 1997 -- Lyubich extends local connectivity to infinitely renormalizable parameters of bounded type, using complex bounds for quadratic-like renormalization.
• 1997 -- Graczyk-Swiatek and Lyubich prove density of hyperbolicity in the real quadratic family.
• 1998 -- Shishikura proves that $\partial M$ has Hausdorff dimension $2$, by parabolic implosion. Whether $\partial M$ has positive area remains open.
• 2005 -- Buff and Cheritat construct quadratic Julia sets of positive area, showing that the analogous area question in the dynamical plane has a negative answer.
• Today -- MLC is known at large classes of parameters, but the general case, and with it the density of hyperbolicity, remain open.

What this mission asks for

The goal theorem is MLC itself, in the form "the Mandelbrot set, as a topological subspace of $\mathbb{C}$, is a locally connected space".

The milestones are of three kinds, and are ordered accordingly:

1. Foundations provable today -- the escape criterion (in the quadratic and the general unicritical degree) and compactness. These make the filter-theoretic definition usable and are the natural entry point for a solver new to the mission.
2. Known theorems from the literature -- connectedness of $M$ (Douady-Hubbard), the implication MLC $\Rightarrow$ density of hyperbolicity (Douady-Hubbard), and $\dim_H(\partial M) = 2$ (Shishikura). These are hard but settled, and formalizing them builds the infrastructure -- Boettcher coordinates, external rays, parabolic implosion -- that any attack on the goal will need.
3. The open companions -- density of hyperbolicity in the quadratic and unicritical families, zero area of $\partial M$, and MLC for all Multibrot sets $M_n$, the parameter sets of $z \mapsto z^n + c$.

All statements are phrased against a single shared definition file, so a solver can move between milestones without re-fixing conventions.

Motivation

An equation for a magma constrains a binary operation without assuming that it is associative, commutative, or has an identity. Which laws imply which others, over all magmas or over finite magmas only, is the question the Equational Theories Project studies at scale. Restricting the underlying set to be finite can change the answer: a structural argument may depend on the fact that a surjective self-map of a finite set is injective.

The project's December 2025 paper reports the finite implication from E677 to E255 as unresolved, while reporting a counterexample to the implication when infinite magmas are allowed. The paper also tentatively conjectures that a finite counterexample exists. This mission makes the affirmative implication its formal target and also accepts a rigorous refutation of the complete finite statement.

This mission treats the universal target as open. Supporting structural facts and conditional reductions are separately identified, so that progress on one does not assert completion of the target.

Setting

A magma here is a type $\alpha$ with a total binary operation $\diamond:\alpha\times\alpha\to\alpha$. Parentheses specify the order of evaluation throughout; no reassociation is permitted. The condition E677 means

$$\forall x,y\in\alpha,\quad x=y\diamond\bigl(x\diamond((y\diamond x)\diamond y)\bigr).$$

The condition E255 means

$$\forall x\in\alpha,\quad x=((x\diamond x)\diamond x)\diamond x.$$

These are the two laws used in Chapter 13 of the project blueprint. For a fixed element $y$, the left translation (left multiplication) map is $L_y(x)=y\diamond x$. A fixer of $x$ is an element $y$ with $y\diamond x=x$; it acts on $x$ from the left. This definition concerns one element $x$; it does not require $y$ to act as an identity on every element. The left orbit of $x$ is the forward orbit $x,L_x(x),L_x^2(x),\ldots$ of $x$ under its own left translation.

Formalization targets

The supporting targets expose the relevant distinction between a constraint on a possible fixer and the existence of a fixer. For every finite $\alpha$ satisfying E677, the first supporting statement is

$$\forall y\in\alpha,\quad L_y\text{ is bijective}.$$

The second supporting statement determines any fixer:

$$\forall x,y\in\alpha,\quad y\diamond x=x\ \Longrightarrow\ y=(x\diamond x)\diamond x.$$

The third supporting statement is the backward recurrence

$$\forall x,y\in\alpha,\quad x=(y\diamond x)\diamond\bigl((y\diamond(y\diamond x))\diamond y\bigr).$$

These three statements are blueprint Lemma 13.1(i)–(iii) and are Proved on this platform. The following fixer-existence assertion is the same obligation as E255 under E677 and finiteness (blueprint Lemma 13.2); it is a reduction node, not a milestone:

$$\forall x\in\alpha,\quad\exists y\in\alpha,\quad y\diamond x=x.$$

The mission goal is

$$\forall\text{ finite magmas }\alpha,\quad \operatorname{E677}(\alpha)\ \Longrightarrow\ \operatorname{E255}(\alpha).$$

For finite E677 magmas, E255 at $x$ supplies the fixer $(x\diamond x)\diamond x$; from any fixer $y$ of $x$, Lemma 13.1(ii) gives $y=(x\diamond x)\diamond x$ and hence E255 at $x$. Each direction is one line, so fixer existence is not a strictly weaker milestone.

Three open sub-goals come from the case split in the accepted reduction sketches for the fixer-existence node. Sub-goal 1 is orbit-local: for a fixed $x$, if two elements of the left orbit of $x$ have equal right products by $x$, then they are equal or $x$ has a fixer. Sub-goal 2 concerns the case of exactly one element $A$ outside the left orbit of $x$, with $x$ having no fixer: a right-translation collision $c\diamond x=A\diamond x$ between an orbit point $c$ and $A$ must propagate to the orbit successor $x\diamond c$. Sub-goal 3 assumes $x\diamond x\ne x$ and at least two elements outside the left orbit: if right translation by $x$ sends an orbit point outside the orbit, then $x$ has a fixer. Sub-goal 3 is not a smaller case of the goal. If it holds for every finite E677 magma, the mission goal follows by a product construction (milestone "Sub-goal 3 support (a)"), and the mission goal gives Sub-goal 3 because E255 at $x$ supplies the fixer $(x\diamond x)\diamond x$. So a proof of Sub-goal 3 alone proves the goal, and a route through Sub-goals 1 and 2 still needs Sub-goal 3. The D4 milestones specialize Sub-goal 1 to a left orbit of exact period four; D4.0, D4.1, D4.2 and D4.4a–e are Proved, and the series is open at D4.3 and its five branch closeouts D4.3a–e. One conditional result (E677 together with conjugacy-closed left translations implies E255; Padilla, 2026) is Proved on this platform. The milestone "Alternative resolution — a finite E677 counterexample to E255" (theorem finite_counterexample) is the disproof target. The sixteen milestones "Counterexample structure (a)–(p)" are constraints on a counterexample and rules for a counterexample search, all Proved; (h)–(j) take small-order facts as hypotheses. None of the sixteen is a disproof. None of the displayed statements restricts the cardinality to a tested range.

In the authors' repository, Sub-goal 1 is called Piece 1, the unique-outsider case containing Sub-goal 2 is called Gap 1, and the case of Sub-goal 3 is called Gap ≥ 2; those names appear in some theorem sources and file names.

Significance

A resolution determines whether this particular law gains E255 as a consequence upon restriction to finite carriers. An affirmative proof must cover every finite cardinality, every operation on each carrier, and every assignment of the universally quantified elements. A finite counterexample must supply an operation that satisfies every instance of E677 while failing E255 at some element.

The formal package provides small, reusable statements of the two laws, the left translation property, and the fixer constraint. Keeping these statements separate allows their precise hypotheses and conclusions to be checked individually. In particular, the second supporting result says what a fixer must be when one exists; the fixer-existence formulation records the additional mathematical content needed to ensure existence.

Difficulty

The left translation conclusion concerns maps with the left input fixed. The fixer-existence formulation instead asks about the image of the map $y\mapsto y\diamond x$, with its right input fixed. No assumption in the formal goal makes these two maps interchangeable. Bijectivity of every left translation map alone does not state that a fixer exists.

Because the implication fails for infinite magmas, E255 is not an equational consequence of E677, so any proof must use finiteness in an essential way. The blueprint's linear and linear-extension constructions cannot produce a finite counterexample (blueprint Lemmas 13.3 and 13.4); community members have formalized on this platform the scalar-coefficient case of the linear lemma, the Type I and Type II affine families, and the linear-extension lemma (see the discussion thread).

Likewise, checking a collection of finite operation tables does not quantify over arbitrary finite cardinalities. Such computation does not discharge the goal submitted here. Any proof must justify every use of finiteness and retain the displayed parenthesization of the laws.

Formalization scope

The representation uses an arbitrary universe-polymorphic type, an explicit binary operation, and a Fintype instance for finite targets. Passing the operation explicitly avoids importing a separate magma package or imposing algebraic typeclass laws. The predicates E677 and E255 themselves do not assume finiteness; each theorem states its own finite-carrier hypothesis.

Empty carriers are included. Both laws hold vacuously on them; the pointwise fixer statement is also vacuous because there is no element $x$. Consequently an empty carrier cannot refute the main goal. Nonempty carriers of every finite size are included without further assumptions. There is no associativity, commutativity, idempotence, identity element, or cancellation hypothesis hidden in the representation.

The definition bundle FiniteMagmaE677 provides E677, E255, HasFixerAt (existence of a fixer of $x$), InLeftOrbit (membership in the left orbit of $x$) and OrbitRightCollisionOrFixer. Three further bundles, FiniteMagmaE677_seventh_element_growth, FiniteMagmaE677_d4_first_return and FiniteMagmaE677_sswap_renewal, hold the period-four packet types used by the D4 milestones.

Status (2026-10-22 UTC). Proved on this platform: Lemma 13.1(i)–(iii), the Sub-goal 1, Sub-goal 2 and Sub-goal 3 support lemmas, D4.0, D4.1, D4.2, D4.4a–e, the conditional conjugacy-closure theorem, Counterexample structure (a)–(p), and three further conditional theorems by omegaestable (existential row transport, parametrized row transport, left-parameter transport; see the discussion thread). Open: Sub-goals 1–3, D4.3 with D4.3a–e, and the counterexample target. Community members have also formalized the blueprint's 496-element non-right-cancellative E677 magma (see the discussion thread).

Welcome contributions: a proof of any open sub-goal or D4.3 branch (a proof of Sub-goal 3 proves the goal; see the milestone "Sub-goal 3 support (a)"); a proof sketch that reduces an open leaf to new lemmas; a concrete operation table on Fin n proving finite_counterexample, which would make the main theorem false.

Results in the captain's private repository that are not on this platform

Results that are Proved on this platform are not repeated here. Readers cannot open the captain's private repository, so each statement is given in full. PROVEN means a complete proof, in the form stated. BOUNDED means a SAT-solver result for one encoded finite structure: each UNSAT result used here has a DRAT proof that drat-trim accepted (unverified C code, not a kernel-checked proof). EMPIRICAL means a computation over finite data, with no certificate.

Not ported

A port of these results to this platform is a long job.

1. The finite facts that Counterexample structure (h)–(j) take as hypotheses. BOUNDED. No E677 magma has order 2, 3, 4, 6 or 8, and every E677 magma of order 7 or 9 has an idempotent. Counterexample structure (h) and (j) give the earlier sources and the captain's check. These facts, except those for orders 2 and 3, are hypotheses of theorems that are Proved on this platform, so a port of them would make (h)–(j) unconditional; it needs kernel-checked proofs made from the DRAT certificates. Source: the captain's private repository, revision dd2ee3e5, experiments/analysis/idempotent-free-small-orders-2026-10-21/ and, for order 8, experiments/analysis/ti-groups-2026-10-19/ (section "Order 8").

2. Period-four refinements of D4.2. PROVEN (Lean; axioms propext, Classical.choice, Quot.sound). A repository theorem refines the five branches of the D4.2 first-return packet and keeps every case. Write $q=c_2\diamond x$. In the R-through-one branch (the repository's name), each outcome is a fixer of $x$, a strict decrease of a finite contact budget, a new $L_x$-cycle disjoint from the elements already accounted for (with its exact size), or a closed trace of $L_q^{-1}$ that is reduced to two phase-contact families. In the two unswapped S branches, each outcome is a fixer of $x$, a decrease by one of the number of unmarked phases on the $L_x$-cycle of $q$, or a new disjoint $L_x$-cycle with its exact size. These results do not close D4.3 or any of D4.3a–e, because the outcomes are not yet combined into one state with a strictly decreasing well-founded measure. A port needs the repository's library of period-four packets. Source: the captain's private repository, revision 4100763b, lean/E677/Spine/Piece1D4RefinedFirstReturn.lean, e677_d4_q_refinedFirstReturnPacket_of_firstReturnPacket.

Not formalized

These results have only solver or computation evidence, and no Lean proof, and no milestone on this platform uses them as hypotheses.

3. A counterexample has at least 11 elements. BOUNDED. Every E677 magma with at most 10 elements satisfies E255. By item 1, no E677 magma has order 2, 3, 4, 6 or 8. Every E677 magma of order 5, 7 or 9 is right-cancellative; then each right translation $y\mapsto y\diamond x$ is a bijection, so $x$ has a fixer, and Lemma 13.1(ii) gives E255 at $x$. At order 10, a point $x$ at which E255 fails has no fixer, so $x$ is not in its own column $\{y\diamond x\}$; a search for such a table, split into 67 cases by the cycle type of $L_x$ (the length $l\ge 2$ of the left orbit of $x$, and the cycle lengths of $L_x$ on the other $10-l$ elements), is UNSAT in each case. Earlier reports: the sources listed in Counterexample structure (h)–(j) for the E677 magmas of orders 2–4 and 6–9, among them a Lean proof for order 6 by J. Hyun. Without certificates (ETP Zulip thread "FINITE: 677 -> 255"): J. Brox (Mace4) reports no counterexample of order 9 (2024-12-10), none of order at most 10 (2025-01-10), no E677 magma of order 10 (2025-01-12) and no counterexample of order 11 (2025-03-12); B. Le Floch (2024-12-22, Mace4) reports none of order at most 9; J. Hyun (2025-01-09, CaDiCaL) none of order 5 to 8; S. Chuks-Onah (2026-05-01, Z3) none of order 5 or 6; R. Schneider (2026-05-15, own search program) and B. Subercaseaux (2026-05-15, SAT) none of order at most 11. The new content here is the DRAT certificates. Source: the captain's private repository, revision dd2ee3e5, experiments/analysis/rc-small-orders-2026-10-19/ and experiments/analysis/rc-cubes-2026-10-19/.

4. Order 35 over the quotient $x\diamond y=4x+3y$ on $\mathbb{F}_7$. With the order-7 fact of item 1, Counterexample structure (i) gives: if a minimum counterexample $M$ has order 35 and a non-universal congruence $\theta$ that relates $z$ and $q(z)$, then $M/\theta$ has 7 elements and an idempotent, and the classes have 5 elements. By the classification of J. Brox (ETP Zulip thread "FINITE: 677 -> 255", 2025-03-26, Mace4, no certificate; not checked by the captain), $M/\theta$ is then isomorphic to $4x+3y$ or to $4x+y$ on $\mathbb{F}_7$. Take $Q$: $x\diamond y=4x+3y$ on $\mathbb{F}_7$ (0 is its only idempotent), write the elements of $M$ as pairs $(a,s)$ with $a\in\mathbb{F}_7$ and $s\in\mathbb{F}_5$, and call the map $(s,t)\mapsto$ (second coordinate of $(a,s)\diamond(b,t)$) the block over $(a,b)$. Results, each for an E677 magma of this form:

• If at most five blocks other than the block over $(0,0)$ do not have the form $(s,t)\mapsto s+f_{ab}(t-s)$ with a permutation $f_{ab}$ of $\mathbb{F}_5$, then E255 holds. BOUNDED (two short paper lemmas reduce it to 48 patterns of non-cyclic blocks, each UNSAT). This includes the case where every block has this form.
• If every block has the form $(s,t)\mapsto A\,t+B$ with $A\in\{1,4\}$ (with $A$ and $B$ chosen for each block and each $s$), then E255 holds. BOUNDED.
• With all blocks free, the solver runs did not finish, so there is no result. The quotient $4x+y$ was not tested.

The only known E677 magma of order 35 with this quotient and classes of 5 elements is isomorphic to $Q\times M_5$, where $M_5$ is $s\diamond t=2s-t$ on $\mathbb{F}_5$ (EMPIRICAL). T. Tao (ETP Zulip thread "FINITE: 677 -> 255", 2024-12-13) proposed the extensions $(x,s)\diamond(y,t)=(4x+3y,\ s\diamond_{x,y}t)$, and (same thread, 2024-12-22) the fibre operations $s+f_{x,y}(t-s)$ of the first result. The second result is a case of the form $(x\diamond y,\ b_{x,y,s}t+c_{x,y,s})$ for which B. Reinke (same thread, 2026-06-11) expected E255 to lift, without a proof. Source: the captain's private repository, revision dd2ee3e5, docs/current/e677-coverage-matrix-2026-10-19.md (the rows for this quotient) and experiments/analysis/pro-counterexample-audit-2026-10-20/.

5. Extensions and row changes of the order-31 magma $x\diamond y=5x-4y+1$ on $\mathbb{F}_{31}$. Call it $Q_{31}$. It has no idempotent, and it is the smallest known E677 magma without an idempotent; every known E677 magma without an idempotent has order divisible by 31 (EMPIRICAL). So $Q_{31}$ is the smallest known candidate quotient in Counterexample structure (j). BOUNDED results:

• No E677 magma has a congruence with quotient $Q_{31}$ and classes of 2 or 3 elements.
• No E677 magma with a congruence with quotient $Q_{31}$ and classes of 4 elements fails E255.
• In the family $(u,s)\diamond(w,t)=(5u-4w+1,\ s+h_{w-u}(t-s))$ on $\mathbb{F}_{31}\times\mathbb{F}_5$, with permutations $h_d$ of $\mathbb{F}_5$, no E677 member fails E255.
• An E677 operation on $\mathbb{F}_{31}$ that fails E255 differs from $Q_{31}$ in at least 20 rows and at least 40 cells.

B. Le Floch (ETP Zulip thread "FINITE: 677 -> 255", 2024-12-13) found $5x-4y+c$ mod 31 as the one linear E677 model in which $c$ cannot be removed, and R. Schneider (same thread, 2025-11-21) noted that $Q_{31}$ has no idempotent. T. Tao (same thread, 2024-12-13) proposed the extensions $(x,s)\diamond(y,t)=(x\diamond y,\ s\diamond_{y-x}t)$ of $Q_{31}$. B. Reinke (same thread, 2025-11-07) encoded them for z3 and wrote that he thought he could exclude classes of fewer than 4 elements (no certificate). The first result above covers all extensions with classes of 2 or 3 elements, not only these; the third result is the case of Tao's extensions with fibre operations $s+h(t-s)$. Source: the captain's private repository, revision dd2ee3e5, experiments/analysis/gap2-monolith-m3-2026-10-17/ (§2, §6), experiments/analysis/pro-counterexample-audit-2026-10-20/ (cyclic-section-19375/, construction-19350/) and experiments/analysis/idempotent-free-2026-10-19/.

6. Tables with an automorphism of prime order, orders 12–21. BOUNDED, incomplete. Let $\alpha$ be an automorphism of prime order $p$ of an E677 magma of order $n$, $12\le n\le 21$, with $f$ fixed points, and let $z$ be a point with no fixer. The fixed points of $\alpha$ form a submagma, so an E677 magma of order $f$; by item 1, $f\notin\{2,3,4,6,8\}$. The search covers $f\in\{0,1,5,7,9,11\}$. If $\alpha$ fixes $z$, the fixed points form an E677 magma of order $f$ that fails E255 at $z$; this is excluded for $f\le 9$ by item 3, and for $f=11$ 4 shapes $(n,p,f)$ are UNSAT and 7 were not run. If $z$ is in a cycle of $\alpha$, 26 shapes are UNSAT (all 9 shapes with $p\ge 11$, and 17 shapes with $p\le 7$); 14 shapes are UNKNOWN after 3600 s, and 40 were not run. Not covered: the shapes with $f=0$ and one cycle ($n=p\in\{13,17,19\}$, translation-invariant tables on $\mathbb{Z}_n$), fixed-point count 10, and fixed-point counts of at least 12. Earlier searches without certificates (ETP Zulip thread "FINITE: 677 -> 255"): R. Schneider (2025-11-20 and 2025-11-21) searched the tables with the automorphism $(0)(1\,2\,\dots\,n-1)$ up to $n=31$ and found only right-cancellative ones (the shapes with $f=1$ and one cycle); B. Reinke (2025-11-21) noted that the fixed points form a submagma and found no table with one cycle and 5 fixed points of order at most 25 other than order 5 (the shapes with $f=5$ and one cycle), and (2025-11-26) noted that in a minimum counterexample only the identity automorphism fixes the failing point. Source: the captain's private repository, revision dd2ee3e5, experiments/analysis/symmetric-simple-2026-10-20/.

7. A refuted intermediate statement. EMPIRICAL (exhaustive check of one explicit table, run twice with independent encodings; not kernel-checked). Let $S(x)$ be the closure of the left orbit of $x$ under $z\mapsto z\diamond x$. The repository's gate CP asserted: in a finite E677 magma, if the hypotheses of Sub-goal 3 hold at $x$ and $z\mapsto z\diamond x$ is not injective on $S(x)$, then the left orbit of $x$ has minimal period $7$. Let $K$ be the 7-element E677 magma of Sub-goal 3 support (a) (file db/7/1 of the public collection memoryleak47/eq677), and let $M$ be the E677 magma of order $77$ in file db/77/65 of the same collection. In $M\times K$ (order $539$; E677 checked on all $539^2$ pairs), the point $(0,0)$ satisfies these hypotheses, and its left orbit has minimal period $\operatorname{lcm}(7,6)=42$. The point $(0,0)$ has the fixer $(76,4)$, so this is not a counterexample to E255, and it refutes CP only in the form without a no-fixer hypothesis. Source: the captain's private repository, revision 4100763b, docs/current/dead-ends/gap-ge-2.md, entry D7-6.

8. $\Phi(x)=(x\diamond x)\diamond x$ is not injective in general. EMPIRICAL. In the 2026-09-27 snapshot of the community database (4091 tables), every table satisfies E255, and $\Phi$ is not injective in 1107 of them; the smallest such order is $7$. In one table of order 7, row 6 is the identity row, so $6$ is a fixer of every $x$ and Lemma 13.1(ii) gives $\Phi(x)=6$ for every $x$. So global injectivity of $\Phi$ is not a usable intermediate target. Source: the captain's private repository, revision 4100763b, docs/professor-phi-injectivity.md, correction of 2026-10-14.

Selected references

• Matthew Bolan et al., The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale, arXiv:2512.07087v2 (December 16, 2025), paper.
• The Equational Theories Project contributors, Equational Theories, online proof blueprint, Chapter 13, equations (1)–(2) and Lemmas 13.1–13.4, chapter, accessed September 7, 2026 and October 13, 2026.
• J. I. Padilla (GitHub: omegaestable), Prove E677 implies E255 under left translation conjugacy closure, Equational Theories Project pull request #1518, 2026 (closed without merge by its author on 2026-10-13; the theorem is Proved on this platform), pull request.
• Lean Zulip, channel "Equational", thread "FINITE: 677 -> 255", thread.