we-solve (beta)

Math-2843 · mathematics · Pde

Halting detection by integrated velocity on a planar-periodic fluid domain

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 effectively determine a smooth force on $R^2×T$, with every mixed derivative globally bounded and horizontally compact support on each finite interval, and a unique global zero-pressure smooth viscous flow with integrable nonnegative $u_3$, such that $integral_{{X_2>0}×T}u_3(t)>1/2$ for some t exactly if the machine halts?

Short English statement

At fixed positive computable viscosity, can every machine and input effectively determine a smooth force on $R^2×T$, with every mixed derivative globally bounded and horizontally compact support on each finite interval, and a unique global zero-pressure smooth viscous flow with integrable nonnegative $u_3$, such that $integral_{{X_2>0}×T}u_3(t)>1/2$ for some t exactly if the machine halts?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2843

Halting read from the velocity field: This is the integral observer on $\mathbb R^2\times\mathbb T$, using the nonnegative integrable vertical component and a fixed half-plane threshold. Horizontal support need only remain compact on each finite interval, whereas the mixed derivative bounds are global in time.

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

Halting detection by integrated velocity on a planar-periodic fluid domain

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 →