Cauchy problem for the Laplace equation with data on a line is ill-posed

Proved

TegmarkDimensionality.elliptic_cauchy_problem_ill_posed

by Lucas · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

ill-posednessmathematical-physicspde

There is a sequence of $C^2$ functions $u_k:\mathbb R^2\to\mathbb R$ , $k=0,1,2,\dots$ , such that:

each $u_k$ solves the Laplace equation $\partial_x^2u_k+\partial_y^2u_k=0$ on $\mathbb R^2$ ;
the Cauchy data on the line $y=0$ tend to zero uniformly: for every $\varepsilon>0$ there is $K$ with $|u_k(x,0)|\le\varepsilon$ and $|\partial_yu_k(x,0)|\le\varepsilon$ for all $k\ge K$ and all $x\in\mathbb R$ ;
off the line the solutions blow up: for every $y\neq0$ and every $M$ there is $K$ such that for every $k\ge K$ some $x$ has $|u_k(x,y)|>M$ .

So arbitrarily small changes in the data on the line $y=0$ produce arbitrarily large changes in the solution at any distance from it. An observer in a world with no time dimension ( $m=0$ , elliptic field equations) can make no inferences from local data.

Formalization Note The statement is the simplest instance of the paper's claim: the two-dimensional Laplace equation with data on a line.

Preamble

import Mathlib

Formal statement

namespace TegmarkDimensionality

/-- Initial data on the line `y = 0` for the Laplace equation `u_xx + u_yy = 0` in the plane
is an ill-posed problem: there are smooth solutions `u_k` whose Cauchy data
`u_k(x,0), ∂_y u_k(x,0)` tend to `0` uniformly in `x`, while for every `y ≠ 0` the solutions
`u_k(·, y)` become unbounded (their supremum over `x` tends to infinity). -/
theorem elliptic_cauchy_problem_ill_posed :
    ∃ u : ℕ → ℝ → ℝ → ℝ,
      (∀ k, ContDiff ℝ 2 (fun p : ℝ × ℝ => u k p.1 p.2)) ∧
      (∀ k x y, deriv (fun x' => deriv (fun x'' => u k x'' y) x') x +
          deriv (fun y' => deriv (fun y'' => u k x y'') y') y = 0) ∧
      (∀ ε > 0, ∃ K, ∀ k ≥ K, ∀ x,
          |u k x 0| ≤ ε ∧ |deriv (fun y => u k x y) 0| ≤ ε) ∧
      (∀ y ≠ 0, ∀ M : ℝ, ∃ K, ∀ k ≥ K, ∃ x, M < |u k x y|) := by sorry

end TegmarkDimensionality

Source

M. Tegmark, *On the dimensionality of spacetime*, Class. Quantum Grav. 14 (1997) L69–L75, https://doi.org/10.1088/0264-9381/14/4/002, p. L73, fifth paragraph ('giving initial data for an elliptic PDE on a non-closed hypersurface, say a plane, is an ill-posed problem'); classical example of Hadamard, cf. Courant–Hilbert vol. II

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source paper and of the intended meaning. It was not produced by a blind, independent auditor, so it may share the drafter's blind spots. Reviewers must not treat it as independent confirmation of faithfulness; compare the Lean code against the source directly.

The theorem asserts the existence of a family $u_k(x,y)$ , indexed by natural numbers $k$ , of real functions of two real variables such that:

for each $k$ , $(x,y)\mapsto u_k(x,y)$ is twice continuously differentiable on $\mathbb R^2$ ;
for all $k,x,y$ : $\dfrac{\partial^2u_k}{\partial x^2}(x,y)+\dfrac{\partial^2u_k}{\partial y^2}(x,y)=0$ , with each second derivative computed as an iterated one-variable derivative;
for every $\varepsilon>0$ there is $K$ such that for all $k\ge K$ and all real $x$ : $|u_k(x,0)|\le\varepsilon$ and $\left|\dfrac{\partial u_k}{\partial y}(x,0)\right|\le\varepsilon$ ;
for every real $y\neq0$ and every real $M$ there is $K$ such that for all $k\ge K$ there exists $x$ with $|u_k(x,y)|>M$ .

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph