Papers With

← All papers
First page of Compactly supported real scalar potentials realizing the Hardy uncertainty endpoint for Schrödinger evolutions

Compactly supported real scalar potentials realizing the Hardy uncertainty endpoint for Schrödinger evolutions

Xiao-Ming Fu, Tianyang Sun

math.AP Jul 25, 2026 · v1
formalization analysis ai-agents
Read PDF arXiv abstract Code
TL;DR
The proof of the main theorem (Theorem 1.1) was formally verified in Lean, with the formalization released in a project repository.
Abstract
At the critical Hardy Gaussian weight for the Schrödinger equation in one space dimension on $[0,1]$, the known nonzero scalar example in the weighted $L^2$ class carries a complex-valued potential. Cassano and Fanelli observed that the existence of a real-valued scalar endpoint example was open, and produced examples with real electric and magnetic potentials only after introducing a magnetic potential. We construct a nonzero smooth solution of $i\partial_t u+\partial_x^2 u=Vu$ on $\mathbb{R}\times[0,1]$ such that $e^{x^2/4}u(\cdot,0),e^{x^2/4}u(\cdot,1)\in L^2(\mathbb{R})$ and the potential is bounded, smooth, real-valued, and purely scalar and is supported in one fixed compact spatial interval for all times. This compact-support endpoint example is the main result. We also record the explicit rational-tail realization underlying the construction. The main results of this paper were obtained by the multi-agent system Eureka and have subsequently been verified by the authors.
Problem

At the critical Hardy Gaussian weight for the 1D Schrödinger equation on [0,1], the only known nonzero endpoint examples used either a complex-valued potential or an added magnetic potential. Whether a real-valued, purely scalar endpoint example exists was an open problem.

Approach

The authors use a transported ansatz with a Gaussian width y(t) satisfying y”=16/y^3 and a pseudoconformal phase b=y'/(4y). This choice makes the continuity equation hold identically, which forces the potential to be real. A rational-tail profile, refined into a compactly supported profile built from parabolic cylinder functions, keeps the weighted L^2 endpoint condition satisfied while the potential stays bounded. The results were obtained by the multi-agent system Eureka, checked by the authors, and the main theorem was formally verified in Lean.

Results

They construct a nonzero smooth solution with e^{x^2/4}u at times 0 and 1 in L^2. The potential is bounded, smooth, real-valued and purely scalar, and is supported in a fixed compact spatial interval for all times. The mechanism extends to all dimensions and to general time intervals.