The slow base on the actual entrance-to-terminal annulus

All fields below use the same solved finite modulation and the same aligned coefficient family. The weight exponent is the square of the actual ACT time, and its two endpoints are the endpoints of the nominal cone interval.

Exact exterior of the repaired modulated slow base

The pressure constant is obtained from the restored integral of the squared regular swirl and the unchanged axis pressure. Exterior equality of the swirl alone would not determine this constant.

The scheme interface records the actual extended coefficient formulas. It allows any seed cutoff with the same order-zero profile and outer radius, including the entrance-aligned scheme.

theorem NavierStokes.ModulatedExterior.integral_equal_after {f g : ℝ → ℝ} {B X : ℝ} (hB : 0 ≤ B) (hX : B ≤ X) (hf : ContinuousOn f (Set.Icc 0 X)) (hg : ContinuousOn g (Set.Icc 0 X)) (hanchor : ∫ (r : ℝ) in 0..B, f r = ∫ (r : ℝ) in 0..B, g r) (htail : Set.EqOn f g (Set.Icc B X)) : ∫ (r : ℝ) in 0..X, f r = ∫ (r : ℝ) in 0..X, g r

An actual primitive equality propagates through an unchanged tail.

theorem NavierStokes.ModulatedExterior.squared_swirl_anchor_of_rows {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (h0 : P.pressure0 = Q.pressure0) {p : ProfileHistories.Point} (hrows : ModulatedHistories.profileRows P p = ModulatedHistories.profileRows Q p) : ProfileHistories.primitive (fun (w : ProfileHistories.Point) => P.f w ^ 2) p = ProfileHistories.primitive (fun (w : ProfileHistories.Point) => Q.f w ^ 2) p

The fifth restored row fixes the squared-swirl integral once the actual axis pressure is fixed. This is an identity of integrals, not a pressure boundary condition imposed on the output.

theorem NavierStokes.ModulatedExterior.pressure_equal_after {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') {B X eta : ℝ} (hB : 0 ≤ B) (hX : B ≤ X) (hP : ∀ r ∈ Set.Icc 0 X, (r, eta) ∈ D.carrier) (hQ : ∀ r ∈ Set.Icc 0 X, (r, eta) ∈ D'.carrier) (h0 : P.pressure0 = Q.pressure0) (hanchor : ProfileHistories.primitive (fun (w : ProfileHistories.Point) => P.f w ^ 2) (B, eta) = ProfileHistories.primitive (fun (w : ProfileHistories.Point) => Q.f w ^ 2) (B, eta)) (htail : ∀ r ∈ Set.Icc B X, P.f (r, eta) = Q.f (r, eta)) : P.pressure (X, eta) = Q.pressure (X, eta)

def NavierStokes.ModulatedExterior.RestoredSquaredSwirl {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} : Prop

The additional finite row needed to retain the canonical pressure constant. The existing finite-modification certificate already retains mass.

Equations

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

theorem NavierStokes.ModulatedExterior.modified_fields_after {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) {X eta : ℝ} (hX : AssembledSlowBase.nominalOuterX W ≤ X) (heta : eta ∈ S) : Q.f (X, eta) = W.profiles.f (X, eta) ∧ Q.U (X, eta) = W.profiles.U (X, eta)

theorem NavierStokes.ModulatedExterior.modified_mass_after {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) {X eta : ℝ} (hX : AssembledSlowBase.nominalOuterX W ≤ X) (heta : eta ∈ S) : Q.M (X, eta) = W.profiles.M (X, eta)

The restored mass at one radius is propagated by actual integration.

theorem NavierStokes.ModulatedExterior.modified_pressure_after {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) (henergy : RestoredSquaredSwirl W Q) {X eta : ℝ} (hX : AssembledSlowBase.nominalOuterX W ≤ X) (heta : eta ∈ S) : Q.pressure (X, eta) = W.profiles.pressure (X, eta)

theorem NavierStokes.ModulatedExterior.modified_pressure_canonical_after {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) (henergy : RestoredSquaredSwirl W Q) {X eta : ℝ} (hX : AssembledSlowBase.nominalOuterX W ≤ X) (heta : eta ∈ Set.Icc (-1) 1) : Q.pressure (X, eta) = -∫ (r : ℝ) in Set.Ioi X, Q.f (r, eta) ^ 2

The reconstructed pressure is the actual canonical tail integral in the exterior. Its integration constant was fixed by the restored row.

structure NavierStokes.ModulatedExterior.RealizesScheme {S : Set ℝ} {h C : ℝ} (s : GlobalSlowProfiles.Scheme S h C) (hI : Set.Icc (-1) 1 ⊆ S) (d : SlowBorelBase.Coefficients) : Prop

Literal scalar coefficient formulas. No support or residual assertion is part of this interface, and the inner cutoff is unrestricted.

• phi : d.phi = fun (n : ℕ) => AssembledSlowBase.extendedCoefficient s hI n 0
• axial : d.axial = fun (n : ℕ) => AssembledSlowBase.extendedCoefficient s hI n 1
• pressure : d.pressure = fun (n : ℕ) => AssembledSlowBase.extendedCoefficient s hI n 3

theorem NavierStokes.ModulatedExterior.realizes_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 : AssembledSlowBase.ZeroOrderSolved s inner) (hI : Set.Icc (-1) 1 ⊆ S) : RealizesScheme s hI (AssembledSlowBase.coefficients L B0 Z0 hI)

theorem NavierStokes.ModulatedExterior.realized_zero_fields {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) {s : GlobalSlowProfiles.Scheme S F.data.h W.axis.normalization} {d : SlowBorelBase.Coefficients} (hd : RealizesScheme s ⋯ d) (hbase : s.base = (AssembledSlowBase.modifiedScheme W Q M).base) {p : SlowBorelBase.Inner} (hX : 0 ≤ p.1) (heta : |p.2| ≤ 1) : d.phi 0 p = W.axis.normalization * Q.f p ∧ d.axial 0 p = Q.U p ∧ d.pressure 0 p = Q.pressure p

theorem NavierStokes.ModulatedExterior.realized_positive_exterior {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) {s : GlobalSlowProfiles.Scheme S F.data.h W.axis.normalization} {d : SlowBorelBase.Coefficients} (hd : RealizesScheme s ⋯ d) (houter : s.B = AssembledSlowBase.nominalOuterRadius W) {n : ℕ} (hn : 0 < n) {p : SlowBorelBase.Inner} (hX : AssembledSlowBase.nominalOuterX W ≤ p.1) : d.phi n p = 0 ∧ d.axial n p = 0 ∧ d.pressure n p = 0

theorem NavierStokes.ModulatedExterior.realized_axial_zero_all {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) {s : GlobalSlowProfiles.Scheme S F.data.h W.axis.normalization} {d : SlowBorelBase.Coefficients} (hd : RealizesScheme s ⋯ d) (hbase : s.base = (AssembledSlowBase.modifiedScheme W Q M).base) (houter : s.B = AssembledSlowBase.nominalOuterRadius W) (n : ℕ) {p : SlowBorelBase.Inner} (hX : AssembledSlowBase.nominalOuterX W ≤ p.1) (heta : |p.2| ≤ 1) : d.axial n p = 0

theorem NavierStokes.ModulatedExterior.realized_primitive_zero_all {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) {s : GlobalSlowProfiles.Scheme S F.data.h W.axis.normalization} {d : SlowBorelBase.Coefficients} (hd : RealizesScheme s ⋯ d) (hbase : s.base = (AssembledSlowBase.modifiedScheme W Q M).base) (houter : s.B = AssembledSlowBase.nominalOuterRadius W) (n : ℕ) {p : SlowBorelBase.Inner} (hX : AssembledSlowBase.nominalOuterX W ≤ p.1) (heta : |p.2| ≤ 1) : ProfileHistories.primitive (d.axial n) p = 0

theorem NavierStokes.ModulatedExterior.realized_exterior_coefficients {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) {s : GlobalSlowProfiles.Scheme S F.data.h W.axis.normalization} {d : SlowBorelBase.Coefficients} (hd : RealizesScheme s ⋯ d) (hbase : s.base = (AssembledSlowBase.modifiedScheme W Q M).base) (houter : s.B = AssembledSlowBase.nominalOuterRadius W) : BaseExterior.ExteriorCoefficients d (BaseExterior.nominalExteriorRadius W)

All coefficient support and stream-mass identities are derived from the actual repaired scheme. The inner cutoff is absent from the premises.

theorem NavierStokes.ModulatedExterior.realized_angular_pure_heat {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) {s : GlobalSlowProfiles.Scheme S F.data.h W.axis.normalization} {d : SlowBorelBase.Coefficients} (hd : RealizesScheme s ⋯ d) (hbase : s.base = (AssembledSlowBase.modifiedScheme W Q M).base) {p : SimilarityProfile.PhysicalPoint} (hp : p ∈ BaseExterior.exteriorDomain F.data.h (BaseExterior.nominalExteriorRadius W)) : BaseExterior.leadingAngular F.data.h W.axis.normalization d p = BaseExterior.heatCoefficient (BaseExterior.nominalHeatNormalization W) F.data.h p

theorem NavierStokes.ModulatedExterior.realized_pressure_pure_heat {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) {s : GlobalSlowProfiles.Scheme S F.data.h W.axis.normalization} {d : SlowBorelBase.Coefficients} (hd : RealizesScheme s ⋯ d) (hbase : s.base = (AssembledSlowBase.modifiedScheme W Q M).base) (henergy : RestoredSquaredSwirl W Q) {p : SimilarityProfile.PhysicalPoint} (hp : p ∈ BaseExterior.exteriorDomain F.data.h (BaseExterior.nominalExteriorRadius W)) : BaseExterior.leadingPressure F.data.h d p = BaseExterior.heatPressure (BaseExterior.nominalHeatNormalization W) F.data.h p

theorem NavierStokes.ModulatedExterior.realized_base_eq_heat {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) {s : GlobalSlowProfiles.Scheme S F.data.h W.axis.normalization} {d : SlowBorelBase.Coefficients} (hd : RealizesScheme s ⋯ d) (hbase : s.base = (AssembledSlowBase.modifiedScheme W Q M).base) (houter : s.B = AssembledSlowBase.nominalOuterRadius W) (hds : SlowBorelBase.SmoothCoefficients d) (henergy : RestoredSquaredSwirl W Q) {a : ℕ → ℕ} (ha : StrictMono a) : Set.EqOn (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization d) (BaseExterior.heatVelocity (BaseExterior.nominalHeatNormalization W) F.data.h) (BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W)) ∧ Set.EqOn (SlowBorelBase.basePressure a F.data.h W.axis.normalization d) (BaseExterior.heatPressureField (BaseExterior.nominalHeatNormalization W) F.data.h) (BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W))

theorem NavierStokes.ModulatedExterior.realized_base_residual_zero {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) {s : GlobalSlowProfiles.Scheme S F.data.h W.axis.normalization} {d : SlowBorelBase.Coefficients} (hd : RealizesScheme s ⋯ d) (hbase : s.base = (AssembledSlowBase.modifiedScheme W Q M).base) (houter : s.B = AssembledSlowBase.nominalOuterRadius W) (hds : SlowBorelBase.SmoothCoefficients d) (henergy : RestoredSquaredSwirl W Q) {a : ℕ → ℕ} (ha : StrictMono a) {z : ProblemStatement.SpaceTime} (hz : z ∈ BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W)) : ProblemStatement.navierStokesResidual (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization d) (SlowBorelBase.basePressure a F.data.h W.axis.normalization d) z.1 z.2 = 0

theorem NavierStokes.ModulatedExterior.realized_residual_germ_zero {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) {s : GlobalSlowProfiles.Scheme S F.data.h W.axis.normalization} {d : SlowBorelBase.Coefficients} (hd : RealizesScheme s ⋯ d) (hbase : s.base = (AssembledSlowBase.modifiedScheme W Q M).base) (houter : s.B = AssembledSlowBase.nominalOuterRadius W) (hds : SlowBorelBase.SmoothCoefficients d) (henergy : RestoredSquaredSwirl W Q) {a : ℕ → ℕ} (ha : StrictMono a) {z : ProblemStatement.SpaceTime} (hz : z ∈ BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W)) : (fun (y : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization d) (SlowBorelBase.basePressure a F.data.h W.axis.normalization d) y.1 y.2) =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.ModulatedExterior.realized_residual_jets_zero {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) {s : GlobalSlowProfiles.Scheme S F.data.h W.axis.normalization} {d : SlowBorelBase.Coefficients} (hd : RealizesScheme s ⋯ d) (hbase : s.base = (AssembledSlowBase.modifiedScheme W Q M).base) (houter : s.B = AssembledSlowBase.nominalOuterRadius W) (hds : SlowBorelBase.SmoothCoefficients d) (henergy : RestoredSquaredSwirl W Q) {a : ℕ → ℕ} (ha : StrictMono a) {z : ProblemStatement.SpaceTime} (hz : z ∈ BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W)) (m : ℕ) : iteratedFDeriv ℝ m (fun (y : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization d) (SlowBorelBase.basePressure a F.data.h W.axis.normalization d) y.1 y.2) z = 0

theorem NavierStokes.ModulatedExterior.actual_squared_swirl_restored {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : RestoredSquaredSwirl W v.profiles

This finite anchor is derived from the actual solved modulation.

theorem NavierStokes.ModulatedExterior.actual_realizes {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : RealizesScheme (AssembledSlowBase.modifiedScheme W v.profiles ⋯) ⋯ (ConstructedSlowBase.Modulated.coefficients v)

theorem NavierStokes.ModulatedExterior.actual_exterior_coefficients {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : BaseExterior.ExteriorCoefficients (ConstructedSlowBase.Modulated.coefficients v) (BaseExterior.nominalExteriorRadius W)

theorem NavierStokes.ModulatedExterior.actual_base_eq_heat {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {a : ℕ → ℕ} (ha : StrictMono a) : Set.EqOn (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization (ConstructedSlowBase.Modulated.coefficients v)) (BaseExterior.heatVelocity (BaseExterior.nominalHeatNormalization W) F.data.h) (BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W)) ∧ Set.EqOn (SlowBorelBase.basePressure a F.data.h W.axis.normalization (ConstructedSlowBase.Modulated.coefficients v)) (BaseExterior.heatPressureField (BaseExterior.nominalHeatNormalization W) F.data.h) (BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W))

Exact heat exterior for this actual modulated sequence and any strictly increasing cutoff schedule. The pressure anchor is discharged internally.

theorem NavierStokes.ModulatedExterior.actual_fields_eq_heat {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) : Set.EqOn (ConstructedSlowBase.Modulated.velocity v c hc upper B) (BaseExterior.heatVelocity (BaseExterior.nominalHeatNormalization W) F.data.h) (BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W)) ∧ Set.EqOn (ConstructedSlowBase.Modulated.pressure v c hc upper B) (BaseExterior.heatPressureField (BaseExterior.nominalHeatNormalization W) F.data.h) (BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W))

theorem NavierStokes.ModulatedExterior.actual_residual_zero {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {z : ProblemStatement.SpaceTime} (hz : z ∈ BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W)) : ProblemStatement.navierStokesResidual (ConstructedSlowBase.Modulated.velocity v c hc upper B) (ConstructedSlowBase.Modulated.pressure v c hc upper B) z.1 z.2 = 0

theorem NavierStokes.ModulatedExterior.actual_residual_jets_zero {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {z : ProblemStatement.SpaceTime} (hz : z ∈ BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W)) (m : ℕ) : iteratedFDeriv ℝ m (fun (y : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (ConstructedSlowBase.Modulated.velocity v c hc upper B) (ConstructedSlowBase.Modulated.pressure v c hc upper B) y.1 y.2) z = 0

theorem NavierStokes.ModulatedExterior.coordinateQ_lt_of_forward_lt {a b : ℝ} {p : ℝ × ℝ} (ha : 0 < a) (ha1 : a < 1) (hb : 0 < b) (hp : 0 < p.1) (hf : p.1 < SimilarityCoordinates.forwardScalar a p.2 b) : SimilarityCoordinates.coordinateQ a p < b

A strict upper test for the actual positive root of the coordinate equation. It uses monotonicity only on the positive branch.

theorem NavierStokes.ModulatedExterior.exists_terminal_exterior_neighborhood {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) : ∃ (U : Set ProblemStatement.SpaceTime), IsOpen U ∧ (1, x) ∈ U ∧ (∀ z ∈ U, 0 < AxisymmetricFields.radialEnergy z.2) ∧ ∀ z ∈ U, z.1 < 1 → z ∈ BaseExterior.cartesianExterior h R

At every positive radius on the central plane, a full spacetime neighborhood on the past side lies in the pure exterior. Spatial position and time are allowed to approach together.

noncomputable def NavierStokes.ModulatedExterior.completedVelocity (C h : ℝ) (u : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

The incoming field is retained at every past time; the actual heat value is supplied at the terminal time.

Equations

• NavierStokes.ModulatedExterior.completedVelocity C h u z = if z.1 < 1 then u z else NavierStokes.BaseExterior.heatVelocity C h z

noncomputable def NavierStokes.ModulatedExterior.completedPressure (C h : ℝ) (p : ProblemStatement.PressureField) : ProblemStatement.PressureField

Completed pressure, defined pointwise by if z.1 < 1 then p z else heatPressureField C h z.

Equations

• NavierStokes.ModulatedExterior.completedPressure C h p z = if z.1 < 1 then p z else NavierStokes.BaseExterior.heatPressureField C h z

theorem NavierStokes.ModulatedExterior.completedVelocity_before (C h : ℝ) (u : ProblemStatement.VelocityField) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) : completedVelocity C h u z = u z

theorem NavierStokes.ModulatedExterior.completedPressure_before (C h : ℝ) (p : ProblemStatement.PressureField) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) : completedPressure C h p z = p z

theorem NavierStokes.ModulatedExterior.completed_fields_smooth_near_terminal {h R C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hR : 0 ≤ R) {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hu : Set.EqOn u (BaseExterior.heatVelocity C h) (BaseExterior.cartesianExterior h R)) (hp : Set.EqOn p (BaseExterior.heatPressureField C h) (BaseExterior.cartesianExterior h R)) {x : ProblemStatement.Space} (hx : x.ofLp 2 = 0) (hs : 0 < AxisymmetricFields.radialEnergy x) : ∃ (U : Set ProblemStatement.SpaceTime), IsOpen U ∧ (1, x) ∈ U ∧ Set.EqOn (completedVelocity C h u) (BaseExterior.heatVelocity C h) U ∧ Set.EqOn (completedPressure C h p) (BaseExterior.heatPressureField C h) U ∧ ContDiffOn ℝ (↑⊤) (completedVelocity C h u) (U ∩ Set.Iic 1 ×ˢ Set.univ) ∧ ContDiffOn ℝ (↑⊤) (completedPressure C h p) (U ∩ Set.Iic 1 ×ˢ Set.univ)

Joint one-sided smooth extension of any fields with the proved heat exterior. The hypotheses are instantiated below from the coefficient and integral construction, rather than imposed on the modulated output.

theorem NavierStokes.ModulatedExterior.realized_terminal_extension {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) {s : GlobalSlowProfiles.Scheme S F.data.h W.axis.normalization} {d : SlowBorelBase.Coefficients} (hd : RealizesScheme s ⋯ d) (hbase : s.base = (AssembledSlowBase.modifiedScheme W Q M).base) (houter : s.B = AssembledSlowBase.nominalOuterRadius W) (hds : SlowBorelBase.SmoothCoefficients d) (henergy : RestoredSquaredSwirl W Q) {a : ℕ → ℕ} (ha : StrictMono a) {x : ProblemStatement.Space} (hx : x.ofLp 2 = 0) (hs : 0 < AxisymmetricFields.radialEnergy x) : ∃ (U : Set ProblemStatement.SpaceTime), IsOpen U ∧ (1, x) ∈ U ∧ Set.EqOn (completedVelocity (BaseExterior.nominalHeatNormalization W) F.data.h (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization d)) (BaseExterior.heatVelocity (BaseExterior.nominalHeatNormalization W) F.data.h) U ∧ Set.EqOn (completedPressure (BaseExterior.nominalHeatNormalization W) F.data.h (SlowBorelBase.basePressure a F.data.h W.axis.normalization d)) (BaseExterior.heatPressureField (BaseExterior.nominalHeatNormalization W) F.data.h) U ∧ ContDiffOn ℝ (↑⊤) (completedVelocity (BaseExterior.nominalHeatNormalization W) F.data.h (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization d)) (U ∩ Set.Iic 1 ×ˢ Set.univ) ∧ ContDiffOn ℝ (↑⊤) (completedPressure (BaseExterior.nominalHeatNormalization W) F.data.h (SlowBorelBase.basePressure a F.data.h W.axis.normalization d)) (U ∩ Set.Iic 1 ×ˢ Set.univ)

theorem NavierStokes.ModulatedExterior.actual_terminal_extension {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (c : ℝ) (hc : 0 < c) (upper : ℝ) (B : ℕ) {x : ProblemStatement.Space} (hx : x.ofLp 2 = 0) (hs : 0 < AxisymmetricFields.radialEnergy x) : ∃ (U : Set ProblemStatement.SpaceTime), IsOpen U ∧ (1, x) ∈ U ∧ Set.EqOn (completedVelocity (BaseExterior.nominalHeatNormalization W) F.data.h (ConstructedSlowBase.Modulated.velocity v c hc upper B)) (BaseExterior.heatVelocity (BaseExterior.nominalHeatNormalization W) F.data.h) U ∧ Set.EqOn (completedPressure (BaseExterior.nominalHeatNormalization W) F.data.h (ConstructedSlowBase.Modulated.pressure v c hc upper B)) (BaseExterior.heatPressureField (BaseExterior.nominalHeatNormalization W) F.data.h) U ∧ ContDiffOn ℝ (↑⊤) (completedVelocity (BaseExterior.nominalHeatNormalization W) F.data.h (ConstructedSlowBase.Modulated.velocity v c hc upper B)) (U ∩ Set.Iic 1 ×ˢ Set.univ) ∧ ContDiffOn ℝ (↑⊤) (completedPressure (BaseExterior.nominalHeatNormalization W) F.data.h (ConstructedSlowBase.Modulated.pressure v c hc upper B)) (U ∩ Set.Iic 1 ×ˢ Set.univ)

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

Edge exponent, given by W.controls.activationTime ^ 2.

Equations

• NavierStokes.FinalSlowBase.edgeExponent W = W.controls.activationTime ^ 2

theorem NavierStokes.FinalSlowBase.edgeExponent_pos {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : 0 < edgeExponent W

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

Log left, given by Real.log (NominalConeAssembly.activeLeft W).

Equations

• NavierStokes.FinalSlowBase.logLeft W = Real.log (NavierStokes.NominalConeAssembly.activeLeft W)

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

Log right, given by Real.log (NominalConeAssembly.activeRight W).

Equations

• NavierStokes.FinalSlowBase.logRight W = Real.log (NavierStokes.NominalConeAssembly.activeRight W)

noncomputable def NavierStokes.FinalSlowBase.annulus {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : Set SlowBorelBase.Inner

Annulus, given by Ioo (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W) ×ˢ Icc (-1 : ℝ) 1.

Equations

• NavierStokes.FinalSlowBase.annulus W = Set.Ioo (NavierStokes.NominalConeAssembly.activeLeft W) (NavierStokes.NominalConeAssembly.activeRight W) ×ˢ Set.Icc (-1) 1

noncomputable def NavierStokes.FinalSlowBase.weight {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : SlowBorelBase.Inner → ℝ

Weight, given by BaseResidual.activeZeta (edgeExponent W) (logLeft W) (logRight W).

Equations

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

noncomputable def NavierStokes.FinalSlowBase.edgeDistance {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : SlowBorelBase.Inner → ℝ

Edge distance, given by BaseResidual.activeDelta (logLeft W) (logRight W).

Equations

• NavierStokes.FinalSlowBase.edgeDistance W = NavierStokes.BaseResidual.activeDelta (NavierStokes.FinalSlowBase.logLeft W) (NavierStokes.FinalSlowBase.logRight W)

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

Box radius, given by max upper (NominalConeAssembly.activeRight W).

Equations

• NavierStokes.FinalSlowBase.boxRadius W upper = max upper (NavierStokes.NominalConeAssembly.activeRight W)

theorem NavierStokes.FinalSlowBase.terminal_pos {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : 0 < NominalConeAssembly.activeRight W

theorem NavierStokes.FinalSlowBase.logRight_eq {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : logRight W = ConstructedSlowBase.activeRight W

theorem NavierStokes.FinalSlowBase.boxRadius_eq {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (upper : ℝ) : boxRadius W upper = ConstructedSlowBase.scaleUpper W upper

theorem NavierStokes.FinalSlowBase.annulus_eq {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : annulus W = BaseResidual.activeWindow (logLeft W) (logRight W)

theorem NavierStokes.FinalSlowBase.annulus_subset_box {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (upper : ℝ) : annulus W ⊆ SlowBorelBase.innerBox 0 (boxRadius W upper)

theorem NavierStokes.FinalSlowBase.iteratedFDeriv_eq_on_dense {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {f g : E → V} {s t : Set E} (hs : IsOpen s) (hst : s ⊆ t) (hts : t ⊆ closure s) (hf : ∀ p ∈ t, ContDiffAt ℝ (↑⊤) f p) (hg : ∀ p ∈ t, ContDiffAt ℝ (↑⊤) g p) (he : Set.EqOn f g s) (m : ℕ) : Set.EqOn (iteratedFDeriv ℝ m f) (iteratedFDeriv ℝ m g) t

Equality on a dense open part determines every ambient derivative when both functions are smooth at the points of the larger set.

noncomputable def NavierStokes.FinalSlowBase.coefficients {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : SlowBorelBase.Coefficients

Coefficients, given by EntranceAlignedBase.modulatedCoefficients H v.

Equations

• NavierStokes.FinalSlowBase.coefficients H v = NavierStokes.EntranceAlignedBase.modulatedCoefficients H v

noncomputable def NavierStokes.FinalSlowBase.profileSequence {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : SlowExpansionResidual.SlowProfiles

Profile sequence, given by asSlowProfiles (EntranceAlignedBase.modulatedScheme H v).

Equations

• NavierStokes.FinalSlowBase.profileSequence H v = NavierStokes.GlobalSlowProfiles.asSlowProfiles (NavierStokes.EntranceAlignedBase.modulatedScheme H v)

theorem NavierStokes.FinalSlowBase.coefficients_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : SlowBorelBase.SmoothCoefficients (coefficients H v)

theorem NavierStokes.FinalSlowBase.finiteIdentities {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : BaseResidual.FiniteIdentities F.data.h W.axis.normalization (coefficients H v) (profileSequence H v)

theorem NavierStokes.FinalSlowBase.stressZeroCore {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : BaseResidual.StressZeroCore (coefficients H v) (NominalConeAssembly.activeLeft W)

noncomputable def NavierStokes.FinalSlowBase.leadingStress {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : SlowBorelBase.Inner → SlowBorelBase.Inner

The literal stress of the same finite modulated profile.

Equations

• NavierStokes.FinalSlowBase.leadingStress v = NavierStokes.LeadingStressWeights.stress v.profiles F.data.h

theorem NavierStokes.FinalSlowBase.leadingStress_smoothAt {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {p : SlowBorelBase.Inner} (hX : 0 < p.1) (heta : p.2 ∈ Set.Icc (-1) 1) : ContDiffAt ℝ (↑⊤) (leadingStress v) p

theorem NavierStokes.FinalSlowBase.leading_stress_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {p : SlowBorelBase.Inner} (hX : 0 ≤ p.1) (heta : |p.2| ≤ 1) : BaseResidual.stressPair (coefficients H v) 0 p = leadingStress v p

theorem NavierStokes.FinalSlowBase.leading_stress_jets {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (m : ℕ) {p : SlowBorelBase.Inner} (hX : 0 < p.1) (heta : p.2 ∈ Set.Icc (-1) 1) : iteratedFDeriv ℝ m (BaseResidual.stressPair (coefficients H v) 0) p = iteratedFDeriv ℝ m (leadingStress v) p

Equality of full derivative tensors holds at both closed parameter endpoints as well as in the interior. No ambient endpoint germ is assumed.

theorem NavierStokes.FinalSlowBase.leading_weighted {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) : ActiveAnnulusWeight.WeightedBounds (Set.Icc (-1) 1) (edgeExponent W) (logLeft W) (logRight W) (LeadingStressWeights.logStress v.profiles F.data.h)

theorem NavierStokes.FinalSlowBase.leading_lowerBound {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) : ∃ (m : ℝ), 0 < m ∧ ∀ p ∈ annulus W, m * weight W p ≤ ‖leadingStress v p‖

theorem NavierStokes.FinalSlowBase.leading_ne_zero {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) {p : SlowBorelBase.Inner} (hp : p ∈ annulus W) : leadingStress v p ≠ 0

theorem NavierStokes.FinalSlowBase.leading_radial_jets {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) (m : ℕ) : ∃ (D : ℝ), 0 < D ∧ ∃ (N : ℕ), ∀ w ∈ annulus W, ‖iteratedFDeriv ℝ m (leadingStress v) w‖ ≤ D * weight W w * (edgeDistance W w)⁻¹ ^ N

theorem NavierStokes.FinalSlowBase.leading_coefficient_jets {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) (m : ℕ) : ∃ (D : ℝ), 0 < D ∧ ∃ (N : ℕ), ∀ w ∈ annulus W, ‖iteratedFDeriv ℝ m (BaseResidual.stressPair (coefficients H v) 0) w‖ ≤ D * weight W w * (edgeDistance W w)⁻¹ ^ N

noncomputable def NavierStokes.FinalSlowBase.leadingFrequency {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : PhaseCalculus.Slow → ℝ

Leading frequency, given by BaseChartJets.leadingFrequency F.data.h W.axis.normalization (coefficients H v).

Equations

• NavierStokes.FinalSlowBase.leadingFrequency H v = NavierStokes.BaseChartJets.leadingFrequency F.data.h W.axis.normalization (NavierStokes.FinalSlowBase.coefficients H v)

noncomputable def NavierStokes.FinalSlowBase.leadingAxial {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : PhaseCalculus.Slow → ℝ

Leading axial, given by BaseChartJets.leadingAxial F.data.h (coefficients H v).

Equations

• NavierStokes.FinalSlowBase.leadingAxial H v = NavierStokes.BaseChartJets.leadingAxial F.data.h (NavierStokes.FinalSlowBase.coefficients H v)

theorem NavierStokes.FinalSlowBase.leadingFrequency_pos {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {p : PhaseCalculus.Slow} (hT : 0 < p.2.2) (hR : 0 < p.1) : 0 < leadingFrequency H v p

theorem NavierStokes.FinalSlowBase.spectral_cones {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) {p : PhaseCalculus.Slow} (hT : 0 < p.2.2) (hR : 0 < p.1) (hw : (BaseChartJets.normalizedCoordinates F.data.h p).2 ∈ annulus W) : PrimaryRepresentatives.ReferenceCone (leadingFrequency H v p) (PhaseEstimates.shearVector (leadingFrequency H v) (leadingAxial H v) p) ∧ PrimaryRepresentatives.TargetCone (leadingFrequency H v p) (PhaseEstimates.shearVector (leadingFrequency H v) (leadingAxial H v) p) (ProfileSpectralCone.stressVector v.profiles F.data.h (BaseChartJets.normalizedCoordinates F.data.h p).2)

noncomputable def NavierStokes.FinalSlowBase.covarianceTarget {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (q : ℝ) (N : ℕ) (U : PartitionedCovariance.UnsignedLabel) (p : PhaseCalculus.Slow) : MovingFrameODE.Plane

The actual covariance target, including its positive chart factor.

Equations

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

theorem NavierStokes.FinalSlowBase.covarianceTarget_cones {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (hcone : LeadingStressWeights.FullTrueCone v) {p : PhaseCalculus.Slow} (hT : 0 < p.2.2) (hR : 0 < p.1) (hw : (BaseChartJets.normalizedCoordinates F.data.h p).2 ∈ annulus W) {q : ℝ} (hq : 0 < q) (N : ℕ) (U : PartitionedCovariance.UnsignedLabel) : PrimaryRepresentatives.ReferenceCone (leadingFrequency H v p) (PhaseEstimates.shearVector (leadingFrequency H v) (leadingAxial H v) p) ∧ PrimaryRepresentatives.TargetCone (leadingFrequency H v p) (PhaseEstimates.shearVector (leadingFrequency H v) (leadingAxial H v) p) (covarianceTarget H v q N U p)

noncomputable def NavierStokes.FinalSlowBase.scales {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ℕ → ℕ

The sequence is selected once from the aligned enlarged bundle.

Equations

• NavierStokes.FinalSlowBase.scales H v upper B = NavierStokes.EntranceAlignedBase.scales H v (NavierStokes.FinalSlowBase.edgeExponent W) ⋯ upper B

theorem NavierStokes.FinalSlowBase.scales_spec {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : B ≤ scales H v upper B 0 ∧ SlowBorelBase.AdmissibleScales F.data.h (BaseResidual.weightedBundle W.axis.normalization (coefficients H v) (weight W)) (SlowBorelBase.innerBox 0 (boxRadius W upper)) (scales H v upper B)

theorem NavierStokes.FinalSlowBase.scales_admissible {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : SlowBorelBase.AdmissibleScales F.data.h (SlowBorelBase.coefficientBundle W.axis.normalization (coefficients H v)) (SlowBorelBase.innerBox 0 (boxRadius W upper)) (scales H v upper B)

theorem NavierStokes.FinalSlowBase.scales_strictMono {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : StrictMono (scales H v upper B)

theorem NavierStokes.FinalSlowBase.scales_admissible_on {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {lo hi : ℝ} (hlo : 0 ≤ lo) (hhi : hi ≤ boxRadius W upper) : SlowBorelBase.AdmissibleScales F.data.h (SlowBorelBase.coefficientBundle W.axis.normalization (coefficients H v)) (SlowBorelBase.innerBox lo hi) (scales H v upper B)

theorem NavierStokes.FinalSlowBase.weighted_bound {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ConstructedSlowBase.WeightedStressBound (scales H v upper B) F.data.h (coefficients H v) (edgeExponent W) (logLeft W) (logRight W)

noncomputable def NavierStokes.FinalSlowBase.velocity {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ProblemStatement.VelocityField

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

Equations

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

noncomputable def NavierStokes.FinalSlowBase.pressure {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ProblemStatement.PressureField

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

Equations

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

noncomputable def NavierStokes.FinalSlowBase.vectorPotential {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ProblemStatement.VelocityField

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

Equations

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

noncomputable def NavierStokes.FinalSlowBase.stressForce {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ProblemStatement.SpaceTime → ProblemStatement.Space

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

Equations

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

noncomputable def NavierStokes.FinalSlowBase.error {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ProblemStatement.SpaceTime → ProblemStatement.Space

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

Equations

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

noncomputable def NavierStokes.FinalSlowBase.normalizedStress {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : SlowBorelBase.Chart → SlowBorelBase.Inner

Normalized stress, given by BaseResidual.normalizedTensor (scales H v upper B) F.data.h (coefficients H v).

Equations

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

theorem NavierStokes.FinalSlowBase.normalizedStress_smoothAt {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {y : SlowBorelBase.Chart} (hy : 0 < y.1) : ContDiffAt ℝ (↑⊤) (normalizedStress H v upper B) y

theorem NavierStokes.FinalSlowBase.velocity_eq_curl {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : velocity H v upper B = SpatialCurl.spatialCurl (vectorPotential H v upper B)

theorem NavierStokes.FinalSlowBase.vectorPotential_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ContDiffOn ℝ (↑⊤) (vectorPotential H v upper B) BaseResidual.past

theorem NavierStokes.FinalSlowBase.velocity_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ContDiffOn ℝ (↑⊤) (velocity H v upper B) BaseResidual.past

theorem NavierStokes.FinalSlowBase.pressure_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ContDiffOn ℝ (↑⊤) (pressure H v upper B) BaseResidual.past

theorem NavierStokes.FinalSlowBase.stressForce_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ContDiffOn ℝ (↑⊤) (stressForce H v upper B) BaseResidual.past

theorem NavierStokes.FinalSlowBase.error_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ContDiffOn ℝ (↑⊤) (error H v upper B) BaseResidual.past

theorem NavierStokes.FinalSlowBase.divergence_zero {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {t : ℝ} (ht : t < 1) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence (velocity H v upper B) t x = 0

theorem NavierStokes.FinalSlowBase.residual_identity {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (z : ProblemStatement.SpaceTime) : ProblemStatement.navierStokesResidual (velocity H v upper B) (pressure H v upper B) z.1 z.2 = stressForce H v upper B z + error H v upper B z

theorem NavierStokes.FinalSlowBase.error_jetRate {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {l : Filter ProblemStatement.SpaceTime} {radius : ℝ} (P : BaseResidual.PhysicalApproach l F.data.h 0 radius) (hr : radius ≤ boxRadius W upper) (m : ℕ) (n : ℝ) (hn : 0 ≤ n) : DiagonalResidual.JetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1) (error H v upper B) m n

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

theorem NavierStokes.FinalSlowBase.leading_origin {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : (coefficients H v).axial 0 (0, 0) = W.axis.j

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

theorem NavierStokes.FinalSlowBase.axis_tendsto {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : Filter.Tendsto (fun (t : ℝ) => ‖velocity H v upper B (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

theorem NavierStokes.FinalSlowBase.speedUnbounded {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ProblemStatement.SpeedUnboundedAtOne (velocity H v upper B)

theorem NavierStokes.FinalSlowBase.weighted_jets {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B m : ℕ) : ∃ (D : ℝ), 0 < D ∧ ∃ (N : ℕ), ∀ (q : ℝ), 0 < q → q ≤ 1 → ∀ w ∈ annulus W, ‖SlowBorelBase.blownJet m (fun (y : SlowBorelBase.Chart) => normalizedStress H v upper B y - BaseResidual.stressPair (coefficients H v) 0 y.2) (q, w)‖ ≤ D * q ^ F.data.h * weight W w * (edgeDistance W w)⁻¹ ^ N

theorem NavierStokes.FinalSlowBase.stress_difference_jets_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B m : ℕ) {q : ℝ} (hq : 0 < q) {w : SlowBorelBase.Inner} (hX : 0 < w.1) (heta : w.2 ∈ Set.Icc (-1) 1) : SlowBorelBase.blownJet m (fun (y : SlowBorelBase.Chart) => normalizedStress H v upper B y - BaseResidual.stressPair (coefficients H v) 0 y.2) (q, w) = SlowBorelBase.blownJet m (fun (y : SlowBorelBase.Chart) => normalizedStress H v upper B y - leadingStress v y.2) (q, w)

The weighted difference can use the literal leading stress even at the parameter endpoints. Its ambient tensors agree by continuity.

theorem NavierStokes.FinalSlowBase.weighted_jets_leading {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B m : ℕ) : ∃ (D : ℝ), 0 < D ∧ ∃ (N : ℕ), ∀ (q : ℝ), 0 < q → q ≤ 1 → ∀ w ∈ annulus W, ‖SlowBorelBase.blownJet m (fun (y : SlowBorelBase.Chart) => normalizedStress H v upper B y - leadingStress v y.2) (q, w)‖ ≤ D * q ^ F.data.h * weight W w * (edgeDistance W w)⁻¹ ^ N

theorem NavierStokes.FinalSlowBase.physical_stress_eq_normalized {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {p : SlowBorelBase.Chart} (hp : p.1 < 1) : (SlowBorelBase.baseStressTheta (scales H v upper B) F.data.h W.axis.normalization (coefficients H v) p, SlowBorelBase.baseStressAxial (scales H v upper B) F.data.h W.axis.normalization (coefficients H v) p) = (SlowBorelBase.physicalChart F.data.h p).1 ^ (-CoordinateAlgebra.A F.data.h - 1 / 2) • normalizedStress H v upper B (SlowBorelBase.physicalChart F.data.h p)

theorem NavierStokes.FinalSlowBase.coefficient_stress_zero_left {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (n : ℕ) {p : SlowBorelBase.Inner} (hp : p.1 ≤ NominalConeAssembly.activeLeft W) : (coefficients H v).stressTheta n p = 0 ∧ (coefficients H v).stressAxial n p = 0

theorem NavierStokes.FinalSlowBase.coefficient_stress_zero_right {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (n : ℕ) {p : SlowBorelBase.Inner} (hp : NominalConeAssembly.activeRight W ≤ p.1) (heta : p.2 ∈ Set.Icc (-1) 1) : (coefficients H v).stressTheta n p = 0 ∧ (coefficients H v).stressAxial n p = 0

theorem NavierStokes.FinalSlowBase.coefficient_stress_support {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (n : ℕ) : SlowStressSupport.radialSupport (Set.Icc (-1) 1) (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W) ((coefficients H v).stressTheta n) ∧ SlowStressSupport.radialSupport (Set.Icc (-1) 1) (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W) ((coefficients H v).stressAxial n)

theorem NavierStokes.FinalSlowBase.positive_stress_support {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {n : ℕ} (hn : 0 < n) : SlowStressSupport.radialSupport (Set.Icc (-1) 1) (EntranceAlignedBase.zeroEnd W H ld.modulation.left) (NominalConeAssembly.activeRight W) ((coefficients H v).stressTheta n) ∧ SlowStressSupport.radialSupport (Set.Icc (-1) 1) (EntranceAlignedBase.zeroEnd W H ld.modulation.left) (NominalConeAssembly.activeRight W) ((coefficients H v).stressAxial n)

theorem NavierStokes.FinalSlowBase.positive_support_gap {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} : NominalConeAssembly.activeLeft W < EntranceAlignedBase.zeroEnd W H ld.modulation.left

theorem NavierStokes.FinalSlowBase.normalizedStress_zero_left {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (q : ℝ) {w : SlowBorelBase.Inner} (hw : w.1 ≤ NominalConeAssembly.activeLeft W) : normalizedStress H v upper B (q, w) = 0

theorem NavierStokes.FinalSlowBase.normalizedStress_zero_outside {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (q : ℝ) {w : SlowBorelBase.Inner} (hw : w.1 ∉ Set.Icc (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W)) (heta : w.2 ∈ Set.Icc (-1) 1) : normalizedStress H v upper B (q, w) = 0

theorem NavierStokes.FinalSlowBase.physicalStress_zero_right {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {p : SlowBorelBase.Chart} (hp : p.1 < 1) (hX : NominalConeAssembly.activeRight W ≤ (SlowBorelBase.physicalChart F.data.h p).2.1) : SlowBorelBase.baseStressTheta (scales H v upper B) F.data.h W.axis.normalization (coefficients H v) p = 0 ∧ SlowBorelBase.baseStressAxial (scales H v upper B) F.data.h W.axis.normalization (coefficients H v) p = 0

theorem NavierStokes.FinalSlowBase.stressForce_zero_right {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hX : NominalConeAssembly.activeRight W < (SlowBorelBase.cartesianChart F.data.h z).2.1) : stressForce H v upper B z = 0

theorem NavierStokes.FinalSlowBase.stressForce_exterior_germ {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hX : NominalConeAssembly.activeRight W < (SlowBorelBase.cartesianChart F.data.h z).2.1) : stressForce H v upper B =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.FinalSlowBase.stressForce_jets_zero_in_exterior {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B m : ℕ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hX : NominalConeAssembly.activeRight W < (SlowBorelBase.cartesianChart F.data.h z).2.1) : iteratedFDeriv ℝ m (stressForce H v upper B) z = 0

theorem NavierStokes.FinalSlowBase.stressForce_core_germ {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hX : (SlowBorelBase.cartesianChart F.data.h z).2.1 < NominalConeAssembly.activeLeft W) : stressForce H v upper B =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.FinalSlowBase.stressForce_jets_zero_in_core {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B m : ℕ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hX : (SlowBorelBase.cartesianChart F.data.h z).2.1 < NominalConeAssembly.activeLeft W) : iteratedFDeriv ℝ m (stressForce H v upper B) z = 0

theorem NavierStokes.FinalSlowBase.realizesScheme {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) : ModulatedExterior.RealizesScheme (EntranceAlignedBase.modulatedScheme H v) ⋯ (coefficients H v)

The exterior comparison uses the actual coefficient formulas, not a separately assumed support or heat-flow conclusion.

theorem NavierStokes.FinalSlowBase.exterior_fields_eq_heat {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : Set.EqOn (velocity H v upper B) (BaseExterior.heatVelocity (BaseExterior.nominalHeatNormalization W) F.data.h) (BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W)) ∧ Set.EqOn (pressure H v upper B) (BaseExterior.heatPressureField (BaseExterior.nominalHeatNormalization W) F.data.h) (BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W))

theorem NavierStokes.FinalSlowBase.exterior_residual_zero {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {z : ProblemStatement.SpaceTime} (hz : z ∈ BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W)) : ProblemStatement.navierStokesResidual (velocity H v upper B) (pressure H v upper B) z.1 z.2 = 0

theorem NavierStokes.FinalSlowBase.exterior_residual_jets_zero {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B m : ℕ) {z : ProblemStatement.SpaceTime} (hz : z ∈ BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W)) : iteratedFDeriv ℝ m (fun (p : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (velocity H v upper B) (pressure H v upper B) p.1 p.2) z = 0

noncomputable def NavierStokes.FinalSlowBase.completedVelocity {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ProblemStatement.VelocityField

Completed velocity, given by ModulatedExterior.completedVelocity (BaseExterior.nominalHeatNormalization W) F.data.h (velocity H v upper B).

Equations

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

noncomputable def NavierStokes.FinalSlowBase.completedPressure {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ProblemStatement.PressureField

Completed pressure, given by ModulatedExterior.completedPressure (BaseExterior.nominalHeatNormalization W) F.data.h (pressure H v upper B).

Equations

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

theorem NavierStokes.FinalSlowBase.completedVelocity_before {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) : completedVelocity H v upper B z = velocity H v upper B z

theorem NavierStokes.FinalSlowBase.completedPressure_before {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) : completedPressure H v upper B z = pressure H v upper B z

theorem NavierStokes.FinalSlowBase.terminal_extension {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {x : ProblemStatement.Space} (hx : x.ofLp 2 = 0) (hs : 0 < AxisymmetricFields.radialEnergy x) : ∃ (U : Set ProblemStatement.SpaceTime), IsOpen U ∧ (1, x) ∈ U ∧ Set.EqOn (completedVelocity H v upper B) (BaseExterior.heatVelocity (BaseExterior.nominalHeatNormalization W) F.data.h) U ∧ Set.EqOn (completedPressure H v upper B) (BaseExterior.heatPressureField (BaseExterior.nominalHeatNormalization W) F.data.h) U ∧ ContDiffOn ℝ (↑⊤) (completedVelocity H v upper B) (U ∩ Set.Iic 1 ×ˢ Set.univ) ∧ ContDiffOn ℝ (↑⊤) (completedPressure H v upper B) (U ∩ Set.Iic 1 ×ˢ Set.univ)

The same exterior yields an actual joint one-sided terminal extension near every non-axis point in the central symmetry plane.

structure NavierStokes.FinalSlowBase.ProfileData : Type

Intermediate data produced by the proved nominal and finite-modulation constructions. No PDE, support, smoothness, or residual conclusion is stored as an input to this record.

• outgoing : OutgoingProfile.Profile

  Outgoing of ProfileData, of type OutgoingProfile.Profile.

• nominal : NominalProfile.Witness self.outgoing

  Nominal of ProfileData, of type NominalProfile.Witness outgoing.

• certificate : NominalConeAssembly.Certificate self.nominal
• loop : ModulatedProfileAssembly.LoopData self.nominal

  Loop of ProfileData, of type ModulatedProfileAssembly.LoopData nominal.

• modulation : ModulatedProfileAssembly.Witness self.loop

  Modulation of ProfileData, of type ModulatedProfileAssembly.Witness loop.

• fullTrueCone : LeadingStressWeights.FullTrueCone self.modulation

theorem NavierStokes.FinalSlowBase.profileData_nonempty : Nonempty ProfileData

noncomputable def NavierStokes.FinalSlowBase.actualProfile : ProfileData

One actual profile is fixed before choosing the scale lower bound or the compact profile box.

Equations

• NavierStokes.FinalSlowBase.actualProfile = Classical.choice NavierStokes.FinalSlowBase.profileData_nonempty

theorem NavierStokes.FinalSlowBase.exists_final_base (upper : ℝ) (B : ℕ) : ∃ (F : OutgoingProfile.Profile) (W : NominalProfile.Witness F) (H : NominalConeAssembly.Certificate W) (ld : ModulatedProfileAssembly.LoopData W) (v : ModulatedProfileAssembly.Witness ld), LeadingStressWeights.FullTrueCone v ∧ SlowBorelBase.SmoothCoefficients (coefficients H v) ∧ BaseResidual.FiniteIdentities F.data.h W.axis.normalization (coefficients H v) (profileSequence H v) ∧ B ≤ scales H v upper B 0 ∧ SlowBorelBase.AdmissibleScales F.data.h (SlowBorelBase.coefficientBundle W.axis.normalization (coefficients H v)) (SlowBorelBase.innerBox 0 (boxRadius W upper)) (scales H v upper B) ∧ SlowBorelBase.AdmissibleScales F.data.h (BaseResidual.weightedBundle W.axis.normalization (coefficients H v) (weight W)) (SlowBorelBase.innerBox 0 (boxRadius W upper)) (scales H v upper B) ∧ ActiveAnnulusWeight.WeightedBounds (Set.Icc (-1) 1) (edgeExponent W) (logLeft W) (logRight W) (LeadingStressWeights.logStress v.profiles F.data.h) ∧ ConstructedSlowBase.WeightedStressBound (scales H v upper B) F.data.h (coefficients H v) (edgeExponent W) (logLeft W) (logRight W) ∧ (∀ (n : ℕ), SlowStressSupport.radialSupport (Set.Icc (-1) 1) (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W) ((coefficients H v).stressTheta n) ∧ SlowStressSupport.radialSupport (Set.Icc (-1) 1) (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W) ((coefficients H v).stressAxial n)) ∧ (∀ (p : SlowBorelBase.Inner), 0 ≤ p.1 → |p.2| ≤ 1 → BaseResidual.stressPair (coefficients H v) 0 p = leadingStress v p) ∧ velocity H v upper B = SpatialCurl.spatialCurl (vectorPotential H v upper B) ∧ ContDiffOn ℝ (↑⊤) (vectorPotential H v upper B) BaseResidual.past ∧ ContDiffOn ℝ (↑⊤) (velocity H v upper B) BaseResidual.past ∧ ContDiffOn ℝ (↑⊤) (pressure H v upper B) BaseResidual.past ∧ ContDiffOn ℝ (↑⊤) (stressForce H v upper B) BaseResidual.past ∧ ContDiffOn ℝ (↑⊤) (error H v upper B) BaseResidual.past ∧ (∀ t < 1, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence (velocity H v upper B) t x = 0) ∧ (∀ (z : ProblemStatement.SpaceTime), ProblemStatement.navierStokesResidual (velocity H v upper B) (pressure H v upper B) z.1 z.2 = stressForce H v upper B z + error H v upper B z) ∧ (∀ t < 1, velocity H v upper B (t, 0) = ((1 - t) ^ (-CoordinateAlgebra.A F.data.h) * W.axis.j) • ProblemStatement.coordinateVector 2) ∧ ProblemStatement.SpeedUnboundedAtOne (velocity H v upper B) ∧ (∀ (l : Filter ProblemStatement.SpaceTime) (a : BaseResidual.PhysicalApproach l F.data.h 0 (boxRadius W upper)), ResidualStability.AllJetsFlat l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart F.data.h z).1) (error H v upper B)) ∧ Set.EqOn (velocity H v upper B) (BaseExterior.heatVelocity (BaseExterior.nominalHeatNormalization W) F.data.h) (BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W)) ∧ Set.EqOn (pressure H v upper B) (BaseExterior.heatPressureField (BaseExterior.nominalHeatNormalization W) F.data.h) (BaseExterior.cartesianExterior F.data.h (BaseExterior.nominalExteriorRadius W))

A complete slow base is constructed without a profile, moment repair, finite PDE identity, support estimate, or residual estimate among the inputs. The same profile, coefficient sequence, and scale sequence occur throughout.