Pointwise and integral velocity-field detection of halting (Lean)

The Lean statement

The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.

theorem main_result :    ∃ B : ℕ, 0 < B ∧      (∀ s : ℝ, |deriv (deriv SmoothBump.profile) s| ≤ (B:ℝ)) ∧    ∀ (ν : ℝ), 0 < ν → ComputableReal ν →    ∀ (b N : ℕ) [NeZero b] [NeZero N]      (M : TM0.Machine (Fin b) (Fin N)) (w : List (Fin b)),    ∃ (Ftor Fcyl : ℝ → VectorField 3),      (compile B M w).Represents .torus Ftor ∧      (compile B M w).Represents .cylinder Fcyl ∧      (ContDiff ℝ ∞ (uncurry (Ftor ν)) ∧        (∀ t, FactorsThrough (Ftor ν t) PeriodicSpace.cover) ∧        (∃ K : Set (Coord 2), IsCompact K ∧ (∀ X ∈ K, ∀ i, X i ∈ Ioo (0:ℝ) 1) ∧          ∀ t X, PeriodicSpace.cover (horizontal X) ∉ PeriodicSpace.cover '' K → Ftor ν t X = 0) ∧        (∀ T d, ∃ C : ℝ, 0 ≤ C ∧ ∀ t ∈ Icc (0:ℝ) T, ∀ X,          ‖iteratedFDeriv ℝ d (uncurry (Ftor ν)) (t,X)‖ ≤ C) ∧        ∃ u : VectorField 3,          ContDiff ℝ ∞ (uncurry u) ∧ TorusClass.ComparisonClass u (fun _ _ => 0) ∧          NavierStokes ν u (fun _ _ => 0) (Ftor ν) ∧          (Observation.torusEvent u ↔ (TM0.eval M w).Dom) ∧          ∀ (v : VectorField 3) (p : ScalarField 3), TorusClass.ComparisonClass v p →            NavierStokes ν v p (Ftor ν) →            ∀ t ≥ 0, (∀ X, v t X = u t X) ∧ (∀ X, p t X = 0)) ∧      (ContDiff ℝ ∞ (uncurry (Fcyl ν)) ∧        UniformDerivatives.Bounded (fun _ : Unit => uncurry (Fcyl ν)) ∧        (∀ t X z, Fcyl ν t (update X 2 z) = Fcyl ν t X) ∧        (∀ T : ℝ, ∃ K : Set (Coord 2), IsCompact K ∧ ∀ t ∈ Icc (0:ℝ) T,          ∀ X : Coord 3, horizontal X ∉ K → Fcyl ν t X = 0) ∧        ∃ u : VectorField 3,          ContDiff ℝ ∞ (uncurry u) ∧          Cylinder.ComparisonClass (fun t x => u t (Cylinder.join x)) (fun _ _ => 0) ∧          NavierStokes ν u (fun _ _ => 0) (Fcyl ν) ∧          (∀ t ≥ 0, (∀ x, 0 ≤ u t (Cylinder.join x) 2) ∧            Integrable (fun x => u t (Cylinder.join x) 2) Cylinder.measure) ∧          (Observation.planeEvent u ↔ (TM0.eval M w).Dom) ∧          ∀ (v : VectorField 3) (p : ScalarField 3),            Cylinder.ComparisonClass (fun t x => v t (Cylinder.join x))              (fun t x => p t (Cylinder.join x)) →            NavierStokes ν v p (Fcyl ν) →            ∀ t ≥ 0, (∀ X, v t X = u t X) ∧ (∀ X, p t X = 0)) := by sorry

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.

Definitions needed to read it

Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.

abbreviation OAI.VelocityDetection.Coord line 10
```
abbrev Coord (n : ℕ) := Fin n → ℝ
```

abbreviation OAI.VelocityDetection.ScalarField line 12

abbrev ScalarField (n : ℕ) := ℝ → Coord n → ℝ

abbreviation OAI.VelocityDetection.VectorField line 14

abbrev VectorField (n : ℕ) := ℝ → Coord n → Coord n

definition OAI.VelocityDetection.spatialD line 22

def spatialD {n : ℕ} (i : Fin n) (q : ScalarField n) : ScalarField n :=  fun t x => deriv (fun s => q t (Function.update x i s)) (x i)

definition OAI.VelocityDetection.timeD line 25

def timeD {n : ℕ} (q : ScalarField n) : ScalarField n :=  fun t x => derivWithin (fun s => q s x) (Ici 0) t

definition OAI.VelocityDetection.laplacian line 28

def laplacian {n : ℕ} (q : ScalarField n) : ScalarField n :=  fun t x => ∑ i : Fin n, spatialD i (spatialD i q) t x

definition OAI.VelocityDetection.advection line 31

def advection {n : ℕ} (a : VectorField n) (q : ScalarField n) : ScalarField n :=  fun t x => ∑ i : Fin n, a t x i * spatialD i q t x

definition OAI.VelocityDetection.divergence line 34

def divergence {n : ℕ} (a : VectorField n) : ScalarField n :=  fun t x => ∑ i : Fin n, spatialD i (fun s y => a s y i) t x

definition OAI.VelocityDetection.NavierStokes line 37

def NavierStokes (ν : ℝ) (u : VectorField 3) (p : ScalarField 3)    (f : VectorField 3) : Prop :=  (∀ (t : ℝ), 0 ≤ t → ∀ x : Coord 3, ∀ i : Fin 3,    timeD (fun s y => u s y i) t x + advection u (fun s y => u s y i) t x =      -spatialD i p t x + ν * laplacian (fun s y => u s y i) t x + f t x i) ∧  (∀ (t : ℝ), 0 ≤ t → ∀ x, divergence u t x = 0) ∧  (∀ x, u 0 x = 0)

definition OAI.VelocityDetection.horizontal line 45

def horizontal (x : Coord 3) : Coord 2 := ![x 0, x 1]

inductive type OAI.VelocityDetection.Stacks.Move line 55

inductive Move  | right  | stay  | left  deriving DecidableEq, Repr

definition OAI.VelocityDetection.Stacks.update line 61

def update (b : ℕ) (m : Move) (β x y : ℕ) : ℕ × ℕ :=  match m with  | .right => (b * x + β, y / b)  | .stay => (x, y - y % b + β)  | .left => (x / b, x % b + b * β + b ^ 2 * (y / b))

structure OAI.VelocityDetection.Stacks.Rule line 67

structure Rule (σ : Type*) (b : ℕ) where  target : σ  written : Fin b  move : Move

structure OAI.VelocityDetection.Stacks.Configuration line 72

structure Configuration (σ : Type*) where  state : σ  leftStack : ℕ  rightStack : ℕ  deriving DecidableEq

definition OAI.VelocityDetection.Stacks.applyRule line 78

def applyRule {σ : Type*} {b : ℕ} (r : Rule σ b) (c : Configuration σ) : Configuration σ :=  let st := update b r.move r.written c.leftStack c.rightStack  ⟨r.target, st.1, st.2⟩

definition OAI.VelocityDetection.Stacks.capacity line 84
```
def capacity (b m n : ℕ) : ℕ := b ^ (m + n)
```
definition OAI.VelocityDetection.Expanding.lambda line 94
```
def lambda (D : ℝ) : ℝ := 4 * D
```

definition OAI.VelocityDetection.Expanding.initialRadius line 96

def initialRadius (ν K D : ℝ) : ℝ :=  1024 * 3000 * (1 + ν) * lambda D * (K * D + 2)

definition OAI.VelocityDetection.Expanding.radius line 99

def radius (ν K D : ℝ) (n : ℕ) : ℝ := initialRadius ν K D * lambda D ^ n

definition OAI.VelocityDetection.Observation.join line 110

def join (X : Coord 2) (z : ℝ) : Coord 3 := ![X 0, X 1, z]

definition OAI.VelocityDetection.Observation.torusEvent line 112

def torusEvent (u : VectorField 3) : Prop :=  letI := neZeroThree  ∃ t : ℝ, 0 ≤ t ∧ ∃ x : Coord 3,    1 / ((32 : ℕ) : ℝ) < x 1 ∧ x 1 < 1 / ((8 : ℕ) : ℝ) ∧ (1 / ((2 : ℕ) : ℝ) : ℝ) < u t x 2

definition OAI.VelocityDetection.Observation.upperHalfPlane line 117
```
def upperHalfPlane : Set (Coord 2) := {X | 0 < X 1}
```

definition OAI.VelocityDetection.Observation.planeMass line 119

def planeMass (u : VectorField 3) (t : ℝ) : ℝ :=  letI := neZeroThree  ∫ q in upperHalfPlane ×ˢ Ioc (0 : ℝ) 1,    u t (join q.1 q.2) 2 ∂(volume.prod volume)

definition OAI.VelocityDetection.Observation.planeEvent line 124

def planeEvent (u : VectorField 3) : Prop :=  ∃ t : ℝ, 0 ≤ t ∧ (1 / ((2 : ℕ) : ℝ) : ℝ) < planeMass u t

72 more definitions are reached the same way; the full file lists them.

Possible paper match, with no recorded review

Atlas selected this possible match by comparing words in the Lean statement with every statement in the family. No review of whether the statements mean the same thing is recorded.

Words of the Lean statement, its names split into words, that also appear in the theorem: horizontal, plane, observations, integrable, eq, two, comparison, compact and 13 more. Found in the paper’s title, which its main theorem states: stokes, navier, field and velocity. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: nonnegative, positive, times and halts.

Statements in Velocity-Field Detection of Computation in Forced Navier–Stokes Flows come first because the release’s name for this Lean statement shares words with that paper’s title.

Theorem 1.1 of Velocity-Field Detection of Computation in Forced Navier–Stokes Flows

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.

Section 1, Observing the velocity rather than a particle Read it in the paper TeX source, line 98

Show the TeX

For each positive computable $\nu$, a machine and a finite input
effectively determine each of the following two forces.
\begin{enumerate}
\item On $\T^3$, a smooth force has a unique global smooth solution
in the torus class above, with pressure zero, for which
\eqref{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.
\item 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
\eqref{eq:comparison-class}, with pressure zero and integrable
nonnegative third component. Event~\eqref{eq:plane-event} holds exactly
when the machine halts.
\end{enumerate}
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.

Other possible paper matches, closest wording first

Theorem 3.2 of Finite Instructions and Solenoidal Shear Flows. Words of the Lean statement, its names split into words, that also appear in the theorem: theta, lifting, coding, next, lowering, scaling and 34 more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: vertical, constructed, positive and times.
Theorem 4.1 of Universal Computation with Eventually Stationary Navier–Stokes Forcing. Words of the Lean statement, its names split into words, that also appear in the theorem: radius, second, compiled, list, lower, source and 30 more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: strip, construct, positive, times and halts.
Theorem 10.2 of Prefix Instructions and Incompressible Flows. Words of the Lean statement, its names split into words, that also appear in the theorem: cases, domain, listed, code, window, planes and 35 more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: prescribed, viscosity, positive, times and halts.
Theorem 3.1 of Velocity-Field Detection of Computation in Forced Navier–Stokes Flows. Words of the Lean statement, its names split into words, that also appear in the theorem: mass, horizontal, eq, two, integer, 1/2 and ten more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: nonnegative, viscosity, positive and times.
Theorem 8.3 of Prefix Instructions and Incompressible Flows. Words of the Lean statement, its names split into words, that also appear in the theorem: blank, plane, gradient, word, uniform, stokes and 26 more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: viscosity, positive and halts.
Proposition 9.3 of Incompressible Box Transport and Finite Computation. Words of the Lean statement, its names split into words, that also appear in the theorem: represents, functions, step, including, tables, space and ten more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: pointwise and halt.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.

Reported Comparator runs

two independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; MathVet. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.

For a configured theorem, Comparator tests whether OpenAI’s proof proves the exact Lean statement. Some files instead configure definitions for comparison by name and type. Acceptance does not establish that the statement means the same thing as the paper’s theorem.

Carlos Toledo’s cert-machine

How they ran it, in their words

Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners (.github/workflows/openai-math-kernel.yml), one j…

Accepted Their term: “CERTIFIED”.
Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
Reported 10 October 2026, at the release version shown here. Original verification report

MathVet

How they ran it, in their words

An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.

Accepted Their term: “comparator-sandboxed-pass”.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Reported 8 October 2026, at the release version shown here. Original verification report

What an accepted Comparator run would establish

If Comparator is run under this configuration and accepts, the solution proves the configured theorem using only the allowed axioms, and the Lean kernel accepts every step.

This configuration lists no definition holes, so every definition the statement uses is compared as it is written in this file.

Allowed axioms: propext, Quot.sound, Classical.choice

Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.

Do family 376’s Lean statements express the advertised result?

These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.

MathVet and cert-machine agree on how much of the advertised result the Lean statements express.

MathVet
Finds the whole advertised result stated or implied Their term: “full”.
The challenge statements imply the headline claim after unpacking definitions or one routine step. Their record
Their note: NavierStokesAlternating.alternating (fixed computable ν > 0) gives computable compilers (Machine × input ↦ triple of Nat.Partrec.Code programs returning approximations, moduli and rapid-decay bounds) and, for every well-formed Turing machine and input, a smooth force f = residual ν U supported in one compact K, with U the unique energy-class solution from rest (zero pressure), such that the machine halts iff the particle started at (-1,0,0) reaches {x₁ > 0}. ForcedNavierStokesComputation and BalancedThreeStack (one theorem stated twice: all ν > 0, particle from (4,0,0) into (-1,2)³) and NavierStokesVelocity (torus and ℝ²×𝕋 detection) are variants. The forcing is not unconstrained: it must be uniformly computable in (M, w) (ProgramFor/EffectiveFamily/Represents), which excludes a force that already knows the halting answer.
Definitions the group asks readers to compare with the paper: The flow is prescribed and the force is derived from it: f = residual ν U := ∂ₜU + U·∇U - νΔU (Alternating) or f₀ := inertialCoefficient U, f₁ := viscousCoefficient U, affineForce f₀ f₁ ν with pressure ≡ 0 (Forced/BalancedThreeStack); legitimate for forced Navier-Stokes since solutions are shown unique in an energy comparison class, but it means the force is only constrained through smoothness, compact support, computability and uniqueness ; NavierStokesVelocity: def compile (B) (M) (w) : Program b N := ⟨B, M, w⟩ is trivial packaging; the effectiveness is carried by the fixed interpreter evaluate := Nat.rfindOpt (valueTrial ..) and the clause Represents, i.e. 'terminating compiler' there means the interpreter always halts with an ε-approximation (the genuinely computable compiler is Computable compileForce in NavierStokesAlternating) ; Three different machine models: Machine := ℕ × ℕ × ℕ × List ℕ × List (Option Rule) (Alternating), FiniteMachine with Option Transition (Forced/BalancedThreeStack), Mathlib Turing.TM0.Machine (Velocity), and 'halts' is ∃ n, isHalting (run n), Halts (reachable configuration without a transition) and (TM0.eval M w).Dom respectively; BalancedThreeStack and ForcedNavierStokesComputation share the theorem name OAI.BalancedTransport.balanced_three_stack_realization and differ only by a Fintype Direction instance
Carlos Toledo’s cert-machine
Finds the whole advertised result stated or implied Their term: “MATCHES”.
The challenge statements state the headline as OpenAI wrote it. Their record

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“The formalization constructs smooth forced three-dimensional Navier–Stokes flows from rest whose velocity fields detect whether a prescribed machine halts, at any positive computable viscosity. On the unit flat torus, halting is equivalent to the vertical velocity exceeding $1/2$ somewhere in a fixed observation strip. On $\mathbb R^2\times\mathbb T$, it is equivalent to the integral of the nonnegative vertical velocity over the observation half-plane times the circle exceeding $1/2$.”
Quoted from OpenAI’s Lean note for this family

An AI agent drafted an interpretation of that note, classifying this statement as “states a paper’s theorem as the paper does”. No human review of the draft is recorded.

Supporting material

The complete Lean statement file

1,275 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.

Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.

Links in the file: 647 to its own declarations, 460 to Mathlib’s documentation. 106 declared names also link to the same declaration in OpenAI’s library. 4 identifiers stay plain because they resolve to no single declaration: variables Lean binds automatically, notation, or names the scan of the pinned sources did not find. 2 of them could name more than one declaration. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

import Mathlibnamespace OAInoncomputable sectionnamespace VelocityDetectionopen scoped BigOperators Topology ContDiffopen Set Function Filterabbrev Coord (n : ℕ) := Fin n → ℝabbrev ScalarField (n : ℕ) := ℝ → Coord n → ℝabbrev VectorField (n : ℕ) := ℝ → Coord n → Coord ntheorem neZeroTwo : NeZero 2 := ⟨Nat.succ_ne_zero 1⟩theorem neZeroThree : NeZero 3 := ⟨Nat.succ_ne_zero 2⟩theorem neZeroFive : NeZero 5 := ⟨Nat.succ_ne_zero 4⟩def spatialD {n : ℕ} (i : Fin n) (q : ScalarField n) : ScalarField n :=  fun t x => deriv (fun s => q t (Function.update x i s)) (x i)def timeD {n : ℕ} (q : ScalarField n) : ScalarField n :=  fun t x => derivWithin (fun s => q s x) (Ici 0) tdef laplacian {n : ℕ} (q : ScalarField n) : ScalarField n :=  fun t x => ∑ i : Fin n, spatialD i (spatialD i q) t xdef advection {n : ℕ} (a : VectorField n) (q : ScalarField n) : ScalarField n :=  fun t x => ∑ i : Fin n, a t x i * spatialD i q t xdef divergence {n : ℕ} (a : VectorField n) : ScalarField n :=  fun t x => ∑ i : Fin n, spatialD i (fun s y => a s y i) t xdef NavierStokes (ν : ℝ) (u : VectorField 3) (p : ScalarField 3)    (f : VectorField 3) : Prop :=  (∀ (t : ℝ), 0 ≤ t → ∀ x : Coord 3, ∀ i : Fin 3,    timeD (fun s y => u s y i) t x + advection u (fun s y => u s y i) t x =      -spatialD i p t x + ν * laplacian (fun s y => u s y i) t x + f t x i) ∧  (∀ (t : ℝ), 0 ≤ t → ∀ x, divergence u t x = 0) ∧  (∀ x, u 0 x = 0)def horizontal (x : Coord 3) : Coord 2 := ![x 0, x 1]end VelocityDetectionendnoncomputable sectionnamespace VelocityDetection.Stacksopen scoped BigOperators Topology ContDiffopen Set Function Filterinductive Move  | right  | stay  | left  deriving DecidableEq, Reprdef update (b : ℕ) (m : Move) (β x y : ℕ) : ℕ × ℕ :=  match m with  | .right => (b * x + β, y / b)  | .stay => (x, y - y % b + β)  | .left => (x / b, x % b + b * β + b ^ 2 * (y / b))structure Rule (σ : Type*) (b : ℕ) where  target : σ  written : Fin b  move : Movestructure Configuration (σ : Type*) where  state : σ  leftStack : ℕ  rightStack : ℕ  deriving DecidableEqdef applyRule {σ : Type*} {b : ℕ} (r : Rule σ b) (c : Configuration σ) : Configuration σ :=  let st := update b r.move r.written c.leftStack c.rightStack  ⟨r.target, st.1, st.2⟩def address (B i x y : ℕ) : ℕ := 1 + x + B * y + B ^ 2 * idef capacity (b m n : ℕ) : ℕ := b ^ (m + n)end VelocityDetection.Stacksendnoncomputable sectionnamespace VelocityDetection.Expandingopen scoped BigOperators Topology ContDiffopen Set Function Filterdef lambda (D : ℝ) : ℝ := 4 * Ddef initialRadius (ν K D : ℝ) : ℝ :=  1024 * 3000 * (1 + ν) * lambda D * (K * D + 2)def radius (ν K D : ℝ) (n : ℕ) : ℝ := initialRadius ν K D * lambda D ^ nend VelocityDetection.Expandingendnoncomputable sectionnamespace VelocityDetection.Observationopen scoped BigOperators Topology ContDiffopen Set Function Filteropen MeasureTheorydef join (X : Coord 2) (z : ℝ) : Coord 3 := ![X 0, X 1, z]def torusEvent (u : VectorField 3) : Prop :=  letI := neZeroThree  ∃ t : ℝ, 0 ≤ t ∧ ∃ x : Coord 3,    1 / ((32 : ℕ) : ℝ) < x 1 ∧ x 1 < 1 / ((8 : ℕ) : ℝ) ∧ (1 / ((2 : ℕ) : ℝ) : ℝ) < u t x 2def upperHalfPlane : Set (Coord 2) := {X | 0 < X 1}def planeMass (u : VectorField 3) (t : ℝ) : ℝ :=  letI := neZeroThree  ∫ q in upperHalfPlane ×ˢ Ioc (0 : ℝ) 1,    u t (join q.1 q.2) 2 ∂(volume.prod volume)def planeEvent (u : VectorField 3) : Prop :=  ∃ t : ℝ, 0 ≤ t ∧ (1 / ((2 : ℕ) : ℝ) : ℝ) < planeMass u tend VelocityDetection.Observationendnoncomputable sectionnamespace VelocityDetection.SmoothProfilesopen scoped BigOperators Topology ContDiffopen Set Function Filteropen Set Function Filter MeasureTheoryopen scoped Topology BigOperators ContDiffabbrev step := Real.smoothTransitionend VelocityDetection.SmoothProfilesendnoncomputable sectionnamespace VelocityDetection.TranslationGatesopen scoped BigOperators Topology ContDiffopen Set Function Filteropen Set Function Filter MeasureTheoryopen scoped Topology BigOperators ContDiffopen SmoothProfilesdef window (s : ℝ) : ℝ := step (s + 3) * step (3 - s)end VelocityDetection.TranslationGatesendnoncomputable sectionnamespace VelocityDetection.CenterPathsopen scoped BigOperators Topology ContDiffopen Set Function Filteropen Set Function Filter MeasureTheoryopen scoped Topology BigOperators ContDiffopen scoped Topology ContDiff BigOperatorsopen SmoothProfilesdef ramp (r : ℝ) : ℝ := step (2 * r - 1 / 2)def theta (a T : ℝ) (j : ℕ) (t : ℝ) : ℝ := ramp (3 * (t - a) / T - j)def privateRow (S : ℝ) (k : ℕ) : ℝ := -((k : ℝ) + 2) * Sdef center (a T S S' σ : ℝ) (k l : ℕ) (t : ℝ) : Coord 2 :=  ![(1 - theta a T 1 t) * S * k + theta a T 1 t * S' * l,    -(1 - theta a T 0 t) * S +      (theta a T 0 t - theta a T 2 t) * privateRow S k + theta a T 2 t * σ * S']end VelocityDetection.CenterPathsendnoncomputable sectionnamespace VelocityDetection.UniformDerivativesopen scoped BigOperators Topology ContDiffopen Set Function Filteropen Set Function Filter MeasureTheoryopen scoped Topology BigOperators ContDiffopen scoped Topology ContDiff BigOperatorsvariable {I E F G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]    [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G]def Bounded (f : I → E → F) : Prop :=  ∀ n : ℕ, ∃ C : ℝ, 0 ≤ C ∧ ∀ a x, ‖iteratedFDeriv ℝ n (f a) x‖ ≤ Cend VelocityDetection.UniformDerivativesendnoncomputable sectionnamespace VelocityDetection.Stacksopen scoped BigOperators Topology ContDiffopen Set Function Filteropen Set Function Filter MeasureTheoryopen scoped Topology BigOperators ContDiffopen scoped Topology ContDiff BigOperatorsvariable {N b : ℕ} (hb : 0 < b) (table : Fin N → Fin b → Option (Rule (Fin N) b))def lookup (c : Configuration (Fin N)) : Option (Rule (Fin N) b) :=  table c.state ⟨c.rightStack % b, Nat.mod_lt _ hb⟩end VelocityDetection.Stacksendnoncomputable sectionnamespace VelocityDetection.TailSpaceopen scoped BigOperators Topology ContDiffopen Set Function Filteropen Set Function Filter MeasureTheoryopen scoped Topology BigOperators ContDiffopen scoped Topology ContDiff BigOperatorsopen scoped Topology ContDiff ZeroAtInftydef compatible (n : ℕ) : Submodule ℝ    (C₀(Coord n, ℝ) × Lp ℝ 1 (volume : Measure (Coord n))) where  carrier := {v | (fun X => v.2 X) =ᵐ[volume] (fun X => v.1 X)}  zero_mem' := by exact Lp.coeFn_zero ..  add_mem' := by    intro v w hv hw    change (fun X => (v.2 + w.2) X) =ᵐ[volume] (fun X => v.1 X + w.1 X)    change (fun X => v.2 X) =ᵐ[volume] (fun X => v.1 X) at hv    change (fun X => w.2 X) =ᵐ[volume] (fun X => w.1 X) at hw    filter_upwards [Lp.coeFn_add v.2 w.2, hv, hw] with X hadd hvx hwx    simpa [hvx, hwx] using hadd  smul_mem' := by    intro c v hv    change (fun X => (c • v.2) X) =ᵐ[volume] (fun X => c * v.1 X)    change (fun X => v.2 X) =ᵐ[volume] (fun X => v.1 X) at hv    filter_upwards [Lp.coeFn_smul c v.2, hv] with X hsmul hvx    simpa [hvx] using hsmulend VelocityDetection.TailSpaceendnoncomputable sectionnamespace VelocityDetection.Cylinderopen scoped BigOperators Topology ContDiffopen Set Function Filteropen Set Function Filter MeasureTheoryopen scoped Topology BigOperators ContDiffopen scoped Topology ContDiff BigOperatorsopen scoped Topology ContDiff ZeroAtInftyabbrev Space := Coord 2 × ℝabbrev Vect := Fin 3 → ℝdef measure : Measure Space := volume.prod (volume.restrict (Ioc (0 : ℝ) 1))def periodic (f : Space → ℝ) : Prop := ∀ X z, f (X, z + 1) = f (X, z)def frame (i : Fin 3) : Space := ![(![1, 0], 0), (![0, 1], 0), (0, 1)] idef D (i : Fin 3) (f : Space → ℝ) (x : Space) : ℝ := fderiv ℝ f x (frame i)structure SliceH2 (v : Space → Vect) : Prop where  smooth : ∀ i, ContDiff ℝ 2 (fun x => v x i)  per : ∀ i, periodic (fun x => v x i)  square_integrable : ∀ i, MemLp (fun x => v x i) 2 measure  derivative_square_integrable : ∀ i k, MemLp (D k (fun x => v x i)) 2 measure  second_square_integrable : ∀ i k l, MemLp (D l (D k (fun x => v x i))) 2 measurestructure PressureH1 (q : Space → ℝ) : Prop where  smooth : ContDiff ℝ 1 q  per : periodic q  square_integrable : MemLp q 2 measure  derivative_square_integrable : ∀ k, MemLp (D k q) 2 measuretheorem twoAtLeastTwo : Nat.AtLeastTwo 2 := ⟨Nat.le_refl 2⟩abbrev LpSpace {α : Type*} [MeasurableSpace α] (E : Type*) [NormedAddCommGroup E]    (p : ENNReal) (μ : Measure α) : Type _ := Lp E p μabbrev L2Space : Type :=  letI := twoAtLeastTwo  LpSpace ℝ 2 measuredef dt (u : ℝ → Space → Vect) (t : ℝ) (x : Space) (i : Fin 3) : ℝ :=  derivWithin (fun s => u s x i) (Ici 0) ttheorem spaceOuterMeasureClass : OuterMeasureClass (Measure Space) Space :=  Measure.instOuterMeasureClassdef continuousL2On (g : ℝ → Space → ℝ) (T : ℝ) : Prop :=  letI : IsTopologicalAddGroup ℝ := instIsTopologicalAddGroupReal  letI := spaceOuterMeasureClass  ∃ G : ℝ → L2Space, ContinuousOn G (Icc 0 T) ∧    ∀ t ∈ Icc 0 T, (fun x => G t x) =ᵐ[measure] g tdef continuousH2On (u : ℝ → Space → Vect) (T : ℝ) : Prop :=  (∀ t ∈ Icc 0 T, SliceH2 (u t)) ∧  (∀ i, continuousL2On (fun t x => u t x i) T) ∧  (∀ i k, continuousL2On (fun t => D k (fun x => u t x i)) T) ∧  (∀ i k l, continuousL2On (fun t => D l (D k (fun x => u t x i))) T)def continuousH1On (p : ℝ → Space → ℝ) (T : ℝ) : Prop :=  (∀ t ∈ Icc 0 T, PressureH1 (p t)) ∧ continuousL2On p T ∧  (∀ i, continuousL2On (fun t => D i (p t)) T)def C1L2On (u : ℝ → Space → Vect) (T : ℝ) : Prop :=  letI : IsTopologicalAddGroup ℝ := instIsTopologicalAddGroupReal  letI := spaceOuterMeasureClass  ∃ U dU : ℝ → Fin 3 → L2Space,    (∀ i, ContinuousOn (fun t => U t i) (Icc 0 T)) ∧    (∀ i, ContinuousOn (fun t => dU t i) (Icc 0 T)) ∧    (∀ t ∈ Icc 0 T, ∀ i, (fun x => U t i x) =ᵐ[measure] (fun x => u t x i)) ∧    (∀ t ∈ Icc 0 T, ∀ i, (fun x => dU t i x) =ᵐ[measure] (fun x => dt u t x i)) ∧    (∀ t ∈ Icc 0 T, ∀ i,      HasDerivWithinAt (fun s => U s i) (dU t i) (Icc 0 T) t)structure ComparisonClass (u : ℝ → Space → Vect) (p : ℝ → Space → ℝ) : Prop where  velocity_H2 : ∀ T > 0, continuousH2On u T  velocity_C1L2 : ∀ T > 0, C1L2On u T  pressure_H1 : ∀ T > 0, continuousH1On p T  time_derivative : ∀ t ≥ 0, ∀ x i,    HasDerivWithinAt (fun s => u s x i) (dt u t x i) (Ici 0) t  velocity_continuous : ∀ T > 0, ∀ i,    ContinuousOn (fun y : ℝ × Space => u y.1 y.2 i) (Icc 0 T ×ˢ univ)  time_continuous : ∀ T > 0, ∀ i,    ContinuousOn (fun y : ℝ × Space => dt u y.1 y.2 i) (Icc 0 T ×ˢ univ)  gradient_continuous : ∀ T > 0, ∀ i k,    ContinuousOn (fun y : ℝ × Space => D k (fun x => u y.1 x i) y.2) (Icc 0 T ×ˢ univ)  second_continuous : ∀ T > 0, ∀ i k l,    ContinuousOn (fun y : ℝ × Space => D l (D k (fun x => u y.1 x i)) y.2) (Icc 0 T ×ˢ univ)  pressure_continuous : ∀ T > 0,    ContinuousOn (fun y : ℝ × Space => p y.1 y.2) (Icc 0 T ×ˢ univ)  pressure_gradient_continuous : ∀ T > 0, ∀ i,    ContinuousOn (fun y : ℝ × Space => D i (p y.1) y.2) (Icc 0 T ×ˢ univ)  bounds : ∀ T > 0, ∃ B : ℝ, 0 ≤ B ∧    (∀ t ∈ Icc 0 T, ∀ x i, |u t x i| ≤ B) ∧    (∀ t ∈ Icc 0 T, ∀ x i k, |D k (fun y => u t y i) x| ≤ B)def join (x : Space) : Coord 3 :=  letI := neZeroTwo  ![x.1 0, x.1 1, x.2]end VelocityDetection.Cylinderendnoncomputable sectionnamespace VelocityDetection.TailSpaceopen scoped BigOperators Topology ContDiffopen Set Function Filteropen Set Function Filter MeasureTheoryopen scoped Topology BigOperators ContDiffopen scoped Topology ContDiff BigOperatorsopen scoped Topology ContDiff ZeroAtInftydef evalLinear (X : Coord 2) : compatible 2 →ₗ[ℝ] ℝ where  toFun f := f.val.1 X  map_add' _ _ := rfl  map_smul' _ _ := rfldef eval (X : Coord 2) : compatible 2 →L[ℝ] ℝ where  toLinearMap := evalLinear X  cont := AddMonoidHomClass.continuous_of_bound (evalLinear X) 1 (fun f => by    change ‖f.val.1 X‖ ≤ 1 * ‖f.val‖    rw [one_mul]    exact (BoundedContinuousFunction.norm_coe_le_norm f.val.1.toBCF X).trans (norm_fst_le f.val))end VelocityDetection.TailSpaceendnoncomputable sectionnamespace VelocityDetection.Historyopen scoped BigOperators Topology ContDiffopen Set Function Filteropen Set Function Filter MeasureTheoryopen scoped Topology BigOperators ContDiffopen scoped Topology ContDiff BigOperatorsopen scoped Topology ContDiff ZeroAtInftyopen scoped Topology ContDiff ZeroAtInfty BigOperatorsopen scoped Topologyopen Stacksstructure Configuration (N : ℕ) where  tape : Stacks.Configuration (Fin N)  history : ℕ  deriving DecidableEqend VelocityDetection.Historyendnoncomputable sectionnamespace VelocityDetection.Historyopen scoped BigOperators Topology ContDiffopen Set Function Filteropen Set Function Filter MeasureTheoryopen scoped Topology BigOperators ContDiffopen scoped Topology ContDiff BigOperatorsopen scoped Topology ContDiff ZeroAtInftyopen scoped Topology ContDiff ZeroAtInfty BigOperatorsopen scoped Topologyopen Stacksvariable {N b : ℕ} (hb : 0 < b)  (table : Fin N → Fin b → Option (Rule (Fin N) b))def radix (N b : ℕ) : ℕ := N * bdef tag (c : Stacks.Configuration (Fin N)) : ℕ := b * c.state.val + c.rightStack % binclude hb indef applyRule (r : Rule (Fin N) b) (c : Configuration N) : Configuration N :=  ⟨Stacks.applyRule r c.tape, radix N b * c.history + tag (b := b) c.tape⟩include hb indef packedState (c : Configuration N) : ℕ := N * c.history + c.tape.state.valdef address (B : ℕ) (c : Configuration N) : ℕ :=  Stacks.address B (packedState c) c.tape.leftStack c.tape.rightStackabbrev Box (N B H : ℕ) := Fin N × Fin B × Fin B × Fin Hdef config {B H : ℕ} (c : Box N B H) : Configuration N :=  ⟨⟨c.1, c.2.1, c.2.2.1⟩, c.2.2.2⟩def Active (B H : ℕ) := {c : Box N B H // (Stacks.lookup hb table (config c).tape).isSome}def rule {B H : ℕ} (c : Active hb table B H) : Rule (Fin N) b :=  (Stacks.lookup hb table (config c.val).tape).get c.propertydef target {B H : ℕ} (c : Active hb table B H) : Configuration N :=  applyRule (rule hb table c) (config c.val)def sourceAddress {B H : ℕ} (c : Active hb table B H) : ℕ := address B (config c.val)def targetAddress {B H : ℕ} (c : Active hb table B H) : ℕ := address (b * B) (target hb table c)end VelocityDetection.Historyendnoncomputable sectionnamespace VelocityDetection.TapeCodesopen scoped BigOperators Topology ContDiffopen Set Function Filteropen Set Function Filter MeasureTheoryopen scoped Topology BigOperators ContDiffopen scoped Topology ContDiff BigOperatorsopen scoped Topology ContDiff ZeroAtInftyopen scoped Topology ContDiff ZeroAtInfty BigOperatorsopen scoped Topologyopen Turing Stacksvariable {b N : ℕ} [NeZero b] [NeZero N]def word (w : List (Fin b)) : ℕ := Nat.ofDigits b (w.map Fin.val)def half (w : ListBlank (Fin b)) : ℕ :=  w.liftOn word (by sorry)def tape (q : Fin N) (T : Tape (Fin b)) : Stacks.Configuration (Fin N) :=  ⟨q, half T.left, half T.right₀⟩def rule (a : Fin b) (q : Fin N) : TM0.Stmt (Fin b) → Rule (Fin N) b  | .move .left => ⟨q, a, .left⟩  | .move .right => ⟨q, a, .right⟩  | .write β => ⟨q, β, .stay⟩def table (M : TM0.Machine (Fin b) (Fin N)) : Fin N → Fin b → Option (Rule (Fin N) b) :=  fun q a => (M q a).map (fun p => rule a p.1 p.2)end VelocityDetection.TapeCodesendnoncomputable sectionnamespace VelocityDetection.Preludeopen scoped BigOperators Topology ContDiffopen Set Function Filteropen Set Function Filter MeasureTheoryopen scoped Topology BigOperators ContDiffopen scoped Topology ContDiff BigOperatorsopen scoped Topology ContDiff ZeroAtInftyopen scoped Topology ContDiff ZeroAtInfty BigOperatorsopen scoped Topologyopen Stacksvariable {N b : ℕ} (hb : 0 < b)  (table : Fin N → Fin b → Option (Rule (Fin N) b)) (q₀ : Fin N)def rule (r : Rule (Fin N) b) : Rule (Fin (N + 1)) b :=  ⟨r.target.castSucc, r.written, r.move⟩def table' : Fin (N + 1) → Fin b → Option (Rule (Fin (N + 1)) b) :=  Fin.lastCases (fun a => some ⟨q₀.castSucc, a, .stay⟩)    (fun q a => (table q a).map rule)def initial (x y : ℕ) : Configuration (Fin (N + 1)) := ⟨Fin.last N, x, y⟩end VelocityDetection.Preludeendnoncomputable sectionnamespace VelocityDetection.MachineHistoryopen scoped BigOperators Topology ContDiffopen Set Function Filteropen Set Function Filter MeasureTheoryopen scoped Topology BigOperators ContDiffopen scoped Topology ContDiff BigOperatorsopen scoped Topology ContDiff ZeroAtInftyopen scoped Topology ContDiff ZeroAtInfty BigOperatorsopen scoped Topologyopen Turing Stacksvariable {b N : ℕ} [NeZero b] [NeZero N]def table (M : TM0.Machine (Fin b) (Fin N)) :    Fin (N + 1) → Fin b → Option (Rule (Fin (N + 1)) b) :=  Prelude.table' (TapeCodes.table M) 0def initial (w : List (Fin b)) : Stacks.Configuration (Fin (N + 1)) :=  Prelude.initial 0 (TapeCodes.word w)end VelocityDetection.MachineHistoryendnoncomputable sectionnamespace VelocityDetection.Effectiveopen Polynomial Set Function Filteropen scoped BigOperators Topology ContDiffabbrev Poly := List (ℕ × ℚ)noncomputable def poly : Poly → Polynomial ℝ  | [] => 0  | (k,q)::ps => Polynomial.C (q:ℝ)*Polynomial.X^k + poly psdef nextPoly : Poly → Poly  | [] => []  | (k,q)::ps => (k+2,q)::(k+1,-q*k)::nextPoly psnoncomputable def flat (p : Poly) (x : ℝ) : ℝ :=  (poly p).eval x⁻¹ * expNegInvGlue xdef polyBound : Poly → ℚ  | [] => 0  | (k,q)::ps => |q| *k.factorial + polyBound psinductive Expr (n : ℕ) where  | rat : ℚ → Expr n  | var : Fin n → Expr n  | add : Expr n → Expr n → Expr n  | neg : Expr n → Expr n  | mul : Expr n → Expr n → Expr n  | inv : Expr n → Expr n  | flat : Poly → Expr n → Expr n  deriving Inhabitedend VelocityDetection.Effectiveendnoncomputable sectionnamespace VelocityDetection.Effective.Expropen Polynomial Set Function Filteropen scoped BigOperators Topology ContDiffvariable {n : ℕ}noncomputable def eval (x : Fin n → ℝ) : Expr n → ℝ  | .rat q => q  | .var i => x i  | .add a b => a.eval x + b.eval x  | .neg a => -a.eval x  | .mul a b => a.eval x * b.eval x  | .inv a => (a.eval x)⁻¹  | .flat p a => Effective.flat p (a.eval x)def diff (i : Fin n) : Expr n → Expr n  | .rat _ => .rat 0  | .var j => .rat (if i=j then 1 else 0)  | .add a b => .add (a.diff i) (b.diff i)  | .neg a => .neg (a.diff i)  | .mul a b => .add (.mul (a.diff i) b) (.mul a (b.diff i))  | .inv a => .neg (.mul (a.diff i) (.mul (.inv a) (.inv a)))  | .flat p a => .mul (.flat (nextPoly p) a) (a.diff i)def jet : List (Fin n) → Expr n → Expr n  | [], e => e  | i::is, e => jet is (e.diff i)end VelocityDetection.Effective.Exprendnoncomputable sectionnamespace VelocityDetection.Effectiveopen Set Filter Functionopen scoped BigOperators Topologystructure Ball where  center : ℚ  radius : ℚ  deriving Inhabiteddef polyEval : Poly → ℚ → ℚ  | [], _ => 0  | (k,q)::ps, x => q*x^k+polyEval ps xdef expSum (q : ℚ) (n : ℕ) : ℚ := ∑ k ∈ Finset.range n, q^k / k.factorialdef expError (q : ℚ) (n : ℕ) : ℚ := |q|^n / n.factorial * 2def flatRound (p : Poly) (q : ℚ) (n : ℕ) : Ball :=  if q ≤ 0 then ⟨0,0⟩ else  if |q⁻¹|/(n+1) ≤ (1/2:ℚ) ∧      |polyEval p q⁻¹| *expError (-q⁻¹) n ≤ polyBound (nextPoly p)*|q| then    ⟨polyEval p q⁻¹*expSum (-q⁻¹) n,|polyEval p q⁻¹| *expError (-q⁻¹) n⟩  else ⟨0,polyBound (nextPoly p)*|q|⟩end VelocityDetection.Effectiveendnoncomputable sectionnamespace VelocityDetection.Effective.Ballopen Set Filter Functionopen scoped Topologydef atom (q : ℚ) : Ball := ⟨q,0⟩def add (a b : Ball) : Ball := ⟨a.center+b.center,a.radius+b.radius⟩def neg (a : Ball) : Ball := ⟨-a.center,a.radius⟩def mul (a b : Ball) : Ball :=  ⟨a.center*b.center,|a.center| *b.radius+|b.center| *a.radius+a.radius*b.radius⟩def inv (a : Ball) : Ball :=  ⟨a.center⁻¹,a.radius/(|a.center| *(|a.center|-a.radius))⟩def invSafe (a : Ball) : Bool := decide (a.radius < |a.center|)def flat (p : Poly) (a : Ball) (k : ℕ) : Ball :=  let b := flatRound p a.center k  ⟨b.center,b.radius+polyBound (nextPoly p)*a.radius⟩end VelocityDetection.Effective.Ballendnoncomputable sectionnamespace VelocityDetection.Effective.Expropen Set Filter Functionopen scoped Topologyvariable {n : ℕ}def round (a : Fin n → Ball) (k : ℕ) : Expr n → Ball :=  Expr.rec (motive := fun _ => Ball)    Ball.atom a    (fun _ _ e f => e.add f)    (fun _ e => e.neg)    (fun _ _ e f => e.mul f)    (fun _ e => e.inv)    (fun p _ e => e.flat p k)def safe (a : Fin n → Ball) (k : ℕ) : Expr n → Bool :=  Expr.rec (motive := fun _ => Bool)    (fun _ => true) (fun _ => true)    (fun _ _ e f => e && f)    (fun _ e => e)    (fun _ _ e f => e && f)    (fun e safe_e => safe_e && (e.round a k).invSafe)    (fun _ _ e => e)end VelocityDetection.Effective.Exprendnoncomputable sectionnamespace VelocityDetection.Effectiveopen Set Filter Functionopen scoped Topologynoncomputable def coordinateD {n : ℕ} (i : Fin n) (f : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) : ℝ :=  deriv (fun s => f (update x i s)) (x i)noncomputable def mixedD {n : ℕ} : List (Fin n) → ((Fin n → ℝ) → ℝ) → (Fin n → ℝ) → ℝ  | [], f => f  | i::is, f => mixedD is (coordinateD i f)def accuracy (k : ℕ) : ℚ := (1/2)^kdef Names {n : ℕ} (q : Fin n → ℕ → ℚ) (x : Fin n → ℝ) : Prop :=  ∀ i k, |x i-(q i k:ℝ)| ≤ (accuracy k:ℝ)def inputBall {n : ℕ} (q : Fin n → ℕ → ℚ) (k : ℕ) (i : Fin n) : Ball :=  ⟨q i k,accuracy k⟩def trial {n : ℕ} (e : Expr n) (is : List (Fin n)) (q : Fin n → ℕ → ℚ)    (ε : ℚ) (k : ℕ) : Option ℚ :=  let d := e.jet is  let a := inputBall q k  if d.safe a k && decide ((d.round a k).radius ≤ ε) then some (d.round a k).center else noneend VelocityDetection.Effectiveendnoncomputable sectionnamespace VelocityDetection.PeriodicSpaceopen Set Function Filter MeasureTheoryopen scoped Topology ContDiff BigOperators BoundedContinuousFunctionabbrev Torus (n : ℕ) := Fin n → AddCircle (1 : ℝ)def cover {n : ℕ} (X : Coord n) : Torus n := fun i => (X i : AddCircle (1 : ℝ))end VelocityDetection.PeriodicSpaceendnoncomputable sectionnamespace VelocityDetection.SmoothBumpopen Set Function Filter MeasureTheoryopen scoped Topology ContDiff BigOperatorsopen TranslationGatesdef profile (s : ℝ) : ℝ := window (((3 : ℕ) : ℝ)*s)end VelocityDetection.SmoothBumpendnoncomputable sectionnamespace VelocityDetection.TorusClassopen Set Function Filter MeasureTheoryopen scoped Topology ContDiff BigOperatorsabbrev Space := Coord 3def measure : Measure Space := volume.restrict (Icc (0 : Space) 1)def periodic (f : Space → ℝ) : Prop := FactorsThrough f PeriodicSpace.coverdef frame (i : Fin 3) : Space := Pi.single i 1def D (i : Fin 3) (f : Space → ℝ) (x : Space) : ℝ := fderiv ℝ f x (frame i)def dt (u : VectorField 3) (t : ℝ) (x : Space) (i : Fin 3) : ℝ :=  derivWithin (fun s => u s x i) (Ici 0) tstructure ComparisonClass (u : VectorField 3) (p : ScalarField 3) : Prop where  velocity_slices : ∀ t ≥ 0, ∀ i, ContDiff ℝ 2 (fun x => u t x i)  pressure_slices : ∀ t ≥ 0, ContDiff ℝ 1 (p t)  velocity_periodic : ∀ t ≥ 0, FactorsThrough (u t) PeriodicSpace.cover  pressure_periodic : ∀ t ≥ 0, periodic (p t)  pressure_mean : ∀ t ≥ 0, (∫ x, p t x ∂measure) = 0  time_derivative : ∀ t ≥ 0, ∀ x i,    HasDerivWithinAt (fun s => u s x i) (dt u t x i) (Ici 0) t  velocity_continuous : ∀ T > 0, ∀ i,    ContinuousOn (fun y : ℝ × Space => u y.1 y.2 i) (Icc 0 T ×ˢ univ)  time_continuous : ∀ T > 0, ∀ i,    ContinuousOn (fun y : ℝ × Space => dt u y.1 y.2 i) (Icc 0 T ×ˢ univ)  gradient_continuous : ∀ T > 0, ∀ i k,    ContinuousOn (fun y : ℝ × Space => D k (fun x => u y.1 x i) y.2) (Icc 0 T ×ˢ univ)  second_continuous : ∀ T > 0, ∀ i k l,    ContinuousOn (fun y : ℝ × Space => D l (D k (fun x => u y.1 x i)) y.2) (Icc 0 T ×ˢ univ)  pressure_continuous : ∀ T > 0,    ContinuousOn (fun y : ℝ × Space => p y.1 y.2) (Icc 0 T ×ˢ univ)  pressure_gradient_continuous : ∀ T > 0, ∀ i,    ContinuousOn (fun y : ℝ × Space => D i (p y.1) y.2) (Icc 0 T ×ˢ univ)end VelocityDetection.TorusClassendnoncomputable sectionnamespace VelocityDetection.MachineTorusopen Set Function MeasureTheoryopen scoped Topology ContDiff BigOperatorsopen Turing Stacksvariable {b N : ℕ} [NeZero b] [NeZero N]def initialAddress (w : List (Fin b)) : ℕ :=  History.address (capacity b (w.length+1) 0) ⟨MachineHistory.initial (N := N) w,0⟩end VelocityDetection.MachineTorusendnoncomputable sectionnamespace VelocityDetection.Effective.Expropen Set Function Filteropen scoped Topology BigOperatorsvariable {n m : ℕ}instance : Add (Expr n) := ⟨Expr.add⟩instance : Neg (Expr n) := ⟨Expr.neg⟩instance : Sub (Expr n) := ⟨fun a b => .add a (.neg b)⟩instance : Mul (Expr n) := ⟨Expr.mul⟩instance : Inv (Expr n) := ⟨Expr.inv⟩instance : Div (Expr n) := ⟨fun a b => .mul a (.inv b)⟩instance (k : ℕ) : OfNat (Expr n) k := ⟨.rat k⟩def subst (v : Fin m → Expr n) : Expr m → Expr n :=  Expr.rec (motive := fun _ => Expr n)    Expr.rat v    (fun _ _ a b => .add a b)    (fun _ a => .neg a)    (fun _ _ a b => .mul a b)    (fun _ a => .inv a)    (fun p _ a => .flat p a)def sumList : List (Expr n) → Expr n  | [] => 0  | e::es => e + sumList esdef sumFin (k : ℕ) (f : Fin k → Expr n) : Expr n := sumList (List.ofFn f)def unaryD (e : Expr 1) (a : Expr n) : Expr n := (e.diff 0).subst (fun _ => a)end VelocityDetection.Effective.Exprendnoncomputable sectionnamespace VelocityDetection.Effective.Recipeopen Set Function Filteropen scoped Topology BigOperatorsopen _root_.OAI.VelocityDetection.Effective.Exprvariable {n : ℕ}def glue (a : Expr n) : Expr n := .flat [(0,1)] adef step (a : Expr n) : Expr n := glue a/(glue a+glue (1-a))def pulse (a : Expr n) : Expr n := (step (.var 0 : Expr 1)).unaryD adef window (a : Expr n) : Expr n := step (a+3)*step (3-a)def windowD (a : Expr n) : Expr n := pulse (a+3)*step (3-a)-step (a+3)*pulse (3-a)def theta (a T : Expr n) (j : ℕ) (t : Expr n) : Expr n :=  step (2*(3*(t-a)/T-.rat j)-.rat (1/2))def center (a T S S' σ : Expr n) (k l : ℕ) (t : Expr n) : Fin 2 → Expr n :=  ![(1-theta a T 1 t)*S*.rat k+theta a T 1 t*S'*.rat l,    -(1-theta a T 0 t)*S+(theta a T 0 t-theta a T 2 t)*(-(.rat k+2)*S)+      theta a T 2 t*σ*S']def gate (R : Expr n) (c G X : Fin 2 → Expr n) : Fin 2 → Expr n :=  letI := neZeroTwo  ![window ((X 0-c 0)/R)*(windowD ((X 1-c 1)/R)/R)*      (G 0*(X 1-c 1)-G 1*(X 0-c 0))+      window ((X 0-c 0)/R)*window ((X 1-c 1)/R)*G 0,    window ((X 0-c 0)/R)*window ((X 1-c 1)/R)*G 1-      (windowD ((X 0-c 0)/R)/R*window ((X 1-c 1)/R))*        (G 0*(X 1-c 1)-G 1*(X 0-c 0))]def impulse (t : Expr n) (p X : Fin 2 → Expr n) : Expr n :=  letI := neZeroTwo  pulse t*pulse (X 0-p 0+.rat (1/2))*pulse (X 1-p 1+.rat (1/2))def packet (R : Expr n) (X : Fin 2 → Expr n) : Expr n :=  letI := neZeroTwo  window (3*(X 0/R))*window (3*(X 1/R))end VelocityDetection.Effective.Recipeendnoncomputable sectionnamespace VelocityDetection.Effective.Expropen Set Functionopen scoped BigOperators Topologyvariable {n : ℕ}def activeSum {N b B H : ℕ} (hb : 0 < b)    (table : Fin N → Fin b → Option (Stacks.Rule (Fin N) b))    (f : History.Active hb table B H → Expr n) : Expr n :=  sumFin N (fun s => sumFin B (fun l => sumFin B (fun r => sumFin H (fun h =>    if hp : (Stacks.lookup hb table (History.config (s,l,r,h)).tape).isSome then      f ⟨(s,l,r,h),hp⟩ else 0))))end VelocityDetection.Effective.Exprendnoncomputable sectionnamespace VelocityDetection.Effective.ArrayRecipeopen Set Functionopen scoped BigOperators Topologyopen _root_.OAI.VelocityDetection.Effective.Expr Stacksvariable {N b : ℕ} (hN : 0 < N) (hb : 0 < b)  (table : Fin N → Fin b → Option (Rule (Fin N) b)) (m : ℕ)abbrev Code := Expr 5def K (N b m : ℕ) : ℕ := N * capacity b (m+1) 0 ^ 2def D (N b : ℕ) : ℕ := b^2 * History.radix N bdef radius (N b m n : ℕ) : Code :=  .rat (1024*3000*(4*(D N b))*(K N b m*D N b+2)*(4*D N b)^n) * (1+.var 0)def spacing (N b m n : ℕ) : Code := 16*radius N b m ndef duration (N b m n : ℕ) : Code :=  spacing N b m (n+1) * .rat (K N b m*D N b^(n+1)+2)def start (N b m : ℕ) : ℕ → Code  | 0 => 1  | n+1 => start N b m n+duration N b m ndef sign (c : History.Configuration N) : ℚ :=  if (lookup hb table c.tape).isNone then 1 else -1abbrev Instruction (n : ℕ) := History.Active hb table (capacity b (m+1) n) (History.radix N b^n)def path (n : ℕ) (c : Instruction hb table m n) : Fin 2 → Code :=  Recipe.center (start N b m n) (duration N b m n) (spacing N b m n)    (spacing N b m (n+1)) (.rat (sign hb table (History.target hb table c)))    (History.sourceAddress hb table c) (History.targetAddress hb table c) (.var 1)def gate (n : ℕ) (c : Instruction hb table m n) : Fin 2 → Code :=  Recipe.gate (radius N b m n) (path hb table m n c)    (fun i => (path hb table m n c i).diff 1) ![.var 2,.var 3]def stage (n : ℕ) (i : Fin 2) : Code :=  activeSum hb table (fun c : Instruction hb table m n => gate hb table m n c i)def field (L : ℕ) (i : Fin 2) : Code := sumFin L (fun n => stage hb table m n i)end VelocityDetection.Effective.ArrayRecipeendnoncomputable sectionnamespace VelocityDetection.Effective.ChartRecipeopen Set Function ArrayRecipeopen scoped BigOperators Topologyopen VelocityDetection.Effective.Exprvariable {N b : ℕ} (hN : 0 < N) (hb : 0 < b)  (table : Fin N → Fin b → Option (Stacks.Rule (Fin N) b)) (m : ℕ)def scale (N b m P : ℕ) : ℚ := (1024*((K N b m:ℚ)*(D N b:ℚ)^(P+1)+4))⁻¹def radius (N b m P : ℕ) : ℚ := scale N b m P/16def targetHeight (P n : ℕ) (c : Instruction hb table m n) : ℚ :=  if ArrayRecipe.sign hb table (History.target hb table c) = 1 then -(7/16) else -scale N b m Pdef path (P n : ℕ) (c : Instruction hb table m n) : Fin 2 → Code :=  letI := neZeroFive  fun i =>    .rat (![1/4,1/2] i) + Recipe.center (.rat n) 1 (.rat (scale N b m P)) (.rat (scale N b m P))      (.rat (targetHeight hb table m P n c/scale N b m P))      (History.sourceAddress hb table c) (History.targetAddress hb table c) (.var 1) idef gate (P n : ℕ) (c : Instruction hb table m n) : Fin 2 → Code :=  letI := neZeroFive  Recipe.gate (.rat (radius N b m P)) (path hb table m P n c)    (fun i => (path hb table m P n c i).diff 1) ![.var 2,.var 3]def stage (P n : ℕ) (i : Fin 2) : Code :=  activeSum hb table (fun c : Instruction hb table m n => gate hb table m P n c i)def prefixCode (P : ℕ) (i : Fin 2) : Code := sumFin P (fun n => stage hb table m P n i)def duration (N b m B k : ℕ) : Code :=  letI := neZeroFive  .rat ((1/16)*(1/2:ℚ)^k) /    (3*(1+.var 0*.rat (2*(B:ℚ)/(radius N b m (k+1))^2)))def localTime (N b m B k : ℕ) : Code :=  letI := neZeroFive  (.var 1-.rat (k+1))/duration N b m B kdef weight (N b m B k : ℕ) : Code :=  Recipe.step (8*localTime N b m B k)-Recipe.step (8*localTime N b m B k-.rat 7)def clock (N b m B k : ℕ) : Code := .rat (k+1)*  (Recipe.step (8*localTime N b m B k-1)-Recipe.step (8*localTime N b m B k-.rat 5))def rawField (B k : ℕ) (i : Fin 2) : Code :=  letI := neZeroFive  (clock N b m B k).diff 1 * (prefixCode hb table m (k+1) i).subst    ![.var 0,clock N b m B k,.var 2,.var 3,.var 4]def initial (N b m P q : ℕ) : Fin 2 → Code :=  ![.rat (1/4+scale N b m P*q),.rat (1/2-scale N b m P)]def rawSource (B q k : ℕ) : Code :=  letI := neZeroFive  (weight N b m B k).diff 1 *    Recipe.packet (.rat (radius N b m (k+1)))      (fun i => (![.var 2,.var 3] i)-initial N b m (k+1) q i)end VelocityDetection.Effective.ChartRecipeendnoncomputable sectionnamespace VelocityDetection.Effectiveopen Set Functionopen scoped Topology BigOperatorsopen _root_.OAI.VelocityDetection.Effective.Expr ArrayRecipedef periodize (R : ℕ) (e : Code) : Code :=  letI := neZeroFive  sumFin (2*R+1) (fun i => sumFin (2*R+1) (fun j =>    e.subst ![.var 0,.var 1,.var 2-.rat ((i:ℚ)-R),.var 3-.rat ((j:ℚ)-R),.var 4]))end VelocityDetection.Effectiveendnoncomputable sectionnamespace VelocityDetection.Effective.ChartRecipeopen Set Functionopen scoped Topology BigOperatorsopen _root_.OAI.VelocityDetection.Effective.Expr ArrayRecipevariable {N b : ℕ} (hN : 0 < N) (hb : 0 < b)  (table : Fin N → Fin b → Option (Stacks.Rule (Fin N) b)) (m : ℕ)def fieldBlock (B R k : ℕ) (i : Fin 2) : Code := periodize R (rawField hb table m B k i)def sourceBlock (N b m B q R k : ℕ) : Code := periodize R (rawSource (N:=N) (b:=b) m B q k)def field (B R L : ℕ) (i : Fin 2) : Code := sumFin L (fun k => fieldBlock hb table m B R k i)def source (N b m B q R L : ℕ) : Code := sumFin L (fun k => sourceBlock N b m B q R k)end VelocityDetection.Effective.ChartRecipeendnoncomputable sectionnamespace VelocityDetection.Effectiveopen Set Filter Functionopen scoped Topology BigOperators ContDiffopen VelocityDetection.Effective.Expr ArrayRecipedef residualCode (a : Fin 2 → Code) (i : Fin 2) : Code :=  letI := neZeroTwo  letI := neZeroFive  (a i).diff 1 + a 0*(a i).diff 2 + a 1*(a i).diff 3 -    .var 0*((((a i).diff 2).diff 2)+(((a i).diff 3).diff 3))end VelocityDetection.Effectiveendnoncomputable sectionnamespace VelocityDetection.Effective.ArrayRecipeopen Set Filter Function Turingopen scoped Topology BigOperators ContDiffopen VelocityDetection.Effective.Expr ArrayRecipedef initialCode (N b m q : ℕ) : Fin 2 → Code :=  ![spacing N b m 0 * .rat q,-spacing N b m 0]def source (N b m q : ℕ) : Code :=  letI := neZeroFive  Recipe.impulse (.var 1) (initialCode N b m q) ![.var 2,.var 3]end VelocityDetection.Effective.ArrayRecipeendnoncomputable sectionnamespace VelocityDetection.Effectiveopen Set Filter Function Turingopen scoped Topology BigOperators ContDiffopen VelocityDetection.Effective.Expr ArrayRecipenoncomputable def forceFunction (f : ℝ → VectorField 3) (i : Fin 3) (x : Fin 5 → ℝ) : ℝ :=  letI := neZeroFive  f (x 0) (x 1) ![x 2,x 3,x 4] iend VelocityDetection.Effectiveendnoncomputable sectionnamespace VelocityDetection.Effective.MachineRecipeopen Set Filter Function Turingopen scoped Topology BigOperators ContDiffopen VelocityDetection.Effective.Expr ArrayRecipevariable {b N : ℕ} [NeZero b] [NeZero N]inductive Domain where | torus | cylinder  deriving DecidableEq, Reprdef field (d : Domain) (B R L : ℕ) (M : TM0.Machine (Fin b) (Fin N))    (w : List (Fin b)) (i : Fin 2) : Code := match d with  | .torus => ChartRecipe.field (NeZero.pos b) (MachineHistory.table M) w.length B R L i  | .cylinder => ArrayRecipe.field (NeZero.pos b) (MachineHistory.table M) w.length L idef source (d : Domain) (B R L : ℕ) (w : List (Fin b)) : Code := match d with  | .torus => ChartRecipe.source (N+1) b w.length B (MachineTorus.initialAddress (N:=N) w) R L  | .cylinder => ArrayRecipe.source (N+1) b w.length (MachineTorus.initialAddress (N:=N) w)def force (d : Domain) (B R L : ℕ) (M : TM0.Machine (Fin b) (Fin N))    (w : List (Fin b)) (i : Fin 3) : Code :=  letI := neZeroTwo  ![residualCode (field d B R L M w) 0,residualCode (field d B R L M w) 1,    source (N:=N) d B R L w] iend VelocityDetection.Effective.MachineRecipeendnoncomputable sectionnamespace VelocityDetection.Effective.MachineRecipeopen Set Filter Function Turingopen scoped Topology ContDiff BigOperatorsvariable {b N : ℕ} [NeZero b] [NeZero N]def timeCutoff (q : Fin 5 → ℕ → ℚ) : ℕ :=  letI := neZeroFive  ⌈q 1 0+2⌉₊def spaceCutoff (q : Fin 5 → ℕ → ℚ) : ℕ :=  letI := neZeroFive  ⌈|q 2 0|+|q 3 0|+3⌉₊def runTrial (d : Domain) (B : ℕ) (M : TM0.Machine (Fin b) (Fin N))    (w : List (Fin b)) (i : Fin 3) (is : List (Fin 5)) (q : Fin 5 → ℕ → ℚ)    (ε : ℚ) (k : ℕ) : Option ℚ :=  trial (force d B (spaceCutoff q) (timeCutoff q) M w i) is q ε kend VelocityDetection.Effective.MachineRecipeendnoncomputable sectionnamespace VelocityDetection.Effectiveopen Set Filter Functionopen scoped Topology BigOperatorsstructure RationalBox (n : ℕ) where  lower : Fin n → ℚ  upper : Fin n → ℚ  ordered : ∀ i, lower i ≤ upper iend VelocityDetection.Effectiveendnoncomputable sectionnamespace VelocityDetection.Effective.RationalBoxopen Set Filter Functionopen scoped Topology BigOperatorsvariable {n : ℕ} (Q : RationalBox n)def carrier : Set (Fin n → ℝ) := Icc (fun i => (Q.lower i:ℝ)) (fun i => (Q.upper i:ℝ))def cell (k : ℕ) (j : Fin n → Fin (k+2)) (i : Fin n) : Ball :=  ⟨Q.lower i+(Q.upper i-Q.lower i)*((j i:ℕ):ℚ)/(k+1),    (Q.upper i-Q.lower i)/(k+1)⟩def boundTrial (e : Expr n) (is : List (Fin n)) (k : ℕ) : Option ℚ :=  if ∀ j : Fin n → Fin (k+2), (e.jet is).safe (Q.cell k j) k = true then    some (∑ j : Fin n → Fin (k+2),      (|((e.jet is).round (Q.cell k j) k).center| + |((e.jet is).round (Q.cell k j) k).radius|))  else noneend VelocityDetection.Effective.RationalBoxendnoncomputable sectionnamespace VelocityDetection.Effective.MachineRecipeopen Set Function Turingvariable {b N : ℕ} [NeZero b] [NeZero N]def boxTimeCutoff (Q : RationalBox 5) : ℕ :=  letI := neZeroFive  ⌈Q.upper 1+1⌉₊def boxSpaceCutoff (Q : RationalBox 5) : ℕ :=  letI := neZeroFive  ⌈|Q.lower 2|+|Q.upper 2|+|Q.lower 3|+|Q.upper 3|+2⌉₊def runBoundTrial (d : Domain) (B : ℕ) (M : TM0.Machine (Fin b) (Fin N))    (w : List (Fin b)) (i : Fin 3) (is : List (Fin 5)) (Q : RationalBox 5) (k : ℕ) : Option ℚ :=  Q.boundTrial (force d B (boxSpaceCutoff Q) (boxTimeCutoff Q) M w i) is kend VelocityDetection.Effective.MachineRecipeendnoncomputable sectionnamespace VelocityDetection.Effective.MachineRecipeopen Turingstructure Program (b N : ℕ) [NeZero b] [NeZero N] where  derivativeBound : ℕ  table : TM0.Machine (Fin b) (Fin N)  input : List (Fin b)def compile {b N : ℕ} [NeZero b] [NeZero N] (B : ℕ) (M : TM0.Machine (Fin b) (Fin N)) (w : List (Fin b)) :    Program b N := ⟨B,M,w⟩end VelocityDetection.Effective.MachineRecipeendnoncomputable sectionnamespace VelocityDetection.Effective.MachineRecipe.Programopen Turingvariable {b N : ℕ} [NeZero b] [NeZero N]def valueTrial (P : Program b N) (d : Domain) (i : Fin 3) (is : List (Fin 5))    (q : Fin 5 → ℕ → ℚ) (ε : ℚ) (k : ℕ) : Option ℚ :=  runTrial d P.derivativeBound P.table P.input i is q ε kdef boundTrial (P : Program b N) (d : Domain) (i : Fin 3) (is : List (Fin 5))    (Q : RationalBox 5) (k : ℕ) : Option ℚ :=  runBoundTrial d P.derivativeBound P.table P.input i is Q knoncomputable def evaluate (P : Program b N) (d : Domain) (i : Fin 3) (is : List (Fin 5))    (q : Fin 5 → ℕ → ℚ) (ε : ℚ) : Part ℚ := Nat.rfindOpt (P.valueTrial d i is q ε)noncomputable def derivativeBounds (P : Program b N) (d : Domain) (i : Fin 3)    (is : List (Fin 5)) (Q : RationalBox 5) : Part ℚ := Nat.rfindOpt (P.boundTrial d i is Q)def Represents (P : Program b N) (d : Domain) (F : ℝ → VectorField 3) : Prop :=  letI := neZeroFive  (∀ (i : Fin 3) (is : List (Fin 5)) (q : Fin 5 → ℕ → ℚ) (x : Fin 5 → ℝ),    Names q x → 0 < x 0 → ∀ ε : ℚ, 0 < ε →      (P.evaluate d i is q ε).Dom ∧      ∀ r ∈ P.evaluate d i is q ε,        |mixedD is (forceFunction F i) x-(r:ℝ)| ≤ (ε:ℝ)) ∧  (∀ (i : Fin 3) (is : List (Fin 5)) (Q : RationalBox 5), 0 < Q.lower 0 →    (P.derivativeBounds d i is Q).Dom ∧    ∀ C ∈ P.derivativeBounds d i is Q, 0 ≤ C ∧      ∀ x ∈ Q.carrier, |mixedD is (forceFunction F i) x| ≤ (C:ℝ))end VelocityDetection.Effective.MachineRecipe.Programendnoncomputable sectionnamespace VelocityDetection.Effectiveopen Turingdef ComputableReal (x : ℝ) : Prop :=  ∃ q : ℕ → ℚ, Computable q ∧ ∀ k, |x-(q k:ℝ)| ≤ (accuracy k:ℝ)end VelocityDetection.Effectiveendnoncomputable sectionnamespace VelocityDetectionopen Set Function MeasureTheory Turingopen scoped ContDiffopen Effective Effective.MachineRecipetheorem main_result :    ∃ B : ℕ, 0 < B ∧      (∀ s : ℝ, |deriv (deriv SmoothBump.profile) s| ≤ (B:ℝ)) ∧    ∀ (ν : ℝ), 0 < ν → ComputableReal ν →    ∀ (b N : ℕ) [NeZero b] [NeZero N]      (M : TM0.Machine (Fin b) (Fin N)) (w : List (Fin b)),    ∃ (Ftor Fcyl : ℝ → VectorField 3),      (compile B M w).Represents .torus Ftor ∧      (compile B M w).Represents .cylinder Fcyl ∧      (ContDiff ℝ ∞ (uncurry (Ftor ν)) ∧        (∀ t, FactorsThrough (Ftor ν t) PeriodicSpace.cover) ∧        (∃ K : Set (Coord 2), IsCompact K ∧ (∀ X ∈ K, ∀ i, X i ∈ Ioo (0:ℝ) 1) ∧          ∀ t X, PeriodicSpace.cover (horizontal X) ∉ PeriodicSpace.cover '' K → Ftor ν t X = 0) ∧        (∀ T d, ∃ C : ℝ, 0 ≤ C ∧ ∀ t ∈ Icc (0:ℝ) T, ∀ X,          ‖iteratedFDeriv ℝ d (uncurry (Ftor ν)) (t,X)‖ ≤ C) ∧        ∃ u : VectorField 3,          ContDiff ℝ ∞ (uncurry u) ∧ TorusClass.ComparisonClass u (fun _ _ => 0) ∧          NavierStokes ν u (fun _ _ => 0) (Ftor ν) ∧          (Observation.torusEvent u ↔ (TM0.eval M w).Dom) ∧          ∀ (v : VectorField 3) (p : ScalarField 3), TorusClass.ComparisonClass v p →            NavierStokes ν v p (Ftor ν) →            ∀ t ≥ 0, (∀ X, v t X = u t X) ∧ (∀ X, p t X = 0)) ∧      (ContDiff ℝ ∞ (uncurry (Fcyl ν)) ∧        UniformDerivatives.Bounded (fun _ : Unit => uncurry (Fcyl ν)) ∧        (∀ t X z, Fcyl ν t (update X 2 z) = Fcyl ν t X) ∧        (∀ T : ℝ, ∃ K : Set (Coord 2), IsCompact K ∧ ∀ t ∈ Icc (0:ℝ) T,          ∀ X : Coord 3, horizontal X ∉ K → Fcyl ν t X = 0) ∧        ∃ u : VectorField 3,          ContDiff ℝ ∞ (uncurry u) ∧          Cylinder.ComparisonClass (fun t x => u t (Cylinder.join x)) (fun _ _ => 0) ∧          NavierStokes ν u (fun _ _ => 0) (Fcyl ν) ∧          (∀ t ≥ 0, (∀ x, 0 ≤ u t (Cylinder.join x) 2) ∧            Integrable (fun x => u t (Cylinder.join x) 2) Cylinder.measure) ∧          (Observation.planeEvent u ↔ (TM0.eval M w).Dom) ∧          ∀ (v : VectorField 3) (p : ScalarField 3),            Cylinder.ComparisonClass (fun t x => v t (Cylinder.join x))              (fun t x => p t (Cylinder.join x)) →            NavierStokes ν v p (Fcyl ν) →            ∀ t ≥ 0, (∀ X, v t X = u t X) ∧ (∀ X, p t X = 0)) := by sorryend VelocityDetectionendend OAI

Every extracted statement of the accompanying papers

The statements the atlas extracted automatically from each accompanying paper’s TeX source, with links to the full sources.

Geometric Programs for Solenoidal Forcing

Theorem (Periodic initialization)

Fix a computable viscosity \nu>0. From a deterministic one-tape machine, with head moves in \{-1,0,1\}, and a finite input, one can effectively construct a smooth force on \mathbb T_1^3 such that:

(i)
The force is divergence free, has zero spatial mean, and is one-periodic from time zero. Equation (sv:NS) has a global smooth solution with pressure zero, unique in the stated classical class.
(ii)
The velocity is one-periodic, vanishes near every integer time, has zero instantaneous self-advection, and has uniformly bounded kinetic energy. Every mixed derivative of force and velocity is globally bounded.
(iii)
For the fixed label a_*=(1/4,1/2,1/4) and fixed open strip O=\{1/2<x_1<7/8\}, the material trajectory enters O at a finite real time exactly when the machine halts, including an initially halted machine.

The construction may use one Cartesian velocity component at a time. For arbitrary fixed real \nu>0 the same formulas hold and are effective relative to that viscosity.

Section 1, The geometry of a finite fluid instruction Read it in the paper TeX source, line 43

Show the TeX

Fix a computable viscosity $\nu>0$.  From a deterministic one-tape
machine, with head moves in $\{-1,0,1\}$, and a finite input, one can
effectively construct a smooth force on $\mathbb T_1^3$ such that:
\begin{enumerate}[label=(\roman*),itemsep=2pt]
\item The force is divergence free, has zero spatial mean, and is
one-periodic from time zero.  Equation~\eqref{sv:NS} has a global
smooth solution with pressure zero, unique in the stated classical class.
\item The velocity is one-periodic, vanishes near every integer time,
has zero instantaneous self-advection, and has uniformly bounded kinetic
energy.  Every mixed derivative of force and velocity is globally bounded.
\item For the fixed label $a_*=(1/4,1/2,1/4)$ and fixed open strip
$O=\{1/2<x_1<7/8\}$, the material trajectory enters $O$ at a finite
real time exactly when the machine halts, including an initially halted
machine.
\end{enumerate}
The construction may use one Cartesian velocity component at a time.
For arbitrary fixed real $\nu>0$ the same formulas hold and are
effective relative to that viscosity.

Theorem (General diagonal maps on a sheet)

Let P_i,Q_i\subset[2,3]^2, 1\le i\le N, be closed rectangles with rational vertices and positive side lengths. Suppose the sources are pairwise positively separated and the targets are pairwise positively separated. Let F_i:P_i\to Q_i be the center-to-center affine map with any positive rational diagonal linear part, with F_i(P_i)=Q_i. For each computable \nu>0 there is an effective smooth mean-zero solenoidal force on \mathbb T_{10}^3, one-periodic from time zero, whose unique solution in the classical class has pressure zero and period map

(y,2)\longmapsto(F_i(y),2)\qquad(y\in P_i).

Its velocity is zero near integer times and has zero self-advection; all mixed derivatives of force and velocity are bounded. No condition is imposed on source–target intersections. For N=0 use zero.

Section 1, The geometry of a finite fluid instruction Read it in the paper TeX source, line 75

Show the TeX

Let $P_i,Q_i\subset[2,3]^2$, $1\le i\le N$, be closed rectangles
with rational vertices and positive side lengths.  Suppose the sources are pairwise
positively separated and the targets are pairwise positively separated.
Let $F_i:P_i\to Q_i$ be the center-to-center affine map with any
positive rational diagonal linear part, with $F_i(P_i)=Q_i$.  For each computable $\nu>0$
there is an effective smooth mean-zero solenoidal force on
$\mathbb T_{10}^3$, one-periodic from time zero, whose unique solution
in the classical class has pressure zero and period map
\[
 (y,2)\longmapsto(F_i(y),2)\qquad(y\in P_i).
\]
Its velocity is zero near integer times and has zero self-advection;
all mixed derivatives of force and velocity are bounded.  No condition
is imposed on source--target intersections.  For $N=0$ use zero.

Computation under Rapidly Vanishing Navier–Stokes Forcing

Theorem (Compact support and rapid decay)

Fix a positive computable viscosity \nu. From a deterministic Turing machine M and a finite input w one can effectively construct a smooth force on [0,\infty)\times\R^3, supported for all times in the fixed compact set

K=[-2,1]\times[-1,2]\times[-1,1],

such that, for every pair of nonnegative integers J,l and spatial multi-index \alpha,

\sup_{t\geq0,\,x\in\R^3} (1+t)^J\bigl|\partial_t^l\partial_x^\alpha f(t,x)\bigr|<\infty.

The Navier–Stokes equation with this force and zero initial velocity has an explicit global smooth solution, unique in the finite-interval class (eq:energy-class). Its material trajectory from the origin satisfies

M\text{ halts on }w \quad\Longleftrightarrow\quad X_1(t,0)<-1\text{ for some }t\geq0.

The velocity has the same fixed support and rapid mixed-derivative bounds. The pressure is zero. The force is a general body force. Because K is fixed, the same bounds hold with (1+t+|x|)^J in place of (1+t)^J.

Section 3, Addressed compact curls Read it in the paper TeX source, line 11

Show the TeX

Fix a positive computable viscosity $\nu$. From a deterministic Turing machine $M$ and a
finite input $w$ one can effectively construct a smooth force on
$[0,\infty)\times\R^3$, supported for all times in the fixed compact set
\[
 K=[-2,1]\times[-1,2]\times[-1,1],
\]
such that, for every pair of nonnegative integers $J,l$ and spatial
multi-index $\alpha$,
\begin{equation}
 \sup_{t\geq0,\,x\in\R^3}
 (1+t)^J\bigl|\partial_t^l\partial_x^\alpha f(t,x)\bigr|<\infty.
 
\end{equation}
The Navier--Stokes equation with this force and zero initial velocity has
an explicit global smooth solution, unique in the finite-interval class \eqref{eq:energy-class}.  Its material trajectory from
the origin satisfies
\begin{equation}
 M\text{ halts on }w
 \quad\Longleftrightarrow\quad
 X_1(t,0)<-1\text{ for some }t\geq0.
 
\end{equation}
The velocity has the same fixed support and rapid mixed-derivative bounds.
The pressure is zero. The force is a general body force. Because $K$ is fixed,
the same bounds hold with $(1+t+|x|)^J$ in place of $(1+t)^J$.

Theorem (Rapid decay with alternating memories)

Fix a positive computable viscosity. From a deterministic Turing machine and a finite input one can effectively construct a smooth force f on [0,\infty)\times\mathbb R^3, with spatial support contained in a fixed compact set independent of time, such that for every J,l\geq0 and spatial multi-index \alpha,

\sup_{t\geq0,\,X\in\mathbb R^3} (1+t+|X|)^J |\partial_t^l\partial_X^\alpha f(t,X)|<\infty.

The solution with zero initial velocity is explicit, global, and unique in the class (eq:energy-class), with pressure zero. Its velocity satisfies the same support and derivative estimates. The material particle initially at (-1,0,0) reaches X_1>0 if and only if the machine halts.

Section 4, Alternating fractional memories Read it in the paper TeX source, line 11

Show the TeX

Fix a positive computable viscosity. From a deterministic Turing machine
and a finite input one can effectively
construct a smooth force $f$ on $[0,\infty)\times\mathbb R^3$, with
spatial support contained in a fixed compact set independent of time,
such that for every $J,l\geq0$ and spatial multi-index $\alpha$,
\begin{equation}
 \sup_{t\geq0,\,X\in\mathbb R^3}
 (1+t+|X|)^J
 |\partial_t^l\partial_X^\alpha f(t,X)|<\infty.
 
\end{equation}
The solution with zero initial velocity is explicit, global, and unique
in the class \eqref{eq:energy-class}, with pressure zero.  Its velocity satisfies
the same support and derivative estimates.  The material particle
initially at $(-1,0,0)$ reaches $X_1>0$ if and only if the machine halts.

Theorem (Periodic lattice memory)

Fix a computable viscosity \nu>0. A finite deterministic machine and a finite input effectively determine a smooth force g on the unit flat torus \T^3=(\R/\mathbb Z)^3 with zero spatial mean. The Navier–Stokes equations with force g and zero initial velocity have a smooth solution (U,0) with zero spatial mean. Its particle from

a_*=(1/4,1/2,1/2)

enters the fixed open set

O=\{x\in\T^3:1/2<x_1<1\pmod 1\}

at some finite time if and only if the machine halts on that input. For every pair of nonnegative integers r,J and every spatial multi-index \alpha, there is an effective constant C_{r,\alpha,J} such that

\|\partial_t^r\partial_x^\alpha U(t)\|_\infty +\|\partial_t^r\partial_x^\alpha g(t)\|_\infty \le C_{r,\alpha,J}(1+t)^{-J},\qquad t\ge0.

There is also an effective smooth mean-zero solenoidal force f with the same bounds and exactly the same velocity and material event. It is f=g-\nabla\phi, with pressure -\phi, where \phi is the mean-zero periodic solution of \Delta\phi=\operatorname{div}g.

For either force, uniqueness holds among periodic classical solutions for which the velocity, its time derivative and its spatial derivatives through order two, and the pressure and its spatial gradient, are continuous on every [0,T]\times\T^3. Pressure is normalized to have zero spatial mean.

Section 5, Periodic lattice memory on the torus Read it in the paper TeX source, line 18

Show the TeX

Fix a computable viscosity $\nu>0$.  A finite deterministic machine and
a finite input effectively determine a smooth force $g$ on the unit
flat torus $\T^3=(\R/\mathbb Z)^3$ with zero spatial mean.  The
Navier--Stokes equations with force $g$ and zero initial velocity have
a smooth solution $(U,0)$ with zero spatial mean.  Its particle from
\[
 a_*=(1/4,1/2,1/2)
\]
enters the fixed open set
\[
 O=\{x\in\T^3:1/2<x_1<1\pmod 1\}
\]
at some finite time if and only if the machine halts on that input.
For every pair of nonnegative integers $r,J$ and every spatial
multi-index $\alpha$, there is an effective constant $C_{r,\alpha,J}$
such that
\begin{equation}
 \|\partial_t^r\partial_x^\alpha U(t)\|_\infty
 +\|\partial_t^r\partial_x^\alpha g(t)\|_\infty
 \le C_{r,\alpha,J}(1+t)^{-J},\qquad t\ge0.
\end{equation}
There is also an effective smooth mean-zero solenoidal force $f$
with the same bounds and exactly the same velocity and material event.
It is $f=g-\nabla\phi$, with pressure $-\phi$, where $\phi$ is the
mean-zero periodic solution of $\Delta\phi=\operatorname{div}g$.

For either force, uniqueness holds among periodic classical solutions
for which the velocity, its time derivative and its spatial derivatives
through order two, and the pressure and its spatial gradient, are
continuous on every $[0,T]\times\T^3$.  Pressure is normalized to have
zero spatial mean.

Velocity-Field Detection of Computation in Forced Navier–Stokes Flows

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.

Section 1, Observing the velocity rather than a particle Read it in the paper TeX source, line 98

Show the TeX

For each positive computable $\nu$, a machine and a finite input
effectively determine each of the following two forces.
\begin{enumerate}
\item On $\T^3$, a smooth force has a unique global smooth solution
in the torus class above, with pressure zero, for which
\eqref{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.
\item 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
\eqref{eq:comparison-class}, with pressure zero and integrable
nonnegative third component. Event~\eqref{eq:plane-event} holds exactly
when the machine halts.
\end{enumerate}
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.

Incompressible Box Transport and Finite Computation

The atlas found no headline statement in this paper’s TeX source.

Configuration and file facts

File: lean/ComparatorChallenges/NavierStokesVelocity.lean
OpenAI’s Lean catalogue: OpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 376 link it.
Solution module: OAI.MathematicalPhysics.NavierStokes.VelocityDetection.Main
Allowed axioms: propext, Quot.sound, Classical.choiceThe axioms this configuration allows a proof to use. A replay shows which of them a proof uses.
Imports: Mathlib
Imports from outside Mathlib: None
Local vocabulary: 196 local vocabulary declarations
Lines of Lean, without comments or blank lines: 607
Second proof-verification program (nanoda): Off in OpenAI's configuration.

A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.

Plectis Atlas