we-solve (beta)

Math-2842 · mathematics · Pde

Computation by compactly supported eventually periodic box transport

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every machine and input and positive computable viscosity, do effective coefficients $f_0,f_1$ on $R^3$ yield $f=f_0+\nu $ $f_1$ and a zero-data smooth Navier–Stokes solution with pressure zero, both supported in one fixed compact spatial set and having globally bounded mixed derivatives, one-periodic after $t=1$, whose particle from (4,0,0) enters $(-1,2)^3$ exactly on halting? Require uniqueness in the stated C H2 intersect C1 L2 comparison class and, for a fixed machine, an input-independent repeated field.

Short English statement

For every machine and input and positive computable viscosity, do effective coefficients $f_0,f_1$ on $R^3$ yield $f=f_0+\nu $ $f_1$ and a zero-data smooth Navier–Stokes solution with pressure zero, both supported in one fixed compact spatial set and having globally bounded mixed derivatives, one-periodic after $t=1$, whose particle from (4,0,0) enters $(-1,2)^3$ exactly on halting? Require uniqueness in the stated C H2 intersect C1 L2 comparison class and, for a fixed machine, an input-independent repeated field.

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2842

Full-box transport and finite computation: The box-transport realization has one fixed compact spatial support and an eventually periodic field with zero pressure. Its repeated mechanism can be fixed for a machine independently of its finite input, while initialization encodes the input and the detector checks the full continuous trajectory.

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

Computation by compactly supported eventually periodic box transport

OpenAI's claim

Full-box transport and finite computation: The paper claims effective incompressible realization of determinant-one positive diagonal maps on neighborhoods of entire solid rational boxes. A balanced recorder turns these maps into particle halting detection with fixed compact spatial support and eventually periodic forcing.

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. On $\mathbb R^3$, the construction supplies effective coefficients $f_0,f_1$ with $f=f_0+\nu f_1$ and an explicit zero-data solution $(U,0)$. Both fields vanish outside the same fixed compact spatial region, every mixed derivative is bounded, and both are period one after $t=1$. For the fixed particle $x_*=(4,0,0)$, \[\exists t\ge0:X(t;x_*)\in(-1,2)^3\quad\Longleftrightarrow\quad M(w)\text{ halts}.\] The repeated mechanism depends only on the machine; uniqueness holds among $u\in CH^2\cap C^1L^2$ with $u,\nabla u$ bounded on any finite interval, and a $CH^1$ pressure representative after choosing its additive constant.

Outline of the argument

Full-box transport and finite computation: Localized curls evacuate overlapping source boxes into storage, deform them there, and deliver them along obstacle-avoiding detours. A three-stack recorder keeps the finite instruction system reversible. The construction checks observations at every intermediate time and derives effective derivative bounds, with separate torus and slow-clock variants treated under their stated comparison classes.

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.

Full-box transport and finite computation: 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 →