# Stable blowup for the defocusing Schrödinger equation

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Stable self-similar blowup for a supercritical defocusing Schrödinger equation on the torus](../../preprints/Stable-Self-Similar-Blowup-for-a-Supercritical-Defocusing-Schrodinger-Equation-on-the-Torus-September-24-2026/paper.pdf)

## Scope

The formalization constructs stable self-similar finite-time blowup for defocusing nonlinear Schrödinger equations on the twelve-dimensional torus. For every prescribed lower bound on the power, it selects an odd power at least that large and a Sobolev index $k>8$ for which a nonempty open set of $H^k$ initial data has the stated classical blowup behavior. The selected quantifier gives arbitrarily large odd powers, rather than every sufficiently large odd power.

For each such construction, Gaussian Fourier data with decay exponent $\alpha>k+6$ assign positive probability to the blowup set, and almost-sure global existence fails. The exponent $\alpha$ may be arbitrarily large.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Stable self-similar blowup and positive-probability Gaussian blowup | [DefocusingNLS.lean](../ComparatorChallenges/DefocusingNLS.lean) |