Plectis Atlas
Finite computation in a balanced zero-data fluid flow
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 balanced_three_stack_realization : ∃ U f₀ f₁ : Family Velocity, ∃ X : Family MaterialFlow, ∃ repeated : FiniteMachine → Velocity, EffectiveFamily U ∧ EffectiveFamily f₀ ∧ EffectiveFamily f₁ ∧ (∀ M, Function.Periodic (repeated M) 1) ∧ ∀ (M : FiniteMachine) (w : Input M), Smooth (U M w) ∧ Smooth (f₀ M w) ∧ Smooth (f₁ M w) ∧ f₀ M w = inertialCoefficient (U M w) ∧ f₁ M w = viscousCoefficient (U M w) ∧ CommonCompactSupport (U M w) (f₀ M w) (f₁ M w) ∧ BoundedMixed (U M w) ∧ PeriodicAfterOne (U M w) ∧ (∀ t, 1 ≤ t → ∀ x, U M w t x = repeated M t x) ∧ ComparisonClass (U M w) (fun _ _ => 0) ∧ IsMaterialFlow (U M w) (X M w) ∧ ((∃ t : ℝ, 0 ≤ t ∧ X M w t fixedLabel ∈ observer) ↔ Halts M w) ∧ ∀ ν : ℝ, 0 < ν →A 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.