Source and verification

This article explains family 080 of the October 6, 2026 OpenAI collection. The research conclusions are attributed to its manuscripts. The source review covers statements, introductions, and the proof mechanisms described below; it is not an independent verification of the complete proofs.

Overview

Family 080 claims almost-everywhere convergence of the free Schrödinger evolution at the exact critical Sobolev exponent in every dimension at least two. The planar and higher-dimensional papers share a final task: combining all frequency scales without losing an extra logarithm or positive power.

🏷️ Preliminaries: the evolution and its representative

For , the unitary Schrödinger evolution is the Fourier multiplier with symbol . The Sobolev norm is

Unitarity and dominated convergence already imply in as . Almost-everywhere convergence along all real times is a stronger assertion. An equivalence class at each time does not automatically specify a jointly meaningful pointwise evolution.

The manuscripts use Gaussian regularization:

Cauchy–Schwarz makes this integral absolutely convergent. At a Lebesgue point of , write for the limit of local spatial averages.

🏷️ The exact endpoint claim

Family 080, as stated in the manuscripts

Put . For and every , there is one full-measure spatial set on which the Gaussian limit

exists for every , extends continuously to , and satisfies . The Gaussian limit is uniform over . (OpenAI, 2026) (OpenAI, 2026b)

The planar exponent is . The higher-dimensional companion handles . There is no added logarithmic Sobolev weight or positive in the stated hypothesis. The Gaussian limit is taken before the limit .

🏷️ Why summing frequencies is the endpoint problem

Let denote a smooth frequency projection to . The Sobolev norm is comparable to

with a low-frequency term understood. A triangle inequality applied to individual maximal estimates would instead produce an sum of the quantities . An sequence need not be summable. With an extra regularity exponent one could pay for this by geometric decay; at equality one cannot.

The source therefore linearizes every frequency on the same measurable time graph: each spatial point is assigned one observation time for the entire sum. A binary tree of time intervals then tracks contributions from different frequency scales. Its square-summation argument aims to preserve exactly the Sobolev norm.

🏷️ The geometric input to square summation

The planar manuscript first claims a transverse power saving for wave-packet configurations, then a bilinear estimate for general smooth packet arrays. The array formulation matters because spatial localization changes packet profiles; estimates restricted to exact solutions would not automatically survive those operations.

The higher-dimensional paper adds an induction that handles concentration near a polynomial wall. Merely saying that directions become narrow does not exclude a curved ruled surface. The source controls the second fundamental form, converts the relevant pieces into approximately affine plates, and applies a lower-dimensional transverse estimate after flattening.

Both papers obtain a short-time weak estimate with some output exponent and no growing loss beyond the critical frequency power. The strict inequality provides a convexity gain for lighter branches in the time tree. Combined with spatial decay, this is used to establish the local maximal estimate

initially for bounded-frequency inputs and uniformly in their frequency cutoff.

🏷️ Constructing one exceptional set

The maximal estimate gives a transparent approximation mechanism. Choose smooth approximations so rapidly that the sum of their successive Sobolev errors is finite. The local maximal bound makes the corresponding maximal differences summable in on each unit ball. Thus, outside one null set, the evolutions form a uniformly Cauchy sequence in time.

Their limit supplies a common continuous time representative. The source then identifies it with Gaussian regularization, using countably many error envelopes. This countable construction is essential: intersecting a full-measure set separately for each real time is not valid, since an uncountable union of null sets need not be null.

The approximation argument explains the final implication once the exact maximal estimate is available. The critical packet and frequency-summation estimates remain the substantive source claims.

🏷️ Key steps and proof outlines

Localization requires a stable class of packet arrays

A frequency cap of side is rescaled to a fixed cube, and the localized Fourier datum is expanded in Fourier series there. Parseval gives

where labels caps and labels spatial translates. The resulting exact packets form the initial array. Later spatial cutoffs multiply the packets, so they are no longer exact solutions with the original profiles. The manuscripts therefore work with a compact class of smooth native profiles having specified derivative and decay bounds.

To transfer exact-solution estimates to this class, a native profile is Fourier transformed in space and time. Its temporal frequency is separated from the quadratic Schrödinger phase. It becomes a sum or integral of exact extensions multiplied by temporal modulations. Integration by parts makes the coefficient tails summable. This is the “exact-field reduction” in the planar source and the corresponding compact-array argument in higher dimensions. (OpenAI, 2026a)

Broad configurations gain; narrow configurations need geometry

A broad frequency configuration contains sufficiently transverse directions. A linear change of coordinates sends representative directions close to coordinate axes, with distortion controlled by a power of the transversality parameter. Multilinear Kakeya estimates then bound simultaneous packet overlap. The source combines this with information estimates to claim a fixed power saving, stronger than a bound with an arbitrary small loss.

If broadness fails, directions lie near a lower-dimensional configuration. In the plane, the argument produces a short list of plates containing rich tubes and uses a one-dimensional distribution estimate after projection. In higher dimensions, a polynomial wall may be curved. The wall section first controls that curvature, then assigns packets to approximately affine plates. Flattening transports the measure, frequency windows, and coefficient energy budgets together. Merely projecting all packet directions to a hyperplane would not control their moving spatial centers.

The angular induction balances the broad saving against the narrow reduction. Its constants must be chosen in order: fix the broad/narrow separation, establish the lower-scale contraction, and then choose the induction constant. Allowing every constant to depend on the current scale would destroy the asserted lossless weak estimate. (OpenAI, 2026b)

One measurable graph linearizes the full maximal operator

For a bounded-frequency input and a finite set of times, choose at each a maximizing time . A measurable tie-breaking rule gives one graph for the whole frequency sum. Push spatial measure forward by ; call the resulting measure . A space–time ball of radius projects into a spatial ball of radius , hence

This estimate uses no regularity of . It places the graph measure in the class to which the packet distribution theorem applies. Passing through increasing finite time sets is later justified by continuity for the regularized or bounded-frequency evolution.

Linearizing each frequency at a separate time would give a larger quantity and lose correlations needed for square summation. The common graph preserves the fact that all frequencies are observed at one time at each point.

A time tree recovers the Sobolev square norm

Organize the selected times into nested dyadic intervals. Frequency scale determines which temporal depths are relevant. The source combines two dual short-time estimates and follows the heavier and lighter branches of this common tree. The weak output exponent gives a strict convexity gain on lighter branches. Spatial off-diagonal decay handles branches whose packet centers are far away.

The summation is designed to produce

rather than . This is the exact endpoint distinction. For instance, a sequence behaving like belongs to but not ; a triangle inequality over all frequency maxima would therefore leave a genuine gap. The time-tree proof is the source’s substantive answer to that gap, after the geometric weak estimate has been obtained.

Uniform approximation fixes the order of the two limits

Choose approximations with . On each unit ball, the maximal estimate and Tonelli imply that the sum of maximal evolution differences is finite almost everywhere. Hence the evolutions converge uniformly in time at those points. A countable cover by unit balls yields one global exceptional set.

The manuscript additionally compares this limit with the Gaussian regularizations using countably many maximal error envelopes. This permits first taking the Gaussian parameter to zero uniformly in time, and then taking time to zero. It avoids the invalid procedure of choosing a different exceptional set for each real time. The common representative is thus a consequence of exact maximal control plus summable approximation, not of unitarity alone.

See Also

🏷️ Manuscripts and verification scope

No family-specific scope page was available at lean/docs/080.md in this snapshot. This records the catalogue lookup, not a claim that no related Lean code exists. No Lean build or axiom audit was performed.

OpenAI collection gives the reading sequence and source policy; coverage register records which families have articles and which remain to be written.

🐻  OpenAI 2026a. Endpoint convergence for the planar Schrödinger equation.
🐻  OpenAI 2026b. Endpoint pointwise convergence for the Schrödinger equation in higher dimensions.