Conditional candidate construction from actual residual derivative limits

The inputs are physical velocity and pressure fields and locally uniform limits of every full derivative of their actual Navier--Stokes residual. No future force or boundary compatibility is assumed. The force is the explicit Taylor--Borel extension of the traced residual of the activated, zero-extended fields.

The residual limits and the existence of singular incoming fields remain analytic hypotheses. This module does not prove the unconditional candidate.

Extending activated physical fields to the whole open past

The physical hypotheses constrain only nonnegative times. We explicitly replace negative-time values by zero. A zero germ at time zero makes this replacement jointly smooth, without any assumption on the original negative-time values. The actual residual is smooth and periodic on the whole open past and retains the original residual's terminal germ and all of its terminal derivative data.

@[reducible, inline]

abbrev NavierStokes.PastExtension.pastDomain : Set ProblemStatement.SpaceTime

Past domain: an abbreviation for SpacetimeEndpoint.openPast 1.

Equations

• NavierStokes.PastExtension.pastDomain = NavierStokes.SpacetimeEndpoint.openPast 1

noncomputable def NavierStokes.PastExtension.zeroBefore {V : Type u_1} [NormedAddCommGroup V] (g : ProblemStatement.SpaceTime → V) (z : ProblemStatement.SpaceTime) : V

Preserve nonnegative times and replace all negative-time values by zero.

Equations

• NavierStokes.PastExtension.zeroBefore g z = if 0 ≤ z.1 then g z else 0

theorem NavierStokes.PastExtension.zeroBefore_of_nonneg {V : Type u_1} [NormedAddCommGroup V] (g : ProblemStatement.SpaceTime → V) {t : ℝ} (ht : 0 ≤ t) (x : ProblemStatement.Space) : zeroBefore g (t, x) = g (t, x)

theorem NavierStokes.PastExtension.zeroBefore_of_neg {V : Type u_1} [NormedAddCommGroup V] (g : ProblemStatement.SpaceTime → V) {t : ℝ} (ht : t < 0) (x : ProblemStatement.Space) : zeroBefore g (t, x) = 0

theorem NavierStokes.PastExtension.zeroBefore_eqOn_nonneg {V : Type u_1} [NormedAddCommGroup V] (g : ProblemStatement.SpaceTime → V) : Set.EqOn (zeroBefore g) g (Set.Ici 0 ×ˢ Set.univ)

theorem NavierStokes.PastExtension.zeroBefore_eventuallyEq_pos {V : Type u_1} [NormedAddCommGroup V] {g : ProblemStatement.SpaceTime → V} {z : ProblemStatement.SpaceTime} (hz : 0 < z.1) : zeroBefore g =ᶠ[nhds z] g

theorem NavierStokes.PastExtension.zeroBefore_eventually_zero_neg {V : Type u_1} [NormedAddCommGroup V] {g : ProblemStatement.SpaceTime → V} {z : ProblemStatement.SpaceTime} (hz : z.1 < 0) : zeroBefore g =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.PastExtension.zeroBefore_eventually_zero_at_zero {V : Type u_1} [NormedAddCommGroup V] {g : ProblemStatement.SpaceTime → V} (x : ProblemStatement.Space) (hzero : g =ᶠ[nhds (0, x)] fun (x : ℝ × ProblemStatement.Space) => 0) : zeroBefore g =ᶠ[nhds (0, x)] fun (x : ℝ × ProblemStatement.Space) => 0

theorem NavierStokes.PastExtension.zeroBefore_eventuallyEq_nonneg {V : Type u_1} [NormedAddCommGroup V] {g : ProblemStatement.SpaceTime → V} (hzero : ∀ (x : ProblemStatement.Space), g =ᶠ[nhds (0, x)] fun (x : ℝ × ProblemStatement.Space) => 0) {t : ℝ} (ht : 0 ≤ t) (x : ProblemStatement.Space) : zeroBefore g =ᶠ[nhds (t, x)] g

The zero germ also preserves every local derivative at time zero.

theorem NavierStokes.PastExtension.zeroBefore_contDiffOn_past {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {g : ProblemStatement.SpaceTime → V} (hg : ContDiffOn ℝ (↑⊤) g ProblemStatement.preSingularDomain) (hzero : ∀ (x : ProblemStatement.Space), g =ᶠ[nhds (0, x)] fun (x : ℝ × ProblemStatement.Space) => 0) : ContDiffOn ℝ (↑⊤) (zeroBefore g) pastDomain

Relative physical smoothness and a zero initial germ suffice for joint smoothness on the entire open past. No negative-time regularity is assumed.

theorem NavierStokes.PastExtension.zeroBefore_periodic {V : Type u_1} [NormedAddCommGroup V] {g : ProblemStatement.SpaceTime → V} (hg : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) g) : ProblemStatement.UnitSpatialPeriodsOn (Set.Iio 1) (zeroBefore g)

noncomputable def NavierStokes.PastExtension.pastVelocity (u : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

Activated velocity with explicitly zero negative-time values.

Equations

• NavierStokes.PastExtension.pastVelocity u = NavierStokes.PastExtension.zeroBefore (NavierStokes.TimeLocalization.activatedVelocity u)

noncomputable def NavierStokes.PastExtension.pastPressure (p : ProblemStatement.PressureField) : ProblemStatement.PressureField

Activated pressure with explicitly zero negative-time values.

Equations

• NavierStokes.PastExtension.pastPressure p = NavierStokes.PastExtension.zeroBefore (NavierStokes.TimeLocalization.activatedPressure p)

theorem NavierStokes.PastExtension.activatedVelocity_zero_germ (u : ProblemStatement.VelocityField) (x : ProblemStatement.Space) : TimeLocalization.activatedVelocity u =ᶠ[nhds (0, x)] fun (x : ℝ × ProblemStatement.Space) => 0

theorem NavierStokes.PastExtension.activatedPressure_zero_germ (p : ProblemStatement.PressureField) (x : ProblemStatement.Space) : TimeLocalization.activatedPressure p =ᶠ[nhds (0, x)] fun (x : ℝ × ProblemStatement.Space) => 0

theorem NavierStokes.PastExtension.pastVelocity_eq_activated (u : ProblemStatement.VelocityField) {t : ℝ} (ht : 0 ≤ t) (x : ProblemStatement.Space) : pastVelocity u (t, x) = TimeLocalization.activatedVelocity u (t, x)

theorem NavierStokes.PastExtension.pastPressure_eq_activated (p : ProblemStatement.PressureField) {t : ℝ} (ht : 0 ≤ t) (x : ProblemStatement.Space) : pastPressure p (t, x) = TimeLocalization.activatedPressure p (t, x)

theorem NavierStokes.PastExtension.pastVelocity_zero_negative (u : ProblemStatement.VelocityField) {t : ℝ} (ht : t < 0) (x : ProblemStatement.Space) : pastVelocity u (t, x) = 0

theorem NavierStokes.PastExtension.pastPressure_zero_negative (p : ProblemStatement.PressureField) {t : ℝ} (ht : t < 0) (x : ProblemStatement.Space) : pastPressure p (t, x) = 0

theorem NavierStokes.PastExtension.pastVelocity_smooth (u : ProblemStatement.VelocityField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) : ContDiffOn ℝ (↑⊤) (pastVelocity u) pastDomain

theorem NavierStokes.PastExtension.pastPressure_smooth (p : ProblemStatement.PressureField) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) : ContDiffOn ℝ (↑⊤) (pastPressure p) pastDomain

theorem NavierStokes.PastExtension.pastVelocity_periodic (u : ProblemStatement.VelocityField) (hu : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) u) : ProblemStatement.UnitSpatialPeriodsOn (Set.Iio 1) (pastVelocity u)

theorem NavierStokes.PastExtension.pastPressure_periodic (p : ProblemStatement.PressureField) (hp : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) p) : ProblemStatement.UnitSpatialPeriodsOn (Set.Iio 1) (pastPressure p)

theorem NavierStokes.PastExtension.pastVelocity_eventuallyEq_activated (u : ProblemStatement.VelocityField) {t : ℝ} (ht : 0 ≤ t) (x : ProblemStatement.Space) : pastVelocity u =ᶠ[nhds (t, x)] TimeLocalization.activatedVelocity u

theorem NavierStokes.PastExtension.pastPressure_eventuallyEq_activated (p : ProblemStatement.PressureField) {t : ℝ} (ht : 0 ≤ t) (x : ProblemStatement.Space) : pastPressure p =ᶠ[nhds (t, x)] TimeLocalization.activatedPressure p

theorem NavierStokes.PastExtension.pastVelocity_eq_late (u : ProblemStatement.VelocityField) {t : ℝ} (ht : 3 / 4 ≤ t) (x : ProblemStatement.Space) : pastVelocity u (t, x) = u (t, x)

theorem NavierStokes.PastExtension.pastPressure_eq_late (p : ProblemStatement.PressureField) {t : ℝ} (ht : 3 / 4 ≤ t) (x : ProblemStatement.Space) : pastPressure p (t, x) = p (t, x)

theorem NavierStokes.PastExtension.pastVelocity_eventuallyEq_late (u : ProblemStatement.VelocityField) {t : ℝ} (ht : 3 / 4 < t) (x : ProblemStatement.Space) : pastVelocity u =ᶠ[nhds (t, x)] u

theorem NavierStokes.PastExtension.pastPressure_eventuallyEq_late (p : ProblemStatement.PressureField) {t : ℝ} (ht : 3 / 4 < t) (x : ProblemStatement.Space) : pastPressure p =ᶠ[nhds (t, x)] p

theorem NavierStokes.PastExtension.pastVelocity_divergence_free (u : ProblemStatement.VelocityField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hdiv : ∀ t ∈ Set.Ico 0 1, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence u t x = 0) (t : ℝ) : t ∈ Set.Iio 1 → ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence (pastVelocity u) t x = 0

theorem NavierStokes.PastExtension.pastVelocity_speed_unbounded (u : ProblemStatement.VelocityField) (hu : ProblemStatement.SpeedUnboundedAtOne u) : ProblemStatement.SpeedUnboundedAtOne (pastVelocity u)

noncomputable def NavierStokes.PastExtension.pastResidual (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) : ProblemStatement.VelocityField

The force used by the endpoint theorem is the actual residual of the new fields on the entire open past, including negative times.

Equations

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

theorem NavierStokes.PastExtension.pastResidual_smooth (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) : ContDiffOn ℝ (↑⊤) (pastResidual u p) pastDomain

theorem NavierStokes.PastExtension.pastResidual_periodic (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) u) (hp : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) p) : ProblemStatement.UnitSpatialPeriodsOn (Set.Iio 1) (pastResidual u p)

theorem NavierStokes.PastExtension.pastResidual_eventually_zero_nonpos (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) {t : ℝ} (ht : t ≤ 0) (x : ProblemStatement.Space) : pastResidual u p =ᶠ[nhds (t, x)] fun (x : ℝ × ProblemStatement.Space) => 0

theorem NavierStokes.PastExtension.pastResidual_zero_nonpos (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) {t : ℝ} (ht : t ≤ 0) (x : ProblemStatement.Space) : pastResidual u p (t, x) = 0

theorem NavierStokes.PastExtension.pastResidual_eq_activated (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) {t : ℝ} (ht : 0 ≤ t) (x : ProblemStatement.Space) : pastResidual u p (t, x) = ProblemStatement.navierStokesResidual (TimeLocalization.activatedVelocity u) (TimeLocalization.activatedPressure p) t x

theorem NavierStokes.PastExtension.pastResidual_eventuallyEq_late (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) {t : ℝ} (ht : 3 / 4 < t) (x : ProblemStatement.Space) : pastResidual u p =ᶠ[nhds (t, x)] fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2

theorem NavierStokes.PastExtension.pastResidual_eq_late (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) {t : ℝ} (ht : 3 / 4 < t) (x : ProblemStatement.Space) : pastResidual u p (t, x) = ProblemStatement.navierStokesResidual u p t x

theorem NavierStokes.PastExtension.pastResidual_iteratedFDeriv_eq_late (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (n : ℕ) {t : ℝ} (ht : 3 / 4 < t) (x : ProblemStatement.Space) : iteratedFDeriv ℝ n (pastResidual u p) (t, x) = iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)

Full joint derivative tensors, not only values, retain the terminal germ.

theorem NavierStokes.PastExtension.pastResidual_locallyUniform_limit (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (n : ℕ) (L : ProblemStatement.Space → ProblemStatement.SpaceTime [×n]→L[ℝ] ProblemStatement.Space) (hlim : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) L (nhdsWithin 1 (Set.Iio 1))) : TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (pastResidual u p) (t, x)) L (nhdsWithin 1 (Set.Iio 1))

Any locally uniform limiting full derivative tensor transfers unchanged. This hypothesis is not supplied by the zero extension itself.

theorem NavierStokes.PastExtension.pastResidual_derivative_recurrence (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (n : ℕ) (z : ProblemStatement.SpaceTime) (hz : z.1 < 1) : HasFDerivAt (iteratedFDeriv ℝ n (pastResidual u p)) (iteratedFDeriv ℝ (n + 1) (pastResidual u p) z).curryLeft z

The full derivative family required by SpacetimeEndpoint is supplied by the actual derivatives of the constructed past residual.

theorem NavierStokes.PastExtension.exists_joint_endpoint_extension_of_residual_limits (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) : ∃ (g : ProblemStatement.VelocityField), Set.EqOn g (pastResidual u p) pastDomain ∧ ContDiffOn ℝ (↑⊤) g (SpacetimeEndpoint.closedPast 1) ∧ ∀ (n : ℕ) (x : ProblemStatement.Space), iteratedFDerivWithin ℝ n g (SpacetimeEndpoint.closedPast 1) (1, x) = L x n

A direct adapter to joint endpoint regularity. Only the locally uniform limits near time one remain an analytic input; no negative-time assumptions are imposed on the original velocity or pressure.

noncomputable def NavierStokes.CandidateFromLimits.tracedResidual (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) : ProblemStatement.VelocityField

Fill in the endpoint trace after extending the activated residual to negative times by the construction in PastExtension.

Equations

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

theorem NavierStokes.CandidateFromLimits.tracedResidual_smooth (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) : ContDiffOn ℝ (↑⊤) (tracedResidual u p L) (SpacetimeEndpoint.closedPast 1)

Closed-side joint smoothness is derived from the actual derivative recurrence and the supplied locally uniform limits.

theorem NavierStokes.CandidateFromLimits.tracedResidual_boundary_jets (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) (n : ℕ) (x : ProblemStatement.Space) : iteratedFDerivWithin ℝ n (tracedResidual u p L) (SpacetimeEndpoint.closedPast 1) (1, x) = L x n

theorem NavierStokes.CandidateFromLimits.tracedResidual_periodic (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) (huper : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) u) (hpper : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) p) : ProblemStatement.UnitSpatialPeriodsOn Set.univ (tracedResidual u p L)

noncomputable def NavierStokes.CandidateFromLimits.force (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) : ProblemStatement.VelocityField

The specified force: glue the traced past residual to the Taylor--Borel series of its actual normal jets. No force is an input to this definition.

Equations

• NavierStokes.CandidateFromLimits.force u p hu hp L hlim = NavierStokes.SpacetimeGluing.smoothExtension 1 (NavierStokes.CandidateFromLimits.tracedResidual u p L) ⋯

theorem NavierStokes.CandidateFromLimits.force_smooth (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) : ContDiff ℝ (↑⊤) (force u p hu hp L hlim)

theorem NavierStokes.CandidateFromLimits.force_periodic (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) (huper : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) u) (hpper : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) p) : ProblemStatement.UnitSpatialPeriodsOn Set.univ (force u p hu hp L hlim)

theorem NavierStokes.CandidateFromLimits.force_eq_pastResidual (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) {t : ℝ} (ht : t < 1) (x : ProblemStatement.Space) : force u p hu hp L hlim (t, x) = PastExtension.pastResidual u p (t, x)

The force agrees with the actual activated residual throughout the whole past, not just on an arbitrarily short terminal overlap.

theorem NavierStokes.CandidateFromLimits.force_eq_activated_residual (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t < 1) (x : ProblemStatement.Space) : force u p hu hp L hlim (t, x) = ProblemStatement.navierStokesResidual (TimeLocalization.activatedVelocity u) (TimeLocalization.activatedPressure p) t x

theorem NavierStokes.CandidateFromLimits.force_zero_from (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) {t : ℝ} (ht : 2 ≤ t) (x : ProblemStatement.Space) : force u p hu hp L hlim (t, x) = 0

theorem NavierStokes.CandidateFromLimits.force_zero_nonpos (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) {t : ℝ} (ht : t ≤ 0) (x : ProblemStatement.Space) : force u p hu hp L hlim (t, x) = 0

theorem NavierStokes.CandidateFromLimits.force_time_support (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) : ProblemStatement.CompactFutureTimeSupport (force u p hu hp L hlim)

theorem NavierStokes.CandidateFromLimits.force_boundary_jets (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) (n : ℕ) (x : ProblemStatement.Space) : iteratedFDeriv ℝ n (force u p hu hp L hlim) (1, x) = L x n

Every full spacetime boundary derivative is exactly its supplied limit.

theorem NavierStokes.CandidateFromLimits.force_derivative_decay (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) (huper : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) u) (hpper : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) p) (m : ℕ) (K : ℝ) (hK : 0 ≤ K) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → ∀ (x : ProblemStatement.Space), ‖iteratedFDeriv ℝ m (force u p hu hp L hlim) (t, x)‖ ≤ C * (1 + t) ^ (-K)

Compact time support and global joint smoothness give arbitrary polynomial decay of every actual full derivative tensor.

theorem NavierStokes.CandidateFromLimits.force_mixed_derivative_decay (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) (huper : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) u) (hpper : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) p) (m : ℕ) (K : ℝ) (hK : 0 ≤ K) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → ∀ (x : ProblemStatement.Space) (directions : Fin m → Fin 4) (j : Fin 3), |((iteratedFDeriv ℝ m (force u p hu hp L hlim) (t, x)) fun (i : Fin m) => CompactForceDecay.spacetimeCoordinate (directions i)).ofLp j| ≤ C * (1 + t) ^ (-K)

The same conclusion for every ordered choice of time/spatial coordinate directions and every output component. The constant is uniform in these choices.

theorem NavierStokes.CandidateFromLimits.candidate_properties (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) (huper : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) u) (hpper : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) p) (hdiv : ∀ t ∈ Set.Ico 0 1, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence u t x = 0) (hunbounded : ProblemStatement.SpeedUnboundedAtOne u) : ProblemStatement.CandidateProperties (TimeLocalization.activatedVelocity u) (TimeLocalization.activatedPressure p) (force u p hu hp L hlim)

The constructed force and activated fields satisfy the original explicit candidate specification. No force or closed-side regularity is assumed.

theorem NavierStokes.CandidateFromLimits.exists_candidate_force (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) (huper : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) u) (hpper : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) p) (hdiv : ∀ t ∈ Set.Ico 0 1, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence u t x = 0) (hunbounded : ProblemStatement.SpeedUnboundedAtOne u) : ∃ (F : ProblemStatement.VelocityField), ProblemStatement.CandidateProperties (TimeLocalization.activatedVelocity u) (TimeLocalization.activatedPressure p) F ∧ ContDiff ℝ (↑⊤) F ∧ ProblemStatement.UnitSpatialPeriodsOn Set.univ F ∧ (∀ (t : ℝ), 2 ≤ t → ∀ (x : ProblemStatement.Space), F (t, x) = 0) ∧ (∀ (n : ℕ) (x : ProblemStatement.Space), iteratedFDeriv ℝ n F (1, x) = L x n) ∧ ∀ (m : ℕ) (K : ℝ), 0 ≤ K → ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → ∀ (x : ProblemStatement.Space) (directions : Fin m → Fin 4) (j : Fin 3), |((iteratedFDeriv ℝ m F (t, x)) fun (i : Fin m) => CompactForceDecay.spacetimeCoordinate (directions i)).ofLp j| ≤ C * (1 + t) ^ (-K)

All force conclusions belong to the same constructed witness. The remaining hypotheses include the actual residual limits and singular velocity.

theorem NavierStokes.CandidateFromLimits.candidateStatement_of_residual_limits (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (L : ProblemStatement.Space → FormalMultilinearSeries ℝ ProblemStatement.SpaceTime ProblemStatement.Space) (hlim : ∀ (n : ℕ), TendstoLocallyUniformly (fun (t : ℝ) (x : ProblemStatement.Space) => iteratedFDeriv ℝ n (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (t, x)) (fun (x : ProblemStatement.Space) => L x n) (nhdsWithin 1 (Set.Iio 1))) (huper : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) u) (hpper : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) p) (hdiv : ∀ t ∈ Set.Ico 0 1, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence u t x = 0) (hunbounded : ProblemStatement.SpeedUnboundedAtOne u) : ProblemStatement.candidateStatement

Conditional reduction of the primary existential target to the stated physical fields and locally uniform limits of all actual residual derivatives.