Comparison with the compact candidate on all of R³

The whole-space uniqueness proof is ported from the verified R³ development. The competitor retains exactly the smoothness and finite-energy conditions of the comparator. The candidate's compact support supplies the reference solution's bounds on each closed interval before time one.

Viscosity normalization for the whole-space comparator

This version retains the comparator's square integrability and uniform kinetic energy bound. It makes no periodicity or compact-support assumption on a hypothetical global solution.

theorem NavierStokes.ComparatorBridge.zero_initial_condition_decay : Comparator.InitialVelocityConditionDecay fun (x : ProblemStatement.Space) => 0

structure NavierStokes.ComparatorBridge.GlobalSolutionRn (f v : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) : Prop

A global whole-space solution in the original physical coordinates.

• velocity_smooth : ContDiffOn ℝ (↑⊤) v ProblemStatement.futureDomain
• pressure_smooth : ContDiffOn ℝ (↑⊤) p ProblemStatement.futureDomain
• initial_velocity (x : ProblemStatement.Space) : v (0, x) = 0
• divergence_free (t : ℝ) : 0 ≤ t → ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence v t x = 0
• navier_stokes (t : ℝ) : 0 < t → ∀ (x : ProblemStatement.Space), ProblemStatement.navierStokesResidual v p t x = f (t, x)
• integrable (t : ℝ) : 0 ≤ t → MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => ‖v (t, x)‖) 2 MeasureTheory.volume
• globally_bounded_energy : ∃ (E : ℝ), ∀ (t : ℝ), 0 ≤ t → ∫ (x : ProblemStatement.Space), ‖v (t, x)‖ ^ 2 < E

theorem NavierStokes.ComparatorBridge.GlobalSolutionRn.toSolutionOn {f v : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (solution : GlobalSolutionRn f v p) : SolutionOn 1 0 (fun (x : ProblemStatement.Space) => 0) (Set.Ici 0) f v p

Forget energy bounds while retaining the shared equation and initial data.

theorem NavierStokes.ComparatorBridge.comparator_equation_Rn {ν : ℝ} {u₀ : ProblemStatement.Space → ProblemStatement.Space} {f v : ProblemStatement.Space → ℝ → ProblemStatement.Space} {p : ProblemStatement.Space → ℝ → ℝ} (h : Comparator.NavierStokesExistenceAndSmoothnessRn ν u₀ f v p) {t : ℝ} (ht : 0 < t) (x : ProblemStatement.Space) : ProblemStatement.temporalDerivative (fromComparator v) t x + ProblemStatement.advection (fromComparator v) t x - ν • ProblemStatement.spatialLaplacian (fromComparator v) t x + ProblemStatement.pressureGradient (fromComparator p) t x = f x t

theorem NavierStokes.ComparatorBridge.normalized_solution_Rn {ν : ℝ} (hν : 0 < ν) {f : ProblemStatement.VelocityField} {v : ProblemStatement.Space → ℝ → ProblemStatement.Space} {p : ProblemStatement.Space → ℝ → ℝ} (h : Comparator.NavierStokesExistenceAndSmoothnessRn ν (fun (x : EuclideanSpace ℝ (Fin 3)) => 0) (toComparator (rescaledForce ν f)) v p) : GlobalSolutionRn f (rescale ν⁻¹ ν⁻¹ (fromComparator v)) (rescale (ν⁻¹ ^ 2) ν⁻¹ (fromComparator p))

Normalize an arbitrary global finite-energy comparison solution to viscosity one.

theorem NavierStokes.ComparatorBridge.GlobalSolutionRn.uniformFiniteEnergy {f v : ProblemStatement.VelocityField} {q : ProblemStatement.PressureField} (h : GlobalSolutionRn f v q) (T : ℝ) : NavierStokesR3.ProblemStatement.UniformFiniteEnergy (Set.Icc 0 T) v

theorem NavierStokes.ComparatorBridge.compact_candidate_excludes_global_solution {u v f : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} (h : R3CompactCandidate.Properties u p f) (hv : GlobalSolutionRn f v q) : False

A compact candidate with unbounded speed excludes every global smooth solution having the comparator's finite-energy bound.