Probability

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.

Motivation

Chapter 4 of Luenberger's Optimization by Vector Space Methods (Wiley, 1969) develops linear least-squares estimation as an application of the Hilbert space projection theorem formalized in Mission I of this series. The chapter's centerpiece is the classical Gauss–Markov theorem: among all linear unbiased estimators of an unknown parameter vector from noisy linear measurements, the estimator $(W^\top Q^{-1} W)^{-1} W^\top Q^{-1} y$ has minimum variance — componentwise, not merely in trace. This result is foundational for statistics and econometrics, and its Hilbert-space derivation is the cleanest known.

Setting

Measurements are modeled as $y = W\beta + \varepsilon$, where $y$ is an $m$-dimensional data vector, $W$ a known $m \times n$ matrix ($n < m$) with linearly independent columns, $\beta$ an unknown $n$-dimensional parameter vector, and $\varepsilon$ a random $m$-vector of measurement errors with $E\varepsilon = 0$ and covariance $E[\varepsilon\varepsilon^\top] = Q$, positive definite. A linear estimate is $\hat\beta = Ky$ for a constant $n \times m$ matrix $K$; it is unbiased when $E\hat\beta = \beta$ for every $\beta$, which holds iff $KW = I$. The optimality criterion is the error second moment $E\|\hat\beta - \beta\|^2$, and the book's key observation (p. 85) is that the problem splits into $n$ independent minimum norm problems, one per component, each solvable by the dual approximation theorem of Mission I.

Formally, randomness is carried by an abstract probability space: a measure space $(\Omega, \mu)$ with $\mu$ a probability measure, random vectors as functions $\Omega \to \mathbb{R}^m$ with explicit integrability hypotheses for all first and second moments, and $E[\cdot] = \int \cdot \, d\mu$.

Formalization targets

The goal is §4.4 Theorem 1 (Gauss–Markov): with $K_0 = (W^\top Q^{-1} W)^{-1} W^\top Q^{-1}$,

$$K_0 W = I, \qquad E\big[(K_0 y - \beta)_i^2\big] \le E\big[(K y - \beta)_i^2\big] \quad \text{for every } i \text{ and every } K \text{ with } KW = I,$$

with error covariance

$$E\big[(K_0 y - \beta)(K_0 y - \beta)^\top\big] = (W^\top Q^{-1} W)^{-1}.$$

Milestones: the deterministic least-squares estimate $\hat\beta = (W^\top W)^{-1} W^\top y$ (§4.3 Theorem 1); the book's deterministic reduction — minimize the diagonal entries of $KQK^\top$ subject to $KW = I$ (p. 85); the minimum-variance estimate $\hat\beta = E[\beta y^\top] (E[y y^\top])^{-1} y$ for random $\beta$ (§4.5 Theorem 1); and the information-form identities $RW^\top(WRW^\top + Q)^{-1} = (W^\top Q^{-1}W + R^{-1})^{-1}W^\top Q^{-1}$ and $R - RW^\top(WRW^\top+Q)^{-1}WR = (W^\top Q^{-1}W + R^{-1})^{-1}$ (§4.5 Corollary 2).

Significance

The Gauss–Markov theorem justifies weighted least squares as the optimal linear unbiased procedure and is the standard benchmark against which biased and nonlinear estimators are measured. The minimum-variance estimate of §4.5 is the Bayesian counterpart with prior covariance $R$; the information-form identities connect the two and exhibit Gauss–Markov as the limit $R^{-1} \to 0$. Mission III builds the recursive (Kalman) estimator directly on these results.

All results are classical and proved in the source. Mathlib has mature measure-theoretic integration but, to date, no Gauss–Markov theorem and no linear estimation theory; the matrix milestones (trace reduction, information form) are also absent as stated. The probabilistic statements here are deliberately phrased with elementary integrals of products of real-valued components — no Bochner integration of vector-valued maps — so they are approachable with MeasureTheory.integral alone.

Difficulty

The subtlety is bookkeeping, not depth. Unbiasedness must be encoded as the algebraic constraint $KW = I$ (the book proves the equivalence with $E\hat\beta = \beta$ for all $\beta$); the componentwise variance claim is strictly stronger than the trace claim and requires the per-component minimum norm argument, not a single matrix inequality. Positive definiteness of $Q$ enters through invertibility of $W^\top Q^{-1} W$, which itself needs the linear independence of the columns of $W$ — dropping either hypothesis makes the goal false. In the probabilistic statements every integral needs an integrability hypothesis; the drafts supply integrability of all pairwise products of components, from which integrability of every derived expression follows.

Formalization scope

Random vectors are plain functions Ω → Fin m → ℝ on a MeasurableSpace Ω with a probability measure μ; second moments are hypotheses of the form ∫ ω, ε ω i * ε ω j ∂μ = Q i j with explicit Integrable assumptions; no independence, Gaussianity, or distributional assumptions are used anywhere. Matrices are Matrix (Fin m) (Fin n) ℝ with Mathlib's Matrix.PosDef, nonconstructive inverse ⁻¹, and mulVec. Norms on parameter space are written as explicit finite sums of squares, avoiding any ambiguity between Euclidean and supremum norms on pi types. The estimators under comparison are strictly linear ($\hat\beta = Ky$, no affine offset), exactly as in the source; §4.5's affine extension (its Problem 6) is out of scope.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969. Chapter 4, pp. 78–102. ISBN 0-471-55359-X.
• A. C. Aitken, On least squares and linear combination of observations, Proc. Roy. Soc. Edinburgh 55 (1935), 42–48 (the weighted-least-squares form of Gauss–Markov).