Missions · Prove2Me

Control Theory Mathematical Physics Optimization+3·Captain: mikedeng1

Optimization of Mean-field Spin Glasses III: The Lagrangian Value of the Stochastic Control Problem Equals the Parisi FunctionalResearch Paper

Motivation

The ground-state energy of a mixed $p$ -spin spin glass, $\mathsf{OPT}_N=\max_{\sigma\in\{\pm1\}^N}H_N(\sigma)/N$ , converges almost surely to the infimum of the Parisi functional over non-decreasing order parameters (Auffinger–Chen 2017). El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) study algorithms that find near-optimal configurations. They introduce incremental approximate message passing (IAMP) and show that, among a broad class of such algorithms, the best achievable energy is the infimum of the Parisi functional over a larger space of order parameters (their Theorem 4).

The upper bound in Theorem 4 is reduced, in Section 4 of the paper, to a stochastic optimal control problem. The energy reached by a message-passing algorithm becomes the objective of a control problem driven by a Brownian motion, with a terminal constraint and a variance constraint. The variance constraint is removed by a Lagrange multiplier $\tfrac12\xi''\gamma$ . Proposition 4.1 states that the resulting Lagrangian value is exactly the Parisi functional $\mathsf P(\gamma)$ . This mission formalizes that duality and the verification argument behind it (Section 7).

Setting

Mixture. Real coefficients $(c_k)_{k\ge2}$ define the mixture $\xi(t)=\sum_{k\ge2}c_k^2t^k$ , with the standing assumption $\xi(1+\varepsilon)<\infty$ for some $\varepsilon>0$ . Its derivatives $\xi'$ , $\xi''$ are nonnegative and nondecreasing on $[0,1]$ .

Order parameters. $\mathsf{SF}_+$ is the set of nonnegative step functions

\gamma=\sum_{i=1}^m\gamma_i\,\mathbb I_{[t_{i-1},t_i)},\qquad 0=t_0<t_1<\dots<t_m=1,\ \gamma_i\ge0 .

Put $\nu(t)=\int_t^1\xi''(s)\gamma(s)\,ds$ .

Parisi PDE and functional. $\Phi_\gamma:[0,1]\times\mathbb R\to\mathbb R$ solves

\partial_t\Phi_\gamma+\tfrac12\xi''(t)\big(\partial_x^2\Phi_\gamma+\gamma(t)(\partial_x\Phi_\gamma)^2\big)=0,\qquad\Phi_\gamma(1,x)=|x| .

For $\gamma\in\mathsf{SF}_+$ it is given explicitly by the Cole–Hopf recursion: with $r(t)=\xi'(1)-\xi'(t)$ and $G\sim\mathsf N(0,1)$ , for $t\in[t_{i-1},t_i)$ ,

\Phi_\gamma(t,x)=\frac1{\gamma_i}\log\mathbb E\exp\big\{\gamma_i\Phi_\gamma(t_i,x+\sqrt{r(t)-r(t_i)}\,G)\big\}.

The Parisi functional is $\mathsf P(\gamma)=\Phi_\gamma(0,0)-\tfrac12\int_0^1t\,\xi''(t)\gamma(t)\,dt$ .

Control problem. Let $B$ be a standard Brownian motion. A control $u\in D[t,1]$ is a process on $[t,1]$ , progressively measurable for the filtration of $(B_r)_{r\in[t,1]}$ , with $\mathbb E\int_t^1\xi''(s)u_s^2\,ds<\infty$ . The value is

\mathcal J_\gamma(t,z)=\sup_{u\in D[t,1]}\mathbb E\Big[\int_t^1\xi''(s)u_s\,ds+\frac12\int_t^1\nu(s)\big(\xi''(s)u_s^2-1\big)ds\Big]\quad\text{s.t.}\quad z+\int_t^1\sqrt{\xi''(s)}\,u_s\,dB_s\in(-1,1)\ \text{a.s.}

Candidate value function. With $\Phi^*_\gamma(t,z)=\inf_x\{\Phi_\gamma(t,x)-xz\}$ ,

V(t,z)=\Phi^*_\gamma(t,z)-\tfrac12\nu(t)z^2-\tfrac12\int_t^1\nu(s)\,ds .

Formalization targets

Goal: Proposition 4.1

\mathcal J_\gamma(0,0)=\mathsf P(\gamma)\qquad\text{for every }\gamma\in\mathsf{SF}_+ .

Milestones

Lemma 7.2 (a)–(e): $\Phi_\gamma(t,\cdot)$ is smooth for $t<1$ , with derivatives jointly continuous on $[0,1)\times\mathbb R$ and $C^1$ in time where $\gamma$ is constant. The range of $\partial_x\Phi_\gamma(t,\cdot)$ is $(-1,1)$ , it is strictly increasing, and $0<\partial_x^2\Phi_\gamma(t',x)\le C(t,\gamma)$ for $t'\le t$ .
Envelope identities (proof of Lemma 7.3): $\partial_z\Phi^*_\gamma(t,z)=-x^*_t(z)$ and $\partial_z^2\Phi^*_\gamma(t,z)=-1/\partial_x^2\Phi_\gamma(t,x^*_t(z))$ , where $x^*_t(z)$ is the unique root of $\partial_x\Phi_\gamma(t,x)=z$ .
Lemma 7.3: $V$ solves the HJB equation

\partial_tV+\xi''(t)\sup_{\lambda\in\mathbb R}\Big\{\lambda+\frac{\lambda^2}{2}\big(\nu(t)+\partial_z^2V\big)\Big\}-\frac12\nu(t)=0,\qquad V(1,z)=0 .

Evaluation at the origin: $V(0,0)=\mathsf P(\gamma)$ .
Proposition 7.1: $\mathcal J_\gamma(t,z)=V(t,z)$ for all $(t,z)\in[0,1]\times(-1,1)$ .

Proposition 7.1 at $(0,0)$ together with milestone 4 gives the goal.

Significance

The result. By integration by parts (Eq. (4.4) of the paper), $\mathcal J_\gamma(0,0)$ bounds the value of the constrained control problem (4.2). That problem in turn bounds the asymptotic energy of every message-passing algorithm in the class of Theorem 4. Proposition 4.1 turns the bound into $\inf_{\gamma\in\mathsf{SF}_+}\mathsf P(\gamma)$ , which is the analytic core of the optimality statement for IAMP. It is also an instance of a broader principle: the Parisi functional has a stochastic-control representation (Jagannath–Tobasco 2016).

Formalizing it. The result is proved in the paper; no machine-checked version exists. A complete formalization needs a verification theorem for a control problem with a state constraint ( $M_1\in(-1,1)$ ), Itô's formula for a $C^{1,2}$ function that is only piecewise $C^1$ in time, and quantitative regularity of the Cole–Hopf solution. Each of these is reusable well beyond spin glasses.

Difficulty

The value function $\mathcal J_\gamma$ is not known to be smooth, and the dynamic-programming equation (4.6) is only heuristic. The proof therefore guesses a solution and verifies it. Two steps carry the difficulty.

First, the guess $V$ is a Legendre transform. Its regularity, and the sign $\nu+\partial_z^2V<0$ that makes the HJB supremum finite, rest on strict convexity and bounded curvature of $\Phi_\gamma(t,\cdot)$ (Lemma 7.2). These must be proved by induction through the Cole–Hopf recursion, including the steps with $\gamma_i=0$ .

Second, the verification argument applies Itô's formula to $V(s,M^u_s)$ , where $M^u$ is a martingale confined to $(-1,1)$ and $V$ is only $C^1$ in time between the jumps of $\gamma$ . The boundary $\theta\to1$ needs a dominated-convergence argument, and attaining the supremum needs an explicit optimal feedback control built from an SDE.

Formalization scope

Mixture. $\xi$ is a coefficient sequence $c:\mathbb N\to\mathbb R$ with $c_0=c_1=0$ imposed. $\xi'$ and $\xi''$ are explicit termwise series.
Step functions. $\mathsf{SF}_+$ is represented by its data (breakpoints and values). $\gamma$ is extended by $0$ outside $[0,1)$ ; its value at $t=1$ never matters.
Cole–Hopf. $\Phi_\gamma$ is defined by the recursion. When $\gamma_i=0$ , the recursion uses its limit, the heat semigroup, instead of dividing by zero. Expectations over $G$ are integrals against gaussianReal 0 1.
Derivatives. Space derivatives are deriv/iteratedDeriv. Time derivatives are right derivatives, because $\gamma$ jumps.
Legendre transform. $\Phi^*_\gamma$ is a real infimum, used only for $|z|<1$ , where it is bounded below.
Brownian motion and filtration. $B$ is a Mathlib IsBrownianReal process on $\mathbb R_{\ge0}$ , with each $B_r$ measurable. The filtration is $\mathcal F^t_s=\sigma(B_r:t\le r\le s)$ .
Stochastic integral. It is the $L^2$ Itô integral of the published definition Peng1990.SMP.IsItoIntegral (horizon $1$ ), whose integrability class is exactly $\mathbb E\int\xi''u^2<\infty$ .
Supremum. $\mathcal J_\gamma(t,z)=v$ is stated as " $v$ is the least upper bound of the objective values of admissible controls" (IsLUB), never as a real sSup. A default value of an empty or unbounded supremum therefore cannot make a statement trivially true.
Disclosed hypothesis. Lemma 7.2, the envelope identities and Lemma 7.3 assume that $\xi$ is not identically zero (some $c_k\neq0$ ). For $\xi\equiv0$ one has $\Phi_\gamma(t,x)=|x|$ for all $t$ , and these statements fail. Proposition 7.1, the evaluation at the origin and the goal need no such hypothesis.
Lemma 7.3. The statement includes the inequality $\nu+\partial_z^2V<0$ , which the page proves. This rules out reading the HJB supremum as a default value.

The paper's algorithmic results (Theorems 2–4, Corollary 2.2) are out of scope. They need the AMP and state-evolution machinery of Section 5 and Appendix A, and an informal model of computation. The optional bound (4.4) is not stated.

Welcome contributions include the regularity of Cole–Hopf solutions (Gaussian convolution, log-moment-generating functions), a general verification theorem for one-dimensional controlled martingales with a terminal state constraint, and Itô's formula for $C^{1,2}$ functions.

Selected references

A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904
A. Auffinger, W.-K. Chen, Parisi formula for the ground state energy in the mixed p-spin model, Ann. Probab. 45(6b), 2017. https://arxiv.org/abs/1606.05335
A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proc. AMS 144, 2016. https://arxiv.org/abs/1502.04398
N. Touzi, Optimal Stochastic Control, Stochastic Target Problems, and Backward SDE, Fields Institute Monographs 29, Springer, 2012 (cited as [Tou12] in the paper; the verification argument of Section 7 follows its Theorem 4.1).

14 thms1 active userReviewed

Mathematical Physics Optimization Partial Differential Equations+1·Captain: mikedeng1

Optimization of Mean-field Spin Glasses II: Under No Overlap Gap, the Monotone Parisi Minimizer Also Minimizes the Extended FunctionalResearch Paper

Motivation

The mixed $p$ -spin model is a random polynomial on the hypercube $\{-1,+1\}^N$ : a centered Gaussian process $H_N(\boldsymbol\sigma)$ with covariance $\mathbb E\{H_N(\boldsymbol\sigma)H_N(\boldsymbol\sigma')\} = N\xi(\langle\boldsymbol\sigma,\boldsymbol\sigma'\rangle/N)$ . Its maximum $\mathrm{OPT}_N = \max_{\boldsymbol\sigma} H_N(\boldsymbol\sigma)/N$ is a canonical random optimization problem; for $\xi(t) = c_2^2t^2$ it is the ground state of the Sherrington–Kirkpatrick model. Auffinger and Chen (AC17) proved that $\mathrm{OPT}_N$ converges almost surely to the infimum of the zero-temperature Parisi functional $\mathsf P$ over a space $\mathscr U$ of non-decreasing order parameters.

El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) characterize what a class of message-passing algorithms achieves on this problem. The answer is the infimum of the same functional over a larger space $\mathscr L$ of order parameters that need not be monotone. Whether these algorithms reach the true optimum is therefore the question whether $\inf_{\mathscr U}\mathsf P = \inf_{\mathscr L}\mathsf P$ . The paper proves this equality under the no-overlap gap assumption, that the Parisi minimizer over $\mathscr U$ can be taken strictly increasing (Assumption 2, p. 8). This is believed to hold for the Sherrington–Kirkpatrick model and to fail for pure $p$ -spin models with $p \ge 3$ . This mission formalizes that equality, stated as a property of the minimizer.

Timeline. Parisi's formula (1979) was proved by Talagrand (2006) and Panchenko (2013). Auffinger and Chen (2017) gave its zero-temperature form (1.7). Jagannath and Tobasco (JT16) gave a PDE and variational treatment of the Parisi functional at positive temperature, including its convexity. Montanari (Mon19) gave a message-passing algorithm for the Sherrington–Kirkpatrick model under no overlap gap. El Alaoui, Montanari and Sellke (2020) extended it to mixed $p$ -spin models and introduced the extended principle over $\mathscr L$ .

Setting

A mixture is $\xi(t) = \sum_{k\ge2} c_k^2 t^k$ with $\xi(1+\varepsilon) < \infty$ for some $\varepsilon > 0$ , with derivatives $\xi'$ and $\xi''$ given by the termwise series. Order parameters are functions $\gamma : [0,1) \to \mathbb R_{\ge0}$ , in one of two spaces:

\mathscr U = \Big\{\gamma \text{ non-decreasing},\ \int_0^1\gamma(t)\,dt < \infty\Big\},\qquad \mathscr L = \Big\{\|\xi''\gamma\|_{TV[0,t]} < \infty\ \forall t<1,\ \int_0^1\xi''(t)\gamma(t)\,dt < \infty\Big\}.

Here $\|\cdot\|_{TV[0,t]}$ is total variation on $[0,t]$ , and $\mathscr U \subseteq \mathscr L$ .

For a step function $\gamma = \sum_i \gamma_i \mathbb I_{[t_{i-1},t_i)}$ with $\gamma_i \ge 0$ (the space $\mathrm{SF}_+$ ), the Parisi PDE

\partial_t\Phi + \tfrac12\xi''(t)\big(\partial_x^2\Phi + \gamma(t)(\partial_x\Phi)^2\big) = 0,\qquad \Phi(1,x) = |x|,

is solved explicitly by the Cole–Hopf recursion (7.3). It is a Gaussian log-moment-generating step on each piece, and a heat-semigroup step where $\gamma_i = 0$ . For general $\gamma \in \mathscr L$ , $\Phi^\gamma$ is the limit of $\Phi^{\gamma_n}$ along step functions $\gamma_n \to \gamma$ in the weighted norm $\int_0^1\xi''|\gamma_n - \gamma|$ . The Parisi functional is

\mathsf P(\gamma) = \Phi^\gamma(0,0) - \frac12\int_0^1 t\,\xi''(t)\gamma(t)\,dt .

The process $X$ is the strong solution of $dX_t = \xi''(t)\gamma(t)\partial_x\Phi^\gamma(t,X_t)\,dt + \sqrt{\xi''(t)}\,dB_t$ , $X_0 = 0$ (Eq. (6.3)), driven by a standard Brownian motion $B$ .

Formalization targets

Goal: the monotone minimizer is a minimizer over $\mathscr L$ (Section 6.3, p. 34)

If $\gamma_* \in \mathscr U$ is strictly increasing on $[0,1)$ and $\mathsf P(\gamma_*) \le \mathsf P(\gamma)$ for every $\gamma \in \mathscr U$ , then

\mathsf P(\gamma_*) \le \mathsf P(\gamma)\qquad\text{for every }\gamma \in \mathscr L .

Since $\mathscr U \subseteq \mathscr L$ , this is the paper's main result 2 (p. 4), $\inf_{\mathscr U}\mathsf P = \inf_{\mathscr L}\mathsf P$ under no overlap gap.

Milestones

Lemma 6.7 (p. 27): for $\gamma\in\mathscr L$ , $t\mapsto\mathbb E\{\partial_x^2\Phi(t,X_t)^2\}$ is continuous on $[0,1)$ .
Proposition 6.8 (p. 27): the right derivative of $s\mapsto\mathsf P(\gamma+s\delta)$ at $0$ is $\frac12\int_0^1\xi''(t)\delta(t)\big(\mathbb E\{\partial_x\Phi(t,X_t)^2\}-t\big)\,dt$ , for admissible directions $\delta$ that vanish near $t = 1$ .
Lemma 6.15 (p. 33): under no overlap gap, $\mathbb E\{\partial_x\Phi^{\gamma_*}(t,X_t)^2\} = t$ for every $t\in[0,1)$ .
Convexity (Section 6.3, p. 34): $\mathsf P$ is convex on $\mathscr L$ .

Significance

The result. The goal identifies the value reached by the paper's message-passing algorithm with the ground-state energy whenever the Parisi minimizer is strictly increasing. Combined with the paper's algorithmic theorem, it yields a $(1-\varepsilon)$ -approximation of $\mathrm{OPT}_N$ in time linear in the input size, for the Sherrington–Kirkpatrick model and any other mixture with no overlap gap (Corollary 2.2). It also gives a structural fact about the variational problem: when the minimizer is strictly increasing, the monotonicity constraint in $\mathscr U$ is not binding.

Formalizing it. The result is proved in the paper, but the proof leans on an external citation ([JT16, Theorem 20]) for convexity of $\mathsf P$ on $\mathscr L$ . It also applies the first-variation formula in a direction that does not meet that formula's stated hypotheses. A machine-checked development closes both gaps. No part of this theory (the Parisi PDE, its Cole–Hopf solution, or the extended functional) has been formalized before, to our knowledge.

Difficulty

The obvious argument is: convexity plus stationarity gives a global minimum. Both inputs are hard. Stationarity (Lemma 6.15) needs the first variation of $\mathsf P$ in directions that keep $\gamma_*+s\delta$ monotone. That variation is a derivative of the solution of a nonlinear PDE with respect to its coefficient, expressed through an SDE driven by that solution's own gradient. Convexity of $\mathsf P$ on $\mathscr L$ is not visible from the formula: $\Phi^\gamma(0,0)$ is defined through a limit of nested Cole–Hopf recursions, and the paper does not prove it, citing a positive-temperature argument instead. Finally, the goal needs the first variation in the direction $\gamma - \gamma_*$ , which is generally non-zero near $t = 1$ , where $\xi''\gamma$ may blow up. Proposition 6.8 as stated excludes such directions.

Formalization scope

Mixture. A coefficient sequence c : ℕ → ℝ with $c_0 = c_1 = 0$ and $\sum_k c_k^2(1+\varepsilon)^k < \infty$ for some $\varepsilon>0$ . $\xi'$ and $\xi''$ are explicit power series.
Order parameters. Functions $\mathbb R\to\mathbb R$ ; membership in $\mathscr U$ and $\mathscr L$ reads only $[0,1)$ . Total variation is eVariationOn; finiteness of integrals is IntegrableOn (which includes measurability).
Cole–Hopf. Step-function data $(m,t,a)$ with $m\ge1$ . The $\gamma_i = 0$ pieces use the heat semigroup, the limit of (7.3). The terminal condition is $|x|$ . Gaussian expectations are integrals against gaussianReal 0 1.
$\Phi^\gamma$ on $\mathscr L$ . limUnder of the Cole–Hopf values along step-function data converging to $\gamma$ in the weighted $L^1$ distance. $\partial_x$ is deriv in $x$ .
SDE. The published definition EthierKurtz.SolvesBrownianSDE in dimension one, with coefficients extended by $0$ after time $1$ . Brownian motion is Mathlib's IsBrownianReal, and expectations are Bochner integrals.
Minimality. Always attainment, $\mathsf P(\gamma_*)\le\mathsf P(\gamma)$ for all $\gamma$ in the space, never a real infimum (which Lean sets to $0$ on unbounded sets).
Disclosed hypothesis. Lemma 6.15 assumes that some $c_k \ne 0$ . For $\xi\equiv0$ it is false: $\mathsf P\equiv0$ , $X\equiv0$ , and the left side is constant in $t$ . The goal does not need it.
Ruled out. A formalization that defines $\Phi^\gamma$ as an arbitrary weak solution of the PDE, or via a choice from an unproved existence statement, would make $\mathsf P$ unconstrained. It is not acceptable. Encoding the hypothesis on $\gamma_*$ as minimality over $\mathscr L$ would make the goal trivial.
Proof gaps in the source. Convexity of $\mathsf P$ on $\mathscr L$ is cited, not proved. The step from stationarity to the goal applies Proposition 6.8 outside its stated hypotheses. The statements are the paper's and are believed true.
Out of scope. The paper's algorithmic results (Theorems 2–4, Corollary 2.2) assert algorithms with complexity bounds in an informal computation model, and rest on a long state-evolution analysis. They are not part of this mission.

Contributions welcome: Cole–Hopf regularity (smoothness and the bound $|\partial_x\Phi|\le1$ ), the Lipschitz estimate in $\gamma$ that makes $\Phi^\gamma$ well defined, well-posedness of the SDE, and Itô calculus for the first variation. The Cole–Hopf layer and the SDE well-posedness are reusable for the companion missions on the full-support theorem and the stochastic-control duality of the same paper.

Selected references

A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904v1
A. Auffinger, W.-K. Chen, Parisi formula for the ground state energy in the mixed p-spin model, Ann. Probab. 45(6b), 2017. https://arxiv.org/abs/1606.05335
A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proc. AMS 144(7), 2016. https://arxiv.org/abs/1502.04398
A. Montanari, Optimization of the Sherrington–Kirkpatrick Hamiltonian, FOCS 2019. https://arxiv.org/abs/1812.10897
M. Talagrand, The Parisi formula, Ann. Math. 163(1), 2006. https://doi.org/10.4007/annals.2006.163.221
D. Panchenko, The Parisi ultrametricity conjecture, Ann. Math. 177(1), 2013. https://arxiv.org/abs/1112.1003

11 thms1 active userReviewed

Probability Stochastic Systems·Captain: mikedeng1

Convergence in law of the minimum of a branching random walk: The Minimum Centred at (3/2) ln n Converges to a Gumbel Law Shifted by the Derivative MartingaleResearch Paper

Motivation

A branching random walk is the simplest model of a population that both reproduces and moves: every particle dies and leaves a random cloud of children displaced relative to it. Its extreme particles control the speed of travelling waves in reaction–diffusion equations (the KPP/Fisher equation), the free energy of directed polymers on trees, the cover and hitting times of random walks on trees, and the maxima of log-correlated fields such as the two-dimensional Gaussian free field. The basic quantity is the position of the leftmost particle at time $n$ .

Timeline.

1974–1976: Hammersley, Kingman and Biggins prove the law of large numbers $M_n/n\to\gamma$ for the minimum.
1978–1983: Bramson shows that for branching Brownian motion the maximum, centred at $\sqrt2\,t-\frac{3}{2\sqrt2}\ln t$ , converges in law (Bramson 1983). Lalley and Sellke (1987, Ann. Probab. 15) identify the limit as a Gumbel law randomly shifted by the limit of the derivative martingale.
2004: Biggins and Kyprianou prove that the derivative martingale of a branching random walk converges to a limit that is non-trivial in the boundary case (Adv. Appl. Probab. 36).
2009: Hu and Shi (arXiv:math/0702799) and Addario-Berry and Reed (Ann. Probab. 37) find the logarithmic correction: $M_n-\frac32\ln n$ is tight. Bramson and Zeitouni (2009) obtain tightness around the median under tail assumptions.
2013: Aïdékon proves convergence in law of $M_n-\frac32\ln n$ for general non-lattice branching random walks, the result this mission formalizes (arXiv:1101.1810, Ann. Probab. 41 (2013)).

Setting

Let $\mathcal L$ be a point process on $\mathbb R$ : a random, possibly infinite, collection of points. Start one particle at $0$ . At time $1$ it dies and leaves children at the points of $\mathcal L$ ; each particle of generation $n$ then dies and leaves children at the points of an independent copy of $\mathcal L$ , translated to its own position. Vertices of the genealogical tree $\mathbb T$ (a Galton–Watson tree) are labelled by finite words $u=(i_0,\dots,i_{k-1})$ ; $|u|=k$ is the generation, $u_j$ the ancestor at generation $j$ , and $V(u)$ the position.

The paper works in the boundary case

\mathbf E\Big[\sum_{|x|=1}1\Big]>1,\qquad \mathbf E\Big[\sum_{|x|=1}e^{-V(x)}\Big]=1,\qquad \mathbf E\Big[\sum_{|x|=1}V(x)e^{-V(x)}\Big]=0,\tag{1.1}

and assumes throughout that $\mathcal L$ is non-lattice and that

\mathbf E\Big[\sum_{|x|=1}V(x)^2e^{-V(x)}\Big]<\infty,\qquad \mathbf E\big[X(\ln_+X)^2\big]<\infty,\qquad \mathbf E\big[\tilde X\ln_+\tilde X\big]<\infty,\tag{1.3–1.4}

with $X=\sum_{|x|=1}e^{-V(x)}$ and $\tilde X=\sum_{|x|=1}V(x)_+e^{-V(x)}$ . The objects of the main theorem are the minimum $M_n=\min\{V(x):|x|=n\}$ (with $\min\varnothing=+\infty$ ) and the derivative martingale

D_n=\sum_{|x|=n}V(x)e^{-V(x)},

which converges almost surely to a limit $D_\infty\ge0$ , strictly positive on non-extinction. A standard example: two children with i.i.d. normal displacements of mean and variance $2\ln2$ .

Formalization targets

Goal: Theorem 1.1

There is a constant $C^*\in(0,\infty)$ such that for every real $x$ ,

\lim_{n\to\infty}\mathbf P\Big(M_n\ge\tfrac32\ln n+x\Big)=\mathbf E\Big[e^{-C^*e^xD_\infty}\Big].

The constant is not specified numerically. It is the product $C_1c_0$ of the constants below.

Milestones, in the order the proof uses them

Many-to-one lemma (2.1): $\mathbf E_a[\sum_{|x|=n}g(V(x_1),\dots,V(x_n))]=\mathbf E_a[e^{S_n-a}g(S_1,\dots,S_n)]$ for a centred random walk $S$ .
Renewal function (2.13): the renewal function $R$ of the strict descending ladder heights of $S$ satisfies $R(x)/x\to c_0>0$ .
Corollary 3.2 and Proposition 1.2: for the walk killed below $0$ , $e^z\,\mathbf P(M_n^{\rm kill}<\frac32\ln n-z)\to C_1$ , uniformly for $z\in[A,\frac32\ln n-A]$ .
Global minimum bound: $\mathbf P(\exists u\in\mathbb T: V(u)\le-y)\le e^{-y}$ .
Corollary 3.5: $\mathbf P(M_n\le\frac32\ln n-y)\le(1+c_{10}(1+y))e^{-y}$ .
Proposition 4.1: $\frac{e^z}{z}\mathbf P(M_n<\frac32\ln n-z)\to C_1c_0$ , uniformly on the same window.
Derivative martingale: $D_n\to D_\infty$ a.s., $D_\infty\ge0$ , $D_\infty>0$ a.s. on non-extinction.
(5.2): $\sum_{u\in\mathcal Z[A]}V(u)e^{-V(u)}\to D_\infty$ a.s. as $A\to\infty$ , where $\mathcal Z[A]$ is the set of particles absorbed at level $A$ .

Significance

The theorem identifies the limit law of the extreme particle: $M_n-\frac32\ln n$ converges in law, on the event of survival, to a Gumbel variable shifted by $-\ln(C^*D_\infty)$ . It is the input for the study of the whole extremal process of the branching random walk seen from its leftmost particle (Madaule, J. Theoret. Probab., 2017), and it is the discrete-time counterpart of the Bramson and Lalley–Sellke results that later work on log-correlated fields takes as its template. The $\frac32$ correction and the role of the derivative martingale are the signature of the boundary case, and of log-correlated extremes generally.

The result is proved and published. It has not been formalized: Mathlib has no branching processes, no Galton–Watson trees with positions, no renewal theory, and no derivative martingale. This mission produces the first machine-checkable statement of the convergence-in-law theorem and of the intermediate results it rests on. A complete development would also give reusable formal versions of the many-to-one lemma and of renewal theory for ladder heights.

Difficulty

The first-moment computation through the many-to-one lemma gives the wrong centring. It predicts that the minimum sits near $\frac12\ln n$ , because the expected number of particles below a level is dominated by rare realisations. The true centring $\frac32\ln n$ only appears after restricting to particles whose ancestral path stays above a barrier, and this restriction requires random-walk estimates (ballot theorems and local limit theorems for walks conditioned to stay positive) that hold uniformly in a window of starting points. A second difficulty is that the limit must be identified, not only shown to exist. Tightness and subsequence arguments do not give the factor $D_\infty$ ; the identification needs the precise tail $C_1c_0\,z\,e^{-z}$ of Proposition 4.1, with a known constant, and the almost-sure behaviour of the sum over the stopping line $\mathcal Z[A]$ .

Formalization scope

Point process. The law $L$ of $\mathcal L$ is a probability measure on configurations $(N,p)\in\mathbb N_\infty\times(\mathbb N\to\mathbb R)$ , where the points are $p_i$ for $i<N$ .
Tree. Labels are List ℕ. The branching random walk is any family $(\xi_u)_{u}$ of independent measurable configurations of law $L$ on a probability space. Every theorem holds for every such realisation, and a canonical realisation exists (product space).
Assumptions. Every expectation in (1.1), (1.3), (1.4) is a lower Lebesgue integral of a $[0,\infty]$ -valued sum. The signed condition in (1.1) is "the expectations of $\sum V_+e^{-V}$ and $\sum V_-e^{-V}$ are equal and finite". Non-lattice means: there are no $a\in\mathbb R$ and $d>0$ with all points a.s. in $a+d\mathbb Z$ .
Which assumptions where. The goal and §§3–5 assume all of them. The many-to-one lemma and the global minimum bound assume only (1.1), and the derivative-martingale milestone drops non-lattice, as in Appendix A.
Minima and limits. $M_n$ and $M_n^{\rm kill}$ are extended reals, $+\infty$ on an empty generation, so extinction lies in $\{M_n\ge\frac32\ln n+x\}$ . $D_n$ is a real sum over generation $n$ , absolutely summable almost surely, and $D_\infty$ is its pointwise limit. The expectation in the goal is a lower integral of $e^{-C^*e^xD_\infty}\in(0,1]$ .
Constants. $C^*$ is chosen before $x$ . In Proposition 4.1, $C_1$ and $c_0$ are hypotheses tied to Proposition 1.2 and (2.13), not re-chosen. Corollaries 3.2 and 3.5 assert existence of their constants without Proposition 3.1 and Corollary 3.4.
Not trivial. A formalization with a real-valued $M_n$ equal to $0$ on extinction, a $D_\infty$ never shown to be the limit, or a $C^*$ depending on $x$ would not be this theorem. The definitions above rule out each of these.

Out of scope: the spine-measure lemmas (Lemmas 2.3, 3.3, 3.8–3.10, 4.3), Propositions 2.1–2.2 cited from Lyons, and Appendices B–C. Contributions are welcome on all milestones. The many-to-one lemma and the renewal statement are independent of the rest and are natural first targets.

Selected references

E. Aïdékon, Convergence in law of the minimum of a branching random walk, Ann. Probab. 41(3A) (2013) 1362–1426. arXiv:1101.1810, doi:10.1214/12-AOP750
J. D. Biggins, A. E. Kyprianou, Measure change in multitype branching, Adv. Appl. Probab. 36 (2004) 544–581. Reference [7] of Aïdékon (2013), arXiv:1101.1810, p. 68
M. Bramson, Convergence of solutions of the Kolmogorov equation to travelling waves, Mem. Amer. Math. Soc. 44, no. 285 (1983). doi:10.1090/memo/0285
S. P. Lalley, T. Sellke, A conditional limit theorem for the frontier of a branching Brownian motion, Ann. Probab. 15 (1987) 1052–1061. Reference [21] of Aïdékon (2013), arXiv:1101.1810, p. 69
Y. Hu, Z. Shi, Minimal position and critical martingale convergence in branching random walks, and directed polymers on disordered trees, Ann. Probab. 37 (2009) 742–789. arXiv:math/0702799
L. Addario-Berry, B. Reed, Minima in branching random walks, Ann. Probab. 37 (2009) 1044–1079. Reference [1] of Aïdékon (2013), arXiv:1101.1810, p. 68
R. Lyons, A simple path to Biggins' martingale convergence for branching random walk, in Classical and Modern Branching Processes, IMA Vol. Math. Appl. 84 (1997) 217–221. Reference [22] of Aïdékon (2013), arXiv:1101.1810, p. 69

13 thms1 active userReviewed

Completed

Combinatorics·Captain: mysticflounder

Six-colour Schur colourings of [1, 1801] under R₄(3) ≤ 61: balanced classes, nested saturation and forced reflectionResearch Paper

Motivation

The Schur number $S(n)$ is the largest $N$ such that $[1, N] = \{1, \dots, N\}$ can be partitioned into $n$ sumfree sets, sets with no $x, y, z$ such that $x + y = z$ ( $x = y$ allowed). Schur's argument gives $S(n) \le R_n(3) - 2$ , where the triangle Ramsey number $R_n(3)$ is the least $N$ such that every colouring of the edges of $K_N$ with $n$ colours has a monochromatic triangle (Fredricksen–Sweet 2000, inequality (2)). Only $S(1), \dots, S(5) = 1, 4, 13, 44, 160$ are known (Heule 2018). For six colours the published range is $536 \le S(6) \le 1836$ ; the upper bound is $R_6(3) - 2$ with $R_6(3) \le 1838$ (DS1, rev. 18).

Timeline.

1955: Greenwood and Gleason prove $R_3(3) = 17$ and $R_{n+1}(3) \le (n+1)(R_n(3) - 1) + 2$ (Theorem 6) (doi).
1961: Baumert finds $S(4) = 44$ by computer, as reported by Fredricksen and Sweet; they and Heule cite Golomb–Baumert 1965 for it.
1973: Chung proves $R_4(3) \ge 51$ (doi).
1997: Wan bounds $R_n(3)$ and, for even $n \ge 6$ , states $S_n < n!\,(e - e^{-1} + 3)/2 - n + 2$ (zbMATH 0882.05095 summary; doi). If his $S_n$ is the least $N$ that forces a monochromatic solution, this is the centred bound below, applied to his own bound on $R_{n-1}(3)$ ; if it is the largest $N$ , it is $1$ above it. His proof was not read.
2000: Fredricksen and Sweet prove $S(6) \ge 536$ (doi).
2004: Fettes, Kramer and Radziszowski prove $R_4(3) \le 62$ (listed in DS1, which also lists $R_5(3) \le 307$ ).
2018: Heule proves $S(5) = 160$ with a certified SAT computation (AAAI-18; preprint arXiv:1711.08076).
2026: a public repository of M. Tatarevic gives a computer-assisted argument for $R_4(3) \le 61$ . Its Lean development assumes that a family of 56,830 SAT instances is unsatisfiable, and the repository records solver results for them. The project of this mission's author produced LRAT certificates for all 56,830 instances and checked them; the report is in the repository's issue tracker. This mission does not depend on it.

The first target is a centred-interval bound: if $R_k(3) \le r$ , then $S(k+1) \le 2(k+1)\lfloor (r-1)/2 \rfloor + 1$ . With $R_4(3) \le 61$ the recursive bound gives $R_5(3) \le 302$ , and the centred bound gives $S(6) \le 1801$ ; with $R_5(3) \le 307$ it gives only $1837$ . The mission formalizes what a Schur colouring of $[1, 1801]$ with six colours would have to look like under $R_4(3) \le 61$ .

Setting

All numbers are natural numbers, $\mathbb{N} = \{0, 1, 2, \dots\}$ , and $[a, b] = \{a, \dots, b\}$ .

Schur colourings and covers. A colouring with $n$ colours is a map $c : \mathbb{N} \to \mathrm{Fin}\,n$ . It is a Schur colouring of $[1, N]$ (SchurColoring N c) if there are no $x, y \ge 1$ with $x + y \le N$ and $c(x) = c(y) = c(x + y)$ , the case $x = y$ included. The cover form uses SumFree S and CoveredBySumFree X n ( $X$ lies in the union of $n$ sumfree sets); for $n \ge 1$ the two bridge theorems pass between the two forms in both directions.

Triangle Ramsey property. $\mathrm{TR}(k, r)$ (TriangleRamsey k r): every colouring with at most $k$ colours of the pairs $x < y$ of a finite set of at least $r$ naturals has a monochromatic triangle. For $k \ge 1$ it is the inequality $R_k(3) \le r$ .

Neighbourhoods. The difference colouring gives a pair $\{x, y\}$ the colour $c(|x - y|)$ . For a Schur colouring of $[1, N]$ it has no monochromatic triangle on $[0, N]$ , since $(y - x) + (z - y) = z - x$ . Write

$\Gamma_i(V, v) = \{\, w \in V : w \ne v,\ c(|v - w|) = i \,\}$ (colorNbhd c V v i);
$V_m = \Gamma_{c(m+1)}([0, 2m+1], m)$ , the central neighbourhood (centralNbhd c m), which contains $2m + 1$ ;
$P_i = \Gamma_i(V_m, 2m+1)$ , the endpoint neighbourhoods (endpointNbhd c m i).

The frontier. The frontier hypotheses are $\mathrm{TR}(k, u + 1)$ , $2t = (k+1)u$ , $m = (k+2)t$ , and $c$ a Schur colouring of $[1, 2m + 1]$ with $k + 2$ colours. From the first two, $\mathrm{TR}(k + 1, 2t + 2)$ holds, and the centred bound excludes Schur colourings of $[1, 2m + 2]$ with $k + 2$ colours; $[1, 2m + 1]$ is the frontier interval. Six colours: $k = 4$ , $u = 60$ , $t = 150$ , $m = 900$ , $2m + 1 = 1801$ .

Example. For $k = 1$ , $u = 2$ , $t = 2$ , $m = 6$ (and $13 = S(3)$ ), the classes $\{1, 4, 7, 10, 13\}$ , $\{2, 3, 11, 12\}$ , $\{5, 6, 8, 9\}$ form a Schur colouring of $[1, 13]$ , with $V_6 = \{2, 5, 7, 10, 13\}$ and endpoint neighbourhoods $\{2, 10\}$ and $\{5, 7\}$ , both closed under $x \mapsto 12 - x$ .

Formalization targets

Goal: six colours under $R_4(3) \le 61$

\mathrm{TR}(4, 61) \ \text{ and } \ c \text{ a Schur colouring of } [1, 1801] \text{ with six colours} \implies (1)\text{–}(5),

where $q = c(901)$ , $V = V_{900}$ and $P_i = \Gamma_i(V, 1801)$ :

each colour occurs $150$ times in $[1, 900]$ ;
$|V| = 301$ ;
$|\Gamma_i(V, v)| = 60$ for every $v \in V$ and every colour $i \ne q$ ;
$c(901 - d) = c(901 + d)$ for every $d \in [1, 900]$ with $c(d) = q$ ;
for every colour $i \ne q$ : $|P_i| = 60$ ; $x \mapsto 1800 - x$ maps $P_i$ to itself without fixed points; and $c(|x - y|) \notin \{i, q\}$ for distinct $x, y \in P_i$ .

The goal is a structure theorem under the hypothesis $R_4(3) \le 61$ . It does not prove $S(6) \le 1800$ , and it does not assert that a Schur colouring of $[1, 1801]$ with six colours exists; whether such a colouring, or the structure it would force, exists is open. The goal is the six-colour instance of the general theorems below.

Centred-interval bound

\mathrm{TR}(k, r) \implies \Bigl[1,\ 2(k+1)\Bigl\lfloor \tfrac{r-1}{2} \Bigr\rfloor + 2\Bigr] \text{ is not covered by } k + 1 \text{ sumfree sets.}

Balanced colour classes

\mathrm{TR}(k, 2t + 2),\ m = (k+1)t,\ c \text{ a Schur colouring of } [1, 2m+1] \text{ with } k + 1 \text{ colours} \implies \bigl|\{\, d \in [1, m] : c(d) = j \,\}\bigr| = t \ \text{ for every colour } j.

Nested saturation

\text{frontier hypotheses} \implies |\Gamma_i(V_m, v)| = u \qquad (v \in V_m,\ i \ne c(m+1)).

Automorphism extension

For a colouring $\mathrm{col}$ of ordered pairs, a finite set $W$ , a point $e \notin W$ and a map $J$ with $J(W) \subseteq W$ , $J \circ J = \mathrm{id}$ on $W$ and $\mathrm{col}(J(x), J(y)) = \mathrm{col}(x, y)$ on $W$ :

v \in W \text{ and } J(v) \text{ have equal colour degrees in } W \cup \{e\} \implies \mathrm{col}(v, e) = \mathrm{col}(J(v), e).

Forced reflection

\text{frontier hypotheses} \implies c(m + 1 - d) = c(m + 1 + d) \qquad (d \in [1, m],\ c(d) = c(m+1)).

The saturation degree is even

\text{frontier hypotheses} \implies u \text{ is even}.

Significance

The result itself. Under $R_4(3) \le 61$ , $S(6) \le 1801$ , and the goal constrains a six-colour Schur colouring of $[1, 1801]$ as listed above. In particular, each of its five endpoint neighbourhoods is a set of $30$ pairs $\{900 - d, 900 + d\}$ whose difference colouring uses at most four colours, is invariant under $x \mapsto 1800 - x$ and, like that of every subset of $[0, 1801]$ , has no monochromatic triangle. So such a colouring yields five colourings of $K_{60}$ with at most four colours, no monochromatic triangle and a fixed-point-free colour-preserving involution. A proof that this configuration cannot occur would give $S(6) \le 1800$ under the same hypothesis. Whether it can occur, and whether $S(6) \le 1800$ , are open.

Formalizing it. All 12 theorems of the tree, the goal included, are proved in Lean 4 with Mathlib over the bundles ClassicalSchurBasic, ClassicalSchurRamsey and ClassicalSchurColoring, with the axioms propext, Classical.choice and Quot.sound only. Independent Claude agents checked the Lean: one rebuilt the frontier theorems, re-ran their axiom audit and checked their statements against the argument; another checked every statement of the tree against the mathematics. The mathematics is in the paper $S(6) \le 1801$ if $R_4(3) \le 61$ : a centred Schur bound and the structure at the frontier (A. McKenna, Zenodo, 2026, doi:10.5281/zenodo.23156099), and the Lean code is in its repository; the paper has not been refereed. $R_4(3) \le 61$ is not formalized in the mission.

Difficulty

The centred bound counts, for one colour class, the points $h \pm a$ around the centre of the interval. At the frontier every such count is tight: each colour has $t$ elements in $[1, m]$ , and inside $V_m$ each colour other than $c(m+1)$ has degree $u$ , the largest value that $R_k(3) \le u + 1$ allows. So no single counting step gives a contradiction, and the theorems describe the tight case instead of excluding it. The first exclusion that the structure gives, parity, works only for odd $u$ ; at six colours $u = 60$ .

The reflection is not a property of Schur colourings in general: the colouring $\{1, 4\}$ , $\{2, 3\}$ , $\{5\}$ of $[1, 5]$ has $c(2) = c(3)$ but $c(1) \ne c(5)$ . At the frontier the theorem asserts it only for the $d$ with $c(d) = c(m+1)$ , so an argument that assumes a fully symmetric colouring proves a different statement. A direct search is no substitute: $S(5) = 160$ already needed a large certified SAT computation (Heule 2018), and $[1, 1801]$ with six colours is a much larger instance.

Formalization scope

Colourings are functions ℕ → Fin n on all of $\mathbb{N}$ ; SchurColoring N c constrains only $[1, N]$ , with $x = y$ allowed. Distances are Nat.dist.
Neighbourhoods are Finsets. $V_m$ lies in range (2 * m + 2) $= [0, 2m+1]$ , so the point $0$ is a candidate member; the centre $m$ never is.
TriangleRamsey k r takes colours from any Finset of at most $k$ naturals; the pair colouring ℕ → ℕ → ℕ is constrained only on the pairs $x < y$ of the vertex set, which is any finite set of naturals. TriangleRamsey k 0 and TriangleRamsey k 1 are false.
Covers. CoveredBySumFree X n uses Fin n → Set ℕ; the sets need not be disjoint or lie in $X$ .
Subtraction is truncated. Under the hypotheses, none of $r - 1$ , $N - 1$ , $m + 1 - d$ , $2m - x$ (with $x \in P_i$ ), $901 - d$ and $1800 - x$ truncates.
No trivialization. The frontier theorems are vacuous for $u = 0$ , and for $k = 0$ (then $[1, 2m + 1] \supseteq [1, 5]$ , while $S(2) = 4$ ). For $k = 1$ they are not: the Schur colourings of $[1, 13]$ meet the hypotheses, and every conclusion can be checked by hand. The goal holds vacuously if $R_4(3) > 61$ or if no six-colour Schur colouring of $[1, 1801]$ exists; it is a structure theorem, not a claim that such a colouring exists.

Bundles: ClassicalSchurBasic (SumFree, CoveredBySumFree) and ClassicalSchurRamsey (TriangleRamsey) are already public; ClassicalSchurColoring holds SchurColoring, colorNbhd, centralNbhd and endpointNbhd. Reusable: the colouring–cover bridges, the pigeonhole step, the centred bound for every $k$ , and the automorphism-extension lemma (arbitrary types). Welcome beyond the targets: a formal proof of TriangleRamsey 4 61, and results on whether the configuration of five paired $60$ -point sets exists.

Provenance: the centred-interval argument was first written by an AI agent based on ChatGPT (OpenAI) in a project discussion on 2026-09-27, and a Claude (Anthropic) agent audited it. The balance, saturation and reflection argument was proposed by an AI agent based on ChatGPT (OpenAI) in a project discussion; Claude checked each step and restated it with explicit hypotheses. Claude wrote the Lean proofs of both parts; the independent checks are described under Formalizing it.

Selected references

R. E. Greenwood, A. M. Gleason, Combinatorial relations and chromatic graphs, Canad. J. Math. 7 (1955) 1–7. https://doi.org/10.4153/CJM-1955-001-4
S. W. Golomb, L. D. Baumert, Backtrack programming, J. ACM 12 (1965) 516–524. https://doi.org/10.1145/321296.321300
F. R. K. Chung, On the Ramsey numbers $N(3, 3, \dots, 3; 2)$ , Discrete Math. 5 (1973) 317–321. https://doi.org/10.1016/0012-365X(73)90125-8
H. Fredricksen, M. M. Sweet, Symmetric sum-free partitions and lower bounds for Schur numbers, Electron. J. Combin. 7 (2000) #R32. https://doi.org/10.37236/1510
M. J. H. Heule, Schur number five, Proc. AAAI Conf. Artif. Intell. 32 (2018). https://doi.org/10.1609/aaai.v32i1.12209 ; preprint arXiv:1711.08076 (2017). https://arxiv.org/abs/1711.08076
S. P. Radziszowski, Small Ramsey numbers, Electron. J. Combin., Dynamic Survey DS1, revision 18, 2026. https://doi.org/10.37236/21
M. Tatarevic, An improved upper bound for the Ramsey number R(3,3,3,3), GitHub repository, 2026, commit ddd7755. https://github.com/milostatarevic/r3333-upper-bound/commit/ddd7755476db3f0751181db0daec75342576cdd1
A. McKenna, $S(6) \le 1801$ if $R_4(3) \le 61$ : a centred Schur bound and the structure at the frontier, Zenodo, 2026. https://doi.org/10.5281/zenodo.23156099 ; Lean code: https://github.com/mysticflounder/schur-centred-bound (release v1.0.1).

15 thms1 active userReviewed

Linear algebra Numerical Analysis Optimization·Captain: mikedeng1

Projection-like Retractions on Matrix Manifolds IV: Within σ_r(X̄)/2 of a Rank-r Matrix, the Truncated SVD Is the Unique Nearest Matrix of Rank Exactly rResearch Paper

Motivation

Optimization over sets of matrices of fixed rank comes up in low-rank matrix completion, model reduction, and the low-rank approximation of solutions of large matrix equations. A standard approach treats the constraint set as a Riemannian manifold and runs gradient or Newton-type methods on it (Absil, Mahony & Sepulchre 2008). Each iteration takes a step in the tangent space and then has to return to the manifold. A map that does this to first order is called a retraction, and its cost is often what decides whether a manifold method is practical.

Absil and Malick (2012) study retractions defined by projection: step to $X+Z$ in the ambient space, then take the nearest point of the manifold. Their Proposition 3.2 shows that for any $C^k$ submanifold ( $k\ge2$ ) this projective retraction is a retraction. Section 3.2 makes it explicit for the manifold of fixed-rank matrices: near any matrix of rank $r$ , the nearest matrix of rank exactly $r$ is the truncated singular value decomposition (Proposition 3.3). Section 4.4 also gives a closed form for a second retraction on the same manifold, the orthographic retraction (Proposition 4.11).

Setting

Fix natural numbers $n$ , $m$ and $r\ge1$ . The space $\mathbb R^{n\times m}$ of real $n\times m$ matrices carries the Frobenius norm $\|X\|^2=\sum_{i,j}X_{ij}^2=\operatorname{trace}(X^\top X)$ (3.6). The fixed-rank set is

\mathcal R_r=\{X\in\mathbb R^{n\times m}:\ \operatorname{rank}(X)=r\},

a smooth submanifold of $\mathbb R^{n\times m}$ . It is not closed: its closure is the set of matrices of rank at most $r$ .

A singular value decomposition (3.5) of $X$ is a factorization $X=U\Sigma V^\top$ in which $U=[u_1,\dots,u_n]\in\mathbb R^{n\times n}$ and $V=[v_1,\dots,v_m]\in\mathbb R^{m\times m}$ are orthogonal and $\Sigma\in\mathbb R^{n\times m}$ is zero off its diagonal. The diagonal of $\Sigma$ holds the singular values of $X$ in nonincreasing order,

\sigma_1(X)\ge\sigma_2(X)\ge\cdots\ge\sigma_{\min\{n,m\}}(X)\ge0,

and $\sigma_i(X)=0$ for $i>\min\{n,m\}$ . A matrix has rank $r$ exactly when $\sigma_r(X)>0=\sigma_{r+1}(X)$ . The truncated SVD of rank $r$ is $\hat X=\sum_{i=1}^r\sigma_i(X)u_iv_i^\top$ (3.7).

For a set $Q$ and a point $X$ , the projection $P_Q(X)$ is the set of nearest points: the $Y\in Q$ with $\|X-Y\|\le\|X-W\|$ for all $W\in Q$ . For a set that is not closed, $P_Q(X)$ may be empty or contain several points.

Formalization targets

Goal: Proposition 3.3

Let $\bar X\in\mathcal R_r$ . For every $X$ with $\|X-\bar X\|<\sigma_r(\bar X)/2$ and every singular value decomposition $X=U\Sigma V^\top$ ,

P_{\mathcal R_r}(X)=\Bigl\{\sum_{i=1}^r\sigma_i(X)\,u_iv_i^\top\Bigr\}.

The projection exists, is unique, and is the truncated SVD. The radius $\sigma_r(\bar X)/2$ and the strict inequality are those of the paper.

Milestones

The paper's proof goes through four claims, which are the milestones in attack order:

Weyl's bound (§3.2, proof of Proposition 3.3, citing Horn–Johnson 7.3.8): $|\sigma_i(\bar X)-\sigma_i(X)|\le\|X-\bar X\|$ for every $i\ge1$ .
Eckart–Young (3.7): for every singular value decomposition of $X$ , $\hat X$ is a nearest matrix to $X$ of rank at most $r$ .
The gap (3.8): if $\operatorname{rank}\bar X=r$ and $\|X-\bar X\|<\sigma_r(\bar X)/2$ , then $\sigma_{r+1}(X)<\sigma_r(\bar X)/2<\sigma_r(X)$ .
Uniqueness under a gap (§3.2, proof of Proposition 3.3, citing Helmke–Moore): if $\sigma_r(X)>\sigma_{r+1}(X)$ , then $\hat X$ is the only nearest matrix of rank at most $r$ .

Further result: Proposition 4.11

Write $X=U\left[\begin{smallmatrix}\Sigma_0&0\\0&0\end{smallmatrix}\right]V^\top$ (4.7), with $\Sigma_0$ the positive diagonal of nonzero singular values, and a tangent vector $Z=U\left[\begin{smallmatrix}A&C\\B&0\end{smallmatrix}\right]V^\top$ (4.8). If $\Sigma_0+A$ is invertible, the orthographic retraction is

R(X,Z)=U\begin{bmatrix}\Sigma_0+A&C\\B&B(\Sigma_0+A)^{-1}C\end{bmatrix}V^\top .

Here $R(X,Z)$ is the nearest point to $X+Z$ of $\mathcal R_r\cap(X+Z+N_{\mathcal R_r}(X))$ .

Significance

The result. Proposition 3.3 reduces the projective retraction on $\mathcal R_r$ to one truncated singular value decomposition. With Proposition 3.2 this gives an explicit, computable retraction for Riemannian optimization on fixed-rank matrices. It is used, for instance, in low-rank matrix completion algorithms. The point is local: $\mathcal R_r$ is not closed, so far from $\mathcal R_r$ the nearest matrix of rank exactly $r$ need not exist, and the proposition gives an explicit radius on which it does exist and is unique. Proposition 4.11 gives a second retraction that needs only products of matrices and one $r\times r$ inverse.

Formalizing it. All results here are proved, on paper. To the best of a search of Mathlib and the Prove2Me catalog, none is machine-checked. Mathlib has singular values of linear maps between finite-dimensional inner product spaces (LinearMap.singularValues), but no singular value decomposition in matrix form, no Weyl perturbation inequality for singular values, and no Eckart–Young theorem. A complete development would add these, and the Eckart–Young theorem with its uniqueness case is a standard result of numerical linear algebra in its own right.

Difficulty

The proof in the paper is short only because it cites three facts, and each of them is a real piece of matrix analysis.

Weyl's bound needs the variational (min–max) description of singular values, which Mathlib does not have for singular values.
Eckart–Young requires comparing $\|X-Y\|$ with the singular values of $X$ for every $Y$ of rank at most $r$ , not only for those diagonal in the same bases. The obvious approach, writing $Y$ in the singular bases of $X$ , fails because $Y$ need not be diagonal there.
Uniqueness under the gap requires showing that every minimizer is diagonal in some singular bases of $X$ and then using the gap to fix its support. Without the gap uniqueness fails: for $X=I_2$ and $r=1$ every $uu^\top$ with $\|u\|=1$ is a nearest point.

A further subtlety: Proposition 3.3 must hold for any singular value decomposition of $X$ . Singular vectors are not unique, so the proof has to show that the truncation does not depend on the choice under the gap (3.8).

Formalization scope

Matrices are Matrix (Fin n) (Fin m) ℝ with Mathlib's Frobenius norm (open scoped Matrix.Norms.Frobenius). The projection is the published platform predicate RandomGradFree.Nonsmooth.IsMetricProjection, and $P_{\mathcal R_r}(X)$ is the set {Y | IsMetricProjection (rankSet r) X Y}. The set equality with a singleton states existence, uniqueness and the formula together.

Conventions committed to:

sv X i is $\sigma_i(X)$ , 1-based as on the page. It is Mathlib's 0-based singularValues of Matrix.toEuclideanLin X at i - 1, so the index $0$ is meaningless and every statement uses indices $\ge1$ .
IsSVD X U S V is the predicate of (3.5). The singular value decomposition is a hypothesis of the theorems, never a choice made inside them, so the theorems hold for every singular value decomposition.
truncSVD r U S V is $\sum_{i\le r}\Sigma_{ii}u_iv_i^\top$ , written with the diagonal of S. That these entries are the singular values $\sigma_i(X)$ is a fact to be proved, not part of the definition.
The hypothesis $r\ge1$ is added, because $\sigma_r$ needs it (and $\mathcal R_0=\{0\}$ ). It is the only hypothesis of Proposition 3.3 not printed on the page.
In Proposition 4.11, matrices use the block index types Fin r ⊕ Fin p and Fin r ⊕ Fin q. The tangent vector and the normal space are taken in the form the page gives, and invertibility of $\Sigma_0+A$ is an explicit hypothesis. In the paper's proof it comes from " $Z$ in a neighborhood of the origin".

A formalization in which the radius is replaced by a smaller one, the projection is taken onto the matrices of rank at most $r$ , or the singular value decomposition is chosen inside the statement is a different theorem and is ruled out.

Wanted contributions, all reusable beyond this mission:

existence of a singular value decomposition in matrix form, and the identification of its diagonal with singularValues;
Weyl's inequality for singular values;
the Eckart–Young theorem and its uniqueness case;
the Schur-complement rank formula for $2\times2$ block matrices, used for Proposition 4.11.

Selected references

P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds, SIAM J. Optim. 22(1):135–158, 2012. https://doi.org/10.1137/100802529 (authors' version HAL hal-00651608v2: https://hal.science/hal-00651608v2)
P.-A. Absil, R. Mahony and R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://press.princeton.edu/absil
C. Eckart and G. Young, The approximation of one matrix by another of lower rank, Psychometrika 1(3):211–218, 1936. https://doi.org/10.1007/BF02288367
R. A. Horn and C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985 (§7.3, §7.4). https://doi.org/10.1017/CBO9780511810817
U. Helmke and J. B. Moore, Optimization and Dynamical Systems, Springer, 1994 (Ch. 5). https://doi.org/10.1007/978-1-4471-3467-1

8 thms1 active userReviewed

Completed

Number Theory·Captain: xuanji

Every Odd Number Greater Than 1 is the Sum of at Most 6101 PrimesResearch Paper

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$ :

Schnirelmann (1930s): some finite $k$ , by elementary methods.
Vinogradov (1937): every sufficiently large odd integer is a sum of three primes.
Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
Tao (2014): at most five primes. (arXiv:1201.6656)
Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's first proved value, $100\,001$ , came from Schnirelmann's method with every constant written out. This entry records a sharper value, $6101$ , from the same elementary circle of ideas.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset of primes summing to $n$ with at most $k$ elements counted with multiplicity. The Schnirelmann density of $A \subseteq \mathbb{Z}_{\ge 0}$ is $\sigma(A) = \inf_{N \ge 1} |A \cap \{1, \dots, N\}|/N$ (Mathlib: schnirelmannDensity).

Formalization target

Goal

\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 6101,\ \textstyle\sum s = n.

This is the campaign template with the value $6101$ filled in. The source proves the stronger statement that every odd $n \ge 12\,203$ is a sum of exactly $6101$ primes; the at-most form for all odd $n > 1$ follows.

How the bound arises

It keeps the explicit Selberg sieve, Cauchy–Schwarz and Schnirelmann's original sumset inequality from the $100\,001$ entry, and improves the first moment:

Whole-triangle count. Counting all pairs with $p + q \le x$ gives $\sum_{s \le x} r(s) \ge 2(x-2000)^2/(9(\log x)^2)$ for $x \ge 2000$ .
Weighting. Weighting $r(s)$ by $(\log s)^2/s$ cancels the varying factor in the sieve bound $r(s) \le 9\,C(s)\,s/(\log s)^2$ , giving a weighted first moment of at least $\tfrac{44}{100}x$ .
Second moment of $C$ . With $\sum_{s \le x,\, 2\mid s} C(s)^2 \le \tfrac{21}{2}x$ , Cauchy–Schwarz yields $\sigma(A) \ge 1/2200$ for $A = B + B$ , $B = \{(p-3)/2\}$ .
Schnirelmann's inequality with $m = 1525$ (the least $m$ with $(1 - 1/2200)^m < 1/2$ ) gives $K = 4m + 1 = 6101$ .

Significance

The bound is far weaker than Tao's $5$ or Helfgott's $3$ , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from $100\,001$ . Reusable components:

Explicit Chebyshev-type lower bound for $\pi(y)$ .
Explicit Selberg upper-bound sieve for $r(s)$ .
Moment bounds for the singular-series factor $C(s)$ .
Schnirelmann's inequality $\sigma(D+E) \ge \sigma(D)+\sigma(E)-\sigma(D)\sigma(E)$ .

Formalization scope

The Lean statement is the campaign template verbatim with $6101$ in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.

Selected references

P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
Explicit improvement of the $100\,001$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $6101$ ; not peer reviewed.

1 thm1 active userReviewed

Completed

Number Theory·Captain: xuanji

Every Odd Number Greater Than 1 is the Sum of at Most 97041 PrimesResearch Paper

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$ :

Schnirelmann (1930s): some finite $k$ , by elementary methods.
Vinogradov (1937): every sufficiently large odd integer is a sum of three primes.
Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
Tao (2014): at most five primes. (arXiv:1201.6656)
Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's first proved value, $100\,001$ , came from Schnirelmann's method with every constant written out. This entry records a sharper value, $97\,041$ , from the same elementary circle of ideas.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset of primes summing to $n$ with at most $k$ elements counted with multiplicity. The Schnirelmann density of $A \subseteq \mathbb{Z}_{\ge 0}$ is $\sigma(A) = \inf_{N \ge 1} |A \cap \{1, \dots, N\}|/N$ (Mathlib: schnirelmannDensity).

Formalization target

Goal

\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 97\,041,\ \textstyle\sum s = n.

This is the campaign template with the value $97\,041$ filled in. The source proves the stronger statement that every odd $n \ge 194\,083$ is a sum of exactly $97\,041$ primes; the at-most form for all odd $n > 1$ follows.

How the bound arises

It is the argument behind the $100\,001$ entry, unchanged up to the last step: the explicit Selberg sieve and Cauchy–Schwarz give $\sigma(A) \ge 1/35\,000$ for $A = B + B$ , $B = \{(p-3)/2 : p \text{ odd prime}\}$ . The only change is to take the smallest admissible $m$ in Schnirelmann's inequality: $(1 - 1/35\,000)^{m} < 1/2$ first holds at $m = 24\,260$ (rather than the rounded $25\,000$ ), so $2mA = \mathbb{Z}_{\ge 0}$ and $K = 4m + 1 = 97\,041$ .

Significance

The bound is far weaker than Tao's $5$ or Helfgott's $3$ , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from $100\,001$ . Reusable components:

Explicit Chebyshev-type lower bound for $\pi(y)$ .
Explicit Selberg upper-bound sieve for $r(s)$ .
Moment bounds for the singular-series factor $C(s)$ .
Schnirelmann's inequality $\sigma(D+E) \ge \sigma(D)+\sigma(E)-\sigma(D)\sigma(E)$ .

Formalization scope

The Lean statement is the campaign template verbatim with $97\,041$ in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.

Selected references

P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
Explicit improvement of the $100\,001$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $97\,041$ ; not peer reviewed.

1 thm1 active userReviewed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Dynamic Pricing Strategies with Reference Effects I: Under Loss Aversion the Steady States Form an Interval and Optimal Paths ConvergeResearch Paper

Motivation

Consumers judge a price against a reference price, an internal standard formed from the prices they have seen before. A price below the reference is perceived as a gain and stimulates demand; a price above it is perceived as a loss and depresses demand. Prospect theory (Kahneman and Tversky 1979) adds that losses loom larger than gains of the same size: this is loss aversion. A firm that sets prices over many periods therefore faces a dynamic trade-off, because today's price moves tomorrow's reference price and with it tomorrow's demand.

Popescu and Wu (Operations Research 55(3), 2007) analyze this problem for general nonlinear demand. Earlier work of Kopalle, Rao and Assunção (1996) and of Fibich, Gavious and Lowengart (2003) had treated linear or piecewise-linear reference effects with explicit solutions. Popescu and Wu replace explicit solutions by structural arguments (supermodularity, monotone policies, comparison of value functions), which is what makes the results reusable for any demand model satisfying their assumptions. Their headline result for loss-averse consumers is that the long-run prices form a whole interval rather than a single point, and that optimal prices outside the interval move monotonically to its nearer endpoint.

Setting

A monopolist chooses a price $p_t$ from $P=[0,\bar p]$ , $\bar p>0$ , in each period $t=0,1,2,\dots$ . The reference price follows exponential smoothing,

r_{t+1}=\alpha r_t+(1-\alpha)p_t,\qquad \alpha\in[0,1),

from a given initial reference price $r_0$ . Demand is $D(p,r)=d(p)+R(r-p,r)$ , where $d(p)=D(p,p)$ is the base demand and $R(x,r)$ is the reference effect of the perceived gain $x=r-p$ , so that $R(0,r)=0$ . The per-period profit (zero unit cost) is $\Pi(p,r)=p\,D(p,r)$ , the base profit is $\pi(p)=p\,d(p)$ , and $\lambda(r)$ denotes the slope of $R(\cdot,r)$ at $x=0$ .

For a discount factor $\beta\in(0,1)$ , the value function is the supremum of discounted profit over all price sequences in $P$ :

V(r_0)=\sup_{(p_t)\in P^{\mathbb N}}\sum_{t\ge 0}\beta^t\,\Pi(p_t,r_t).

The Bellman objective is $W(p,r)=\Pi(p,r)+\beta V(\alpha r+(1-\alpha)p)$ . The optimal pricing policy $p^*(r)$ is the largest maximizer of $W(\cdot,r)$ over $P$ , and $q^*(r)=\alpha r+(1-\alpha)p^*(r)$ is the next reference price. The state path is $r^*_{t+1}=q^*(r^*_t)$ and the price path is $p^*_t=p^*(r^*_t)$ . A steady state is a price $p^{**}\in P$ with $p^*(p^{**})=p^{**}$ .

The standing Assumption 1 requires $D$ to be nonnegative, bounded and continuous, decreasing in $p$ , increasing in $r$ , and $R$ increasing in $x$ . For a smooth (loss-neutral) $R$ , Assumptions 2–3 require $R$ to be twice differentiable, $\pi$ to be nonmonotonic and concave, $\pi'(r)-r\lambda(r)$ to be strictly decreasing, and the reference profit $\Pi^R(p,r)=pR(r-p,r)$ to be concave in $p$ and supermodular.

Under loss aversion the reference effect is kinked: $R_K(x,r)=R_G(x,r)$ for gains $x\ge 0$ and $R_K(x,r)=R_L(x,r)$ for losses $x<0$ . Assumption 4 makes $R_G$ and $R_L$ twice differentiable and increasing in $x$ , makes $R_G-R_L$ single crossing, and imposes $\lambda_L(r)>\lambda_G(r)$ . Assumption 5 requires the gain and loss profits to satisfy Assumption 3. The problems $(K)$ , $(P_L)$ and $(P_G)$ are the pricing problem with reference effect $R_K$ , $R_L$ and $R_G$ , respectively, and $(P_\theta)$ uses $R_\theta=\theta R_G+(1-\theta)R_L$ for $\theta\in[0,1]$ .

Formalization targets

Goal: Theorem 4 of the paper

There exist prices $p^{**}_L\le p^{**}_G$ such that $p^{**}_L$ is the unique steady state of $(P_L)$ , $p^{**}_G$ is the unique steady state of $(P_G)$ , and

\{\,r:\ r \text{ is a steady state of }(K)\,\}=[p^{**}_L,p^{**}_G].

Moreover, the following hold:

from $r_0\in[p^{**}_L,p^{**}_G]$ , the optimal price path of $(K)$ is constant, $p^*_t=r_0$ ;
from $r_0<p^{**}_L$ , the state path of $(K)$ is nondecreasing and converges to $p^{**}_L$ , and so does the price path;
from $r_0>p^{**}_G$ , the state path is nonincreasing and converges to $p^{**}_G$ , and so does the price path.

Milestones

In attack order, the milestones are:

Remark 2 ( $V$ increasing);
Lemma 2 ( $q^*$ increasing);
Theorem 1, first sentence (a steady state is the unique solution of $\pi'(p)/(1-\beta)=p\lambda(p)/(1-\alpha\beta)$ );
Theorem 2 (a unique steady state exists and attracts every optimal path, with monotone state paths);
Remark 3 (a steeper reference effect gives a lower steady state);
Lemma 4 ( $(P_\theta)$ satisfies Assumptions 1–3, $V_\theta\ge V_K$ , and steady states of $(P_\theta)$ are steady states of $(K)$ );
the §5.2 statement that the steady states $p^{**}_\theta$ span $[p^{**}_L,p^{**}_G]$ ;
the §A.11 identity $V_K(r_0)=V_L(r_0)$ for $r_0<p^{**}_L$ .

Significance

The theorem separates loss-averse markets from loss-neutral ones. With a smooth reference effect, Theorem 2 gives one long-run price. Under loss aversion, every price in $[p^{**}_L,p^{**}_G]$ is self-sustaining: a firm that starts there gains nothing by moving. Prices therefore exhibit stickiness, an interval of rigid prices, which is the dynamic counterpart of the kink in the reference effect. The paper uses this result to derive price monotonicity under loss aversion (its Proposition 4) and the behavior of myopic firms (its Proposition 5).

The result is proved in the paper; nothing here is open. What the mission adds is a machine-checked proof, and that proof has to supply steps the paper passes over quickly. Among them are the existence of steady states in Theorem 2 (the paper argues it in two sentences) and the largest-maximizer bookkeeping when steady states are transferred from $(P_\theta)$ to $(K)$ .

Difficulty

The bulk of the work sits in the infinite-horizon dynamic program itself. The value function is a supremum over infinite price sequences. Before any comparative statics can be done, one must show that it satisfies the Bellman equation (2), that it is continuous, and that the argmax is nonempty, so that the largest maximizer is well defined and actually maximizes. The monotonicity of $q^*$ does not follow from supermodularity of $\Pi$ alone, because the policy maximizes current profit plus a continuation value evaluated at a state that itself depends on the price.

For the kinked problem, $R_K$ is not differentiable at $x=0$ , so the first-order analysis behind Theorem 1 does not apply to $(K)$ . A first-order condition with one-sided derivatives is the natural first idea. It yields inequalities that every steady state must satisfy, but it establishes neither that steady states exist nor that the whole interval consists of steady states. The set equality also depends on the largest-maximizer convention, since a price that is merely a maximizer of the Bellman objective is not a steady state under the paper's definition.

Formalization scope

All declarations live in the namespace ReferencePricing.LossAversion.

Data. The model data are a base demand d : ℝ → ℝ and reference effects R : ℝ → ℝ → ℝ, with demand d p + R (r - p) r. $R(0,r)=0$ is a field of Assumption 1.
Value function. value takes the per-period profit as a parameter and is the real supremum ⨆ over sequences ℕ → Set.Icc 0 pbar of the tsum of discounted profits. It is not a function assumed to solve (2).
Policy. optPrice is sSup of the set of maximizers in $P$ of the Bellman objective, following the paper's largest-maximizer convention. Nonemptiness of that set is to be proved, never assumed.
Steady states. IsSteadyState r is r ∈ P ∧ optPrice r = r.
Encodings. Monotonicity, concavity and supermodularity hypotheses are required on $P$ or $P\times P$ , and monotonicity in $x$ and single crossing on the reachable gains $[r-\bar p,r]$ . "Twice differentiable" means that the uncurried function and its Fréchet derivative are differentiable. "Nonmonotonic" means neither monotone nor antitone on $P$ .
Added hypotheses. Two hypotheses are added and disclosed in each item. The base demand $d$ is differentiable, because $\pi'$ appears in Assumption 3(b). The demands of $R_G$ and $R_L$ satisfy Assumption 1, which the paper's proof of Lemma 4 uses.
Typos. The page's typo " $r_0>p^*_G$ " in Theorem 4 is read as $p^{**}_G$ .
Ruling out trivial versions. The goal quantifies $p^{**}_L$ and $p^{**}_G$ existentially with uniqueness, so the existence of these steady states is part of the claim. It is not a formalization with arbitrary endpoints supplied as hypotheses, nor one with "some optimal policy" in place of the largest maximizer. The hypotheses are jointly satisfiable: the linear instance $\bar p=3/4$ , $d(p)=1-p$ , $R_L=x/4$ , $R_G=x/8$ meets all of them.

A complete development needs:

the Bellman equation and continuity of the value function for bounded continuous rewards on a compact action set (Berge's maximum theorem);
Topkis-type monotone comparative statics on intervals;
convergence of monotone bounded sequences.

The first two are reusable beyond this mission, and contributions of either as general lemmas are welcome.

Selected references

I. Popescu and Y. Wu, Dynamic Pricing Strategies with Reference Effects, Operations Research 55(3):413–429, 2007. https://doi.org/10.1287/opre.1070.0393
D. Kahneman and A. Tversky, Prospect Theory: An Analysis of Decision under Risk, Econometrica 47(2):263–291, 1979. https://doi.org/10.2307/1914185
P. K. Kopalle, A. G. Rao and J. L. Assunção, Asymmetric Reference Price Effects and Dynamic Pricing Policies, Marketing Science 15(1):60–85, 1996. https://doi.org/10.1287/mksc.15.1.60
G. Fibich, A. Gavious and O. Lowengart, Explicit Solutions of Optimization Models and Differential Games with Nonsmooth (Asymmetric) Reference-Price Effects, Operations Research 51(5):721–734, 2003. https://doi.org/10.1287/opre.51.5.721.16758
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
N. L. Stokey, R. E. Lucas and E. C. Prescott, Recursive Methods in Economic Dynamics, Harvard University Press, 1989. https://www.hup.harvard.edu/books/9780674750968

13 thms1 active userReviewed

Dynamic Programming Linear Optimization Operations Research+2·Captain: mikedeng1

On the Choice-Based Linear Programming Model for Network Revenue Management I: The CDLP Is Asymptotically Optimal under Proportional ScalingResearch Paper

Motivation

Airlines, hotels and railways sell a fixed stock of perishable capacity (seats on flight legs, room-nights) to customers who arrive over a finite selling horizon. Network revenue management decides, at each moment, which products to keep open for sale. In the classical independent-demand model each product has its own demand stream. In practice customers choose among the products on offer, and closing a cheap fare shifts some of its demand to a more expensive one. Talluri and van Ryzin (Management Science 2004) modelled this with choice-based demand on a single resource: the firm chooses an offer set $S$ , and an arriving customer buys product $j$ with probability $P_j(S)$ .

On a network the exact dynamic program has one state per vector of remaining leg capacities, and cannot be solved at realistic sizes. Gallego, Iyengar, Phillips and Dubey (CORC Technical Report TR-2004-01, 2004) proposed replacing it with a linear program over the time allotted to each offer set, the choice-based deterministic linear program (CDLP). Liu and van Ryzin (MSOM 2008) analysed this LP. Their first result has two parts: the CDLP value is an upper bound on the optimal expected revenue, and the bound is asymptotically tight when capacity and horizon are scaled up together. For the independent-demand deterministic LP the analogous statement goes back to Gallego and van Ryzin (Operations Research 1997) and Cooper (Operations Research 2002). This mission targets the choice-based version.

Setting

A choice-based network instance has $m$ legs and $n$ products $N = \{1,\dots,n\}$ , and consists of:

an incidence matrix $A = [a_{ij}]$ with $a_{ij} \in \{0,1\}$ , where $a_{ij}=1$ when product $j$ uses leg $i$ ; $A_j$ is its $j$ th column;
a revenue $r_j \in \mathbb{R}$ for each product (no sign assumed);
an arrival probability $\lambda \in [0,1]$ per period;
choice probabilities $P_j(S)$ for every offer set $S \subseteq N$ , with $P_j(S) \ge 0$ , $P_j(S)=0$ for $j \notin S$ , and $\sum_{j\in S} P_j(S) \le 1$ . The no-purchase probability is $P_0(S) = 1 - \sum_{j\in S}P_j(S)$ .

$\lambda$ and $P$ are the same in every period. Each offer set has an expected revenue $R(S) = \sum_{j\in S} r_j P_j(S)$ and a capacity-consumption vector $Q(S) = AP(S)$ .

The dynamic program. With remaining capacity $x \in \mathbb{N}^m$ , an offer set is allowed if $x - A_j \ge 0$ for all $j \in S$ (no overbooking). The empty set is always allowed. The value with $k$ periods left is $V^{(0)} \equiv 0$ and

V^{(k+1)}(x) = \max_{S \text{ allowed at } x}\Big\{\sum_{j\in S}\lambda P_j(S)\big(r_j + V^{(k)}(x-A_j)\big) + \big(\lambda P_0(S)+1-\lambda\big)V^{(k)}(x)\Big\}.

The optimal expected revenue over $T$ periods from capacity $c \in \mathbb{N}^m$ is $V^*(c,T) = V^{(T)}(c)$ (dpValue).

The CDLP. Its variables are times $t(S) \ge 0$ , one for each $S \subseteq N$ , and

V^{\mathrm{CDLP}}(c,T) = \max\Big\{\sum_{S}\lambda R(S)t(S) \;:\; \sum_S \lambda Q(S)t(S) \le c,\ \sum_S t(S) \le T,\ t \ge 0\Big\}

(cdlpValue).

Scaling. For $\theta \in \mathbb{N}$ , the $\theta$ -scaled problems have capacities $\theta c$ and horizon $\theta T$ . Write $V^*_\theta = V^*(\theta c,\theta T)$ and $V^{\mathrm{CDLP}}_\theta = V^{\mathrm{CDLP}}(\theta c, \theta T)$ .

Formalization targets

Goal: Proposition 2 (p. 294)

\lim_{\theta\to\infty}\frac1\theta V^*_\theta \;=\; \lim_{\theta\to\infty}\frac1\theta V^{\mathrm{CDLP}}_\theta \;=\; V^{\mathrm{CDLP}}(c,T),

for every instance, every $c \in \mathbb{N}^m$ and every $T\in\mathbb{N}$ . It is stated as two Tendsto statements along $\theta \to \infty$ in $\mathbb{N}$ .

Milestones

Proposition 1 (p. 294): $V^*(c,T) \le V^{\mathrm{CDLP}}(c,T)$ for every $c$ and $T$ .
Scaling of the CDLP (proof of Proposition 2, first paragraph): $V^{\mathrm{CDLP}}(\theta c,\theta T) = \theta\,V^{\mathrm{CDLP}}(c,T)$ for every $\theta \in \mathbb{N}$ .
Lower half of the first limit (proof of Proposition 2, pp. 294–295): for every $\varepsilon>0$ , eventually in $\theta$ , $V^{\mathrm{CDLP}}(c,T) - \varepsilon \le \frac1\theta V^*_\theta$ .

The goal follows from the three milestones.

Significance

The result. Proposition 1 makes the CDLP a certified upper bound on what any control policy can earn, whatever the choice model. Numerical studies use it to benchmark heuristics. Proposition 2 says the bound is exact to first order in large systems, so policies driven by the CDLP solution (time allocations, bid prices from its dual) lose only a vanishing fraction of revenue. It is the justification for the whole family of CDLP-based controls that the paper and later work study (column generation, decomposition, and later the affine and piecewise-linear relaxations of the choice-based network problem).

Formalizing it. The result is proved in the paper. No machine-checked version exists: no revenue-management DP with choice-based demand on a network, no CDLP, and no fluid-limit argument of this kind is on the platform. The existing RevenueManagement material from the Talluri–van Ryzin textbook covers single-resource and dynamic-pricing models. Formalizing the result produces a reusable network-RM DP with an offer-set action space, the CDLP as a Lean object, and a checked asymptotic-optimality theorem that other deterministic-approximation results (independent demand, bid-price heuristics) can follow.

Difficulty

The upper bound compares a stochastic dynamic program with a linear program. The natural route builds a feasible LP point from the optimal policy (expected times each set is offered), but the DP here is a recursion over capacity vectors, not a policy class with a notion of "expected time offered". That connection has to be made from the recursion itself.

The lower bound is harder. The paper's policy offers each set for a fractional number of periods and caps accepted demand at its mean after customers have chosen. Neither is an action available in the DP, where the firm can only pick an allowed offer set each period and must accept whatever the customer picks. The obvious transcription therefore does not type-check against the model: one needs a genuine DP policy whose revenue is $\theta V^{\mathrm{CDLP}} - o(\theta)$ while it respects capacity on every sample path. The no-overbooking rule forbids offering a set once any of its products would exceed remaining capacity. Negative revenues are allowed, and $\lambda$ may be $0$ or $1$ .

Formalization scope

Legs are Fin m, products Fin n, offer sets Finset (Fin n). The instance is a structure ChoiceNetwork m n carrying $A$ (entries in $\mathbb{N}$ , each $0$ or $1$ ), $r$ , $\lambda\in[0,1]$ and $P$ with the three choice-model axioms. The DP and CDLP use one $\lambda$ and one $P$ for every period, matching the paper's time-homogeneous model. Capacities and horizon are natural numbers; CDLP times and all values are real. $\theta$ ranges over $\mathbb{N}$ , because $\theta T$ must be a whole number of periods, and the limits use real division by $\theta$ .

$V^*$ is defined by the Bellman recursion (1), which the paper states is equivalent to the stochastic control problem (4). No measure-theoretic policy class is built. The maximization runs over the offer sets allowed at the current capacity, so the DP can neither overbook nor pick products outside an offer set. The paper's boundary condition $V_t(0)=0$ is not imposed separately: it follows from the recursion whenever every product uses a leg, and imposing it on top could contradict the recursion. $V^{\mathrm{CDLP}}$ is sSup of the objective over the feasible set. That set is nonempty ( $t=0$ ) and bounded ( $0 \le t(S) \le T$ ), so the value is the LP optimum.

The goal is the limit equality with both capacity and horizon scaled. A statement with only the upper bound, only capacity scaled, or a DP that ignores capacity or chooses products freely would be a trivializing formalization, and the definitions rule each of these out. Milestone 3 is the paper's conclusion stated on the DP value, not on the paper's informal policy. It is not a repair.

A complete development needs: LP duality or a direct feasibility construction for Proposition 1; the scaling identity for the CDLP; and, for the lower bound, a concrete DP policy together with a law-of-large-numbers or concentration estimate for sums of per-period sales (Mathlib's ProbabilityTheory.strong_law_ae and Hoeffding-type bounds are available). A policy-evaluation lemma that bounds the DP value below by the expected revenue of any feasible offer-set policy is reusable beyond this mission, as is the CDLP scaling lemma. Contributions to either are welcome.

Selected references

Q. Liu, G. van Ryzin, On the Choice-Based Linear Programming Model for Network Revenue Management, Manufacturing & Service Operations Management 10(2):288–310, 2008. https://doi.org/10.1287/msom.1070.0169
K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1):15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147
G. Gallego, G. Iyengar, R. Phillips, A. Dubey, Managing Flexible Products on a Network, CORC Technical Report TR-2004-01, Columbia University, 2004.
G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1):24–41, 1997. https://doi.org/10.1287/opre.45.1.24
W. L. Cooper, Asymptotic Behavior of an Allocation Policy for Revenue Management, Operations Research 50(4):720–727, 2002. https://doi.org/10.1287/opre.50.4.720.2862

7 thms1 active userReviewed

Operations Research Optimization·Captain: mikedeng1

The d-Level Nested Logit Model: Assortment and Price Optimization Problems II: The Push-Up-Then-Push-Down Prices Converge to a Stationary PointResearch Paper

Motivation

Retailers that sell many substitutable products must set all their prices at once, and a customer's reaction to one price depends on what else is on the shelf. The nested logit model captures this by grouping similar products into nests, so that raising one price shifts demand mostly to close substitutes. The $d$ -level nested logit model extends the familiar two-level version to a whole taxonomy tree of depth $d$ (for example category → brand → size). It is consistent with random utility maximization (McFadden 1978) and is widely used in demand estimation.

Pricing under logit-type models is harder than it looks. Already for the multinomial logit model, which is the one-level case, Hanson and Martin (1996) point out that the expected revenue is not necessarily concave in the prices. For the two-level nested logit, Gallego and Wang (2014) show that the expected revenue is not concave and can have several local maxima. Li, Rusmevichientong and Topaloglu (Oper. Res. 63(2), 2015) treat the general $d$ -level model. Their pricing result, Theorem 7.3, is the target of this mission. It shows that a simple gradient-free iteration, the push-up-then-push-down (PUPD) algorithm, produces prices that converge to a stationary point of the expected revenue.

Setting

The products $l=1,\dots,n$ are the leaves of a rooted tree $T=(V,E)$ , all at depth $d$ . A further leaf, node $0$ (the no-purchase option), hangs directly from $\mathrm{root}$ . Every other node $j$ is a nonleaf node with a nonempty set $\mathrm{Children}(j)$ and a parameter $\eta_j$ . The standing assumptions are $\eta_j\in(0,1]$ for nonleaf $j\neq\mathrm{root}$ and $\eta_{\mathrm{root}}=0$ . Each product carries parameters $\alpha_l\in\mathbb R$ and $\beta_l>0$ , and node $0$ carries $\alpha_0\in\mathbb R$ .

Given a price vector $\mathbf p=(p_1,\dots,p_n)$ , where the no-purchase price is fixed at $p_0=0$ , the preference weights are computed bottom-up:

V_l(\mathbf p)=e^{\alpha_l-\beta_lp_l},\qquad V_0(\mathbf p)=e^{\alpha_0},\qquad V_j(\mathbf p)=\Big(\sum_{k\in\mathrm{Children}(j)}V_k(\mathbf p)\Big)^{\eta_j}.

The expected revenues are $R_l(\mathbf p)=p_l$ , $R_0(\mathbf p)=0$ , and

R_j(\mathbf p)=\frac{\sum_{k\in\mathrm{Children}(j)}V_k(\mathbf p)R_k(\mathbf p)}{\sum_{k\in\mathrm{Children}(j)}V_k(\mathbf p)}

at a nonleaf node. The expected revenue of $\mathbf p$ is $R_{\mathrm{root}}(\mathbf p)$ . A customer walks down from $\mathrm{root}$ , choosing a child with probability proportional to its weight. The probability $\theta_l(\mathbf p)$ of ending at product $l$ is the product, over the levels $h=1,\dots,d$ , of $V_{\mathrm{An}(l,h)}/\sum_{k\in\mathrm{Sibling}(\mathrm{An}(l,h))}V_k$ , where $\mathrm{An}(l,h)$ is the ancestor of $l$ in level $h$ .

Top-down, the scalars $u_j(\mathbf p)$ are $u_{\mathrm{root}}=R_{\mathrm{root}}$ and $u_j=\eta_ju_{\mathrm{Parent}(j)}+(1-\eta_j)R_j$ . A stationary point of $R_{\mathrm{root}}$ is a price vector at which the gradient of $R_{\mathrm{root}}$ is zero.

The PUPD algorithm starts from $\mathbf p^0=\mathbf 0$ . Given $\mathbf p^s$ , it sets $t^s_{\mathrm{root}}=R_{\mathrm{root}}(\mathbf p^s)$ and, for every other nonleaf node,

t^s_j=\max\big\{t^s_{\mathrm{Parent}(j)},\ \eta_jt^s_{\mathrm{Parent}(j)}+(1-\eta_j)R_j(\mathbf p^s)\big\}.

It then updates $p^{s+1}_l=1/\beta_l+t^s_{\mathrm{Parent}(l)}$ for every product $l$ .

Formalization targets

Goal: Theorem 7.3 (p. 336)

\exists\,\mathbf p^*\in\mathbb R^n:\qquad \lim_{s\to\infty}\mathbf p^s=\mathbf p^* \quad\text{and}\quad \nabla R_{\mathrm{root}}(\mathbf p^*)=0 .

The whole sequence converges and its limit is stationary. No rate is claimed, and none is asked for.

Milestones

Lemma 7.1 (p. 335). For $\mathbf p\in\mathbb R^n_+$ and every product $l$ ,

\frac{\partial R_{\mathrm{root}}}{\partial p_l}(\mathbf p)=-\theta_l(\mathbf p)\,\beta_l\Big(p_l-\frac1{\beta_l}-u_{\mathrm{Parent}(l)}(\mathbf p)\Big).

Corollary 7.2 (p. 336). For $\mathbf p\in\mathbb R^n_+$ , $\mathbf p$ is a stationary point of $R_{\mathrm{root}}$ if and only if $p_l=1/\beta_l+u_{\mathrm{Parent}(l)}(\mathbf p)$ for all $l$ .

Significance

The result itself. Theorem 7.3 turns a nonconcave, many-product pricing problem into an iteration that needs no gradient evaluations and no step size. Each iteration costs one bottom-up and one top-down pass over the tree. The paper's numerical experiments (§8) report that it reaches a stationary point much faster than gradient ascent. Lemma 7.1 gives the gradient of the expected revenue in closed form for any depth. Corollary 7.2 turns stationarity into a fixed-point equation in the prices, which is what makes a price-update scheme like PUPD natural.

Formalizing it. The proofs of Lemma 7.1 and Theorem 7.3 are in the paper's online Appendix E. The acknowledgments (pp. 340–341) record that an error found in an earlier version led to a new proof that the revenues under the PUPD algorithm are always bounded. A machine-checked proof would settle the convergence claim independently of that history. No nested logit or multinomial logit pricing result, and no part of this one, has a machine-checked proof on Prove2Me.

Difficulty

Lemma 7.1 is a chain-rule computation through a tree of power means, and it is technical rather than deep. The hard part is Theorem 7.3. The obvious fixed-point iteration $p^{s+1}_l=1/\beta_l+u_{\mathrm{Parent}(l)}(\mathbf p^s)$ suggested by Corollary 7.2 is not the algorithm. PUPD replaces $u$ by the scalars $t^s$ , which involve a maximum, and the update direction $\mathbf p^{s+1}-\mathbf p^s$ is in general not parallel to the gradient. So neither contraction arguments for the plain fixed-point map nor the standard ascent analysis of gradient methods applies directly. $R_{\mathrm{root}}$ is not concave and may have several stationary points, so convergence of the whole sequence, not only of a subsequence or of the gradient norms, is the substance of the claim.

Formalization scope

The node type is Option (Fin n) ⊕ Inner. Sum.inl (some l) is product $l$ , indexed by Fin n, so the paper's products $1,\dots,n$ are $0,\dots,n-1$ . Sum.inl none is node $0$ . Inner is a finite type of nonleaf nodes containing root, with a parent map into Inner and a level function that encodes the $d$ levels. Every nonleaf node has a child. Prices are Fin n → ℝ, so node $0$ has no price coordinate, and all $n$ products are priced (there is no assortment decision). The conventions:

Powers $x^{\eta_j}$ are Real.rpow. Since $\eta_{\mathrm{root}}=0$ , $V_{\mathrm{root}}=1$ and it is never used. Division is Lean's, but every denominator is positive under the standing assumptions.
$R_{\mathrm{root}}$ , $\theta_l$ and $u_j$ are defined on all of $\mathbb R^n$ by the paper's formulas. The paper restricts to $\mathbb R^n_+$ , and Lemma 7.1 and Corollary 7.2 keep that hypothesis as printed.
The partial derivative in Lemma 7.1 is HasDerivAt of $x\mapsto R_{\mathrm{root}}(\mathbf p$ with $p_l:=x)$ at $p_l$ . "Stationary point" is HasFDerivAt R_root 0 p (the gradient is zero). This is the unconstrained gradient, as on p. 335, with no boundary condition, and it is the same notion in Corollary 7.2 and in the goal.
$\theta_l$ is defined by the printed product along the root-to-leaf path, and $\mathrm{An}(l,h)$ is reached by $d-h$ parent steps. $\theta_l$ is not a free parameter.
The PUPD iterates are a definition (pupd) with $\mathbf p^0=\mathbf 0$ and the max-based $t^s$ , and $t^s_{\mathrm{root}}=R_{\mathrm{root}}(\mathbf p^s)$ . The goal is not stated for an arbitrary start point or for the $u$ -based iteration.

A trivializing formalization is ruled out: convergence is Filter.Tendsto of the full sequence to a point at which HasFDerivAt holds with derivative $0$ . It is not a statement about limit points, gradient norms, or an arbitrary sequence satisfying a hypothesis.

A complete development needs derivatives of Real.rpow compositions over a finite tree, positivity of the weights and choice probabilities, and a convergence argument for the PUPD iteration. The weight and revenue recursions over a finite rooted tree could be reused for the assortment half of the same paper and for other tree-structured choice models. Contributions to any milestone, and alternative proofs of Lemma 7.1, are welcome.

Selected references

H. Li, P. Rusmevichientong, H. Topaloglu, The d-Level Nested Logit Model: Assortment and Price Optimization Problems, Operations Research 63(2):325–341, 2015. https://doi.org/10.1287/opre.2015.1355
G. Gallego, R. Wang, Multiproduct Price Optimization and Competition Under the Nested Logit Model with Product-Differentiated Price Sensitivities, Operations Research 62(2):450–461, 2014. https://doi.org/10.1287/opre.2013.1249
W. Hanson, K. Martin, Optimizing Multinomial Logit Profit Functions, Management Science 42(7):992–1003, 1996. https://doi.org/10.1287/mnsc.42.7.992
D. McFadden, Modelling the Choice of Residential Location, in A. Karlqvist et al. (eds.), Spatial Interaction Theory and Planning Models, North-Holland, 1978, 75–96 (cited as McFadden 1978 on p. 328 of Li et al.).

6 thms1 active userReviewed

Completed

Group Theory·Captain: dbenbenn

Moore: the Følner function of Thompson's group F grows faster than any tower of exponentialsResearch Paper

This mission formalizes J. T. Moore, Fast growth in the Følner function for Thompson's group F, Groups Geom. Dyn. 7 (2013) 633–651 (doi:10.4171/GGD/201; arXiv:0905.1118v7, whose page numbers are used): if Thompson's group $F$ has Følner sets at all, they are larger than any tower of exponentials.

Motivation

Whether Thompson's group $F$ is amenable is a long-standing open problem, the goal of the F-amenability mission on this platform. By Følner's criterion a finitely generated group is amenable exactly when it has Følner sets, finite sets almost invariant under translation by the generators, of every precision. Moore's theorem is unconditional: for every finite symmetric generating set there is a constant $C > 1$ such that every $C^{-n}$ -Følner set has at least $\exp_n(0)$ elements, a tower of $n$ exponentials. If $F$ is amenable, its Følner function therefore outgrows every tower, and $F$ would answer negatively Gromov's question whether some primitive recursive function dominates the Følner functions of all amenable finitely presented groups (Moore's Question 1.2, from Gromov 2008, p. 578).

Timeline.

1979: Geoghegan conjectures that $F$ is not amenable (Cannon–Floyd–Parry 1996, p. 227).
2001: Burillo, Cleary and Stein estimate word length in $F$ by the size of reduced tree diagrams (doi:10.1090/S0002-9947-00-02650-7).
2008: Gromov asks whether the Følner functions of amenable finitely presented groups are dominated by a primitive recursive function (doi:10.4171/ggd/48).
2013: Moore proves the tower lower bound for $F$ (doi:10.4171/GGD/201).

Setting

Thompson's group $F$ (CannonFloydParry.F, published) is the group of order-preserving homeomorphisms of $[0,1]$ that are piecewise linear with finitely many breakpoints, all dyadic rationals, and all slopes powers of $2$ . Moore multiplies elements as " $f$ followed by $g$ "; that group, the opposite of the group of maps under composition, is MooreF, and it acts on the right.

A finite set $A \subseteq F$ is $\varepsilon$ -Følner with respect to a finite $\Gamma$ (IsFolnerSet Γ A ε) when $\sum_{\gamma \in \Gamma} |(A \cdot \gamma) \mathbin{\triangle} A| < \varepsilon |A|$ , where $A \cdot \gamma = \{a \gamma : a \in A\}$ . The tower function is $\exp_0(n) = n$ , $\exp_{p+1}(n) = 2^{\exp_p(n)}$ (ThompsonAmenability.towerExp, published). The Følner function $\mathrm{Føl}_{F,\Gamma}(n)$ (folnerFunction) is the least size of a $1/n$ -Følner set, and $\infty$ if there is none.

The proof works with finite rooted binary trees, recorded as the sets of addresses of their leaves (IsTree), on which $F$ acts partially by acting on the addresses (treeAct), and with weighted Følner sets and marginal sets for partial actions of a group (IsWeightedFolner, IsMarginal). These are defined in the two definitions items.

Formalization targets

Goal: Theorem 1.1

For every finite symmetric generating set $\Gamma$ of $F$ there is $C > 1$ such that, for every $n$ ,

A \text{ is } C^{-n}\text{-Følner} \implies |A| \ge \exp_n(0).

The goal is the published F-amenability milestone ThompsonAmenability.exists_const_forall_isFolner_le_card, for the product of maps by composition and left translates; a milestone states the same theorem in Moore's conventions, and another states its second sentence, that $\mathrm{Føl}_{F,\Gamma}$ is not eventually dominated by any $\exp_p$ .

Milestones

Every numbered result of §§3–5 (Lemmas 3.4, 3.5, 3.9–3.12, 3.14, 3.15, 4.1, 4.2, 5.2, 5.4, 5.5, 5.7, 5.9, 5.10, 5.12, 5.13, Remark 3.8 and Claim 5.14), the unnumbered facts about trees and tree diagrams stated in §2, and the word-length bound Moore cites from Burillo, Cleary and Stein.

Significance

The result. The theorem constrains any proof that $F$ is amenable: Følner sets of $F$ , if they exist, cannot be found by any search whose size is bounded by a tower of fixed height. If $F$ is amenable, it answers Gromov's question negatively. If $F$ is not amenable, the bound is vacuous but its method, controlling how Følner sets distribute over tree diagrams, is one of the few quantitative tools on the problem.

Formalizing it. None of the paper is formalized. The general theory of §3 (partial actions, weighted Følner sets, marginal sets) applies to any group acting partially on a set and is reusable; the partial action of $F$ on binary trees is the natural model for combinatorial arguments about $F$ .

Difficulty

The difficulty is quantitative. A Følner set is defined only by an inequality between counts, and nothing in that inequality forces its elements to be large; yet the bound must hold for every Følner set, with a single constant $C$ for all $n$ , while the height of the tower grows with $n$ . Any argument can therefore afford to lose only a constant factor in the Følner constant for each level of the tower.

Formalization scope

Lean representation and conventions.

Moore's $F$ is (CannonFloydParry.F)ᵐᵒᵖ, so products and right translates match the paper; the goal is stated for CannonFloydParry.F with left translates.
Trees are finite sets of binary sequences (List Bool). Tree diagrams, their maps on sequences, equivalence and reducedness follow Moore's §2; a tree diagram describes an element of the published $F$ through the dyadic intervals of its leaves, and Moore's sentence defining $F$ as the reduced tree diagrams is a milestone.
A partial action is an Option-valued function, and the action of $F$ is defined on all finite sets of sequences; on trees it is Moore's action.
Weighted Følner sets are finitely supported non-negative functions; sums over $S$ are finite sums over their supports.

What is left out, and deviations.

Question 1.2 (Gromov's question) and Remark 5.11 (consequences for invariant measures on trees, not used in the proof) are not formalized.
In Definition 3.1, Moore's "for which all computations involving $\cdot$ are defined" can be read two ways. It is read here as asserting that $x \cdot (gh)$ is defined whenever $x \cdot g$ and $(x \cdot g) \cdot h$ are (Exel's composition law for partial actions), which Moore's proof of Lemma 3.5 uses and the action of $F$ on trees satisfies. On the weaker reading, equality only where all three are defined, Lemmas 3.5, 3.9, 3.10 and 3.12 fail (the note on the §3 definitions links p2m theorems proving this).
Definition 3.13 is read with the joining chain staying inside the set; the literal reading makes every subset of a group acting on itself by right multiplication $\Gamma$ -connected for a symmetric generating set $\Gamma$ .
Lemmas 3.5 and 3.9 assume $g \ne e$ , where the strict inequalities fail; Claim 5.14 bounds the reduced diagram, where "a tree diagram" would be vacuous. Each is explained in the milestone's statement.
The word-length bound is cited: Burillo, Cleary and Stein prove it for elements with positive normal form, and Moore applies it to all of $F$ .

What a development needs. Tree diagrams, normal forms and generation of $F$ are published and proved on this platform (the Cannon–Floyd–Parry missions on tree diagrams and the normal form and the two presentations of $F$ ); Følner's criterion is published by Garrido's first mission. New are the combinatorics of binary trees as leaf sets, the bridge between them and the published tree diagrams, and the theory of §3. Proofs of any milestone are welcome.

Selected references

J. T. Moore, Fast growth in the Følner function for Thompson's group F, Groups Geom. Dyn. 7 (2013) 633–651. doi:10.4171/GGD/201
J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996) 215–256. doi:10.5169/seals-87877
J. Burillo, S. Cleary, M. I. Stein, Metrics and embeddings of generalizations of Thompson's group F, Trans. Amer. Math. Soc. 353 (2001) 1677–1689. doi:10.1090/S0002-9947-00-02650-7
R. Exel, Partial actions of groups and actions of inverse semigroups, Proc. Amer. Math. Soc. 126 (1998) 3481–3494. doi:10.1090/S0002-9939-98-04575-4
M. Gromov, Entropy and isoperimetry for linear and non-linear group actions, Groups Geom. Dyn. 2 (2008) 499–593. doi:10.4171/ggd/48

36 thms1 active userReviewed

Bandit Algorithms Dynamic Programming Operations Research+1·Captain: mikedeng1

The Complexity of Optimal Queuing Network Control II: Restless Bandits with Deterministic Transitions are PSPACE-hardResearch Paper

Motivation

Among queueing control problems, a small class admits efficiently computable optimal policies: a single server choosing among several customer streams (Klimov 1974). These problems can be recast as multi-armed bandit problems, whose optimal policies are given by Gittins indices (Gittins 1979), and those indices are computable in polynomial time. The most studied generalization that could have extended this tractability is the restless bandit problem of Whittle (1988), in which bandits that are not played also change state and incur cost. Whittle's index heuristic and its asymptotic optimality (Weber and Weiss 1990) made the model a standard tool in scheduling, sensor management and resource allocation.

Papadimitriou and Tsitsiklis (1999) settled whether restless bandits are as easy as ordinary bandits. Their Theorem 4 shows that finding an optimal policy is PSPACE-hard, even when every transition is deterministic. The same paper shows that general queueing network control is EXP-complete (Theorem 1, the subject of a companion mission).

Setting

A restless bandit instance with deterministic transition rules consists of:

$n \ge 1$ bandits, indexed $1, \dots, n$ , on a common finite state space $S = \{1, \dots, M\}$ ;
initial states $X_1(0), \dots, X_n(0) \in S$ ;
two maps $P, Q : S \to S$ : $P$ moves the bandit that is played, $Q$ moves every other bandit;
two rational cost functions $c, d : S \to \mathbb{Q}$ ;
a rational threshold $K$ .

A policy is a map $\pi : S^n \to \{1, \dots, n\}$ . At each time $t = 0, 1, 2, \dots$ it plays the bandit $i(t) = \pi(X_1(t), \dots, X_n(t))$ ; then $X_{i(t)}(t+1) = P(X_{i(t)}(t))$ and $X_i(t+1) = Q(X_i(t))$ for every $i \ne i(t)$ . The cost at time $t$ is

C(t) = c\bigl(X_{i(t)}(t)\bigr) + \sum_{i \ne i(t)} d\bigl(X_i(t)\bigr),

and the average cost of $\pi$ is

J(\pi) = \limsup_{T \to \infty} \frac{1}{T}\sum_{t=1}^{T} C(t).

The classical multi-armed bandit is the case $Q = \mathrm{id}$ , $d = 0$ . The paper's general model has transition probability matrices; the deterministic case is a special case, so hardness for it implies hardness in general.

The decision problem RESTLESS BANDITS asks whether there is a policy $\pi$ with $J(\pi) \le K$ .

Problems are sets of instances, and instances are bit strings under a fixed binary encoding. A problem is in PSPACE if a multi-stack Turing machine decides it on every input using a number of stack cells polynomial in the input length. It is PSPACE-hard if every PSPACE language reduces to it by a polynomial-time many-one reduction: a map computable in polynomial time that sends yes-instances to yes-instances and no-instances to no-instances. It is PSPACE-complete if it is also in PSPACE.

The proof starts from an auxiliary problem, CIRCULAR-TAPE HALTING. The input is a circular tape with squares $1, \dots, n$ holding values in $\{1, \dots, A\}$ , a rule $F : \{1,\dots,A\}^2 \to \{1,\dots,A\}$ with $F(1,1) = 1$ , and an initial configuration $v(0)$ . At time $t$ the head points at the square $i \equiv t \pmod n$ , replaces its value by $F(v_{i-1 \bmod n}(t), v_i(t))$ and moves on; every other square keeps its value. The process halts if at some time every square holds $1$ . The question is whether the process halts.

Formalization targets

Goal: Theorem 4

\text{RESTLESS BANDITS with deterministic transition rules is PSPACE-hard.}

In Lean: PSPACEHard Instance.enc restlessBandits. Every language in PSPACE reduces to the decision problem in polynomial time.

Milestone 1: the circular-tape claim

\text{CIRCULAR-TAPE HALTING is PSPACE-complete.}

In Lean: PSPACEComplete TapeInstance.enc circularTapeHalting, meaning the problem is in PSPACE and PSPACE-hard. The paper claims completeness at this point. The goal uses only the hardness half.

Milestone 2: the reduction

\text{CIRCULAR-TAPE HALTING} \;\le_p\; \text{RESTLESS BANDITS (deterministic)}.

In Lean: PolyReduces TapeInstance.enc circularTapeHalting Instance.enc restlessBandits. This is the existence of a polynomial-time reduction. It is not a statement about the specific construction in the paper.

Significance

The result. Theorem 4 shows that the index theory of multi-armed bandits does not extend to restless bandits. The index-based approach has no efficient exact counterpart unless P = PSPACE, even with no randomness at all. It is why the restless-bandit literature works with heuristics (Whittle's index) and asymptotic optimality results, not exact polynomial-time algorithms. It is also one of the standard hardness results cited for average-cost Markov decision problems whose state space is a product of many small components.

Formalizing it. The paper's argument is informal. It assumes the simulation of polynomial-space machines by circular-tape processes, and it describes the bandit construction in prose. A complete formalization produces a machine-checked PSPACE-hardness proof for a controlled-dynamics problem. It also produces a reusable space-bounded computation layer on Mathlib's Turing machines, which has polynomial time but no space measure. No part of this result has a machine-checked proof yet.

Difficulty

The obvious first idea is to encode a space-bounded machine's configuration in the bandits' joint state. The difficulty is that a policy sees only the product state and plays exactly one bandit per step. The rules $P$ and $Q$ are shared by all bandits, so no bandit knows its own index. The reduction also has to be exact for the average-cost criterion. A policy that simulates the computation correctly for a long but finite time, then deviates, must not reach average cost zero. A policy that halts must reach it. Milestone 1 needs its own work as well: a polynomial-space machine has to be recast as an in-place computation on a circular tape whose local rule $F$ sees only a square and its predecessor.

Formalization scope

Conventions fixed in Lean:

Encoding. Instances are bit strings built by concatenating self-delimiting binary numerals (each bit doubled, then 01), sign-magnitude integers, (numerator, denominator) rationals, and tables listed in index order after their dimensions. The encoded length is polynomial in the instance's bit size and vice versa. Mathlib's Encodable/Nat.pair encodings are not used.
Machines. Time is Mathlib's Turing.TM2ComputableInPolyTime. PSPACE is defined here: a Turing.FinTM2 that halts on every input with the correct output bit, and in which every reachable configuration has total stack length at most $p(|\text{input}|)$ . The input stack is counted.
Decision version. The paper states only the optimization problem ("finding a policy with minimal average expected cost"). The decision version asks for $\exists \pi,\ J(\pi) \le K$ , with the rational $K$ part of the input; the paper's reduction uses $K = 0$ . Instances with $n = 0$ are no-instances.
Decision epochs and policies. Time is discrete, and $t = 0$ is the first decision. Policies are all deterministic stationary maps $S^n \to \{1,\dots,n\}$ , as on the page. The dynamics are deterministic, so $E[C(t)] = C(t)$ . The average is the real limsup of $\frac1T \sum_{t=1}^T C(t)$ . The running averages are bounded, so the limsup has no junk value.
Indices. Bandits, states, squares and values are Fin n, Fin M, Fin n, Fin A (0-based). Square $j+1$ is index $j$ , and the value $1$ is index $0$ .
Circular tape. The display on p. 303 prints " $v_i(t)$ if $i = t \bmod n$ ", which would update every square but one. The prose says that only the square under the head is updated, and the formalization follows the prose. The head is at square $i \equiv t \pmod n$ at time $t$ , so it starts at square $n$ . Well-formedness ( $n \ge 1$ , $F(1,1) = 1$ ) is part of the problem.

Excluded trivialization. The goal quantifies over every PSPACE language and asks for a reduction computable in polynomial time on a compact encoding. Exhibiting one hard instance, stating the correctness of the paper's construction for the constructed instance, or measuring against a padded encoding would not prove Theorem 4.

Theorem 4 is stated as hardness only. The proof's last sentence and the introduction say "PSPACE-complete", but membership in PSPACE is not argued in the paper.

Infrastructure. A complete development needs: closure of polynomial-time TM2 computations under composition, which gives transitivity of $\le_p$ and turns the two milestones into the goal; a space-bounded simulation of TM2 machines by circular-tape processes; and the bandit construction with an average-cost analysis of eventually periodic deterministic trajectories. The encoding and PSPACE layer can be reused by any complexity result on the platform. Contributions to the polynomial-time composition lemmas are especially welcome.

Selected references

C. H. Papadimitriou and J. N. Tsitsiklis, The Complexity of Optimal Queuing Network Control, Mathematics of Operations Research 24(2):293–305, 1999. https://doi.org/10.1287/moor.24.2.293
P. Whittle, Restless Bandits: Activity Allocation in a Changing World, Journal of Applied Probability 25A:287–298, 1988. https://doi.org/10.2307/3214163
R. R. Weber and G. Weiss, On an Index Policy for Restless Bandits, Journal of Applied Probability 27(3):637–648, 1990. https://doi.org/10.2307/3214547
J. C. Gittins, Bandit Processes and Dynamic Allocation Indices, Journal of the Royal Statistical Society B 41(2):148–177, 1979. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
G. P. Klimov, Time-Sharing Service Systems I, Theory of Probability and Its Applications 19(3):532–551, 1974. https://doi.org/10.1137/1119060

8 thms1 active userReviewed

Dynamic Programming Markov Chain Operations Research+1·Captain: mikedeng1

The Complexity of Optimal Queuing Network Control I: NETWORK OF QUEUES is EXP-completeResearch Paper

Motivation

Multiclass queueing networks model manufacturing lines, computer systems and communication networks. In these systems jobs of several types move between shared resources, and a controller decides where to send a job next (routing) and which waiting job a free resource works on (sequencing). The central design question is to find a control policy that maximizes long-run throughput. For decades this was attacked with heuristics, approximations and performance bounds (Walrand 1988; Bertsimas, Paschalidis and Tsitsiklis 1994; Kumar and Kumar 1994, all cited in the introduction of Papadimitriou and Tsitsiklis 1999). No general exact algorithm faster than solving a Markov decision process over all network states was found.

Papadimitriou and Tsitsiklis (1999) explained why. For closed networks with exponential service times, computing an optimal policy is EXP-complete, and therefore provably requires exponential time, independently of whether P equals NP. The paper describes this as, in its authors' experience, the first intractability result of this strength for a practical optimization problem that had been attacked for decades. This mission formalizes that theorem, Theorem 1 of the paper.

Setting

A network of queues has a finite set $C$ of customer classes and a finite set $S$ of servers. Each class $c$ has a single server $\sigma(c) \in S$ that can serve it, a mean service time $\mu(c) \ge 0$ and a weight $w(c) \in \mathbb{Q}$ . Service times are independent and exponentially distributed with the prescribed mean. The classes are partitioned into $D$ and $R$ . When a class- $c$ customer completes service it changes to a new class $c'$ : the controller chooses $c'$ from a given nonempty set $N(c) \subseteq C$ if $c \in D$ , and $c'$ is drawn with given rational probabilities $p_{cc'}$ if $c \in R$ . The network is closed: no customer arrives or leaves.

The state records the number of customers of each class waiting, and the class (if any) being served at each server. A policy $\pi$ makes decisions as a function of the current state. At time $0$ and at every service completion it routes the completing customer (if its class is in $D$ ), and then lets each free server either idle or start a waiting customer of one of its own classes. Service is nonpreemptive. Under a fixed policy the state evolves as a continuous-time Markov chain. Let $a^\pi_c(t)$ be the number of class- $c$ completions up to time $t$ from the given initial state. The weighted throughput is

J^\pi = \limsup_{t\to\infty} \frac1t \sum_{c\in C} w(c)\, \mathbb{E}\big[a^\pi_c(t)\big].

NETWORK OF QUEUES is the decision problem: given all these data (with the initial counts in binary) and a rational $K$ , is there a policy $\pi$ with $J^\pi > K$ ?

EXP is the class of problems solvable in time $2^{p(n)}$ for a polynomial $p$ , on inputs of length $n$ . A problem is EXP-complete if it lies in EXP and every problem in EXP reduces to it by a polynomial-time many-one reduction.

The reduction source in the paper is STOCHASTIC IN-PLACE ACCEPTANCE (SIPA). A stochastic Turing machine has nondeterministic and stochastic states, each with two continuations. Its computation tree is evaluated bottom-up, taking the maximum at nondeterministic nodes and the average at stochastic nodes, and the machine accepts if the value exceeds $1/2$ . SIPA asks, for a machine $M$ and an integer $n$ in unary, whether $M$ accepts $n$ zeroes without leaving the $n$ input squares.

Formalization targets

Goal: Theorem 1

\text{NETWORK OF QUEUES is EXP-complete.}

In Lean, EXPComplete Instance.enc networkOfQueues. The problem is in EXP, and every language $L \in \mathrm{EXP}$ reduces to it in polynomial time.

Milestones

Lemma 1: SIPA is EXP-complete.
Upper bound (proof of Theorem 1, p. 296): NETWORK OF QUEUES $\in$ EXP.
Completeness (proof of Theorem 1, pp. 296–300): SIPA $\le_p$ NETWORK OF QUEUES.

Milestones 2 and 3, Lemma 1, and the transitivity of polynomial-time reductions together give the goal.

Significance

The result. Theorem 1 separates what can be computed exactly for queueing networks from what cannot. Since EXP strictly contains P by the time hierarchy theorem, no algorithm computes optimal throughput policies for all closed exponential networks in polynomial time. Unlike NP-hardness, this is unconditional. The result justifies the literature's turn to approximations, bounds and asymptotic regimes, and it motivated the complexity analysis of restless bandits in the same paper. The stochastic-machine characterization of EXP, polynomial space with stochastic and nondeterministic states, is a tool of independent interest.

Formalizing it. The theorem is proved on paper, with a reduction that the paper itself presents in sketched form. It has no machine-checked proof. The formal work includes an exponential-time Markov decision process solver expressed as a Turing machine, a simulation of alternating polynomial-space machines by stochastic ones, and the queueing-network gadget with its optimality argument. It also produces a reusable layer: EXP and polynomial-time reductions over Mathlib's Turing.FinTM2, and a controlled continuous-time Markov chain for closed queueing networks.

Difficulty

The membership half needs an exponential-time decision procedure for the average-reward criterion. This is a multichain Markov decision process with instantaneous transitions, and it must be implemented and timed on an actual Turing machine rather than argued about informally. The hardness half is harder. The network has to encode a stochastic machine's configuration. In the paper, one customer per tape square carries the square's bit and a single test customer carries the machine's state and head position. The weights are chosen so that an optimal policy is forced to simulate the machine faithfully. The paper argues optimality through the average-reward optimality equation with explicit error bounds, and it states several steps (the normal forms of the machine, the padding to linear space) as standard. Every one of these has to be made precise. Finally, composing reductions needs the composition of polynomial-time Turing machines, which Mathlib states only as proof_wanted TM2ComputableInPolyTime.comp.

Formalization scope

All declarations are in the namespace OptimalQueuingComplexity.Network. The following conventions are fixed:

Encoding. Instances are bit strings built by concatenating self-delimiting pieces. Naturals (including customer counts) are in binary with doubled digits and a terminator, integers in sign–magnitude form, rationals as reduced numerator/denominator pairs, and tables in index order. Classes are Fin nC and servers Fin nS. SIPA's $n$ is in unary. Encodable and Nat.pair are not used: their exponential padding would make membership in EXP trivial.
Well-formedness is part of the problem, and ill-formed instances are no-instances. It requires $\sigma(c_s) = s$ for busy servers, $\mu \ge 0$ , probability vectors on $R$ , and $N(c) \ne \emptyset$ on $D$ . It also requires, as an added hypothesis, that no routing cycle consists of zero-mean classes.
Zero mean service time means instantaneous service. Simultaneous instantaneous completions are processed in increasing server index.
Decision epochs are time $0$ and every completion. Routing precedes sequencing. Policies are deterministic and stationary. The count of a class excludes the customers in service.
Throughput. $\mathbb{E}[a^\pi_c(t)]$ is an extended nonnegative real computed from the embedded chain and convolutions of exponential laws (ProbabilityTheory.expMeasure). The $\limsup$ is taken in EReal. The inequality $J^\pi > K$ is strict.
SIPA uses the binary alphabet. Leaving the input squares is rejection. Acceptance means that some finite-depth tree value exceeds $1/2$ , which equals the paper's tree value for precise machines.
EXP means TM2ComputableInTime with time bounded by $2^{p(n)}$ . Reductions are TM2ComputableInPolyTime. Hardness quantifies over every EXP language, not over one constructed instance.

A statement about the paper's specific gadget (its servers, router and weights) is a proof step and not a target. Contributions welcome beyond the targets include composition of polynomial-time machines, a decision procedure for finite average-reward MDPs, and structural facts about the throughput (finiteness under well-formedness, attainment by stationary policies).

Selected references

C. H. Papadimitriou and J. N. Tsitsiklis, The Complexity of Optimal Queuing Network Control, Mathematics of Operations Research 24(2):293–305, 1999. https://doi.org/10.1287/moor.24.2.293
A. K. Chandra, D. C. Kozen and L. J. Stockmeyer, Alternation, Journal of the ACM 28(1):114–133, 1981. https://doi.org/10.1145/322234.322243
C. H. Papadimitriou, Games Against Nature, Journal of Computer and System Sciences 31(2):288–301, 1985. https://doi.org/10.1016/0022-0000(85)90045-5
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

10 thms1 active userReviewed

Dynamic Programming Markov Chain Operations Research+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems V: The Average Cost Optimality Equation and Value Iteration for Finite State SpacesTextbook

Motivation

Average cost Markov decision chains model systems that run indefinitely and are judged by their long-run cost per step: admission and routing control in queues, inventory replenishment, machine maintenance. For a finite state space the classical tool is the average cost optimality equation (ACOE)

J + h(i) = \min_{a \in A_i}\Big\{C(i,a) + \sum_j P_{ij}(a)\,h(j)\Big\},

whose solution gives both the minimum average cost $J$ and an optimal stationary policy. To be useful the equation has to be solved numerically, and the method used in practice is value iteration: compute the minimum $n$ -horizon costs $v_n$ and extract $J$ and $h$ from their growth. This mission formalizes Sections 6.4–6.6 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037): when the minimum average cost is constant, the ACOE holds, any solution of it is optimal, and value iteration converges, provided the optimal policies are aperiodic. When they are not, a transformation of the model makes them so.

Related classical work includes Blackwell's discrete dynamic programming (1962) and Schweitzer–Federgruen's analysis of undiscounted value iteration (1977); Sennott's treatment derives the ACOE from the discounted value function $V_\alpha$ as $\alpha \to 1^-$ , which is the route that extends to countable state spaces in later chapters of the book.

Setting

A Markov decision chain (MDC) $\Delta$ has a finite state space $S$ ; in each state $i$ a finite nonempty action set $A_i$ ; nonnegative costs $C(i,a)$ ; and transition probabilities $P_{ij}(a)$ . A policy $\theta$ may use the whole history and randomize; a stationary policy $e$ always chooses $e(i) \in A_i$ in state $i$ and induces a Markov chain with transitions $P_{ij}(e) = P_{ij}(e(i))$ .

For a policy $\theta$ and initial state $i$ : $v_{\theta,n}(i)$ is the expected cost of the first $n$ steps, $V_{\theta,\alpha}(i)$ the expected $\alpha$ -discounted cost, and $J_\theta(i) = \limsup_n v_{\theta,n}(i)/n$ the average cost. The value functions are the infima over all policies: $v_n$ , $V_\alpha$ and the minimum average cost $J(i)$ . A policy is average cost optimal if $J_\theta \equiv J$ .

Section 6.2 of the book provides a stationary policy $f$ that is $\alpha$ discount optimal for all $\alpha$ close to $1$ (a Blackwell optimal policy), and Section 6.3 builds from it a relative value function $w^*$ . For a distinguished state $z$ put

h_\alpha(i) = V_\alpha(i) - V_\alpha(z), \qquad h(i) = \lim_{\alpha\to1^-} h_\alpha(i), \qquad d_n(i) = h(i) + nJ - v_n(i).

For a distinguished state $x$ the finite horizon relative value function is $r_n(i) = v_n(i) - v_n(x)$ .

A positive recurrent class $R$ of a Markov chain is aperiodic if $P^{(n)}_{ij} \to \pi_j$ for $i, j \in R$ , where $\pi$ is the steady state distribution. Assumption OPA ("optimal policies are aperiodic") requires every positive recurrent class of every average cost optimal stationary policy to be aperiodic. The aperiodicity transformation $\Delta^*$ with $0<\tau<1$ keeps states and actions, scales costs by $\tau$ , and sets $P^*_{ij}(a) = \tau P_{ij}(a)$ for $j \ne i$ , $P^*_{ii}(a) = \tau P_{ii}(a) + (1-\tau)$ .

Formalization targets

Goal: convergence of value iteration (Proposition 6.6.3)

If $J(i) \equiv J$ and Assumption OPA holds, then for any distinguished state $x$

\lim_{n\to\infty}[v_n(x) - v_{n-1}(x)] = J, \qquad \lim_{n\to\infty} r_n(i) =: r(i) \text{ exists},

$(J, r)$ solves the ACOE, and every limit point of the finite horizon optimal stationary policies is average cost optimal.

Milestones

Proposition 6.4.1: unichain structure, bounded $|V_\alpha(i) - V_\alpha(z)|$ , or pairwise reachability imply $J(i) \equiv J$ , with the implication diagram (6.26).
Theorem 6.4.2: under $J(i) \equiv J$ , $h$ exists, solves the ACOE (6.31), yields optimal policies, $|d_n| \le L$ and $v_n/n \to J$ .
Proposition 6.5.1: any finite solution $(F, r)$ of the ACOE (or of the inequality (6.36)) gives $J \equiv F$ and optimal policies, and differs from $h$ by constants on recurrent classes.
Lemma 6.6.2: on an aperiodic positive recurrent class of an optimal policy, $d_n$ converges to a constant.
Lemma 6.6.5 and Proposition 6.6.6: $\Delta^*$ has the same recurrent classes and steady states, all of them aperiodic, costs scaled by $\tau$ ; value iteration on $\Delta^*$ produces a solution $(J^*/\tau, r^*)$ of the ACOE of $\Delta$ .

Significance

The ACOE with constant $J$ is the standard certificate of optimality for finite average cost models, and Proposition 6.5.1 is what allows any numerical solution of it to be trusted. Proposition 6.6.3 is the correctness theorem of the value iteration algorithm (VIA 6.6.4 of the book), and Proposition 6.6.6 removes its one extra hypothesis at the price of a model transformation. Chapter 8 of the book runs this algorithm on a sequence of finite truncations to compute optimal policies for countable-state queueing models, so these results are the base of the book's computational method.

All results in this mission are proved in the book; none has a machine-checked proof. Existing formalizations on the platform treat average reward models under a unichain hypothesis with a single action set type; this mission assumes only a constant minimum average cost (multichain models allowed) and uses the general policy class throughout.

Difficulty

The ACOE itself is not the obstacle; convergence of $v_n(x) - v_{n-1}(x)$ is. Theorem 6.4.2 bounds $d_n$ but does not make it converge, and Example 6.6.1 of the book (a two-state periodic chain) shows that without aperiodicity $v_n(x) - v_{n-1}(x)$ oscillates. The naive argument, passing to the limit in the finite horizon optimality equation, assumes the limits exist, which is exactly what is in question. Chain structure is the obstruction: a multichain optimal policy has several recurrent classes, and the Cesàro-type convergence that suffices for the ACOE itself is weaker than the pointwise convergence value iteration needs. The policy statement is also delicate, since the finite horizon minimizers $f_n$ need not converge.

Formalization scope

The state type S is finite ([Fintype S]); actions are a type Act with per-state nonempty Finset action sets. Costs are in ℝ≥0, transition probabilities in ℝ≥0∞, and all value functions are defined in [0,∞] as infima over all history-dependent randomized policies, then converted to ℝ (they are finite for finite $S$ ).
$J$ constant is stated as $J(i) = J$ for all $i$ , with $J \in \mathbb R_{\ge 0}$ . The relative value $h$ is defined as the limit $\alpha \to 1^-$ of $h_\alpha$ , not taken as an arbitrary solution of the ACOE; Theorem 6.4.2(i) asserts the limit exists. The Blackwell optimal policy $f$ enters as a hypothesis: any stationary policy discount optimal on an interval $(\alpha_0,1)$ .
min_a is Finset.inf' over $A_i$ . Limit points of policy sequences follow Definition B.1 (a subsequence agreeing eventually in every state). Finite horizon optimal policies $f_n$ are any minimizers of $v_n(i) = \min_a\{C(i,a) + \sum_j P_{ij}(a) v_{n-1}(j)\}$ .
Aperiodicity of a class is the book's definition ( $P^{(n)}_{ij} \to \pi_j$ on the class), with $\pi_j = 1/m_{jj}$ . Assumption OPA quantifies over average cost optimal stationary policies only, not over all stationary policies.
A trivializing formalization is ruled out: $h$ , $r_n$ , $d_n$ and $v_n$ are computed from the model, not free functions constrained by the ACOE, and the ACOE conclusions are equalities of real numbers with the minimum over the actual action sets.
The model, criteria and Markov chain definitions restate those of mission IV of this series in their own namespace; they are reusable for any finite average cost result. Contributions of general Markov chain facts (convergence of $P^{(n)}$ on aperiodic classes, Cesàro limits $\frac1n\sum_t P^{(t)}$ ) are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, Wiley, 1999. https://doi.org/10.1002/9780470317037
D. Blackwell, Discrete dynamic programming, Annals of Mathematical Statistics 33 (1962), 719–726. https://doi.org/10.1214/aoms/1177704593
P. J. Schweitzer and A. Federgruen, The asymptotic behavior of undiscounted value iteration in Markov decision problems, Mathematics of Operations Research 2 (1977), 360–381. https://doi.org/10.1287/moor.2.4.360
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

13 thms1 active userReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Lost-Sales Problems with Stochastic Lead Times: Convexity Results for Base-Stock Policies: Expected Discounted Cost Is Convex in the Base-Stock LevelResearch Paper

Why base-stock levels in lost-sales systems

In many inventory systems, demand that cannot be met from stock is lost rather than backordered: a customer who finds the shelf empty buys elsewhere. For such lost-sales systems with positive lead times the optimal replenishment policy is known to be complex and to depend on the whole pipeline of outstanding orders (Karlin and Scarf, 1958; Morton, 1969). In practice, firms nonetheless use base-stock (order-up-to- $S$ ) policies, which reorder every period whatever was sold. Choosing such a policy comes down to choosing one number, the base-stock level $S$ . How easy that choice is depends on how the expected cost behaves as a function of $S$ .

Earlier work had established convexity in $S$ for backordered demand (Healy, 1992, for $(s,S)$ policies) and for lost sales with deterministic lead times (Downs, Metters and Semple, 2001). Nahmias (1979) observed in simulation that the cost surface looked convex for lost-sales systems with random lead times, but had no proof. Janakiraman and Roundy (2004) proved convexity for lost-sales systems whose lead times are stochastic but do not cross. On every sample path this holds when holding cost is charged only on the inventory position. In expectation it holds for the full cost under the lead-time model of Kaplan (1970). This mission formalizes the finite-horizon part of that paper (Sections 3–4).

Setting

Periods are indexed $n = 0, 1, \dots, N$ . The demand in period $n$ is $D_n \ge 0$ . The order placed in period $t$ has a lead time $L(t) \in \{0, 1, 2, \dots\}$ and arrives in period $t + L(t)$ . The arrival index is

\lambda_n = \max\{t : t + L(t) \le n\},

the index of the latest order that has arrived by period $n$ , with $\lambda_n = 0$ when no order has arrived (in particular $\lambda_0 = 0$ ). Assumption 1 (orders do not cross) requires $n + L(n)$ to be weakly increasing in $n$ .

Under an order-up-to- $S$ policy, the system starts with $S$ units on hand and nothing on order. Each period it orders what was sold in the previous period. With orders $q_n(S)$ , the quantities of period $n$ are:

the order $q_0(S) = 0$ and $q_{n+1}(S) = y_n(S)$ ;
the inventory on hand after receipts, $x_n(S) = S - \sum_{\lambda_n < t \le n} q_t(S)$ ;
the sales $y_n(S) = \min(x_n(S), D_n)$ ;
the end-of-period inventory on hand $i_n(S) = x_n(S) - y_n(S)$ ;
the end-of-period inventory position $\pi_n(S) = S - y_n(S)$ ;
the lost sales $l_n(S) = D_n - y_n(S)$ .

For a discount factor $0 < \alpha \le 1$ and cost rates $h_1, h_2, p \ge 0$ , the discounted cost (3.1) is

C_N(S) = \sum_{n=0}^{N} \alpha^n \big(h_1\,\pi_n(S) + h_2\,i_n(S) + p\,l_n(S)\big).

Here $h_1$ is charged on the inventory position (on hand plus in transit), $h_2$ on stock physically on hand, and $p$ on each lost unit.

In the Kaplan lead-time model (Assumption 2) the arrival index is random: $\lambda_0 = 0$ and $\lambda_n = \max(\lambda_{n-1}, n - \rho_n)$ for $n \ge 1$ , where $(\rho_n)$ is an i.i.d. sequence of nonnegative integer-valued random variables. The same dynamics, driven by $\lambda(\rho)$ , give random quantities $x_n(S,\rho)$ , $i_n(S,\rho)$ , $\pi_n(S,\rho)$ and $l_n(S,\rho)$ . $E_\rho$ is the expectation over $\rho$ with the demands held fixed.

Formalization targets

Goal: Theorem 8

Under Assumption 2, for every realization of demands $D_0, \dots, D_N \ge 0$ , every $0 < \alpha \le 1$ and all $h_1, h_2, p \ge 0$ ,

S \mapsto E_\rho\Big[\sum_{n=0}^{N} \alpha^n\big(h_1\,\pi_n(S,\rho) + h_2\,i_n(S,\rho) + p\,l_n(S,\rho)\big)\Big] \text{ is convex on } [0,\infty).

Milestones

Lemma 3. On a noncrossing sample path, for every $m \le N+1$ and every nonnegative, weakly decreasing $(\beta_n)$ , $S \mapsto \sum_{n=0}^{m} \beta_n\, q_n(S)$ is concave.
Corollary 4. On a noncrossing sample path, for every $m \le N$ and every such $(\beta_n)$ , $\sum_{n=0}^{m}\beta_n\, l_n(S)$ and $\sum_{n=0}^{m}\beta_n\,\pi_n(S)$ are convex in $S$ .
Theorem 5. On a noncrossing sample path, $\sum_{n=0}^{N}\alpha^n\big(h_1\,\pi_n(S) + p\,l_n(S)\big)$ is convex in $S$ .
Lemma 6. Under Assumption 2, $\sum_{n=0}^{m}\beta_n\, E_\rho[x_n(S,\rho)]$ is convex in $S$ for every $m \le N$ and every such $(\beta_n)$ .
Corollary 7. The same holds for $\sum_{n=0}^{m}\beta_n\, E_\rho[i_n(S,\rho)]$ .

Significance

Theorem 5 shows that, when the only holding cost is charged on the inventory position, the discounted cost of every noncrossing sample path is convex in $S$ . It therefore stays convex under any distribution of noncrossing lead times and any demand process independent of them. Theorem 8 extends convexity to storage costs on stock on hand, which matter whenever payment is due on arrival. A sample-path statement cannot do this. On a sample path the extension fails: the paper's Example 1 exhibits a concave kink at $S = 1$ when $h_2 > 0$ . Both results make the choice of the best base-stock level a one-dimensional convex minimization, so bisection or simulation-based search methods are guaranteed to converge to a global optimum. The paper's Example 2 shows that noncrossing cannot be dropped.

The results are proved in the paper. As far as is known, none has a machine-checked proof. A formalization adds a precise, reusable model of periodic-review lost-sales dynamics with stochastic lead times, and a checked account of exactly which hypotheses (noncrossing, $h_2 = 0$ on sample paths, the Kaplan structure in expectation) each convexity claim needs.

Difficulty

Individual per-period quantities are not convex: $q_n(S)$ , $x_n(S)$ , $i_n(S)$ and $\pi_n(S)$ are piecewise linear with slopes in $\{0,1\}$ and are neither convex nor concave in $S$ . The obvious approach, proving each term of the cost convex and summing, therefore fails. Convexity appears only in the weighted sums, and only for nonnegative, weakly decreasing weights. The recursion defining $x_n$ refers back to earlier orders through a window $(\lambda_n, n]$ that moves with the lead-time path, so an induction on $m$ has to carry a family of weight sequences rather than one fixed sum.

In expectation, the storage-cost term $\sum_n \beta_n\, i_n$ is not convex path by path. Convexity of its expectation depends on the distributional structure of the Kaplan model, namely that the lead time of the order placed in period $n$ is independent of the state of the system at that time. Stating this correctly requires a genuine probability space, not a sample-path argument.

Formalization scope

Model. One definition of the dynamics, parametrised by an arrival-index path $\lambda : \mathbb{N} \to \mathbb{N}$ , a demand path $D : \mathbb{N} \to \mathbb{R}$ and a real $S$ (orderQty, onHand, sales, endOnHand, invPosition, lostSales). The sample-path results use arrivalIndex L (via Nat.findGreatest). The Kaplan results use kaplanIndex ρ, the recursion of Assumption 2 with $\lambda_0 = 0$ . The discounted cost (3.1) is discountedCost.
Hypotheses. Assumption 1 is MonotoneOn (fun n => n + L n) (Set.Iic N). Demands satisfy $D_n \ge 0$ for $n \le N$ . Weight sequences are β : ℕ → ℝ with 0 ≤ β n and Antitone β. Costs satisfy $0 < \alpha \le 1$ and $h_1, h_2, p \ge 0$ , the paper's Section 3 standing assumptions. "Increasing" and "decreasing" are weak, as the paper states.
Domain. Every convexity or concavity claim is ConvexOn ℝ (Set.Ici 0) / ConcaveOn ℝ (Set.Ici 0): the base-stock level is an initial stock, $S \ge 0$ .
Expectation. $(\Omega, P)$ is a probability space. $\rho : \mathbb{N} \to \Omega \to \mathbb{N}$ has measurable coordinates, iIndepFun ρ P, and IdentDistrib (ρ n) (ρ 0) P P for all $n$ . $E_\rho[f]$ is the Bochner integral $\int f(\lambda(\rho(\omega)))\,dP(\omega)$ . For $S \ge 0$ the integrands are bounded and depend on finitely many coordinates, so they are integrable and the integral is the paper's expectation. Measurability of $\rho$ is the field's standing convention.
Ruled out. The Kaplan statements are about the Kaplan index of an i.i.d. sequence, not about an arbitrary nondecreasing arrival process. The sample-path statements carry the noncrossing hypothesis, without which they are false. The convexity domain is the half-line, not a finite or degenerate set.
Needed infrastructure. Convexity and concavity of finite sums and minima (Mathlib's ConvexOn/ConcaveOn), integrals of bounded functions of finitely many independent discrete variables, and the independence and identical distribution facts of the Kaplan model. The dynamics and the Kaplan index are reusable for any further analysis of base-stock lost-sales systems, including the paper's infinite-horizon results. Proofs of the milestones in any order are welcome, as are auxiliary lemmas identifying the Kaplan index as the arrival index of a noncrossing lead-time path.

Selected references

G. Janakiraman and R. O. Roundy, Lost-Sales Problems with Stochastic Lead Times: Convexity Results for Base-Stock Policies, Operations Research 52(5):795–803, 2004. https://doi.org/10.1287/opre.1040.0130
R. S. Kaplan, A Dynamic Inventory Model with Stochastic Lead Times, Management Science 16(7):491–507, 1970. https://doi.org/10.1287/mnsc.16.7.491
S. Karlin and H. Scarf, Inventory Models of the Arrow–Harris–Marschak Type with Time Lag, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
T. E. Morton, Bounds on the Solution of the Lagged Optimal Inventory Equation with No Demand Backlogging and Proportional Costs, SIAM Review 11(4):572–596, 1969. https://doi.org/10.1137/1011090
S. Nahmias, Simple Approximations for a Variety of Dynamic Leadtime Lost-Sales Inventory Models, Operations Research 27(5):904–924, 1979. https://doi.org/10.1287/opre.27.5.904
B. Downs, R. Metters and J. Semple, Managing Inventory with Multiple Products, Lags in Delivery, Resource Constraints, and Lost Sales: A Mathematical Programming Approach, Management Science 47(3):464–479, 2001. https://doi.org/10.1287/mnsc.47.3.464.9775
R. Ehrhardt, (s, S) Policies for a Dynamic Inventory Model with Stochastic Lead Times, Operations Research 32(1):121–132, 1984. https://doi.org/10.1287/opre.32.1.121

10 thms1 active userReviewed

Functional Analysis·Captain: savarin

Does the sharp diagonal Hlawka constant work for all complex matrices when p ≥ 256?Open Problem

The Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.

Does the sharp diagonal constant work for general matrices?

For every real $p\ge256$ , the optimal Hlawka constant for complex diagonal matrices is already proved in Lean. This mission asks whether that same constant works for all complex matrices, including rectangular ones. The statement is a conjecture. Accepted diagonal result

Audenaert and Kittaneh's Problem 7 asks for the best constant in the Schatten-norm setting, if one exists. Existence of some finite dimension-independent constant for every real $p>1$ is already settled by the project's Lean theorem. The task here is to establish the specified sharp candidate in the range $p\ge256$ . Audenaert–Kittaneh, §8.2, proved existence result

Definitions and the goal

For a complex matrix $A$ with singular values $s_i(A)$ , its Schatten norm is

N_p(A)=\left(\sum_i s_i(A)^p\right)^{1/p}.

There is no normalization by dimension. For three matrices of the same shape, define

\Delta_3=N_p(A)+N_p(B)+N_p(C)-N_p(A+B+C),

\Delta_2=2\bigl(N_p(A)+N_p(B)+N_p(C)\bigr) -N_p(A+B)-N_p(A+C)-N_p(B+C).

Formal Schatten-norm definition

The shared cyclic candidate is

K_p=\sup_{t\in[1/2,2]} \frac{3(t^p+2)^{1/p}-3^{1/p}|2-t|} {6(t^p+2)^{1/p}-3(2|1-t|^p+2^p)^{1/p}}.

The fraction is the deficit ratio for the coordinate triple $(-t,1,1),(1,-t,1),(1,1,-t)$ . For $p>1$ , its denominator is positive on the displayed interval and the supremum is attained. Cyclic definitions and attainment

The goal asks whether $\Delta_3\le K_p\Delta_2$ for every real $p\ge256$ and every triple of complex matrices of every finite shape. One constant for each exponent must work across all dimensions and triples. The endpoint 256, noninteger exponents, zero dimensions, singular and zero matrices, unequal norms and zero pair deficit are included.

Lean states the goal for complex-linear maps between any two finite-dimensional complex inner-product spaces, allowing different dimensions. No positivity, self-adjointness, commutativity or common diagonalization assumption is imposed.

Why the diagonal proof does not settle this

The singular values determine a matrix's own norm. However, the separate singular-value lists of three matrices do not determine the norms of their pair sums and total sum. The diagonal theorem therefore does not supply the seven matrix norms needed in this inequality. Their relative directions matter as well.

The existing existence theorem supplies a constant, but does not identify it with $K_p$ . A proof here needs the exact cyclic constant. A proof only for even integer exponents or a restricted class of matrices would not settle this goal.

What a resolution would establish

If the conjectured bound holds, it is automatically optimal uniformly over all finite matrix shapes: diagonal three-dimensional examples already require at least $K_p$ . Thus the missing step is that this constant works for arbitrary matrices. A counterexample would show that the diagonal constant is insufficient somewhere in the stated range. Cyclic lower bound, diagonal Schatten identity

Either outcome addresses this range of exponents; it would not settle the optimal general-matrix constant for every $1<p<256$ .

The foundation mission establishes the optimal diagonal constant for every real $p\ge256$ . The cutoff-90 mission has since extended the diagonal result in Lean to every real $p\ge90$ . The diagonal campaign invites contributors to lower that cutoff below 90.

This mission keeps $p\ge256$ and asks whether the same optimal constant works for arbitrary complex matrices, including rectangular ones. It can be pursued independently of improvements to the diagonal cutoff.

Its three linked milestones are already-proved background: existence, the sharp diagonal result, and the diagonal norm identity. The main general-matrix goal remains open. No complete proof is supplied for it.

References

K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, 2012, §8.2, Problem 7. arXiv:1201.5232
Ezzeri Esa and contributors, Hlawka–Schatten inequalities, Lean source repository, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Existence and diagonal libraries

Established results on Prove2Me

98 thms1 active userReviewed

Numerical Analysis Operations Research Optimization·Captain: mikedeng1

Minimization Methods for Non-Differentiable Functions IX: Convergence of the r-Algorithm with Exact Directional MinimizationTextbook

Motivation

The r-algorithm of N. Z. Shor is a variable-metric method for minimizing functions that are not differentiable everywhere, such as maxima of smooth functions, penalty functions and Lagrangian dual functions of integer and decomposition problems. It combines a subgradient step with a space dilation along the difference of two successive almost-gradients, and the book reports it competitive with the best variable-metric and conjugate-gradient methods on "gully"-shaped test problems (Shor 1985, §3.6, pp. 68–77). Its convergence theory is limited. Section 3.7 of Shor's book gives a convergence proof only for an idealized version with exact directional minimization, on a class of piecewise smooth functions, and the book itself calls a weakening of the assumptions and rate estimates desirable (p. 85). This mission formalizes that section.

Timeline. Shor and Zhurbenko introduced the r-algorithm in 1971 (Kibernetika, no. 3, 51–59). Shor analysed the convergence of its exact-line-search version in 1975 (Kibernetika, no. 4, 48–53). Section 3.7 of the 1979 Russian monograph, translated in 1985, gives that analysis for piecewise smooth functions. The book states on p. 85 that weaker assumptions and rate estimates would be desirable.

Setting

Let $E_n$ be $n$ -dimensional Euclidean space with inner product $(x, y)$ , $n \ge 1$ . For a unit vector $\xi$ and $\alpha > 0$ the operator of space dilation is $R_\alpha(\xi)x = x + (\alpha - 1)(x, \xi)\xi$ .

Widths. For a compact convex set $W$ and a unit vector $\eta$ , the width in direction $\eta$ is $d_\eta(W) = \max_{x \in W}(\eta, x) - \min_{x \in W}(\eta, x)$ . The width is $d(W) = \min_{\|\eta\| = 1} d_\eta(W)$ and the diameter is $D(W) = \max_{\|\eta\| = 1} d_\eta(W)$ . With $e_\rho(W) = \inf_{z \in W}|(\rho, z)|$ put $K_\rho(W) = d_\rho(W)/e_\rho(W)$ (or $+\infty$ when $e_\rho(W) = 0$ ) and $p(W) = \inf_{\|\rho\| = 1} K_\rho(W)$ .

The class $K$ . $E_n$ is partitioned into closed sets $\bar D_1, \dots, \bar D_m$ , each the closure of its interior, whose interiors are disjoint and homeomorphic to an open ball or open halfspace; $f_i$ is continuously differentiable on an open set containing $\bar D_i$ ; and $f = f_i$ on $\bar D_i$ . At a point $x$ , the set of almost-gradients $G_f(x)$ is the set of gradients $\nabla f_i(x)$ of the pieces with $x \in \bar D_i$ . For $\delta, \varepsilon > 0$ , $\bar P_{\delta,\varepsilon}(x)$ is the closed convex hull of all $G_f(y)$ , $\|y - x\| < \delta$ , together with the $\varepsilon$ -balls around the elements of $G_f(x)$ .

The $r(\alpha)$ -algorithm. Fix $\alpha > 1$ , $\beta = 1/\alpha$ . Start from $x_0$ , $\tilde g_0 = 0$ and a nonsingular $B_0$ . At iteration $k + 1$ choose $g_f(x_k) \in G_f(x_k)$ with $(B_k^* g_f(x_k), \tilde g_k) \le 0$ ; set $g_k^* = B_k^* g_f(x_k)$ , $r_k = g_k^* - \tilde g_k$ , $\xi_{k+1} = r_k/\|r_k\|$ , $B_{k+1} = B_k R_\beta(\xi_{k+1})$ , $\tilde g_{k+1} = R_\beta(\xi_{k+1}) g_k^*$ , and $x_{k+1} = x_k - h_{k+1}B_{k+1}\tilde g_{k+1}$ with $h_{k+1} \ge 0$ such that $f$ does not increase along the step and some almost-gradient at $x_{k+1}$ makes a non-acute angle with $\tilde g_{k+1}$ in the transformed metric. The standing assumption is $f(x) \to +\infty$ as $\|x\| \to \infty$ (3.50).

Formalization targets

Goal: convergence to an isolated local minimum (Theorem 3.13)

Assume (3.50) and $\|x_{k+1} - x_k\| \to 0$ (3.52). If $x^*$ is an isolated local minimum, the component of $\{x : f(x^*) \le f(x) \le f(x_0)\}$ containing $x_0$ also contains $x^*$ , and no other point $z$ of that component has linearly dependent $G_f(z)$ , then

\lim_{k \to \infty} x_k = x^* .

Milestones

Lemma 3.2 (p. 80): for $B = SO$ with minimum eigenvalue $\lambda(B)$ of $S$ , $\lambda(B)d(W) \le d(BW) \le \lambda(B)D(W)$ .
Lemma 3.3 (p. 80): for $z_1, z_2 \in W$ , $0 < \beta \le 1$ and $\gamma = \|z_1 - z_2\|/d(W) \ge 1$ ,

d\Big(R_\beta\big(\tfrac{z_1 - z_2}{\|z_1 - z_2\|}\big)W\Big) \ge \frac{d(W)}{\sqrt{1 + (1-\beta^2)/(\beta^2\gamma^2)}} .

Theorem 3.11 (p. 82): for every $\sqrt[n]{\beta} < v < 1$ , $\varepsilon, \delta > 0$ and $r \ge 1$ there is $\bar k > r$ with

p\big(\bar P_{\delta,\varepsilon}(x_{\bar k})\big) \ge \sqrt{\frac{v^2\sqrt[n]{\alpha^2} - 1}{\alpha^2 - 1}} .

Theorem 3.12 (p. 84): the level set $\{f = f_\infty\}$ , $f_\infty = \lim_k f(x_k)$ , contains a point $x^*$ with $G_f(x^*)$ linearly dependent.

Significance

Theorem 3.13 is the only convergence theorem the book gives for the r-algorithm. Theorems 3.11 and 3.12 hold for any function of the class $K$ , convex or not, and say that iterates of the exact version cannot stall at a point where the local almost-gradients are linearly independent: linear dependence of $G_f(x)$ is a generalized stationarity condition that includes $0 \in \operatorname{conv} G_f(x)$ . Lemmas 3.2 and 3.3 are statements about widths of convex bodies under linear maps and single dilations, and apply to any analysis of space-dilation methods, including the ellipsoid method.

All four results and the goal are proved in the book, the goal as a corollary without a written proof. None of them is formalized. The formalization adds a machine-checked definition of the class $K$ and of the algorithm as a relation on sequences covering every admissible choice of almost-gradients and stepsizes, a verified proof of the book's argument, and a check of the corollary step, which the book leaves to the reader.

Difficulty

The obvious argument for descent methods is that the function value drops by a fixed amount at every step unless the gradient is small. That argument fails here. The r-algorithm can make null steps, with $x_{k+1} = x_k$ while $B_k$ and $\tilde g_k$ change, and its steps are measured in a metric that degenerates as the dilations accumulate ( $\det B_k = \beta^k \det B_0$ ). A small step does not certify near-stationarity, and a large accumulated dilation does not certify progress.

The difficulty is to relate the geometry of the transformed almost-gradient sets $B_k^*\bar P_{\delta,\varepsilon}(x_k)$ to the decay forced on $B_k$ . This needs width estimates for convex bodies under linear maps and single dilations, which Mathlib does not have. Theorem 3.12 also needs a uniform lower bound, near a compact level set, on the Gram determinants of the piece gradients, and the book's proof of it is only sketched. Theorem 3.13 is stated as a corollary with no proof at all. Deriving it requires showing that the iterates cannot leave the prescribed component of $\{f(x^*) \le f \le f(x_0)\}$ , and that their accumulation points reduce to $x^*$ .

Formalization scope

$E_n$ is EuclideanSpace ℝ (Fin n) with $n \ge 1$ ; operators are continuous linear maps; $B_k^*$ is the adjoint. $K_\rho$ and $p$ are valued in $[0, +\infty]$ , so $K_\rho(W) = +\infty$ is represented exactly. Widths are sInf/sSup of support values, equal to the book's minima and maxima on nonempty compact sets.
A function of class $K$ is given with its representation (pieces, open domains, smooth $f_i$ ), and $G_f(x)$ is the set of gradients of the incident pieces, as on p. 79. Linear dependence of $G_f(x)$ is the negation of linear independence of that set.
A run of the algorithm is a predicate on sequences $x_k, \tilde g_k, B_k, g_f(x_k), h_{k+1}$ ; every theorem holds for every run. Step (3) divides by $\|r_k\|$ , so $r_k \ne 0$ is part of the run: a run that reaches a point where no admissible choice gives $r_k \ne 0$ has no continuation, as in the book. The stepsize $h_{k+1} = \operatorname{argmin}$ is one admissible choice, not the definition.
The standing assumption (3.50) is a hypothesis of Theorem 3.11 as well as of 3.12 and 3.13, because the book imposes it for the rest of the section on p. 79.
In Lemma 3.3, $\beta > 0$ is added (the bound divides by $\beta^2$ ). "Body" means nonempty interior. An isolated local minimum is a local minimum with a neighbourhood containing no other local minimum.
Runs exist, so the hypotheses are not vacuous. For $f(t) = |t_1| + 2|t_2|$ (four quadrant pieces), started at the minimizer $x_0 = 0$ with null steps, one can choose $g_f(x_{k+1}) = -g_f(x_k)$ at every step, and $0 \notin G_f$ keeps $r_k \neq 0$ . A formalization under which no infinite run exists would make every theorem vacuous. The run predicate also forbids the degenerate reading $h_{k+1} < 0$ , under which the monotonicity condition (a) would hold vacuously on an empty segment.
Needed infrastructure: widths of compact convex sets under linear maps (via the singular values of $B$ ), the effect of a rank-one dilation on widths, determinant bounds for products of dilations, and Gram-determinant continuity. The first three apply to any space-dilation method and are welcome as independent lemmas.

Selected references

N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer 1985, §3.7, pp. 77–85. doi:10.1007/978-3-642-82118-9
N. Z. Shor, N. G. Zhurbenko, A minimization method using the operation of space dilation in the direction of the difference of two successive gradients, Kibernetika (Kiev), no. 3, 51–59, 1971 (listed in the bibliography of Shor 1985; no online copy known).
N. Z. Shor, The analysis of convergence of a gradient type method with space dilation in the direction of the difference of two successive gradients, Kibernetika (Kiev), no. 4, 48–53, 1975 (listed in the bibliography of Shor 1985; no online copy known).

7 thms1 active userReviewed

Analysis Geometry & Topology·Captain: Tamas Fulop

Moving Sofa ProblemOpen Problem

Motivation

The question of the largest area that can be moved around a corner has been studied since the late 1960s. Leo Moser posed it in 1966, and F. H. Hammersley gave the lower bound $\pi/2+2/\pi\approx2.2074$ and the upper bound $2\sqrt{2}\approx2.828$ in 1968. Joseph Gerver constructed a shape of area approximately $2.2195$ in 1992 and described four constants $A$ , $B$ , $\varphi$ , $\theta$ satisfying four equations, from which the shape is built. Dan Romik rewrote those equations in exact form as equations (1)-(4) in 2018 and reported high-precision values of the constants. Jineon Baek proved in 2024 that Gerver's shape is optimal: no larger shape can be moved around the corner. The proof was autoformalized in Lean 4 by Dean Cureton and AI agents in 2026, as the repository deancureton/MovingSofa, building on Dawid Trela's formalization of Gerver's constants and motion, Jonathan Ho's Brunn-Minkowski development, the Jordan-curve developments of R. Kirov and the TauCeti project, and Google DeepMind's formal-conjectures statement.

Timeline: Moser poses the problem (1966); Hammersley gives the $\pi/2+2/\pi\approx2.2074$ lower bound and the $2\sqrt{2}\approx2.828$ upper bound (1968); Gerver exhibits the $2.2195$ shape and its differential equations (1992); Romik gives the exact equations and numerics (2018); Baek proves optimality (2024, arXiv:2411.19826); Cureton et al. complete a Lean 4 proof of optimality, existence and uniqueness of the constants, and movability of Gerver's shape (2026).

Setting

Work in the plane $\mathbb{R}^2$ . The hallway is $(-\infty,1]\times[0,1]\cup[0,1]\times(-\infty,1]$ , the union of its horizontal and vertical sides. A moving sofa is a nonempty closed connected set $s$ in the horizontal side together with a continuous path $m$ of plane isometries indexed by the unit interval, starting at the identity, keeping the image of $s$ inside the hallway at all times, and ending with the image inside the vertical side. Motions take values in the full isometry group $E(2)$ ; continuity together with $m(0)=\mathrm{id}$ forces the path to lie in the orientation-preserving component. The sofa constant is the supremum, in the extended nonnegative reals, of the areas $\mathrm{volume}(s)$ over all moving sofas. The supremum is finite, at least $11/5$ , and attained.

Gerver's shape is defined from a rotation path. For constants $A$ , $B$ , $\varphi$ , $\theta$ , let $r$ be the piecewise function with breakpoints $\varphi$ , $\theta$ , $\pi/2-\theta$ , $\pi/2-\varphi$ from Romik's Theorem 2, let $x$ and $y$ be its cosine and sine integrals, and let $p$ be the associated translation path. The sofa for those constants is the intersection over angles in $[0,\pi/2]$ of the correspondingly rotated and translated hallways, with the endpoints using the horizontal and vertical sides. The four equations ABphiThetaSpec cut out the constants. They have exactly one solution with $0\le\varphi\le\theta\le\pi/4$ and $0\le A$ , $0\le B$ . The same Lean development uses the identical notation as the formal statements, so prose and code read as one document.

Formalization targets

Goal: optimality of Gerver's sofa

For every $A$ , $B$ , $\varphi$ , $\theta$ satisfying ABphiThetaSpec,

\mathrm{sofaConstant} = \mathrm{volume}(\mathrm{gerversSofaWith}(A,B,\varphi,\theta)).

The goal leaves unfixed which solution of the spec is used; by uniqueness all choices give the same shape up to the proved identification, so this is the stable form of Baek's Theorem 1.1. It asserts that the supremum equals the area of Gerver's shape, hence that no moving sofa has larger area and that the supremum is attained.

Supporting targets

\exists!\,(A,B,\varphi,\theta),\ \mathrm{ABphiThetaSpec}(A,B,\varphi,\theta).

\forall\,A,B,\varphi,\theta,\ \mathrm{ABphiThetaSpec}(A,B,\varphi,\theta)\implies \exists\,m,\ \mathrm{IsMovingSofa}(\mathrm{gerversSofaWith}(A,B,\varphi,\theta),m).

The first is Gerver's Theorem 2 in Romik's equation form on the closed domain. The second says every such shape admits a hallway motion. Together they supply the constants and the witness that the supremum is attained. The live mission records a root sketch composing the upper-bound half (every moving sofa is bounded by Gerver's area) with the movability witness into the supremum equality.

Significance

The result itself closes a problem open since 1966. It identifies the maximum area, shows the maximum is attained by an explicit shape, and determines that shape from four equations whose solution is unique. Consequences include the numerical enclosure $11/5\le\mathrm{volume}\le\infty$ proved by interval arithmetic, the finiteness of the supremum, and the reduction of future improvements to the analysis of the functional $Q$ on caps. Without it the exact maximum remains unknown.

Formalizing it adds a machine-checked proof that makes no classical area assumption: the Green-type curve-area identity and the Minkowski-type mixed-area facts quoted by the paper are proved, the paper's 11 proof gaps and 33 misprints are repaired, and the numerical certificate is kernel-checked. The hallway, motion, cap, convex-body, and surface-measure infrastructure is reusable for related isoperimetric and kinematic formalizations. Status honesty: the underlying paper proof is complete and has been formalized in the source repository; on this platform the three statements above are open targets awaiting proofs, and the uniqueness of the maximizer up to rigid motion remains open and is not part of this mission.

Difficulty

The obvious argument bounds the area of an arbitrary sofa by the area of a circumscribed cap, but caps need not satisfy the injectivity condition that makes the functional $Q$ an upper bound, and $Q$ need not be concave on the full space of caps. Maximizing sequences of polygons need not converge to a sofa, and limits need not be connected or attain the supremum. The naive idea of taking a supremum over all connected closed sets and extracting a convergent subsequence fails until compactness of motions, closedness of the moving-sofa predicate, and a balanced maximum with rotation angle $\pi/2$ are established. Each step fails for general sets and only holds after the polygon approximation and monotonization constructions.

Formalization scope

Lean represents the plane as EuclideanSpace ℝ (Fin 2) with its standard orientation, hallway sides as explicit sets, motions as I → E(2) where E(2) is ℝ² ≃ᵃⁱ[ℝ] ℝ² with the topology induced from continuous maps, and area as MeasureSpace.volume. The supremum is in ℝ≥0∞. Statements target the c5ea003 (Lean v4.30.0) environment, an older supported revision against which the development was verified locally. The spec uses non-strict inequalities, which makes uniqueness stronger than the strict-inequality literature form. The functions $r$ , $x$ , $y$ , $p$ take the constants as explicit arguments rather than reading global chosen constants, so the definition bundle stays independent of the existence proof; given uniqueness this implies the source statements. Boundedness and measurability are not assumed; every moving sofa is proved compact in the source development. A submission that drops closedness or connectedness, that allows a discontinuous motion, or that hard-codes the numerical value $2.2195$ instead of proving equality with the volume of the defined shape, does not satisfy the statements. Contributions welcome: direct proofs of the three targets, sharper enclosures of the volume, and reusable hallway and motion lemmas. Out of scope: uniqueness up to congruence, the $11/5$ certificate details beyond the stated lower bound, and the 20 unformalized numbered environments listed in the source NOTES.md that none of the three targets depends on.

Selected references

Jineon Baek, Optimality of Gerver's Sofa, arXiv:2411.19826, 2024. https://arxiv.org/abs/2411.19826
Joseph L. Gerver, On moving a sofa around a corner, Geometriae Dedicata 42 (1992), 267-283.
Dan Romik, Differential equations and exact solutions in the moving sofa problem, Experimental Mathematics 27 (2018), 316-330. https://arxiv.org/abs/1606.08111
Dean Cureton et al., MovingSofa: Autoformalization of Baek's solution, 2026. https://github.com/deancureton/MovingSofa
Google DeepMind, formal-conjectures, FormalConjectures/Wikipedia/MovingSofa.lean at ddfbaf90. https://github.com/google-deepmind/formal-conjectures
Dawid Trela, GerverSofaLean v1.1.0. https://github.com/dawidmtrela-dotcom/GerverSofaLean

46 thms1 active userReviewed

Theoretical Computer Science·Captain: Goku

QMA Strong Error Reduction with No Witness-Length IncreaseResearch Paper

Motivation

A QMA verifier receives a quantum witness and checks it with a circuit generated efficiently from the input. An acceptance probability separated by an inverse-polynomial gap is enough to define the class, but applications often need the probability of a wrong answer to be exponentially small. Repeating the verifier on many supplied witness registers achieves this error reduction while allowing the witness to grow. Marriott and Watrous proved the stronger statement that the same error reduction can be obtained without increasing the number of witness qubits Quantum Arthur–Merlin Games, Section 3.

The existing Lean development verifies the copy-based theorem, including soundness for witnesses entangled across the copies, and constructs a uniform circuit family with polynomial resources. This mission asks for the separate witness-preserving theorem. The paper already proves that mathematical statement; the open work here is its formalization in the stated QMA circuit model.

Setting

At each input length $n$ , a verifier has $m(n)$ witness qubits, a finite work register, a designated output wire, and a quantum circuit. A uniformly generated family has a polynomial-time classical procedure that emits the complete circuit description, including the witness and work-register sizes. On yes-instances, some normalized witness makes the verifier accept with probability at least $a(n)$ . On no-instances, every normalized witness is accepted with probability at most $b(n)$ . The thresholds satisfy $0\le b(n)\le a(n)\le1$ and $a(n)-b(n)\ge1/q(n)$ for a polynomial $q$ .

The existing formalization represents witnesses as complex amplitude functions on bit strings, requires normalization explicitly, and uses layered circuits over its specified finite gate set. It also represents efficiently available real thresholds by polynomial-time procedures that output dyadic approximations. These are part of the formal statement's interface and must be made visible to users of the mission.

Target

For every polynomial error exponent $r$ and every source verifier satisfying the conditions above, construct a uniformly generated, well-formed, polynomial-resource verifier for the same language, with completeness at least $1-2^{-r(n)}$ and soundness at most $2^{-r(n)}$ , while keeping the witness count exactly $m(n)$ at every input length:

m_{\mathrm{new}}(n)=m_{\mathrm{old}}(n).

This is the witness-preserving strong error-reduction result of Marriott and Watrous (Theorem 4). The existing copy-based result corresponds to the weaker QMA class inclusion in Theorem 3 and will be linked as a proved background result. The mission goal must state the witness-count equation explicitly so that a copy-based amplifier cannot satisfy it.

Significance

Witness-preserving amplification lets a QMA protocol demand much stronger reliability without asking the prover for a longer message. That matters whenever witness size is itself a resource being compared or bounded. The copy-based theorem shows that the QMA class is robust under error reduction, but does not establish this fixed-message guarantee.

Formalizing the stronger result would add a reusable account of a verifier that reuses one witness, proves soundness for every normalized input state, and compiles its behavior into an ordinary uniform circuit family. Those components can support later formalizations that reason about repeated quantum verification under a fixed witness budget.

Difficulty

The completed copy-based proof uses three independent verifier blocks in each amplification round and bounds arbitrary entangled witnesses across those blocks. Its circuit resource analysis therefore allows the witness count to grow. A witness-preserving argument cannot use that construction. It must analyze repeated verification on one register and establish exponentially small error without assuming the input witness has a special spectral form. The formal circuit model currently exposes final-output measurements; any additional measurement behavior used in the analysis must be justified in that model and shown implementable by a finite, uniformly generated circuit.

The central audit point is the exact witness-length equation. A theorem that merely returns another polynomial-size witness, or that changes the source verifier's witness definition, is a useful class-level result but does not prove this mission's target.

Formalization scope

The goal is parameterized by input-length-dependent completeness and soundness thresholds with an inverse-polynomial gap, and by a polynomial target exponent. Every witness quantifier is over normalized states. The output verifier must satisfy the same well-formedness and polynomial-resource conditions as the completed copy-based development. The platform statement uses its existing ShiClassQMAU.UniformQMA circuit-family encoding, which includes the witness and ancilla counts separately. A final proof should be kernel checked with only Lean's standard logical axioms and should not assume an amplification transducer or an unproved measurement lemma.

The paper quantifies over the class poly of unary-time constructible functions. This proposal represents the gap denominator and target exponent as literal Polynomial ℕ values, matching the checked copy-based development. It therefore formalizes a polynomial-parameter instance of Theorem 4 rather than the paper's full function-class generality. The threshold functions are supplied by polynomial-time dyadic approximators in place of the paper's informal efficient-computation convention. These interface choices are explicit in the Lean goal and should not be read as a proof of the broader formulation.

The local copy-based proof is complete and audited, but it has not yet been transplanted to Prove2Me. Its publication is preparatory work for this mission, not evidence that the witness-preserving goal is already solved. The proposal should reference the published copy-based endpoint and include only a few substantial milestones, so each item is meaningful to audit.

Selected references

C. Marriott and J. Watrous, Quantum Arthur–Merlin Games, Computational Complexity 14 (2005), Section 3, Theorems 3 and 4. Paper.
A. Kitaev, A. Shen, and M. Vyalyi, Classical and Quantum Computation, Graduate Studies in Mathematics 47, American Mathematical Society (2002), Section 14.2, cited by Marriott and Watrous for the copy-based amplification proof.

3 thms1 active userReviewed

Number Theory·Captain: Lucas

Brocard's Conjecture: Four Primes Between Consecutive Prime SquaresOpen Problem

Motivation

For $n \ge 1$ let $p_n$ denote the $n$ -th prime. Brocard's conjecture, named after Henri Brocard, asserts that for every $n \ge 2$ there are at least four primes strictly between $p_n^2$ and $p_{n+1}^2$ (Wikipedia). It belongs to the family of "primes between consecutive squares" problems together with Legendre's conjecture, and it is a concrete, elementary-looking question about short-interval prime distribution that remains open.

Timeline

Early 20th century — Brocard states the conjecture.
2023 — L. A. Ferreira (arXiv:2307.08725) proves that the conjecture holds for all sufficiently large $n$ .

Setting

Primes are listed in increasing order. In the Lean development the list is 0-indexed: Nat.nth Nat.Prime k is the $k$ -th prime counting from $0$ , so nth 0 = 2, nth 1 = 3, nth 2 = 5, and so on. For an index $n$ write $\mathrm{prev} =$ n.nth Nat.Prime and $\mathrm{next} =$ (n+1).nth Nat.Prime, two consecutive primes. The quantity of interest is

\#\{\, q \text{ prime} : \mathrm{prev}^2 < q < \mathrm{next}^2 \,\}.

Target

Milestone (Ferreira): for all sufficiently large indices $n$ ,

4 \le \#\{\, q \text{ prime} : \mathrm{prev}^2 < q < \mathrm{next}^2 \,\}.

Goal (Brocard's conjecture): the same inequality for every 0-indexed $n \ge 1$ , i.e. for every pair of consecutive primes starting from $(3,5)$ .

Significance

A proof of the goal settles Brocard's conjecture outright. Given Ferreira's asymptotic result, the remaining work splits into making the threshold effective and closing the finite range below it, both of which would be new formal content; the milestone itself (formalizing Ferreira's analytic argument) is a substantial analytic-number-theory formalization project.

Difficulty

Unconditional results on primes in short intervals $[x, x + x^{\theta}]$ only reach exponents $\theta$ well above $1/2$ , while the interval $(p_n^2, p_{n+1}^2)$ has length about $2 p_n g_n$ where $g_n = p_{n+1} - p_n$ can be small (e.g. twin primes), i.e. length on the order of the square root of its endpoint. Standard short-interval theorems therefore do not apply uniformly, and Legendre's conjecture — which would only give two primes here — is itself open.

Formalization scope

Everything is stated with Mathlib's Nat.nth Nat.Prime, Finset.Ioo (open interval, endpoints excluded) and Finset.filter Nat.Prime, followed by Finset.card. The hypothesis 1 ≤ n in the goal is the 0-indexed form of the source's " $n \ge 2$ "; it is necessary, since for index $0$ (primes $2, 3$ ) the interval $(4, 9)$ contains only the two primes $5, 7$ . The milestone uses Filter.atTop ("for all sufficiently large $n$ "), with no explicit threshold. No custom definitions are required.

Selected references

Brocard's conjecture, Wikipedia. https://en.wikipedia.org/wiki/Brocard%27s_conjecture
L. A. Ferreira, Real exponential sums over primes and prime gaps, arXiv:2307.08725 (2023). https://arxiv.org/abs/2307.08725
Statement adapted from the Formal Conjectures project (Apache-2.0), file BrocardConjecture.lean.

4 thms1 active userReviewed

Completed

Group Theory·Captain: burkh4rt

Local conjugacy in prosolvable groupsResearch Paper

Motivation

Two closed subgroups $H$ and $H'$ of a profinite group $G$ are locally conjugate if, for every prime $p$ , a Sylow $p$ -subgroup of $H$ is conjugate in $G$ to a Sylow $p$ -subgroup of $H'$ . Conjugate subgroups are always locally conjugate. The converse, which lets conjugacy be tested one prime at a time, fails in general. Deciding when it holds is a classical question about supplements of nilpotent normal subgroups.

1964. Glauberman: if $G = NJ$ acts on a set with $N$ transitive and $|N|$ , $|J|$ coprime, then $J$ fixes a point ([Glauberman 1964], Thm. 4).
1979. Losey and Stonehewer: in a finite solvable group, two locally conjugate supplements of a nilpotent normal subgroup $N$ are conjugate if (A) $G/N$ is nilpotent, (B) $N$ is abelian, or (C) the Sylow subgroups of $G$ have class at most two. They also exhibit $S_3$ acting on $Q_8$ inside $GL(2,3)$ , where the converse fails.
1988. Evans and Shin: for abelian $N$ , solvability of $G$ is not needed.
1995. Shin: Losey and Stonehewer's results hold for profinite $G$ and nilpotent $N$ .

Groups, local conditions, and cohomology

A profinite group is a compact Hausdorff totally disconnected topological group. Equivalently, it can be described through compatible finite quotient groups. A pronilpotent group has nilpotent finite continuous quotients. A prosupersolvable group has supersolvable finite continuous quotients; a finite group is supersolvable when it admits a normal series with cyclic factors. These properties concern all finite continuous quotients, with no uniform bound on their orders or nilpotency classes.

A subgroup $H$ supplements a normal subgroup $N$ when $NH=G$ . It complements $N$ when, in addition, $N\cap H=1$ . Two closed subgroups are locally conjugate when, for each prime $p$ , a Sylow $p$ -subgroup of one is conjugate in $G$ to a Sylow $p$ -subgroup of the other. For profinite groups, Sylow subgroups are maximal closed pro- $p$ subgroups. The conjugating element may depend on the prime. All subgroup notation in the paper carries closedness, as stipulated in §1.2.

The cohomological statements concern a profinite group $J$ acting continuously by automorphisms on a discrete group $N$ . With a left action, a continuous cocycle satisfies $f(xy)=f(x)(x\cdot f(y))$ . Two cocycles are equivalent when $g(x)=n^{-1}f(x)(x\cdot n)$ for one fixed $n\in N$ . Their quotient is the pointed set $H^1(J,N)$ , whose distinguished point is the identity cocycle. Stable classes on a subgroup compare a cocycle with its conjugates after restriction to the relevant intersections. This matters when the subgroup itself is not normal. The definitions follow §§1–1.2.

Formalization targets

The central conjugacy assertion is Theorem 1.1. For a closed normal pronilpotent subgroup $N$ of a profinite group $G$ , assume that $G$ is prosupersolvable or $G/N$ is pronilpotent. Then closed supplements $H,H'$ of $N$ satisfy

H\sim_G H'\quad\Longleftrightarrow\quad H\text{ and }H'\text{ are locally conjugate}.

Lemma 1.2 asserts, for finite nilpotent coefficients and its stated structural alternatives, a pointed bijection induced by simultaneous restriction:

H^1(J,N)\cong\prod_{p\in\pi(J)}\operatorname{inv}_J H^1(J_p,N).

The other numbered targets are Corollaries 1.3–1.4 and Propositions 2.1–2.3, 3.1–3.2, and 4.1–4.2. They retain the paper's distinctions between finite coefficients, locally finite discrete coefficients, and arbitrary closed pronilpotent subgroups. They also retain the normal-intersection condition in the semidirect-product inclusion and fixed-point results. The abelian conclusions impose no solvability assumption on the ambient profinite group.

Both counterexamples in §1 are targets. The quaternion example realizes $Q_8\rtimes S_3$ in $GL(2,3)$ , has exactly two global cohomology classes and trivial Sylow cohomology, and exhibits locally conjugate complements that are not conjugate. The Heisenberg example uses $C_3\wr S_3$ of order $162$ , with $N$ the Heisenberg group of order $27$ , $J\cong C_6$ , and $H\cong C_3\times S_3$ . Local containment holds while containment of a conjugate of $J$ fails.

The combined goal asserts all eleven numbered results and both counterexamples. Each assertion remains a separate milestone with the source's numbering or, for the unnumbered counterexamples, its section and page.

What a completed formalization provides

The conjugacy and containment theorems make precise when separate prime-wise witnesses can be replaced by one global witness. The fixed-point results similarly turn prime-wise fixed points, which can be different points, into a point fixed by the full subgroup. The counterexamples record the limits of these conclusions under weakened hypotheses. These are proved mathematical results of the preprint, rather than new conjectures.

A completed development would also provide reusable formal interfaces for continuous nonabelian first cohomology, stable classes, profinite Sylow and Hall conditions, and local subgroup relations. An earlier local Lean development supplies definitions and substantial proof material. The present draft statements are aligned to the arXiv version; their target proofs remain open in this proposal. Reusing earlier proofs requires checking their types against these interfaces and the pinned environment.

What makes the statements demanding

Local conjugators can vary with the prime, and there need not be one conjugator that works for all primes simultaneously. The quaternion example demonstrates this obstruction even in finite groups. Nonabelian cohomology is a pointed set, so the usual additive primary-decomposition language does not itself provide the needed assertion. The transition from finite groups to profinite groups also requires tracking topology, closedness, and continuity. The counterexamples and the finite-versus-profinite distinctions are part of the mathematical scope, not optional simplifications. See §§1–3.

Formalization scope and conventions

All declarations use the namespace LocalConjugacy. Profinite ambient groups use Mathlib's ProfiniteGrp; subgroups, quotient groups, normality, complements, actions, fixed points, finite Sylow subgroups, nilpotence, and solvability use Mathlib structures or predicates. Custom definitions cover the continuous nonabelian quotient and the profinite local conditions absent from the pinned library interface. Conjugation is written on the left. This changes the notation for the conjugating element, not the conjugacy or inclusion assertion.

The fixed-point targets quantify over nonempty sets with no added topology and require closed stabilizers. Propositions 2.1–2.2 allow infinite locally finite discrete coefficients. Theorem 1.1 allows arbitrary closed pronilpotent $N$ . Finite special cases cannot replace these targets. Both counterexamples include explicit isomorphisms to the concrete groups named in the paper. Contributions may reuse the existing proof development, improve the reusable interfaces, or prove the targets directly while preserving these statements.

Selected references

M. C. Burkhart, Local conjugacy in prosolvable groups, preprint, 2026. https://arxiv.org/abs/2609.37678
G. O. Losey and S. E. Stonehewer, Local conjugacy in finite soluble groups, Quart. J. Math. Oxford (2) 30 (1979), 183–190.
M. J. Evans and H. Shin, Local conjugacy in finite groups, Arch. Math. 50 (1988), 289–291.
H. Shin, A conjugacy theorem in profinite groups, Bull. Korean Math. Soc. 32 (1995), 139–144.
G. Glauberman, Fixed points in groups with operator groups, Math. Z. 84 (1964), 120–125.
L. Ribes and P. Zalesskii, Profinite Groups, 2nd ed., Springer, 2010.
J.-P. Serre, Galois Cohomology, Springer, 2002.

18 thms1 active userReviewed

Completed

Category Theory Quantum Information·Captain: Bingyu Xia

Categorical Quantum Mechanics II: The Born RuleTextbook

Motivation

Quantum mechanics predicts probabilities, but it is notoriously quiet about what a probability is. Categorical quantum mechanics answers that by rewriting the finite-dimensional formalism in the language of dagger categories: a state is a morphism $I \to A$ , an effect is a morphism $A \to I$ , and the probability of an outcome is a scalar — an endomorphism of the tensor unit. On that translation the Born rule stops being an axiom and becomes a theorem about a complete, disjoint family of effects.

This mission formalizes that theorem, together with the two lemmas it rests on, in Lean 4 over Mathlib. It covers the dagger and measurement material of Chapter 2 of Reutter and Vicary's Categorical Quantum Mechanics.

Setting

Fix a monoidal dagger category $\mathcal{C}$ with zero morphisms. The unit object $I$ carries a commutative monoid structure $\mathrm{End}(I)$ — the scalars. For a state $a : I \to c$ and an effect $x : c \to I$ , the probability that $x$ occurs on $a$ is the scalar

\mathrm{Prob}(a,x) \;=\; a^\dagger \circ x^\dagger \circ x \circ a .

A family of effects $x : I \to \mathrm{Eff}(c)$ is complete when the induced map $\langle x \rangle : \bigoplus_i I \to c$ satisfies $\bigvee_i x_i = \mathrm{id}_c$ , and disjoint when $x_i^\dagger \circ x_j = 0$ for $i \neq j$ . Both conditions are stated for a dagger biproduct of the unit objects.

Formalization targets

Goal — the Born rule

\sum_{i} \mathrm{Prob}(a, x_i) \;=\; \mathrm{id}_I \qquad \text{for } x \text{ complete and disjoint}

This is the mission's goal. It fixes nothing beyond completeness and disjointness; the statement is exactly the categorical Born rule for a finite outcome set.

Supporting results

Lemma 2.52. A family of effects is disjoint if and only if the dagger of its lift is an isometry; and complete if and only if the kernel of its lift is trivial.
Lemma 2.53. A complete and disjoint family of effects lifts to a unitary $\langle x \rangle : \bigoplus_i I \to c$ .
Lemma 2.41, Corollary 2.42. Dagger biproducts: transposing a matrix of morphisms daggers every entry, and daggers distribute over addition.

Significance

The Born rule is the point where the categorical and the Hilbert-space pictures are reconciled: the abstract statement specialises, in $\mathbf{Hilb}$ , to the usual $\sum_i |\langle x_i | a \rangle|^2 = 1$ . Proving it categorically means the rule is a consequence of the dagger-biproduct structure rather than an extra assumption, which is what makes the framework usable for quantum protocols — measurement, teleportation and the like are all built on complete disjoint families.

The supporting lemmas are reusable well beyond this mission: dagger biproducts are the categorical home of matrix calculus, and the isometry/unitary characterisations of disjointness and completeness are the standard toolkit for any later argument about measurements.

Difficulty

Moderate. The mathematics is elementary once the definitions are in place — the work is in bookkeeping: biproduct universal properties, the interaction of the dagger with the biproduct structure, and careful handling of the scalar monoid. The main intellectual step is realising that completeness alone, not equalizers, gives the second unitary identity.

Formalization scope

Formalized here: dagger categories and their morphism classes (§2.3), dagger biproducts (§2.3.3), and the scalar/state/effect vocabulary with the Born rule (§2.4.3). Mathlib has no dagger-category theory at all, so the definitions are supplied from scratch as Lean Definitions and are importable independently of this mission.

Not formalized: the Hilbert-space and relational models, the graphical calculus of §2.2, and the measurement/post-processing material after §2.4.3.

Two corrections to the source are made and documented in the formalization. The printed statement of Proposition 2.55 assumes completeness only, which is false; disjointness is required, as the book's own proof (which invokes Lemma 2.52) already assumes. And the book attributes the identity $x^\dagger \circ x = \mathrm{id}$ on $A$ to Lemma 2.52, whereas Lemma 2.52 only gives the identity on $\bigoplus_i I$ ; the identity on $A$ is Lemma 2.53. Lemma 2.53 is proved here without the book's equalizer hypothesis, so it is strictly stronger than the printed version.

Selected references

D. Reutter and J. Vicary, Categorical Quantum Mechanics, §2.3.3 and §2.4.3.
S. Abramsky and B. Coecke, A categorical semantics of quantum protocols, LICS 2004.
The Mathlib CategoryTheory.Limits.Biproducts and CategoryTheory.Monoidal.Category API, on which the definitions are built.

9 thms1 active userReviewed

Numerical Analysis Probability Stochastic Systems·Captain: mikedeng1

Euler Approximations with Varying Coefficients II: Strong Order 1/2 in Lp for Superlinearly Growing Diffusion CoefficientsResearch Paper

Motivation

Stochastic differential equations with superlinearly growing coefficients appear throughout applied probability: population models with cubic damping, Langevin dynamics with polynomial potentials, and stochastic volatility models such as the 3/2-model used for pricing VIX options, whose diffusion coefficient grows like $|x|^{3/2}$ . For such equations the classical explicit Euler–Maruyama method fails: Hutzenthaler, Jentzen and Kloeden (2011) proved that its $p$ -th moments diverge whenever a coefficient grows superlinearly, so it cannot converge in $\mathcal L^p$ . Implicit methods converge (Higham–Mao–Stuart 2002) but cost a nonlinear solve per step.

The tamed Euler schemes are the explicit response.

Hutzenthaler, Jentzen and Kloeden (2012) tamed a superlinear drift and proved strong order $1/2$ for globally Lipschitz diffusion coefficients.
Sabanis (2013) gave a simpler proof for a family of tamed drifts.
Hutzenthaler and Jentzen (2015) treated superlinear diffusion coefficients, obtaining $\mathcal L^p$ -convergence without a rate and only for small $p$ .
Sabanis (2016), the source of this mission, tames drift and diffusion together and proves the optimal strong rate $1/2$ in $\mathcal L^p$ under a one-sided (monotonicity) condition and polynomial growth. For the 3/2-model with $p_1=3.5$ , $p_0=6$ this gives $\mathcal L^2$ -convergence with order $1/2$ , which earlier results did not cover (p. 2).

This mission is the second of three on the paper. Mission I formalizes $\mathcal L^p$ -convergence without a rate (Theorem 1), mission III the uniform-in-time rate (Theorem 3).

Setting

Fix a filtered probability space $(\Omega,\{\mathcal F_t\}_{t\ge0},\mathcal F,P)$ with right-continuous filtration, a horizon $T>0$ , dimensions $d,d_1$ , and a $d_1$ -dimensional Wiener martingale $W$ : a standard Brownian motion adapted to $\{\mathcal F_t\}$ whose future increments are independent of $\mathcal F_t$ . The coefficients are Borel maps $b:[0,\infty)\times\mathbb R^d\to\mathbb R^d$ and $\sigma:[0,\infty)\times\mathbb R^d\to\mathbb R^{d\times d_1}$ ; $|x|$ is the Euclidean norm, $|A|$ the Hilbert–Schmidt norm, $xy$ the scalar product. The SDE is

dX(t)=b(t,X(t))\,dt+\sigma(t,X(t))\,dW(t),\qquad t\in[0,T],\qquad(2.1)

with an $\mathcal F_0$ -measurable initial value $X(0)=\xi$ . For $n\ge1$ let $\kappa_n(t)=\lfloor nt\rfloor/n$ and consider the scheme

dX_n(t)=b_n(t,X_n(\kappa_n(t)))\,dt+\sigma_n(t,X_n(\kappa_n(t)))\,dW(t),\qquad X_n(0)=\xi,\qquad(2.2)

whose coefficients are frozen at the last grid point, so that $X_n$ is computable step by step. The tamed coefficients of Model 2 are

b_n(t,x)=\frac{b(t,x)}{1+n^{-\alpha}|x|^l},\qquad \sigma_n(t,x)=\frac{\sigma(t,x)}{1+n^{-\alpha}|x|^l}.\qquad(2.11)\text{–}(2.12)

The hypotheses, with constants $p_0,p_1\ge2$ :

A-2: $b$ is bounded on balls, uniformly in $t\in[0,T]$ .
A-4 (coercivity): $2xb(t,x)+(p_0-1)|\sigma(t,x)|^2\le K(1+|x|^2)$ .
A-5: $\mathbb E|X(0)|^{p_0}<\infty$ .
A-6 (global monotonicity, polynomial growth): for positive $l$ and $L$ , $2(x-y)(b(t,x)-b(t,y))+(p_1-1)|\sigma(t,x)-\sigma(t,y)|^2\le L|x-y|^2$ and $|b(t,x)-b(t,y)|\le L(1+|x|^l+|y|^l)|x-y|$ .
The $\mathfrak p$ -condition: the scheme uses (2.11)–(2.12) with $\alpha=1/2$ , $l\le\frac{p_0-2}{4}$ , and $0<p<p_1$ , $p\le\frac{p_0}{2l+1}$ .
B-2 and B-3 (for the milestones): $|b_n|\le\min(Cn^\alpha(1+|x|),|b|)$ , $|\sigma_n|^2\le\min(Cn^\alpha(1+|x|^2),|\sigma|^2)$ , and A-4 for $b_n,\sigma_n$ with a constant uniform in $n$ .

Formalization targets

Goal: Theorem 2 (p. 6)

Under A-2, A-4–A-6, the $\mathfrak p$ -condition and $p_1>2$ , there is a constant $C$ independent of $n$ with

\sup_{0\le t\le T}\mathbb E\big[|X(t)-X_n(t)|^p\big]\le Cn^{-p/2}\qquad(n\ge1).\qquad(2.13)

The constant is existential and may depend on all data except $n$ .

Milestones

Lemma 2 (p. 8): $\sup_t\mathbb E|X(t)|^p$ and $\sup_{n\ge1}\sup_t\mathbb E|X_n(t)|^p$ are finite for $0<p\le p_0$ , under A-1–A-5, B-2, B-3.
Lemma 3 (p. 15): for Model 2, $\mathbb E\int_0^T|b(s,X_n(\kappa_n(s)))-b_n(s,X_n(\kappa_n(s)))|^p\,ds\le Cn^{-\alpha p}$ , and the same for $\sigma$ .
Lemma 4 (p. 16): $\sup_t\mathbb E|X_n(t)-X_n(\kappa_n(t))|^p\le Cn^{-p/2}$ .

Significance

Theorem 2 shows that an explicit scheme costing one coefficient evaluation per step attains the same strong order as the classical Euler method under global Lipschitz conditions. It does so for drift and diffusion coefficients that grow polynomially, and for moment orders $p$ that are small relative to $p_0$ and $p_1$ . Strong $\mathcal L^p$ rates are what multilevel Monte Carlo needs: the variance of level corrections is controlled by the $\mathcal L^2$ rate. When $l$ could be taken to be $0$ the statement specializes to the classical globally Lipschitz rate (Remark 6).

The result is proved on paper; it has no machine-checked proof. Stochastic integrals are not in Mathlib; this mission uses the Brownian Itô-integral relation published by the Ethier–Kurtz series on the platform. A formal proof would give the first verified strong convergence rate for any Euler-type scheme. Along the way it produces reusable moment bounds for tamed schemes and the $L^p$ control of one-step increments.

Difficulty

The obvious argument applies Itô's formula to $|X-X_n|^p$ and closes a Gronwall inequality. Two steps of it fail without taming. First, the error splits into the monotone part, handled by A-6, and cross terms such as $|X_n(s)-X_n(\kappa_n(s))|^p$ multiplied by $(1+|X_n|^{2l})^{p/2}$ ; they are controlled only through moments of $X_n$ of order well above $p$ that are uniform in $n$ , which the untamed scheme lacks. Second, the taming itself introduces an error $b-b_n$ that must be shown to be $O(n^{-1/2})$ in $\mathcal L^p$ and not merely $o(1)$ . The exponents in the $\mathfrak p$ -condition are exactly what the Hölder splittings of these two terms require.

Formalization scope

Processes. Solutions are hypotheses, not constructed: $X$ solves (2.1) and each $X_n$ solves (2.2), on one probability space, with one $W$ and one $\xi$ , on $[0,T]$ only. An Itô process is a measurable process adapted to the null-set completion of the filtration, with continuous paths on $[0,T]$ , and a.s. for all $t\le T$ simultaneously $X(t)=\xi+\int_0^t B\,ds+\int_0^t S\,dW$ . The stochastic integral is the platform relation EthierKurtz_HasBrownianItoIntegral, with the integrand cut off after $T$ .
Expectations and suprema are computed in $[0,\infty]$ (lower Lebesgue integrals), so no junk value of a non-integrable Bochner integral or of an unbounded real supremum enters. Rates are stated as $\le Cn^{-p/2}$ for every $n\ge1$ , with $C$ real and quantified after all data.
Added hypotheses, disclosed. Theorem 2 carries $p_1>2$ : the printed proof covers $2\le p<p_1$ and reduces $p<2$ to $p=2$ , which the $\mathfrak p$ -condition admits exactly when $p_1>2$ . Lemma 4 carries B-3, which its proof uses through Lemma 2. Lemma 2 drops the stated dependence of $C$ on $(p,T,K,\mathbb E|X(0)|^p)$ and keeps only its finiteness uniformly in $n$ .
Ruling out trivialization. The hypotheses are satisfiable, e.g. by $b=\sigma=0$ with constant solutions and $p_0=6$ , $p_1=3$ , $l=1$ , $p=2$ . The rate is a bound for every $n\ge1$ , not an eventual or $o(1)$ statement. A proof that uses a constant depending on $n$ , or treats only $X\equiv X_n$ , does not prove the goal.
Infrastructure needed: Itô's formula for $|x|^p$ against the platform's Itô integral, the Burkholder–Davis–Gundy inequality (or its $\mathcal L^p$ moment form), the zero-expectation property of Itô integrals of square-integrable integrands, and Gronwall's lemma in integral form. These are reusable far beyond this mission, and contributions of any of them are welcome.

Selected references

S. Sabanis, Euler approximations with varying coefficients: the case of superlinearly growing diffusion coefficients, Ann. Appl. Probab. 26(4), 2016. https://arxiv.org/abs/1308.1796 (v4)
M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong and weak divergence in finite time of Euler's method for stochastic differential equations with non-globally Lipschitz continuous coefficients, Proc. R. Soc. A 467, 2011. https://doi.org/10.1098/rspa.2010.0348
M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong convergence of an explicit numerical method for SDEs with non-globally Lipschitz continuous coefficients, Ann. Appl. Probab. 22, 2012. https://mathscinet.ams.org/mathscinet-getitem?mr=MR2985171
M. Hutzenthaler, A. Jentzen, Numerical approximations of stochastic differential equations with non-globally Lipschitz continuous coefficients, Mem. Amer. Math. Soc. 236(1112), 2015. https://doi.org/10.1090/memo/1112
S. Sabanis, A note on tamed Euler approximations, Electron. Commun. Probab. 18, 2013. https://mathscinet.ams.org/mathscinet-getitem?mr=MR3070913
D. J. Higham, X. Mao, A. M. Stuart, Strong convergence of Euler-type methods for nonlinear stochastic differential equations, SIAM J. Numer. Anal. 40, 2002. https://mathscinet.ams.org/mathscinet-getitem?mr=MR1949404

13 thms1 active userReviewed

Analysis Control Theory Partial Differential Equations·Captain: mikedeng1

Stability and Instability Results of the Wave Equation with a Delay Term in the Boundary or Internal Feedbacks II: Exponential Decay under Delayed Internal DampingResearch Paper

Motivation

Feedback laws that damp vibrations in elastic structures are implemented by sensors and actuators, and a physical loop always reacts with some time delay $\tau>0$ : the damping force at time $t$ is computed from the velocity measured at time $t-\tau$ . Datko, Lagnese and Polis showed in 1986 that an arbitrarily small delay in a boundary feedback can destroy the stability of a one-dimensional wave equation (Datko–Lagnese–Polis, SIAM J. Control Optim. 24 (1986)), and Datko showed that such fragility is common to a broad class of feedback-stabilized hyperbolic systems (Datko, SIAM J. Control Optim. 26 (1988)). Delay-robustness is therefore a genuine question for every stabilizing feedback, not a technicality.

Nicaise and Pignotti (SIAM J. Control Optim. 45 (2006) 1561–1585) identified a simple sufficient condition in several space dimensions: if the feedback contains an undelayed velocity term with gain $\mu_1$ and a delayed one with gain $\mu_2$ , and $\mu_2<\mu_1$ , the energy still decays exponentially; if $\mu_2\ge\mu_1$ , instabilities appear for some delays. This mission formalizes the stability half for internal (distributed) damping, localized near the Neumann part of the boundary.

Timeline.

1986: Datko, Lagnese, Polis — small delays destabilize a boundary-damped 1D wave equation.
1988: Datko — many feedback-stabilized hyperbolic systems are not robust with respect to small delays.
1990: Zuazua — exponential decay for the semilinear wave equation with locally distributed damping, without delay (Comm. PDE 15 (1990)); Liu (1997) treats locally distributed damping for general conservative systems (SIAM J. Control Optim. 35 (1997)).
2006: Nicaise, Pignotti — exponential decay with a delayed boundary or internal feedback under $\mu_2<\mu_1$ (Theorems 1.1 and 1.3), and instability examples when $\mu_2\ge\mu_1$ (Theorems 1.2 and 1.4).

Setting

Let $\Omega\subset\mathbb{R}^n$ , $n\ge1$ , be a bounded open set with boundary $\Gamma$ of class $C^2$ , split as $\Gamma=\Gamma_D\cup\Gamma_N$ with $\overline{\Gamma_D}\cap\overline{\Gamma_N}=\emptyset$ and $\Gamma_D\neq\emptyset$ . Write $\nu$ for the outer unit normal, $d\Gamma$ for the surface measure, $u_t,u_{tt}$ for time derivatives and $\Delta$ for the Laplacian in $x$ .

Geometric hypothesis (1.6)–(1.7): there are a $C^2$ function $v$ and $\alpha>0$ with $\langle D^2v(x)\xi,\xi\rangle\ge2\alpha|\xi|^2$ for all $x\in\overline\Omega$ , $\xi\in\mathbb{R}^n$ , and $\nabla v(x)\cdot\nu(x)\le0$ on $\Gamma_D$ .

Damping coefficient. $\omega\subset\Omega$ is an open neighbourhood of $\Gamma_N$ (in $\Omega$ ), and $a\in L^\infty(\Omega)$ satisfies

a(x)\ge0\ \text{a.e. in }\Omega\quad(1.17),\qquad a(x)>a_0>0\ \text{a.e. in }\omega\quad(1.18).

The system (1.12)–(1.16): for gains $\mu_1,\mu_2>0$ and delay $\tau>0$ ,

u_{tt}(x,t)-\Delta u(x,t)+a(x)\big[\mu_1u_t(x,t)+\mu_2u_t(x,t-\tau)\big]=0\quad\text{in }\Omega\times(0,\infty),

with $u=0$ on $\Gamma_D$ , $\partial u/\partial\nu=0$ on $\Gamma_N$ , initial data $u(\cdot,0)=u_0$ , $u_t(\cdot,0)=u_1$ , and history $u_t(x,t-\tau)=g_0(x,t-\tau)$ for $t\in(0,\tau)$ .

The energy. Assume $\mu_2<\mu_1$ (1.8) and fix $\xi$ with $\tau\mu_2<\xi<\tau(2\mu_1-\mu_2)$ (1.10). Then

\mathcal F(t)=\frac12\int_\Omega\big\{u_t^2(x,t)+|\nabla u(x,t)|^2\big\}dx+\frac\xi2\int_\Omega a(x)\int_0^1u_t^2(x,t-\tau\rho)\,d\rho\,dx\qquad(1.19).

The first summand is the standard energy $\mathcal E(t)$ ; the second accounts for the velocity history on the delay window.

Formalization targets

Goal: Theorem 1.3

There exist $C_1,C_2>0$ , depending on the data but not on the solution, such that every solution satisfies

\mathcal F(t)\le C_1\,\mathcal F(0)\,e^{-C_2t}\qquad\forall t\ge0.

The constants are left existential, as in the paper, so no later sharpening of rates invalidates the goal.

Milestones (in the order of the proof)

(4.4) The energy identity

\mathcal F'(t)=-\mu_1\!\int_\Omega a u_t^2(t)-\mu_2\!\int_\Omega a u_t(t)u_t(t-\tau)+\frac{\xi\tau^{-1}}2\!\int_\Omega a u_t^2(t)-\frac{\xi\tau^{-1}}2\!\int_\Omega a u_t^2(t-\tau).

Proposition 4.1 $\mathcal F$ is nonincreasing and $\mathcal F'(t)\le-C\int_\Omega a\{u_t^2(t)+u_t^2(t-\tau)\}dx$ with $C>0$ .
Proposition 4.2 Observability for the undamped mixed problem: for $T$ larger than some $T_0$ , $\mathcal E_w(0)\le C_1\int_0^T\int_\omega w_t^2\,dx\,dt$ .
Proposition 4.3 Observability for the delayed system: for $T$ larger than some $\overline T$ , $\mathcal F(0)\le C_0\int_0^T\int_\Omega a\{u_t^2(t)+u_t^2(t-\tau)\}dx\,dt$ .
Contraction step (p. 1579): some $T>0$ and $\widetilde C\in[0,1)$ with $\mathcal F(T)\le\widetilde C\,\mathcal F(0)$ for every solution.

Significance

The result. Theorem 1.3 shows that a localized viscous damping acting only near the Neumann boundary keeps its exponential stabilizing effect when part of the feedback is delayed, provided the delayed gain is dominated by the undelayed one. Together with Theorem 1.4 of the same paper (instability for $\mu_2\ge\mu_1$ and suitable delays) it gives a sharp threshold in terms of the gains. The energy $\mathcal F$ with its history term became the standard Lyapunov functional for delayed wave and plate equations in the literature that followed.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any exponential decay result for a multidimensional wave equation, is known to exist. A complete development would produce reusable Lean infrastructure: energy identities for the wave equation on $C^2$ domains via the divergence theorem, the delay-energy calculus, and an observability inequality for the wave equation with mixed boundary conditions. Each milestone has value on its own; Proposition 4.2 in particular is a classical control-theoretic result.

Difficulty

The energy estimates (milestones 1 and 2) are calculus once the divergence theorem is available. The central difficulty is observability. Energy dissipation alone gives only $\mathcal F$ nonincreasing; exponential decay needs the energy at time $0$ to be controlled by the energy dissipated on $[0,T]$ (Proposition 4.3), and that needs the conservative wave equation to be observable from $\omega$ (Proposition 4.2). The observability inequality does not follow from energy identities: the paper relies on Carleman estimates of Lasiecka–Triggiani–Yao (1999) and a compactness–uniqueness argument, neither of which is available in Mathlib. The obvious attempt, a multiplier identity with $\nabla v\cdot\nabla u$ alone, leaves boundary terms on $\Gamma_N$ that cannot be absorbed without a localization near $\Gamma_N$ and a lower-order compactness step.

Formalization scope

Points are EuclideanSpace ℝ (Fin n) with 1 ≤ n; solutions are real valued.
The $C^2$ boundary is given by a global $C^2$ defining function $\psi$ with $\Omega=\{\psi<0\}$ , $\partial\Omega=\{\psi=0\}$ , $\nabla\psi\ne0$ on $\partial\Omega$ ; $\nu=\nabla\psi/|\nabla\psi|$ .
The surface measure $d\Gamma$ is a finite measure carried by $\partial\Omega$ for which the Gauss–Green formula holds for every $C^1$ vector field; this determines it uniquely. It is not Mathlib's unnormalized Hausdorff measure.
Solutions are classical: $u$ is $C^2$ on $\mathbb{R}^n\times\mathbb{R}$ , the equation holds for every $t>0$ and almost every $x\in\Omega$ (because $a$ is only $L^\infty$ ), and the initial data and history are the values of $u$ and $u_t$ at $t\le0$ . This is a subclass of the paper's solutions, so the formal theorems are consequences of the paper's.
$a$ is measurable and essentially bounded on $\Omega$ ; (1.17) and (1.18) are almost-everywhere conditions. "Open neighbourhood of $\Gamma_N$ " means $\omega\supseteq O\cap\Omega$ for some open $O\supseteq\Gamma_N$ (a subset of $\Omega$ cannot contain $\Gamma_N$ itself).
Added hypothesis (Propositions 4.2, 4.3, the contraction step and Theorem 1.3): the closure of every connected component of $\Omega$ meets $\Gamma_D$ ; this holds whenever $\Omega$ is connected. The proof of Proposition 4.2 uses Poincaré's inequality for functions vanishing on $\Gamma_D$ , and its compactness–uniqueness step concludes that a harmonic function vanishing on $\Gamma_D$ with zero normal derivative on $\Gamma_N$ is zero; both need this condition.
"Decreasing" in Proposition 4.1 is read as nonincreasing; its constant $C>0$ is existential, chosen before the solution.
Printed slips on p. 1575: the last line of (4.3) integrates with $d\Gamma$ where $dx$ is meant, and its first line repeats $u_\rho(x,t-\tau)$ for $u_\rho(x,t-\tau\rho)$ . Neither affects any formal statement; (4.4) itself is correct.
A formalization in which the $a$ -weighted integrals are Lean's junk value $0$ (non-measurable $a$ ), in which $\omega$ is required to contain $\Gamma_N$ (unsatisfiable), or in which the surface measure is arbitrary, would trivialize or falsify the targets; all three are excluded by the definitions.

Needed infrastructure: the divergence theorem on $C^2$ domains (assumed here as a structure field), differentiation under the integral sign for the energies, Carleman estimates or another route to observability for the mixed wave problem, and a compactness argument (Rellich). Contributions of any of these as standalone lemmas are welcome.

Selected references

S. Nicaise, C. Pignotti, Stability and instability results of the wave equation with a delay term in the boundary or internal feedbacks, SIAM J. Control Optim. 45(5):1561–1585, 2006. https://doi.org/10.1137/060648891
R. Datko, J. Lagnese, M. P. Polis, An example on the effect of time delays in boundary feedback stabilization of wave equations, SIAM J. Control Optim. 24:152–156, 1986. https://doi.org/10.1137/0324007
R. Datko, Not all feedback stabilized hyperbolic systems are robust with respect to small time delays in their feedbacks, SIAM J. Control Optim. 26:697–713, 1988. https://doi.org/10.1137/0326040
E. Zuazua, Exponential decay for the semilinear wave equation with locally distributed damping, Comm. Partial Differential Equations 15:205–235, 1990. https://doi.org/10.1080/03605309908820684
K. Liu, Locally distributed control and damping for the conservative systems, SIAM J. Control Optim. 35:1574–1590, 1997. https://doi.org/10.1137/S0363012995284928
I. Lasiecka, R. Triggiani, P. F. Yao, Inverse/observability estimates for second-order hyperbolic equations with variable coefficients, J. Math. Anal. Appl. 235:13–57, 1999 (reference [14] of the paper; the Carleman estimates used in Proposition 4.2). https://doi.org/10.1006/jmaa.1999.6348

9 thms1 active userReviewed

Completed

Functional Analysis·Captain: savarin

Sharp diagonal Hlawka constants: foundation and proved cutoff 256Research Paper

The Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.

This mission establishes the best possible constant for complex diagonal matrices for every real $p\ge256$ . The result is proved in Lean. For each exponent, one constant works for every triple of diagonal matrices of the same size, across all finite sizes.

The constant comes from a simple family of three $3\times3$ diagonal matrices, called the cyclic family. Varying one parameter determines the largest comparison constant these examples require. The theorem proves that this value also works for every other triple of diagonal matrices, however large. The goal theorem gives the exact formula and statement.

This is the foundation of the sharp diagonal Hlawka campaign. It supplies the shared definitions and supporting results for lowering the exponent cutoff while keeping the same formula. A later mission has now established the result in Lean for every real $p\ge90$ ; the campaign invites further improvements.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

References

K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library

Established results on Prove2Me

59 thms1 active userReviewed

All missions

Optimization of Mean-field Spin Glasses III: The Lagrangian Value of the Stochastic Control Problem Equals the Parisi FunctionalResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 4.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimization of Mean-field Spin Glasses II: Under No Overlap Gap, the Monotone Parisi Minimizer Also Minimizes the Extended FunctionalResearch Paper

Motivation

Setting

Formalization targets

Goal: the monotone minimizer is a minimizer over L\mathscr LL (Section 6.3, p. 34)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Convergence in law of the minimum of a branching random walk: The Minimum Centred at (3/2) ln n Converges to a Gumbel Law Shifted by the Derivative MartingaleResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.1

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

Six-colour Schur colourings of [1, 1801] under R₄(3) ≤ 61: balanced classes, nested saturation and forced reflectionResearch Paper

Motivation

Setting

Formalization targets

Goal: six colours under R4(3)≤61R_4(3) \le 61R4​(3)≤61

Centred-interval bound

Balanced colour classes

Nested saturation

Automorphism extension

Forced reflection

The saturation degree is even

Significance

Difficulty

Formalization scope

Selected references

Projection-like Retractions on Matrix Manifolds IV: Within σ_r(X̄)/2 of a Rank-r Matrix, the Truncated SVD Is the Unique Nearest Matrix of Rank Exactly rResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3.3

Milestones

Further result: Proposition 4.11

Significance

Difficulty

Formalization scope

Selected references

Every Odd Number Greater Than 1 is the Sum of at Most 6101 PrimesResearch Paper

Motivation

Setting

Formalization target

Goal

How the bound arises

Significance

Formalization scope

Selected references

Every Odd Number Greater Than 1 is the Sum of at Most 97041 PrimesResearch Paper

Motivation

Setting

Formalization target

Goal

How the bound arises

Significance

Formalization scope

Selected references

Dynamic Pricing Strategies with Reference Effects I: Under Loss Aversion the Steady States Form an Interval and Optimal Paths ConvergeResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4 of the paper

Goal: the monotone minimizer is a minimizer over $\mathscr L$ (Section 6.3, p. 34)

Goal: six colours under $R_4(3) \le 61$