The physical natural core

The core is the actual Cartesian curl of meridional and swirl potentials obtained from the natural profiles. All regularity assertions are on the explicit open physical domain where those profiles have been constructed. No assertion about the regularity of the final Navier--Stokes force is made.

noncomputable def NavierStokes.NaturalCore.physicalQ (h : ℝ) (p : AxisymmetricFields.ProfilePoint) : ℝ

Physical Q, given by SimilarityCoordinates.coordinateQ (2 * h) (1 - p.1, p.2.2).

Equations

• NavierStokes.NaturalCore.physicalQ h p = NavierStokes.SimilarityCoordinates.coordinateQ (2 * h) (1 - p.1, p.2.2)

noncomputable def NavierStokes.NaturalCore.physicalEta (h : ℝ) (p : AxisymmetricFields.ProfilePoint) : ℝ

Physical eta, given by SimilarityCoordinates.coordinateEta (2 * h) (1 - p.1, p.2.2).

Equations

• NavierStokes.NaturalCore.physicalEta h p = NavierStokes.SimilarityCoordinates.coordinateEta (2 * h) (1 - p.1, p.2.2)

noncomputable def NavierStokes.NaturalCore.similarityPoint (h : ℝ) (p : AxisymmetricFields.ProfilePoint) : ℝ × ℝ

Similarity point, given by (p.2.1 / physicalQ h p, physicalEta h p).

Equations

• NavierStokes.NaturalCore.similarityPoint h p = (p.2.1 / NavierStokes.NaturalCore.physicalQ h p, NavierStokes.NaturalCore.physicalEta h p)

noncomputable def NavierStokes.NaturalCore.profileDomain (h Λ : ℝ) : Set AxisymmetricFields.ProfilePoint

Profile domain, given by {p | p.1 < 1 ∧ similarityPoint h p ∈ NaturalProfile.domain Λ}.

Equations

• NavierStokes.NaturalCore.profileDomain h Λ = {p : NavierStokes.AxisymmetricFields.ProfilePoint | p.1 < 1 ∧ NavierStokes.NaturalCore.similarityPoint h p ∈ NavierStokes.NaturalProfile.domain Λ}

noncomputable def NavierStokes.NaturalCore.coreDomain (h Λ : ℝ) : Set ProblemStatement.SpaceTime

Core domain, given by {z | profilePoint z.1 z.2 ∈ profileDomain h Λ}.

Equations

• NavierStokes.NaturalCore.coreDomain h Λ = {z : NavierStokes.ProblemStatement.SpaceTime | NavierStokes.AxisymmetricFields.profilePoint z.1 z.2 ∈ NavierStokes.NaturalCore.profileDomain h Λ}

noncomputable def NavierStokes.NaturalCore.radialPrimitive (f : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

The actual integral from zero to the radial profile coordinate.

Equations

• NavierStokes.NaturalCore.radialPrimitive f p = ∫ (v : ℝ) in 0..p.1, f (v, p.2)

noncomputable def NavierStokes.NaturalCore.meridionalPotential (h : ℝ) (V : ℝ × ℝ → ℝ) : AxisymmetricFields.Profile

Meridional potential, defined pointwise by physicalQ h p ^ (-NaturalAxisData.A h) * V (similarityPoint h p).

Equations

• NavierStokes.NaturalCore.meridionalPotential h V p = NavierStokes.NaturalCore.physicalQ h p ^ (-NavierStokes.NaturalAxisData.A h) * V (NavierStokes.NaturalCore.similarityPoint h p)

noncomputable def NavierStokes.NaturalCore.swirlPotential (h : ℝ) (f : ℝ × ℝ → ℝ) : AxisymmetricFields.Profile

Swirl potential, defined pointwise by -(physicalQ h p ^ (-h)) * radialPrimitive f (similarityPoint h p).

Equations

• NavierStokes.NaturalCore.swirlPotential h f p = -NavierStokes.NaturalCore.physicalQ h p ^ (-h) * NavierStokes.NaturalCore.radialPrimitive f (NavierStokes.NaturalCore.similarityPoint h p)

noncomputable def NavierStokes.NaturalCore.corePotential (h : ℝ) (f V : ℝ × ℝ → ℝ) : ProblemStatement.VelocityField

Core potential, given by potential (meridionalPotential h V) (swirlPotential h f).

Equations

• NavierStokes.NaturalCore.corePotential h f V = NavierStokes.AxisymmetricFields.potential (NavierStokes.NaturalCore.meridionalPotential h V) (NavierStokes.NaturalCore.swirlPotential h f)

noncomputable def NavierStokes.NaturalCore.coreVelocity (h : ℝ) (f V : ℝ × ℝ → ℝ) : ProblemStatement.VelocityField

Core velocity, given by velocity (meridionalPotential h V) (swirlPotential h f).

Equations

• NavierStokes.NaturalCore.coreVelocity h f V = NavierStokes.AxisymmetricFields.velocity (NavierStokes.NaturalCore.meridionalPotential h V) (NavierStokes.NaturalCore.swirlPotential h f)

theorem NavierStokes.NaturalCore.physicalQ_pos {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) : 0 < physicalQ h p

theorem NavierStokes.NaturalCore.physicalQ_contDiffAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) : ContDiffAt ℝ (↑⊤) (physicalQ h) p

theorem NavierStokes.NaturalCore.physicalEta_contDiffAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) : ContDiffAt ℝ (↑⊤) (physicalEta h) p

theorem NavierStokes.NaturalCore.similarityPoint_contDiffAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) : ContDiffAt ℝ (↑⊤) (similarityPoint h) p

theorem NavierStokes.NaturalCore.profileDomain_isOpen {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (Λ : ℝ) : IsOpen (profileDomain h Λ)

theorem NavierStokes.NaturalCore.coreDomain_isOpen {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (Λ : ℝ) : IsOpen (coreDomain h Λ)

theorem NavierStokes.NaturalCore.physicalQ_at_zero_z {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {t : ℝ} (ht : t < 1) (s : ℝ) : physicalQ h (t, s, 0) = 1 - t

theorem NavierStokes.NaturalCore.physicalEta_at_zero_z (h t s : ℝ) : physicalEta h (t, s, 0) = 0

theorem NavierStokes.NaturalCore.profile_axis_mem (h Λ : ℝ) {t : ℝ} (ht : t < 1) : (t, 0, 0) ∈ profileDomain h Λ

theorem NavierStokes.NaturalCore.core_axis_mem (h Λ : ℝ) {t : ℝ} (ht : t < 1) : (t, 0) ∈ coreDomain h Λ

theorem NavierStokes.NaturalCore.radial_segment_mem_domain {Λ : ℝ} {p : ℝ × ℝ} (hp : p ∈ NaturalProfile.domain Λ) {r : ℝ} (hr : r ∈ Set.Icc 0 1) : (p.1 * r, p.2) ∈ NaturalProfile.domain Λ

theorem NavierStokes.NaturalCore.parameterJet_contDiffAt {F : (ℝ × ℝ) × ℝ → ℝ} {z : (ℝ × ℝ) × ℝ} (hF : ContDiffAt ℝ (↑⊤) F z) (k : ℕ) : ContDiffAt ℝ (↑⊤) (fun (w : (ℝ × ℝ) × ℝ) => iteratedFDeriv ℝ k (fun (p : ℝ × ℝ) => F (p, w.2)) w.1) z

Local joint smoothness implies local joint smoothness of all actual parameter derivatives, even when the integration variable lies at an endpoint.

theorem NavierStokes.NaturalCore.radialPrimitive_unit_interval (f : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : radialPrimitive f p = p.1 * ∫ (r : ℝ) in 0..1, f (p.1 * r, p.2)

theorem NavierStokes.NaturalCore.radialPrimitive_contDiffOn {Λ : ℝ} {f : ℝ × ℝ → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (NaturalProfile.domain Λ)) : ContDiffOn ℝ (↑⊤) (radialPrimitive f) (NaturalProfile.domain Λ)

theorem NavierStokes.NaturalCore.radial_interval_mem_domain {Λ : ℝ} {p : ℝ × ℝ} (hp : p ∈ NaturalProfile.domain Λ) {r : ℝ} (hr : r ∈ Set.uIcc 0 p.1) : (r, p.2) ∈ NaturalProfile.domain Λ

theorem NavierStokes.NaturalCore.radialPrimitive_hasDerivAt {Λ : ℝ} {f : ℝ × ℝ → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (NaturalProfile.domain Λ)) {p : ℝ × ℝ} (hp : p ∈ NaturalProfile.domain Λ) : HasDerivAt (fun (r : ℝ) => radialPrimitive f (r, p.2)) (f p) p.1

The radial primitive has the claimed ordinary derivative by the fundamental theorem of calculus on its actual profile domain.

theorem NavierStokes.NaturalCore.partialS_eq_deriv_slice {F : AxisymmetricFields.Profile} {p : AxisymmetricFields.ProfilePoint} (hF : DifferentiableAt ℝ F p) : AxisymmetricFields.partialS F p = deriv (fun (s : ℝ) => F (p.1, s, p.2.2)) p.2.1

theorem NavierStokes.NaturalCore.meridionalPotential_contDiffAt {h Λ : ℝ} {V : ℝ × ℝ → ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hV : ContDiffOn ℝ (↑⊤) V (NaturalProfile.domain Λ)) {p : AxisymmetricFields.ProfilePoint} (hp : p ∈ profileDomain h Λ) : ContDiffAt ℝ (↑⊤) (meridionalPotential h V) p

theorem NavierStokes.NaturalCore.swirlPotential_contDiffAt {h Λ : ℝ} {f : ℝ × ℝ → ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hf : ContDiffOn ℝ (↑⊤) f (NaturalProfile.domain Λ)) {p : AxisymmetricFields.ProfilePoint} (hp : p ∈ profileDomain h Λ) : ContDiffAt ℝ (↑⊤) (swirlPotential h f) p

theorem NavierStokes.NaturalCore.meridionalPotential_partialS {h Λ : ℝ} {V : ℝ × ℝ → ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hV : ContDiffOn ℝ (↑⊤) V (NaturalProfile.domain Λ)) {p : AxisymmetricFields.ProfilePoint} (hp : p ∈ profileDomain h Λ) : AxisymmetricFields.partialS (meridionalPotential h V) p = physicalQ h p ^ (-NaturalAxisData.A h) / physicalQ h p * NaturalAxisBridge.partialY V (similarityPoint h p)

theorem NavierStokes.NaturalCore.swirlPotential_partialS {h Λ : ℝ} {f : ℝ × ℝ → ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hf : ContDiffOn ℝ (↑⊤) f (NaturalProfile.domain Λ)) {p : AxisymmetricFields.ProfilePoint} (hp : p ∈ profileDomain h Λ) : AxisymmetricFields.partialS (swirlPotential h f) p = -(physicalQ h p ^ (-h) / physicalQ h p) * f (similarityPoint h p)

theorem NavierStokes.NaturalCore.corePotential_contDiffAt {h Λ : ℝ} {f V : ℝ × ℝ → ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hf : ContDiffOn ℝ (↑⊤) f (NaturalProfile.domain Λ)) (hV : ContDiffOn ℝ (↑⊤) V (NaturalProfile.domain Λ)) {z : ProblemStatement.SpaceTime} (hz : z ∈ coreDomain h Λ) : ContDiffAt ℝ (↑⊤) (corePotential h f V) z

The potential is genuinely jointly smooth in Cartesian spacetime, including the axis, throughout the explicitly stated core domain.

theorem NavierStokes.NaturalCore.coreVelocity_contDiffOn {h Λ : ℝ} {f V : ℝ × ℝ → ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hf : ContDiffOn ℝ (↑⊤) f (NaturalProfile.domain Λ)) (hV : ContDiffOn ℝ (↑⊤) V (NaturalProfile.domain Λ)) : ContDiffOn ℝ (↑⊤) (coreVelocity h f V) (coreDomain h Λ)

theorem NavierStokes.NaturalCore.coreVelocity_divergence {h Λ : ℝ} {f V : ℝ × ℝ → ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hf : ContDiffOn ℝ (↑⊤) f (NaturalProfile.domain Λ)) (hV : ContDiffOn ℝ (↑⊤) V (NaturalProfile.domain Λ)) {t : ℝ} {x : ProblemStatement.Space} (hx : (t, x) ∈ coreDomain h Λ) : ProblemStatement.spatialDivergence (coreVelocity h f V) t x = 0

Divergence vanishes as an identity of the actual physical Fréchet derivatives, by Schwarz's theorem for the Cartesian potential.

theorem NavierStokes.NaturalCore.coreVelocity_axial {h j Λ : ℝ} {P0 a0 : ℝ → ℝ} {f U V Pr : ℝ × ℝ → ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a0 f U V Pr) {t : ℝ} {x : ProblemStatement.Space} (hx : (t, x) ∈ coreDomain h Λ) : (coreVelocity h f V (t, x)).ofLp 2 = physicalQ h (AxisymmetricFields.profilePoint t x) ^ (-NaturalAxisData.A h) * U (similarityPoint h (AxisymmetricFields.profilePoint t x))

The averaged meridional potential recovers the actual axial profile.

theorem NavierStokes.NaturalCore.coreVelocity_angular {h Λ : ℝ} {f V : ℝ × ℝ → ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hf : ContDiffOn ℝ (↑⊤) f (NaturalProfile.domain Λ)) (hV : ContDiffOn ℝ (↑⊤) V (NaturalProfile.domain Λ)) {t : ℝ} {x : ProblemStatement.Space} (hx : (t, x) ∈ coreDomain h Λ) : x.ofLp 0 * (coreVelocity h f V (t, x)).ofLp 1 - x.ofLp 1 * (coreVelocity h f V (t, x)).ofLp 0 = 2 * AxisymmetricFields.radialEnergy x * (physicalQ h (AxisymmetricFields.profilePoint t x) ^ (-h) / physicalQ h (AxisymmetricFields.profilePoint t x)) * f (similarityPoint h (AxisymmetricFields.profilePoint t x))

theorem NavierStokes.NaturalCore.scaled_sqrt_identity {q s : ℝ} (hq : 0 < q) (hs : 0 ≤ s) (h : ℝ) : √(2 * s) * (q ^ (-h) / q) = q ^ (-NaturalAxisData.A h) * √(2 * (s / q))

theorem NavierStokes.NaturalCore.coreVelocity_swirl {h Λ : ℝ} {f V : ℝ × ℝ → ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hf : ContDiffOn ℝ (↑⊤) f (NaturalProfile.domain Λ)) (hV : ContDiffOn ℝ (↑⊤) V (NaturalProfile.domain Λ)) {t : ℝ} {x : ProblemStatement.Space} (hx : (t, x) ∈ coreDomain h Λ) (hs : 0 < AxisymmetricFields.radialEnergy x) : (x.ofLp 0 * (coreVelocity h f V (t, x)).ofLp 1 - x.ofLp 1 * (coreVelocity h f V (t, x)).ofLp 0) / √(2 * AxisymmetricFields.radialEnergy x) = physicalQ h (AxisymmetricFields.profilePoint t x) ^ (-NaturalAxisData.A h) * √(2 * (similarityPoint h (AxisymmetricFields.profilePoint t x)).1) * f (similarityPoint h (AxisymmetricFields.profilePoint t x))

Away from the axis the cylindrical azimuthal velocity is precisely q^(-A) sqrt(2X) f(X,eta). The Cartesian field remains smooth on the axis.

theorem NavierStokes.NaturalCore.coreVelocity_at_origin {h j Λ : ℝ} {P0 a0 : ℝ → ℝ} {f U V Pr : ℝ × ℝ → ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a0 f U V Pr) {t : ℝ} (ht : t < 1) : coreVelocity h f V (t, 0) = ((1 - t) ^ (-NaturalAxisData.A h) * j) • ProblemStatement.coordinateVector 2

The axial velocity is exactly the prescribed nonzero axis datum, multiplied by the singular similarity scale.

theorem NavierStokes.NaturalCore.coreVelocity_norm_at_origin {h j Λ : ℝ} {P0 a0 : ℝ → ℝ} {f U V Pr : ℝ × ℝ → ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hj : 0 < j) (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a0 f U V Pr) {t : ℝ} (ht : t < 1) : ‖coreVelocity h f V (t, 0)‖ = (1 - t) ^ (-NaturalAxisData.A h) * j

theorem NavierStokes.NaturalCore.coreVelocity_axis_tendsto_atTop {h j Λ : ℝ} {P0 a0 : ℝ → ℝ} {f U V Pr : ℝ × ℝ → ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hj : 0 < j) (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a0 f U V Pr) : Filter.Tendsto (fun (t : ℝ) => ‖coreVelocity h f V (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

theorem NavierStokes.NaturalCore.speedUnbounded_of_axis_tendsto {u : ProblemStatement.VelocityField} (hu : Filter.Tendsto (fun (t : ℝ) => ‖u (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : ProblemStatement.SpeedUnboundedAtOne u

theorem NavierStokes.NaturalCore.coreVelocity_speedUnbounded {h j Λ : ℝ} {P0 a0 : ℝ → ℝ} {f U V Pr : ℝ × ℝ → ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hj : 0 < j) (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a0 f U V Pr) : ProblemStatement.SpeedUnboundedAtOne (coreVelocity h f V)

theorem NavierStokes.NaturalCore.extension_speedUnbounded {h j Λ : ℝ} {P0 a0 : ℝ → ℝ} {f U V Pr : ℝ × ℝ → ℝ} {u : ProblemStatement.VelocityField} (hh : 0 < h) (hh1 : h < 1 / 2) (hj : 0 < j) (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a0 f U V Pr) (hagrees : ∀ᶠ (t : ℝ) in nhdsWithin 1 (Set.Iio 1), u (t, 0) = coreVelocity h f V (t, 0)) : ProblemStatement.SpeedUnboundedAtOne u

Any field which agrees with the core along the axis sufficiently near time one has the exact target's quantified unbounded-speed property.

theorem NavierStokes.NaturalCore.extension_on_core_speedUnbounded {h j Λ : ℝ} {P0 a0 : ℝ → ℝ} {f U V Pr : ℝ × ℝ → ℝ} {u : ProblemStatement.VelocityField} (hh : 0 < h) (hh1 : h < 1 / 2) (hj : 0 < j) (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a0 f U V Pr) (hagrees : Set.EqOn u (coreVelocity h f V) (coreDomain h Λ)) : ProblemStatement.SpeedUnboundedAtOne u

theorem NavierStokes.NaturalCore.exists_natural_core {h j : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) {g a : ℝ → ℝ} {cap B : ℝ} (hp : PressureDatum.Admissible g a cap) (hB : 2 ≤ B) (hg : ∀ y ≤ 0, g y = B ^ 2 * Real.exp (1 / 5 * y)) (ha : ∀ y ≤ 0, a y = 1) : ∃ (Λ : ℝ), 0 < Λ ∧ ∃ (f : ℝ × ℝ → ℝ) (V : ℝ × ℝ → ℝ), IsOpen (coreDomain h Λ) ∧ (∀ t < 1, (t, 0) ∈ coreDomain h Λ) ∧ ContDiffOn ℝ (↑⊤) (coreVelocity h f V) (coreDomain h Λ) ∧ (∀ (t : ℝ) (x : ProblemStatement.Space), (t, x) ∈ coreDomain h Λ → ProblemStatement.spatialDivergence (coreVelocity h f V) t x = 0) ∧ (∀ t < 1, coreVelocity h f V (t, 0) = ((1 - t) ^ (-NaturalAxisData.A h) * j) • ProblemStatement.coordinateVector 2) ∧ ProblemStatement.SpeedUnboundedAtOne (coreVelocity h f V)

The constructed natural profiles produce an actual smooth, divergence-free physical core with unbounded speed. This is a local core existence statement, not the existence of the final forced periodic flow.