Plectis Atlas
Rapidly decaying alternating-coordinate memory
Family 376: Universal computation in forced Navier–Stokes flows
Candidate pairing
Theorem
For each positive computable \nu, a machine and a finite input effectively determine each of the following two forces.
- 1.
On \T^3, a smooth force has a unique global smooth solution in the torus class above, with pressure zero, for which (eq:torus-event) holds exactly when the machine halts. The force is supported in K\times\T for a compact K\subset(0,1)^2 independent of time. Its derivatives are bounded on every finite time interval; their bounds may grow with that interval.
- 2.
On \R^2\times\T, a smooth force and all its mixed derivatives are globally bounded. On each finite time interval its horizontal support is compact. It has a unique global smooth solution in (eq:comparison-class), with pressure zero and integrable nonnegative third component. Event (eq:plane-event) holds exactly when the machine halts.
The sets and thresholds in both observations are independent of the machine and input. The compact set K in the first construction may depend on that instance, but is independent of time. Both force prescriptions install all the required local instructions, without executing the selected computation.
Velocity-Field Detection of Computation in Forced Navier–Stokes Flows
TeX label thm:main, build/main.tex, line 98
The Lean statement says
theorem alternating (ν : ℝ) (hν : 0 < ν) (hc : ComputableReal ν) : AlternatingConclusion ν := by sorryA Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.