NavierStokes.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

20 declarations, 4 contain sorry, 0 declared as axioms

Existence And Smoothness Of The Navier–Stokes Equation

This file formalizes the Clay Mathematics Institute millennium problem concerning the existence and smoothness of solutions to the Navier-Stokes equations in three spatial dimensions. While the definitions are generalized to arbitrary dimension n, the millennium problem specifically concerns the case n = 3.

References

Main Theorems (Clay Millennium Problem for n = 3)

The Clay Millennium Problem asks for a proof of one of the following four statements:

navier_stokes_existence_and_smoothness_R3: (A) Global existence on ℝ³
navier_stokes_existence_and_smoothness_periodic: (B) Global existence on ℝ³/ℤ³
navier_stokes_breakdown_R3: (C) Existence of breakdown scenario on ℝ³
navier_stokes_breakdown_periodic: (D) Existence of breakdown scenario on ℝ³/ℤ³

In September 2026, an internal OpenAI model proved alternatives (C) and (D) by constructing solutions that develop finite-time singularities under smooth forcing.

Variable conventions

Fefferman writes the velocity as $u(x,t)$, the initial velocity as $u^\circ(x)$, the pressure as $p(x,t)$, the force as $f(x,t)$, and the viscosity as $\nu$. In Lean, u₀ : ℝ^n → ℝ^n denotes the initial velocity, while v : ℝ^n → ℝ → ℝ^n denotes the solution velocity. The curried order v x t, p x t, and f x t keeps the source convention that position comes before time.

Since the Clay statement gives equation (1) on the closed time half-line $t \ge 0$, the time derivative is encoded with derivWithin relative to Set.Ici 0. The Clay PDF also includes errata; in particular, we include spatial 1-periodicity of the pressure in the periodic case. The sign correction to the weak-solution identity in the errata is not represented here, since this file formalizes the four prize alternatives rather than the later weak-solution discussion.

Imports (1)

FormalConjecturesUtil

def NavierStokes.divergence line 80 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, EuclideanSpace, Real, Fin
Proof uses: LinearMap, RingHom.id, OfNat.ofNat, ENNReal, LinearMap.trace, fderiv
35 instances, coercions and auxiliary constants left out.
theorem NavierStokes.divergence_of_not_differentiableAt The divergence of a vector field is $0$ at points where fderiv has its junk value line 87 source
Source documentation
The divergence of a vector field is $0$ at points where fderiv has its junk value.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, EuclideanSpace, Real, Fin, Not, DifferentiableAt, OfNat.ofNat, ENNReal, Eq, NavierStokes.divergence
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, LinearMap, RingHom.id, LinearMap.trace, fderiv, ContinuousLinearMap, fderiv_zero_of_not_differentiableAt, map_zero, RingHom, eq_self
77 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem divergence_of_not_differentiableAt {v : ℝ^n → ℝ^n} {x : ℝ^n}
    (hv : ¬ DifferentiableAt ℝ v x) : ∇⬝ v x = 0 := by
…
```
theorem NavierStokes.divergence_zero The divergence of the zero vector field is zero line 93 source
Source documentation
The divergence of the zero vector field is zero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, EuclideanSpace, Real, Fin, Eq, NavierStokes.divergence, OfNat.ofNat, ENNReal
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, LinearMap, RingHom.id, LinearMap.trace, fderiv, ContinuousLinearMap, congrFun, fderiv_zero, map_zero, RingHom, eq_self
72 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem divergence_zero (x : ℝ^n) : ∇⬝ (0 : ℝ^n → ℝ^n) x = 0 := by
…
```
theorem NavierStokes.divergence_const The divergence of a constant vector field is zero line 98 source
Source documentation
The divergence of a constant vector field is zero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, EuclideanSpace, Real, Fin, Eq, NavierStokes.divergence, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, LinearMap, RingHom.id, ENNReal, LinearMap.trace, fderiv, ContinuousLinearMap, congrFun, fderiv_fun_const, map_zero, RingHom, eq_self
53 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem divergence_const (c : ℝ^n) (x : ℝ^n) :
    ∇⬝ (fun _ : ℝ^n => c) x = 0 := by
…
```
Mentions: c
theorem NavierStokes.divergence_add Divergence is additive at points where both vector fields are differentiable line 104 source
Source documentation
Divergence is additive at points where both vector fields are differentiable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, EuclideanSpace, Real, Fin, DifferentiableAt, OfNat.ofNat, ENNReal, Eq, NavierStokes.divergence, HAdd.hAdd
Proof uses: Eq.mpr, LinearMap, RingHom.id, LinearMap.trace, fderiv, id, congrArg, NavierStokes.divergence.eq_1, ContinuousLinearMap, fderiv_fun_add, map_add
95 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem divergence_add {v w : ℝ^n → ℝ^n} {x : ℝ^n}
    (hv : DifferentiableAt ℝ v x) (hw : DifferentiableAt ℝ w x) :
    ∇⬝ (fun y => v y + w y) x = ∇⬝ v x + ∇⬝ w x := by
…
```
theorem NavierStokes.divergence_smul Divergence commutes with scalar multiplication at differentiability points line 112 source
Source documentation
Divergence commutes with scalar multiplication at differentiability points.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, EuclideanSpace, Fin, DifferentiableAt, OfNat.ofNat, ENNReal, Eq, NavierStokes.divergence, HSMul.hSMul, HMul.hMul
Proof uses: Eq.mpr, LinearMap, RingHom.id, LinearMap.trace, fderiv, id, congrArg, NavierStokes.divergence.eq_1, ContinuousLinearMap, fderiv_fun_const_smul, of_eq_true, Eq.trans, True, congrFun', map_smul, eq_self
133 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem divergence_smul (c : ℝ) {v : ℝ^n → ℝ^n} {x : ℝ^n}
    (hv : DifferentiableAt ℝ v x) : ∇⬝ (fun y => c • v y) x = c * ∇⬝ v x := by
…
```
Mentions: c
def NavierStokes.IsOnePeriodic A function $f : \mathbb{R}^n \to \alpha$ is 1-periodic if it is periodic in each coordinate with period $1$, i.e. $f(x + e_i) = f(x)$ for each unit vector $e_i$ line 122 source
Source documentation
A function $f : \mathbb{R}^n \to \alpha$ is 1-periodic if it is periodic in each coordinate with period $1$, i.e. $f(x + e_i) = f(x)$ for each unit vector $e_i$. This captures functions on the $n$-torus $\mathbb{R}^n/\mathbb{Z}^n$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, EuclideanSpace, Real, Fin
Proof uses: Eq, HAdd.hAdd, OfNat.ofNat, ENNReal, EuclideanSpace.single
17 instances, coercions and auxiliary constants left out.
```
def IsOnePeriodic {α : Sort*} (f : ℝ^n → α) : Prop :=
…
```
structure NavierStokes.InitialVelocityCondition Basic conditions on initial velocity field for the Navier-Stokes equations in $n$-dimensional space line 135 source
Source documentation
Basic conditions on initial velocity field for the Navier-Stokes equations in $n$-dimensional space.
The initial velocity must be:
- Divergence-free (incompressibility condition: $\nabla \cdot u_0 = 0$)
- Smooth ($C^\infty$)
These conditions apply regardless of spatial dimension.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, EuclideanSpace, Real, Fin
```
structure InitialVelocityCondition (u₀ : ℝ^n → ℝ^n) : Prop where
…
```
structure NavierStokes.InitialVelocityConditionDecay Initial velocity conditions for the Navier-Stokes problem on all of $\mathbb{R}^n$ line 151 source
Source documentation
Initial velocity conditions for the Navier-Stokes problem on all of $\mathbb{R}^n$.
In addition to being smooth and divergence-free, the velocity must decay faster than any polynomial at spatial infinity (condition 4 in Fefferman's paper).
This condition ensures the velocity field has finite energy and reasonable behavior as $\lVert x \rVert \to \infty$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, EuclideanSpace, Real, Fin
```
structure InitialVelocityConditionDecay (u₀ : ℝ^n → ℝ^n) : Prop extends
    InitialVelocityCondition u₀ where
…
```
Mentions: NavierStokes.InitialVelocityCondition
structure NavierStokes.InitialVelocityConditionPeriodic Initial velocity conditions for the periodic Navier-Stokes problem on $\mathbb{R}^n/\mathbb{Z}^n$ line 165 source
Source documentation
Initial velocity conditions for the periodic Navier-Stokes problem on $\mathbb{R}^n/\mathbb{Z}^n$.
The velocity must be smooth, divergence-free, and 1-periodic in each coordinate (condition 8, part 1 in Fefferman's paper).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, EuclideanSpace, Real, Fin
```
structure InitialVelocityConditionPeriodic (u₀ : ℝ^n → ℝ^n) : Prop extends
    InitialVelocityCondition u₀ where
…
```
Mentions: NavierStokes.InitialVelocityCondition
structure NavierStokes.ForceCondition The basic smoothness condition on the external forcing term line 176 source
Source documentation
The basic smoothness condition on the external forcing term.
The force $f(x,t)$ must be smooth ($C^\infty$) in both space and time variables for $t \ge 0$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, EuclideanSpace, Real, Fin
```
structure ForceCondition (f : ℝ^n → ℝ → ℝ^n) : Prop where
…
```
structure NavierStokes.ForceConditionDecay Force conditions for the Navier-Stokes problem on all of $\mathbb{R}^n$ line 186 source
Source documentation
Force conditions for the Navier-Stokes problem on all of $\mathbb{R}^n$.
The force must be smooth and decay faster than any polynomial in both space and time (condition 5 in Fefferman's paper).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, EuclideanSpace, Real, Fin
```
structure ForceConditionDecay (f : ℝ^n → ℝ → ℝ^n) : Prop extends ForceCondition f where
…
```
Mentions: NavierStokes.ForceCondition
structure NavierStokes.ForceConditionPeriodic Force conditions for the periodic Navier-Stokes problem on $\mathbb{R}^n/\mathbb{Z}^n$ line 201 source
Source documentation
Force conditions for the periodic Navier-Stokes problem on $\mathbb{R}^n/\mathbb{Z}^n$.
The force must be smooth, 1-periodic in space, and decay in time (conditions 8, part 1 and 9 in Fefferman's paper).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, EuclideanSpace, Real, Fin
```
structure ForceConditionPeriodic (f : ℝ^n → ℝ → ℝ^n) : Prop extends ForceCondition f where
…
```
Mentions: NavierStokes.ForceCondition
structure NavierStokes.NavierStokesExistenceAndSmoothness A solution (v, p) to the Navier-Stokes equations in n-dimensional space with viscosity $\nu$, initial velocity $u_0$, and external force $f$ line 218 source
Source documentation
A solution (v, p) to the Navier-Stokes equations in n-dimensional space with viscosity $\nu$, initial velocity $u_0$, and external force $f$.
This structure captures the core requirements for a solution:
1. The velocity and pressure satisfy the Navier-Stokes PDE (equation 1)
2. The velocity remains divergence-free for all time (equation 2)
3. The initial condition is satisfied (equation 3)
4. The solution is smooth ($C^\infty$) for all time $t \ge 0$ (equations 6, 11)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, EuclideanSpace, Fin
```
structure NavierStokesExistenceAndSmoothness
    (nu : ℝ) (u₀ : ℝ^n → ℝ^n) (f : ℝ^n → ℝ → ℝ^n)
    (v : ℝ^n → ℝ → ℝ^n) (p : ℝ^n → ℝ → ℝ) : Prop where
…
```
structure NavierStokes.NavierStokesExistenceAndSmoothnessRn A solution to the Navier-Stokes equations on all of $\mathbb{R}^n$ with appropriate decay and energy bounds line 246 source
Source documentation
A solution to the Navier-Stokes equations on all of $\mathbb{R}^n$ with appropriate decay and energy bounds.
In addition to the basic solution properties, we require:
- The velocity is in $L^2$ at each time $t \ge 0$ (finite kinetic energy)
- The total energy remains bounded for all time (condition 7)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, EuclideanSpace, Fin
```
structure NavierStokesExistenceAndSmoothnessRn
    (nu : ℝ) (u₀ : ℝ^n → ℝ^n) (f : ℝ^n → ℝ → ℝ^n)
    (v : ℝ^n → ℝ → ℝ^n) (p : ℝ^n → ℝ → ℝ) : Prop
  extends NavierStokesExistenceAndSmoothness nu u₀ f v p where
…
```
Mentions: NavierStokes.NavierStokesExistenceAndSmoothness
structure NavierStokes.NavierStokesExistenceAndSmoothnessPeriodic A solution to the Navier-Stokes equations on the $n$-torus $\mathbb{R}^n/\mathbb{Z}^n$ line 263 source
Source documentation
A solution to the Navier-Stokes equations on the $n$-torus $\mathbb{R}^n/\mathbb{Z}^n$.
The velocity must be 1-periodic in each spatial direction for all times (condition 10). The pressure is also required to be 1-periodic, following the errata appended to the Clay problem statement.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, EuclideanSpace, Fin
```
structure NavierStokesExistenceAndSmoothnessPeriodic
    (nu : ℝ) (u₀ : ℝ^n → ℝ^n) (f : ℝ^n → ℝ → ℝ^n)
    (v : ℝ^n → ℝ → ℝ^n) (p : ℝ^n → ℝ → ℝ) : Prop
  extends NavierStokesExistenceAndSmoothness nu u₀ f v p where
…
```
Mentions: NavierStokes.NavierStokesExistenceAndSmoothness
theorem NavierStokes.navier_stokes_existence_and_smoothness_R3 (A) Existence and smoothness of (unforced) Navier–Stokes solutions on ℝ³ sorry line 274 source
Source documentation
(A) Existence and smoothness of (unforced) Navier–Stokes solutions on ℝ³.

depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, EuclideanSpace, Fin, Nat, NavierStokes.InitialVelocityConditionDecay, Exists, NavierStokes.NavierStokesExistenceAndSmoothnessRn, ENNReal
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem navier_stokes_existence_and_smoothness_R3 (nu : ℝ) (hnu : nu > 0)
    (u₀ : ℝ³ → ℝ³) (hu₀ : InitialVelocityConditionDecay u₀) :
    ∃ v p, NavierStokesExistenceAndSmoothnessRn nu u₀ (f := 0) v p := by
…
```
Mentions: NavierStokes.InitialVelocityConditionDecay, NavierStokes.NavierStokesExistenceAndSmoothnessRn
theorem NavierStokes.navier_stokes_existence_and_smoothness_periodic (B) Existence and smoothness of (unforced) Navier–Stokes solutions in ℝ³/ℤ³ sorry line 281 source
Source documentation
(B) Existence and smoothness of (unforced) Navier–Stokes solutions in ℝ³/ℤ³.

depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, EuclideanSpace, Fin, Nat, NavierStokes.InitialVelocityConditionPeriodic, Exists, NavierStokes.NavierStokesExistenceAndSmoothnessPeriodic, ENNReal
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem navier_stokes_existence_and_smoothness_periodic (nu : ℝ) (hnu : nu > 0)
    (u₀ : ℝ³ → ℝ³) (hu₀ : InitialVelocityConditionPeriodic u₀) :
    ∃ v p, NavierStokesExistenceAndSmoothnessPeriodic nu u₀ (f := 0) v p := by
…
```
Mentions: NavierStokes.InitialVelocityConditionPeriodic, NavierStokes.NavierStokesExistenceAndSmoothnessPeriodic
theorem NavierStokes.navier_stokes_breakdown_R3 sorry line 294 source
depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Exists, EuclideanSpace, Fin, Nat, And, NavierStokes.InitialVelocityConditionDecay, NavierStokes.ForceConditionDecay, Not, NavierStokes.NavierStokesExistenceAndSmoothnessRn
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem NavierStokes.navier_stokes_breakdown_periodic sorry line 308 source
depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Exists, EuclideanSpace, Fin, Nat, And, NavierStokes.InitialVelocityConditionPeriodic, NavierStokes.ForceConditionPeriodic, Not, NavierStokes.NavierStokesExistenceAndSmoothnessPeriodic
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.