Classical uniqueness for periodic Navier--Stokes fields

The differential operators are those of ProblemStatement. The energy estimate is derived from the equations and periodic integration by parts.

noncomputable def NavierStokes.PeriodicUniqueness.slab (a b : ℝ) : Set ProblemStatement.SpaceTime

Slab, given by Icc a b ×ˢ univ.

Equations

• NavierStokes.PeriodicUniqueness.slab a b = Set.Icc a b ×ˢ Set.univ

theorem NavierStokes.PeriodicUniqueness.spatial_smooth {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {a b t : ℝ} {u : ProblemStatement.SpaceTime → V} (hu : ContDiffOn ℝ (↑⊤) u (slab a b)) (ht : t ∈ Set.Icc a b) : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => u (t, x)

theorem NavierStokes.PeriodicUniqueness.smooth_at_interior {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {a b t : ℝ} {u : ProblemStatement.SpaceTime → V} (hu : ContDiffOn ℝ (↑⊤) u (slab a b)) (ht : t ∈ Set.Ioo a b) (x : ProblemStatement.Space) : ContDiffAt ℝ (↑⊤) u (t, x)

theorem NavierStokes.PeriodicUniqueness.spatialDerivative_sub {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => v (t, x)) (x : ProblemStatement.Space) : ProblemStatement.spatialDerivative (u - v) t x = ProblemStatement.spatialDerivative u t x - ProblemStatement.spatialDerivative v t x

theorem NavierStokes.PeriodicUniqueness.spatialDivergence_sub {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => v (t, x)) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence (u - v) t x = ProblemStatement.spatialDivergence u t x - ProblemStatement.spatialDivergence v t x

theorem NavierStokes.PeriodicUniqueness.advection_difference {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => v (t, x)) (x : ProblemStatement.Space) : ProblemStatement.advection u t x - ProblemStatement.advection v t x = (ProblemStatement.spatialDerivative u t x) ((u - v) (t, x)) + (ProblemStatement.spatialDerivative (u - v) t x) (v (t, x))

theorem NavierStokes.PeriodicUniqueness.spatialLaplacian_sub {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => v (t, x)) (x : ProblemStatement.Space) : ProblemStatement.spatialLaplacian (u - v) t x = ProblemStatement.spatialLaplacian u t x - ProblemStatement.spatialLaplacian v t x

theorem NavierStokes.PeriodicUniqueness.pressureGradient_sub {p q : ProblemStatement.PressureField} {t : ℝ} (hp : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => p (t, x)) (hq : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => q (t, x)) (x : ProblemStatement.Space) : ProblemStatement.pressureGradient (p - q) t x = ProblemStatement.pressureGradient p t x - ProblemStatement.pressureGradient q t x

theorem NavierStokes.PeriodicUniqueness.temporalDerivative_sub {u v : ProblemStatement.VelocityField} {t : ℝ} {x : ProblemStatement.Space} (hu : DifferentiableAt ℝ (fun (s : ℝ) => u (s, x)) t) (hv : DifferentiableAt ℝ (fun (s : ℝ) => v (s, x)) t) : ProblemStatement.temporalDerivative (u - v) t x = ProblemStatement.temporalDerivative u t x - ProblemStatement.temporalDerivative v t x

theorem NavierStokes.PeriodicUniqueness.difference_equation {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} {t : ℝ} {x : ProblemStatement.Space} (hu : ContDiff ℝ ↑⊤ fun (y : ProblemStatement.Space) => u (t, y)) (hv : ContDiff ℝ ↑⊤ fun (y : ProblemStatement.Space) => v (t, y)) (hp : ContDiff ℝ ↑⊤ fun (y : ProblemStatement.Space) => p (t, y)) (hq : ContDiff ℝ ↑⊤ fun (y : ProblemStatement.Space) => q (t, y)) (htu : DifferentiableAt ℝ (fun (s : ℝ) => u (s, x)) t) (htv : DifferentiableAt ℝ (fun (s : ℝ) => v (s, x)) t) (hNS : ProblemStatement.navierStokesResidual u p t x = ProblemStatement.navierStokesResidual v q t x) : ProblemStatement.temporalDerivative (u - v) t x = ProblemStatement.spatialLaplacian (u - v) t x - (ProblemStatement.spatialDerivative u t x) ((u - v) (t, x)) - (ProblemStatement.spatialDerivative (u - v) t x) (v (t, x)) - ProblemStatement.pressureGradient (p - q) t x

Subtract the actual Navier--Stokes residuals, retaining the favorable transport decomposition Du(w) + Dw(v).

theorem NavierStokes.PeriodicUniqueness.nonlinear_energy_bound (A : ProblemStatement.Space →L[ℝ] ProblemStatement.Space) (w : ProblemStatement.Space) {B : ℝ} (hB : ‖A‖ ≤ B) : -inner ℝ w (A w) ≤ B * ‖w‖ ^ 2

The only indefinite energy term is controlled by the operator norm of the first velocity gradient.

theorem NavierStokes.PeriodicUniqueness.gronwall_zero {a b K : ℝ} {E E' : ℝ → ℝ} (hab : a ≤ b) (hcont : ContinuousOn E (Set.Icc a b)) (hinitial : E a = 0) (hnonneg : ∀ t ∈ Set.Icc a b, 0 ≤ E t) (hderiv : ∀ t ∈ Set.Ioo a b, HasDerivAt E (E' t) t) (hbound : ∀ t ∈ Set.Ioo a b, E' t ≤ K * E t) (t : ℝ) : t ∈ Set.Icc a b → E t = 0

The zero-initial-data Gronwall conclusion, proved by the integrating factor and mean-value theorem. Only interior derivatives are required.

theorem NavierStokes.PeriodicUniqueness.spatialDerivative_eq_within_comp {a b t : ℝ} {u : ProblemStatement.VelocityField} (hu : ContDiffOn ℝ (↑⊤) u (slab a b)) (ht : t ∈ Set.Icc a b) (x : ProblemStatement.Space) : ProblemStatement.spatialDerivative u t x = fderivWithin ℝ u (slab a b) (t, x) ∘SL ContinuousLinearMap.inr ℝ ℝ ProblemStatement.Space

The ordinary spatial derivative at a time endpoint is the restriction of the joint within-derivative to spatial directions.

theorem NavierStokes.PeriodicUniqueness.exists_gradient_bound {a b : ℝ} (hab : a < b) {u : ProblemStatement.VelocityField} (hu : ContDiffOn ℝ (↑⊤) u (slab a b)) {K : Set ProblemStatement.Space} (hK : IsCompact K) : ∃ (B : ℝ), 0 < B ∧ ∀ t ∈ Set.Icc a b, ∀ x ∈ K, ‖ProblemStatement.spatialDerivative u t x‖ ≤ B

Compactness supplies the spatial-gradient bound used by the energy estimate; it is a conclusion from smoothness, not an input to uniqueness.

theorem NavierStokes.PeriodicUniqueness.sum_coordinates (x : ProblemStatement.Space) : ∑ i : Fin 3, x.ofLp i • ProblemStatement.coordinateVector i = x

Reconstruction in the standard Euclidean coordinate basis.

theorem NavierStokes.PeriodicUniqueness.periodic_lattice {W : Type u_1} {f : ProblemStatement.Space → W} (hf : ∀ (i : Fin 3), Function.Periodic f (ProblemStatement.coordinateVector i)) (n : Fin 3 → ℤ) : Function.Periodic f (∑ i : Fin 3, n i • ProblemStatement.coordinateVector i)

Unit coordinate periods imply invariance under every integer lattice translation; no quotient or fundamental-domain claim is assumed.

theorem NavierStokes.PeriodicUniqueness.exists_cube_representative {W : Type u_1} {f : ProblemStatement.Space → W} (hf : ∀ (i : Fin 3), Function.Periodic f (ProblemStatement.coordinateVector i)) (x : ProblemStatement.Space) : ∃ (y : ProblemStatement.Space), (∀ (i : Fin 3), y.ofLp i ∈ Set.Icc 0 1) ∧ f y = f x

Each point has a representative in the unit cube with the same value under every function having the three unit coordinate periods.

theorem NavierStokes.PeriodicUniqueness.periodic_fderiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.Space → V} (hp : ∀ (x : ProblemStatement.Space) (i : Fin 3), f (x + ProblemStatement.coordinateVector i) = f x) (x : ProblemStatement.Space) (i : Fin 3) : fderiv ℝ f (x + ProblemStatement.coordinateVector i) = fderiv ℝ f x

theorem NavierStokes.PeriodicUniqueness.spatial_partial_contDiff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.Space → V} (hf : ContDiff ℝ (↑⊤) f) (i : Fin 3) : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => (fderiv ℝ f x) (ProblemStatement.coordinateVector i)

theorem NavierStokes.PeriodicUniqueness.component_contDiff {f : ProblemStatement.Space → ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (j : Fin 3) : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => (f x).ofLp j

theorem NavierStokes.PeriodicUniqueness.fderiv_component {f : ProblemStatement.Space → ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (j : Fin 3) (x v : ProblemStatement.Space) : (fderiv ℝ (fun (y : ProblemStatement.Space) => (f y).ofLp j) x) v = ((fderiv ℝ f x) v).ofLp j

theorem NavierStokes.PeriodicUniqueness.fderiv_apply_eq_sum (f : ProblemStatement.Space → ℝ) (x v : ProblemStatement.Space) : (fderiv ℝ f x) v = ∑ i : Fin 3, v.ofLp i * (fderiv ℝ f x) (ProblemStatement.coordinateVector i)

theorem NavierStokes.PeriodicUniqueness.fderiv_normsq {f : ProblemStatement.Space → ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (x v : ProblemStatement.Space) : (fderiv ℝ (fun (y : ProblemStatement.Space) => ‖f y‖ ^ 2) x) v = 2 * inner ℝ (f x) ((fderiv ℝ f x) v)

theorem NavierStokes.PeriodicUniqueness.fderiv_inner {f g : ProblemStatement.Space → ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (x v : ProblemStatement.Space) : (fderiv ℝ (fun (y : ProblemStatement.Space) => inner ℝ (f y) (g y)) x) v = inner ℝ (f x) ((fderiv ℝ g x) v) + inner ℝ ((fderiv ℝ f x) v) (g x)

theorem NavierStokes.PeriodicUniqueness.inner_pressureGradient (p : ProblemStatement.PressureField) (t : ℝ) (x w : ProblemStatement.Space) : inner ℝ w (ProblemStatement.pressureGradient p t x) = (fderiv ℝ (fun (y : ProblemStatement.Space) => p (t, y)) x) w

The pressure term paired with a vector is its scalar directional derivative. This uses exactly the gradient definition in the target.

theorem NavierStokes.PeriodicUniqueness.energy_density_derivative {u : ProblemStatement.VelocityField} {t : ℝ} {x : ProblemStatement.Space} (hu : DifferentiableAt ℝ (fun (s : ℝ) => u (s, x)) t) : HasDerivAt (fun (s : ℝ) => ‖u (s, x)‖ ^ 2) (2 * inner ℝ (u (t, x)) (ProblemStatement.temporalDerivative u t x)) t

theorem NavierStokes.PeriodicUniqueness.component_periodic {f : ProblemStatement.Space → ProblemStatement.Space} (hf : PeriodicIntegration.UnitPeriods f) (j : Fin 3) : PeriodicIntegration.UnitPeriods fun (x : ProblemStatement.Space) => (f x).ofLp j

theorem NavierStokes.PeriodicUniqueness.spatial_partial_periodic {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.Space → V} (hf : PeriodicIntegration.UnitPeriods f) (i : Fin 3) : PeriodicIntegration.UnitPeriods (PeriodicIntegration.spatialPartial i f)

theorem NavierStokes.PeriodicUniqueness.normsq_periodic {f : ProblemStatement.Space → ProblemStatement.Space} (hf : PeriodicIntegration.UnitPeriods f) : PeriodicIntegration.UnitPeriods fun (x : ProblemStatement.Space) => ‖f x‖ ^ 2

theorem NavierStokes.PeriodicUniqueness.cubeIntegral_fderiv_apply {f : ProblemStatement.Space → ℝ} {v : ProblemStatement.Space → ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (hv : ContDiff ℝ (↑⊤) v) (hpf : PeriodicIntegration.UnitPeriods f) (hpv : PeriodicIntegration.UnitPeriods v) : (PeriodicIntegration.cubeIntegral fun (x : ProblemStatement.Space) => (fderiv ℝ f x) (v x)) = -PeriodicIntegration.cubeIntegral fun (x : ProblemStatement.Space) => f x * ∑ i : Fin 3, (PeriodicIntegration.spatialPartial i v x).ofLp i

Scalar transport integration by parts, derived from the three coordinate identities on the unit cube.

theorem NavierStokes.PeriodicUniqueness.cubeIntegral_fderiv_apply_zero {f : ProblemStatement.Space → ℝ} {v : ProblemStatement.Space → ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (hv : ContDiff ℝ (↑⊤) v) (hpf : PeriodicIntegration.UnitPeriods f) (hpv : PeriodicIntegration.UnitPeriods v) (hdiv : ∀ (x : ProblemStatement.Space), ∑ i : Fin 3, (PeriodicIntegration.spatialPartial i v x).ofLp i = 0) : (PeriodicIntegration.cubeIntegral fun (x : ProblemStatement.Space) => (fderiv ℝ f x) (v x)) = 0

theorem NavierStokes.PeriodicUniqueness.cubeIntegral_transport_energy_zero {w v : ProblemStatement.Space → ProblemStatement.Space} (hw : ContDiff ℝ (↑⊤) w) (hv : ContDiff ℝ (↑⊤) v) (hpw : PeriodicIntegration.UnitPeriods w) (hpv : PeriodicIntegration.UnitPeriods v) (hdiv : ∀ (x : ProblemStatement.Space), ∑ i : Fin 3, (PeriodicIntegration.spatialPartial i v x).ofLp i = 0) : (PeriodicIntegration.cubeIntegral fun (x : ProblemStatement.Space) => inner ℝ (w x) ((fderiv ℝ w x) (v x))) = 0

Divergence-free transport has zero contribution to the energy.

theorem NavierStokes.PeriodicUniqueness.cubeIntegral_inner_partial {f g : ProblemStatement.Space → ProblemStatement.Space} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hpf : PeriodicIntegration.UnitPeriods f) (hpg : PeriodicIntegration.UnitPeriods g) (i : Fin 3) : (PeriodicIntegration.cubeIntegral fun (x : ProblemStatement.Space) => inner ℝ (f x) (PeriodicIntegration.spatialPartial i g x)) = -PeriodicIntegration.cubeIntegral fun (x : ProblemStatement.Space) => inner ℝ (PeriodicIntegration.spatialPartial i f x) (g x)

Vector integration by parts follows from the scalar derivative of the Euclidean inner product; it is not assumed as an energy identity.

theorem NavierStokes.PeriodicUniqueness.cubeIntegral_laplacian_energy {w : ProblemStatement.VelocityField} {t : ℝ} (hw : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => w (t, x)) (hpw : PeriodicIntegration.UnitPeriods fun (x : ProblemStatement.Space) => w (t, x)) : (PeriodicIntegration.cubeIntegral fun (x : ProblemStatement.Space) => inner ℝ (w (t, x)) (ProblemStatement.spatialLaplacian w t x)) = -∑ i : Fin 3, PeriodicIntegration.cubeIntegral fun (x : ProblemStatement.Space) => ‖PeriodicIntegration.spatialPartial i (fun (y : ProblemStatement.Space) => w (t, y)) x‖ ^ 2

The viscosity term is minus the actual integrated sum of squared coordinate derivatives of the difference field.

theorem NavierStokes.PeriodicUniqueness.cubeIntegral_pressure_energy_zero {w : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {t : ℝ} (hw : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => w (t, x)) (hp : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => p (t, x)) (hpw : PeriodicIntegration.UnitPeriods fun (x : ProblemStatement.Space) => w (t, x)) (hpp : PeriodicIntegration.UnitPeriods fun (x : ProblemStatement.Space) => p (t, x)) (hdiv : ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence w t x = 0) : (PeriodicIntegration.cubeIntegral fun (x : ProblemStatement.Space) => inner ℝ (w (t, x)) (ProblemStatement.pressureGradient p t x)) = 0

Pressure has zero energy contribution when the difference velocity is divergence free.

theorem NavierStokes.PeriodicUniqueness.spatialLaplacian_contDiff {w : ProblemStatement.VelocityField} {t : ℝ} (hw : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => w (t, x)) : ContDiff ℝ (↑⊤) (ProblemStatement.spatialLaplacian w t)

theorem NavierStokes.PeriodicUniqueness.pressureGradient_contDiff {p : ProblemStatement.PressureField} {t : ℝ} (hp : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => p (t, x)) : ContDiff ℝ (↑⊤) (ProblemStatement.pressureGradient p t)

theorem NavierStokes.PeriodicUniqueness.unitPeriods_sub {V : Type u_1} [Sub V] {f g : ProblemStatement.Space → V} (hf : PeriodicIntegration.UnitPeriods f) (hg : PeriodicIntegration.UnitPeriods g) : PeriodicIntegration.UnitPeriods (f - g)

noncomputable def NavierStokes.PeriodicUniqueness.energy (u v : ProblemStatement.VelocityField) (t : ℝ) : ℝ

Squared L² distance, using the actual unit-cube Lebesgue integral.

Equations

• NavierStokes.PeriodicUniqueness.energy u v t = NavierStokes.PeriodicIntegration.cubeIntegral fun (x : NavierStokes.ProblemStatement.Space) => ‖(u - v) (t, x)‖ ^ 2

noncomputable def NavierStokes.PeriodicUniqueness.energyRate (u v : ProblemStatement.VelocityField) (t : ℝ) : ℝ

Energy rate, given by cubeIntegral (fun x => 2 * ⟪(u - v) (t, x), temporalDerivative (u - v) t x⟫_ℝ).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.PeriodicUniqueness.dissipation (w : ProblemStatement.VelocityField) (t : ℝ) : ℝ

Dissipation, given by ∑ i : Fin 3, cubeIntegral (fun x => ‖spatialPartial i (fun y => w (t, y)) x‖ ^ 2).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.PeriodicUniqueness.coupling (u w : ProblemStatement.VelocityField) (t : ℝ) : ℝ

Coupling, given by cubeIntegral (fun x => ⟪w (t, x), spatialDerivative u t x (w (t, x))⟫_ℝ).

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.PeriodicUniqueness.energy_nonneg (u v : ProblemStatement.VelocityField) (t : ℝ) : 0 ≤ energy u v t

theorem NavierStokes.PeriodicUniqueness.dissipation_nonneg (w : ProblemStatement.VelocityField) (t : ℝ) : 0 ≤ dissipation w t

theorem NavierStokes.PeriodicUniqueness.energy_balance {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} {t : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => v (t, x)) (hp : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => p (t, x)) (hq : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => q (t, x)) (hpu : PeriodicIntegration.UnitPeriods fun (x : ProblemStatement.Space) => u (t, x)) (hpv : PeriodicIntegration.UnitPeriods fun (x : ProblemStatement.Space) => v (t, x)) (hpp : PeriodicIntegration.UnitPeriods fun (x : ProblemStatement.Space) => p (t, x)) (hpq : PeriodicIntegration.UnitPeriods fun (x : ProblemStatement.Space) => q (t, x)) (hdu : ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence u t x = 0) (hdv : ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence v t x = 0) (htu : ∀ (x : ProblemStatement.Space), DifferentiableAt ℝ (fun (s : ℝ) => u (s, x)) t) (htv : ∀ (x : ProblemStatement.Space), DifferentiableAt ℝ (fun (s : ℝ) => v (s, x)) t) (hNS : ∀ (x : ProblemStatement.Space), ProblemStatement.navierStokesResidual u p t x = ProblemStatement.navierStokesResidual v q t x) : energyRate u v t = -2 * dissipation (u - v) t - 2 * coupling u (u - v) t

The exact difference-energy balance, derived from the actual PDE, pressure cancellation, divergence-free transport, and viscous integration by parts. No energy inequality is an input.

theorem NavierStokes.PeriodicUniqueness.neg_coupling_le_energy {u v : ProblemStatement.VelocityField} {t B : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => v (t, x)) (hB : ∀ y ∈ PeriodicIntegration.cube, ‖ProblemStatement.spatialDerivative u t (PeriodicIntegration.toSpace y)‖ ≤ B) : -coupling u (u - v) t ≤ B * energy u v t

Integrating the pointwise nonlinear bound only needs a gradient bound on the compact unit cube.

theorem NavierStokes.PeriodicUniqueness.energy_rate_le {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} {t B : ℝ} (hu : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => u (t, x)) (hv : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => v (t, x)) (hp : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => p (t, x)) (hq : ContDiff ℝ ↑⊤ fun (x : ProblemStatement.Space) => q (t, x)) (hpu : PeriodicIntegration.UnitPeriods fun (x : ProblemStatement.Space) => u (t, x)) (hpv : PeriodicIntegration.UnitPeriods fun (x : ProblemStatement.Space) => v (t, x)) (hpp : PeriodicIntegration.UnitPeriods fun (x : ProblemStatement.Space) => p (t, x)) (hpq : PeriodicIntegration.UnitPeriods fun (x : ProblemStatement.Space) => q (t, x)) (hdu : ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence u t x = 0) (hdv : ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence v t x = 0) (htu : ∀ (x : ProblemStatement.Space), DifferentiableAt ℝ (fun (s : ℝ) => u (s, x)) t) (htv : ∀ (x : ProblemStatement.Space), DifferentiableAt ℝ (fun (s : ℝ) => v (s, x)) t) (hNS : ∀ (x : ProblemStatement.Space), ProblemStatement.navierStokesResidual u p t x = ProblemStatement.navierStokesResidual v q t x) (hB : ∀ y ∈ PeriodicIntegration.cube, ‖ProblemStatement.spatialDerivative u t (PeriodicIntegration.toSpace y)‖ ≤ B) : energyRate u v t ≤ 2 * B * energy u v t

theorem NavierStokes.PeriodicUniqueness.time_differentiable_at_interior {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {a b t : ℝ} {u : ProblemStatement.SpaceTime → V} (hu : ContDiffOn ℝ (↑⊤) u (slab a b)) (ht : t ∈ Set.Ioo a b) (x : ProblemStatement.Space) : DifferentiableAt ℝ (fun (s : ℝ) => u (s, x)) t

theorem NavierStokes.PeriodicUniqueness.energy_continuousOn {a b : ℝ} {u v : ProblemStatement.VelocityField} (hu : ContDiffOn ℝ (↑⊤) u (slab a b)) (hv : ContDiffOn ℝ (↑⊤) v (slab a b)) : ContinuousOn (energy u v) (Set.Icc a b)

theorem NavierStokes.PeriodicUniqueness.energy_hasDerivAt {a b t : ℝ} {u v : ProblemStatement.VelocityField} (hu : ContDiffOn ℝ (↑⊤) u (slab a b)) (hv : ContDiffOn ℝ (↑⊤) v (slab a b)) (ht : t ∈ Set.Ioo a b) : HasDerivAt (energy u v) (energyRate u v t) t

Differentiation under the genuine spatial integral is justified by joint smoothness and compactness of the cube.

theorem NavierStokes.PeriodicUniqueness.energy_initial_zero {u v : ProblemStatement.VelocityField} {a : ℝ} (hinitial : ∀ (x : ProblemStatement.Space), u (a, x) = v (a, x)) : energy u v a = 0

theorem NavierStokes.PeriodicUniqueness.eq_of_energy_zero {u v : ProblemStatement.VelocityField} {t : ℝ} (hu : Continuous fun (x : ProblemStatement.Space) => u (t, x)) (hv : Continuous fun (x : ProblemStatement.Space) => v (t, x)) (hpu : PeriodicIntegration.UnitPeriods fun (x : ProblemStatement.Space) => u (t, x)) (hpv : PeriodicIntegration.UnitPeriods fun (x : ProblemStatement.Space) => v (t, x)) (hzero : energy u v t = 0) (x : ProblemStatement.Space) : u (t, x) = v (t, x)

Zero squared L² difference implies equality everywhere, using continuity on the cube and the explicitly proved periodic representatives.

theorem NavierStokes.PeriodicUniqueness.classical_uniqueness_on_Icc {a b : ℝ} {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (hu : ContDiffOn ℝ (↑⊤) u (slab a b)) (hv : ContDiffOn ℝ (↑⊤) v (slab a b)) (hp : ContDiffOn ℝ (↑⊤) p (slab a b)) (hq : ContDiffOn ℝ (↑⊤) q (slab a b)) (hpu : ProblemStatement.UnitSpatialPeriodsOn (Set.Icc a b) u) (hpv : ProblemStatement.UnitSpatialPeriodsOn (Set.Icc a b) v) (hpp : ProblemStatement.UnitSpatialPeriodsOn (Set.Icc a b) p) (hpq : ProblemStatement.UnitSpatialPeriodsOn (Set.Icc a b) q) (hdu : ∀ t ∈ Set.Ioo a b, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence u t x = 0) (hdv : ∀ t ∈ Set.Ioo a b, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence v t x = 0) (hNSu : ∀ t ∈ Set.Ioo a b, ∀ (x : ProblemStatement.Space), ProblemStatement.navierStokesResidual u p t x = f (t, x)) (hNSv : ∀ t ∈ Set.Ioo a b, ∀ (x : ProblemStatement.Space), ProblemStatement.navierStokesResidual v q t x = f (t, x)) (hinitial : ∀ (x : ProblemStatement.Space), u (a, x) = v (a, x)) (t : ℝ) : t ∈ Set.Icc a b → ∀ (x : ProblemStatement.Space), u (t, x) = v (t, x)

Classical uniqueness on a compact time interval for the exact periodic Navier--Stokes equation of ProblemStatement, with viscosity one. Both solutions have the same force and initial datum. The energy inequality, uniform gradient bound, and spatial integration identities are conclusions of the preceding proofs, not assumptions of this theorem.

theorem NavierStokes.PeriodicUniqueness.candidate_unique_on_Icc {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {f : ProblemStatement.VelocityField} (h : ProblemStatement.CandidateProperties u p f) {T : ℝ} (hT : T < 1) {v : ProblemStatement.VelocityField} {q : ProblemStatement.PressureField} (hv : ContDiffOn ℝ (↑⊤) v (slab 0 T)) (hq : ContDiffOn ℝ (↑⊤) q (slab 0 T)) (hpv : ProblemStatement.UnitSpatialPeriodsOn (Set.Icc 0 T) v) (hpq : ProblemStatement.UnitSpatialPeriodsOn (Set.Icc 0 T) q) (hdv : ∀ t ∈ Set.Ioo 0 T, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence v t x = 0) (hNSv : ∀ t ∈ Set.Ioo 0 T, ∀ (x : ProblemStatement.Space), ProblemStatement.navierStokesResidual v q t x = f (t, x)) (hvzero : ∀ (x : ProblemStatement.Space), v (0, x) = 0) (t : ℝ) : t ∈ Set.Icc 0 T → ∀ (x : ProblemStatement.Space), u (t, x) = v (t, x)

Direct application to the exact candidate specification: any other classical periodic solution with its force and zero initial velocity must agree on every compact interval strictly before time one. The comparison solution is not assumed to satisfy the candidate blow-up condition.