Probability

Why stochastic-gradient convergence matters

Training a machine-learning model often means choosing a vector of parameters to minimize an average loss. Evaluating the full gradient can require processing an entire dataset. A stochastic-gradient method instead updates the parameters using a random direction obtained from a smaller amount of information. Its computational appeal raises a mathematical question: which assumptions on those directions and the stepsizes guarantee progress, and what kind of convergence follows?

This mission formalizes the core convergence theory in Section 4 of Bottou, Curtis, and Nocedal, Optimization Methods for Large-Scale Machine Learning. The results distinguish strongly convex objectives, where expected objective error can be controlled, from general smooth objectives, where the guarantee concerns gradients. They also distinguish constant stepsizes, which leave a noise-dependent error bound, from diminishing stepsizes.

Historical timeline

• 1951: Robbins and Monro introduced stochastic approximation for finding a root using noisy observations. Their work is the historical foundation for the stepsize conditions used here; the original root-finding theorem is not a separate target of this mission. Original paper.
• 2016: Bottou, Curtis, and Nocedal released the first version of their survey, organizing stochastic-gradient theory around smoothness and moment assumptions. arXiv record.
• 2018: The revised survey appeared in SIAM Review. This mission fixes arXiv version 3 for stable theorem numbering and PDF page citations. Published article.

The mathematics targeted here is already proved in the literature; the task is its Lean formalization, not a claim that these convergence results are unresolved research conjectures.

Objective, algorithm, and probability model

Let $F:\mathbb R^d\to\mathbb R$ be differentiable with an $L$-Lipschitz gradient, where $L>0$. On a probability space $(\Omega,\mathcal A,\mathbb P)$, let $\mathcal H_k$ contain the history before step $k$. Starting from a deterministic vector $w_0$, the algorithm uses positive deterministic stepsizes $\alpha_k$ and random directions $g_k$ to update

$$w_{k+1}=w_k-\alpha_k g_k.$$

The state $w_k$ is measurable with respect to $\mathcal H_k$; the direction $g_k$ is measurable with respect to $\mathcal H_{k+1}$ and has a finite second moment. Conditional assertions hold almost surely. This uses the adapted-process formulation expressly permitted in footnote 4, PDF p. 22, rather than requiring independent sample seeds. The local index $k=0$ corresponds to the paper's $k=1$. Algorithm 4.1 and footnote 4.

Write $\mathbb E_k$ for conditioning on $\mathcal H_k$. The moment conditions use constants $\mu_G\ge\mu>0$ and $M,M_V\ge0$:

$$\langle\nabla F(w_k),\mathbb E_k g_k\rangle\ge\mu\|\nabla F(w_k)\|^2, \qquad \|\mathbb E_k g_k\|\le\mu_G\|\nabla F(w_k)\|,$$ $$\mathbb E_k\|g_k\|^2-\|\mathbb E_k g_k\|^2 \le M+M_V\|\nabla F(w_k)\|^2.$$

Define $M_G=M_V+\mu_G^2$. The iterates lie almost surely in an open region on which $F\ge F_{\inf}$ for a real lower bound $F_{\inf}$. These are Assumptions 4.1 and 4.3, PDF pp. 23–24, equations (4.6)–(4.9). Source.

Formalization targets

The goal is Theorem 4.10, Section 4.3, PDF p. 33, equations (4.30a)–(4.30b). Suppose

$$\sum_{k=0}^\infty\alpha_k=\infty,\qquad \sum_{k=0}^\infty\alpha_k^2<\infty.$$

For $A_K=\sum_{k=0}^{K-1}\alpha_k$, establish both

$$\exists S\in\mathbb R:\quad \mathbb E\!\left[\sum_{k=0}^{K-1}\alpha_k\|\nabla F(w_k)\|^2\right]\longrightarrow S,$$ $$\frac{1}{A_K}\mathbb E\!\left[\sum_{k=0}^{K-1}\alpha_k\|\nabla F(w_k)\|^2\right] \longrightarrow0.$$

There is no convexity assumption and no restriction that the initial stepsizes already satisfy a small-step bound. Theorem 4.10.

Four milestones capture the surrounding theory. Lemma 4.4 gives the two successive conditional expected-descent inequalities (4.10a)–(4.10b), PDF pp. 24–25. It is a common input to the convergence results. Theorem 4.6 gives a geometric upper bound for strongly convex objectives with a constant stepsize. Theorem 4.7 gives the corresponding $O(1/k)$ bound for $\alpha_k=\beta/(\gamma+k+1)$. These are parallel strongly convex targets, not prerequisites for the nonconvex goal. Theorem 4.8 gives finite-horizon sum and average squared-gradient bounds for general objectives with a constant stepsize. Section 4.

For example, if $c>0$ is the strong-convexity constant, $d\ge1$, and $0<a\le\mu/(LM_G)$, Theorem 4.6 states, with $B=aLM/(2c\mu)$ and $F_*=\inf_xF(x)$,

$$\mathbb E[F(w_k)-F_*]\le B+(1-ac\mu)^k(F(w_0)-F_*-B).$$

The upper bound tends to $B$; this does not assert that the actual expected error tends to $B$. Every milestone retains the paper's constants and all displayed conclusions. Equations (4.13)–(4.14), PDF p. 26.

What a completed formalization provides

The result explains precisely how noise and stepsize interact. The general-objective goal guarantees that the stepsize-weighted expected squared gradients average to zero even when $M>0$. The strongly convex milestones quantify objective error and the effect of initialization. These results concern the stated quantities; they do not assert convergence of iterates, global optimality for a nonconvex objective, or almost-sure convergence. Sections 4.2–4.3.

A completed development would provide reusable Lean results for smooth objective functions, conditional moment bounds, stochastic updates, and expected convergence. The proposed statements are open proof obligations. Compilation establishes that the definitions and statements are well formed, not that their convergence claims have already been proved.

Mathematical and formal difficulties

Finite conditional expectations must be connected to unconditional integrals without relying on total-function defaults. The infinite-horizon result also requires careful handling of a finite initial segment: square summability gives eventually small steps, not a bound at every step. Strong convexity must justify the objective-gap estimates and the properties of the optimum. Treating a descent recurrence as a hypothesis would omit the analytic content that this mission is intended to formalize.

Formalization scope

The model uses real finite-dimensional Euclidean space, Mathlib gradients, filtrations, Bochner conditional expectations, and ordinary real integrals. The probability space is arbitrary; no finite-support or standard-Borel restriction is imposed. Directions have explicit finite second moments, making the finite-expectation convention in the paper visible. Square integrability of iterates and integrability of losses are consequences to establish, not extra model fields.

Strong convexity uses Mathlib's StrongConvexOn, equivalent here to Assumption 4.5's first-order inequality. The optimum is defined as the infimum of the range of $F$, with its finiteness to be derived in the strongly convex branch. That branch requires $d\ge1$: the paper's deduction $c\le L$ implicitly uses a nontrivial space. The nonconvex statements allow $d=0$. Zero noise is allowed. Finite-horizon averages require $K>0$; the value assigned at $K=0$ does not affect an asymptotic limit.

Contributions to the conditional-descent infrastructure and any of the four milestones are welcome. Variance reduction, Newton-type methods, and the remainder of the survey are outside this initial mission.

Selected references

• Léon Bottou, Frank E. Curtis, and Jorge Nocedal. Optimization Methods for Large-Scale Machine Learning. SIAM Review 60(2), 223–311, 2018. arXiv:1606.04838v3; DOI. All page numbers above refer to the 95-page arXiv v3 PDF.
• Herbert Robbins and Sutton Monro. A Stochastic Approximation Method. Annals of Mathematical Statistics 22(3), 400–407, 1951. DOI. Historical background only.

Problem

Solve a consistent system $Ax=b$, with $A\in\mathbb{C}^{m\times n}$ of full rank and $m\ge n\ge 1$. Kaczmarz's method (1937) projects the current iterate onto the solution hyperplane of one equation at a time. The cyclic version converges, but its rate depends on the order of the rows and has no clean bound in terms of a condition number.

Strohmer and Vershynin (2009) pick row $i$ at random with probability $\|a_i\|_2^2/\|A\|_F^2$ and prove

$$\mathbb{E}\,\|x_k-x\|_2^2 \le \bigl(1-\kappa(A)^{-2}\bigr)^k\,\|x_0-x\|_2^2,\qquad \kappa(A)=\frac{\|A\|_F}{\sigma_{\min}(A)}.$$

The rate does not depend on the number of equations $m$.

Setting

• Rows. $a_i\in\mathbb{C}^n$ is the conjugate of row $i$, so equation $i$ reads $\langle a_i,x\rangle=b_i$.
• Condition number. $\sigma_{\min}(A)=\inf_{\|z\|_2=1}\|Az\|_2$ and $\kappa(A)=\|A\|_F/\sigma_{\min}(A)$ (Demmel). It satisfies $\sqrt n\le\kappa(A)\le\sqrt n\,\|A\|_2/\sigma_{\min}(A)$.
• Algorithm 1. From any $x_0$, draw row $r$ independently with probability $p_r=\|a_r\|_2^2/\|A\|_F^2$ and set

$$x_{k+1}=x_k+\frac{b_r-\langle a_r,x_k\rangle}{\|a_r\|_2^2}\,a_r .$$

• Expectation. $\mathbb{E}\|x_k-x\|_2^2$ is a finite sum over the $m^k$ possible row sequences.

Targets

• Theorem 2 (goal): the bound above, for every $x_0$ and $k$.
• Theorem 3: some $x_0\ne x$ has $\mathbb{E}\|x_k-x\|_2^2\ge(1-2k/\kappa(A)^2)\|x_0-x\|_2^2$ for all $k\ge1$, so $\kappa(A)^{-2}$ is sharp up to a constant. Caveat: the source's proof only reaches the unsquared bound $\mathbb{E}\|x_k-x\|_2\ge\dots$ and then cites Jensen, which goes the wrong way. Its estimates give the squared bound with $4$ in place of $2$. Both forms are milestones.
• Sharpness (§3.2): Theorem 2 is an equality when $\kappa(A)=\sqrt n$.
• Iteration count (§2.1): $k\ge 2\log\varepsilon/\log(1-\kappa(A)^{-2})$ steps give $\mathbb{E}\|x_k-x\|_2^2\le\varepsilon^2\|x_0-x\|_2^2$.

Proof idea

A single projection can barely reduce the error, when the error is almost orthogonal to the chosen row. On average it always does. If $Z=a_j/\|a_j\|_2$ is drawn with probability $p_j$, then

$$\mathbb{E}\,|\langle z,Z\rangle|^2=\frac{\|Az\|_2^2}{\|A\|_F^2}\ge\kappa(A)^{-2}\|z\|_2^2 .$$

Pythagoras for one projection then gives $\mathbb{E}\|x_{k+1}-x\|_2^2\le(1-\kappa(A)^{-2})\,\|x_k-x\|_2^2$; induct on $k$.

Formalization

• Vectors live in EuclideanSpace ℂ (Fin n) and matrices in Matrix (Fin m) (Fin n) ℂ. Mathlib's inner product is conjugate-linear in its first argument, which is why $a_i$ is a conjugated row.
• Full rank is stated as injectivity of $z\mapsto Az$.
• The expectation expErrSq is an explicit finite sum, so no measure theory is needed. The tower identity is a milestone.
• A zero row makes the step the identity (Lean's division by zero) and has probability $0$, so it is harmless.
• Mathlib has no Kaczmarz iteration, scaled condition number or $\sigma_{\min}$ lower bound; the mission builds them.

History

• 1937: Kaczmarz introduces the cyclic method and proves convergence, with no rate.
• 1970: Gordon, Bender and Herman rediscover it as ART for tomography.
• 2009: Strohmer and Vershynin give the first rate in terms of a condition number.
• 2010 onward: extensions to noisy systems, block methods, SGD and sketch-and-project (Needell; Needell–Tropp; Needell–Srebro–Ward; Gower–Richtárik).

References

• S. Kaczmarz, Angenäherte Auflösung von Systemen linearer Gleichungen, Bull. Int. Acad. Polon. Sci. Lett. A 35 (1937), 355–357.
• T. Strohmer and R. Vershynin, A randomized Kaczmarz algorithm with exponential convergence, J. Fourier Anal. Appl. 15 (2009), 262–278. arXiv:math/0702226
• J. Demmel, The probability that a numerical analysis problem is difficult, Math. Comp. 50 (1988), 449–480. DOI
• D. Needell, Randomized Kaczmarz solver for noisy linear systems, BIT Numer. Math. 50 (2010), 395–403. arXiv:0902.0958
• D. Needell, N. Srebro and R. Ward, Stochastic gradient descent, weighted sampling, and the randomized Kaczmarz algorithm, Math. Program. 155 (2016), 549–573. arXiv:1310.5715
• R. M. Gower and P. Richtárik, Randomized iterative methods for linear systems, SIAM J. Matrix Anal. Appl. 36 (2015), 1660–1690. arXiv:1506.03296

Motivation

The free energy principle (FEP) proposes that a self-organizing system — a brain, an organism, an agent — persists by minimizing one quantity: the variational free energy of its sensory states under an internal generative model. Introduced by Karl Friston as a principle of brain function [Friston 2006] and stated in its unified form [Friston 2010], the principle makes a precise mathematical claim at its core: whatever internal state estimate the system holds, the free energy of incoming data is never below the data's surprisal (negative log marginal likelihood), and the excess is exactly the Kullback–Leibler divergence between the system's recognition density and the Bayesian posterior implied by the model. Active inference extends the same functional from perception to action and planning [Friston et al. 2017], and the same bound is known in machine learning as the evidence lower bound (ELBO) of variational inference [Parr et al. 2022].

Timeline of the mathematical content this mission formalizes:

• 2006 — Friston, A free energy principle for the brain (J. Physiol. Paris 100): the bound stated for perception as variational inference on a generative model.
• 2010 — Friston, The free-energy principle: a unified brain theory? (Nat. Rev. Neurosci. 11, 127–138): free energy as an upper bound on surprisal, presented as the core of a unified account.
• 2017 — Friston, FitzGerald, Rigoli, Schwartenbeck, Pezzulo, Active inference: a process theory (Neural Comput. 29(1), 1–49): the same functional drives policy selection through expected free energy.
• 2022 — Parr, Pezzulo, Friston, Active Inference (MIT Press): textbook treatment; the posterior-form identity $F = D_{\mathrm{KL}}(Q\,\|\,P(s|o)) - \log P(o)$ as the central equation.
• 2026 — fep_formal (Active Inference Institute): a machine-checked Lean 4 catalogue of 155 Free Energy Principle topics, compiled with zero proof holes against a pinned Mathlib. This mission transcribes the catalogue's core-free-energy chain — topic fep-002 and the foundation module active_inference — onto the platform, turning the first link of the FEP development into solvable community infrastructure.

Setting

Everything is finite, and laws are normalized real mass functions.

A finite law on a finite type $\alpha$ is a function $p : \alpha \to \mathbb{R}$ with $p(x) \ge 0$ for every $x$ and $\sum_x p(x) = 1$. A finite kernel from $\alpha$ to $\beta$ assigns to each $x \in \alpha$ a normalized row over $\beta$. The mission's definitions Def_fep_finite_laws and Def_fep_finite_information package these carriers with entropy, cross-entropy, and the KL divergence

$$D_{\mathrm{KL}}(p\,\|\,q) \;=\; \sum_{x} q(x)\cdot \mathrm{klFun}\!\left(\frac{p(x)}{q(x)}\right), \qquad \mathrm{klFun}(x) = x\log x + 1 - x,$$

a totalized real-valued divergence that is finite even at zero-mass atoms (the convention $0 \cdot \log 0 = 0$ via Real.negMulLog) and nonnegative on normalized laws.

A finite generative model for active inference (definition Def_fep_generative_model) over finite types $\mathsf{Policy}, \mathsf{State}, \mathsf{Outcome}$ consists of: an initial state law $P(s)$; a policy-conditioned transition kernel; a state-to-outcome likelihood kernel; a preference law over outcomes; and a policy prior. Under a policy $\pi$ the model predicts the state law $P(s \mid \pi)$ and the outcome law $P(o \mid \pi)$. A recognition density is any finite law $Q$ over states — the system's internal estimate. At an outcome $o$ with positive predicted mass, the Bayesian posterior $P(\cdot \mid o, \pi)$ is the exact finite Bayes rule. The outcome surprisal is $-\log P(o \mid \pi)$, and the posterior-form variational free energy of a recognition density $Q$ is

$$F[Q, o, \pi] \;=\; D_{\mathrm{KL}}\big(Q \,\|\, P(\cdot \mid o, \pi)\big) \;-\; \log P(o \mid \pi).$$

Formalization targets

Goal: the variational free-energy bound

For every generative model, every policy $\pi$, every outcome $o$ with $P(o\mid\pi) > 0$, and every recognition density $Q$:

$$-\log P(o \mid \pi) \;\le\; F[Q, o, \pi].$$

The recognition density $Q$ is universally quantified — the bound holds for whatever state estimate the system happens to carry.

Exactness, uniqueness, and the ELBO form

Three companions pin down the equality case, ordered weakest to strongest alongside the milestone list:

• Exactness — the Bayesian posterior attains the bound:

$$F\big[P(\cdot \mid o, \pi),\, o,\, \pi\big] = -\log P(o \mid \pi).$$

• Uniqueness — equality characterizes the posterior, with no full-support assumption:

$$F[Q, o, \pi] = -\log P(o \mid \pi) \iff Q = P(\cdot \mid o, \pi).$$

• ELBO form — negating both sides:

$$-F[Q, o, \pi] \;\le\; \log P(o \mid \pi).$$

Measure-theoretic core

Independently of the finite model, in Mathlib's nonnegative extended reals $\mathbb{R}_{\ge0} \cup \{\infty\}$, with $q$, $p$ measures on any measurable space and $s \in \mathbb{R}_{\ge0} \cup \{\infty\}$:

$$s \;\le\; s + D_{\mathrm{KL}}(q \,\|\, p),$$

the unconditional shape of the bound (topic fep-002 of the source catalogue), with the divergence taken as $\infty$ when the log-likelihood ratio is not integrable.

Significance

The result itself. This inequality is the load-bearing step of the FEP: it converts "minimize free energy" into "move recognition toward the posterior," and it is the exact statement whose continuous, dynamic, and policy-selecting extensions (expected free energy, Markov blankets, non-equilibrium thermodynamics) form the rest of the FEP literature. Without it, the principle's variational step has no mathematical content.

Formalizing it. The mathematics here is classical — Gibbs' inequality — and the source development already proves every row with no proof holes. What the mission adds is faithful, reusable infrastructure: the definitions are published as platform nodes in the shared namespace FreeEnergyPrinciple, so later missions in this programme (expected free energy and policy selection, Markov blankets, Gaussian and continuous-time variants, already proved in the source repository) can import them instead of re-deriving the substrate. Status honesty: all eight items below are formalized and machine-checked locally against the platform environment; each is an open problem on the platform only in the sense that no proof has yet been submitted to it.

Difficulty

The bound itself is a one-line consequence of KL nonnegativity — the naive idea "prove it by simp on the KL sum" is essentially right, and the source proofs are correspondingly short. The actual difficulty is boundary precision, where plausible renderings go silently wrong:

• The positivity premise $P(o \mid \pi) > 0$ is not decoration: the Bayesian posterior is defined only where the evidence has positive mass, and hiding that in a totalized division would change the statement.
• The uniqueness characterization is not a formality: at zero-mass reference atoms the logarithmic cross-entropy identity degenerates, and the proof needs the normalization lemma $D_{\mathrm{KL}}(p\,\|\,q) = 0 \leftrightarrow p = q$, which forces the recognition law's mass to zero wherever the posterior's is zero. A solver who proves the bound but states equality with a full-support hypothesis has proved something different from the source.
• The measure-theoretic core is deliberately unconditional; adding finiteness side conditions to it would weaken the source's point that $\mathbb{R}_{\ge0} \cup \{\infty\}$ absorbs the degenerate cases.

A vacuous formalization — quantifying over a single distinguished recognition law, or taking "posterior" as an arbitrary variable — would trivialize the goal; the targets below rule this out by fixing the exact finite Bayes rule and universally quantifying $Q$.

Formalization scope

Committed conventions of this mission's Lean development:

• All model carriers are finite types (Fintype); laws are $\mathbb{R}$-valued normalized mass functions; kernels are normalized rows. No measure-theoretic machinery below the finite substrate except for the measure-theoretic core milestone.
• KL is the totalized real-valued finite divergence $D_{\mathrm{KL}}(p\,\|\,q) = \sum_x q(x)\cdot \mathrm{klFun}(p(x)/q(x))$; entropy uses Real.negMulLog, so $0 \cdot \log 0 = 0$ exactly, not by exception-handling.
• The posterior is the exact finite Bayes rule FiniteKernel.posterior, taken at the explicit hypothesis $0 < P(o \mid \pi)$.
• One mission-wide namespace FreeEnergyPrinciple; definitions live in the published definition files Def_fep_finite_laws, Def_fep_finite_information, Def_fep_generative_model, and every theorem item imports them. A Free Energy Principle II mission (expected free energy) is expected to reuse the same namespace and definitions.
• The measure-theoretic core uses Mathlib's InformationTheory.klDiv in ℝ≥0∞ with no finiteness hypotheses.
• Contributions welcome: alternative measure-theoretic renderings of the core bound, the Gaussian instantiation of the same identity, and ports of the source repository's subsequent rows (Bayesian model reduction, expected free energy) onto these definitions.

Selected references

• K. Friston, A free energy principle for the brain, Journal of Physiology (Paris) 100 (2006) 70–87. https://doi.org/10.1016/j.jphysparis.2006.10.001
• K. Friston, The free-energy principle: a unified brain theory?, Nature Reviews Neuroscience 11 (2010) 127–138. https://doi.org/10.1038/nrn2787
• K. Friston, T. FitzGerald, F. Rigoli, P. Schwartenbeck, G. Pezzulo, Active inference: a process theory, Neural Computation 29 (2017) 1–49. https://doi.org/10.1162/neco_a_00912
• T. Parr, G. Pezzulo, K. J. Friston, Active Inference: The Free Energy Principle in Mind, Brain, and Behavior, MIT Press (2022). https://mitpress.mit.edu/9780262045354/active-inference/
• D. A. Friedman, fep_formal: Towards Lean 4 Formalization of the Free Energy Principle (v1.2.0), Active Inference Institute (2026), the formal source of truth for this mission. https://github.com/ActiveInferenceInstitute/fep_formal
• D. A. Friedman, Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, Active Inference Journal (2026). https://doi.org/10.5281/zenodo.19699233

Why control variates matter in federated optimization

Federated optimization trains one model using objectives held by many clients. Performing several local updates between communication rounds saves communication, but clients with different objectives can move in different directions. SCAFFOLD maintains a correction for each client to address this disagreement, including when only some clients participate. Karimireddy et al. establish convergence without a bound on how similar the client objectives are. The relevant result is Theorem III, Section 5, PDF p. 5.

SCAFFOLD: Convergence with Client Sampling concerns that known result's formalization. Its exact targets are finite-round bounds from the Appendix E analysis, covering strongly convex, general convex, and nonconvex objectives. The paper's FedAvg results and its separate quadratic-acceleration theorem are outside this scope.

Setting: local updates and sampled clients

There are $N\ge1$ clients, with differentiable objectives $f_i:\mathbb R^d\to\mathbb R$. The global objective is $f(x)=N^{-1}\sum_i f_i(x)$. Every client gradient is $\beta$-Lipschitz, where $\beta>0$. A stochastic gradient query is conditionally unbiased and has conditional squared-error expectation at most $\sigma^2$, with $\sigma\ge0$. Current queries on different clients are conditionally independent given the full history. These make precise the fresh-oracle interpretation of A4–A5, Appendix B.1, PDF p. 14.

Each of $T\ge1$ rounds selects a uniform subset $A_r$ of $S$ clients, where $1\le S\le N$. Each selected client takes $K\ge1$ local steps. Let $x^r$ be the server model, $c_i^r$ its stored client control variates, and $c^r=N^{-1}\sum_i c_i^r$. With constant local and global step sizes $\eta_l>0$ and $\eta_g\ge1$, a client starts at $y_{i,0}^r=x^r$ and uses

$$y_{i,k+1}^r=y_{i,k}^r-\eta_l\bigl(g_{i,k}^r-c_i^r+c^r\bigr), \qquad x^{r+1}=x^r+\frac{\eta_g}{S}\sum_{i\in A_r}(y_{i,K}^r-x^r).$$

Option II replaces a participating client's control with $K^{-1}\sum_{k=0}^{K-1}g_{i,k}^r$ and retains every other control. These are Algorithm 1, PDF p. 4, and Appendix E, equations (18)–(21), PDF pp. 25–26. Write $h=K\eta_l\eta_g$ for the effective step size.

Formalization targets

Four milestones support a root goal that is the conjunction of the two convergence statements below.

GradientGrowth states, for convex clients and a global minimizer $x^\star$,

$$\frac1N\sum_i\|\nabla f_i(x)-\nabla f_i(x^\star)\|^2 \le2\beta\bigl(f(x)-f(x^\star)\bigr).$$

This is Appendix B.1, equation (9), PDF p. 14. PerturbedStrongConvexity states, for each $\mu$-strongly convex client and $\mu\ge0$,

$$\langle\nabla f_i(x),z-y\rangle\ge f_i(z)-f_i(y) +\frac\mu4\|y-z\|^2-\beta\|z-x\|^2,$$

as in Appendix C, Lemma 5, PDF p. 17.

ConvexFiniteRoundConvergence allows arbitrary deterministic initial controls $c_i^0$. Assume all clients are $\mu$-strongly convex with $\mu\ge0$, including ordinary convexity when $\mu=0$, and fix a minimizer $x^\star$ of $f$. Define

$$C_0=\frac1N\sum_i\|c_i^0-\nabla f_i(x^\star)\|^2, \qquad V_0=\|x^0-x^\star\|^2+\frac{9Nh^2}{S}C_0,$$ $$q=1-\frac{\mu h}{2},\qquad w_r=q^{-(r+1)},\qquad W_T=\sum_{r=0}^{T-1}w_r.$$

For $h\le1/(81\beta)$ and $\mu h\le S/(15N)$, the target is

$$\frac1{W_T}\sum_{r=0}^{T-1}w_r\, \mathbb E\bigl[f(x^r)-f(x^\star)\bigr] \le\frac{V_0}{hW_T} +\frac{12h\sigma^2}{KS}\left(1+\frac S{\eta_g^2}\right).$$

This is a finite-round formulation of Appendix E.1, Lemma 15, PDF p. 30; its $\mu=0$ case is the first bound on PDF p. 31.

NonconvexFiniteRoundConvergence assumes a lower bound $f_\mathrm{lower}$ for $f$ and initializes every client control with $K$ fresh gradients at $x^0$. Put $F_0=f(x^0)-f_\mathrm{lower}$. For $h\le(S/N)^{2/3}/(24\beta)$, establish

$$\frac1T\sum_{r=0}^{T-1}\mathbb E\|\nabla f(x^r)\|^2 \le\frac{14F_0}{hT} +\frac{70\beta h\sigma^2}{KS}\left(1+\frac S{\eta_g^2}\right).$$

This is the explicit finite-round consequence targeted from Appendix E.2, Lemma 19, PDF p. 34, with the initialization specified on PDF pp. 31 and 35. The full-client warm start's communication cost is separate from these $T$ optimization rounds.

What the result establishes

The bounds quantify optimization progress under stochastic gradients, several local steps, and partial participation. They permit arbitrarily different client objectives within the stated smoothness and convexity assumptions. Their output is a weighted random server iterate, represented by its expected loss, or a uniform random server iterate for the squared-gradient guarantee; this follows the output convention in equation (22), PDF p. 26.

The mathematical convergence analysis is published. The open work here is a Lean proof under the explicit stochastic-run model. The proposed statements do not themselves supply a machine-checked convergence proof. A completed development would provide reusable results about sampled finite averages, adaptive gradient queries, and optimization with stored noisy controls.

Where the difficulty lies

Local gradients are evaluated at different client states, and inactive clients retain controls computed in earlier rounds. Consequently, treating the server update as a centralized stochastic-gradient step discards both local disagreement and stale-control error. The challenge is to control these quantities while preserving their dependence on earlier randomness, as reflected in Appendix E.1–E.2, PDF pp. 26–35.

The source also needs careful transcription. The printed Theorem VII nonconvex noise term on PDF p. 25 differs from Lemma 19 in its smoothness and sampling factors, while output indices differ between equation (22) and the finite sum on p. 31. The exact targets above use the proof's finite-round constants and explicit indexing; they do not claim a verbatim formalization of every printed asymptotic rate.

Formalization scope

SCAFFOLD.Space is finite-dimensional real Euclidean space; SCAFFOLD.Problem records differentiable client objectives and smoothness. SCAFFOLD.Run records a standard Borel probability space, full-history filtration, measurable square-integrable iterates and oracle samples, and the concrete updates. Virtual local paths are generated before a fresh uniform size-$S$ subset is sampled, as permitted by the paragraph after equation (22), PDF p. 26.

The conventions include $S=N$, $K=1$, zero noise, and $\mu=0$. The output indices are precisely $0,\ldots,T-1$. Convex initial controls are deterministic; the nonconvex branch uses the specified stochastic warm start. The run definition assumes no descent inequality or convergence conclusion. Contributions should establish the four named propositions and necessary analysis/probability infrastructure while retaining these semantics.

Selected references

• Sai Praneeth Karimireddy, Satyen Kale, Mehryar Mohri, Sashank J. Reddi, Sebastian U. Stich, and Ananda Theertha Suresh, SCAFFOLD: Stochastic Controlled Averaging for Federated Learning, ICML 2020, PMLR 119:5132–5143; arXiv:1910.06378v4, revised 2021. Primary scope: Theorem III, PDF p. 5; A3–A5 and (9), p. 14; Lemma 5, p. 17; Appendix E, pp. 25–35, especially Lemmas 15 and 19.

Why local training needs a convergence guarantee

Federated optimization studies learning when data and computation are spread across clients. Communicating after every stochastic gradient step can be costly, so clients often take several steps before averaging their models. The difficulty is that different clients can optimize different objective functions. Their models then move apart between communication rounds. A convergence guarantee must account for both stochastic gradient noise and this disagreement. Wang et al. give an explicit analysis of this tradeoff in A Field Guide to Federated Optimization, Section 6.1.

The relevant historical sequence is the introduction of FedAvg by McMahan et al. in 2017, the development of local-SGD convergence analyses reviewed by Wang et al., and the unified illustrative analysis in the 2021 field guide. The present target is that guide's known convex convergence theorem, rather than a new conjecture about arbitrary federated learning. The remaining open task is a Lean proof of the stated result. The mission is categorized as ResearchPaper: it formalizes a specific known result rather than proposing a new mathematical conjecture.

Setting: full participation with uniform weights

There are $M\ge1$ clients and a parameter vector in $\mathbb R^d$. Client $i$ has a differentiable convex objective $F_i$. The global objective is $F(x)=M^{-1}\sum_{i=1}^M F_i(x)$. Every local gradient is $L$-Lipschitz for the same $L>0$. Fix a global minimizer $x^\star$ of $F$ and a deterministic initial model $x_0$, and write $D=\|x_0-x^\star\|$.

Every client participates in every round. Each of $T\ge1$ rounds consists of $\tau\ge1$ local steps with constant learning rate $\eta$. If $x_i^{t,k}$ is client $i$'s state after $k$ local steps of round $t$, its next state is $x_i^{t,k+1}=x_i^{t,k}-\eta g_i^{t,k}$. At the next round all clients restart from the average of the preceding round's terminal states. The shadow iterate is $\bar x^{t,k}=M^{-1}\sum_i x_i^{t,k}$; it is defined even at local steps where clients do not communicate.

On a probability space $(\Omega,\mathcal A,\mathbb P)$, the history before a step contains all past oracle draws. The stochastic gradients are conditionally unbiased, their conditional squared errors have expectation at most $\sigma^2$, and the different clients' current gradients are conditionally independent. The heterogeneity bound is $\|\nabla F_i(x)-\nabla F(x)\|\le\zeta$ for every client and every point, where $\sigma,\zeta\ge0$. These are the assumptions of Section 6.1.1, PDF p. 40, equations (11)–(14), with the history and independence convention used explicitly in Appendix D.1 immediately after equation (27), PDF p. 87.

Formalization targets

The principal goal is Theorem 1, equation (15). For $0<\eta\le1/(4L)$, establish

$$\mathbb E\!\left[\frac1{\tau T}\sum_{t=0}^{T-1}\sum_{k=1}^{\tau} \bigl(F(\bar x^{t,k})-F(x^\star)\bigr)\right] \le \frac{D^2}{2\eta\tau T}+\frac{\eta\sigma^2}{M} +4\tau\eta^2L\sigma^2+18\tau^2\eta^2L\zeta^2.$$

Two source milestones describe the intermediate results. Lemma 1 bounds the conditional average loss within a round by the decrease of squared distance to the minimizer, plus a noise term and a sum of client disagreements. Lemma 2 bounds each conditional squared disagreement by $18\tau^2\eta^2\zeta^2+4\tau\eta^2\sigma^2$. Both are stated on PDF p. 41, Section 6.1.2, with proofs in Appendix D, PDF pp. 86–88. They remain genuine open proof obligations; the algorithm model does not assume either estimate.

An additional milestone records the same theorem's tuned-step consequence, equations (16)–(17), in the regime $D,\sigma,\zeta>0$. With

$$\eta=\min\left\{\frac1{4L}, \frac{\sqrt M D}{\sqrt\tau\sqrt T\sigma}, \frac{D^{2/3}}{\tau^{2/3}T^{1/3}L^{1/3}\sigma^{2/3}}, \frac{D^{2/3}}{\tau T^{1/3}L^{1/3}\zeta^{2/3}}\right\},$$

the same expected loss is at most

$$\frac{2LD^2}{\tau T}+\frac{2\sigma D}{\sqrt{M\tau T}} +\frac{5L^{1/3}\sigma^{2/3}D^{4/3}}{\tau^{1/3}T^{2/3}} +\frac{19L^{1/3}\zeta^{2/3}D^{4/3}}{T^{2/3}}.$$

The principal goal includes zero-noise and zero-heterogeneity cases. The extra positivity conditions apply only to the printed tuned-step formula, whose denominators otherwise require separate conventions.

What this establishes

The bound separates an initial-distance term, a noise term improved by the number of clients, and two costs of local updates. It quantifies how local work interacts with stochastic noise and differing client objectives. Its conclusion concerns the average objective gap along the post-update shadow sequence; it does not assert the same bound for every last iterate or for the average of client losses. These distinctions follow directly from the quantity defined in equation (14).

A completed formalization would provide reusable checked components for stochastic optimization: finite client averages, history-conditioned oracle assumptions, per-round potential estimates, and disagreement bounds. The paper supplies the mathematical proof; this draft supplies checked statements and definitions. No convergence proof is claimed by creating or compiling the proposal.

Where the difficulty lies

The average update evaluates each gradient at its own client's state. It therefore does not directly equal a centralized stochastic-gradient step at the shadow iterate. A proof must control that discrepancy quantitatively, preserve the conditioning on the round's starting history, and justify the $1/M$ noise improvement using independent client sampling. Ignoring the sampling relationship can invalidate the advertised bound even for scalar quadratic objectives.

Formalization scope

The model uses finite-dimensional real Euclidean space, including the harmless zero-dimensional case, and a standard Borel probability space. A filtration indexed by $t\tau+k$ records the full past. Local states and gradients carry explicit measurability and finite-second-moment conditions. These probability conventions support actual Bochner and conditional expectations; integrals are not treated as arbitrary total functions without analytic obligations.

The local objectives, global objective, gradients, iterates, and shadow averages are concrete functions. The model assumes neither a drift bound nor a progress bound. Source hypotheses are uniform in the model point, and the minimizer is an actual minimizer of the averaged objective. Unequal weighting, partial client participation, nonconvex objectives, adaptive step sizes, and privacy mechanisms are outside this particular theorem. Contributions should prove the named source lemmas or their necessary analytic infrastructure while retaining these statements.

Selected references

• Jianyu Wang et al., A Field Guide to Federated Optimization, 2021, arXiv:2107.06917v1, Section 6.1.1–6.1.2, PDF pp. 40–41; Appendix D, PDF pp. 86–88.
• H. Brendan McMahan et al., Communication-Efficient Learning of Deep Networks from Decentralized Data, AISTATS 2017, arXiv:1602.05629, the FedAvg algorithm cited by the field guide. This is historical context, not an additional target.

Motivation

Bayesian filtering estimates an unobserved state from measurements arriving over time. A filter combines what the state dynamics predict with what the newest observation says. In neural decoding, for example, the state may describe an intended movement while the observation contains activity from many recorded neurons. The observation can have many more coordinates than the state and need not follow a linear Gaussian observation model.

The Discriminative Kalman Filter (DKF) uses a Gaussian approximation to the state conditional on the newest observation. It combines that approximation with a Gaussian state transition and a correction for the stationary state distribution. The resulting recursion retains a mean vector and covariance matrix. Burkhart et al. developed this construction and proved an asymptotic justification in Theorem 2 of Appendix B.

The historical starting point is the linear Gaussian filter of Kalman (1960). The 2020 DKF paper changes how observation information enters the update and establishes a corresponding approximation theorem. The present mission concerns formal verification of that published theorem.

Setting

The state space is $\mathbb R^d$ for a positive finite dimension $d$. Write $\eta_d(z;m,C)$ for the ordinary multivariate Gaussian density with mean $m$ and symmetric positive-definite covariance $C$. Densities and their $L^1$ distances are with respect to Lebesgue measure.

The state model has a matrix $A$ and positive-definite covariance matrices $\Gamma,S$ satisfying

$$S=ASA^\top+\Gamma.$$

Its stationary density and transition density are

$$p(z)=\eta_d(z;0,S),\qquad \tau(y,z)=\eta_d(z;Ay,\Gamma).$$

For an integrable density $s$, prediction gives

$$(\tau s)(z)=\int\tau(y,z)s(y)\,dy.$$

The discriminative update combines a previous filtering density $s$ with a density $u$ for the state given the current observation:

$$\frac{u\,\tau s/p}{\|u\,\tau s/p\|_1}.$$

This expression is a probability density when its nonnegative weight has a finite, strictly positive integral. Dividing by $p$ is part of the standard DKF under consideration.

For Gaussian inputs with parameters $(a,V)$ and $(b,U)$, define

$$G=AVA^\top+\Gamma,\qquad T=(U^{-1}+G^{-1}-S^{-1})^{-1},$$ $$c=T(U^{-1}b+G^{-1}Aa).$$

The DKF step returns mean $c$ and covariance $T$ when the precision is invertible and the covariance is positive definite. The recursive filter starts from mean zero and covariance $S$, using the current observation's functions $f$ and $Q$ as the Gaussian input mean and covariance. These are the updates in equation (2.7) of the paper.

Formalization targets

Fix sequences of probability densities $s_n,u_n$, indexed by positive integers, whose exact normalized updates

$$p_n=\frac{u_n\tau s_n/p}{\|u_n\tau s_n/p\|_1}$$

are well defined for every index. Fix Gaussian density sequences $s'_n,u'_n$, a point $b$, and a probability measure $P$. The five assumptions are

$$\begin{aligned} \mathrm{A1}:&\quad s_n\Rightarrow P,\\ \mathrm{A2}:&\quad \|s_n-s'_n\|_1\longrightarrow0,\\ \mathrm{A3}:&\quad u_n\Rightarrow\delta_b,\\ \mathrm{A4}:&\quad \|u_n-u'_n\|_1\longrightarrow0,\\ \mathrm{A5}:&\quad p_n\Rightarrow\delta_b. \end{aligned}$$

Here $\Rightarrow$ denotes weak convergence, characterized by convergence of expectations of every bounded continuous real function; $\delta_b$ is the unit point mass at $b$. The measure $P$ need not have a density and may be degenerate.

The main goal is the complete conjunction of Theorem 2's conclusions, with separate milestones for each:

• C1: $s'_n\Rightarrow P$.
• C2: $u'_n\Rightarrow\delta_b$.
• C3: the specific update

$$p'_n=\frac{u'_n\tau s'_n/p}{\|u'_n\tau s'_n/p\|_1}$$

is a well-defined Gaussian density for all sufficiently large $n$.

• C4: $p'_n\Rightarrow\delta_b$.
• C5: $\|p_n-p'_n\|_1\longrightarrow0$.

A sixth milestone is Lemma 1 (DKF equation): the normalized Gaussian-input update has the explicit mean and covariance above whenever valid, and the two input weak limits imply its eventual validity and convergence to $\delta_b$. It includes both the exact equation and the asymptotic assertion from the source.

Significance

In addition to neurodecoding with intracortical brain-computer interfaces, the DKF has also found applications in optimization and sequential data augmentation (see references). The original study was successfully reproduced by Casco-Rodriguez, et al. in ReScience C.

Difficulty

The inverse stationary density can grow in the tails, so small $L^1$ errors in the input densities do not immediately control the error after division and renormalization. Normalizing constants must remain finite and nonzero. The candidate Gaussian covariance must also become positive definite as a conclusion of the assumptions, rather than through an extra validity assumption imposed at every index.

There is a second distinction between convergence to a point mass and approximation in $L^1$. Two sequences may concentrate at the same point while retaining different shapes at shrinking scales. The C5 target therefore requires the full approximation argument, beyond the weak-convergence conclusions.

Formalization scope

Lean represents states as Fin d → ℝ and covariance matrices as real square matrices. The Gaussian density is the standard determinant-and-quadratic-form formula. The definition of Gaussian PDF includes positive-definite covariance and equality of densities almost everywhere. Thus null-set changes do not constrain the theorem artificially.

Probability density validity explicitly includes nonnegativity almost everywhere, integrability and total integral one. The $L^1$ quantity is an extended nonnegative integral. The update's validity explicitly requires measurable weight and a finite, strictly positive normalizer. Total expressions outside that domain supply no assumed probability interpretation; C3 establishes validity on a tail.

All density sequences use positive integer indices. The limit measure is a Mathlib probability measure. Weak convergence is tested against Mathlib bounded continuous functions using the actual measures generated by the densities. The stationary model, standard recursive DKF, exact update and approximate update are defined independently of the theorem conclusions.

The mission addresses deterministic Theorem 2 of Appendix B. The random-sequence extension in Remark 4, conditions implying a Bernstein–von Mises theorem, and induction over filtering time are separate developments. The proof plan follows the appendix through C1–C2, Lemma 1, C3–C4, and the five-term comparison for C5.

Selected references

• M. C. Burkhart, D. M. Brandman, B. Franco, L. R. Hochberg and M. T. Harrison, The Discriminative Kalman Filter for Bayesian Filtering with Nonlinear and Nongaussian Observation Models, Neural Computation 32(5), 969–1017, 2020. DOI: 10.1162/neco_a_01275.
• R. E. Kalman, A New Approach to Linear Filtering and Prediction Problems, Journal of Basic Engineering 82(1), 35–45, 1960. DOI: 10.1115/1.3662552.
• M. C. Burkhart, A Discriminative Approach to Bayesian Filtering with Applications to Human Neural Decoding, Ph.D. dissertation, Brown University, 2019. DOI: 10.26300/nhfp-xv22.
• D. M. Brandman, M. C. Burkhart, J. Kelemen, B. Franco, M. T. Harrison and L. R. Hochberg, Robust Closed-Loop Control of a Cursor in a Person with Tetraplegia using Gaussian Process Regression, Neural Computation 30(11), 2986–3008, 2018. DOI: 10.1162/neco_a_01129.
• D. M. Brandman, T. Hosman, J. Saab, M. C. Burkhart, B. E. Shanahan, J. G. Ciancibello et al., Rapid calibration of an intracortical brain–computer interface for people with tetraplegia, Journal of Neural Engineering 15(2), 026007, 2018. DOI: 10.1088/1741-2552/aa9ee7.
• J. Casco-Rodriguez, C. Kemere and R. G. Baraniuk, [Re] The Discriminative Kalman Filter for Bayesian Filtering with Nonlinear and Non-Gaussian Observation Models, ReScience C 10(1), article 3, 2025. DOI: 10.5281/zenodo.15172014, published PDF.
• M. C. Burkhart, Discriminative Bayesian filtering lends momentum to the stochastic Newton method for minimizing log-convex functions, Optimization Letters 17, 657–673, 2023. DOI: 10.1007/s11590-022-01895-5.

Motivation

Transformer sequence models modulate attention scores by a function of the relative position between a query and a key: the attention logit between token $m$ and token $n$ is scaled by a fixed profile $f(p_m - p_n)$. Realizing this modulation the naive way means evaluating $f$ once per pair $(m,n)$ and materializing an $L\times L$ adjustment over the whole sequence — quadratic in the sequence length $L$. Rotary Position Embedding (RoPE) Su et al. 2021 avoids this entirely: it rotates the query at position $p_m$ and the key at position $p_n$ independently, each by an angle depending only on its own position, so that the pairwise quantity $f(p_m-p_n)$ falls out of the dot product of the two separately rotated vectors — $f$ is never evaluated pairwise, and no $L\times L$ matrix is ever built. This is what lets RoPE stay a linear, per-token preprocessing step compatible with efficient (sub-quadratic) attention implementations, rather than an $O(L^2)$ modulation. The catch is that RoPE's specific log-linear frequency schedule bakes in one particular profile: a monotone, decaying $f$. That schedule is a poor fit whenever the correlation structure of the data is not monotonically decaying with distance — the leading example being periodicity: in sequential recommendation, interactions separated by exactly one day or one week are more correlated than interactions separated by, say, half a day, and a decaying profile cannot express that "attention comes back" at the period.

Chen, Ainslie, Choromanski et al., ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling (arXiv:2607.26369), ask a more general question first: which attention-modulation profiles $f$ can be realized at all by this same per-token, pairwise-iteration-free rotation trick — rotate each token once, on its own, and let the pairwise profile emerge from the dot product — and by what rotation-frequency schedule? Their answer is a random-features construction — sample the rotation frequencies from the kernel's own Fourier transform, rather than fixing them log-linearly — that realizes any continuous, normalized, positive-definite profile in expectation, with a quantified concentration rate, all while keeping the exact same per-token rotate-then-dot-product computation RoPE already uses. ClockRoPE is the periodic instance of this general theory, later deployed in a production-scale generative-retrieval system.

Setting

Fix an embedding dimension $d = 2n$ and group a vector $v \in \mathbb{R}^d$ into $n$ consecutive feature pairs $v^{(j)} = (v_{2j}, v_{2j+1}) \in \mathbb{R}^2$ for $j = 0, \dots, n-1$. For an angle $\theta$, let

$$R(\theta) = \begin{pmatrix} \cos\theta & -\sin\theta \\ \sin\theta & \cos\theta \end{pmatrix}$$

be the $2\times 2$ (Givens) rotation matrix. A real kernel $f : \mathbb{R} \to \mathbb{R}$ is positive definite if for every finite family of points $x_1,\dots,x_N \in \mathbb{R}$ and complex coefficients $c_1,\dots,c_N$, $\sum_{i,j} \overline{c_i} c_j f(x_i - x_j)$ has nonnegative real part; it is normalized if $f(0) = 1$. When $f$ is also continuous and Lebesgue-integrable, its Fourier transform

$$\tau(\xi) = \int_{\mathbb{R}} f(x) e^{-i2\pi\xi x}\,dx$$

is (by Bochner's theorem) a genuine probability density on $\mathbb{R}$: this is the distribution the mission's rotation frequencies are sampled from.

Given a query $q_m \in \mathbb{R}^{2n}$ at position $p_m$, a key $k_n \in \mathbb{R}^{2n}$ at position $p_n$, and $n$ i.i.d. frequencies $\xi_0, \dots, \xi_{n-1} \sim \tau$, the Random Fourier Rotation (RFR) estimator is

$$\hat g(q_m, k_n, p_m, p_n) = \sum_{j=0}^{n-1} \big(R(2\pi\xi_j p_m)\, q_m^{(j)}\big)^\top \big(R(2\pi\xi_j p_n)\, k_n^{(j)}\big).$$

$\hat g$ is exactly the modulated attention logit computed by rotating query/key feature pairs with per-pair, sampled RoPE frequencies — the same operation standard RoPE performs, but with $\xi_j$ drawn from $\tau$ instead of fixed by a log-linear schedule.

Formalization targets

Goal — convergence of the RFR estimator (Proposition 3.2)

$$P\!\left(\left|\tfrac1n \hat g(q_m,k_n,p_m,p_n) - \tfrac1n\, q_m^\top k_n f(p_m-p_n)\right| \ge \epsilon\right) \le 2\exp\!\left(-\frac{\epsilon^2(2n)^2}{8\sum_{j=0}^{n-1}\big(\lVert q_m^{(j)}\rVert\, \lVert k_n^{(j)}\rVert\big)^2}\right)$$

for every $\epsilon > 0$. This is the mission's central target: it upgrades the mean identity below into a quantitative, non-asymptotic guarantee that the sampled estimator is close to the target profile with high probability, at a rate that is exponential in the embedding dimension $d = 2n$.

Milestone — unbiasedness of the RFR estimator (Proposition 3.1)

$$\mathbb{E}_{\xi_0,\dots,\xi_{n-1}\sim\tau}\big[\hat g(q_m,k_n,p_m,p_n)\big] = q_m^\top k_n\, f(p_m-p_n).$$

The expectation identity that the concentration bound above sharpens; it is the feasibility half of the claim ("this construction is correct on average") that the convergence half needs as its starting point.

Milestone — periodic case via Herglotz's theorem (Corollary 3.3)

For a continuous, positive-definite, $T$-periodic $f$ with $f(0)=1$ and Fourier coefficients $\alpha_k = \frac1T \int_0^T f(x) e^{-i2\pi kx/T}\,dx$,

$$\alpha_k \ge 0 \text{ for all } k \in \mathbb{Z}, \qquad \sum_{k=-\infty}^{\infty} \alpha_k = f(0) = 1.$$

The periodic specialization needed to apply the goal and first milestone with a discrete frequency distribution over harmonics $k/T$ — the regime ClockRoPE actually deploys, since daily/weekly routines are periodic rather than merely decaying.

Significance

The result gives a general recipe — sample, don't hand-design — for turning any admissible attention-modulation profile into a RoPE-compatible rotation schedule, with a concentration guarantee that says how many feature pairs are needed before the sampled schedule reliably approximates the target profile. Crucially, the recipe changes only which frequencies the per-token rotation uses — it never touches the computational shape of RoPE itself: each query and key is still rotated once, independently, by an angle depending only on its own position, and the target pairwise profile $f(p_m-p_n)$ is still recovered purely from the dot product of the two rotated vectors. So realizing an arbitrary positive-definite $f$ this way costs exactly what realizing RoPE's own log-linear profile costs — linear in the sequence length, with no pairwise evaluation of $f$ and no $L\times L$ matrix ever materialized — rather than the quadratic cost a direct, per-pair implementation of an arbitrary modulation function would require. This subsumes standard RoPE's log-linear schedule as one instance and explains, via the periodic corollary, why a schedule built from the kernel's own spectrum (rather than an arbitrary log-linear one) is the right way to encode periodicity: nothing about the construction, or its efficiency, is specific to decay. The paper reports this translated into measured gains in a production-scale generative-retrieval system, which is unusual weight of practical evidence behind a Bochner/Herglotz-style spectral argument.

At the time of writing, none of these three results have a machine-checked proof; this mission asks for the first formalization of all three, together with the shared scaffolding (feature-pair extraction, the rotation estimator, and the notion of a positive-definite kernel) they are stated over.

Difficulty

The natural first attempt at the concentration bound is a direct union bound or a naive variance argument, but the estimator $\hat g$ is a sum of $n$ terms that are each bounded (each rotated pair lies on a fixed-radius circle) rather than governed by a variance bound that shrinks with $n$ under a fixed frequency; the source proof instead applies McDiarmid's bounded-differences inequality, treating each sampled frequency $\xi_j$ as one coordinate of the input and bounding the one-coordinate change in $\hat g$ by $2\lVert q_m^{(j)}\rVert\lVert k_n^{(j)}\rVert$ via the maximal distance between two points on the unit circle — not by directly bounding a variance term. Establishing Proposition 3.1 itself already requires care: it requires justifying that $\tau$, defined purely as an integral transform of $f$, is in fact a legitimate probability density (Bochner's theorem), and then a real/complex bookkeeping argument identifying the real inner product of rotated pairs with the real part of a product of complex exponentials.

Formalization scope

The mission works over the reals and represents feature pairs as functions Fin (2 * n) → ℝ sliced into Fin n-indexed pairs, matching the "$n$ feature pairs, dimension $d = 2n$" convention used throughout; $2\times2$ rotations are ordinary Matrix (Fin 2) (Fin 2) ℝ values built with Matrix.mulVec/Matrix.dotProduct, and expectation over i.i.d. $\tau$-distributed frequencies is formalized as integration against the product measure MeasureTheory.Measure.pi of n independent copies of the measure with density $\tau$ (MeasureTheory.Measure.withDensity) — this is mathematically equivalent to, and more directly usable in Lean than, introducing an abstract probability space with named i.i.d. random variables.

Since a general continuous positive-definite kernel need not have an integrable Fourier transform (the periodic case in Corollary 3.3 is exactly the counterexample: its "Fourier transform" is a discrete measure, not a density) — the goal and first milestone add Integrable f as an explicit hypothesis beyond what the paper states in prose, so that $\tau$ is genuinely a density rather than a junk value. This is not a strengthening of the target profiles the paper cares about in practice (Gaussian, Laplace, and the cosine/Gaussian priors used by ClockRoPE itself are all integrable) and mirrors the paper's own split between the density case (Propositions 3.1–3.2) and the discrete, purely-periodic case (Corollary 3.3). A formalization that dropped this hypothesis and instead let the Fourier integral silently evaluate to Lean's junk value (0 for non-integrable integrands) would make the goal statement possible to "prove" vacuously and must be avoided.

Definitions needed: a positive-definite-kernel predicate, the real-valued Fourier transform of a kernel, feature-pair extraction, the $2\times2$ rotation matrix, and the RFR estimator itself — all reusable by any future mission formalizing RoPE-family positional encodings (e.g. STRING, nD-RoPE) or other random-Fourier-feature results. McDiarmid's inequality, if not already in Mathlib in the needed form, is itself a independently reusable contribution.

Selected references

• Yiwen Chen, Joshua Ainslie, Krzysztof Choromanski, Xiang Gao, Su-Lin Wu, Yiping Yuan, Qian Sun, ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling, 2026. arXiv:2607.26369
• Jianlin Su, Yu Lu, Shengfeng Pan, Ahmed Murtadha, Bo Wen, Yunfeng Liu, RoFormer: Enhanced Transformer with Rotary Position Embedding, arXiv, 2021. arXiv:2104.09864
• Ali Rahimi, Benjamin Recht, Random Features for Large-Scale Kernel Machines, NeurIPS, 2007.
• Salomon Bochner, Monotone Funktionen, Stieltjessche Integrale und harmonische Analyse, Springer, 1933.
• Gustav Herglotz, Über Potenzreihen mit positivem, reellem Teil im Einheitskreis, Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig, 1911.

Motivation

Reflection positivity and infrared bounds form a standard finite-volume route from the geometry of a lattice reflection to quantitative control of long wavelength fluctuations. In the classical argument, reflection positivity supplies a Cauchy--Schwarz inequality for reflected observables, while Fourier diagonalization of the lattice Laplacian identifies the free covariance used in the infrared comparison. These ingredients underlie rigorous results on continuous-symmetry lattice systems in Fröhlich, Simon, and Spencer's development of infrared bounds and spontaneous symmetry breaking (1976), and the general theory of reflection positivity developed by Fröhlich, Israel, Lieb, and Simon (1978). Related technology appears in Fröhlich and Spencer's treatment of the two-dimensional Abelian spin systems and Coulomb gas (1981).

The analytic and model-specific theorems are substantial, but their finite algebraic interface is sharply separable. This mission isolates that interface so later clock, XY, and Gaussian-domination developments can share one checked notion of reflection, one spectral covariance convention, and one treatment of the constant mode.

Setting

Let $X$ be a finite set of configurations on one side of a reflection plane. A full split configuration is a pair $(x,y)\in X\times X$, and reflection exchanges its two entries. A plus-half observable is a function $F:X\to \mathbb R$ lifted to $X\times X$ through the first coordinate. Its reflected copy therefore depends on the second coordinate.

A split weight is specified by a finite feature index $A$, real coefficients $c_a$, and features $\phi_a:X\to\mathbb R$:

$$W(x,y)=\sum_{a\in A}c_a\phi_a(x)\phi_a(y).$$

For a finite family of plus-half observables $F_i$, the reflected kernel is

$$K_{ij}=\sum_{(x,y)\in X\times X} W(x,y)F_i(x)F_j(y).$$

A real matrix is positive semidefinite here when it is symmetric and its quadratic form is nonnegative on every real coordinate vector.

The spectral side uses a finite mode set $I$ with a distinguished zero mode $0$. An infrared spectrum consists of a function $\lambda:I\to\mathbb R$ that is nonnegative and vanishes exactly at $0$. For $\beta>0$, the free mode covariance is diagonal, equals zero at the constant mode, and has entry

$$G_{kk}=\frac{1}{\beta\lambda_k}$$

away from zero. Covariance domination is tested only on source vectors whose zero-mode coordinate vanishes. The concrete spectral fixture is the $4\times4$ periodic square lattice, with tensor-product discrete Fourier modes and the nearest-neighbor graph Laplacian.

Formalization targets

Finite reflection positivity

The first target identifies the split reflection pairing with the explicit double sum over the two halves. Under $c_a\ge0$, the resulting reflected kernel must be positive semidefinite:

$$\sum_{i,j}u_iK_{ij}u_j\ge0.$$

Every such kernel must satisfy the two-observable chessboard inequality

$$K_{ij}^{2}\le K_{ii}K_{jj}.$$

Typed finite spectrum

For every Torus-4 frequency $k$ and site $x$, the registered Fourier mode $\psi_k$ must satisfy the pointwise eigenvalue equation

$$(\Delta_{\mathrm{T4}}\psi_k)(x)=\lambda_k\psi_k(x).$$

The eigenvalues must be nonnegative and vanish exactly at the constant mode, and these laws must be packaged as the same spectrum type consumed by the infrared definitions.

Zero-mode-restricted infrared bound

The diagonal free covariance must be positive semidefinite for $\beta>0$. If an interacting covariance $C$ is quadratically dominated by $G$ on sources with $u_0=0$, then every nonzero Fourier mode must satisfy

$$C_{kk}\le\frac{1}{\beta\lambda_k}\qquad(k\ne0).$$

Two finite counterfixtures are part of the target. They assert that an arbitrary full-vertex reflected two-point matrix need not be positive semidefinite, and that domination restricted away from the zero mode need not extend to full-matrix domination.

Significance

The resulting interface prevents three substitutions that otherwise look notational but change the theorem. Reflection positivity is tested on observables supported on one half rather than on an arbitrary matrix indexed by all vertices. The infrared comparison excludes the constant mode rather than forcing a fluctuating zero mode below a covariance with zero diagonal. The graph-Laplacian eigenvalue is connected to the Fourier mode by an explicit pointwise theorem rather than by assigning a function the name laplacianEigenvalue.

Several ingredients already have machine-checked Lean proofs in the LeanProofs repository: the finite matrix Cauchy--Schwarz theorem, the Torus-4 DFT diagonalization and zero-mode theorem, and the diagonal free-covariance calculation. This mission reorganizes those results around a corrected consumer boundary and adds the split-half and off-zero adapters. It does not present the finite statements as new mathematics.

Difficulty

The main difficulty is maintaining the correct domain at each interface. A reflection of lattice sites does not by itself imply positive semidefiniteness of a correlation matrix indexed by every site; the tested observables and their support are part of the assertion. Likewise, a free covariance whose constant-mode entry is defined to be zero cannot dominate an arbitrary covariance on all source vectors. Finally, a Fourier multiplier used for a pseudospectral derivative is not automatically the eigenvalue of the nearest-neighbor graph Laplacian. The formal statements must keep these three objects distinct.

Formalization scope

All configuration, feature, observable, and mode types are finite. Kernels, weights, coefficients, source vectors, and quadratic forms are real. Complex numbers occur only in the explicit discrete Fourier modes. Reflected pairings are unnormalized finite sums; no partition function or probability measure is introduced. The inverse temperature satisfies $\beta>0$. The distinguished zero mode is part of the spectrum interface, and infrared domination is restricted to source vectors that vanish at that coordinate.

The mission does not assert reflection positivity of a clock or XY Gibbs measure, nonnegative Fourier coefficients of a physical cross-bond weight, Gaussian domination, a thermodynamic limit, a Kosterlitz--Thouless transition, or a universal jump. It also does not identify the Torus-4 graph spectrum with the Grid3 pseudospectral multiplier from the Fourier--Hodge packet. Those are separate future missions requiring additional model and analytic input.

The reusable outputs are the split-weight RP interface, the finite positive-semidefinite kernel API, the typed spectrum object, and the zero-mode-restricted domination predicate. Contributions should preserve the explicit half support and zero-mode restrictions; a proof obtained by adding the desired conclusion as a hypothesis is outside scope.

Selected references

• J. Fröhlich, B. Simon, and T. Spencer, Infrared bounds, phase transitions and continuous symmetry breaking, Communications in Mathematical Physics 50 (1976), 79--95. https://doi.org/10.1007/bf01608557
• J. Fröhlich, R. Israel, E. H. Lieb, and B. Simon, Phase transitions and reflection positivity. I. General theory and long range lattice models, Communications in Mathematical Physics 62 (1978), 1--34. https://doi.org/10.1007/bf01940327
• J. Fröhlich and T. Spencer, The Kosterlitz--Thouless transition in two-dimensional Abelian spin systems and the Coulomb gas, Communications in Mathematical Physics 81 (1981), 527--602. https://doi.org/10.1007/bf01208273
• LeanProofs, ReflectionPositivityInfraredBound.lean, exact repository snapshot dbf503b2909cc17787d40a21eb75a0c9354cc6ef. https://github.com/MonumentalSystems/LeanProofs/blob/dbf503b2909cc17787d40a21eb75a0c9354cc6ef/LeanProofs/StatMech/ReflectionPositivityInfraredBound.lean

A performance guarantee for a simple replenishment rule

When replenishment takes several periods, an inventory decision commits stock before the demand that will consume it is known. Too much stock incurs holding costs; too little loses sales. An optimal decision can depend on the entire pipeline of outstanding orders. A rule with only two adjustable parameters is easier to implement, but its simplicity alone gives no guarantee on the cost it can incur.

Capped base-stock policies combine an inventory-position target with a maximum order quantity. The class was introduced and analyzed by Xin (2021). The present target is the finite-lead-time guarantee in Linwei Xin's Capped Base-Stock Policies: A 2.33-Approximation, specifically the author-supplied manuscript with source label thm-main. A public listing of the paper identifies the July 17, 2026 working paper; the supplied text is the authoritative version for this formalization.

Demand, stock, and delayed orders

Periods are discrete. Demand is a sequence of independent, identically distributed nonnegative real random variables $D_t$ with finite, strictly positive mean $\mu$. The deterministic lead time is an integer $L\ge1$. Holding and lost-sales rates are $h>0$ and $p>0$.

At the beginning of period $t$, $I_t$ is on-hand inventory and $x_{1,t},\ldots,x_{L,t}$ are outstanding orders, with $x_{1,t}$ due immediately. That arrival is received, an order $q_t\ge0$ is placed, demand is realized, and costs are charged. The new order arrives $L$ periods later. The equations are

$$I_{t+1}=(I_t+x_{1,t}-D_t)^+,\qquad x_{i,t+1}=x_{i+1,t}\ (i<L),\qquad x_{L,t+1}=q_t.$$

Here $u^+=\max\{u,0\}$. Unfilled demand is lost rather than backlogged. With $\ell_t=(D_t-I_t-x_{1,t})^+$, the period cost is $hI_{t+1}+p\ell_t$. Initial inventory and every pipeline coordinate are zero. A nonanticipative policy chooses orders using only information available before the current demand; policies may depend on the entire observed past and on independent private randomization.

For a policy $\pi$, its long-run expected average cost is

$$C(\pi)=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[hI_{t+1}^\pi+p\ell_t^\pi],\qquad \mathrm{OPT}=\inf_{\pi\in\Pi}C(\pi).$$

The capped rule is $q_t=\min\{(S-I_t-\sum_{i=1}^Lx_{i,t})^+,r\}$ for finite $S,r\ge0$. Write $C^*_{\rm CBS}=\inf_{S,r\ge0}C(\pi_{S,r})$. Ordinary base stock is already included by taking $r=S$; no infinite order cap is required.

Formalization targets

For $0\le r\le\mu$ and $m\ge1$, set

$$I_r^m=\max_{0\le k\le m}\sum_{i=1}^k(r-D_i),\qquad G_m(r,z)=\mathbb E\left[\left(I_r^m+\sum_{i=1}^m(D_i-r)-z\right)^+\right].$$

Empty sums are zero. The lower certificate is

$$\underline C=\inf\{hz+p(\mu-r):0\le r\le\mu,\ z\ge0,\ G_L(r,z)\le L(\mu-r),\ G_{L+1}(r,z)\le(L+1)(\mu-r)\}.$$

The pair $(0,0)$ is feasible. Both horizon constraints are retained. With

$$\kappa_L=1+\frac{4L^2}{(L+1)(3L-1)},$$

the goal is Theorem 1's complete assertion:

$$C^*_{\rm CBS}\le\kappa_L\underline C,\qquad C^*_{\rm CBS}\le\kappa_L\mathrm{OPT}\le\frac73\mathrm{OPT}.$$

The exact rational constant is used; the title's 2.33 is a rounded description. Multiplicative inequalities also make sense when the optimal cost is zero.

Five supporting targets reproduce selected source statements: Proposition 1's lower-certificate bound; Proposition 2's finite-cap cost conclusion; Lemma 2's bound on a consecutive block in the greedy recursion; Proposition 3's ordinary-base-stock cost bound; and Proposition 4's two-branch inequality. The finite-cap and ordinary-base-stock parameters remain exactly $(S,r)=((L+1)r+z,r)$ and $S=(L+1)r+2z$, respectively. Labels accompany the printed numbering so the supplied source is unambiguous.

What completing the mission establishes

The result gives a uniform cost guarantee for this policy class across all positive holding and penalty rates, every positive integer lead time, and arbitrary nonnegative demand laws with finite positive mean. It bounds the infimum of costs over the policy parameters; it does not by itself provide an algorithm for selecting parameters or assert that the infimum is attained. At $L=1$ the displayed coefficient is 2, while its uniform upper bound is $7/3$.

The manuscript supplies mathematical proofs. This mission asks for checked proofs of their formal statements. Compiling the declarations confirms that they are well formed, not that the claims are proved. A completed development would provide reusable delayed-inventory dynamics, measurable history policies, average-cost optimization objects, finite-horizon demand envelopes, and policy-comparison results.

Where the formal work lies

The pipeline carries consequences of past decisions across multiple demand periods. Nonanticipativity and independence must be stated precisely before expectation and convexity arguments can be used. Also, existence of a stationary distribution alone does not identify its expected cost with a long-run cost from an empty initial system. The manuscript invokes stationary results from prior inventory work, including Xin and Goldberg (2016), and uses stationary CBS quantities in intermediate arguments. Their needed hypotheses and connections to the original objective require proof within a complete development.

The two cost bounds depend on both coordinates of a feasible lower-certificate pair. Losing either horizon constraint changes that certificate. Replacing it with an arbitrary scalar lower bound or assuming the policy comparisons would remove substantive parts of the result.

Formalization scope and conventions

Stock, orders, and demand take arbitrary nonnegative real values. Time is represented from zero in the operational model, corresponding to period one in the manuscript. The formal representation uses a canonical probability model with independent demand coordinates and an independent uniform private seed; measurable time-dependent decision functions use only preceding demands and that seed. Connecting arbitrary standard-Borel randomized controls to this canonical realization is a representation obligation. The zero-start optimum ranges over these general history policies, not only stationary or capped policies.

Expected nonnegative costs, their upper limits, and cost infima are represented in the extended nonnegative reals. Thus a policy with infinite expected cost does not acquire a fictitious zero value through a totalized real integral. The finite-horizon envelope expectations use the original integrable demand law. The greedy lemma uses integer-indexed sequences so subtraction of earlier times has no natural-number truncation; its blocks are nonempty, as required to define their maximum.

Definitions contain no unproved facts. In particular, stationarity, convergence from the empty initial state, lower bounds, and upper policy comparisons are not fields assumed by the model. Contributions to these intermediate obligations and to any of the five source targets support the central theorem.

Selected references

• Linwei Xin, Capped Base-Stock Policies: A 2.33-Approximation, working paper, 2026. SSRN listing. Author-supplied LaTeX is authoritative: Theorem 1 (thm-main), Proposition 1 (lemma-lb), Proposition 2 (prop-finite-cap-bound), Lemma 2 (lem-greedy-window), Proposition 3 (prop-base-stock-bound), Proposition 4 (lem-two-branch). Source SHA-256: f353793c255e1ebed5f3ec541037284bd926183e3e5b71941f13e79c2d67cb7a.
• Linwei Xin, Technical Note—Understanding the Performance of Capped Base-Stock Policies in Lost-Sales Inventory Models, Operations Research 69(1), 61–70, 2021. DOI.
• Linwei Xin and David A. Goldberg, Optimality Gap of Constant-Order Policies Decays Exponentially in the Lead Time for Lost Sales Models, Operations Research 64(6), 1556–1565, 2016. DOI.

Motivation

In 1999 Artzner, Delbaen, Eber and Heath asked what a risk measure ought to satisfy, wrote down four axioms, and observed that the industry standard of the day -- Value-at-Risk -- fails one of them. The failing axiom is subadditivity: merging two positions should never require more capital than holding them apart. VaR can violate it, so under VaR a diversified book can appear riskier than its parts.

That observation did not stay academic. It is the reason the Basel framework moved its market-risk capital standard from Value-at-Risk to Expected Shortfall. Few results in mathematical finance have had a more direct regulatory consequence, and the mathematics is elementary enough to state completely.

Setting

A position is a payoff X : Fin (n+1) -> R across finitely many equally-weighted states, and a risk measure rho sends it to the capital that must be added to make it acceptable. Following Definition 2.4 of the paper, rho is coherent when it is translation-invariant, subadditive, positively homogeneous and monotone. Nonemptiness of the state space is carried in the index type so the worst case is always attained; no probability measure is needed for these four axioms, which is faithful to the paper -- Artzner et al. state T, S, PH and M without reference to one.

Value-at-Risk is defined here at an integer tolerance k rather than a probability level, which keeps the quantile unambiguous on a finite space: VaR X k is the least capital leaving at most k states in loss, corresponding to level k/(n+1).

The goal

The mission's goal theorem is the negative result: Value-at-Risk is not subadditive. A witness is 25 equiprobable states with X losing 100 in state 0 alone and Y losing 100 in state 1 alone. Each has one losing state in twenty-five, so at tolerance k = 1 both have VaR = 0; their sum loses in two states, exceeding the tolerance, so VaR (X+Y) 1 = 100 > 0 + 0. The witness was checked numerically before this mission was drafted; what is open is the Lean proof.

The milestones establish the positive contrast on the same footing: worst-case risk, the most conservative measure, satisfies all four axioms, so the failure is specific to VaR rather than inherent to risk measurement.

Source

P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent Measures of Risk, Mathematical Finance 9 (1999) 203-228. Axioms T, S, PH and M are Definition 2.4; the failure of subadditivity for VaR and the diversification consequence are discussed in Section 3.

The problem

(a) In a tennis match, you are the favorite, and win each point independently with probability $q\in(1/2,1)$. Let $n,m$ be odd positive integers greater than $1$. You have the choice between playing a best-of-$nm$ (i.e., you play $nm$ points and whoever wins the majority of points wins the match), or a best-of-$n$ of best-of-$m$'s (i.e., the match is won by winning the majority of $n$ "sets", and each "set" is won by winning the majority of $m$ points). Prove that your probability of winning the match is strictly greater by playing the best-of-$nm$.

(b) We now consider two generalizations: $m_1,\ldots,m_k$ are odd positive integers, while $n$ is any positive integer, with all integers being greater than $1$. You have the choice between playing a best-of-$nm_1\cdots m_k$, or a best-of-$n$ of "sets", which are best-of-$m_1$'s of "games", …, which are best-of-$m_k$'s of "points". In both cases, now that $n$ may be even, it is possible for the players to tie, in which case the match winner is determined by an independent fair coin. Prove again that your probability of winning the match is strictly greater by playing the best-of-$nm_1\cdots m_k$.

(c) We consider a further generalization where each completed "set" counts toward the match score in an independently random way:

• with probability $a$, the winner gains $1$ in the match score, as usual;
• with probability $b$, the set is ignored and does not count toward the match score;
• with probability $c$, the loser gains $1$ in the match score;

with $a+b+c=1$ and $a>c$, so players are still incentivized to win sets (previously we had $a=1$, $b=c=0$). This random scoring rule is applied once per completed set, at the outermost layer only: the games and points inside a set are decided by plain majorities, with no randomness, and only the set's final result is scored. If you choose to play the best-of-$nm_1\cdots m_k$, then each individual point counts as a set and is subject to the same randomness with probabilities $a,b,c$. Prove that your probability of winning the match is still strictly greater by playing the best-of-$nm_1\cdots m_k$ (the fair-coin-on-ties convention continues).

(d) Continue from part (c), but change the fair-coin-on-ties convention so that you only win the match if you have a strictly greater match score than your opponent. Assuming $b\ge1/2$, prove that your probability of winning the match is strictly greater by playing the best-of-$nm_1\cdots m_k$.

Source and connection to Dorner–Hardt

Florian E. Dorner and Moritz Hardt, Don't Label Twice: Quantity Beats Quality when Comparing Binary Classifiers on a Budget, ICML 2024. arXiv:2402.02249 (v3, 8 April 2026).

The paper asks how to spend a fixed budget of noisy crowdworker labels when comparing two binary classifiers: one label each for many data points, or several labels per data point aggregated by majority vote. It proves, via Cramér's theorem, that one label each is asymptotically optimal, and states the finite-sample version as an open conjecture (Section 5, Conjecture 1), still open in the April 2026 revision. Its Section 3 displays the finite-sample inequality for the independent, homogeneous-label case and verifies it numerically over about five billion parameter settings.

Part (d) of this mission with one level of sets is that Section 3 inequality in tennis language. A point is a single crowdworker label being correct ($q$ is the label accuracy); a set is a data point, whose test label is the majority of its $m$ labels; and the scoring rule is what the two classifiers do with that label. Writing $p$ for the worse classifier's accuracy and $p+\epsilon$ for the better one's, a set is scored to its winner when the better classifier alone matches the test label, ignored when the two classifiers agree, and scored to its loser when the worse classifier alone matches:

$$a=(p+\epsilon)(1-p),\qquad c=p(1-p-\epsilon),\qquad b=1-a-c,$$

so that $a-c=\epsilon>0$, and $b\ge1/2$ always holds because two classifiers of accuracy at least $1/2$ agree on at least half the data. Substituting into the paper's Proposition 1 recovers its gap-indicator probabilities exactly: $\Pr(+1)=q\epsilon+p(1-p-\epsilon)$, $\Pr(-1)=(1-q)\epsilon+p(1-p-\epsilon)$. The paper's inequality also allows $n=1$ and $q=1$, which parts (c)–(d) exclude only because the inequality can fail to be strict at $b=0$ there; for $b\ge1/2$ the same argument covers those edge cases. The paper's Conjecture 1 as literally stated concerns a correlated-error setting (its Section 3.2) and is not claimed here.

Parts (a)–(c) go beyond the paper's setting: arbitrary nesting depth, a fair-coin tie rule, and no constraint on the ignore rate $b$. The hypothesis $b\ge1/2$ in part (d) cannot be dropped: with one level, $(a,b,c)=(0.9,0.1,0)$, $q=0.6$, $m=3$, $n=1$, the single best-of-3 finishes strictly ahead with probability $0.5832$ while three single points do so with probability $0.5761$.

Timeline

• Feb 2024 — arXiv v1; ICML 2024. Asymptotic theorem via Cramér; finite-sample statement conjectured; ~5·10⁹-configuration numerical sweep.
• Oct 2024 — arXiv v2.
• Apr 2026 — arXiv v3; conjecture still stated as open.
• Aug 2026 — private proof of the Section 3 inequality (strict win, $b\ge1/2$, one level) via exponential tilting of the tie probability.
• Sep 2026 — private proof of the fair-coin version with no constraint on $b$ (Bernstein degree elevation and a hypergeometric parity argument), then of the full four-part statement via a pairing lemma for player-symmetric rules. This mission formalizes that proof.

Conventions in the formal statement

"Greater than $1$" is read as $n\ge2$ and each $m_i\ge3$ odd; the list of set sizes in (b)–(d) is nonempty. Laws are functions $\mathbb Z\to\mathbb R$ and every probability is a finite sum — no measure theory. The goal theorem is the conjunction of the four parts.