Source and verification

This article explains family 077 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

Fourier extension turns a function on a curved surface into an oscillatory wave in ambient space. Family 077 claims the full strict diagonal range for positively curved surfaces in three dimensions. The two manuscripts distinguish bounded input on the sphere from general input on a curved surface.

🏷️ Preliminaries: extension and curvature

Let be a compact smooth surface with surface measure . Its extension operator is

The integral superposes plane waves whose frequencies lie on . Positive curvature means that the second fundamental form is definite; locally, after choosing an orientation, the surface is a strictly convex graph. Curvature makes the directions normal to nearby frequency patches vary.

The name restriction comes from the adjoint question: when can the Fourier transform of an ambient-space function be meaningfully restricted to a lower-dimensional surface? Duality translates that question into bounds for .

🏷️ The two manuscript claims

Family 077, as stated in the manuscripts

For every , the spherical extension operator maps boundedly into . The companion claims, for every compact smooth positively curved surface , possibly with smooth boundary,

The surface is fixed, and the constant may depend on it. (OpenAI, 2026) (OpenAI, 2026a)

The second statement is a diagonal estimate: its input and output exponents agree. A bounded-data theorem by itself does not give it by the finite measure of . The inclusion points in the wrong direction for that inference.

🏷️ Why the endpoint is excluded

For and , rotation invariance reduces the integral to a one-dimensional calculation:

Its th power has radial integral proportional to

On a fixed positive fraction of each period the sine is bounded away from zero. The integral therefore diverges for . At the obstruction is logarithmic. This explains the strict output range even for a completely smooth input.

🏷️ Wave packets: the geometric intermediate objects

At spatial scale , a frequency cap of diameter generates a packet concentrated along a tube of length about and transverse radius about . The uncertainty principle gives the transverse scale; curvature sets the propagation direction. A general input decomposes into many such packets, with complex coefficients.

Tube counting sees where packet energy can accumulate. It does not fully describe the oscillatory sum: replacing every packet by its absolute value can destroy cancellation. The source consequently separates a theorem about positive geometric distributions from a theorem about complex packet arrays.

🏷️ Capacity propagation and the diagonal companion

The spherical manuscript assigns weights to elongated geometric tests, with a penalty for eccentricity. These weights quantify how much mass a test should be allowed to capture. A hypothetical violation is organized into nearly extremal width profiles across scales. Conditional entropy and projection estimates then oppose the concentration demanded by those profiles.

The next stage propagates estimates through packet frames. Intermediate selections act on coefficient arrays, so the proof tracks their effect on oscillatory amplitudes rather than declaring the descendants orthogonal. Geometric control of the available support is combined with second- and fourth-moment estimates to obtain the critical cubic estimate with an arbitrarily small spatial power loss.

The final spatial argument removes that loss for by controlling large-value sets across separated balls. A local estimate with a factor is not itself the claimed global estimate; the passage to the global norm is a separate part of the proof.

The companion treats finite input norms and general elliptic graph charts through the array formulation and phase continuation. It therefore addresses two issues absent from the bounded spherical statement: large amplitudes on small frequency sets and variation of the local phase beyond a quadratic or spherical model.

🏷️ Key steps and proof outlines

Exact frames separate coefficient energy from interference

A packet frame analyzes a frequency-localized input into coefficients indexed by a cap and a spatial lattice point. For a fixed cap, those coefficients are Fourier-series coefficients after rescaling its frequency window to a fixed square. Parseval therefore controls their squared sum. Summing over caps uses bounded overlap, yielding an coefficient bound in terms of the input’s norm.

That calculation is an analysis estimate, not a statement that all propagated packets are mutually orthogonal. To move between scales, the manuscript uses explicit frame matrices. Integration by parts in the overlap kernel makes entries small when the corresponding positions and directions are incompatible. Summable rows and columns bound the tails. Keeping these matrices is necessary because spatial masks and later selections change coefficients and may mix packets that were initially almost orthogonal. See “Propagation of oscillatory packets.” (OpenAI, 2026b)

Capacity detects anisotropic concentration

A round ball does not distinguish a family spread across a two-dimensional cross-section from one concentrated in a very thin strip. The geometric capacity tests therefore allow ellipses with unequal axes. Their weights include the aspect ratio, so fitting a large mass into a thin ellipse carries a different cost from fitting it into a round one.

To prove propagation, the source assumes an excessive growth exponent and selects an extremal sequence. It regularizes the finite labels before passing to entropy profiles. A profile records how much information is needed to specify position, direction, and time at linked resolutions. Changing frame acts by an exact shear; the mixed term in the shear must be retained because it can be comparable to the finest spatial resolution.

Projection estimates then constrain the tangent rates of those profiles. If the aspect ratio remains stationary, one set of scalar inequalities applies; if it increases, the change of eccentricity contributes an additional rate. The source excludes every calibrated aspect path. This is the positive geometric theorem underlying the packet argument, and it is stronger than an unweighted count of occupied tubes.

Positive support estimates feed a cubic oscillatory bound

The packet stage selects near-extremal coefficient arrays and keeps the masks defining the selected paths. A retained terminal coefficient can receive contributions from several initial coefficients. Locality estimates show which initial indices can contribute substantially, but they do not permit replacing the complex sum by a disjoint energy decomposition.

The proof combines the capacity control of those contributing indices with second- and fourth-moment estimates for packet synthesis. Interpolation between these moments targets the cubic functional. The second moment accounts for coefficient energy; the fourth moment detects pairs of overlapping packets. The geometric theorem bounds the concentration patterns that could make the fourth moment too large. Iterating this structure gives the local cubic estimate with a subpower spatial loss.

A useful elementary model is , obtained by Cauchy–Schwarz applied to . The manuscript’s weighted frame argument is more elaborate because the norms are localized and the selected arrays change between scales. The model identifies the roles of the two moments without replacing their actual estimates.

Sparse spatial covering removes the scale loss

An estimate on one ball of radius with factor does not give a global estimate by sending . Instead, the source selects large-value regions and covers them by sparse families of balls. Widely separated balls interact weakly through oscillatory kernels, so a joint estimate controls their contributions without multiplying the input norm by the number of balls. A multiscale covering organizes clusters that are not yet sufficiently separated.

Integrating the resulting level-set estimate uses the strict margin . In general,

The spare exponent above three absorbs the local subpower loss. At , that margin disappears, consistently with the spherical example above.

General curved surfaces require uniform phase control

The diagonal companion writes the surface in finitely many graph charts, rescales each chart so its Hessian is close to a fixed positive matrix, and continues the local phase outside the chart using a cutoff. The cutoff derivatives are checked together with the Taylor remainder so ellipticity survives. The velocity map, given by the phase gradient, is then bi-Lipschitz on the fixed frequency range. This permits conversion between frequency bins and directional tubes.

Weighted tube density estimates and joint sparse-ball bounds retain the input amplitude information needed for finite norms. Finally, a partition of unity and the smooth surface Jacobian transfer the chart estimates to . This explains both the dependence on the fixed surface and why the bounded spherical theorem is not the entire diagonal proof. (OpenAI, 2026a)

See Also

🏷️ Manuscripts and verification scope

No family-specific scope page was available at lean/docs/077.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. Diagonal Fourier extension for positively curved surfaces in three dimensions.
🐻  OpenAI 2026b. Elliptic capacity propagation and Fourier restriction to the sphere.