Partial Differential Equations

Motivation

The incompressible Navier–Stokes equations are the standard model for the motion of a viscous fluid such as water or air, used daily in engineering, meteorology and oceanography. Yet the most basic mathematical question about them is open: starting from smooth initial data in three dimensions, does a smooth solution exist for all time? This is one of the seven Millennium Prize Problems of the Clay Mathematics Institute. Its official formulation is Charles Fefferman's problem description, Existence and smoothness of the Navier–Stokes equation (2000), which offers a prize for a proof of any one of four statements: global existence and smoothness on $\mathbb{R}^3$ (statement (A)) or on the torus $\mathbb{R}^3/\mathbb{Z}^3$ (statement (B)), or a counterexample to either (statements (C) and (D)). This mission formalizes statement (A), together with the classical partial results that Fefferman lists as known.

Timeline.

• 1822–1845: Navier and Stokes write down the equations of a viscous incompressible fluid.
• 1934: Jean Leray, Sur le mouvement d'un liquide visqueux emplissant l'espace (Acta Math. 63), proves on $\mathbb{R}^3$ that smooth solutions exist for a positive time depending on the data, that they exist for all time when the data is small compared with the viscosity, and that global weak solutions with finite energy always exist. Their smoothness and uniqueness are left open.
• 1933–1969: the two-dimensional problem is settled (Leray for the plane; Olga Ladyzhenskaya's monograph The Mathematical Theory of Viscous Incompressible Flow, 2nd ed. 1969, for bounded domains): smooth solutions exist for all time and are unique.
• 1984: Tosio Kato, Strong $L^p$-solutions of the Navier–Stokes equation in $\mathbb{R}^m$ (Math. Z. 187), gives global solutions for initial data small in $L^3(\mathbb{R}^3)$.
• 1976–1998: partial regularity. Scheffer, then Caffarelli, Kohn and Nirenberg (Comm. Pure Appl. Math. 35, 1982), show that the singular set of a suitable weak solution has one-dimensional parabolic Hausdorff measure zero.
• 2000: the Clay Mathematics Institute adopts Fefferman's formulation as a Millennium Prize Problem. It remains open.

Setting

Fix a dimension $n \ge 1$ and write $\mathbb{R}^n$ for Euclidean $n$-space with its Euclidean norm $|x|$; in Lean this is NavierStokes.Vec n. A velocity field assigns to each time $t \in \mathbb{R}$ and point $x \in \mathbb{R}^n$ a vector $u(x,t) \in \mathbb{R}^n$; in Lean $u\,t$ is the field at time $t$ and $u\,t\,x$ is Fefferman's $u(x,t)$. A pressure is a real function $p(x,t)$. The viscosity $\nu$ is a positive constant. The external force of Fefferman's equation (1) is identically zero throughout, as in statement (A).

For a vector field $v : \mathbb{R}^n \to \mathbb{R}^n$ the divergence is

$$\operatorname{div} v = \sum_{i=1}^n \frac{\partial v_i}{\partial x_i},$$

in Lean NavierStokes.div, computed from the Fréchet derivative $Dv(x)$ as $\sum_i (Dv(x)\,e_i)_i$. The Laplacian $\Delta v = \sum_i \partial^2 v/\partial x_i^2$ acts componentwise (Mathlib's Laplacian on inner product spaces). The gradient $\nabla p$ is Mathlib's gradient. The convective term $\sum_j u_j\,\partial u/\partial x_j$ is the derivative of $u(\cdot,t)$ at $x$ in the direction $u(x,t)$. Finally $|\nabla v|^2 = \sum_{i,j} (\partial v_i/\partial x_j)^2$ is NavierStokes.gradNormSq.

Admissible initial data (Fefferman's condition (4), NavierStokes.IsInitialData): a $C^\infty$, divergence-free vector field $u^0$ that decays together with all its derivatives faster than any power,

$$|\partial_x^\alpha u^0(x)| \le C_{\alpha K}\,(1+|x|)^{-K} \quad \text{on } \mathbb{R}^n, \text{ for every } \alpha \text{ and } K.$$

In Lean the bound is $(1+|x|)^K\,\|D^k u^0(x)\| \le C_{kK}$ on the $k$-th Fréchet derivative, an equivalent family of conditions. These are exactly the divergence-free Schwartz functions.

A physically reasonable solution on a set $S$ of times (NavierStokes.IsSolutionOn; $S = [0,\infty)$ for NavierStokes.IsSolution) is a pair $(u,p)$ such that

1. (Fefferman (6)) $u$ and $p$ are $C^\infty$ on $S \times \mathbb{R}^n$, up to the boundary of $S$;
2. (Fefferman (1), $f \equiv 0$) for every $t \in S$ with $t > 0$ and every $x$,

$$\frac{\partial u}{\partial t} + \sum_{j=1}^n u_j \frac{\partial u}{\partial x_j} = \nu\,\Delta u - \nabla p;$$

3. (Fefferman (2)) $\operatorname{div} u(\cdot,t) = 0$ for every $t \in S$;
4. (Fefferman (3)) $u(x,0) = u^0(x)$;
5. (Fefferman (7), bounded energy) $\int_{\mathbb{R}^n} |u(x,t)|^2\,dx < C$ for all $t \in S$, for some constant $C$.

Formalization targets

Goal: Fefferman's statement (A)

Take $\nu > 0$ and $n = 3$. For every admissible initial datum $u^0$ there exist a velocity field $u$ and a pressure $p$ forming a physically reasonable solution on $\mathbb{R}^3 \times [0,\infty)$:

$$\forall\, \nu > 0,\ \forall\, u^0 \text{ satisfying (4)},\ \exists\, (u,p) \text{ satisfying (1), (2), (3), (6), (7) on } \mathbb{R}^3 \times [0,\infty).$$

This is NavierStokes.existence_and_smoothness_R3. It is open; a proof would settle the Millennium Prize Problem in the affirmative.

Milestones: what Fefferman lists as known

1. Local existence (NavierStokes.local_existence_R3): for $n = 3$ and every admissible $u^0$ there are $T > 0$ and a physically reasonable solution on $\mathbb{R}^3 \times [0,T)$. Fefferman: "(A) and (B) hold ... if the time interval $[0,\infty)$ is replaced by a small time interval $[0,T)$, with $T$ depending on the initial data."
2. Global existence for small data (NavierStokes.small_data_global_existence_R3): there is an absolute constant $c > 0$ such that, for $n = 3$, (A) holds for every admissible $u^0$ with

$$\|u^0\|_{L^2}^2\,\|\nabla u^0\|_{L^2}^2 \le c\,\nu^4.$$

Fefferman: "(A) and (B) hold provided the initial velocity $u^0$ satisfies a smallness condition." The scale-invariant product is Leray's form of the condition; it implies smallness of $\|u^0\|_{L^3}/\nu$, so Kato's theorem also applies. 3. The two-dimensional case (NavierStokes.existence_and_smoothness_R2): statement (A) with $n = 2$. Fefferman: "In two dimensions, the analogues of assertions (A) and (B) have been known for a long time (Ladyzhenskaya)."

A bridging lemma, NavierStokes.isInitialData_iff_schwartz, identifies the admissible data with the divergence-free elements of Mathlib's Schwartz space.

Significance

The result itself. Statement (A) asks whether the basic model of viscous flow is well posed in the classical sense, i.e. whether smooth finite-energy flows can develop singularities in finite time. A positive answer shows the equations never leave the classical regime; a negative one shows the model predicts its own breakdown. Fefferman: "since we don't even know whether these solutions exist, our understanding is at a very primitive level."

Formalizing it. None of the results in this mission has a machine-checked proof, and Mathlib contains no theory of the Navier–Stokes or Euler equations. The milestones are all proved in the literature; formalizing them requires building, on Mathlib's calculus, measure theory and Schwartz space, the heat semigroup on $\mathbb{R}^n$, the pressure equation $\Delta p = -\sum_{i,j} \partial_i\partial_j(u_i u_j)$ or the Leray projection, energy estimates, and a fixed-point construction of solutions, most of which is reusable for other evolution equations. The goal is open and expected to remain so; its role is to fix in Lean the exact statement the prize asks for, so partial results are formalized against it.

Difficulty

The energy identity $\frac{d}{dt}\int|u|^2 = -2\nu\int|\nabla u|^2$ controls $u$ in $L^2$ and $\nabla u$ in $L^2_{t,x}$, but in three dimensions this control is supercritical: under the scaling $u_\lambda(x,t) = \lambda u(\lambda x, \lambda^2 t)$ that preserves the equations, the energy of $u_\lambda$ shrinks as $\lambda \to \infty$, so bounded energy does not prevent concentration at small scales. Every known continuation criterion (Leray, Prodi–Serrin, Beale–Kato–Majda, Escauriaza–Seregin–Šverák) needs a quantity at or above critical scaling, none of which the energy controls. The obvious first idea, an ordinary differential inequality for $\|\nabla u(t)\|_{L^2}$, gives $\frac{d}{dt}\|\nabla u\|_{L^2}^2 \le C\nu^{-3}\|\nabla u\|_{L^2}^6$, which closes only for small data or short time. That is exactly why milestones 1 and 2 are theorems and the goal is not.

The formalization adds a second difficulty: the solutions of the literature live in Sobolev or Besov spaces, with pointwise smoothness of $u$ and $p$ recovered afterwards by regularity theory, and Mathlib has neither Sobolev spaces on $\mathbb{R}^n$ nor the heat semigroup in usable form.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure; the dimension is a parameter, the goal fixes $n = 3$ and the 2D milestone $n = 2$.
• A velocity field is a function of all real times, but every condition is imposed only on the time set $S$; values at negative times are unconstrained.
• Smoothness on $\mathbb{R}^n \times [0,\infty)$ is Mathlib's ContDiffOn of the uncurried map on the closed half-space, i.e. all derivatives extend continuously to $t = 0$. The momentum equation is imposed at interior times $t > 0$ with two-sided derivatives; by continuity of the derivatives this is equivalent to Fefferman's "$t \ge 0$".
• Derivatives are Mathlib's total functions (fderiv, deriv, iteratedFDeriv, gradient, Laplacian) with junk value $0$ at non-differentiable points; the smoothness hypotheses make every derivative in the statements honest.
• The energy is a Lebesgue integral in $[0,\infty]$, equal to $\infty$ when $u(\cdot,t) \notin L^2$, so bounded energy cannot hold vacuously. The $L^2$ norms in the small-data hypothesis are Bochner integrals, genuine for Schwartz data.
• No normalization is imposed on the pressure, as in Fefferman's text.

No trivializing formalization. The zero field solves the equations only for $u^0 = 0$; for any other admissible $u^0$ the initial condition, smoothness, the equation on $t > 0$ and bounded energy must all hold.

Infrastructure needed and welcome contributions. The heat kernel on $\mathbb{R}^n$ with Schwartz bounds; the Riesz-transform representation of the pressure or the Leray projection; energy identities for smooth decaying solutions; local existence by Picard iteration; the two-dimensional vorticity equation and its maximum principle. Theorems in the NavierStokes namespace, decompositions of the milestones, and Mathlib lemmas about ContDiffOn on half-spaces are all welcome. Statements (B), (C), (D) and the Euler equations ($\nu = 0$) are out of scope.

Selected references

• C. L. Fefferman, Existence and smoothness of the Navier–Stokes equation, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf
• J. Leray, Sur le mouvement d'un liquide visqueux emplissant l'espace, Acta Mathematica 63 (1934), 193–248. https://doi.org/10.1007/BF02547354
• O. A. Ladyzhenskaya, The Mathematical Theory of Viscous Incompressible Flow, 2nd ed., Gordon and Breach, 1969. https://archive.org/details/mathematicaltheo0000lady
• T. Kato, Strong $L^p$-solutions of the Navier–Stokes equation in $\mathbb{R}^m$, with applications to weak solutions, Mathematische Zeitschrift 187 (1984), 471–480. https://doi.org/10.1007/BF01174182
• L. Caffarelli, R. Kohn, L. Nirenberg, Partial regularity of suitable weak solutions of the Navier–Stokes equations, Communications on Pure and Applied Mathematics 35 (1982), 771–831. https://doi.org/10.1002/cpa.3160350604
• A. J. Majda, A. L. Bertozzi, Vorticity and Incompressible Flow, Cambridge University Press, 2002. https://doi.org/10.1017/CBO9780511613203
• J. C. Robinson, J. L. Rodrigo, W. Sadowski, The Three-Dimensional Navier–Stokes Equations: Classical Theory, Cambridge University Press, 2016. https://doi.org/10.1017/CBO9781139095143

Motivation

Let $S\subset\mathbb{R}^{2n+2}$ be a hypersurface that is strictly star-shaped about the origin. The standard Liouville form restricts to a contact form on $S$, and its Reeb vector field $R$ is a reparametrization of the Hamiltonian flow of any function with $S$ as a regular level. Weinstein conjectured in 1978, motivated by results of Rabinowitz, that Reeb flows on closed contact manifolds have periodic orbits; H. Hofer established this for the three-sphere and further three-dimensional cases in 1993 (Invent. Math. 114), with finite-energy pseudoholomorphic curves in the symplectization $\mathbb{R}\times S$ as the central objects. Since then these curves have been the main source of periodic orbits, global surfaces of section and invariants of Reeb flows, for example in U. Hryniewicz's characterization of the Reeb orbits that bound disk-like global surfaces of section (arXiv:1105.2077).

The basic fact about these curves is their behaviour near a puncture: a finite-energy curve on a punctured disk either extends over the puncture or approaches a periodic Reeb orbit there. This mission formalizes that statement for the symplectization of a strictly star-shaped level in $\mathbb{R}^{2n+2}$, following C. Wendl, Lectures on Symplectic Field Theory, Lecture 9 (arXiv:1612.01009), together with the results on planes, cylinders and energy concentration that accompany it in Hofer's and Hryniewicz's papers. It is the seventh mission in a series on symplectic field theory and builds on the sixth, which defines almost complex structures and pseudoholomorphic maps on open subsets of a vector space.

Setting

• Linear data. $V=\mathbb{R}^{2n+2}$ with coordinates $(q_1,p_1,\dots,q_{n+1},p_{n+1})$, the complex structure $j_0$ (multiplication by $i$ on $q_k+ip_k$), $\omega_0=\sum_kdq_k\wedge dp_k$ and $\lambda_0=\tfrac12\sum_k(q_k\,dp_k-p_k\,dq_k)$.
• The level. $H:V\to\mathbb{R}$ is smooth, every ray from $0$ meets $S=H^{-1}(1)$ exactly once, and $dH(x)x>0$ on $S$. The Reeb field is $R=X_H/\lambda_0(X_H)$ with $X_H=j_0\nabla H$, and $\xi_x=\ker\lambda_0(x)\cap\ker dH(x)$ is the contact plane.
• Symplectization. $\mathbb{R}\times S$ is identified with $V\setminus\{0\}$ by $(a,x)\mapsto e^{2a}x$. A smooth $J$ that is a $d\lambda_0$-compatible complex structure on each $\xi_x$ determines the almost complex structure $\tilde J$ on $V\setminus\{0\}$ with $\partial_a\mapsto R$, $R\mapsto-\partial_a$, and $J$ on $\xi$.
• Energy. For a map $u$ from an open $U\subseteq\mathbb{C}$, with $a$ and $w=\mathrm{proj}\circ u$ its two components, Hofer's energy is $E(u)=\sup_\varphi\int_Uu^*d(\varphi(a)\lambda_0)$ over smooth nondecreasing $\varphi:\mathbb{R}\to[0,1]$, and the $d\lambda$-energy is $\int_Uw^*d\lambda_0$.
• Finite-energy curves. Smooth maps $u:U\to V\setminus\{0\}$ with $\partial_su+\tilde J(u)\partial_tu=0$ and $E(u)<\infty$.
• Periodic Reeb orbits $P=(x,T)$, $T>0$ not necessarily minimal, the trivial cylinder $F_P(e^{2\pi(s+it)})=e^{2Ts}x(Tt)$, and the charge of a puncture: the limit of the actions $\int\lambda_0$ of the image loops of small clockwise circles around it.

Formalization targets

Goal: asymptotics of finite-energy punctured disks

Let $u$ be a finite-energy $\tilde J$-holomorphic curve on the punctured unit disk $D\setminus\{0\}$. Then either $u$ extends smoothly and $\tilde J$-holomorphically over $0$ with values in $V\setminus\{0\}$, or the charge $Q$ at $0$ exists and is nonzero, $a(u(z))\to\pm\infty$ as $z\to0$ with the sign of $Q$, and for every sequence $\rho_k\to0^+$ a subsequence of the loops $t\mapsto\mathrm{proj}\,u(\rho_ke^{-2\pi it})$ converges in $C^\infty$ to $t\mapsto x(Qt+c)$ for a periodic Reeb orbit $(x,|Q|)$ (Wendl, Theorem 9.8, without the nondegenerate and Morse–Bott clause and without the linear asymptotics of $a$ along the end).

Milestones

1. Structure of the symplectization. $\tilde J$ is a smooth almost complex structure on $V\setminus\{0\}$, invariant under $y\mapsto cy$; the radial coordinates are smooth (Hryniewicz § 2.2).
2. Reeb field. $\lambda_0(R)=1$ and $\omega_0(R,\cdot)=0$ on $TS$ (Hofer § 1).
3. Compatibility. $\omega_0$ is compatible with $\tilde J(y)$ for every $y\ne0$.
4. Energy densities. The energy integrands of finite-energy curves are nonnegative, $\int u^*d\lambda\le E(u)$, and $E(u)=0$ forces a constant map on a connected domain (Hryniewicz (17)).
5. Periods. The periods of periodic Reeb orbits on $S$ have a positive lower bound.
6. Hofer's lemma for continuous nonnegative functions on complete metric spaces (Wendl, Lemma 9.4).
7. Monotonicity. For $J$ on an open subset of a finite-dimensional space and $K$ compact, proper $J$-holomorphic maps into a small ball $B_r(p)$, $p\in K$, passing through $p$, have $\int\|Du\|^2\ge cr^2$ (Zinger, Proposition 3.12).
8. Removal of singularities for $J$-holomorphic punctured disks of finite energy with values in a compact set (Wendl, Theorem 9.2).
9. Zero $d\lambda$-energy, negative punctures. Such curves on $\mathbb{C}\setminus\Gamma$ are $F_P\circ p$ for a polynomial $p$ (Hryniewicz, Theorem 2.18).
10. Planes. Nonconstant finite-energy planes have positive $d\lambda$-energy (Hryniewicz, Corollary 2.19).
11. Cylinders. A nonconstant finite-energy cylinder with zero $d\lambda$-energy is $z\mapsto F_P(cz^k)$ (Wendl, Lemma 9.9).
12. Bubbling-off points. Gradient blow-up of curves with bounded energy concentrates $d\lambda$-energy at least the period of some Reeb orbit of period $\le$ the energy bound (Hryniewicz, Lemma 2.20).
13. Isolated orbits. If loops at a nonremovable puncture converge along one sequence of radii to an isolated orbit, they converge to it up to phase for all small radii (Wendl, Lemma 9.18).
14. Asymptotics of planes. A nonconstant finite-energy plane has a positive puncture at $\infty$ with charge equal to its $d\lambda$-energy (Hofer, Theorem 31).
15. Bridge to $\mathbb{R}^4$. For $n=1$, star-shapedness and periodic orbits agree with the HryniewiczCriterion setting, with period equal to action.

Significance

The results. The goal is the local half of SFT compactness and of the Fredholm theory of punctured curves: it says every finite-energy end is cylindrical over a Reeb orbit, which is what makes asymptotic operators, Conley–Zehnder indices and the index formula of the earlier missions applicable to actual curves. Milestones 9–14 (from Hofer, Hryniewicz and Wendl) describe planes, cylinders and bubbling in the form in which they enter Hofer's work on the Weinstein conjecture for $S^3$ and Hryniewicz's work on global surfaces of section; milestone 15 connects them to the open HryniewiczCriterion mission. Milestones 6–8 are general results about pseudoholomorphic maps into any finite-dimensional space.

Formalizing them. All results are classical and proved in the cited sources. None of them has been formalized in a proof assistant, as far as a literature search shows; Mathlib has no symplectizations, no Hofer energy and no Reeb dynamics. The mission produces these objects in general dimension $2n+2$, with the energies as lower Lebesgue integrals.

Difficulty

The target $V\setminus\{0\}$ is not compact and $\tilde J$ is not the standard structure, so the curves can escape to $0$ or to infinity; the goal has to decide which happens and produce a limit orbit, though the limit orbit is not assumed nondegenerate and may depend on the chosen sequence of radii. Hofer's energy is a supremum over a family of integrands rather than a single integral, and its finiteness does not bound the Euclidean area of the curve. The Euclidean size of the derivative grows with $e^{2a}$, so all scale-sensitive statements are made with the size $\|D(a\circ u)\|+\|D(\mathrm{proj}\circ u)\|$, which is invariant under $y\mapsto cy$. Milestones 7–8 hold for an arbitrary norm on the target and an almost complex structure defined only on an open set.

Formalization scope

• Namespace FiniteEnergyPlane; the definition module FiniteEnergyPlane_Setting imports JHolomorphic_Setting (the sixth mission) for IsAlmostComplexOn and IsJHolomorphicOn. The bridge item also imports HryniewiczCriterion_Basic.
• Space. $V$ is Fin (2 * (n + 1)) → ℝ with interleaved coordinates; $n=1$ matches HryniewiczCriterion.R4. Its default norm is the sup norm.
• Radial coordinates. scaleToS H y is the $r>0$ with $H(ry)=1$ (default $1$, used only at $y=0$), proj H y = scaleToS H y • y, aCoord H y = -½ log (scaleToS H y).
• Energies are ℝ≥0∞-valued lower integrals of ENNReal.ofReal of the integrands, so $E(u)<\infty$ is a genuine restriction (a Bochner integral would return $0$ on non-integrable integrands and make it vacuous).
• Punctures and loops. All finite punctures use clockwise loops $t\mapsto z_0+\rho e^{-2\pi it}$, and $\infty$ uses counterclockwise loops $t\mapsto Re^{2\pi it}$; at a negative puncture the limit $x(Qt+c)$ with $Q<0$ therefore runs the orbit backward. Removability requires an extension that avoids $0$.
• Not included. The statement in Wendl's Theorem 9.8 that $a\mp|Q|s$ converges in $C^\infty$ along the end, convergence for all radii at nondegenerate or Morse–Bott orbits, exponential convergence and the asymptotic eigenvector are left to a later mission.

Contributions welcome: general lemmas on lower integrals over planar domains and on radial projections to star-shaped hypersurfaces.

Selected references

• C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009 (2016), Lecture 9. https://arxiv.org/abs/1612.01009
• H. Hofer, Pseudoholomorphic curves in symplectizations with applications to the Weinstein conjecture in dimension three, Invent. Math. 114 (1993), 515–563. https://doi.org/10.1007/BF01232679
• U. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014), § 2.2. https://arxiv.org/abs/1105.2077
• A. Zinger, Notes on J-holomorphic maps, arXiv:1706.00331 (2017), §§ 3.3 and 5.1. https://arxiv.org/abs/1706.00331
• H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectisations I: Asymptotics, Ann. Inst. H. Poincaré Anal. Non Linéaire 13 (1996), 337–379. https://doi.org/10.1016/S0294-1449(16)30108-1

Motivation

An investor may care about reaching a target, avoiding a loss, or crossing an aspiration level rather than maximizing a concave function of final wealth. A target reward can jump from zero to one at a specified wealth. Such nonconcave utility is a natural model for goal-reaching portfolios, but its discontinuity changes what the associated Hamilton–Jacobi–Bellman equation can say at maturity. Portfolio bounds make the distinction sharper: an investor with finite leverage and short-sale limits cannot instantaneously smooth a jump in the payoff. Dai, Kou, Qian and Wan analyze this combination of nonconcavity, portfolio constraints, and a liquidation floor in their 2022 paper.

The paper proves a comparison principle and identifies the control value as the unique viscosity solution under a special terminal asymptotic condition. These are known mathematical results; this mission asks for their Lean proofs. The source is the authors' accepted manuscript, whose main theorem is Theorem 4.2 on printed page 12. The e-companion supplies boundary and terminal results supporting that theorem.

Setting

The market contains one risky stock and one riskless bond. After the paper's forward-wealth normalization, wealth $W_s$ started from $W_t=w$ follows

$$dW_s=W_s\pi_s(\eta\,ds+\sigma\,d\mathcal B_s),\qquad t\le s\le T.$$

Here $\eta$ is the excess stock return, $\sigma>0$ is volatility, $\mathcal B$ is Brownian motion, and $\pi_s$ is the fraction of wealth invested in the stock. Portfolio weights satisfy $d\le\pi_s\le u$, with $d\le0\le u$; either endpoint may be infinite. Wealth remains above the liquidation floor $B\ge0$. For utility $U$, the value function is

$$V(t,w)=\sup_{\pi\text{ admissible}}\mathbb E[U(W_T)\mid W_t=w].$$

Assumption 3.1 permits utility to be nondecreasing and right-continuous without being concave or continuous. For some $0<\hat p<1$, it eventually satisfies $U(w)\le w^{\hat p}$. At $w=B$ it either has a finite value or, when $B=0$, has the paper's CRRA form near zero. The second case includes logarithmic utility. These alternatives lead to different liquidation boundary conditions.

The formalized Hamiltonian is

$$H(w,p,A)=\sup_{d\le\pi\le u}\left\{\frac12\pi^2w^2\sigma^2A+\pi w\eta p\right\},$$

and the HJB equation is $-V_t-H(w,V_w,V_{ww})=0$ for $t<T$ and $w>B$. Definition A.1 tests upper and lower semicontinuous envelopes of candidate solutions against smooth functions and uses the corresponding envelopes $H^*$ and $H_*$. It also imposes the liquidation boundary condition and a terminal asymptotic condition. For bounded portfolio weights the terminal condition retains the jump of $U$ through the normal distribution function $\Phi$ and $L=\sigma\max\{u,-d\}$. For unbounded weights its target is the concave envelope $\hat U$.

Formalization targets

Value-function characterization

The goal is Theorem 4.2: for both bounded and unbounded portfolio intervals, the control value satisfies Definition A.1 and is continuous on $[0,T)\times(B,\infty)$. In the growth class used by Theorem 4.1, every other viscosity solution agrees with it:

$$V'(t,w)=V(t,w),\qquad 0<t<T,\quad w>B.$$

The goal keeps the actual stochastic-control supremum as $V$ and quantifies over competing solutions $V'$. It does not select a particular numerical method or a preferred proof. Theorem 4.1 gives comparison in this class. Proposition EC.3.2 gives the liquidation boundary behavior. Proposition EC.3.3 gives two terminal regimes, and Lemma EC.3.3 supplies the power-majorant statement used in the unbounded regime. The milestone list follows these stated results, specialized to the one-stock constant-coefficient model of the main theorem.

Significance

The characterization connects a portfolio optimization problem to an HJB equation even when the terminal utility jumps. It specifies the terminal behavior that distinguishes the bounded and unbounded portfolio regimes. In the bounded case a discontinuity can persist in the approach to maturity; in the unbounded case the limiting target is the concave envelope. The comparison statement then makes the characterization unique within the stated growth class. These conclusions are the analytical basis for the paper's later discussion of numerical schemes, although the numerical convergence theorem is outside this mission's scope (Dai et al., 2022, §§4 and EC.3).

A complete formalization would produce reusable definitions of the constrained control value, the extended-real Hamiltonian and its envelopes, and terminal limits for discontinuous payoffs. The paper's results are proved on paper but have no machine-checked proof in this proposal. The declarations here are compiled statements awaiting proofs. Independent work on the comparison theorem, boundary behavior, terminal asymptotics, and supporting real analysis can proceed against the same definition layer.

Difficulty

The usual terminal condition $V(T,w)=U(w)$ does not describe the limit of $V(t,\zeta)$ as $(t,\zeta)$ approaches $(T,w)$ when $U$ jumps. Replacing the limit by $U(w)$ would erase the singular behavior that the paper studies. The bounded-portfolio condition instead depends on the left limit $U(w-)$, the size of the jump, and the scaled quantity $\log(\zeta/w)/\sqrt{T-t}$. A viscosity comparison argument must handle this terminal profile while the Hamiltonian itself can be infinite or discontinuous in the unbounded portfolio regime. The liquidation boundary has a separate CRRA asymptotic when utility diverges at zero. Each of these clauses is part of the solution concept and must remain compatible with the value function.

Formalization scope

The Lean market stores $\eta,\sigma,T,B$ as real numbers and $d,u$ as extended real endpoints. It assumes $\sigma>0$, $T>0$, $B\ge0$, $d\le0\le u$, and at least one nonzero admissible weight. The last three inequalities include the paper's standing bounds and exclude $L=0$. Admissible controls are progressively measurable, obey the bounds and liquidation floor, satisfy the integral wealth equation through a Brownian Itô integral, and have integrable terminal utility. The supremum of their expectations is extended real so an infinite value is preserved; the goal explicitly proves finiteness before converting it to a real value. Brownian motions are quantified over filtered probability spaces and have independent future increments relative to their filtration.

The PDE domain is $D=[0,T)\times(B,\infty)$. Semicontinuous envelopes and boundary and terminal limits approach within $D$. Smooth tests are $C^\infty$ real functions. The Hamiltonian and its envelopes are extended real; finite-width expressions involving $L$ are used only under bounded portfolio endpoints. The terminal point $w=B$ is included only for the finite-utility boundary branch, where the source defines $U(B-)=U(B)$. The CRRA formula uses a logarithmic branch at zero power, avoiding division by zero. These commitments rule out a vacuous solution notion or a value function defined as an arbitrary viscosity solution. Proving the control value finite, nontrivial comparison, and both terminal limits remains part of the mission. The e-companion's multivariate statements are included only in the one-stock constant-coefficient specialization used by Theorems 4.1–4.2.

Selected references

• M. Dai, S. Kou, S. Qian and X. Wan, Nonconcave utility maximization with portfolio bounds, Management Science 68(11), 8368–8385, 2022. DOI: 10.1287/mnsc.2021.4228. This mission cites the authors' accepted manuscript, including its e-companion.

Motivation: uniqueness of weak Boltzmann solutions

The Boltzmann equation describes a dilute gas through a density $F(t,x,v)$ of particles at position $x$ with velocity $v$, evolving by free transport and binary collisions. For hard spheres, the collision rate is proportional to the normal relative speed. In 1989 DiPerna and Lions constructed global renormalized solutions for all initial data with finite mass, energy and entropy, and weak stability holds at the same level. Existence and stability do not give uniqueness, though: the physical bounds do not even make the quadratic collision term locally integrable, and the uniqueness of general renormalized solutions is a basic question in kinetic theory (Silvestre 2022, §2). Uniqueness is known only under much stronger assumptions, such as Maxwellian upper bounds or closeness to equilibrium.

Timeline

• 1974 — Ukai: global existence and uniqueness near a Maxwellian for periodic cutoff hard potentials (Proc. Japan Acad. 1974).
• 1978 — Kaniel and Shinbrot: uniqueness and local existence under Maxwellian upper bounds (CMP 1978).
• 1988 — Golse, Lions, Perthame and Sentis: velocity averaging lemmas (JFA 1988).
• 1989 — DiPerna and Lions: global renormalized solutions and weak stability (Ann. of Math. 1989); the entropy inequality follows in 1991 (ARMA 1991).
• 1999 — For the spatially homogeneous hard-sphere equation, Mischler and Wennberg prove uniqueness among conservative solutions with finite mass and energy (Ann. IHP C 1999); Wennberg gives homogeneous nonuniqueness examples in which the energy increases (J. Stat. Phys. 1999).
• 2010 — Levermore and Masmoudi give a periodic formulation of renormalized solutions relative to a Maxwellian (ARMA 2010).
• 2024–2026 — Ill-posedness results: Chen–Holmer for the constant kernel (Ann. PDE 2024), Chen–Guo–Shen–Zhang for hard spheres in Gaussian-weighted $L^2_vH^s_x$ (arXiv:2606.01331). Gismondi, Golding and Novack conjecture nonuniqueness of renormalized inhomogeneous Landau and Boltzmann solutions for a dense class of data (arXiv:2608.13758).
• 2026 — An OpenAI preprint, Nonuniqueness for the periodic hard-sphere Boltzmann equation (OpenAI Math Release, September 23, 2026), claims a single finite-entropy datum on $\mathbb T^3\times\mathbb R^3$ with two distinct admissible solutions. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Phase space is $\Omega=\mathbb T^3_x\times\mathbb R^3_v$, with $\mathbb T^3=\mathbb R^3/\mathbb Z^3$. For incoming velocities $v,v_*$ and a collision normal $\omega\in S^2$, put $a=(v-v_*)\cdot\omega$, $v'=v-a\omega$, $v_*'=v_*+a\omega$. The hard-sphere collision operator is

$$Q(F,F)(v)=\int_{\mathbb R^3\times S^2}|a|\,\big(F(v')F(v_*')-F(v)F(v_*)\big)\,dv_*\,d\omega ,$$

with ordinary surface measure on $S^2$; the two terms are the gain and the loss. The Cauchy problem is $(\partial_t+v\cdot\nabla_x)F=Q(F,F)$, $F(0)=F_0$. An initial datum has finite entropy if it is nonnegative and $\int_\Omega F_0(1+|v|^2+|\log F_0|)<\infty$.

A solution is admissible (Definition 2.1 of the source) if, with $M(v)=(2\pi)^{-3/2}e^{-|v|^2/2}$:

• it is renormalized: the equation holds weakly for $M\beta(F/M)$ for every $C^1$ $\beta$ with $\beta(0)=0$ and $|\beta'(z)|\le C_\beta/(1+z)$, and the separately renormalized gain and loss are integrable on bounded time intervals;
• it is weakly continuous in $L^1$ against every bounded measurable test and takes the initial value $F_0$;
• mass, energy and absolute entropy stay bounded on bounded time intervals;
• it conserves local mass and total momentum, and satisfies the energy inequality and the relative-entropy inequality with the full entropy dissipation at every time.

Formalization targets

Goal: two admissible solutions from one datum (Theorem 1.1)

There is a nonnegative finite-entropy datum $F_0$ with bounded velocity support, two admissible global solutions $F,G$ with initial datum $F_0$, and a time $T>0$ such that

$$F,G\in C([0,T];L^1(\Omega)),\qquad Q^\pm(F),\,Q^\pm(G)\in L^1([0,T]\times\Omega),\qquad F(t)\neq G(t)\ \text{in } L^1 \text{ for some } t\in[0,T].$$

This is Theorem 1.1 of the source (p. 3), with the difference placed in the common interval of strong continuity, which is where the source establishes it. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. If the source's proof is correct, the theorem shows that the DiPerna–Lions framework, even with local mass conservation, momentum conservation and the energy and entropy inequalities retained, does not determine the evolution uniquely. The example is spatially inhomogeneous and periodic, and the two solutions start from exactly the same datum, unlike ill-posedness results that compare nearby data. On the interval where they differ, both solutions satisfy the unrenormalized equation. The datum has bounded velocities but unbounded amplitudes concentrated at smaller and smaller spatial scales, which points to the kind of extra control a uniqueness theorem has to impose.

Formalizing it. The statement fixes a long list of admissibility conditions. Its definitions are a useful contribution in their own right: renormalized solutions, entropy dissipation and kinetic test functions on the torus are not in Mathlib. The 65-page proof (colored decompositions, Carleman representation, velocity averaging, a dilation limit and a branching analysis) is a long-term target. Its propositions are natural milestones.

Difficulty

Constructing two different weak limits is not the hard part: approximations with and without a small "hot seed" give two candidate solutions. The difficulty is to show that they really differ. A vanishing seed can produce a hit on the a priori cap that carries arbitrarily little mass, and weak compactness can erase it in the limit. The source must rule out this loss of information uniformly as the cold velocity distributions collapse onto an axis, where the weight controlling the hot density is singular. At the same time every admissibility condition, including the entropy-dissipation inequality and local mass conservation, has to survive the limits. Energy-increasing constructions (Wennberg) and homogeneous examples do not meet these constraints.

Formalization scope

• Velocities live in EuclideanSpace ℝ (Fin 3), positions in Fin 3 → AddCircle 1, and densities are real functions on phase space. The sphere carries (volume).toSphere, which is ordinary surface area, not a probability measure.
• gain and loss are Bochner integrals. To prevent them from silently returning $0$ on non-integrable fibers, AdmissibleGlobal requires fiberwise integrability and space-time integrability of the renormalized gain and loss.
• AdmissibleGlobal f₀ F encodes Definition 2.1: finite entropy at each time, a.e. initial value, weak continuity against bounded measurable tests, uniform moment bounds, the renormalized equation for all Renormalization $\beta$ and all smooth periodic KineticTest $\varphi$, local mass conservation against MassTest, total momentum conservation, the energy inequality, and the entropy inequality in ℝ≥0∞ with the lower semicontinuous extension of $(A-B)\log(A/B)$.
• StrongEarly T F adds $T>0$, strong $L^1$ continuity on $[0,T]$ via eLpNorm, and integrability of gain and loss on $[0,T]$. Distinctness is ¬ (F t =ᵐ G t) for some $t\in[0,T]$.
• Infrastructure needed: averaging lemmas, renormalized-solution compactness, the Carleman representation, and estimates on free transport on the torus. Contributions to any of these are welcome.

Selected references

• R. J. DiPerna and P.-L. Lions, On the Cauchy problem for Boltzmann equations: global existence and weak stability, Ann. of Math. 130 (1989), 321–366. https://doi.org/10.2307/1971423
• R. J. DiPerna and P.-L. Lions, Global solutions of Boltzmann's equation and the entropy inequality, Arch. Ration. Mech. Anal. 114 (1991), 47–55. https://doi.org/10.1007/BF00375684
• C. D. Levermore and N. Masmoudi, From the Boltzmann equation to an incompressible Navier–Stokes–Fourier system, Arch. Ration. Mech. Anal. 196 (2010), 753–809. https://doi.org/10.1007/s00205-009-0254-5
• L. Silvestre, Regularity estimates and open problems in kinetic equations, arXiv:2204.06401 (2022). https://doi.org/10.48550/arXiv.2204.06401
• S. Kaniel and M. Shinbrot, The Boltzmann equation. I. Uniqueness and local existence, Comm. Math. Phys. 58 (1978), 65–84. https://doi.org/10.1007/BF01624788
• S. Ukai, On the existence of global solutions of mixed problem for non-linear Boltzmann equation, Proc. Japan Acad. 50 (1974), 179–184. https://doi.org/10.3792/pja/1195519027
• S. Mischler and B. Wennberg, On the spatially homogeneous Boltzmann equation, Ann. Inst. H. Poincaré C 16 (1999), 467–501. https://doi.org/10.1016/S0294-1449(99)80025-0
• B. Wennberg, An example of nonuniqueness for solutions to the homogeneous Boltzmann equation, J. Stat. Phys. 95 (1999), 469–477. https://doi.org/10.1023/A:1004546031908
• F. Golse, P.-L. Lions, B. Perthame and R. Sentis, Regularity of the moments of the solution of a transport equation, J. Funct. Anal. 76 (1988), 110–125. https://doi.org/10.1016/0022-1236(88)90051-1
• X. Chen and J. Holmer, Well/ill-posedness bifurcation for the Boltzmann equation with constant collision kernel, Ann. PDE 10 (2024), Art. 14. https://doi.org/10.1007/s40818-024-00177-w
• X. Chen, Y. Guo, S. Shen and Z. Zhang, Sharp $H^s_x$ ill-posedness of the hard-sphere Boltzmann equation, arXiv:2606.01331 (2026). https://doi.org/10.48550/arXiv.2606.01331
• N. Gismondi, W. Golding and M. Novack, A sharp rigidity/flexibility threshold for the isotropic Landau equation, arXiv:2608.13758 (2026). https://doi.org/10.48550/arXiv.2608.13758
• OpenAI, Nonuniqueness for the periodic hard-sphere Boltzmann equation, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 3; Definition 2.1, p. 8). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Nonuniqueness-for-the-periodic-hard-sphere-Boltzmann-equation-September-23-2026/paper.pdf

Motivation: curvature conditions in optimal transport on manifolds

In optimal transport on a Riemannian manifold with the quadratic cost $c(x,y)=d(x,y)^2/2$, the regularity of optimal maps is governed by a fourth-order curvature quantity of the cost, the Ma–Trudinger–Wang (MTW) tensor. Its nonnegativity on orthogonal pairs, the weak MTW condition (A3w), is necessary for continuity of optimal maps, and together with convexity of the tangent injectivity domains it yields the global geometric "supporting" properties used in regularity theory. Whether weak MTW by itself forces those injectivity domains to be convex was proposed by Villani and proved previously only under a nonfocality assumption, which excludes cut points that are also conjugate points.

Background

• 2005 — Ma, Trudinger and Wang introduce a strictly positive curvature condition for regularity of transport potentials (MTW 2005).
• 2009 — Trudinger and Wang treat the degenerate nonnegative form A3w (TW 2009); Loeper proves necessity for continuity and the supporting-mountain principle (Loeper 2009).
• 2010 — Loeper and Villani connect MTW to cut-locus geometry, proving convexity under strong MTW and nonfocality (Loeper–Villani 2010); Kim and McCann give a geometric formulation and a double-mountain principle (Kim–McCann 2010); Figalli's Bourbaki survey (Astérisque 332, 2010).
• 2011 — Figalli, Rifford and Villani derive the global supporting principle from weak MTW plus convex injectivity domains (FRV 2011); Villani proposes that weak MTW alone should force convexity of every tangent injectivity domain (Villani 2011, §4.2).
• 2015 — Figalli, Gallouët and Rifford prove that implication on nonfocal manifolds (FGR 2015, Thm 1.7).
• 2026 — An OpenAI preprint, Global Support and Convex Injectivity Domains under Weak MTW (OpenAI Math Release, September 25, 2026), claims the implication on every smooth compact connected Riemannian manifold of dimension $n\ge2$, with conjugate cut points allowed. It has not been peer reviewed and its theorems are not formally verified.

Setting

Let $(M,g)$ be a smooth, connected, compact Riemannian manifold without boundary, of dimension $n\ge2$, with geodesic distance $d$ and exponential map $\exp_x:T_xM\to M$. The open tangent injectivity domain at $x$ is

$$I(x)=\{v\in T_xM:\ d(x,\exp_x(av))=a|v|_x\ \text{for some } a>1\},$$

the set of velocities whose geodesic is still minimizing slightly beyond time one. With $c(x,y)=d(x,y)^2/2$, the MTW quantity at $v\in I(x)$ is

$$\mathfrak S_{(x,v)}(\xi,\eta)=-\frac32\,\frac{\partial^4}{\partial s^2\,\partial t^2}\,c\big(\exp_x(t\xi),\exp_x(v+s\eta)\big)\Big|_{s=t=0},$$

and weak MTW means $\mathfrak S_{(x,v)}(\xi,\eta)\ge0$ whenever $\langle\xi,\eta\rangle_x=0$, for all $x$ and $v\in I(x)$. No nonfocality, strict positivity, or prior convexity is assumed.

In Lean, $M$ is a Mathlib Riemannian manifold modelled on EuclideanSpace ℝ (Fin n) (so without boundary), with CompactSpace, ConnectedSpace and IsRiemannianManifold linking the metric-space distance to the Riemannian metric. exp x v is the time-one point of a smooth curve with initial point $x$, initial velocity $v$, and locally constant-speed distance-realizing behaviour; mtw is the iterated one-variable derivative formula above.

Formalization targets

Goal: convexity of injectivity domains

If $(M,g)$ satisfies weak MTW, then for every $x\in M$, every $v_0,v_1\in I(x)$ and $\theta\in[0,1]$,

$$(1-\theta)v_0+\theta v_1\in I(x),$$

i.e. $I(x)$ is convex. This is Theorem 1.1 of the source. The goal is published on the platform with status Open.

Significance

The result itself. Combined with the Figalli–Rifford–Villani supporting principle, convexity of injectivity domains under weak MTW alone removes an extra geometric hypothesis from the regularity theory of optimal transport on compact manifolds, and covers focal manifolds where minimizing geodesics may reach conjugate cut points. The source also proves a global supporting property, convexity of lifted gap sections, and uniform $C^{1,1}$ intermediate-time geometry (Theorem 1.2), which feed the companion preprint on bi-Hölder regularity of transport maps.

Formalizing it. The statement uses only geodesics, distance and a four-fold derivative of the squared distance, so it can be phrased with current Mathlib Riemannian infrastructure. A proof needs nonsmooth analysis of the distance function near the cut locus, semiconvex potentials and their subdifferentials, and a continuity (degree) argument; this layer would be reusable for other cut-locus results.

Difficulty

The cost $c$ is smooth only before the cut locus, while convexity of $I(x)$ concerns segments whose interior points might a priori leave the region where $\mathfrak S$ is defined. Weak MTW controls the cost Hessian only in directions perpendicular to a velocity segment and gives no strict inequality. Smooth-cost concavity arguments therefore cannot be applied beyond their domain, and nonfocality — the assumption that cut points are reached strictly before conjugate points — is exactly what earlier proofs used to keep the cost smooth along the segment.

Formalization scope

• exp is defined through complete geodesics with prescribed initial data (ContMDiff curve, mfderiv at $0$ equal to $v$, locally $d(\gamma s,\gamma r)=|v|\,|s-r|$); on a compact manifold such a geodesic exists and is unique, so the Classical.choose fallback is never used.
• injectivityDomain matches $I(x)$ exactly; mtw uses iterated deriv, which is the true fourth derivative wherever the cost is smooth (the case $v\in I(x)$, near $s=t=0$).
• The hypothesis quantifies over all $x$, all $v\in I(x)$, and all $g_x$-orthogonal $\xi,\eta$; the conclusion is Convex ℝ (injectivityDomain x) for every $x$.
• Dimension $n\ge2$, compactness and connectedness are explicit hypotheses; boundaryless-ness comes from the Euclidean model.
• Needed infrastructure: Hopf–Rinow and uniqueness of geodesics, first and second variation, semiconcavity of the distance squared, cut and conjugate locus theory.

Selected references

• X.-N. Ma, N. S. Trudinger and X.-J. Wang, Regularity of potential functions of the optimal transportation problem, Arch. Ration. Mech. Anal. 177 (2005), 151–183. https://doi.org/10.1007/s00205-005-0362-9
• N. S. Trudinger and X.-J. Wang, On the second boundary value problem for Monge–Ampère type equations and optimal transportation, Ann. Sc. Norm. Super. Pisa 8 (2009), 143–174. https://doi.org/10.2422/2036-2145.2009.1.07
• G. Loeper, On the regularity of solutions of optimal transportation problems, Acta Math. 202 (2009), 241–283. https://doi.org/10.1007/s11511-009-0037-8
• G. Loeper and C. Villani, Regularity of optimal transport in curved geometry: the nonfocal case, Duke Math. J. 151 (2010), 431–485. https://doi.org/10.1215/00127094-2010-003
• Y.-H. Kim and R. J. McCann, Continuity, curvature, and the general covariance of optimal transportation, J. Eur. Math. Soc. 12 (2010), 1009–1040. https://doi.org/10.4171/JEMS/221
• A. Figalli, Regularity of optimal transport maps [after Ma–Trudinger–Wang and Loeper], Séminaire Bourbaki 2008/2009, Astérisque 332 (2010), 341–368.
• A. Figalli, L. Rifford and C. Villani, Necessary and sufficient conditions for continuity of optimal transport maps on Riemannian manifolds, Tohoku Math. J. 63 (2011), 855–876. https://doi.org/10.2748/tmj/1325886291
• C. Villani, Regularity of optimal transport and cut locus: from nonsmooth analysis to geometry to smooth analysis, Discrete Contin. Dyn. Syst. 30 (2011), 559–571. https://doi.org/10.3934/dcds.2011.30.559
• A. Figalli, T. O. Gallouët and L. Rifford, On the convexity of injectivity domains on nonfocal manifolds, SIAM J. Math. Anal. 47 (2015), 969–1000. https://doi.org/10.1137/140961821
• OpenAI, Global Support and Convex Injectivity Domains under Weak MTW, OpenAI Math Release preprint, September 25, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Global-Support-and-Convex-Injectivity-Domains-under-Weak-MTW-September-25-2026/paper.pdf

Motivation

The Ising mixed $p$-spin model assigns to each configuration $\sigma \in \{-1,+1\}^N$ the energy of a random polynomial whose covariance is $\mathbb E\{H_N(\sigma)H_N(\sigma')\} = N\xi(\langle\sigma,\sigma'\rangle/N)$. Its ground-state energy $\max_\sigma H_N(\sigma)/N$ converges to the value of a variational problem, the zero-temperature Parisi formula (Auffinger–Chen 2017), in which a functional $\mathsf P$ is minimized over non-decreasing order parameters $\gamma$. El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) ask how close a polynomial-time algorithm can get to this maximum. Their answer is an extended variational principle: the best value reachable by incremental approximate message passing is $\inf_{\gamma\in\mathscr L}\mathsf P(\gamma)$, where the space $\mathscr L$ drops the monotonicity constraint.

The algorithm that reaches this value is built from a minimizer $\gamma_*$ of $\mathsf P$ over $\mathscr L$, and it runs along the set of times where $\gamma_*$ is positive. Theorem 5 of the paper (p. 30) shows that this set is dense: a minimizer has full support. This mission formalizes that theorem and the first- and second-order optimality conditions it rests on (Section 6.1, pp. 22–31).

Timeline. Parisi proposed the variational formula in 1979. Talagrand (2006) and Panchenko (2013) proved it at positive temperature. Auffinger and Chen (2017) established the zero-temperature version with $\Phi(1,x)=|x|$ and proved that a minimizer over the monotone space exists. Jagannath and Tobasco (2016) developed the PDE and SDE tools for the Parisi functional that Section 6.1 of the present paper adapts to non-monotone order parameters. Montanari (2019) gave the first message passing algorithm for the Sherrington–Kirkpatrick case; the present paper (2020) extended it to general mixtures and introduced $\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$; its derivatives $\xi'$, $\xi''$ are the termwise differentiated power series, non-negative and non-decreasing on $[0,1]$.

An order parameter is a function $\gamma : [0,1) \to \mathbb R_{\ge0}$. The extended space is

$$\mathscr L = \Bigl\{\gamma : [0,1)\to\mathbb R_{\ge0} : \|\xi''\gamma\|_{\mathrm{TV}[0,t]}<\infty\ \forall t\in[0,1),\ \int_0^1\xi''(t)\gamma(t)\,dt<\infty\Bigr\},$$

with the weighted distance $\|\gamma_1-\gamma_2\|_{1,\xi''} = \int_0^1\xi''(t)|\gamma_1(t)-\gamma_2(t)|\,dt$. The non-negative step functions $\mathsf{SF}_+$ are the finite sums $\sum_i a_i\mathbb I_{[t_{i-1},t_i)}$ with $0=t_0<\dots<t_m=1$ and $a_i\ge0$.

For a terminal condition $f_0$ (convex, continuous, even, non-negative, differentiable off $0$ with $0\le f_0'\le1$ on $(0,\infty)$) and $\gamma\in\mathsf{SF}_+$, the Parisi PDE

$$\partial_t\Phi + \tfrac12\xi''(t)\bigl(\partial_x^2\Phi + \gamma(t)(\partial_x\Phi)^2\bigr) = 0,\qquad \Phi(1,x) = f_0(x),$$

has the explicit Cole–Hopf solution $\Phi^\gamma$: on $[t_{i-1},t_i)$, $\Phi(t,x) = \gamma_i^{-1}\log\mathbb E\exp\{\gamma_i\Phi(t_i, x+\sqrt{\xi'(t_i)-\xi'(t)}\,G)\}$ with $G\sim\mathsf N(0,1)$. For $\gamma\in\mathscr L$, $\Phi^\gamma$ is the limit of $\Phi^{\gamma_n}$ along step functions $\gamma_n\to\gamma$ in the weighted distance. The Parisi functional is

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

Given a Brownian motion $B$, the process $X$ solves $dX_t = \xi''(t)\gamma(t)\,\partial_x\Phi^\gamma(t,X_t)\,dt + \sqrt{\xi''(t)}\,dB_t$, $X_0 = 0$. The support of $\gamma$ is $S(\gamma) = \{t\in[0,1):\gamma(t)>0\}$, and $\overline S(\gamma)$ is its closure in $[0,1)$.

Formalization targets

Goal: Theorem 5

With $f_0(x) = |x|$, if $\gamma_*\in\mathscr L$ satisfies $\mathsf P(\gamma_*) = \inf_{\gamma\in\mathscr L}\mathsf P(\gamma)$, then

$$\overline S(\gamma_*) = [0,1).$$

Milestones

The path to the goal, in attack order:

• Proposition 6.1(b),(c): on step functions, $\partial_x\Phi$ is non-decreasing with $|\partial_x\Phi|\le1$, and $\|\Phi^{\gamma_1}-\Phi^{\gamma_2}\|_\infty\le\|\xi''(\gamma_1-\gamma_2)\|_1$.
• Lemma 6.2: these properties pass to $\gamma\in\mathscr L$.
• Lemma 6.5: the SDE has a unique strong solution on $[0,1]$.
• Corollary 6.6: $\mathbb E\{\partial_x\Phi(t_2,X_{t_2})^2\}-\mathbb E\{\partial_x\Phi(t_1,X_{t_1})^2\}=\int_{t_1}^{t_2}\xi''(s)\,\mathbb E\{(\partial_x^2\Phi(s,X_s))^2\}\,ds$.
• Lemma 6.7: the map $t\mapsto\mathbb E\{\partial_x^2\Phi(t,X_t)^2\}$ is continuous on $[0,1)$.
• Proposition 6.8: the first variation $\frac{d}{ds}\mathsf P(\gamma+s\delta)|_{s=0+}=\frac12\int_0^1\xi''\delta\,(\mathbb E\{\partial_x\Phi(t,X_t)^2\}-t)\,dt$.
• Lemma 6.9: $S(\gamma)$ is a countable disjoint union of intervals.
• Corollary 6.10: $\mathbb E\{\partial_x\Phi^{\gamma_*}(t,X_t)^2\}=t$ on $\overline S(\gamma_*)$ and $\ge t$ off it.
• Corollary 6.11: $\xi''(t)\,\mathbb E\{\partial_x^2\Phi^{\gamma_*}(t,X_t)^2\}=1$ on $\overline S(\gamma_*)$.
• Lemma 6.12: the law of $X_t$ has a density, bounded below on compact sets, once $\gamma$ vanishes.

Significance

The result. Full support identifies the extended variational principle as one whose minimizers are "nowhere flat". The algorithm of Theorem 3 in the paper follows $\gamma_*$ through incremental steps whose size is set by $\gamma_*$, and it needs no special treatment of gaps where $\gamma_* = 0$. The stationarity conditions (Corollaries 6.10–6.11) also characterize minimizers over $\mathscr L$ the way the Auffinger–Chen conditions characterize minimizers over the monotone space. They are the starting point for comparing $\inf_{\mathscr L}\mathsf P$ with the Parisi value.

Formalizing it. The theorem is proved in the paper; nothing here is open mathematics. The paper's proofs rely on cited PDE regularity (Jagannath–Tobasco 2016) and on standard SDE theory, often in one line. The mission produces a machine-checked chain from the explicit Cole–Hopf formula to the support theorem. Along the way it builds the Parisi PDE solution on a non-monotone class, a first-variation formula, and stationarity conditions, none of which have a formal counterpart. No formal statement of the Parisi functional or the Parisi PDE exists on Prove2Me (index search, 2026-10-03).

Difficulty

Two steps resist a direct argument. The first is the first variation (Proposition 6.8): differentiating $\Phi^\gamma(0,0)$ in $\gamma$ requires comparing the SDE for $\gamma$ with the SDE for the perturbed parameter and controlling their difference uniformly, which needs bounds on $\partial_x^2\Phi$ that degenerate as $t\to1$. The second is the exclusion of gaps: on an interval where $\gamma_*=0$ the PDE is a time-changed heat equation, and the contradiction comes from a strict inequality, which requires the law of $X_t$ to charge every interval (Lemma 6.12). The obvious idea of perturbing $\gamma_*$ upward on a gap only yields the inequality (6.14), which is consistent with a gap; the second-order identity at the gap's endpoints is what closes the argument.

Formalization scope

Conventions committed to in Lean:

• The mixture is a coefficient sequence $c$ with $c_0=c_1=0$; $\xi,\xi',\xi''$ are explicit series.
• Order parameters are functions $\mathbb R\to\mathbb R$ read only on $[0,1)$. Membership in $\mathscr L$ uses eVariationOn for the total variation and IntegrableOn for the integral; the latter includes the a.e.-measurability that the paper takes for granted.
• $\Phi^\gamma$ for step functions is the Cole–Hopf recursion (7.3). For a piece with $\gamma_i = 0$ the formula's limit, the heat semigroup, is used instead of a division by zero. $\mathbb E$ over $G$ is integration against gaussianReal 0 1. For $\gamma\in\mathscr L$, $\Phi^\gamma$ is a limit along the filter of step functions converging in the weighted $L^1$ distance; it is never "some solution of the PDE".
• $\partial_x\Phi$ and $\partial_x^2\Phi$ are iterated derivs in $x$. Lemma 6.2's weak-derivative claim is stated as "convex and 1-Lipschitz", its equivalent.
• The SDE uses the published strong-solution concept EthierKurtz.SolvesBrownianSDE in dimension one, with coefficients extended by zero after time $1$. The driver is assumed to be a standard Brownian motion (IsBrownianReal). Statements about $X$ hold for every strong solution, which by Lemma 6.5 is unique.
• Section 6.1's results are stated for every admissible $f_0$; $\mathsf P$ is parametrized by $f_0$, and Theorem 5 fixes $f_0=|\cdot|$.
• Minimality is "$\mathsf P(\gamma_*)\le\mathsf P(\gamma)$ for all $\gamma\in\mathscr L$", never a real infimum. $\overline S(\gamma)$ is closure (S γ) ∩ Ico 0 1. Right-continuity of $\gamma_*$, the paper's convention from p. 28, is a hypothesis.
• Disclosed hypothesis $\xi\not\equiv0$ (some $c_k\neq0$) on Theorem 5, Corollaries 6.10–6.11 and Lemma 6.12. For $\xi\equiv0$ every $\gamma$ minimizes $\mathsf P$ and $X\equiv0$, so $\gamma_*\equiv0$ has empty support and each of those statements fails. When $c_2=0$ no minimizer exists (Corollary 6.11 at $t=0$), and Theorem 5 is vacuous, as in the paper.
• Lemma 6.12's density bound is stated without choosing density versions: $\varepsilon\,\mathrm{Leb}(A)\le\mathbb P(X_t\in A)$ for measurable $A\subseteq[-M,M]$.

A trivializing formalization is excluded: $\Phi^\gamma$ and $X$ are the paper's objects, built from the data, so the goal cannot be met by choosing a convenient solution, and minimality over $\mathscr L$ cannot be satisfied by a junk infimum.

Not formalized: the weak formulation (6.4) of Lemma 6.2, printed with a wrong boundary term; the stochastic-integral identity (6.7) of Lemma 6.5; the regularity Lemmas 6.3–6.4; Proposition 6.1(a). The paper's algorithmic Theorems 2–4 are out of scope, because they concern algorithms in an informal model of computation and an AMP state-evolution theory that is not part of this mission.

Useful infrastructure beyond this mission: the Cole–Hopf solution and its Lipschitz dependence on $\gamma$, the Parisi functional on $\mathscr L$, and the SDE (6.3). Contributions that formalize Itô's formula for these processes or the regularity of $\Phi^\gamma$ are welcome as supporting lemmas.

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, Annals of Probability, 2017. https://arxiv.org/abs/1606.05335
• A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proceedings of the AMS, 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, Annals of Mathematics 163(1), 2006. https://doi.org/10.4007/annals.2006.163.221
• D. Panchenko, The Parisi ultrametricity conjecture, Annals of Mathematics 177(1), 2013. https://doi.org/10.4007/annals.2013.177.1.8

Motivation

Feedback laws in engineering are applied with a lag: sensors, actuators and communication channels introduce a time delay $\tau$ between the measurement of a state and the control that reacts to it. For finite-dimensional systems small delays are usually harmless. For distributed systems such as the wave equation they need not be: Datko, Lagnese and Polis (SIAM J. Control Optim. 24, 1986) and Datko (SIAM J. Control Optim. 26, 1988) showed, for one-dimensional examples, that an arbitrarily small delay in a stabilizing feedback can destroy stability. The question matters to anyone who designs boundary or internal controllers for vibrating structures and wants to know whether a stabilizing law is robust to delay.

Nicaise and Pignotti (SIAM J. Control Optim. 45 (2006)) study the wave equation on a bounded domain of $\mathbb R^n$ with a damping term that combines an instantaneous and a delayed velocity feedback, with coefficients $\mu_1$ and $\mu_2$. They show that the system is exponentially stable when $\mu_2 < \mu_1$ (Theorems 1.1 and 1.3), and that when $\mu_2 \ge \mu_1$ stability can fail (Theorems 1.2 and 1.4). This mission is Theorem 1.4, the internal-damping instability result, in the case the paper proves.

• 1986–1988: Datko, Lagnese and Polis; Datko — destabilization by small delays in one-dimensional boundary-damped wave equations.
• 2006: Nicaise and Pignotti — the multi-dimensional dichotomy $\mu_2 < \mu_1$ (stability) versus $\mu_2 \ge \mu_1$ (instability for some delays), for boundary and internal feedback.

Setting

Let $n \ge 1$ and let $\Omega \subset \mathbb R^n$ 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 and $\partial u/\partial\nu$ for the normal derivative. Let $\mu_1 > 0$, $\mu_2 > 0$ and let $\tau > 0$ be the delay. With damping coefficient $a \equiv 1$ the problem is

$$u_{tt}(x,t) - \Delta u(x,t) + \mu_1 u_t(x,t) + \mu_2 u_t(x,t-\tau) = 0 \quad \text{in } \Omega \times (0,\infty),$$ $$u = 0 \ \text{ on } \Gamma_D \times (0,\infty), \qquad \frac{\partial u}{\partial\nu} = 0 \ \text{ on } \Gamma_N \times (0,\infty),$$

with initial data $u(\cdot,0) = u_0$, $u_t(\cdot,0) = u_1$ and a history $u_t = g_0$ on $\Omega \times (-\tau, 0)$. The standard energy of a solution is

$$\mathcal E(t) = \frac12 \int_\Omega \big\{ |u_t(x,t)|^2 + |\nabla u(x,t)|^2 \big\}\,dx .$$

The condition $\mu_2 < \mu_1$ is the paper's assumption (1.8). The paper's problem (1.12)–(1.16) carries a general coefficient $a \in L^\infty(\Omega)$ with $a \ge 0$ and $a > a_0 > 0$ near $\Gamma_N$; $a \equiv 1$ is one such coefficient.

Formalization targets

Goal: Theorem 1.4 for $a \equiv 1$

If (1.8) fails, i.e. $0 < \mu_1 \le \mu_2$, then

$$\forall \varepsilon > 0\ \exists \tau \in (0,\varepsilon)\ \exists u \text{ solving the problem with delay } \tau:\ \ \mathcal E(t) \not\to 0 \ (t \to \infty),$$

and the same holds with "$\tau \in (0,\varepsilon)$" replaced by "$\tau > M$", for every $M$. The goal asserts only non-decay, not a rate of growth or the value of the energy, so it survives any sharpening of the examples.

Milestones

1. (5.21)–(5.23): if $\varphi$ is an eigenfunction of the mixed Dirichlet–Neumann Laplacian, $\Delta\varphi = -\Lambda^2\varphi$, and $\lambda \in \mathbb C$ solves $\lambda^2 + (\mu_1 + \mu_2 e^{-\lambda\tau})\lambda = -\Lambda^2$, then $e^{\lambda t}\varphi(x)$ is a solution.
2. (5.24)–(5.25): with $\lambda = \alpha + i\beta$ and $\beta\tau = (2l+1)\pi$, that equation is equivalent to $\alpha^2 + \beta^2 = \Lambda^2$, $\mu_2 e^{-\alpha\tau} = 2\alpha + \mu_1$.
3. Case (a), $\mu_1 = \mu_2$: the system forces $\alpha = 0$ and $\beta^2 = \Lambda^2$.
4. Case (b), $\mu_2 > \mu_1$, (5.26)–(5.27): for every $\Lambda > 0$ and $l$ there is $\alpha \in (0, (\mu_2-\mu_1)/2)$ with $\tau(\alpha) = \alpha^{-1}\ln(\mu_2/(\mu_1+2\alpha)) > 0$ solving the system.
5. Energy of separated solutions (p. 1584): $\mathcal E(t) = e^{2\,\mathrm{Re}(\lambda)t}\,\mathcal E(0)$ with $\mathcal E(0) > 0$.
6. Delay bounds (p. 1585, corrected): $(2l+1)\pi/\Lambda < \tau < (2l+1)\pi/\sqrt{\Lambda^2 - (\mu_2-\mu_1)^2/4}$, the second when $\Lambda^2 > (\mu_2-\mu_1)^2/4$.

Significance

The result shows that the stability threshold $\mu_2 < \mu_1$ of Theorem 1.3 is sharp in the sense that matters for design: at or beyond the threshold there is no delay margin, since delays as small as desired already produce solutions whose energy does not decay. Together with Theorem 1.3 it gives a complete dichotomy in the coefficients $(\mu_1,\mu_2)$ for the internally damped wave equation with delay, in any dimension, and it identifies the mechanism (roots of the characteristic equation on or to the right of the imaginary axis) that later work on delayed stabilization has had to avoid.

The result is proved in the paper; to the best of current knowledge it has not been machine-checked. The mission's product is a formal proof of the $a \equiv 1$ case together with its algebraic core: the reduction of the transcendental characteristic equation, the analysis of both cases, and the two-sided bounds on the delays. The spectral input it needs, an unbounded sequence of eigenvalues of the mixed Dirichlet–Neumann Laplacian with regular eigenfunctions, is reusable well beyond this paper.

Difficulty

The scalar part is elementary. The difficulty is the spectral input. The small delays come from $\tau_{n,l} \approx (2l+1)\pi/\Lambda_n$ with $\Lambda_n \to \infty$, so the proof needs infinitely many eigenvalues $\Lambda_n^2 \to \infty$ of the Laplacian with mixed Dirichlet–Neumann conditions on a $C^2$ domain, with eigenfunctions that are $C^2$ inside and $C^1$ up to the boundary. This requires compactness of the embedding $H^1_{\Gamma_D}(\Omega) \hookrightarrow L^2(\Omega)$, the spectral theorem for compact self-adjoint operators, and elliptic regularity for a mixed problem, none of which is available in Mathlib for domains in $\mathbb R^n$. A single eigenpair gives only the large delays (letting $l \to \infty$); it does not give the small ones.

A second point: the paper's own bound $(2l+1)^2\pi^2/\tau_{n,l}^2 \le \Lambda_n^2$ bounds $\tau_{n,l}$ only from below, so it does not by itself give $\tau_{n,l} \to 0$; the upper bound of milestone 6 is needed.

Formalization scope

• Space: $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with $n \ge 1$. The $C^2$ boundary is given by a global $C^2$ defining function $\psi$ ($\Omega = \{\psi < 0\}$, $\partial\Omega = \{\psi = 0\}$, $\nabla\psi \ne 0$ on $\partial\Omega$); $\nu = \nabla\psi/|\nabla\psi|$; the surface measure is pinned by the Gauss–Green formula for all $C^1$ fields.
• Solutions are complex valued functions $u(x,t)$ defined for all $t \in \mathbb R$, $C^2$ on $\Omega \times \mathbb R$ and $C^1$ on $\overline\Omega \times \mathbb R$; the equation and boundary conditions hold for $t > 0$; initial data and history are the traces of $u$. The Neumann condition uses the derivative within $\overline\Omega$. $|\nabla u|^2$ is the sum of the squared moduli of the partial derivatives.
• Corrected scope: Theorem 1.4 is printed for a general $a$ satisfying (1.17)–(1.18); §5.2 proves it only for $a \equiv 1$, which is what is stated.
• Corrected slips: (5.22) prints $\Delta\varphi = -\mu^2\varphi$ for $-\Lambda^2\varphi$; p. 1584 prints $e^{\alpha+i\beta}\varphi(x)$ for $e^{(\alpha+i\beta)t}\varphi(x)$; the p. 1585 bound is supplemented by the upper bound of milestone 6. Milestone texts are quoted verbatim, including the slips.
• The standing hypotheses (1.6)–(1.7) and the constant $\xi$ of (1.10) are not used by §5.2 and are omitted, which strengthens the statements.
• A trivializing formalization is ruled out: the goal's conclusion $\mathcal E \not\to 0$ excludes $u \equiv 0$, the energy integrand is continuous on the compact $\overline\Omega$ so the integral is genuine, and the normal derivative is taken within $\overline\Omega$ so the Neumann condition is not satisfied by a junk value.
• No statement assumes the existence of eigenvalues; supplying the spectral theory of the mixed Laplacian is part of the goal. Contributions welcome: the spectral theorem for the mixed Dirichlet–Neumann Laplacian on a bounded $C^2$ domain, boundary regularity of its eigenfunctions, and the energy identity for separated solutions.

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, 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.
• 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.
• P. Grisvard, Elliptic Problems in Nonsmooth Domains, Pitman, 1985 (regularity of mixed boundary value problems).