OpenAI claim summary for Math-2844

A velocity-field halting detector in forced viscous flow

OpenAI's claim

Halting read from the velocity field: The paper claims halting tests based on the third velocity component of a smooth forced Navier--Stokes solution, rather than solely a marked particle. A torus pointwise detector and an integral detector on $\mathbb R^2\times\mathbb T$ are treated separately.

Mathematical statement of the claimed result

Mathematical claim 1.

For the incompressible system $\partial_tu+(u\cdot\nabla)u=-\nabla p+\nu\Delta u+f$, $\nabla\cdot u=0$, $u(0)=0$, choose viscosity $\nu>0$, whose value is computable. Two effective Eulerian halting detectors are claimed. On the unit torus there is a smooth force, supported in $K\times\mathbb T$ for a time-independent compact $K\subset(0,1)^2$, and a unique global smooth zero-pressure solution for which \[M(w)\text{ halts}\quad\Longleftrightarrow\quad\exists t,x:\ 1/32<x_2<1/8,\ u_3(t,x)>1/2.\] Mixed derivatives are bounded on each finite interval. On $\mathbb R^2\times\mathbb T$ another force has globally bounded mixed derivatives and compact horizontal support on each finite interval, with a unique global smooth zero-pressure solution in $CH^2\cap C^1L^2$, bounded $u,\nabla u$ on finite intervals and $p\in CH^1$. Its third component is nonnegative and integrable, and \[M(w)\text{ halts}\quad\Longleftrightarrow\quad\exists t:\int_{\{x_2>0\}\times\mathbb T}u_3(t,x)\,dx>1/2.\] The observation regions and thresholds are fixed independently of the instance.

Outline of the argument

Halting read from the velocity field: An advection--diffusion equation carries the vertical signal. Successively shorter stirring bursts bound the pointwise diffusion error in the torus construction. In the noncompact variant an expanding collection of translation regions is paired with a moving cutoff, which controls escaped signal mass and gives the integral detector while maintaining bounded mixed derivatives.

Formal verification

Family 376 describes Lean coverage for the selected sheet-program, rapidly decaying particle-detector, velocity-detector, and full-box transport statements described separately in its Comparator files.

Halting read from the velocity field: The manuscript links BalancedBoxRouting.lean, BalancedThreeStack.lean, ForcedNavierStokesComputation.lean, NavierStokesAlternating.lean, NavierStokesVelocity.lean, SolenoidalSheetPrograms.lean.

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

• OpenAI, Velocity-Field Detection of Computation in Forced Navier–Stokes Flows, 2026-09-27; citation key OAI:Velocity-Field-Detection-of-Computation-in-Forced-Navier-Stokes-Flows-September-27-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 376: Lean scope.
• Comparator BalancedBoxRouting.json.
• Comparator BalancedBoxRouting.lean.
• Comparator BalancedThreeStack.json.
• Comparator BalancedThreeStack.lean.
• Comparator ForcedNavierStokesComputation.json.
• Comparator ForcedNavierStokesComputation.lean.
• Comparator NavierStokesAlternating.json.
• Comparator NavierStokesAlternating.lean.
• Comparator NavierStokesVelocity.json.
• Comparator NavierStokesVelocity.lean.
• Comparator SolenoidalSheetPrograms.json.
• Comparator SolenoidalSheetPrograms.lean.
• OpenAI catalogue entry.