Assembling the actual global slow coefficients and their common base

All coefficient extensions in this module are constructed from the coherent GlobalSlowProfiles sequence. One parameter window is fixed before any coefficient or derivative order is selected.

noncomputable def NavierStokes.AssembledSlowBase.commonWindow {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hI : Set.Icc (-1) 1 ⊆ S) : ParametricRadialExtension.ParameterWindow S

Common window, given by ParametricRadialExtension.parameterWindow s.domain.isOpen hI.

Equations

• NavierStokes.AssembledSlowBase.commonWindow s hI = NavierStokes.ParametricRadialExtension.parameterWindow ⋯ hI

noncomputable def NavierStokes.AssembledSlowBase.extendEven {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) (f : GlobalSlowProfiles.EvenProfile S) : GlobalSlowProfiles.Field

Extend even, given by ParametricRadialExtension.extension w f f.smooth (fun _ heta R => f.even heta R).

Equations

• NavierStokes.AssembledSlowBase.extendEven w f = NavierStokes.ParametricRadialExtension.extension w ↑f ⋯ ⋯

theorem NavierStokes.AssembledSlowBase.extendEven_contDiff {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) (f : GlobalSlowProfiles.EvenProfile S) : ContDiff ℝ (↑⊤) (extendEven w f)

theorem NavierStokes.AssembledSlowBase.extendEven_eq {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) (f : GlobalSlowProfiles.EvenProfile S) {p : ℝ × ℝ} (hX : 0 ≤ p.1) (heta : |p.2| ≤ w.inner) : extendEven w f p = GlobalSlowProfiles.xProfile f p

theorem NavierStokes.AssembledSlowBase.extendEven_pullback {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) (f : GlobalSlowProfiles.EvenProfile S) (R : ℝ) {eta : ℝ} (heta : |eta| ≤ w.inner) : extendEven w f (R ^ 2 / 2, eta) = ↑f (R, eta)

theorem NavierStokes.AssembledSlowBase.extendEven_germ {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) (f : GlobalSlowProfiles.EvenProfile S) {p : ℝ × ℝ} (hX : 0 < p.1) (heta : |p.2| < w.inner) : extendEven w f =ᶠ[nhds p] GlobalSlowProfiles.xProfile f

theorem NavierStokes.AssembledSlowBase.extendEven_right_jets {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) (f : GlobalSlowProfiles.EvenProfile S) (m : ℕ) {X eta : ℝ} (hX : 0 ≤ X) (heta : |eta| ≤ w.inner) : iteratedDeriv m (fun (Y : ℝ) => extendEven w f (Y, eta)) X = iteratedDerivWithin m (fun (Y : ℝ) => GlobalSlowProfiles.xProfile f (Y, eta)) (Set.Ici 0) X

theorem NavierStokes.AssembledSlowBase.extendEven_mixed_jets {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) (f : GlobalSlowProfiles.EvenProfile S) (m : ℕ) {p : ℝ × ℝ} (hp : p ∈ Set.Ici 0 ×ˢ Set.Ioo (-w.inner) w.inner) : iteratedFDeriv ℝ m (extendEven w f) p = iteratedFDerivWithin ℝ m (GlobalSlowProfiles.xProfile f) (Set.Ici 0 ×ˢ Set.Ioo (-w.inner) w.inner) p

theorem NavierStokes.AssembledSlowBase.extendEven_support {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) (f : GlobalSlowProfiles.EvenProfile S) {B : ℝ} (hB : 0 ≤ B) (hs : GlobalSlowProfiles.Exterior B S ↑f) : tsupport (extendEven w f) ⊆ Set.Icc (-1) (B ^ 2 / 2) ×ˢ Set.Icc (-w.outer) w.outer

noncomputable def NavierStokes.AssembledSlowBase.extendCoreZero {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) (r : ℝ) (f : GlobalSlowProfiles.EvenProfile S) (p : ℝ × ℝ) : ℝ

For a profile already zero on a fixed axis neighborhood, remove the unused negative-X extension without changing any physical value.

Equations

• NavierStokes.AssembledSlowBase.extendCoreZero w r f p = NavierStokes.TransportPrimitive.cutoff (r / 8) (r / 4) p.1 * NavierStokes.AssembledSlowBase.extendEven w f p

theorem NavierStokes.AssembledSlowBase.extendCoreZero_contDiff {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) (r : ℝ) (f : GlobalSlowProfiles.EvenProfile S) : ContDiff ℝ (↑⊤) (extendCoreZero w r f)

theorem NavierStokes.AssembledSlowBase.extendCoreZero_eq {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) {r : ℝ} (hr : 0 < r) (f : GlobalSlowProfiles.EvenProfile S) (hz : ∀ eta ∈ S, ∀ R ∈ Set.Icc 0 √r, ↑f (R, eta) = 0) {p : ℝ × ℝ} (hX : 0 ≤ p.1) (heta : |p.2| ≤ w.inner) : extendCoreZero w r f p = GlobalSlowProfiles.xProfile f p

theorem NavierStokes.AssembledSlowBase.extendCoreZero_zero_left {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) {r : ℝ} (hr : 0 < r) (f : GlobalSlowProfiles.EvenProfile S) {p : ℝ × ℝ} (hp : p.1 ≤ r / 8) : extendCoreZero w r f p = 0

theorem NavierStokes.AssembledSlowBase.extendCoreZero_zero_right {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) (r : ℝ) (f : GlobalSlowProfiles.EvenProfile S) {B : ℝ} (hB : 0 ≤ B) (hs : GlobalSlowProfiles.Exterior B S ↑f) {p : ℝ × ℝ} (hp : B ^ 2 / 2 ≤ p.1) : extendCoreZero w r f p = 0

theorem NavierStokes.AssembledSlowBase.extendCoreZero_zero_parameter {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) (r : ℝ) (f : GlobalSlowProfiles.EvenProfile S) {p : ℝ × ℝ} (hp : w.outer ≤ |p.2|) : extendCoreZero w r f p = 0

noncomputable def NavierStokes.AssembledSlowBase.extendedCoefficient {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hI : Set.Icc (-1) 1 ⊆ S) (n : ℕ) (i : Fin 4) : GlobalSlowProfiles.Field

Each entry is an extension of the actual recursively repaired field.

Equations

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

theorem NavierStokes.AssembledSlowBase.extendedCoefficient_contDiff {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hI : Set.Icc (-1) 1 ⊆ S) (n : ℕ) (i : Fin 4) : ContDiff ℝ (↑⊤) (extendedCoefficient s hI n i)

theorem NavierStokes.AssembledSlowBase.extendedCoefficient_eq {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hI : Set.Icc (-1) 1 ⊆ S) (n : ℕ) (i : Fin 4) {p : ℝ × ℝ} (hX : 0 ≤ p.1) (heta : |p.2| ≤ 1) : extendedCoefficient s hI n i p = GlobalSlowProfiles.xProfile (GlobalSlowProfiles.component (GlobalSlowProfiles.profiles s n) i) p

theorem NavierStokes.AssembledSlowBase.extendedCoefficient_support {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hI : Set.Icc (-1) 1 ⊆ S) {n : ℕ} (hn : 0 < n) (i : Fin 4) : tsupport (extendedCoefficient s hI n i) ⊆ Set.Icc (-1) (s.B ^ 2 / 2) ×ˢ Set.Icc (-(commonWindow s hI).outer) (commonWindow s hI).outer

theorem NavierStokes.AssembledSlowBase.extendedCoefficient_compactSupport {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hI : Set.Icc (-1) 1 ⊆ S) {n : ℕ} (hn : 0 < n) (i : Fin 4) : HasCompactSupport (extendedCoefficient s hI n i)

theorem NavierStokes.AssembledSlowBase.extendedCoefficient_zero_exterior {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hI : Set.Icc (-1) 1 ⊆ S) {n : ℕ} (hn : 0 < n) (i : Fin 4) {p : ℝ × ℝ} (hp : s.B ^ 2 / 2 ≤ p.1) : extendedCoefficient s hI n i p = 0

theorem NavierStokes.AssembledSlowBase.extendedCoefficient_inner {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (hI : Set.Icc (-1) 1 ⊆ S) {n : ℕ} (hn : 0 < n) (i : Fin 4) {p : ℝ × ℝ} (hX : 0 ≤ p.1) (hi : p.1 < inner) (heta : |p.2| ≤ 1) : extendedCoefficient s hI n i p = SlowRecursion.profile (A.coefficients n (GlobalSlowProfiles.localIndex i)) p

theorem NavierStokes.AssembledSlowBase.extendedCoefficient_axis {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (hI : Set.Icc (-1) 1 ⊆ S) {n : ℕ} (hn : 0 < n) (i : Fin 4) {eta : ℝ} (heta : |eta| ≤ 1) : extendedCoefficient s hI n i (0, eta) = 0

theorem NavierStokes.AssembledSlowBase.extendedCoefficient_axis_jets {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (hI : Set.Icc (-1) 1 ⊆ S) {n : ℕ} (hn : 0 < n) (i : Fin 4) (m : ℕ) {eta : ℝ} (heta : |eta| ≤ 1) : iteratedDeriv m (fun (X : ℝ) => extendedCoefficient s hI n i (X, eta)) 0 = iteratedDerivWithin m (fun (X : ℝ) => SlowRecursion.profile (A.coefficients n (GlobalSlowProfiles.localIndex i)) (X, eta)) (Set.Ici 0) 0

noncomputable def NavierStokes.AssembledSlowBase.radialPullback {S : Set ℝ} {D : Set (ℝ × ℝ)} (F : GlobalSlowProfiles.Field) (hF : ContDiffOn ℝ (↑⊤) F D) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D) : GlobalSlowProfiles.EvenProfile S

A profile smooth on a neighborhood of the nonnegative X half-plane gives a genuine globally signed-radius even field by polynomial pullback.

Equations

• NavierStokes.AssembledSlowBase.radialPullback F hF hD = ⟨fun (w : ℝ × ℝ) => F (w.1 ^ 2 / 2, w.2), ⋯⟩

theorem NavierStokes.AssembledSlowBase.radialPullback_xProfile {S : Set ℝ} {D : Set (ℝ × ℝ)} (F : GlobalSlowProfiles.Field) (hF : ContDiffOn ℝ (↑⊤) F D) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D) {p : ℝ × ℝ} (hX : 0 ≤ p.1) : GlobalSlowProfiles.xProfile (radialPullback F hF hD) p = F p

theorem NavierStokes.AssembledSlowBase.coefficient_smoothAt {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (n : ℕ) {w : ℝ × ℝ} (hX : 0 < w.1) (heta : w.2 ∈ S) : ContDiffAt ℝ (↑⊤) (SlowExpansionResidual.angularCoefficient h (GlobalSlowProfiles.asSlowProfiles s) n) w ∧ ContDiffAt ℝ (↑⊤) (SlowExpansionResidual.axialCoefficient h (GlobalSlowProfiles.asSlowProfiles s) n) w

theorem NavierStokes.AssembledSlowBase.weightedRadius_smooth {S : Set ℝ} (hS : IsOpen S) {r : ℝ} (hr : 0 < r) {F : GlobalSlowProfiles.Field} (hF : ∀ (w : ℝ × ℝ), 0 < w.1 → w.2 ∈ S → ContDiffAt ℝ (↑⊤) F w) (hz : ∀ (w : ℝ × ℝ), 0 < w.1 → w.1 < r → w.2 ∈ S → F w = 0) {m : ℕ} (hm : m ≠ 0) : GlobalSlowProfiles.Smooth S fun (w : ℝ × ℝ) => w.1 ^ m * F (w.1 ^ 2 / 2, w.2)

A positive radial weight removes the irrelevant value of a coefficient at X=0. Vanishing on a genuine core then gives joint smoothness there.

structure NavierStokes.AssembledSlowBase.ZeroOrderSolved {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (r : ℝ) : Prop

The remaining finite order-zero input. Positive-order equations are proved by GlobalSlowProfiles and are not fields of this proposition.

• angular (w : SimilarityProfile.InnerPoint) : 0 < w.1 → w.1 < r → w.2 ∈ S → SlowExpansionResidual.angularCoefficient h (GlobalSlowProfiles.asSlowProfiles s) 0 w = 0
• axial (w : SimilarityProfile.InnerPoint) : 0 < w.1 → w.1 < r → w.2 ∈ S → SlowExpansionResidual.axialCoefficient h (GlobalSlowProfiles.asSlowProfiles s) 0 w = 0

theorem NavierStokes.AssembledSlowBase.coefficients_zero_inner {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (n : ℕ) {w : ℝ × ℝ} (hX : 0 < w.1) (hi : w.1 < inner) (heta : w.2 ∈ S) : SlowExpansionResidual.angularCoefficient h (GlobalSlowProfiles.asSlowProfiles s) n w = 0 ∧ SlowExpansionResidual.axialCoefficient h (GlobalSlowProfiles.asSlowProfiles s) n w = 0

theorem NavierStokes.AssembledSlowBase.thetaDensity_smooth {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (n : ℕ) : GlobalSlowProfiles.Smooth S (SlowResidualMatching.thetaDensity h C (GlobalSlowProfiles.asSlowProfiles s) n)

theorem NavierStokes.AssembledSlowBase.zDensity_smooth {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (n : ℕ) : GlobalSlowProfiles.Smooth S (SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) n)

theorem NavierStokes.AssembledSlowBase.densities_zero_inner {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (n : ℕ) {R eta : ℝ} (hR : R ∈ Set.Icc 0 √inner) (heta : eta ∈ S) : SlowResidualMatching.thetaDensity h C (GlobalSlowProfiles.asSlowProfiles s) n (R, eta) = 0 ∧ SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) n (R, eta) = 0

noncomputable def NavierStokes.AssembledSlowBase.thetaEven {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (n : ℕ) : GlobalSlowProfiles.EvenProfile S

Theta even, constructed using evenCorrection.

Equations

• NavierStokes.AssembledSlowBase.thetaEven L B0 Z0 n = NavierStokes.GlobalSlowProfiles.evenCorrection ⋯

noncomputable def NavierStokes.AssembledSlowBase.zEven {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (n : ℕ) : GlobalSlowProfiles.EvenProfile S

Z even, constructed using evenCorrection.

Equations

• NavierStokes.AssembledSlowBase.zEven L B0 Z0 n = NavierStokes.GlobalSlowProfiles.evenCorrection ⋯

theorem NavierStokes.AssembledSlowBase.thetaEven_eq {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (n : ℕ) {R eta : ℝ} (hR : 0 ≤ R) : ↑(thetaEven L B0 Z0 n) (R, eta) = SlowStressSupport.stress 2 (SlowResidualMatching.thetaDensity h C (GlobalSlowProfiles.asSlowProfiles s) n) (R, eta)

theorem NavierStokes.AssembledSlowBase.zEven_eq {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (n : ℕ) {R eta : ℝ} (hR : 0 ≤ R) : ↑(zEven L B0 Z0 n) (R, eta) = SlowStressSupport.stress 1 (SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) n) (R, eta)

theorem NavierStokes.AssembledSlowBase.thetaEven_zero {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (n : ℕ) {R eta : ℝ} (hR : R ∈ Set.Icc 0 √inner) (heta : eta ∈ S) : ↑(thetaEven L B0 Z0 n) (R, eta) = 0

theorem NavierStokes.AssembledSlowBase.zEven_zero {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (n : ℕ) {R eta : ℝ} (hR : R ∈ Set.Icc 0 √inner) (heta : eta ∈ S) : ↑(zEven L B0 Z0 n) (R, eta) = 0

noncomputable def NavierStokes.AssembledSlowBase.coefficients {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) : SlowBorelBase.Coefficients

Coefficients, bundling axial, phi, pressure, stressTheta and the required compatibility proofs.

Equations

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

theorem NavierStokes.AssembledSlowBase.coefficients_smooth {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) : SlowBorelBase.SmoothCoefficients (coefficients L B0 Z0 hI)

theorem NavierStokes.AssembledSlowBase.coefficients_fields_eq {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) (n : ℕ) {p : ℝ × ℝ} (hX : 0 ≤ p.1) (heta : |p.2| ≤ 1) : (coefficients L B0 Z0 hI).phi n p = (GlobalSlowProfiles.asSlowProfiles s).phi n p ∧ (coefficients L B0 Z0 hI).axial n p = (GlobalSlowProfiles.asSlowProfiles s).axial n p ∧ (coefficients L B0 Z0 hI).pressure n p = (GlobalSlowProfiles.asSlowProfiles s).pressure n p

theorem NavierStokes.AssembledSlowBase.coefficients_fields_germ {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) (n : ℕ) {p : ℝ × ℝ} (hX : 0 < p.1) (heta : |p.2| ≤ 1) : (coefficients L B0 Z0 hI).phi n =ᶠ[nhds p] (GlobalSlowProfiles.asSlowProfiles s).phi n ∧ (coefficients L B0 Z0 hI).axial n =ᶠ[nhds p] (GlobalSlowProfiles.asSlowProfiles s).axial n ∧ (coefficients L B0 Z0 hI).pressure n =ᶠ[nhds p] (GlobalSlowProfiles.asSlowProfiles s).pressure n

theorem NavierStokes.AssembledSlowBase.coefficients_stress_eq {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) (n : ℕ) {w : ℝ × ℝ} (hX : 0 ≤ w.1) (heta : |w.2| ≤ 1) : (coefficients L B0 Z0 hI).stressTheta n w = SlowResidualMatching.thetaStress h C (GlobalSlowProfiles.asSlowProfiles s) n w ∧ (coefficients L B0 Z0 hI).stressAxial n w = SlowResidualMatching.zStress h (GlobalSlowProfiles.asSlowProfiles s) n w

theorem NavierStokes.AssembledSlowBase.coefficients_stress_zero_left {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) (n : ℕ) {w : ℝ × ℝ} (hw : w.1 ≤ inner / 8) : (coefficients L B0 Z0 hI).stressTheta n w = 0 ∧ (coefficients L B0 Z0 hI).stressAxial n w = 0

theorem NavierStokes.AssembledSlowBase.coefficients_stress_zero_right {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) (n : ℕ) {B : ℝ} (hB : 0 ≤ B) (hTheta : GlobalSlowProfiles.Exterior B S (SlowStressSupport.stress 2 (SlowResidualMatching.thetaDensity h C (GlobalSlowProfiles.asSlowProfiles s) n))) (hZ : GlobalSlowProfiles.Exterior B S (SlowStressSupport.stress 1 (SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) n))) {w : ℝ × ℝ} (hw : B ^ 2 / 2 ≤ w.1) : (coefficients L B0 Z0 hI).stressTheta n w = 0 ∧ (coefficients L B0 Z0 hI).stressAxial n w = 0

theorem NavierStokes.AssembledSlowBase.coefficients_stress_zero_parameter {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) (n : ℕ) {w : ℝ × ℝ} (hw : (commonWindow s hI).outer ≤ |w.2|) : (coefficients L B0 Z0 hI).stressTheta n w = 0 ∧ (coefficients L B0 Z0 hI).stressAxial n w = 0

theorem NavierStokes.AssembledSlowBase.coefficients_stress_support {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) (n : ℕ) {B : ℝ} (hB : 0 ≤ B) (hTheta : GlobalSlowProfiles.Exterior B S (SlowStressSupport.stress 2 (SlowResidualMatching.thetaDensity h C (GlobalSlowProfiles.asSlowProfiles s) n))) (hZ : GlobalSlowProfiles.Exterior B S (SlowStressSupport.stress 1 (SlowResidualMatching.zDensity h (GlobalSlowProfiles.asSlowProfiles s) n))) : (tsupport fun (w : SlowBorelBase.Inner) => ((coefficients L B0 Z0 hI).stressTheta n w, (coefficients L B0 Z0 hI).stressAxial n w)) ⊆ Set.Icc (inner / 8) (B ^ 2 / 2) ×ˢ Set.Icc (-(commonWindow s hI).outer) (commonWindow s hI).outer

theorem NavierStokes.AssembledSlowBase.coefficients_stress_zero {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) (n : ℕ) {w : ℝ × ℝ} (hX : 0 ≤ w.1) (hi : w.1 ≤ inner / 2) (heta : |w.2| ≤ 1) : (coefficients L B0 Z0 hI).stressTheta n w = 0 ∧ (coefficients L B0 Z0 hI).stressAxial n w = 0

theorem NavierStokes.AssembledSlowBase.coefficients_common_zero_core {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) : ∃ (r : ℝ), 0 < r ∧ ∀ (n : ℕ), ∀ X ∈ Set.Ico 0 r, ∀ eta ∈ Set.Icc (-1) 1, (coefficients L B0 Z0 hI).stressTheta n (X, eta) = 0 ∧ (coefficients L B0 Z0 hI).stressAxial n (X, eta) = 0

theorem NavierStokes.AssembledSlowBase.exists_assembled_base {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : GlobalSlowProfiles.Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : GlobalSlowProfiles.Localization s A inner) (B0 : GlobalSlowProfiles.BaseAgreement s A inner) (Z0 : ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) (hh : 0 < h) (hh1 : h < 1 / 2) (lo hi : ℝ) (N : ℕ) : ∃ (a : ℕ → ℕ), N ≤ a 0 ∧ SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C (coefficients L B0 Z0 hI)) (SlowBorelBase.innerBox lo hi) a ∧ ContDiffOn ℝ (↑⊤) (SlowBorelBase.baseVelocity a h C (coefficients L B0 Z0 hI)) (Set.Iio 1 ×ˢ Set.univ) ∧ ∀ t < 1, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence (SlowBorelBase.baseVelocity a h C (coefficients L B0 Z0 hI)) t x = 0

One actual coefficient family gives one schedule and one smooth divergence-free physical base. No scale bounds are supplied as hypotheses.

theorem NavierStokes.AssembledSlowBase.massHistory_extendEven {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) (u : GlobalSlowProfiles.EvenProfile S) {R eta : ℝ} (hR : 0 ≤ R) (heta : |eta| ≤ w.inner) : PositiveOrderMoments.massHistory ↑u (R, eta) = ProfileHistories.primitive (extendEven w u) (R ^ 2 / 2, eta)

theorem NavierStokes.AssembledSlowBase.parameterMassHistory_extendEven {S : Set ℝ} (hS : IsOpen S) (w : ParametricRadialExtension.ParameterWindow S) (u : GlobalSlowProfiles.EvenProfile S) {R eta : ℝ} (hR : 0 ≤ R) (heta : |eta| < w.inner) : PositiveOrderMoments.parameterMassHistory ↑u (R, eta) = ProfileHistories.primitive (ProfileHistories.parameterPartial (extendEven w u)) (R ^ 2 / 2, eta)

theorem NavierStokes.AssembledSlowBase.fluxHistory_extendEven {S : Set ℝ} {h : ℝ} (d : GlobalSlowProfiles.Domain S h) (w : ParametricRadialExtension.ParameterWindow S) (lam : ℝ) (u : GlobalSlowProfiles.EvenProfile S) {R eta : ℝ} (hR : 0 ≤ R) (heta : |eta| < w.inner) : PositiveOrderMoments.fluxHistory h lam ↑u (R, eta) = SlowDivergence.radialFlux h lam (extendEven w u) (R ^ 2 / 2, eta)

theorem NavierStokes.AssembledSlowBase.betaFromU_extended {S : Set ℝ} {h : ℝ} (d : GlobalSlowProfiles.Domain S h) (w : ParametricRadialExtension.ParameterWindow S) (lam : ℝ) (u : GlobalSlowProfiles.EvenProfile S) {p : ℝ × ℝ} (hX : 0 ≤ p.1) (heta : |p.2| < w.inner) : p.1 * extendEven w (GlobalSlowProfiles.betaFromU d lam u) p = SlowDivergence.radialFlux h lam (extendEven w u) p

The extended regular quotient is the actual radial flux of the extended axial coefficient. The identity includes X=0.

theorem NavierStokes.AssembledSlowBase.extended_flux {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hI : Set.Icc (-1) 1 ⊆ S) {n : ℕ} (hn : 0 < n) {p : ℝ × ℝ} (hX : 0 ≤ p.1) (heta : |p.2| ≤ 1) : p.1 * extendedCoefficient s hI n 2 p = SlowDivergence.radialFlux h (AxisSourceRegularity.slowOrder h n) (extendedCoefficient s hI n 1) p

theorem NavierStokes.AssembledSlowBase.extended_flux_zero {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hI : Set.Icc (-1) 1 ⊆ S) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) {p : ℝ × ℝ} (hX : 0 ≤ p.1) (heta : |p.2| ≤ 1) : p.1 * extendedCoefficient s hI 0 2 p = SlowDivergence.radialFlux h 0 (extendedCoefficient s hI 0 1) p

theorem NavierStokes.AssembledSlowBase.extended_axial_primitive_zero {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hI : Set.Icc (-1) 1 ⊆ S) {n : ℕ} (hn : 0 < n) {p : ℝ × ℝ} (hX : s.B ^ 2 / 2 ≤ p.1) (heta : |p.2| ≤ 1) : ProfileHistories.primitive (extendedCoefficient s hI n 1) p = 0

The repaired mass row makes the actual positive-order stream primitive zero outside the common support radius.

theorem NavierStokes.AssembledSlowBase.extended_axial_average_zero {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hI : Set.Icc (-1) 1 ⊆ S) {n : ℕ} (hn : 0 < n) {p : ℝ × ℝ} (hX : s.B ^ 2 / 2 ≤ p.1) (heta : |p.2| ≤ 1) : ProfileHistories.average (extendedCoefficient s hI n 1) p = 0

noncomputable def NavierStokes.AssembledSlowBase.baseFields {S : Set ℝ} {h : ℝ} {D : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (C : ℝ) (P : ProfileHistories.Profiles D) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier) : GlobalSlowProfiles.Coefficient S

The four order-zero fields are computed from one actual profile. In particular beta is reconstructed from U; it is not independent data.

Equations

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

theorem NavierStokes.AssembledSlowBase.baseFields_phi {S : Set ℝ} {h : ℝ} {D : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (C : ℝ) (P : ProfileHistories.Profiles D) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier) {p : ℝ × ℝ} (hX : 0 ≤ p.1) : GlobalSlowProfiles.xProfile (baseFields d C P hD).phi p = C * P.f p

theorem NavierStokes.AssembledSlowBase.baseFields_axial {S : Set ℝ} {h : ℝ} {D : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (C : ℝ) (P : ProfileHistories.Profiles D) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier) {p : ℝ × ℝ} (hX : 0 ≤ p.1) : GlobalSlowProfiles.xProfile (baseFields d C P hD).axial p = P.U p

theorem NavierStokes.AssembledSlowBase.baseFields_pressure {S : Set ℝ} {h : ℝ} {D : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (C : ℝ) (P : ProfileHistories.Profiles D) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier) {p : ℝ × ℝ} (hX : 0 ≤ p.1) : GlobalSlowProfiles.xProfile (baseFields d C P hD).pressure p = P.pressure p

theorem NavierStokes.AssembledSlowBase.baseFields_angular {S : Set ℝ} {h : ℝ} {D : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (C : ℝ) (P : ProfileHistories.Profiles D) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier) (hC : C ≠ 0) {R eta : ℝ} (hR : 0 ≤ R) : GlobalSlowProfiles.angularField C (baseFields d C P hD).phi (R, eta) = P.E (R ^ 2 / 2, eta)

theorem NavierStokes.AssembledSlowBase.baseFields_mass {S : Set ℝ} {h : ℝ} {D : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (C : ℝ) (P : ProfileHistories.Profiles D) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier) {R eta : ℝ} (hR : 0 ≤ R) (heta : eta ∈ S) : PositiveOrderMoments.massHistory ↑(baseFields d C P hD).axial (R, eta) = P.M (R ^ 2 / 2, eta)

theorem NavierStokes.AssembledSlowBase.baseFields_parameterMass {S : Set ℝ} {h : ℝ} {D : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (C : ℝ) (P : ProfileHistories.Profiles D) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier) {R eta : ℝ} (hR : 0 ≤ R) (heta : eta ∈ S) : PositiveOrderMoments.parameterMassHistory ↑(baseFields d C P hD).axial (R, eta) = ProfileHistories.primitive (ProfileHistories.parameterPartial P.U) (R ^ 2 / 2, eta)

theorem NavierStokes.AssembledSlowBase.baseFields_beta_flux {S : Set ℝ} {h : ℝ} {D : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (C : ℝ) (P : ProfileHistories.Profiles D) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier) {R eta : ℝ} (hR : 0 ≤ R) (heta : eta ∈ S) : R ^ 2 / 2 * ↑(baseFields d C P hD).beta (R, eta) = SlowDivergence.radialFlux h 0 P.U (R ^ 2 / 2, eta)

theorem NavierStokes.AssembledSlowBase.baseFields_beta_value {S : Set ℝ} {h : ℝ} {D : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (C : ℝ) (P : ProfileHistories.Profiles D) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier) {p : ℝ × ℝ} (hX : 0 < p.1) (heta : p.2 ∈ S) : GlobalSlowProfiles.xProfile (baseFields d C P hD).beta p = SlowDivergence.radialFlux h 0 P.U p / p.1

theorem NavierStokes.AssembledSlowBase.baseFields_axial_exterior {S : Set ℝ} {h : ℝ} {D : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (C : ℝ) (P : ProfileHistories.Profiles D) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier) {B : ℝ} (hB : 0 ≤ B) (hu : ∀ eta ∈ S, ∀ (X : ℝ), B ^ 2 / 2 ≤ X → P.U (X, eta) = 0) : GlobalSlowProfiles.Exterior B S ↑(baseFields d C P hD).axial

theorem NavierStokes.AssembledSlowBase.baseFields_beta_exterior {S : Set ℝ} {h : ℝ} {D : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (C : ℝ) (P : ProfileHistories.Profiles D) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier) {B : ℝ} (hB : 0 < B) (hu : ∀ eta ∈ S, ∀ (X : ℝ), B ^ 2 / 2 ≤ X → P.U (X, eta) = 0) (hm : ∀ eta ∈ S, P.M (B ^ 2 / 2, eta) = 0) : GlobalSlowProfiles.Exterior B S ↑(baseFields d C P hD).beta

noncomputable def NavierStokes.AssembledSlowBase.baseDataOfProfile {S : Set ℝ} {h : ℝ} {D : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (C : ℝ) (P : ProfileHistories.Profiles D) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier) {lam a b B : ℝ} (hC : C ≠ 0) (ha : 0 ≤ a) (hB : 0 < B) (hu : ∀ eta ∈ S, ∀ (X : ℝ), B ^ 2 / 2 ≤ X → P.U (X, eta) = 0) (hm : ∀ eta ∈ S, P.M (B ^ 2 / 2, eta) = 0) (amplitude : ℝ → ℝ) (hs : ContDiffOn ℝ (↑⊤) amplitude S) (hne : ∀ eta ∈ S, amplitude eta ≠ 0) (hup : ∀ eta ∈ S, ∀ R ∈ Set.Ioo a b, P.U (R ^ 2 / 2, eta) = 0) (hep : ∀ eta ∈ S, ∀ R ∈ Set.Ioo a b, P.E (R ^ 2 / 2, eta) = FiveRowRank.background lam (amplitude eta) R) : GlobalSlowProfiles.BaseData S C lam a b B

Finite exterior and pure-power facts suffice to construct the input record for the actual infinite repair recursion.

Equations

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

theorem NavierStokes.AssembledSlowBase.local_average_eq {S : Set ℝ} {r : ℝ} {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (hu : Set.EqOn P.U Q.U (Set.Ico 0 r ×ˢ S)) {p : ℝ × ℝ} (hp : p ∈ Set.Ico 0 r ×ˢ S) : P.Ubar p = Q.Ubar p

theorem NavierStokes.AssembledSlowBase.local_flux_eq {S : Set ℝ} {h r : ℝ} {D D' : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (hu : Set.EqOn P.U Q.U (Set.Ico 0 r ×ˢ S)) {p : ℝ × ℝ} (hX : 0 < p.1) (hi : p.1 < r) (heta : p.2 ∈ S) : SlowDivergence.radialFlux h 0 P.U p = SlowDivergence.radialFlux h 0 Q.U p

theorem NavierStokes.AssembledSlowBase.local_beta_eq_pos {S : Set ℝ} {h C r : ℝ} {D D' : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (hP : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier) (hQ : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D'.carrier) (hu : Set.EqOn P.U Q.U (Set.Ico 0 r ×ˢ S)) {p : ℝ × ℝ} (hX : 0 < p.1) (hi : p.1 < r) (heta : p.2 ∈ S) : GlobalSlowProfiles.xProfile (baseFields d C P hP).beta p = GlobalSlowProfiles.xProfile (baseFields d C Q hQ).beta p

theorem NavierStokes.AssembledSlowBase.local_beta_eq_axis {S : Set ℝ} {h C r : ℝ} {D D' : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (hP : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier) (hQ : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D'.carrier) (hr : 0 < r) (hu : Set.EqOn P.U Q.U (Set.Ico 0 r ×ˢ S)) {eta : ℝ} (heta : eta ∈ S) : ↑(baseFields d C P hP).beta (0, eta) = ↑(baseFields d C Q hQ).beta (0, eta)

theorem NavierStokes.AssembledSlowBase.baseFields_local_eq {S : Set ℝ} {h C r : ℝ} {D D' : ProfileHistories.RadialDomain} (d : GlobalSlowProfiles.Domain S h) (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (hP : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier) (hQ : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D'.carrier) (hr : 0 < r) (h0 : P.pressure0 = Q.pressure0) (hf : Set.EqOn P.f Q.f (Set.Ico 0 r ×ˢ S)) (hu : Set.EqOn P.U Q.U (Set.Ico 0 r ×ˢ S)) (i : Fin 4) {p : ℝ × ℝ} (hp : p ∈ Set.Ico 0 r ×ˢ S) : GlobalSlowProfiles.xProfile (GlobalSlowProfiles.component (baseFields d C P hP) i) p = GlobalSlowProfiles.xProfile (GlobalSlowProfiles.component (baseFields d C Q hQ) i) p

Local edits do not change any base field on the smaller core. The pressure and beta conclusions are derived from actual integrals and germs.

noncomputable def NavierStokes.AssembledSlowBase.nominalOuterX {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : ℝ

Nominal outer X, constructed using max.

Equations

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

noncomputable def NavierStokes.AssembledSlowBase.nominalOuterRadius {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : ℝ

Nominal outer radius, given by Real.sqrt (2 * nominalOuterX W).

Equations

• NavierStokes.AssembledSlowBase.nominalOuterRadius W = √(2 * NavierStokes.AssembledSlowBase.nominalOuterX W)

theorem NavierStokes.AssembledSlowBase.nominalOuterX_gt_radius {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : W.controls.radius < nominalOuterX W

theorem NavierStokes.AssembledSlowBase.nominalOuterX_pos {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : 0 < nominalOuterX W

theorem NavierStokes.AssembledSlowBase.nominalOuterX_gt_pulse {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : OutgoingDilation.pulseEndRadius F W.controls.radius < nominalOuterX W

theorem NavierStokes.AssembledSlowBase.nominalOuterX_gt_patch {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : ReservedPatches.right F W.controls.radius ReservedPatches.Slot.positive < nominalOuterX W

theorem NavierStokes.AssembledSlowBase.nominalOuterRadius_pos {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : 0 < nominalOuterRadius W

theorem NavierStokes.AssembledSlowBase.nominalOuterRadius_square {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : nominalOuterRadius W ^ 2 / 2 = nominalOuterX W

theorem NavierStokes.AssembledSlowBase.nominal_patch_before_outer {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : ReservedPatches.radialRight F W.controls.radius ReservedPatches.Slot.positive < nominalOuterRadius W

theorem NavierStokes.AssembledSlowBase.nominal_pulse_gt_radius {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : W.controls.radius < OutgoingDilation.pulseEndRadius F W.controls.radius

theorem NavierStokes.AssembledSlowBase.nominalOuterX_eq_pulse {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : nominalOuterX W = OutgoingDilation.pulseEndRadius F W.controls.radius + 1

theorem NavierStokes.AssembledSlowBase.nominalOuterX_lt_switch {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : nominalOuterX W < OutgoingDilation.switchRadius F W.controls.radius

The common higher-order support radius is strictly inside the later heat switch and hence before the order-one terminal collar.

theorem NavierStokes.AssembledSlowBase.matching_before_window {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (slot : ReservedPatches.Slot) {X : ℝ} (hX : X ∈ ReservedPatches.window F W.controls.radius slot) : W.controls.radius < X

theorem NavierStokes.AssembledSlowBase.nominal_positive_patch {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {R eta : ℝ} (hR : R ∈ ReservedPatches.radialWindow F W.controls.radius ReservedPatches.Slot.positive) : W.U (R ^ 2 / 2, eta) = 0 ∧ W.E (R ^ 2 / 2, eta) = FiveRowRank.background F.data.core.lam (ReservedPatches.radialAmplitude F W.controls.radius eta) R

theorem NavierStokes.AssembledSlowBase.nominal_axial_exterior {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {S : Set ℝ} (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ W.domain.carrier) (eta : ℝ) : eta ∈ S → ∀ (X : ℝ), nominalOuterRadius W ^ 2 / 2 ≤ X → W.profiles.U (X, eta) = 0

theorem NavierStokes.AssembledSlowBase.nominal_mass_exterior {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {S : Set ℝ} (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ W.domain.carrier) (eta : ℝ) : eta ∈ S → W.profiles.M (nominalOuterRadius W ^ 2 / 2, eta) = 0

noncomputable def NavierStokes.AssembledSlowBase.nominalBaseData {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {S : Set ℝ} (d : GlobalSlowProfiles.Domain S F.data.h) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ W.domain.carrier) : GlobalSlowProfiles.BaseData S W.axis.normalization F.data.core.lam (ReservedPatches.radialLeft F W.controls.radius ReservedPatches.Slot.positive) (ReservedPatches.radialRight F W.controls.radius ReservedPatches.Slot.positive) (nominalOuterRadius W)

A finite base input constructed from the same nominal witness, with the manuscript's reserved positive-order patch.

Equations

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

theorem NavierStokes.AssembledSlowBase.nominalBaseData_beta {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {S : Set ℝ} (d : GlobalSlowProfiles.Domain S F.data.h) (hD : ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ W.domain.carrier) : (nominalBaseData W d hD).fields.beta = GlobalSlowProfiles.betaFromU d 0 (nominalBaseData W d hD).fields.axial

theorem NavierStokes.AssembledSlowBase.nominalPressure_eq {F : OutgoingProfile.Profile} : F.axisDatum = PressureDatum.pressure (SchedulePressure.clockWeight F.data) (SchedulePressure.shapeExponent F.data)

noncomputable def NavierStokes.AssembledSlowBase.nominalTube {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : ActivationHolomorphic.InitialTube (ReferenceJetBounds.referenceInput W.axis.natural.profile ⋯) F.data.h F.axisDatum (5 / W.axis.scale) (AxisHolomorphic.parameterTube ActivationHolomorphic.parameterWindow (ActualSlowAxis.tubeWidth ⋯ ⋯ W.axis.natural.profile ⋯ ⋯ ⋯))

Nominal tube, constructed using ActualSlowAxis.constructedTube.

Equations

• NavierStokes.AssembledSlowBase.nominalTube W = NavierStokes.ActualSlowAxis.constructedTube ⋯ ⋯ W.axis.natural.profile ⋯ ⋯ ⋯

noncomputable def NavierStokes.AssembledSlowBase.nominalComplexDomain {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : Set ℂ

Nominal complex domain, constructed using ActualSlowAxis.parameterDomain.

Equations

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

theorem NavierStokes.AssembledSlowBase.nominalComplexDomain_open {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : IsOpen (nominalComplexDomain W)

noncomputable def NavierStokes.AssembledSlowBase.nominalHierarchy {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : SlowRecursion.LocalHierarchy (ActualSlowAxis.axisRadius (ReferenceJetBounds.referenceInput W.axis.natural.profile ⋯) W.controls.referenceWidth) (ActualSlowAxis.parameterDomain (AxisHolomorphic.parameterTube ActivationHolomorphic.parameterWindow (ActualSlowAxis.tubeWidth ⋯ ⋯ W.axis.natural.profile ⋯ ⋯ ⋯))) F.data.h W.axis.normalization fun (i : Fin 5) => SlowRecursion.profile (ActualSlowAxis.base (nominalTube W) ⋯ ⋯ ⋯ W.controls.kappa ⋯ W.axis.normalization ⋯ i)

Nominal hierarchy, constructed using ActualSlowAxis.hierarchy.

Equations

• NavierStokes.AssembledSlowBase.nominalHierarchy W = NavierStokes.ActualSlowAxis.hierarchy (NavierStokes.AssembledSlowBase.nominalTube W) ⋯ ⋯ ⋯ W.controls.kappa ⋯ W.axis.normalization

noncomputable def NavierStokes.AssembledSlowBase.nominalRadius {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : ℝ

Nominal radius, given by ActualSlowAxis.axisRadius W.axis.referenceInput W.controls.referenceWidth.

Equations

• NavierStokes.AssembledSlowBase.nominalRadius W = NavierStokes.ActualSlowAxis.axisRadius W.axis.referenceInput W.controls.referenceWidth

noncomputable def NavierStokes.AssembledSlowBase.nominalParameters {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : Set ℝ

One open parameter set serves the nominal fields and every order of the same analytic local hierarchy.

Equations

• NavierStokes.AssembledSlowBase.nominalParameters W = {eta : ℝ | (0, eta) ∈ W.domain.carrier} ∩ Complex.ofReal ⁻¹' NavierStokes.AssembledSlowBase.nominalComplexDomain W

theorem NavierStokes.AssembledSlowBase.nominalParameters_open {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : IsOpen (nominalParameters W)

theorem NavierStokes.AssembledSlowBase.nominalParameters_contains {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : Set.Icc (-1) 1 ⊆ nominalParameters W

theorem NavierStokes.AssembledSlowBase.nominalParameters_domain {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (X : ℝ) (hX : 0 ≤ X) (eta : ℝ) (heta : eta ∈ nominalParameters W) : (X, eta) ∈ W.domain.carrier

theorem NavierStokes.AssembledSlowBase.nominalParameters_reference {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {eta : ℝ} (heta : eta ∈ nominalParameters W) : eta ∈ ReferencePath.parameterInterval

theorem NavierStokes.AssembledSlowBase.nominalDomain {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : GlobalSlowProfiles.Domain (nominalParameters W) F.data.h

noncomputable def NavierStokes.AssembledSlowBase.nominalInner {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : ℝ

Nominal inner, given by (4 / W.axis.scale) / 4.

Equations

• NavierStokes.AssembledSlowBase.nominalInner W = 4 / W.axis.scale / 4

noncomputable def NavierStokes.AssembledSlowBase.nominalStop {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : ℝ

Nominal stop, given by (4 / W.axis.scale) / 2.

Equations

• NavierStokes.AssembledSlowBase.nominalStop W = 4 / W.axis.scale / 2

theorem NavierStokes.AssembledSlowBase.nominalInner_pos {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : 0 < nominalInner W

theorem NavierStokes.AssembledSlowBase.nominalInner_lt_stop {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : nominalInner W < nominalStop W

theorem NavierStokes.AssembledSlowBase.nominalStop_lt_initial {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : nominalStop W < 4 / W.axis.scale

theorem NavierStokes.AssembledSlowBase.nominalInitial_le_collar {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : 4 / W.axis.scale ≤ 4 / W.axis.scale * Real.exp W.controls.referenceWidth

theorem NavierStokes.AssembledSlowBase.nominalStop_lt_radius {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : nominalStop W < nominalRadius W ^ 2

theorem NavierStokes.AssembledSlowBase.nominalStop_lt_patch {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : nominalStop W < ReservedPatches.radialLeft F W.controls.radius ReservedPatches.Slot.positive ^ 2 / 2

noncomputable def NavierStokes.AssembledSlowBase.nominalScheme {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : GlobalSlowProfiles.Scheme (nominalParameters W) F.data.h W.axis.normalization

The global recursive sequence uses the same nominal profile and the same constructed natural/ACT local hierarchy, with one common cutoff.

Equations

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

theorem NavierStokes.AssembledSlowBase.nominalLocalization {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : GlobalSlowProfiles.Localization (nominalScheme W) (nominalHierarchy W) (nominalInner W)

noncomputable def NavierStokes.AssembledSlowBase.nominalACT {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : ProfileHistories.Profiles W.axis.referenceInput.radialDomain

Nominal ACT, constructed using StressActivation.FromReference.histories.

Equations

• NavierStokes.AssembledSlowBase.nominalACT W = NavierStokes.StressActivation.FromReference.histories W.axis.referenceInput ⋯ ⋯ ⋯ W.controls.kappa F.axisDatum ⋯

theorem NavierStokes.AssembledSlowBase.nominalInitial_le_Xi {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : 4 / W.axis.scale ≤ NominalProfile.Xi

theorem NavierStokes.AssembledSlowBase.nominalACT_fields {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {X eta : ℝ} (hX : 0 ≤ X) (hi : X ≤ 4 / W.axis.scale) (heta : eta ∈ ReferencePath.parameterInterval) : W.profiles.f (X, eta) = (nominalACT W).f (X, eta) ∧ W.profiles.U (X, eta) = (nominalACT W).U (X, eta)

theorem NavierStokes.AssembledSlowBase.nominalACT_histories {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {X eta : ℝ} (hX : 0 ≤ X) (hi : X ≤ 4 / W.axis.scale) (heta : eta ∈ ReferencePath.parameterInterval) : W.profiles.Ubar (X, eta) = (nominalACT W).Ubar (X, eta) ∧ W.profiles.pressure (X, eta) = (nominalACT W).pressure (X, eta)

theorem NavierStokes.AssembledSlowBase.nominalACT_flux {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {X eta : ℝ} (hX : 0 < X) (hi : X < 4 / W.axis.scale) (heta : eta ∈ ReferencePath.parameterInterval) : SlowDivergence.radialFlux F.data.h 0 W.profiles.U (X, eta) = SlowDivergence.radialFlux F.data.h 0 (nominalACT W).U (X, eta)

theorem NavierStokes.AssembledSlowBase.nominalHierarchy_base {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {X eta : ℝ} (hX : 0 ≤ X) (hi : X < nominalInner W) (heta : eta ∈ nominalParameters W) : SlowRecursion.profile ((nominalHierarchy W).coefficients 0 0) (X, eta) = W.axis.normalization * W.profiles.f (X, eta) ∧ SlowRecursion.profile ((nominalHierarchy W).coefficients 0 1) (X, eta) = W.profiles.U (X, eta) ∧ SlowRecursion.profile ((nominalHierarchy W).coefficients 0 3) (X, eta) = W.profiles.pressure (X, eta)

theorem NavierStokes.AssembledSlowBase.nominalBase_beta_pos {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {X eta : ℝ} (hX : 0 < X) (hi : X < nominalInner W) (heta : eta ∈ nominalParameters W) : GlobalSlowProfiles.xProfile (nominalScheme W).base.beta (X, eta) = SlowRecursion.profile ((nominalHierarchy W).coefficients 0 4) (X, eta)

theorem NavierStokes.AssembledSlowBase.nominalBase_beta_axis {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {eta : ℝ} (heta : eta ∈ nominalParameters W) : ↑(nominalScheme W).base.beta (0, eta) = ↑(GlobalSlowProfiles.localExtension ⋯ 0 4) (0, eta)

theorem NavierStokes.AssembledSlowBase.nominalBaseAgreement {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : GlobalSlowProfiles.BaseAgreement (nominalScheme W) (nominalHierarchy W) (nominalInner W)

theorem NavierStokes.AssembledSlowBase.nominal_pressure_inner {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ℝ × ℝ} (hX : 0 ≤ p.1) (hi : p.1 < nominalInner W) (heta : p.2 ∈ nominalParameters W) : GlobalSlowProfiles.xProfile (nominalScheme W).base.pressure p = SlowRecursion.profile ((nominalHierarchy W).coefficients 0 3) p

theorem NavierStokes.AssembledSlowBase.nominal_zero_coefficients {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ℝ × ℝ} (hX : 0 < p.1) (hi : p.1 < nominalInner W) (heta : p.2 ∈ nominalParameters W) : SlowExpansionResidual.angularCoefficient F.data.h (GlobalSlowProfiles.asSlowProfiles (nominalScheme W)) 0 p = 0 ∧ SlowExpansionResidual.axialCoefficient F.data.h (GlobalSlowProfiles.asSlowProfiles (nominalScheme W)) 0 p = 0

theorem NavierStokes.AssembledSlowBase.nominalZeroOrder {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : ZeroOrderSolved (nominalScheme W) (nominalInner W)

noncomputable def NavierStokes.AssembledSlowBase.nominalCoefficients {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : SlowBorelBase.Coefficients

The complete smooth input family is constructed from the single nominal witness; there are no freely supplied repaired coefficient fields.

Equations

• NavierStokes.AssembledSlowBase.nominalCoefficients W = NavierStokes.AssembledSlowBase.coefficients ⋯ ⋯ ⋯ ⋯

theorem NavierStokes.AssembledSlowBase.nominalCoefficients_smooth {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : SlowBorelBase.SmoothCoefficients (nominalCoefficients W)

theorem NavierStokes.AssembledSlowBase.nominalCoefficients_zero_fields {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ℝ × ℝ} (hX : 0 ≤ p.1) (heta : |p.2| ≤ 1) : (nominalCoefficients W).phi 0 p = W.axis.normalization * W.f p ∧ (nominalCoefficients W).axial 0 p = W.U p ∧ (nominalCoefficients W).pressure 0 p = W.Pi p

theorem NavierStokes.AssembledSlowBase.nominalCoefficients_stress_zero {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ℝ × ℝ} (hp : p.1 ≤ nominalInner W / 8) (n : ℕ) : (nominalCoefficients W).stressTheta n p = 0 ∧ (nominalCoefficients W).stressAxial n p = 0

theorem NavierStokes.AssembledSlowBase.nominalCoefficients_stress_eq {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ℝ × ℝ} (hp : 0 ≤ p.1) (heta : |p.2| ≤ 1) (n : ℕ) : (nominalCoefficients W).stressTheta n p = SlowResidualMatching.thetaStress F.data.h W.axis.normalization (GlobalSlowProfiles.asSlowProfiles (nominalScheme W)) n p ∧ (nominalCoefficients W).stressAxial n p = SlowResidualMatching.zStress F.data.h (GlobalSlowProfiles.asSlowProfiles (nominalScheme W)) n p

theorem NavierStokes.AssembledSlowBase.nominal_extended_flux {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (n : ℕ) {p : ℝ × ℝ} (hX : 0 ≤ p.1) (heta : |p.2| ≤ 1) : p.1 * extendedCoefficient (nominalScheme W) ⋯ n 2 p = SlowDivergence.radialFlux F.data.h (AxisSourceRegularity.slowOrder F.data.h n) ((nominalCoefficients W).axial n) p

theorem NavierStokes.AssembledSlowBase.nominal_exists_base {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (lo hi : ℝ) (N : ℕ) : ∃ (a : ℕ → ℕ), N ≤ a 0 ∧ SlowBorelBase.AdmissibleScales F.data.h (SlowBorelBase.coefficientBundle W.axis.normalization (nominalCoefficients W)) (SlowBorelBase.innerBox lo hi) a ∧ ContDiffOn ℝ (↑⊤) (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (nominalCoefficients W)) (Set.Iio 1 ×ˢ Set.univ) ∧ ∀ t < 1, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (nominalCoefficients W)) t x = 0

A common smooth solenoidal physical base now follows from one actual nominal witness, including the derived zero-order equations.

theorem NavierStokes.AssembledSlowBase.nominal_divergenceCoefficient {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (n : ℕ) {p : ℝ × ℝ} (hX : 0 < p.1) (heta : p.2 ∈ nominalParameters W) : SlowExpansionResidual.divergenceCoefficient F.data.h (GlobalSlowProfiles.asSlowProfiles (nominalScheme W)) n p = 0

theorem NavierStokes.AssembledSlowBase.nominal_pressureCoefficient {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (n : ℕ) {p : ℝ × ℝ} (hX : 0 < p.1) (heta : p.2 ∈ nominalParameters W) : SlowExpansionResidual.pressureCoefficient F.data.h W.axis.normalization (GlobalSlowProfiles.asSlowProfiles (nominalScheme W)) n p = 0

theorem NavierStokes.AssembledSlowBase.nominal_densities_smooth {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (n : ℕ) : GlobalSlowProfiles.Smooth (nominalParameters W) (SlowResidualMatching.thetaDensity F.data.h W.axis.normalization (GlobalSlowProfiles.asSlowProfiles (nominalScheme W)) n) ∧ GlobalSlowProfiles.Smooth (nominalParameters W) (SlowResidualMatching.zDensity F.data.h (GlobalSlowProfiles.asSlowProfiles (nominalScheme W)) n)

theorem NavierStokes.AssembledSlowBase.nominalCoefficients_axis {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {n : ℕ} (hn : 0 < n) {eta : ℝ} (heta : |eta| ≤ 1) : (nominalCoefficients W).phi n (0, eta) = 0 ∧ (nominalCoefficients W).axial n (0, eta) = 0 ∧ (nominalCoefficients W).pressure n (0, eta) = 0

theorem NavierStokes.AssembledSlowBase.nominalCoefficients_compactSupport {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {n : ℕ} (hn : 0 < n) : HasCompactSupport ((nominalCoefficients W).phi n) ∧ HasCompactSupport ((nominalCoefficients W).axial n) ∧ HasCompactSupport ((nominalCoefficients W).pressure n)

theorem NavierStokes.AssembledSlowBase.nominalCoefficients_positive_exterior {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {n : ℕ} (hn : 0 < n) {p : ℝ × ℝ} (hp : nominalOuterX W ≤ p.1) : (nominalCoefficients W).phi n p = 0 ∧ (nominalCoefficients W).axial n p = 0 ∧ (nominalCoefficients W).pressure n p = 0

theorem NavierStokes.AssembledSlowBase.nominal_axial_primitive_zero {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {n : ℕ} (hn : 0 < n) {p : ℝ × ℝ} (hX : nominalOuterX W ≤ p.1) (heta : |p.2| ≤ 1) : ProfileHistories.primitive ((nominalCoefficients W).axial n) p = 0

theorem NavierStokes.AssembledSlowBase.nominal_axial_average_zero {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {n : ℕ} (hn : 0 < n) {p : ℝ × ℝ} (hX : nominalOuterX W ≤ p.1) (heta : |p.2| ≤ 1) : ProfileHistories.average ((nominalCoefficients W).axial n) p = 0

theorem NavierStokes.AssembledSlowBase.nominal_exterior_base {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ℝ × ℝ} (hX : nominalOuterX W ≤ p.1) (heta : |p.2| ≤ 1) : W.U p = 0 ∧ W.profiles.M p = 0

theorem NavierStokes.AssembledSlowBase.nominalCoefficients_axial_zero_all {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (n : ℕ) {p : ℝ × ℝ} (hX : nominalOuterX W ≤ p.1) (heta : |p.2| ≤ 1) : (nominalCoefficients W).axial n p = 0

theorem NavierStokes.AssembledSlowBase.nominal_axial_primitive_zero_all {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (n : ℕ) {p : ℝ × ℝ} (hX : nominalOuterX W ≤ p.1) (heta : |p.2| ≤ 1) : ProfileHistories.primitive ((nominalCoefficients W).axial n) p = 0

theorem NavierStokes.AssembledSlowBase.nominal_axial_average_zero_all {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (n : ℕ) {p : ℝ × ℝ} (hX : nominalOuterX W ≤ p.1) (heta : |p.2| ≤ 1) : ProfileHistories.average ((nominalCoefficients W).axial n) p = 0

structure NavierStokes.AssembledSlowBase.FiniteModification {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) (S : Set ℝ) (lo hi : ℝ) : Prop

A finite modification certificate. These are literal identities of the modified physical fields and their mass primitive, not assumptions about the positive-order hierarchy or its infinite sum. A modulation construction can obtain them from supported transplant and restoration of the five rows.

• isOpen : IsOpen S
• contains : Set.Icc (-1) 1 ⊆ S
• subset : S ⊆ nominalParameters W
• halfPlane (X : ℝ) : 0 ≤ X → ∀ eta ∈ S, (X, eta) ∈ D.carrier
• inner : nominalInner W ≤ lo
• ordered : lo < hi
• outer : hi ≤ ReservedPatches.left F W.controls.radius ReservedPatches.Slot.positive
• pressure0 : Q.pressure0 = W.profiles.pressure0
• fields (p : ℝ × ℝ) : 0 ≤ p.1 → p.2 ∈ S → p.1 ≤ lo ∨ hi ≤ p.1 → Q.f p = W.profiles.f p ∧ Q.U p = W.profiles.U p
• mass (eta : ℝ) : eta ∈ S → Q.M (nominalOuterX W, eta) = W.profiles.M (nominalOuterX W, eta)

theorem NavierStokes.AssembledSlowBase.modifiedDomain {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) : GlobalSlowProfiles.Domain S F.data.h

theorem NavierStokes.AssembledSlowBase.modified_original_domain {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) (X : ℝ) (hX : 0 ≤ X) (eta : ℝ) (heta : eta ∈ S) : (X, eta) ∈ W.domain.carrier

theorem NavierStokes.AssembledSlowBase.modification_before_outer {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) : hi < nominalOuterX W

theorem NavierStokes.AssembledSlowBase.modified_axial_exterior {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) (eta : ℝ) : eta ∈ S → ∀ (X : ℝ), nominalOuterRadius W ^ 2 / 2 ≤ X → Q.U (X, eta) = 0

theorem NavierStokes.AssembledSlowBase.modified_mass_zero {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) (eta : ℝ) : eta ∈ S → Q.M (nominalOuterRadius W ^ 2 / 2, eta) = 0

theorem NavierStokes.AssembledSlowBase.modified_positive_patch {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) {R eta : ℝ} (heta : eta ∈ S) (hR : R ∈ ReservedPatches.radialWindow F W.controls.radius ReservedPatches.Slot.positive) : Q.U (R ^ 2 / 2, eta) = 0 ∧ Q.E (R ^ 2 / 2, eta) = FiveRowRank.background F.data.core.lam (ReservedPatches.radialAmplitude F W.controls.radius eta) R

noncomputable def NavierStokes.AssembledSlowBase.modifiedBaseData {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) : GlobalSlowProfiles.BaseData S W.axis.normalization F.data.core.lam (ReservedPatches.radialLeft F W.controls.radius ReservedPatches.Slot.positive) (ReservedPatches.radialRight F W.controls.radius ReservedPatches.Slot.positive) (nominalOuterRadius W)

Modified base data, constructed using baseDataOfProfile.

Equations

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

noncomputable def NavierStokes.AssembledSlowBase.modifiedScheme {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) : GlobalSlowProfiles.Scheme S F.data.h W.axis.normalization

Modified scheme, constructed using schemeFromHierarchy.

Equations

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

theorem NavierStokes.AssembledSlowBase.modifiedLocalization {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) : GlobalSlowProfiles.Localization (modifiedScheme W Q M) (nominalHierarchy W) (nominalInner W)

theorem NavierStokes.AssembledSlowBase.modified_base_local {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) (i : Fin 4) {p : ℝ × ℝ} (hX : 0 ≤ p.1) (hinner : p.1 < nominalInner W) (heta : p.2 ∈ S) : GlobalSlowProfiles.xProfile (GlobalSlowProfiles.component (modifiedScheme W Q M).base i) p = GlobalSlowProfiles.xProfile (GlobalSlowProfiles.component (nominalScheme W).base i) p

theorem NavierStokes.AssembledSlowBase.modifiedBaseAgreement {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) : GlobalSlowProfiles.BaseAgreement (modifiedScheme W Q M) (nominalHierarchy W) (nominalInner W)

theorem NavierStokes.AssembledSlowBase.modified_zero_coefficients {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) {p : ℝ × ℝ} (hX : 0 < p.1) (hinner : p.1 < nominalInner W) (heta : p.2 ∈ S) : SlowExpansionResidual.angularCoefficient F.data.h (GlobalSlowProfiles.asSlowProfiles (modifiedScheme W Q M)) 0 p = 0 ∧ SlowExpansionResidual.axialCoefficient F.data.h (GlobalSlowProfiles.asSlowProfiles (modifiedScheme W Q M)) 0 p = 0

theorem NavierStokes.AssembledSlowBase.modifiedZeroOrder {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) : ZeroOrderSolved (modifiedScheme W Q M) (nominalInner W)

noncomputable def NavierStokes.AssembledSlowBase.modifiedCoefficients {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) : SlowBorelBase.Coefficients

All positive profiles, canonical stress primitives, and global smooth extensions are rebuilt from the actual finite modified profile.

Equations

• NavierStokes.AssembledSlowBase.modifiedCoefficients W Q M = NavierStokes.AssembledSlowBase.coefficients ⋯ ⋯ ⋯ ⋯

theorem NavierStokes.AssembledSlowBase.modifiedCoefficients_smooth {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) : SlowBorelBase.SmoothCoefficients (modifiedCoefficients W Q M)

theorem NavierStokes.AssembledSlowBase.modifiedCoefficients_zero_fields {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) {p : ℝ × ℝ} (hX : 0 ≤ p.1) (heta : |p.2| ≤ 1) : (modifiedCoefficients W Q M).phi 0 p = W.axis.normalization * Q.f p ∧ (modifiedCoefficients W Q M).axial 0 p = Q.U p ∧ (modifiedCoefficients W Q M).pressure 0 p = Q.pressure p

theorem NavierStokes.AssembledSlowBase.modifiedCoefficients_axis {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) {n : ℕ} (hn : 0 < n) {eta : ℝ} (heta : |eta| ≤ 1) : (modifiedCoefficients W Q M).phi n (0, eta) = 0 ∧ (modifiedCoefficients W Q M).axial n (0, eta) = 0 ∧ (modifiedCoefficients W Q M).pressure n (0, eta) = 0

theorem NavierStokes.AssembledSlowBase.modified_extended_flux {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) (n : ℕ) {p : ℝ × ℝ} (hX : 0 ≤ p.1) (heta : |p.2| ≤ 1) : p.1 * extendedCoefficient (modifiedScheme W Q M) ⋯ n 2 p = SlowDivergence.radialFlux F.data.h (AxisSourceRegularity.slowOrder F.data.h n) ((modifiedCoefficients W Q M).axial n) p

theorem NavierStokes.AssembledSlowBase.modified_divergenceCoefficient {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) (n : ℕ) {p : ℝ × ℝ} (hX : 0 < p.1) (heta : p.2 ∈ S) : SlowExpansionResidual.divergenceCoefficient F.data.h (GlobalSlowProfiles.asSlowProfiles (modifiedScheme W Q M)) n p = 0

theorem NavierStokes.AssembledSlowBase.modified_pressureCoefficient {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) (n : ℕ) {p : ℝ × ℝ} (hX : 0 < p.1) (heta : p.2 ∈ S) : SlowExpansionResidual.pressureCoefficient F.data.h W.axis.normalization (GlobalSlowProfiles.asSlowProfiles (modifiedScheme W Q M)) n p = 0

theorem NavierStokes.AssembledSlowBase.modified_exists_base {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : FiniteModification W Q S lo hi) (lower upper : ℝ) (N : ℕ) : ∃ (a : ℕ → ℕ), N ≤ a 0 ∧ SlowBorelBase.AdmissibleScales F.data.h (SlowBorelBase.coefficientBundle W.axis.normalization (modifiedCoefficients W Q M)) (SlowBorelBase.innerBox lower upper) a ∧ ContDiffOn ℝ (↑⊤) (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (modifiedCoefficients W Q M)) (Set.Iio 1 ×ˢ Set.univ) ∧ ∀ t < 1, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (modifiedCoefficients W Q M)) t x = 0