The actual constructed slow base

The finite residual identities, regular axis descriptors, and stress support used here are derived from the same repaired coefficient sequence. No residual estimate or infinite-dimensional output certificate is an input.

The actual pure-heat exterior of the summed slow base

The exterior comparison is with the physical radial heat solution and its canonical improper-integral pressure. All stream cutoffs are retained until their coefficients are shown to vanish in an exterior neighborhood.

noncomputable def NavierStokes.BaseExterior.heatCoefficient (C h : ℝ) : SimilarityProfile.PhysicalProfile

The regular Cartesian swirl coefficient of the physical heat solution.

Equations

• NavierStokes.BaseExterior.heatCoefficient C h = NavierStokes.TerminalStress.swirlCoefficient C h fun (x : ℝ) => 1

noncomputable def NavierStokes.BaseExterior.heatPressure (C h : ℝ) : SimilarityProfile.PhysicalProfile

The pressure is the literal canonical radial integral.

Equations

• NavierStokes.BaseExterior.heatPressure C h = NavierStokes.TerminalStress.canonicalPressure (NavierStokes.BaseExterior.heatCoefficient C h)

noncomputable def NavierStokes.BaseExterior.heatVelocity (C h : ℝ) : ProblemStatement.VelocityField

Heat velocity, given by AxisymmetricResidual.velocity (fun _ => 0) (heatCoefficient C h) (fun _ => 0).

Equations

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

noncomputable def NavierStokes.BaseExterior.heatPressureField (C h : ℝ) : ProblemStatement.PressureField

Heat pressure field, given by AxisymmetricResidual.pressure (heatPressure C h).

Equations

• NavierStokes.BaseExterior.heatPressureField C h = NavierStokes.AxisymmetricResidual.pressure (NavierStokes.BaseExterior.heatPressure C h)

theorem NavierStokes.BaseExterior.heatCoefficient_eq (C h : ℝ) (p : SimilarityProfile.PhysicalPoint) : heatCoefficient C h p = TerminalStress.physicalHeat C (1 + h) p / √(2 * p.2.1)

theorem NavierStokes.BaseExterior.heatCoefficient_z_invariant (C h t s z z' : ℝ) : heatCoefficient C h (t, s, z) = heatCoefficient C h (t, s, z')

theorem NavierStokes.BaseExterior.heatPressure_z_invariant (C h t s z z' : ℝ) : heatPressure C h (t, s, z) = heatPressure C h (t, s, z')

theorem NavierStokes.BaseExterior.heatCoefficient_smoothAt (C : ℝ) {h : ℝ} (hh : 0 < h) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : ContDiffAt ℝ (↑⊤) (heatCoefficient C h) p

theorem NavierStokes.BaseExterior.heatPressure_smoothAt (C : ℝ) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : ContDiffAt ℝ (↑⊤) (heatPressure C h) p

theorem NavierStokes.BaseExterior.partialZ_of_invariant {f : SimilarityProfile.PhysicalProfile} {p : SimilarityProfile.PhysicalPoint} (hf : DifferentiableAt ℝ f p) (he : ∀ (z : ℝ), f (p.1, p.2.1, z) = f p) : SimilarityProfile.partialZ f p = 0

theorem NavierStokes.BaseExterior.heatCoefficient_partialZ (C : ℝ) {h : ℝ} (hh : 0 < h) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : SimilarityProfile.partialZ (heatCoefficient C h) p = 0

theorem NavierStokes.BaseExterior.heatCoefficient_partialZZ (C : ℝ) {h : ℝ} (hh : 0 < h) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : SimilarityProfile.partialZ (SimilarityProfile.partialZ (heatCoefficient C h)) p = 0

theorem NavierStokes.BaseExterior.heatPressure_partialZ (C : ℝ) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : SimilarityProfile.partialZ (heatPressure C h) p = 0

theorem NavierStokes.BaseExterior.heatCoefficient_sq_integrable (C : ℝ) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {t a z : ℝ} (ht : t < 1) (ha : 0 < a) : MeasureTheory.IntegrableOn (fun (s : ℝ) => heatCoefficient C h (t, s, z) ^ 2) (Set.Ioi a) MeasureTheory.volume

theorem NavierStokes.BaseExterior.heatCoefficient_sq_continuous (C : ℝ) {h : ℝ} (hh : 0 < h) {t a z : ℝ} (ht : t < 1) (ha : 0 < a) : ContinuousOn (fun (s : ℝ) => heatCoefficient C h (t, s, z) ^ 2) (Set.Ioi a)

theorem NavierStokes.BaseExterior.heatPressure_partialS (C : ℝ) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : SimilarityProfile.partialS (heatPressure C h) p = heatCoefficient C h p ^ 2

theorem NavierStokes.BaseExterior.heatCoefficient_residual_zero (C : ℝ) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : TerminalStress.residualCoefficient (heatCoefficient C h) p = 0

theorem NavierStokes.BaseExterior.heat_navierStokesResidual_zero (C : ℝ) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {t : ℝ} {x : ProblemStatement.Space} (ht : t < 1) (hs : 0 < AxisymmetricFields.radialEnergy x) : ProblemStatement.navierStokesResidual (heatVelocity C h) (heatPressureField C h) t x = 0

The physical heat exterior solves the unforced Cartesian equations exactly. Both the heat equation and canonical pressure balance are proved.

structure NavierStokes.BaseExterior.ExteriorCoefficients (d : SlowBorelBase.Coefficients) (R : ℝ) : Prop

Original scalar coefficient and mass identities. These say nothing about the summed velocity or its residual.

• axial (n : ℕ) (w : SlowBorelBase.Inner) : R < w.1 → w.2 ∈ Set.Icc (-1) 1 → d.axial n w = 0
• mass (n : ℕ) (w : SlowBorelBase.Inner) : R < w.1 → w.2 ∈ Set.Icc (-1) 1 → ProfileHistories.primitive (d.axial n) w = 0
• phi (n : ℕ) : 0 < n → ∀ (w : SlowBorelBase.Inner), R < w.1 → w.2 ∈ Set.Icc (-1) 1 → d.phi n w = 0
• pressure (n : ℕ) : 0 < n → ∀ (w : SlowBorelBase.Inner), R < w.1 → w.2 ∈ Set.Icc (-1) 1 → d.pressure n w = 0

theorem NavierStokes.BaseExterior.ExteriorCoefficients.average {d : SlowBorelBase.Coefficients} {R : ℝ} (hd : ExteriorCoefficients d R) (hR : 0 ≤ R) (n : ℕ) {w : SlowBorelBase.Inner} (hw : R < w.1) (he : w.2 ∈ Set.Icc (-1) 1) : ProfileHistories.average (d.axial n) w = 0

theorem NavierStokes.BaseExterior.physical_eta_mem {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) : (SlowBorelBase.physicalChart h p).2.2 ∈ Set.Icc (-1) 1

noncomputable def NavierStokes.BaseExterior.exteriorDomain (h R : ℝ) : Set SimilarityProfile.PhysicalPoint

Exterior domain, given by {p | p.1 < 1 ∧ R < (physicalChart h p).2.1}.

Equations

• NavierStokes.BaseExterior.exteriorDomain h R = {p : NavierStokes.SimilarityProfile.PhysicalPoint | p.1 < 1 ∧ R < (NavierStokes.SlowBorelBase.physicalChart h p).2.1}

noncomputable def NavierStokes.BaseExterior.cartesianExterior (h R : ℝ) : Set ProblemStatement.SpaceTime

Cartesian exterior, given by {z | z.1 < 1 ∧ R < (cartesianChart h z).2.1}.

Equations

• NavierStokes.BaseExterior.cartesianExterior h R = {z : NavierStokes.ProblemStatement.SpaceTime | z.1 < 1 ∧ R < (NavierStokes.SlowBorelBase.cartesianChart h z).2.1}

theorem NavierStokes.BaseExterior.exteriorDomain_isOpen {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (R : ℝ) : IsOpen (exteriorDomain h R)

theorem NavierStokes.BaseExterior.cartesianExterior_isOpen {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (R : ℝ) : IsOpen (cartesianExterior h R)

theorem NavierStokes.BaseExterior.physicalProfile_eq_leading {a : ℕ → ℕ} {h b : ℝ} {f : ℕ → SlowBorelBase.Inner → ℝ} {p : SimilarityProfile.PhysicalPoint} (hf : ∀ (n : ℕ), 0 < n → f n (SlowBorelBase.physicalChart h p).2 = 0) : SlowBorelBase.physicalProfile a h b f p = SimilarityProfile.pullback h b (f 0) p

theorem NavierStokes.BaseExterior.exterior_stream_zero {a : ℕ → ℕ} {h C R : ℝ} {d : SlowBorelBase.Coefficients} (hh : 0 < h) (hh1 : h < 1 / 2) (hR : 0 ≤ R) (hd : ExteriorCoefficients d R) {p : SimilarityProfile.PhysicalPoint} (hp : p ∈ exteriorDomain h R) : SlowBorelBase.streamFactor a h C d p = 0

theorem NavierStokes.BaseExterior.exterior_stream_germ {a : ℕ → ℕ} {h C R : ℝ} {d : SlowBorelBase.Coefficients} (hh : 0 < h) (hh1 : h < 1 / 2) (hR : 0 ≤ R) (hd : ExteriorCoefficients d R) {p : SimilarityProfile.PhysicalPoint} (hp : p ∈ exteriorDomain h R) : SlowBorelBase.streamFactor a h C d =ᶠ[nhds p] fun (x : SimilarityProfile.PhysicalPoint) => 0

All derivatives of the actual cut stream vanish in the exterior. In particular this includes derivatives falling on the scale cutoffs.

noncomputable def NavierStokes.BaseExterior.leadingAngular (h C : ℝ) (d : SlowBorelBase.Coefficients) : SimilarityProfile.PhysicalProfile

Leading angular, defined pointwise by C⁻¹ * SimilarityProfile.pullback h (-CoordinateAlgebra.A h - 1 / 2) (d.phi 0) p.

Equations

• NavierStokes.BaseExterior.leadingAngular h C d p = C⁻¹ * NavierStokes.SimilarityProfile.pullback h (-NavierStokes.CoordinateAlgebra.A h - 1 / 2) (d.phi 0) p

noncomputable def NavierStokes.BaseExterior.leadingPressure (h : ℝ) (d : SlowBorelBase.Coefficients) : SimilarityProfile.PhysicalProfile

Leading pressure, given by SimilarityProfile.pullback h (-2 * CoordinateAlgebra.A h) (d.pressure 0).

Equations

• NavierStokes.BaseExterior.leadingPressure h d = NavierStokes.SimilarityProfile.pullback h (-2 * NavierStokes.CoordinateAlgebra.A h) (d.pressure 0)

theorem NavierStokes.BaseExterior.exterior_swirl_derivative {a : ℕ → ℕ} (ha : StrictMono a) {h C R : ℝ} {d : SlowBorelBase.Coefficients} (hh : 0 < h) (hh1 : h < 1 / 2) (hds : SlowBorelBase.SmoothCoefficients d) (hd : ExteriorCoefficients d R) {p : SimilarityProfile.PhysicalPoint} (hp : p ∈ exteriorDomain h R) : AxisymmetricFields.partialS (SlowBorelBase.swirlPotential a h C d) p = -leadingAngular h C d p

theorem NavierStokes.BaseExterior.exterior_velocity_eq_leading {a : ℕ → ℕ} (ha : StrictMono a) {h C R : ℝ} {d : SlowBorelBase.Coefficients} (hh : 0 < h) (hh1 : h < 1 / 2) (hR : 0 ≤ R) (hds : SlowBorelBase.SmoothCoefficients d) (hd : ExteriorCoefficients d R) {z : ProblemStatement.SpaceTime} (hz : z ∈ cartesianExterior h R) : SlowBorelBase.baseVelocity a h C d z = AxisymmetricResidual.velocity (fun (x : AxisymmetricFields.ProfilePoint) => 0) (leadingAngular h C d) (fun (x : AxisymmetricFields.ProfilePoint) => 0) z

theorem NavierStokes.BaseExterior.exterior_pressure_eq_leading {a : ℕ → ℕ} {h C R : ℝ} {d : SlowBorelBase.Coefficients} (hh : 0 < h) (hh1 : h < 1 / 2) (hd : ExteriorCoefficients d R) {z : ProblemStatement.SpaceTime} (hz : z ∈ cartesianExterior h R) : SlowBorelBase.basePressure a h C d z = AxisymmetricResidual.pressure (leadingPressure h d) z

theorem NavierStokes.BaseExterior.exterior_base_eq_heat {a : ℕ → ℕ} (ha : StrictMono a) {h C R K : ℝ} {d : SlowBorelBase.Coefficients} (hh : 0 < h) (hh1 : h < 1 / 2) (hR : 0 ≤ R) (hds : SlowBorelBase.SmoothCoefficients d) (hd : ExteriorCoefficients d R) (hphi : Set.EqOn (leadingAngular h C d) (heatCoefficient K h) (exteriorDomain h R)) (hp : Set.EqOn (leadingPressure h d) (heatPressure K h) (exteriorDomain h R)) : Set.EqOn (SlowBorelBase.baseVelocity a h C d) (heatVelocity K h) (cartesianExterior h R) ∧ Set.EqOn (SlowBorelBase.basePressure a h C d) (heatPressureField K h) (cartesianExterior h R)

Exact physical leading identities suffice for the exterior comparison; there is no hypothesis about the summed velocity or residual.

theorem NavierStokes.BaseExterior.exterior_base_residual_zero {a : ℕ → ℕ} (ha : StrictMono a) {h C R K : ℝ} {d : SlowBorelBase.Coefficients} (hh : 0 < h) (hh1 : h < 1 / 2) (hR : 0 ≤ R) (hds : SlowBorelBase.SmoothCoefficients d) (hd : ExteriorCoefficients d R) (hphi : Set.EqOn (leadingAngular h C d) (heatCoefficient K h) (exteriorDomain h R)) (hp : Set.EqOn (leadingPressure h d) (heatPressure K h) (exteriorDomain h R)) {z : ProblemStatement.SpaceTime} (hz : z ∈ cartesianExterior h R) : ProblemStatement.navierStokesResidual (SlowBorelBase.baseVelocity a h C d) (SlowBorelBase.basePressure a h C d) z.1 z.2 = 0

theorem NavierStokes.BaseExterior.q_radial (h t s s' z : ℝ) : SimilarityProfile.q h (t, s, z) = SimilarityProfile.q h (t, s', z)

theorem NavierStokes.BaseExterior.eta_radial (h t s s' z : ℝ) : SimilarityProfile.eta h (t, s, z) = SimilarityProfile.eta h (t, s', z)

theorem NavierStokes.BaseExterior.pullback_radial_scaled (h b : ℝ) (f : SimilarityProfile.InnerProfile) {p : SimilarityProfile.PhysicalPoint} (hq : 0 < SimilarityProfile.q h p) (u : ℝ) : SimilarityProfile.pullback h b f (p.1, SimilarityProfile.q h p * u, p.2.2) = SimilarityProfile.q h p ^ b * f (u, SimilarityProfile.eta h p)

theorem NavierStokes.BaseExterior.canonicalPressure_pullback (h b : ℝ) (f : SimilarityProfile.InnerProfile) {p : SimilarityProfile.PhysicalPoint} (hq : 0 < SimilarityProfile.q h p) : TerminalStress.canonicalPressure (SimilarityProfile.pullback h b f) p = SimilarityProfile.q h p ^ (2 * b + 1) * -∫ (u : ℝ) in Set.Ioi (SimilarityProfile.X h p), f (u, SimilarityProfile.eta h p) ^ 2

Dilation of the actual improper pressure integral. No pressure regularity or pressure identity is assumed.

theorem NavierStokes.BaseExterior.canonicalPressure_congr_tail {F G : SimilarityProfile.PhysicalProfile} {p : SimilarityProfile.PhysicalPoint} (he : ∀ (s : ℝ), p.2.1 < s → F (p.1, s, p.2.2) = G (p.1, s, p.2.2)) : TerminalStress.canonicalPressure F p = TerminalStress.canonicalPressure G p

theorem NavierStokes.BaseExterior.physical_angular_from_profile (h : ℝ) {f E : SimilarityProfile.InnerProfile} {p : SimilarityProfile.PhysicalPoint} (hq : 0 < SimilarityProfile.q h p) (hs : 0 < p.2.1) (he : E (SimilarityProfile.inner h p) = √(2 * SimilarityProfile.X h p) * f (SimilarityProfile.inner h p)) : SimilarityProfile.pullback h (-CoordinateAlgebra.A h - 1 / 2) f p = SimilarityProfile.q h p ^ (-CoordinateAlgebra.A h) * E (SimilarityProfile.inner h p) / √(2 * p.2.1)

noncomputable def NavierStokes.BaseExterior.closedHeatDomain : Set SimilarityProfile.PhysicalPoint

Closed heat domain, given by {p | p.1 ≤ 1 ∧ 0 < p.2.1}.

Equations

• NavierStokes.BaseExterior.closedHeatDomain = {p : NavierStokes.SimilarityProfile.PhysicalPoint | p.1 ≤ 1 ∧ 0 < p.2.1}

theorem NavierStokes.BaseExterior.heatCoefficient_sq_scaled (C h : ℝ) {p : SimilarityProfile.PhysicalPoint} (hs : 0 < p.2.1) {v : ℝ} (hv : 0 < v) : heatCoefficient C h (p.1, p.2.1 * v, p.2.2) ^ 2 = C ^ 2 / 2 * p.2.1 ^ (-2 * TerminalPressure.amplitudeExponent h - 1) * TerminalPressure.heatDensity h ((1 - p.1) / p.2.1) v

theorem NavierStokes.BaseExterior.heatPressure_formula (C h : ℝ) {p : SimilarityProfile.PhysicalPoint} (hs : 0 < p.2.1) : heatPressure C h p = -(C ^ 2 / 2) * p.2.1 ^ (-2 * TerminalPressure.amplitudeExponent h) * TerminalPressure.heatPressureFactor h ((1 - p.1) / p.2.1)

A formula for the canonical heat pressure valid also at zero time remaining. Its factor is the actual convergent pressure integral.

theorem NavierStokes.BaseExterior.heatCoefficient_contDiffOn_closed (C : ℝ) {h : ℝ} (hh : 0 < h) : ContDiffOn ℝ (↑⊤) (heatCoefficient C h) closedHeatDomain

Joint one-sided smoothness at t=1 at every positive physical radius.

theorem NavierStokes.BaseExterior.heatPressure_contDiffOn_closed (C : ℝ) {h : ℝ} (hh : 0 < h) : ContDiffOn ℝ (↑⊤) (heatPressure C h) closedHeatDomain

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

Nominal heat switch, given by OutgoingDilation.switchRadius F W.controls.radius.

Equations

• NavierStokes.BaseExterior.nominalHeatSwitch W = NavierStokes.OutgoingDilation.switchRadius F W.controls.radius

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

Nominal exterior radius, given by max (nominalOuterX W) (max W.controls.radius (nominalHeatSwitch W * Real.exp 3)).

Equations

• NavierStokes.BaseExterior.nominalExteriorRadius W = max (NavierStokes.AssembledSlowBase.nominalOuterX W) (max W.controls.radius (NavierStokes.BaseExterior.nominalHeatSwitch W * Real.exp 3))

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

Nominal heat normalization, given by PhysicalHeatCoordinates.normalization F.data (nominalHeatSwitch W).

Equations

• NavierStokes.BaseExterior.nominalHeatNormalization W = NavierStokes.PhysicalHeatCoordinates.normalization F.data (NavierStokes.BaseExterior.nominalHeatSwitch W)

theorem NavierStokes.BaseExterior.nominalHeatSwitch_pos {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : 0 < nominalHeatSwitch W

theorem NavierStokes.BaseExterior.nominalExteriorRadius_pos {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : 0 < nominalExteriorRadius W

theorem NavierStokes.BaseExterior.nominalExteriorRadius_ge_outer {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : AssembledSlowBase.nominalOuterX W ≤ nominalExteriorRadius W

theorem NavierStokes.BaseExterior.nominalExteriorRadius_ge_radius {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : W.controls.radius ≤ nominalExteriorRadius W

theorem NavierStokes.BaseExterior.nominalExteriorRadius_ge_late {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : nominalHeatSwitch W * Real.exp 3 ≤ nominalExteriorRadius W

theorem NavierStokes.BaseExterior.nominalExteriorRadius_gt_switch {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : nominalHeatSwitch W < nominalExteriorRadius W

theorem NavierStokes.BaseExterior.nominal_exterior_coefficients {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : ExteriorCoefficients (AssembledSlowBase.nominalCoefficients W) (nominalExteriorRadius W)

All required original coefficient support and mass identities are discharged for the actual repaired nominal sequence.

theorem NavierStokes.BaseExterior.nominal_leadingAngular_eq_pullback {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hX : 0 ≤ SimilarityProfile.X F.data.h p) : leadingAngular F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W) p = SimilarityProfile.pullback F.data.h (-CoordinateAlgebra.A F.data.h - 1 / 2) W.f p

theorem NavierStokes.BaseExterior.nominal_late_ratio {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {X : ℝ} (hX : nominalExteriorRadius W < X) : 3 ≤ Real.log (X / nominalHeatSwitch W) + 1 / 5

theorem NavierStokes.BaseExterior.nominal_angular_pure_heat {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : SimilarityProfile.PhysicalPoint} (hp : p ∈ exteriorDomain F.data.h (nominalExteriorRadius W)) : leadingAngular F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W) p = heatCoefficient (nominalHeatNormalization W) F.data.h p

theorem NavierStokes.BaseExterior.nominal_pressure_regular_integral {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {X eta : ℝ} (hX : 0 ≤ X) (he : eta ∈ HeatedOutgoing.parameterDomain) : W.Pi (X, eta) = -∫ (u : ℝ) in Set.Ioi X, W.f (u, eta) ^ 2

The nominal pressure is the actual squared regular swirl integral.

theorem NavierStokes.BaseExterior.nominal_pressure_pullback {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hX : 0 ≤ SimilarityProfile.X F.data.h p) : leadingPressure F.data.h (AssembledSlowBase.nominalCoefficients W) p = TerminalStress.canonicalPressure (SimilarityProfile.pullback F.data.h (-CoordinateAlgebra.A F.data.h - 1 / 2) W.f) p

theorem NavierStokes.BaseExterior.nominal_pressure_pure_heat {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : SimilarityProfile.PhysicalPoint} (hp : p ∈ exteriorDomain F.data.h (nominalExteriorRadius W)) : leadingPressure F.data.h (AssembledSlowBase.nominalCoefficients W) p = heatPressure (nominalHeatNormalization W) F.data.h p

theorem NavierStokes.BaseExterior.nominal_base_eq_heat {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {a : ℕ → ℕ} (ha : StrictMono a) : Set.EqOn (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) (heatVelocity (nominalHeatNormalization W) F.data.h) (cartesianExterior F.data.h (nominalExteriorRadius W)) ∧ Set.EqOn (SlowBorelBase.basePressure a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) (heatPressureField (nominalHeatNormalization W) F.data.h) (cartesianExterior F.data.h (nominalExteriorRadius W))

The actual summed nominal velocity and pressure are exactly the radial heat field outside one common profile radius, for every cutoff schedule.

theorem NavierStokes.BaseExterior.nominal_base_residual_zero {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {a : ℕ → ℕ} (ha : StrictMono a) {z : ProblemStatement.SpaceTime} (hz : z ∈ cartesianExterior F.data.h (nominalExteriorRadius W)) : ProblemStatement.navierStokesResidual (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) (SlowBorelBase.basePressure a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) z.1 z.2 = 0

Exact zero residual in the actual summed exterior. No exterior solution property is supplied as a premise.

theorem NavierStokes.BaseExterior.nominal_base_residual_germ_zero {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {a : ℕ → ℕ} (ha : StrictMono a) {z : ProblemStatement.SpaceTime} (hz : z ∈ cartesianExterior F.data.h (nominalExteriorRadius W)) : (fun (y : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) (SlowBorelBase.basePressure a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) y.1 y.2) =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.BaseExterior.nominal_base_residual_jets_zero {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {a : ℕ → ℕ} (ha : StrictMono a) {z : ProblemStatement.SpaceTime} (hz : z ∈ cartesianExterior F.data.h (nominalExteriorRadius W)) (m : ℕ) : iteratedFDeriv ℝ m (fun (y : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) (SlowBorelBase.basePressure a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) y.1 y.2) z = 0

Every physical derivative of the actual Cartesian residual is exactly zero on the exterior, not just asymptotically small.

noncomputable def NavierStokes.BaseExterior.closedCartesianHeatDomain : Set ProblemStatement.SpaceTime

Closed cartesian heat domain, given by {z | z.1 ≤ 1 ∧ 0 < AxisymmetricFields.radialEnergy z.2}.

Equations

• NavierStokes.BaseExterior.closedCartesianHeatDomain = {z : NavierStokes.ProblemStatement.SpaceTime | z.1 ≤ 1 ∧ 0 < NavierStokes.AxisymmetricFields.radialEnergy z.2}

theorem NavierStokes.BaseExterior.heatVelocity_eq_angularVector (C h : ℝ) (z : ProblemStatement.SpaceTime) : heatVelocity C h z = heatCoefficient C h (AxisymmetricFields.profilePoint z.1 z.2) • BaseResidual.angularVector z

theorem NavierStokes.BaseExterior.heatVelocity_contDiffOn_closed (C : ℝ) {h : ℝ} (hh : 0 < h) : ContDiffOn ℝ (↑⊤) (heatVelocity C h) closedCartesianHeatDomain

The exact exterior solution is jointly smooth up to the terminal time on every region of positive physical radius, in Cartesian coordinates.

theorem NavierStokes.BaseExterior.heatPressureField_contDiffOn_closed (C : ℝ) {h : ℝ} (hh : 0 < h) : ContDiffOn ℝ (↑⊤) (heatPressureField C h) closedCartesianHeatDomain

theorem NavierStokes.BaseExterior.near_one_in_exterior {h R : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hR : 0 ≤ R) {x : ProblemStatement.Space} (hx : x.ofLp 2 = 0) (_hs : 0 < AxisymmetricFields.radialEnergy x) {t : ℝ} (ht : t ∈ Set.Ioo (1 - AxisymmetricFields.radialEnergy x / (R + 1)) 1) : (t, x) ∈ cartesianExterior h R

theorem NavierStokes.BaseExterior.nominal_base_terminal_extension {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {a : ℕ → ℕ} (ha : StrictMono a) {x : ProblemStatement.Space} (hx : x.ofLp 2 = 0) (hs : 0 < AxisymmetricFields.radialEnergy x) : ∃ (δ : ℝ), 0 < δ ∧ (∀ t ∈ Set.Ioo (1 - δ) 1, SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W) (t, x) = heatVelocity (nominalHeatNormalization W) F.data.h (t, x) ∧ SlowBorelBase.basePressure a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W) (t, x) = heatPressureField (nominalHeatNormalization W) F.data.h (t, x)) ∧ ContDiffOn ℝ (↑⊤) (fun (t : ℝ) => heatVelocity (nominalHeatNormalization W) F.data.h (t, x)) (Set.Iic 1) ∧ ContDiffOn ℝ (↑⊤) (fun (t : ℝ) => heatPressureField (nominalHeatNormalization W) F.data.h (t, x)) (Set.Iic 1)

For each fixed positive radius on the central plane, the actual base equals the explicit heat extension on a whole terminal time interval.

theorem NavierStokes.BaseExterior.nominal_base_meridional_zero {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {a : ℕ → ℕ} (ha : StrictMono a) {z : ProblemStatement.SpaceTime} (hz : z ∈ cartesianExterior F.data.h (nominalExteriorRadius W)) : (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W) z).ofLp 2 = 0 ∧ z.2.ofLp 0 * (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W) z).ofLp 0 + z.2.ofLp 1 * (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W) z).ofLp 1 = 0

The curl of the finite slow potentials

The finite Borel prefixes use the average of the axial coefficient and the primitive of the angular coefficient. Their curl is identified here with the finite slow field, using the actual radial flux formula and FTC.

theorem NavierStokes.BasePrefixIdentity.average_radial_identity {U : SlowBorelBase.Inner → ℝ} (hU : ContDiff ℝ (↑⊤) U) (w : SlowBorelBase.Inner) : ProfileHistories.average U w + w.1 * SimilarityProfile.partialX (ProfileHistories.average U) w = U w

Differentiating the actual primitive gives the radial average identity.

theorem NavierStokes.BasePrefixIdentity.radialFlux_eq_neg_X_Z_average {U : SlowBorelBase.Inner → ℝ} (hU : ContDiff ℝ (↑⊤) U) (h lam : ℝ) (w : SlowBorelBase.Inner) : SlowDivergence.radialFlux h lam U w = -w.1 * SimilarityProfile.Z h (-CoordinateAlgebra.A h + lam) (ProfileHistories.average U) w

The flux computed from histories is the axial derivative of the averaged stream coefficient, with its exact exponent. No divergence equation is assumed.

theorem NavierStokes.BasePrefixIdentity.physicalUncutPrefix_germ {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (b : ℝ) (f : ℕ → SlowBorelBase.Inner → ℝ) (J : ℕ) {p : SlowBorelBase.Chart} (hp : p.1 < 1) : SlowBorelBase.physicalUncutPrefix h b f J =ᶠ[nhds p] SlowExpansionResidual.finiteProfile J h b f

The direct finite profile and the finite Borel prefix have the same local germ throughout the past-time chart.

theorem NavierStokes.BasePrefixIdentity.partialS_physicalUncutPrefix {h b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (J : ℕ) (f : ℕ → SlowBorelBase.Inner → ℝ) {p : SlowBorelBase.Chart} (hp : p.1 < 1) (hf : ∀ n ≤ J, DifferentiableAt ℝ (f n) (SimilarityProfile.inner h p)) : AxisymmetricFields.partialS (SlowBorelBase.physicalUncutPrefix h b f J) p = SlowExpansionResidual.finiteProfile J h (b - 1) (fun (n : ℕ) => SimilarityProfile.partialX (f n)) p

theorem NavierStokes.BasePrefixIdentity.partialZ_physicalUncutPrefix {h b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (J : ℕ) (f : ℕ → SlowBorelBase.Inner → ℝ) {p : SlowBorelBase.Chart} (hp : p.1 < 1) (hf : ∀ n ≤ J, DifferentiableAt ℝ (f n) (SimilarityProfile.inner h p)) : AxisymmetricFields.partialZ (SlowBorelBase.physicalUncutPrefix h b f J) p = SlowExpansionResidual.finiteProfile J h (b - CoordinateAlgebra.D h) (fun (n : ℕ) => SimilarityProfile.Z h (b + SlowExpansionResidual.slowOrder h n) (f n)) p

noncomputable def NavierStokes.BasePrefixIdentity.profiles (h : ℝ) (d : SlowBorelBase.Coefficients) : SlowExpansionResidual.SlowProfiles

The coefficient family whose flux is constructed from its axial history.

Equations

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

theorem NavierStokes.BasePrefixIdentity.prefixStream_axial {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (J : ℕ) (C : ℝ) {p : SlowBorelBase.Chart} (hp : p.1 < 1) : BaseResidual.prefixStream J h C d p + p.2.1 * AxisymmetricFields.partialS (BaseResidual.prefixStream J h C d) p = SlowExpansionResidual.slowAxial J h (profiles h d) p

theorem NavierStokes.BasePrefixIdentity.prefixSwirl_radial {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (J : ℕ) (C : ℝ) {p : SlowBorelBase.Chart} (hp : p.1 < 1) : -AxisymmetricFields.partialS (BaseResidual.prefixSwirl J h C d) p = SlowExpansionResidual.slowSwirl J h C (profiles h d) p

theorem NavierStokes.BasePrefixIdentity.prefixStream_flux {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (J : ℕ) (C : ℝ) {p : SlowBorelBase.Chart} (hp : p.1 < 1) : -p.2.1 * AxisymmetricFields.partialZ (BaseResidual.prefixStream J h C d) p = SlowExpansionResidual.slowFlux J h (profiles h d) p

theorem NavierStokes.BasePrefixIdentity.prefixVelocity_eq_profiles {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (J : ℕ) (C : ℝ) {t : ℝ} (ht : t < 1) (x : ProblemStatement.Space) (hs : 0 < AxisymmetricFields.radialEnergy x) : BaseResidual.prefixVelocity J h C d (t, x) = SlowExpansionResidual.slowVelocity J h C (profiles h d) (t, x)

The actual finite curl is the slow field with the flux constructed above.

noncomputable def NavierStokes.BasePrefixIdentity.profileWindow : Set SlowBorelBase.Inner

The physical similarity coordinates range inside this open half strip.

Equations

• NavierStokes.BasePrefixIdentity.profileWindow = Set.Ioi 0 ×ˢ Set.Ioo (-1) 1

theorem NavierStokes.BasePrefixIdentity.profileWindow_open : IsOpen profileWindow

theorem NavierStokes.BasePrefixIdentity.inner_mem_profileWindow {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SlowBorelBase.Chart} (ht : p.1 < 1) (hs : 0 < p.2.1) : SimilarityProfile.inner h p ∈ profileWindow

structure NavierStokes.BasePrefixIdentity.VelocityMatches (h : ℝ) (d : SlowBorelBase.Coefficients) (f : SlowExpansionResidual.SlowProfiles) : Prop

Only scalar coefficient values and the actual flux identity are needed to identify the reconstructed velocity.

• phi (n : ℕ) : Set.EqOn (d.phi n) (f.phi n) profileWindow
• axial (n : ℕ) : Set.EqOn (d.axial n) (f.axial n) profileWindow
• flux (n : ℕ) : Set.EqOn (SlowDivergence.radialFlux h (SlowExpansionResidual.slowOrder h n) (d.axial n)) (f.flux n) profileWindow

theorem NavierStokes.BasePrefixIdentity.finiteProfile_eq_of_values (J : ℕ) (h b : ℝ) {f g : ℕ → SlowBorelBase.Inner → ℝ} {p : SlowBorelBase.Chart} (he : ∀ n ≤ J, f n (SimilarityProfile.inner h p) = g n (SimilarityProfile.inner h p)) : SlowExpansionResidual.finiteProfile J h b f p = SlowExpansionResidual.finiteProfile J h b g p

theorem NavierStokes.BasePrefixIdentity.prefixVelocity_eq_slowVelocity {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {f : SlowExpansionResidual.SlowProfiles} (hm : VelocityMatches h d f) (J : ℕ) (C : ℝ) {t : ℝ} (ht : t < 1) (x : ProblemStatement.Space) (hs : 0 < AxisymmetricFields.radialEnergy x) : BaseResidual.prefixVelocity J h C d (t, x) = SlowExpansionResidual.slowVelocity J h C f (t, x)

theorem NavierStokes.BasePrefixIdentity.prefixVelocity_germ {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {f : SlowExpansionResidual.SlowProfiles} (hm : VelocityMatches h d f) (J : ℕ) (C : ℝ) {z : ProblemStatement.SpaceTime} (hz : z ∈ BaseResidual.annularPast) : BaseResidual.prefixVelocity J h C d =ᶠ[nhds z] SlowExpansionResidual.slowVelocity J h C f

theorem NavierStokes.BasePrefixIdentity.velocityMatches_of_beta (h : ℝ) (d : SlowBorelBase.Coefficients) (beta : ℕ → SlowBorelBase.Inner → ℝ) (hb : ∀ (n : ℕ), ∀ w ∈ profileWindow, w.1 * beta n w = SlowDivergence.radialFlux h (SlowExpansionResidual.slowOrder h n) (d.axial n) w) : VelocityMatches h d (SlowResidualMatching.ofBeta d.phi d.axial beta d.pressure)

In the regular radial-quotient convention, the sole radial input is the proved identity X * beta = radialFlux; it determines the finite curl.

structure NavierStokes.BasePrefixIdentity.CoefficientMatches (h C : ℝ) (d : SlowBorelBase.Coefficients) (f : SlowExpansionResidual.SlowProfiles) extends NavierStokes.BasePrefixIdentity.VelocityMatches h d f : Prop

The remaining agreements concern scalar pressure and the actual canonical stress primitives. No finite-field or residual identity is an input.

• phi (n : ℕ) : Set.EqOn (d.phi n) (f.phi n) profileWindow
• axial (n : ℕ) : Set.EqOn (d.axial n) (f.axial n) profileWindow
• flux (n : ℕ) : Set.EqOn (SlowDivergence.radialFlux h (SlowExpansionResidual.slowOrder h n) (d.axial n)) (f.flux n) profileWindow
• pressure (n : ℕ) : Set.EqOn (d.pressure n) (f.pressure n) profileWindow
• stressTheta (n : ℕ) : Set.EqOn (d.stressTheta n) (SlowResidualMatching.thetaStress h C f n) profileWindow
• stressAxial (n : ℕ) : Set.EqOn (d.stressAxial n) (SlowResidualMatching.zStress h f n) profileWindow

theorem NavierStokes.BasePrefixIdentity.coefficient_germ {f g : SlowBorelBase.Inner → ℝ} (he : Set.EqOn f g profileWindow) {w : SlowBorelBase.Inner} (hw : w ∈ profileWindow) : f =ᶠ[nhds w] g

theorem NavierStokes.BasePrefixIdentity.prefixProfile_germ_of_coefficients {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (J : ℕ) (b : ℝ) {f g : ℕ → SlowBorelBase.Inner → ℝ} (he : ∀ (n : ℕ), Set.EqOn (f n) (g n) profileWindow) {p : SlowBorelBase.Chart} (ht : p.1 < 1) (hs : 0 < p.2.1) : SlowBorelBase.physicalUncutPrefix h b f J =ᶠ[nhds p] SlowExpansionResidual.finiteProfile J h b g

theorem NavierStokes.BasePrefixIdentity.prefixPressure_germ {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} {f : SlowExpansionResidual.SlowProfiles} (hm : CoefficientMatches h C d f) (J : ℕ) {z : ProblemStatement.SpaceTime} (hz : z ∈ BaseResidual.annularPast) : BaseResidual.prefixPressure J h C d =ᶠ[nhds z] SlowExpansionResidual.slowPressureField J h f

theorem NavierStokes.BasePrefixIdentity.radialDivergence_congr_germ (k : ℝ) {f g : SlowBorelBase.Chart → ℝ} {p : SlowBorelBase.Chart} (he : f =ᶠ[nhds p] g) : LeadingStress.radialDivergence k f p = LeadingStress.radialDivergence k g p

theorem NavierStokes.BasePrefixIdentity.prefixStressForce_eq {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} {f : SlowExpansionResidual.SlowProfiles} (hm : CoefficientMatches h C d f) (J : ℕ) {z : ProblemStatement.SpaceTime} (hz : z ∈ BaseResidual.annularPast) : BaseResidual.prefixStressForce J h C d z = SlowResidualMatching.tangentialStressForce (SlowResidualMatching.physicalThetaStress J h C f) (SlowResidualMatching.physicalZStress J h f) z.1 z.2

theorem NavierStokes.BasePrefixIdentity.VelocityMatches.phi_contDiffAt {h : ℝ} {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {f : SlowExpansionResidual.SlowProfiles} (hm : VelocityMatches h d f) (n : ℕ) {w : SlowBorelBase.Inner} (hw : w ∈ profileWindow) : ContDiffAt ℝ (↑⊤) (f.phi n) w

theorem NavierStokes.BasePrefixIdentity.VelocityMatches.axial_contDiffAt {h : ℝ} {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {f : SlowExpansionResidual.SlowProfiles} (hm : VelocityMatches h d f) (n : ℕ) {w : SlowBorelBase.Inner} (hw : w ∈ profileWindow) : ContDiffAt ℝ (↑⊤) (f.axial n) w

theorem NavierStokes.BasePrefixIdentity.VelocityMatches.flux_contDiffAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {f : SlowExpansionResidual.SlowProfiles} (hm : VelocityMatches h d f) (n : ℕ) {w : SlowBorelBase.Inner} (hw : w ∈ profileWindow) : ContDiffAt ℝ (↑⊤) (f.flux n) w

theorem NavierStokes.BasePrefixIdentity.CoefficientMatches.pressure_contDiffAt {h C : ℝ} {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {f : SlowExpansionResidual.SlowProfiles} (hm : CoefficientMatches h C d f) (n : ℕ) {w : SlowBorelBase.Inner} (hw : w ∈ profileWindow) : ContDiffAt ℝ (↑⊤) (f.pressure n) w

theorem NavierStokes.BasePrefixIdentity.finiteIdentities_of_coefficients {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {f : SlowExpansionResidual.SlowProfiles} (hm : CoefficientMatches h C d f) (hTheta : ∀ (n : ℕ), SlowStressSupport.Smooth (Set.Ioo (-1) 1) (SlowResidualMatching.thetaDensity h C f n)) (hZ : ∀ (n : ℕ), SlowStressSupport.Smooth (Set.Ioo (-1) 1) (SlowResidualMatching.zDensity h f n)) (hp : ∀ (n : ℕ), ∀ w ∈ profileWindow, SlowExpansionResidual.pressureCoefficient h C f n w = 0) : BaseResidual.FiniteIdentities h C d f

The finite identity required by the Borel residual estimates, now derived from the actual finite potentials and scalar recurrence data.

theorem NavierStokes.ConstructedSlowBase.admissibleScales_mono {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} {f : ℕ → SlowBorelBase.Inner → V} {K K' : Set SlowBorelBase.Inner} (ha : SlowBorelBase.AdmissibleScales h f K a) (hK : K' ⊆ K) : SlowBorelBase.AdmissibleScales h f K' a

Restricting the compact set preserves the very same cutoff schedule.

noncomputable def NavierStokes.ConstructedSlowBase.potential (a : ℕ → ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : ProblemStatement.VelocityField

The genuine smooth vector potential of the summed base.

Equations

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

theorem NavierStokes.ConstructedSlowBase.velocity_eq_curl_potential (a : ℕ → ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : SlowBorelBase.baseVelocity a h C d = SpatialCurl.spatialCurl (potential a h C d)

theorem NavierStokes.ConstructedSlowBase.potential_smooth {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (C : ℝ) : ContDiffOn ℝ (↑⊤) (potential a h C d) BaseResidual.past

theorem NavierStokes.ConstructedSlowBase.repaired_coefficientMatches {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 : AssembledSlowBase.ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) : BasePrefixIdentity.CoefficientMatches h C (AssembledSlowBase.coefficients L B0 Z0 hI) (GlobalSlowProfiles.asSlowProfiles s)

The only base flux premise is the actual mass reconstruction. Every positive-order flux is reconstructed by the global recursion itself.

theorem NavierStokes.ConstructedSlowBase.repaired_finiteIdentities {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 : AssembledSlowBase.ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) (hh : 0 < h) (hh1 : h < 1 / 2) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) (hp : ∀ (n : ℕ), ∀ w ∈ BasePrefixIdentity.profileWindow, SlowExpansionResidual.pressureCoefficient h C (GlobalSlowProfiles.asSlowProfiles s) n w = 0) : BaseResidual.FiniteIdentities h C (AssembledSlowBase.coefficients L B0 Z0 hI) (GlobalSlowProfiles.asSlowProfiles s)

The finite Cartesian PDE identity is derived from scalar equations and the actual stream primitives, using the proved finite-prefix bridge.

theorem NavierStokes.ConstructedSlowBase.repaired_stressZeroCore {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 : AssembledSlowBase.ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) : BaseResidual.StressZeroCore (AssembledSlowBase.coefficients L B0 Z0 hI) (inner / 8)

noncomputable def NavierStokes.ConstructedSlowBase.regularDomain {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hI : Set.Icc (-1) 1 ⊆ S) : Set SlowBorelBase.Inner

One open coefficient neighborhood contains the whole physical parameter band and avoids the coordinate denominator's zeros.

Equations

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

theorem NavierStokes.ConstructedSlowBase.regularDomain_open {S : Set ℝ} {h C : ℝ} {s : GlobalSlowProfiles.Scheme S h C} (hI : Set.Icc (-1) 1 ⊆ S) : IsOpen (regularDomain s hI)

theorem NavierStokes.ConstructedSlowBase.innerBox_subset_regularDomain {S : Set ℝ} {h C : ℝ} {s : GlobalSlowProfiles.Scheme S h C} (hI : Set.Icc (-1) 1 ⊆ S) (hh : 0 < h) (hh1 : h < 1 / 2) (lo hi : ℝ) : SlowBorelBase.innerBox lo hi ⊆ regularDomain s hI

theorem NavierStokes.ConstructedSlowBase.regular_fields_eq {S : Set ℝ} {h C : ℝ} {s : GlobalSlowProfiles.Scheme S h C} (hI : Set.Icc (-1) 1 ⊆ S) (n : ℕ) {w : SlowBorelBase.Inner} (hw : w ∈ regularDomain s hI) (hX : 0 ≤ w.1) : (GlobalSlowProfiles.asSlowProfiles s).phi n w = AssembledSlowBase.extendedCoefficient s hI n 0 w ∧ (GlobalSlowProfiles.asSlowProfiles s).axial n w = AssembledSlowBase.extendedCoefficient s hI n 1 w ∧ (GlobalSlowProfiles.asSlowProfiles s).flux n w = w.1 * AssembledSlowBase.extendedCoefficient s hI n 2 w

theorem NavierStokes.ConstructedSlowBase.repaired_jetRate {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 : AssembledSlowBase.ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (P : BaseResidual.PhysicalApproach l h 0 hi) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C (AssembledSlowBase.coefficients L B0 Z0 hI)) (SlowBorelBase.innerBox 0 hi) a) (hf : BaseResidual.FiniteIdentities h C (AssembledSlowBase.coefficients L B0 Z0 hI) (GlobalSlowProfiles.asSlowProfiles s)) (m : ℕ) (n : ℝ) (hn : 0 ≤ n) : DiagonalResidual.JetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (BaseResidual.baseResidual a h C (AssembledSlowBase.coefficients L B0 Z0 hI)) m n

Every fixed physical derivative has every requested power of decay, including on approaches that meet the symmetry axis.

theorem NavierStokes.ConstructedSlowBase.repaired_allJetsFlat {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 : AssembledSlowBase.ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (P : BaseResidual.PhysicalApproach l h 0 hi) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C (AssembledSlowBase.coefficients L B0 Z0 hI)) (SlowBorelBase.innerBox 0 hi) a) (hf : BaseResidual.FiniteIdentities h C (AssembledSlowBase.coefficients L B0 Z0 hI) (GlobalSlowProfiles.asSlowProfiles s)) : ResidualStability.AllJetsFlat l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (BaseResidual.baseResidual a h C (AssembledSlowBase.coefficients L B0 Z0 hI))

theorem NavierStokes.ConstructedSlowBase.repaired_higherInteriorSupport {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 : AssembledSlowBase.ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) (hbase : s.base.beta = GlobalSlowProfiles.betaFromU ⋯ 0 s.base.axial) {left right : ℝ} (hl : Real.exp left < inner / 8) (hr : s.B ^ 2 / 2 < Real.exp right) : BaseResidual.HigherInteriorSupport (AssembledSlowBase.coefficients L B0 Z0 hI) left right

Exterior confinement is a consequence of the five repaired rows, not an extra hypothesis on higher-order stress coefficients.

theorem NavierStokes.ConstructedSlowBase.height_pos {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : 0 < F.data.h

theorem NavierStokes.ConstructedSlowBase.height_lt_half {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : F.data.h < 1 / 2

theorem NavierStokes.ConstructedSlowBase.nominal_coefficientMatches {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : BasePrefixIdentity.CoefficientMatches F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W) (GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.nominalScheme W))

theorem NavierStokes.ConstructedSlowBase.nominal_finiteIdentities {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : BaseResidual.FiniteIdentities F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W) (GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.nominalScheme W))

theorem NavierStokes.ConstructedSlowBase.nominal_stressZeroCore {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : BaseResidual.StressZeroCore (AssembledSlowBase.nominalCoefficients W) (AssembledSlowBase.nominalInner W / 8)

theorem NavierStokes.ConstructedSlowBase.nominal_jetRate {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {hi : ℝ} (P : BaseResidual.PhysicalApproach l F.data.h 0 hi) (ha : SlowBorelBase.AdmissibleScales F.data.h (SlowBorelBase.coefficientBundle W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) (SlowBorelBase.innerBox 0 hi) a) (m : ℕ) (n : ℝ) (hn : 0 ≤ n) : DiagonalResidual.JetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1) (BaseResidual.baseResidual a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) m n

theorem NavierStokes.ConstructedSlowBase.nominal_allJetsFlat {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {hi : ℝ} (P : BaseResidual.PhysicalApproach l F.data.h 0 hi) (ha : SlowBorelBase.AdmissibleScales F.data.h (SlowBorelBase.coefficientBundle W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) (SlowBorelBase.innerBox 0 hi) a) : ResidualStability.AllJetsFlat l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1) (BaseResidual.baseResidual a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W))

theorem NavierStokes.ConstructedSlowBase.nominal_higherInteriorSupport {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {left right : ℝ} (hl : Real.exp left < AssembledSlowBase.nominalInner W / 8) (hr : AssembledSlowBase.nominalOuterX W < Real.exp right) : BaseResidual.HigherInteriorSupport (AssembledSlowBase.nominalCoefficients W) left right

theorem NavierStokes.ConstructedSlowBase.nominal_leading_axis {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {eta : ℝ} (heta : eta ∈ Set.Icc (-1) 1) : (AssembledSlowBase.nominalCoefficients W).axial 0 (0, eta) = 4 * eta + W.axis.j

The leading coefficient retains the actual natural axis datum.

theorem NavierStokes.ConstructedSlowBase.nominal_leading_origin {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : (AssembledSlowBase.nominalCoefficients W).axial 0 (0, 0) = W.axis.j

theorem NavierStokes.ConstructedSlowBase.nominal_origin {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {a : ℕ → ℕ} (ha : StrictMono a) {t : ℝ} (ht : t < 1) : SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W) (t, 0) = ((1 - t) ^ (-CoordinateAlgebra.A F.data.h) * W.axis.j) • ProblemStatement.coordinateVector 2

theorem NavierStokes.ConstructedSlowBase.nominal_axis_tendsto {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {a : ℕ → ℕ} (ha : StrictMono a) : Filter.Tendsto (fun (t : ℝ) => ‖SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W) (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

theorem NavierStokes.ConstructedSlowBase.nominal_speedUnbounded {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {a : ℕ → ℕ} (ha : StrictMono a) : ProblemStatement.SpeedUnboundedAtOne (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W))

theorem NavierStokes.ConstructedSlowBase.nominal_velocity_smooth {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {a : ℕ → ℕ} (ha : StrictMono a) : ContDiffOn ℝ (↑⊤) (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) BaseResidual.past

theorem NavierStokes.ConstructedSlowBase.nominal_pressure_smooth {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {a : ℕ → ℕ} (ha : StrictMono a) : ContDiffOn ℝ (↑⊤) (SlowBorelBase.basePressure a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) BaseResidual.past

theorem NavierStokes.ConstructedSlowBase.nominal_stressForce_smooth {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {a : ℕ → ℕ} (ha : StrictMono a) : ContDiffOn ℝ (↑⊤) (BaseResidual.baseStressForce a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) BaseResidual.past

theorem NavierStokes.ConstructedSlowBase.nominal_residual_smooth {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {a : ℕ → ℕ} (ha : StrictMono a) : ContDiffOn ℝ (↑⊤) (BaseResidual.baseResidual a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) BaseResidual.past

theorem NavierStokes.ConstructedSlowBase.nominal_divergence_zero {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {a : ℕ → ℕ} (ha : StrictMono a) {t : ℝ} (ht : t < 1) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) t x = 0

theorem NavierStokes.ConstructedSlowBase.modified_coefficientMatches {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) : BasePrefixIdentity.CoefficientMatches F.data.h W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M) (GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.modifiedScheme W Q M))

theorem NavierStokes.ConstructedSlowBase.modified_finiteIdentities {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) : BaseResidual.FiniteIdentities F.data.h W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M) (GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.modifiedScheme W Q M))

theorem NavierStokes.ConstructedSlowBase.modified_stressZeroCore {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) : BaseResidual.StressZeroCore (AssembledSlowBase.modifiedCoefficients W Q M) (AssembledSlowBase.nominalInner W / 8)

theorem NavierStokes.ConstructedSlowBase.modified_jetRate {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {upper : ℝ} (P : BaseResidual.PhysicalApproach l F.data.h 0 upper) (ha : SlowBorelBase.AdmissibleScales F.data.h (SlowBorelBase.coefficientBundle W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M)) (SlowBorelBase.innerBox 0 upper) a) (m : ℕ) (n : ℝ) (hn : 0 ≤ n) : DiagonalResidual.JetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1) (BaseResidual.baseResidual a F.data.h W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M)) m n

theorem NavierStokes.ConstructedSlowBase.modified_allJetsFlat {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {upper : ℝ} (P : BaseResidual.PhysicalApproach l F.data.h 0 upper) (ha : SlowBorelBase.AdmissibleScales F.data.h (SlowBorelBase.coefficientBundle W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M)) (SlowBorelBase.innerBox 0 upper) a) : ResidualStability.AllJetsFlat l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1) (BaseResidual.baseResidual a F.data.h W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M))

theorem NavierStokes.ConstructedSlowBase.modified_higherInteriorSupport {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {left right : ℝ} (hl : Real.exp left < AssembledSlowBase.nominalInner W / 8) (hr : AssembledSlowBase.nominalOuterX W < Real.exp right) : BaseResidual.HigherInteriorSupport (AssembledSlowBase.modifiedCoefficients W Q M) left right

theorem NavierStokes.ConstructedSlowBase.modified_leading_axis {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {eta : ℝ} (heta : eta ∈ Set.Icc (-1) 1) : (AssembledSlowBase.modifiedCoefficients W Q M).axial 0 (0, eta) = 4 * eta + W.axis.j

theorem NavierStokes.ConstructedSlowBase.modified_leading_origin {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) : (AssembledSlowBase.modifiedCoefficients W Q M).axial 0 (0, 0) = W.axis.j

theorem NavierStokes.ConstructedSlowBase.modified_origin {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {a : ℕ → ℕ} (ha : StrictMono a) {t : ℝ} (ht : t < 1) : SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M) (t, 0) = ((1 - t) ^ (-CoordinateAlgebra.A F.data.h) * W.axis.j) • ProblemStatement.coordinateVector 2

theorem NavierStokes.ConstructedSlowBase.modified_axis_tendsto {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {a : ℕ → ℕ} (ha : StrictMono a) : Filter.Tendsto (fun (t : ℝ) => ‖SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M) (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

theorem NavierStokes.ConstructedSlowBase.modified_speedUnbounded {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {a : ℕ → ℕ} (ha : StrictMono a) : ProblemStatement.SpeedUnboundedAtOne (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M))

def NavierStokes.ConstructedSlowBase.WeightedStressBound (a : ℕ → ℕ) (h : ℝ) (d : SlowBorelBase.Coefficients) (c left right : ℝ) : Prop

The actual two-slot, all-order weighted estimate, used only as an output of the coefficient construction and common schedule selection.

Equations

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

theorem NavierStokes.ConstructedSlowBase.weighted_on_actual_scales {a : ℕ → ℕ} {h C : ℝ} (hh : 0 < h) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {c left right inner cut : ℝ} (hc : 0 < c) (hl : Real.exp left < inner) (hi : inner ≤ cut) (hr : cut < Real.exp right) (hs : BaseResidual.HigherInteriorSupport d left right) (hz : ∀ (w : SlowBorelBase.Inner), w.1 < inner → BaseResidual.stressPair d 1 w = 0) (ho : BaseResidual.PolynomialEdgeJets (BaseResidual.outerWindow cut right) (BaseResidual.activeZeta c left right) (BaseResidual.activeDelta left right) (BaseResidual.stressPair d 1)) {K : Set SlowBorelBase.Inner} (hK : IsCompact K) (hWK : BaseResidual.activeWindow left right ⊆ K) (ha : SlowBorelBase.AdmissibleScales h (BaseResidual.weightedBundle C d (BaseResidual.activeZeta c left right)) K a) : WeightedStressBound a h d c left right

This form uses actual derivative bounds on the closed parameter band. It requires no ambient germ equality to an auxiliary extension at eta=±1.

theorem NavierStokes.ConstructedSlowBase.firstStress_edgeJets (Cedge : ℝ) (tail : OutgoingTail.TailData) (y0 : ℝ) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {c left width inner : ℝ} (hc : 0 < c) (hw : 0 < width) (hl : Real.exp left < inner) (hi : inner ≤ Real.exp (y0 + 3 - width)) (hz : ∀ (w : SlowBorelBase.Inner), w.1 < inner → BaseResidual.stressPair d 1 w = 0) (he : ∀ w ∈ BaseResidual.outerWindow (Real.exp (y0 + 3 - width)) (y0 + 3), BaseResidual.stressPair d 1 =ᶠ[nhds w] fun (v : SlowBorelBase.Inner) => (SlowFirstOrderEdge.stressX Cedge tail y0 v, 0)) : BaseResidual.PolynomialEdgeJets (BaseResidual.activeWindow left (y0 + 3)) (BaseResidual.activeZeta c left (y0 + 3)) (BaseResidual.activeDelta left (y0 + 3)) (BaseResidual.stressPair d 1)

The terminal amplitude and the normalization of the slow swirl field are independent constants. This proof keeps them independent.

theorem NavierStokes.ConstructedSlowBase.exists_common_scales_from_primitive {h : ℝ} (hh : 0 < h) (Cbase Cedge : ℝ) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (tail : OutgoingTail.TailData) (y0 : ℝ) {c left width inner : ℝ} (hc : 0 < c) (hw : 0 < width) (hl : Real.exp left < inner) (hi : inner ≤ Real.exp (y0 + 3 - width)) (hs : BaseResidual.HigherInteriorSupport d left (y0 + 3)) (hz : ∀ (w : SlowBorelBase.Inner), w.1 < inner → BaseResidual.stressPair d 1 w = 0) (he : ∀ w ∈ BaseResidual.outerWindow (Real.exp (y0 + 3 - width)) (y0 + 3), BaseResidual.stressPair d 1 =ᶠ[nhds w] fun (v : SlowBorelBase.Inner) => (SlowFirstOrderEdge.stressX Cedge tail y0 v, 0)) {K : Set SlowBorelBase.Inner} (hK : IsCompact K) (hWK : BaseResidual.activeWindow left (y0 + 3) ⊆ K) (B : ℕ) : ∃ (a : ℕ → ℕ), B ≤ a 0 ∧ SlowBorelBase.AdmissibleScales h (BaseResidual.weightedBundle Cbase d (BaseResidual.activeZeta c left (y0 + 3))) K a ∧ SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle Cbase d) K a ∧ WeightedStressBound a h d c left (y0 + 3)

Choose one sequence for the actual seven-component stream bundle and the higher stress quotients. The weighted estimate is then derived.

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

Active left, given by Real.log (nominalInner W / 16).

Equations

• NavierStokes.ConstructedSlowBase.activeLeft W = Real.log (NavierStokes.AssembledSlowBase.nominalInner W / 16)

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

Terminal shift, given by TerminalHistoryBridge.shift F W.controls.radius.

Equations

• NavierStokes.ConstructedSlowBase.terminalShift W = NavierStokes.TerminalHistoryBridge.shift F W.controls.radius

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

Active right, given by terminalShift W + 3.

Equations

• NavierStokes.ConstructedSlowBase.activeRight W = NavierStokes.ConstructedSlowBase.terminalShift W + 3

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

Active upper, given by Real.exp (activeRight W).

Equations

• NavierStokes.ConstructedSlowBase.activeUpper W = Real.exp (NavierStokes.ConstructedSlowBase.activeRight W)

noncomputable def NavierStokes.ConstructedSlowBase.scaleUpper {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (upper : ℝ) : ℝ

Scale upper, given by max upper (activeUpper W).

Equations

• NavierStokes.ConstructedSlowBase.scaleUpper W upper = max upper (NavierStokes.ConstructedSlowBase.activeUpper W)

theorem NavierStokes.ConstructedSlowBase.exp_activeLeft {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : Real.exp (activeLeft W) = AssembledSlowBase.nominalInner W / 16

theorem NavierStokes.ConstructedSlowBase.activeLeft_margin {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : Real.exp (activeLeft W) < AssembledSlowBase.nominalInner W / 8

theorem NavierStokes.ConstructedSlowBase.core_before_outer {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : AssembledSlowBase.nominalInner W / 8 < AssembledSlowBase.nominalOuterX W

theorem NavierStokes.ConstructedSlowBase.switch_before_collar {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : BaseExterior.nominalHeatSwitch W < Real.exp (terminalShift W + 2)

theorem NavierStokes.ConstructedSlowBase.outer_before_collar {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : AssembledSlowBase.nominalOuterX W < Real.exp (terminalShift W + 2)

theorem NavierStokes.ConstructedSlowBase.collar_before_upper {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : Real.exp (terminalShift W + 2) < activeUpper W

theorem NavierStokes.ConstructedSlowBase.outer_before_upper {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : AssembledSlowBase.nominalOuterX W < activeUpper W

theorem NavierStokes.ConstructedSlowBase.core_before_collar {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : AssembledSlowBase.nominalInner W / 8 ≤ Real.exp (terminalShift W + 3 - 1)

theorem NavierStokes.ConstructedSlowBase.activeLeft_before_collar {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : activeLeft W < terminalShift W + 2

theorem NavierStokes.ConstructedSlowBase.activeEdges_ordered {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : activeLeft W < activeRight W

theorem NavierStokes.ConstructedSlowBase.scaleUpper_pos {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (upper : ℝ) : 0 < scaleUpper W upper

theorem NavierStokes.ConstructedSlowBase.activeWindow_subset_box {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (upper : ℝ) : BaseResidual.activeWindow (activeLeft W) (activeRight W) ⊆ SlowBorelBase.innerBox 0 (scaleUpper W upper)

theorem NavierStokes.ConstructedSlowBase.nominal_higher_support {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : BaseResidual.HigherInteriorSupport (AssembledSlowBase.nominalCoefficients W) (activeLeft W) (activeRight W)

theorem NavierStokes.ConstructedSlowBase.nominal_quotients_smooth {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {c : ℝ} (hc : 0 < c) (j : ℕ) : ContDiff ℝ (↑⊤) (BaseResidual.higherStressQuotient (AssembledSlowBase.nominalCoefficients W) (BaseResidual.activeZeta c (activeLeft W) (activeRight W)) j)

theorem NavierStokes.ConstructedSlowBase.modified_higher_support {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) : BaseResidual.HigherInteriorSupport (AssembledSlowBase.modifiedCoefficients W Q M) (activeLeft W) (activeRight W)

theorem NavierStokes.ConstructedSlowBase.modified_quotients_smooth {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {c : ℝ} (hc : 0 < c) (j : ℕ) : ContDiff ℝ (↑⊤) (BaseResidual.higherStressQuotient (AssembledSlowBase.modifiedCoefficients W Q M) (BaseResidual.activeZeta c (activeLeft W) (activeRight W)) j)

noncomputable def NavierStokes.ConstructedSlowBase.nominalScales {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : ℕ → ℕ

This is one actual choice for the enlarged bundle. The ordinary base schedule and the weighted stress estimate use this very same function.

Equations

• NavierStokes.ConstructedSlowBase.nominalScales W c hc upper B = Classical.choose ⋯

theorem NavierStokes.ConstructedSlowBase.nominalScales_spec {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : B ≤ nominalScales W c hc upper B 0 ∧ SlowBorelBase.AdmissibleScales F.data.h (BaseResidual.weightedBundle W.axis.normalization (AssembledSlowBase.nominalCoefficients W) (BaseResidual.activeZeta c (activeLeft W) (activeRight W))) (SlowBorelBase.innerBox 0 (scaleUpper W upper)) (nominalScales W c hc upper B)

theorem NavierStokes.ConstructedSlowBase.nominalScales_admissible {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : SlowBorelBase.AdmissibleScales F.data.h (SlowBorelBase.coefficientBundle W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) (SlowBorelBase.innerBox 0 (scaleUpper W upper)) (nominalScales W c hc upper B)

theorem NavierStokes.ConstructedSlowBase.nominalScales_strictMono {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : StrictMono (nominalScales W c hc upper B)

theorem NavierStokes.ConstructedSlowBase.nominalScales_admissible_on {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {lo hi : ℝ} (hlo : 0 ≤ lo) (hhi : hi ≤ scaleUpper W upper) : SlowBorelBase.AdmissibleScales F.data.h (SlowBorelBase.coefficientBundle W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) (SlowBorelBase.innerBox lo hi) (nominalScales W c hc upper B)

theorem NavierStokes.ConstructedSlowBase.nominalScales_jetRate {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {l : Filter ProblemStatement.SpaceTime} {hi : ℝ} (P : BaseResidual.PhysicalApproach l F.data.h 0 hi) (hhi : hi ≤ scaleUpper W upper) (m : ℕ) (n : ℝ) (hn : 0 ≤ n) : DiagonalResidual.JetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1) (BaseResidual.baseResidual (nominalScales W c hc upper B) F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) m n

theorem NavierStokes.ConstructedSlowBase.nominalScales_allJetsFlat {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {l : Filter ProblemStatement.SpaceTime} {hi : ℝ} (P : BaseResidual.PhysicalApproach l F.data.h 0 hi) (hhi : hi ≤ scaleUpper W upper) : ResidualStability.AllJetsFlat l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1) (BaseResidual.baseResidual (nominalScales W c hc upper B) F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W))

theorem NavierStokes.ConstructedSlowBase.nominalScales_origin {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {t : ℝ} (ht : t < 1) : SlowBorelBase.baseVelocity (nominalScales W c hc upper B) F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W) (t, 0) = ((1 - t) ^ (-CoordinateAlgebra.A F.data.h) * W.axis.j) • ProblemStatement.coordinateVector 2

theorem NavierStokes.ConstructedSlowBase.nominalScales_speedUnbounded {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : ProblemStatement.SpeedUnboundedAtOne (SlowBorelBase.baseVelocity (nominalScales W c hc upper B) F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W))

theorem NavierStokes.ConstructedSlowBase.nominalScales_smooth_and_divergence {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : ContDiffOn ℝ (↑⊤) (SlowBorelBase.baseVelocity (nominalScales W c hc upper B) F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) BaseResidual.past ∧ ContDiffOn ℝ (↑⊤) (SlowBorelBase.basePressure (nominalScales W c hc upper B) F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) BaseResidual.past ∧ ∀ t < 1, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence (SlowBorelBase.baseVelocity (nominalScales W c hc upper B) F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) t x = 0

theorem NavierStokes.ConstructedSlowBase.nominalScales_potential_smooth {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : ContDiffOn ℝ (↑⊤) (potential (nominalScales W c hc upper B) F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) BaseResidual.past

theorem NavierStokes.ConstructedSlowBase.nominalScales_tangential_bound {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {lo hi : ℝ} (hlo : 0 < lo) (hhi : hi ≤ scaleUpper W upper) (m : ℕ) : ∃ (D : ℝ), 0 < D ∧ ∀ (q : ℝ), 0 < q → q ≤ 1 → ∀ w ∈ SlowBorelBase.innerBox lo hi, ‖SlowBorelBase.blownJet m (fun (y : SlowBorelBase.Chart) => SlowBorelBase.normalizedSwirl (nominalScales W c hc upper B) F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W) y - SlowBorelBase.leadingSwirl W.axis.normalization (AssembledSlowBase.nominalCoefficients W) y.2) (q, w)‖ ≤ D * q ^ (2 * F.data.h) ∧ ‖SlowBorelBase.blownJet m (fun (y : SlowBorelBase.Chart) => SlowBorelBase.slowSum (nominalScales W c hc upper B) F.data.h (AssembledSlowBase.nominalCoefficients W).axial y - (AssembledSlowBase.nominalCoefficients W).axial 0 y.2) (q, w)‖ ≤ D * q ^ (2 * F.data.h)

theorem NavierStokes.ConstructedSlowBase.nominalScales_exterior_residual_zero {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {z : ProblemStatement.SpaceTime} (hz : z ∈ BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W)) : ProblemStatement.navierStokesResidual (SlowBorelBase.baseVelocity (nominalScales W c hc upper B) F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) (SlowBorelBase.basePressure (nominalScales W c hc upper B) F.data.h W.axis.normalization (AssembledSlowBase.nominalCoefficients W)) z.1 z.2 = 0

noncomputable def NavierStokes.ConstructedSlowBase.modifiedScales {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) : ℕ → ℕ

The modified family gets one schedule, derived from its actual repaired coefficients. No stress estimate enters this definition.

Equations

• NavierStokes.ConstructedSlowBase.modifiedScales W c hc upper B Q M = Classical.choose ⋯

theorem NavierStokes.ConstructedSlowBase.modifiedScales_spec {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) : B ≤ modifiedScales W c hc upper B Q M 0 ∧ SlowBorelBase.AdmissibleScales F.data.h (BaseResidual.weightedBundle W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M) (BaseResidual.activeZeta c (activeLeft W) (activeRight W))) (SlowBorelBase.innerBox 0 (scaleUpper W upper)) (modifiedScales W c hc upper B Q M)

theorem NavierStokes.ConstructedSlowBase.modifiedScales_admissible {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) : SlowBorelBase.AdmissibleScales F.data.h (SlowBorelBase.coefficientBundle W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M)) (SlowBorelBase.innerBox 0 (scaleUpper W upper)) (modifiedScales W c hc upper B Q M)

theorem NavierStokes.ConstructedSlowBase.modifiedScales_strictMono {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) : StrictMono (modifiedScales W c hc upper B Q M)

theorem NavierStokes.ConstructedSlowBase.modifiedScales_allJetsFlat {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {l : Filter ProblemStatement.SpaceTime} {radius : ℝ} (P : BaseResidual.PhysicalApproach l F.data.h 0 radius) (hr : radius ≤ scaleUpper W upper) : ResidualStability.AllJetsFlat l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1) (BaseResidual.baseResidual (modifiedScales W c hc upper B Q M) F.data.h W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M))

theorem NavierStokes.ConstructedSlowBase.modifiedScales_origin {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {t : ℝ} (ht : t < 1) : SlowBorelBase.baseVelocity (modifiedScales W c hc upper B Q M) F.data.h W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M) (t, 0) = ((1 - t) ^ (-CoordinateAlgebra.A F.data.h) * W.axis.j) • ProblemStatement.coordinateVector 2

theorem NavierStokes.ConstructedSlowBase.modifiedScales_speedUnbounded {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) : ProblemStatement.SpeedUnboundedAtOne (SlowBorelBase.baseVelocity (modifiedScales W c hc upper B Q M) F.data.h W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M))

theorem NavierStokes.ConstructedSlowBase.modifiedScales_smooth_and_divergence {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) : ContDiffOn ℝ (↑⊤) (SlowBorelBase.baseVelocity (modifiedScales W c hc upper B Q M) F.data.h W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M)) BaseResidual.past ∧ ContDiffOn ℝ (↑⊤) (SlowBorelBase.basePressure (modifiedScales W c hc upper B Q M) F.data.h W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M)) BaseResidual.past ∧ ∀ t < 1, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence (SlowBorelBase.baseVelocity (modifiedScales W c hc upper B Q M) F.data.h W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M)) t x = 0

theorem NavierStokes.ConstructedSlowBase.modifiedScales_potential_smooth {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) : ContDiffOn ℝ (↑⊤) (potential (modifiedScales W c hc upper B Q M) F.data.h W.axis.normalization (AssembledSlowBase.modifiedCoefficients W Q M)) BaseResidual.past

theorem NavierStokes.ConstructedSlowBase.nominalScales_weighted_bound {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : WeightedStressBound (nominalScales W c hc upper B) F.data.h (AssembledSlowBase.nominalCoefficients W) c (activeLeft W) (activeRight W)

The actual nominal coefficient supplies the terminal derivative bounds; the already selected sequence gives the full weighted stress estimate.

theorem NavierStokes.ConstructedSlowBase.modifiedScales_weighted_bound {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) (hI : ∀ eta ∈ S, Q.I (AssembledSlowBase.nominalOuterX W, eta) = W.profiles.I (AssembledSlowBase.nominalOuterX W, eta)) : WeightedStressBound (modifiedScales W c hc upper B Q M) F.data.h (AssembledSlowBase.modifiedCoefficients W Q M) c (activeLeft W) (activeRight W)

A finite modification additionally retains its literal angular history. This fixes the first-order integration constant; the actual modulation witness proves this equality from its five restored rows.

noncomputable def NavierStokes.ConstructedSlowBase.Modulated.coefficients {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : SlowBorelBase.Coefficients

The coefficients are rebuilt from this particular solved finite modulation, using its preserved histories and its original nominal witness.

Equations

• NavierStokes.ConstructedSlowBase.Modulated.coefficients v = NavierStokes.AssembledSlowBase.modifiedCoefficients W v.profiles ⋯

theorem NavierStokes.ConstructedSlowBase.Modulated.coefficients_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : SlowBorelBase.SmoothCoefficients (coefficients v)

noncomputable def NavierStokes.ConstructedSlowBase.Modulated.scales {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : ℕ → ℕ

Scales, given by modifiedScales W c hc upper B v.profiles v.finiteModification.

Equations

• NavierStokes.ConstructedSlowBase.Modulated.scales v c hc upper B = NavierStokes.ConstructedSlowBase.modifiedScales W c hc upper B v.profiles ⋯

theorem NavierStokes.ConstructedSlowBase.Modulated.scales_spec {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : B ≤ scales v c hc upper B 0 ∧ SlowBorelBase.AdmissibleScales F.data.h (BaseResidual.weightedBundle W.axis.normalization (coefficients v) (BaseResidual.activeZeta c (activeLeft W) (activeRight W))) (SlowBorelBase.innerBox 0 (scaleUpper W upper)) (scales v c hc upper B)

theorem NavierStokes.ConstructedSlowBase.Modulated.scales_admissible {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : SlowBorelBase.AdmissibleScales F.data.h (SlowBorelBase.coefficientBundle W.axis.normalization (coefficients v)) (SlowBorelBase.innerBox 0 (scaleUpper W upper)) (scales v c hc upper B)

theorem NavierStokes.ConstructedSlowBase.Modulated.scales_strictMono {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : StrictMono (scales v c hc upper B)

noncomputable def NavierStokes.ConstructedSlowBase.Modulated.velocity {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : ProblemStatement.VelocityField

Velocity, given by baseVelocity (scales v c hc upper B) F.data.h W.axis.normalization (coefficients v).

Equations

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

noncomputable def NavierStokes.ConstructedSlowBase.Modulated.pressure {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : ProblemStatement.PressureField

Pressure, given by basePressure (scales v c hc upper B) F.data.h W.axis.normalization (coefficients v).

Equations

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

noncomputable def NavierStokes.ConstructedSlowBase.Modulated.stressForce {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : ProblemStatement.SpaceTime → ProblemStatement.Space

Stress force, given by BaseResidual.baseStressForce (scales v c hc upper B) F.data.h W.axis.normalization (coefficients v).

Equations

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

noncomputable def NavierStokes.ConstructedSlowBase.Modulated.error {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : ProblemStatement.SpaceTime → ProblemStatement.Space

Error, given by BaseResidual.baseResidual (scales v c hc upper B) F.data.h W.axis.normalization (coefficients v).

Equations

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

noncomputable def NavierStokes.ConstructedSlowBase.Modulated.vectorPotential {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : ProblemStatement.VelocityField

Vector potential, given by potential (scales v c hc upper B) F.data.h W.axis.normalization (coefficients v).

Equations

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

theorem NavierStokes.ConstructedSlowBase.Modulated.velocity_eq_curl {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : velocity v c hc upper B = SpatialCurl.spatialCurl (vectorPotential v c hc upper B)

theorem NavierStokes.ConstructedSlowBase.Modulated.vectorPotential_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : ContDiffOn ℝ (↑⊤) (vectorPotential v c hc upper B) BaseResidual.past

theorem NavierStokes.ConstructedSlowBase.Modulated.smooth_and_divergence {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : ContDiffOn ℝ (↑⊤) (velocity v c hc upper B) BaseResidual.past ∧ ContDiffOn ℝ (↑⊤) (pressure v c hc upper B) BaseResidual.past ∧ ∀ t < 1, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence (velocity v c hc upper B) t x = 0

theorem NavierStokes.ConstructedSlowBase.Modulated.origin {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {t : ℝ} (ht : t < 1) : velocity v c hc upper B (t, 0) = ((1 - t) ^ (-CoordinateAlgebra.A F.data.h) * W.axis.j) • ProblemStatement.coordinateVector 2

theorem NavierStokes.ConstructedSlowBase.Modulated.speedUnbounded {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : ProblemStatement.SpeedUnboundedAtOne (velocity v c hc upper B)

theorem NavierStokes.ConstructedSlowBase.Modulated.finiteIdentities {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : BaseResidual.FiniteIdentities F.data.h W.axis.normalization (coefficients v) (GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.modifiedScheme W v.profiles ⋯))

theorem NavierStokes.ConstructedSlowBase.Modulated.residual_identity {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) (z : ProblemStatement.SpaceTime) : ProblemStatement.navierStokesResidual (velocity v c hc upper B) (pressure v c hc upper B) z.1 z.2 = stressForce v c hc upper B z + error v c hc upper B z

theorem NavierStokes.ConstructedSlowBase.Modulated.error_allJetsFlat {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {l : Filter ProblemStatement.SpaceTime} {radius : ℝ} (P : BaseResidual.PhysicalApproach l F.data.h 0 radius) (hr : radius ≤ scaleUpper W upper) : ResidualStability.AllJetsFlat l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1) (error v c hc upper B)

theorem NavierStokes.ConstructedSlowBase.Modulated.weighted_bound {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : WeightedStressBound (scales v c hc upper B) F.data.h (coefficients v) c (activeLeft W) (activeRight W)

Every finite identity and support input of this weighted estimate is proved for the same actual modulation witness.

theorem NavierStokes.ConstructedSlowBase.exists_actual_base (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : ∃ (F : OutgoingProfile.Profile) (W : NominalProfile.Witness F) (ld : ModulatedProfileAssembly.LoopData W) (v : ModulatedProfileAssembly.Witness ld), (∀ (p : SlowBorelBase.Inner), NominalConeAssembly.activeLeft W < p.1 → p.1 < NominalConeAssembly.activeRight W → p.2 ∈ Set.Icc (-1) 1 → TrueConeLoop.InTrueCone (ActivationStocks.profileStockOne v.profiles F.data.h p) (ActivationStocks.profileStockTwo v.profiles F.data.h p) (ModulatedCone.angularShear v.profiles.E p) (ModulatedCone.signedAxialShear v.profiles.E v.profiles.U p)) ∧ B ≤ Modulated.scales v c hc upper B 0 ∧ SlowBorelBase.AdmissibleScales F.data.h (BaseResidual.weightedBundle W.axis.normalization (Modulated.coefficients v) (BaseResidual.activeZeta c (activeLeft W) (activeRight W))) (SlowBorelBase.innerBox 0 (scaleUpper W upper)) (Modulated.scales v c hc upper B) ∧ WeightedStressBound (Modulated.scales v c hc upper B) F.data.h (Modulated.coefficients v) c (activeLeft W) (activeRight W) ∧ ContDiffOn ℝ (↑⊤) (Modulated.velocity v c hc upper B) BaseResidual.past ∧ ContDiffOn ℝ (↑⊤) (Modulated.pressure v c hc upper B) BaseResidual.past ∧ (∀ t < 1, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence (Modulated.velocity v c hc upper B) t x = 0) ∧ (∀ t < 1, Modulated.velocity v c hc upper B (t, 0) = ((1 - t) ^ (-CoordinateAlgebra.A F.data.h) * W.axis.j) • ProblemStatement.coordinateVector 2) ∧ ProblemStatement.SpeedUnboundedAtOne (Modulated.velocity v c hc upper B) ∧ ∀ (l : Filter ProblemStatement.SpaceTime) (a : BaseResidual.PhysicalApproach l F.data.h 0 upper), ResidualStability.AllJetsFlat l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1) (Modulated.error v c hc upper B)

An actual nominal profile and its solved finite modulation are chosen by the proved finite construction. The resulting summed base has genuine Cartesian smoothness, incompressibility, weighted stress, exact axial growth, and flat error. There is no profile, PDE identity, or residual estimate among the inputs.