Partial Differential Equations

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

Motivation

Boundary feedback stabilization of the wave equation asks whether a damping term placed on part of the boundary drives the energy of every solution to zero. Without delay the answer is classical: the feedback $\partial u/\partial\nu = -\mu_1 u_t$ on a part $\Gamma_N$ of the boundary gives exponential energy decay under geometric conditions (Chen, Lagnese, Lasiecka–Triggiani, Komornik–Zuazua). In practice a feedback is applied with a lag, and a small lag can destroy stability. Datko, Lagnese and Polis (doi:10.1137/0324007) and Datko (doi:10.1137/0326040) showed, in one space dimension, that a purely delayed boundary feedback destabilizes the system for arbitrarily small delays.

Nicaise and Pignotti (doi:10.1137/060648891) study a feedback made of an instantaneous part and a delayed part, with weights $\mu_1$ and $\mu_2$, in any space dimension. Their Theorem 1.1 gives exponential decay when $\mu_2 < \mu_1$. This mission formalizes the converse, Theorem 1.2: when $\mu_2 \ge \mu_1$, some delays admit solutions whose energy does not decay at all.

Timeline.

• 1986: Datko, Lagnese and Polis, a one-dimensional wave equation whose delayed boundary feedback is unstable.
• 1988: Datko, instability under arbitrarily small delays for a class of hyperbolic systems.
• 2006: Xu, Yung and Li (doi:10.1051/cocv:2006021), one space dimension, by spectral analysis: stability for $\mu_2 < \mu_1$, instability for $\mu_2 > \mu_1$, possible instabilities for $\mu_1 = \mu_2$.
• 2006: Nicaise and Pignotti, the same dichotomy in any dimension $n$, with explicit destabilizing delays built from eigenfunctions (§5.1).

Setting

Let $n \ge 1$ and let $\Omega \subset \mathbb R^n$ be a bounded open set with boundary $\Gamma$ of class $C^2$. The boundary is 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 $d\Gamma$ for the surface measure. Together these data form a mixed domain (MixedDomain n in Lean).

Fix $\mu_1, \mu_2 > 0$ and a delay $\tau > 0$. The problem (1.1)–(1.3) is

$$\begin{cases} u_{tt}(x,t) - \Delta u(x,t) = 0 & \text{in } \Omega \times (0,+\infty),\\ u(x,t) = 0 & \text{on } \Gamma_D \times (0,+\infty),\\ \dfrac{\partial u}{\partial\nu}(x,t) = -\mu_1 u_t(x,t) - \mu_2 u_t(x,t-\tau) & \text{on } \Gamma_N \times (0,+\infty), \end{cases}$$

with initial data $u(\cdot,0)$, $u_t(\cdot,0)$ and a history $u_t$ on $\Gamma_N \times (-\tau,0)$ (1.4)–(1.5). The standard energy of a solution is (3.7)

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

Condition (1.8) of the paper is $\mu_2 < \mu_1$. This mission concerns the complementary case $\mu_2 \ge \mu_1$.

For real functions $w$ on $\Omega$, (5.11) defines $q_0(w) = \int_{\Gamma_N} |w|^2\,d\Gamma$ and $q_1(w) = \int_\Omega |\nabla w|^2\,dx$.

Formalization targets

Goal: Theorem 1.2 (p. 1563)

If $\mu_2 \ge \mu_1$, there exist delays $0 < \tau_0 < \tau_1 < \cdots$ and, for each $k$, a classical solution $u_k$ of (1.1)–(1.3) with delay $\tau_k$ and a constant $c_k > 0$ such that

$$\mathcal E_k(t) = c_k \qquad \text{for all } t \ge 0 .$$

The statement fixes no formula for the delays and no value of the energy. It asserts only the existence of infinitely many delays for which the energy does not decay.

Milestones

1. (5.1)–(5.2), pp. 1579–1580. If $\lambda \in \mathbb C$ and $\varphi$ solves $-\Delta\varphi + \lambda^2\varphi = 0$ in $\Omega$, $\varphi = 0$ on $\Gamma_D$ and $\partial\varphi/\partial\nu = -(\mu_1 + \mu_2 e^{-\lambda\tau})\lambda\varphi$ on $\Gamma_N$, then $u = e^{\lambda t}\varphi$ solves (1.1)–(1.3).
2. (5.5)–(5.7), pp. 1580 and 1582. For $b > 0$, $l \in \mathbb N$ and $b\tau = \arccos(-\mu_1/\mu_2) + 2l\pi$:

$$\cos(b\tau) = -\mu_1/\mu_2,\qquad \mu_2\sin(b\tau) = \sqrt{\mu_2^2-\mu_1^2},\qquad (\mu_1 + \mu_2e^{-ib\tau})\,ib = b\sqrt{\mu_2^2-\mu_1^2}.$$

3. Case (a), $\mu_1 = \mu_2$, p. 1581. For a normalized mixed Dirichlet–Neumann eigenfunction $\varphi$ with $-\Delta\varphi = b^2\varphi$ and $\tau = (2l+1)\pi/b$, the function $u = e^{ibt}\varphi$ is a solution and

$$\int_\Omega(|\nabla u|^2 + |u_t|^2)\,dx = 2b^2 \quad (t \ge 0).$$

4. Case (b), $\mu_2 > \mu_1$, pp. 1581–1582. A normalized minimizer $\varphi$ of $s\,q_0(w) + \sqrt{s^2q_0(w)^2 + 4q_1(w)}$, where $s = \sqrt{\mu_2^2-\mu_1^2}$, solves the variational problem (5.7) with $2b$ equal to the minimum value.

Significance

The result. Theorem 1.2 shows that the threshold $\mu_2 < \mu_1$ of Theorem 1.1 is sharp in the following sense: once the delayed weight reaches the instantaneous one, no geometric assumption restores asymptotic stability for every delay. Together, Theorems 1.1 and 1.2 separate robust from non-robust boundary feedbacks by a single inequality between the two gains. The explicit delays of case (a), $\tau_{n,l} = (2l+1)\pi/b_n$, become arbitrarily small or large. So even an arbitrarily short lag in an equally weighted feedback can remove decay.

The formalization. The paper proves the result. It has not been formalized, and Mathlib has no wave equation on domains, no mixed eigenvalue problems and no Sobolev spaces on domains. This mission produces:

• a machine-checked statement of the instability half of the paper's dichotomy;
• the reduction to a spectral problem as separate, checkable steps;
• a precise record of what the paper leaves implicit. In case (b) the existence of the minimizer is assumed ("if the minimum … is attained"), and in case (a) the existence of Dirichlet–Neumann eigenfunctions is quoted.

Difficulty

Milestones 1 and 2 are calculus and trigonometry. The difficulty sits in producing $\varphi$. The goal needs a nonzero function $\varphi$ that is $C^2$ in $\Omega$ and $C^1$ up to the boundary and solves an eigenvalue problem with mixed Dirichlet and Neumann (case (a)) or Dirichlet and Robin-type (case (b)) boundary conditions. Existence requires compactness of $H^1_{\Gamma_D}(\Omega) \hookrightarrow L^2(\Omega)$ and of the trace into $L^2(\Gamma_N)$, followed by elliptic regularity up to a $C^2$ boundary. None of these is in Mathlib.

A shortcut does not work: in case (b) the frequency $b$ enters the boundary condition, so $\varphi$ is not an eigenfunction of a fixed self-adjoint operator. The page instead minimizes a non-quadratic functional, and its first-variation computation (5.18)–(5.19) needs care: the functional is not 2-homogeneous, so the normalization by $1 + \varepsilon^2\|v\|^2$ does not literally give $g(\varepsilon) \ge g(0)$, although the first-order condition is right.

Taking real parts does not give a real-valued solution with constant energy: in case (b) the energy of $\cos(bt)\varphi$ oscillates.

Formalization scope

• Solutions are complex-valued, $u : \mathbb R^n \times \mathbb R \to \mathbb C$, as the page's $e^{\lambda t}\varphi$ with $\lambda \in \mathbb C$ are. $|u_t|^2$ and $|\nabla u|^2 = \sum_i |\partial_i u|^2$ are squared moduli.
• Classical solutions. A solution is $C^2$ on $\Omega \times \mathbb R$ and $C^1$ on $\overline\Omega \times \mathbb R$. It solves the equations for $t > 0$, and its values at $t \le 0$ are the initial data and history. The normal derivative is the derivative within $\overline\Omega$ applied to $\nu$. $C^2$ regularity up to the boundary is not required, because eigenfunctions of mixed problems generally lack it.
• The domain. The $C^2$ boundary is given by a global defining function $\psi$ with $\Omega = \{\psi < 0\}$. The surface measure is pinned down by the Gauss–Green formula for all $C^1$ vector fields, which determines it uniquely.
• Dropped hypotheses. The geometric hypotheses (1.6)–(1.7) and the parameter $\xi$ of (1.10) are not used in §5.1 and are omitted. This strengthens the statements.
• Sobolev spaces. $H^1_{\Gamma_D}(\Omega)$ is replaced in milestone 4 by the class of real functions that are $C^2$ in $\Omega$, $C^1$ on $\overline\Omega$ and zero on $\Gamma_D$, both as the minimization class and as the test class.
• Non-triviality. The goal requires the constant energy to be positive and the delays to be strictly increasing. Without positivity, the zero solution would satisfy "constant energy". Without strict monotonicity, one delay repeated would count as a sequence.

A complete development needs the following:

• Green's first identity on $C^2$ domains for functions that are $C^1$ up to the boundary;
• existence and regularity of eigenfunctions of the Laplacian with mixed boundary conditions;
• in case (b), existence of the minimizer (Rellich compactness and the trace theorem).

These pieces are reusable well beyond this mission. Contributions of any of them, or of an alternative route to a $\varphi$ with the required properties, 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
• G. Q. Xu, S. P. Yung, L. K. Li, Stabilization of wave systems with input delay in the boundary control, ESAIM Control Optim. Calc. Var. 12:770–785, 2006. https://doi.org/10.1051/cocv:2006021