Terminal extensions from a common shrinking outer support

The actual similarity coordinate tends jointly to zero at a terminal point whose axial coordinate is zero. A family supported inside a common multiple of its square root therefore vanishes on one common open past neighborhood of every nonzero such point. This argument applies before summing or taking the spatial curl, and requires neither a lower support radius nor estimates on the individual summands.

@[reducible, inline]

abbrev NavierStokes.AnnularEndpoint.Space : Type

Space: an abbreviation for ProblemStatement.Space.

Equations

• NavierStokes.AnnularEndpoint.Space = NavierStokes.ProblemStatement.Space

@[reducible, inline]

abbrev NavierStokes.AnnularEndpoint.SpaceTime : Type

Space time: an abbreviation for ProblemStatement.SpaceTime.

Equations

• NavierStokes.AnnularEndpoint.SpaceTime = NavierStokes.ProblemStatement.SpaceTime

noncomputable def NavierStokes.AnnularEndpoint.radius (w : SpaceTime) : ℝ

The actual Cartesian distance to the symmetry axis.

Equations

• NavierStokes.AnnularEndpoint.radius w = NavierStokes.PolarCharts.radius (NavierStokes.PhysicalGraphBounds.radialProjection w)

theorem NavierStokes.AnnularEndpoint.radius_continuous : Continuous radius

theorem NavierStokes.AnnularEndpoint.radius_nonneg (w : SpaceTime) : 0 ≤ radius w

theorem NavierStokes.AnnularEndpoint.radius_pos_at_terminal {x : Space} (hx : x ≠ 0) (hz : x.ofLp 2 = 0) : 0 < radius (1, x)

noncomputable def NavierStokes.AnnularEndpoint.outerRadius (h C : ℝ) (w : SpaceTime) : ℝ

The support radius uses the same physical similarity coordinate as the wave construction, rather than a separately postulated scale.

Equations

• NavierStokes.AnnularEndpoint.outerRadius h C w = C * √(NavierStokes.PhysicalWaveSum.physicalQ h w)

theorem NavierStokes.AnnularEndpoint.physicalQ_tendsto_zero {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {x : Space} (hz : x.ofLp 2 = 0) : Filter.Tendsto (PhysicalWaveSum.physicalQ h) (nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1)) (nhds 0)

theorem NavierStokes.AnnularEndpoint.outerRadius_tendsto_zero {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (C : ℝ) {x : Space} (hz : x.ofLp 2 = 0) : Filter.Tendsto (outerRadius h C) (nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1)) (nhds 0)

theorem NavierStokes.AnnularEndpoint.outerRadius_continuousAt {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {w : SpaceTime} (ht : w.1 < 1) : ContinuousAt (outerRadius h C) w

theorem NavierStokes.AnnularEndpoint.exists_separating_neighborhood {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (C : ℝ) {x : Space} (hx : x ≠ 0) (hz : x.ofLp 2 = 0) : ∃ (U : Set SpaceTime), IsOpen U ∧ (1, x) ∈ U ∧ ∀ w ∈ U, w.1 < 1 → outerRadius h C w < radius w

One geometric neighborhood works for every member of any family with the same outer support constant. No sign or size assumption on C is needed.

def NavierStokes.AnnularEndpoint.ShrinkingSupport {V : Type u_1} [Zero V] (h C : ℝ) (f : SpaceTime → V) : Prop

A pointwise physical support invariant. It contains no endpoint or derivative assertion.

Equations

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

theorem NavierStokes.AnnularEndpoint.ShrinkingSupport.zero_of_separated {V : Type u_1} [Zero V] {h C : ℝ} {f : SpaceTime → V} (hf : ShrinkingSupport h C f) {w : SpaceTime} (ht : w.1 < 1) (hs : outerRadius h C w < radius w) : f w = 0

theorem NavierStokes.AnnularEndpoint.ShrinkingSupport.map_zero {V : Type u_1} [Zero V] {W : Type u_2} [Zero W] {h C : ℝ} {f : SpaceTime → V} (hf : ShrinkingSupport h C f) (T : SpaceTime → V → W) (hT : ∀ (w : SpaceTime), T w 0 = 0) : ShrinkingSupport h C fun (w : SpaceTime) => T w (f w)

Zero-preserving pointwise reconstructions, including real parts and vector-valued coefficient maps, preserve the physical support invariant.

theorem NavierStokes.AnnularEndpoint.exists_common_zero_neighborhood {V : Type u_1} [Zero V] {ι : Type u_2} {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ι → SpaceTime → V} (hf : ∀ (i : ι), ShrinkingSupport h C (f i)) {x : Space} (hx : x ≠ 0) (hz : x.ofLp 2 = 0) : ∃ (U : Set SpaceTime), IsOpen U ∧ (1, x) ∈ U ∧ ∀ w ∈ U, w.1 < 1 → ∀ (i : ι), f i w = 0

theorem NavierStokes.AnnularEndpoint.exists_zero_neighborhood {V : Type u_1} [Zero V] {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : SpaceTime → V} (hf : ShrinkingSupport h C f) {x : Space} (hx : x ≠ 0) (hz : x.ofLp 2 = 0) : ∃ (U : Set SpaceTime), IsOpen U ∧ (1, x) ∈ U ∧ Set.EqOn f (fun (x : SpaceTime) => 0) (U ∩ SpacetimeEndpoint.openPast 1)

theorem NavierStokes.AnnularEndpoint.ShrinkingSupport.smul {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h C : ℝ} {f : SpaceTime → V} (hf : ShrinkingSupport h C f) (c : SpaceTime → ℝ) : ShrinkingSupport h C fun (w : SpaceTime) => c w • f w

Multiplying a correction by any scalar cutoff preserves its outer support; the cutoff can depend on all physical variables.

theorem NavierStokes.AnnularEndpoint.ShrinkingSupport.add {V : Type u_1} [NormedAddCommGroup V] {h C : ℝ} {f g : SpaceTime → V} (hf : ShrinkingSupport h C f) (hg : ShrinkingSupport h C g) : ShrinkingSupport h C fun (w : SpaceTime) => f w + g w

theorem NavierStokes.AnnularEndpoint.ShrinkingSupport.finset_sum {V : Type u_1} [NormedAddCommGroup V] {ι : Type u_2} {h C : ℝ} {f : ι → SpaceTime → V} (s : Finset ι) (hf : ∀ i ∈ s, ShrinkingSupport h C (f i)) : ShrinkingSupport h C fun (w : SpaceTime) => ∑ i ∈ s, f i w

theorem NavierStokes.AnnularEndpoint.ShrinkingSupport.tsum {V : Type u_1} [NormedAddCommGroup V] {ι : Type u_2} {h C : ℝ} {f : ι → SpaceTime → V} (hf : ∀ (i : ι), ShrinkingSupport h C (f i)) : ShrinkingSupport h C fun (w : SpaceTime) => ∑' (i : ι), f i w

theorem NavierStokes.AnnularEndpoint.ShrinkingSupport.finsum {V : Type u_1} [NormedAddCommGroup V] {ι : Type u_2} {h C : ℝ} {f : ι → SpaceTime → V} (hf : ∀ (i : ι), ShrinkingSupport h C (f i)) : ShrinkingSupport h C fun (w : SpaceTime) => ∑ᶠ (i : ι), f i w

theorem NavierStokes.AnnularEndpoint.ShrinkingSupport.potentialSum {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h C : ℝ} {f : ℕ → SpaceTime → V} (hf : ∀ (j : ℕ), ShrinkingSupport h C (f j)) (a : ℕ → ℝ) (q : SpaceTime → ℝ) : ShrinkingSupport h C (SolenoidalDiagonal.potentialSum a q f)

theorem NavierStokes.AnnularEndpoint.radius_le_of_scaled_annulus {a b q : ℝ} {n : ℕ} {w : SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b) (hQ : ChartScales.Q n ≤ 2 * q) : radius w ≤ 2 * b * √2 * √q

The normalized annulus and the actual dyadic-mask comparison imply a uniform physical outer radius. The product norm costs a factor of two.

theorem NavierStokes.AnnularEndpoint.shrinkingSupport_of_normalized_annulus {V : Type u_1} [Zero V] {a b h : ℝ} {f : SpaceTime → V} (hf : ∀ (w : SpaceTime), w.1 < 1 → f w ≠ 0 → ∃ (n : ℕ), (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b ∧ ChartScales.Q n ≤ 2 * PhysicalWaveSum.physicalQ h w) : ShrinkingSupport h (2 * b * √2) f

theorem NavierStokes.AnnularEndpoint.regularFamily_term_support {H : ℕ} {f : PhysicalWaveSum.WaveFamily H} {a b h r0 Z : ℝ} {Δ : ℕ} (hf : PhysicalWaveSum.RegularFamily f a b h r0 Z Δ) (I : PhysicalWaveSum.WaveIndex H) : ShrinkingSupport h (2 * b * √2) (f.term a h r0 I)

An adapter from the already constructed scalar physical wave family. This uses its actual amplitude support and its actual slow mask.

theorem NavierStokes.AnnularEndpoint.regularFamily_sum_support {H : ℕ} {f : PhysicalWaveSum.WaveFamily H} {a b h r0 Z : ℝ} {Δ : ℕ} (hf : PhysicalWaveSum.RegularFamily f a b h r0 Z Δ) : ShrinkingSupport h (2 * b * √2) (f.sum a h r0)

theorem NavierStokes.AnnularEndpoint.copyFamily_sum_support {H Δ : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} (hf : PhysicalCopyBounds.RegularFamily f a b h r0 Z Δ) : ShrinkingSupport h (2 * b * √2) (f.sum a h r0)

The complete physical copy-and-label sum has the same outer support. The support witness keeps the individual copy and its own carrier center.

theorem NavierStokes.AnnularEndpoint.copyFamily_real_sum_support {H Δ : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} (hf : PhysicalCopyBounds.RegularFamily f a b h r0 Z Δ) : ShrinkingSupport h (2 * b * √2) fun (w : SpaceTime) => (f.sum a h r0 w).re

theorem NavierStokes.AnnularEndpoint.copyFamily_vector_support {H Δ : ℕ} {K : Type u_1} {f : Fin 3 → PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} (hf : ∀ (i : Fin 3), PhysicalCopyBounds.RegularFamily (f i) a b h r0 Z Δ) : ShrinkingSupport h (2 * b * √2) (PhysicalCopyBounds.vectorSum f a h r0)

theorem NavierStokes.AnnularEndpoint.zero_germ_of_eqOn {V : Type u_1} [NormedAddCommGroup V] {f : SpaceTime → V} {U : Set SpaceTime} (hU : IsOpen U) (hf : Set.EqOn f (fun (x : SpaceTime) => 0) (U ∩ SpacetimeEndpoint.openPast 1)) {w : SpaceTime} (hw : w ∈ U) (ht : w.1 < 1) : f =ᶠ[nhds w] fun (x : SpaceTime) => 0

theorem NavierStokes.AnnularEndpoint.ShrinkingSupport.zero_germ {V : Type u_1} [NormedAddCommGroup V] {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : SpaceTime → V} (hf : ShrinkingSupport h C f) {w : SpaceTime} (ht : w.1 < 1) (hs : outerRadius h C w < radius w) : f =ᶠ[nhds w] fun (x : SpaceTime) => 0

At every preterminal point strictly outside the support radius the field is zero on an ambient neighborhood.

theorem NavierStokes.AnnularEndpoint.ShrinkingSupport.derivative_support {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : SpaceTime → V} (hf : ShrinkingSupport h C f) (m : ℕ) : ShrinkingSupport h C (iteratedFDeriv ℝ m f)

theorem NavierStokes.AnnularEndpoint.jets_zero_of_eqOn {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} {U : Set SpaceTime} (hU : IsOpen U) (hf : Set.EqOn f (fun (x : SpaceTime) => 0) (U ∩ SpacetimeEndpoint.openPast 1)) (m : ℕ) : Set.EqOn (iteratedFDeriv ℝ m f) (fun (x : SpaceTime) => 0) (U ∩ SpacetimeEndpoint.openPast 1)

Actual joint derivatives vanish on the same open past neighborhood.

noncomputable def NavierStokes.AnnularEndpoint.zeroExtension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SpaceTime → V} {x : Space} {U : Set SpaceTime} (hU : IsOpen U) (hxU : (1, x) ∈ U) (hf : Set.EqOn f (fun (x : SpaceTime) => 0) (U ∩ SpacetimeEndpoint.openPast 1)) : JointResidualLimits.OneSidedExtension f x

The extension is the literal zero function on an actual ambient open neighborhood, not only a limiting boundary value.

Equations

• NavierStokes.AnnularEndpoint.zeroExtension hU hxU hf = { value := fun (x : NavierStokes.JointResidualLimits.SpaceTime) => 0, domain := U, isOpen := hU, mem := hxU, smooth := ⋯, agrees := ⋯ }

theorem NavierStokes.AnnularEndpoint.ShrinkingSupport.oneSidedExtension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : SpaceTime → V} (hf : ShrinkingSupport h C f) {x : Space} (hx : x ≠ 0) (hz : x.ofLp 2 = 0) : Nonempty (JointResidualLimits.OneSidedExtension f x)

theorem NavierStokes.AnnularEndpoint.ShrinkingSupport.jets_eventually_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : SpaceTime → V} (hf : ShrinkingSupport h C f) {x : Space} (hx : x ≠ 0) (hz : x.ofLp 2 = 0) (m : ℕ) : iteratedFDeriv ℝ m f =ᶠ[nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1)] fun (x : ℝ × Space) => 0

theorem NavierStokes.AnnularEndpoint.ShrinkingSupport.jets_tendsto_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : SpaceTime → V} (hf : ShrinkingSupport h C f) {x : Space} (hx : x ≠ 0) (hz : x.ofLp 2 = 0) (m : ℕ) : Filter.Tendsto (iteratedFDeriv ℝ m f) (nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1)) (nhds 0)

theorem NavierStokes.AnnularEndpoint.awayExtensions_of_offplane {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : SpaceTime → V} (hf : ShrinkingSupport h C f) (hoff : ∀ (x : Space), x.ofLp 2 ≠ 0 → Nonempty (JointResidualLimits.OneSidedExtension f x)) : JointResidualLimits.AwayExtensions f

The support argument supplies the central-plane branch. Extensions at nonzero axial coordinate remain a separate, explicit input.

noncomputable def NavierStokes.AnnularEndpoint.addZeroExtension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f g : SpaceTime → V} {x : Space} (e : JointResidualLimits.OneSidedExtension f x) {U : Set SpaceTime} (hU : IsOpen U) (hxU : (1, x) ∈ U) (hg : Set.EqOn g (fun (x : SpaceTime) => 0) (U ∩ SpacetimeEndpoint.openPast 1)) : JointResidualLimits.OneSidedExtension (fun (w : JointResidualLimits.SpaceTime) => f w + g w) x

Adding a correction which vanishes on a past neighborhood preserves the literal extension of the base field on the intersection.

Equations

• NavierStokes.AnnularEndpoint.addZeroExtension e hU hxU hg = { value := e.value, domain := e.domain ∩ U, isOpen := ⋯, mem := ⋯, smooth := ⋯, agrees := ⋯ }

theorem NavierStokes.AnnularEndpoint.add_supported_extension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f g : SpaceTime → V} {x : Space} (e : JointResidualLimits.OneSidedExtension f x) (hg : ShrinkingSupport h C g) (hx : x ≠ 0) (hz : x.ofLp 2 = 0) : Nonempty (JointResidualLimits.OneSidedExtension (fun (w : JointResidualLimits.SpaceTime) => f w + g w) x)

theorem NavierStokes.AnnularEndpoint.ShrinkingSupport.spatialCurl {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {A : SpaceTime → Space} (hA : ShrinkingSupport h C A) : ShrinkingSupport h C (SpatialCurl.spatialCurl A)

noncomputable def NavierStokes.AnnularEndpoint.curlExtension {A : SpaceTime → Space} {x : Space} (e : JointResidualLimits.OneSidedExtension A x) : JointResidualLimits.OneSidedExtension (SpatialCurl.spatialCurl A) x

The extension of a potential yields the extension of its actual Cartesian spatial curl.

Equations

• NavierStokes.AnnularEndpoint.curlExtension e = { value := NavierStokes.SpatialCurl.spatialCurl e.value, domain := e.domain, isOpen := ⋯, mem := ⋯, smooth := ⋯, agrees := ⋯ }

theorem NavierStokes.AnnularEndpoint.diagonal_sums_zero_near_terminal {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {A : ℕ → SpaceTime → Space} {p : ℕ → SpaceTime → ℝ} (hA : ∀ (j : ℕ), ShrinkingSupport h C (A j)) (hp : ∀ (j : ℕ), ShrinkingSupport h C (p j)) (a : ℕ → ℝ) (q : SpaceTime → ℝ) {x : Space} (hx : x ≠ 0) (hz : x.ofLp 2 = 0) : ∃ (U : Set SpaceTime), IsOpen U ∧ (1, x) ∈ U ∧ Set.EqOn (SolenoidalDiagonal.potentialSum a q A) (fun (x : SpaceTime) => 0) (U ∩ SpacetimeEndpoint.openPast 1) ∧ Set.EqOn (SolenoidalDiagonal.potentialSum a q p) (fun (x : SpaceTime) => 0) (U ∩ SpacetimeEndpoint.openPast 1) ∧ Set.EqOn (SolenoidalDiagonal.velocitySum a q A) (fun (x : ProblemStatement.SpaceTime) => 0) (U ∩ SpacetimeEndpoint.openPast 1) ∧ ∀ (m : ℕ), Set.EqOn (iteratedFDeriv ℝ m (SolenoidalDiagonal.potentialSum a q A)) (fun (x : SpaceTime) => 0) (U ∩ SpacetimeEndpoint.openPast 1) ∧ Set.EqOn (iteratedFDeriv ℝ m (SolenoidalDiagonal.potentialSum a q p)) (fun (x : SpaceTime) => 0) (U ∩ SpacetimeEndpoint.openPast 1) ∧ Set.EqOn (iteratedFDeriv ℝ m (SolenoidalDiagonal.velocitySum a q A)) (fun (x : ProblemStatement.SpaceTime) => 0) (U ∩ SpacetimeEndpoint.openPast 1)

One neighborhood kills both complete diagonal sums, their actual curl, and every joint derivative. The scalar cutoffs are arbitrary.

noncomputable def NavierStokes.AnnularEndpoint.diagonalAddition {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : SpaceTime → V) (a : ℕ → ℝ) (q : SpaceTime → ℝ) (F : ℕ → SpaceTime → V) (w : SpaceTime) : V

Add the actual diagonal sum before taking any velocity derivative.

Equations

• NavierStokes.AnnularEndpoint.diagonalAddition f a q F w = f w + NavierStokes.SolenoidalDiagonal.potentialSum a q F w

theorem NavierStokes.AnnularEndpoint.diagonal_addition_extension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : SpaceTime → V} {F : ℕ → SpaceTime → V} (hF : ∀ (j : ℕ), ShrinkingSupport h C (F j)) (a : ℕ → ℝ) (q : SpaceTime → ℝ) {x : Space} (hx : x ≠ 0) (hz : x.ofLp 2 = 0) (e : JointResidualLimits.OneSidedExtension f x) : Nonempty (JointResidualLimits.OneSidedExtension (diagonalAddition f a q F) x)

theorem NavierStokes.AnnularEndpoint.diagonal_addition_germs {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A0 : SpaceTime → Space) (p0 : SpaceTime → ℝ) {A : ℕ → SpaceTime → Space} {p : ℕ → SpaceTime → ℝ} (hA : ∀ (j : ℕ), ShrinkingSupport h C (A j)) (hp : ∀ (j : ℕ), ShrinkingSupport h C (p j)) (a : ℕ → ℝ) (q : SpaceTime → ℝ) {x : Space} (hx : x ≠ 0) (hz : x.ofLp 2 = 0) : ∃ (U : Set SpaceTime), IsOpen U ∧ (1, x) ∈ U ∧ ∀ w ∈ U, w.1 < 1 → diagonalAddition A0 a q A =ᶠ[nhds w] A0 ∧ SpatialCurl.spatialCurl (diagonalAddition A0 a q A) =ᶠ[nhds w] SpatialCurl.spatialCurl A0 ∧ diagonalAddition p0 a q p =ᶠ[nhds w] p0 ∧ (fun (z : SpaceTime) => ProblemStatement.navierStokesResidual (SpatialCurl.spatialCurl (diagonalAddition A0 a q A)) (diagonalAddition p0 a q p) z.1 z.2) =ᶠ[nhds w] fun (z : SpaceTime) => ProblemStatement.navierStokesResidual (SpatialCurl.spatialCurl A0) p0 z.1 z.2

Exact local agreement includes the concrete nonlinear Cartesian residual, without an assumed residual estimate.

noncomputable def NavierStokes.AnnularEndpoint.residualExtension {u : SpaceTime → Space} {p : SpaceTime → ℝ} {x : Space} (eu : JointResidualLimits.OneSidedExtension u x) (ep : JointResidualLimits.OneSidedExtension p x) : JointResidualLimits.OneSidedExtension (fun (w : JointResidualLimits.SpaceTime) => ProblemStatement.navierStokesResidual u p w.1 w.2) x

Local smooth field extensions determine a smooth extension of the actual Navier--Stokes residual by its differential formula.

Equations

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

theorem NavierStokes.AnnularEndpoint.final_diagonal_extensions {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {C : ℝ} {A : ℕ → SpaceTime → Space} {p : ℕ → SpaceTime → ℝ} (hA : ∀ (j : ℕ), ShrinkingSupport F.data.h C (A j)) (hp : ∀ (j : ℕ), ShrinkingSupport F.data.h C (p j)) (a : ℕ → ℝ) (q : SpaceTime → ℝ) {x : Space} (hx : x ≠ 0) (hz : x.ofLp 2 = 0) : have A' := diagonalAddition (TailGaugePotential.finalPotential H v upper B) a q A; have p' := diagonalAddition (FinalSlowBase.pressure H v upper B) a q p; Nonempty (JointResidualLimits.OneSidedExtension A' x) ∧ Nonempty (JointResidualLimits.OneSidedExtension (SpatialCurl.spatialCurl A') x) ∧ Nonempty (JointResidualLimits.OneSidedExtension p' x) ∧ Nonempty (JointResidualLimits.OneSidedExtension (fun (w : JointResidualLimits.SpaceTime) => ProblemStatement.navierStokesResidual (SpatialCurl.spatialCurl A') p' w.1 w.2) x)

Apply the shrinking-support construction to the actual selected slow-base potential in the terminally smooth radial gauge. All correction orders are retained. This assertion is at the central plane only.

theorem NavierStokes.AnnularEndpoint.final_diagonal_germs {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {C : ℝ} {A : ℕ → SpaceTime → Space} {p : ℕ → SpaceTime → ℝ} (hA : ∀ (j : ℕ), ShrinkingSupport F.data.h C (A j)) (hp : ∀ (j : ℕ), ShrinkingSupport F.data.h C (p j)) (a : ℕ → ℝ) (q : SpaceTime → ℝ) {x : Space} (hx : x ≠ 0) (hz : x.ofLp 2 = 0) : have A' := diagonalAddition (TailGaugePotential.finalPotential H v upper B) a q A; have p' := diagonalAddition (FinalSlowBase.pressure H v upper B) a q p; ∃ (U : Set SpaceTime), IsOpen U ∧ (1, x) ∈ U ∧ ∀ w ∈ U, w.1 < 1 → SpatialCurl.spatialCurl A' =ᶠ[nhds w] FinalSlowBase.velocity H v upper B ∧ p' =ᶠ[nhds w] FinalSlowBase.pressure H v upper B ∧ (fun (z : SpaceTime) => ProblemStatement.navierStokesResidual (SpatialCurl.spatialCurl A') p' z.1 z.2) =ᶠ[nhds w] fun (z : SpaceTime) => ProblemStatement.navierStokesResidual (FinalSlowBase.velocity H v upper B) (FinalSlowBase.pressure H v upper B) z.1 z.2

Near each nonzero terminal central-plane point, the corrected actual velocity, pressure, and residual agree as ambient germs with the same constructed slow base. All joint derivatives therefore agree there too.