we-solve (beta)

Math-2844 · mathematics · Pde

A velocity-field halting detector in forced viscous flow

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
At fixed positive computable viscosity, can every machine and input be effectively realized by a unique zero-pressure global smooth forced Navier–Stokes flow on $T^3$, whose force has horizontal support in a time-independent compact subset of $(0,1)^2$ and finite-interval derivative bounds, such that some velocity component $u_3$ exceeds 1/2 in the fixed strip $1/32<y<1/8$ at some time exactly if the machine halts?

Short English statement

At fixed positive computable viscosity, can every machine and input be effectively realized by a unique zero-pressure global smooth forced Navier–Stokes flow on $T^3$, whose force has horizontal support in a time-independent compact subset of $(0,1)^2$ and finite-interval derivative bounds, such that some velocity component $u_3$ exceeds 1/2 in the fixed strip $1/32<y<1/8$ at some time exactly if the machine halts?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2844-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2844

Halting read from the velocity field: This question selects the torus velocity observer rather than the noncompact integral observer. The force has a fixed compact horizontal support, but its derivative estimates are required only on finite time intervals; the pointwise strip threshold is uniform over the encoded computation.

With the hypotheses and conventions above, the claimed result addresses the whole mathematical assertion on this page.

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

Go to contribution →