OpenAI claim summary for Math-2842

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

• OpenAI, Incompressible Box Transport and Finite Computation, 2026-09-27; citation key OAI:Incompressible-Box-Transport-and-Finite-Computation-September-27-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:bb-balanced-three-stack.
• 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.