Smooth attachment at the native dyadic band boundaries

The dyadic profile is flat at its support endpoints, although it does not have a zero germ there. Local smoothness of the actual raw primary is proved from the fixed prepared family before using that flatness.

@[reducible, inline]

abbrev NavierStokes.NativeBandExtension.Native : Type

Native: an abbreviation for WaveEdgeExtension.NativePoint.

Equations

• NavierStokes.NativeBandExtension.Native = NavierStokes.WaveEdgeExtension.NativePoint

@[reducible, inline]

abbrev NavierStokes.NativeBandExtension.Slow : Type

Slow type used in native band extension.

Equations

• NavierStokes.NativeBandExtension.Slow = NavierStokes.PhaseCalculus.Slow

@[instance_reducible]

noncomputable def NavierStokes.NativeBandExtension.instNormedAddCommGroupMat2 : NormedAddCommGroup SmoothCovariance.Mat2

Use the entrywise matrix norm inherited from the finite function space.

Equations

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

@[instance_reducible]

noncomputable def NavierStokes.NativeBandExtension.instNormedSpaceRealMat2 : NormedSpace ℝ SmoothCovariance.Mat2

Scalar multiplication is the pointwise real vector-space structure on matrices.

Equations

• NavierStokes.NativeBandExtension.instNormedSpaceRealMat2 = { toModule := Matrix.module, norm_smul_le := NavierStokes.NativeBandExtension.instNormedSpaceRealMat2._proof_1 }

theorem NavierStokes.NativeBandExtension.jets_zero_at_closure {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {f : D → E} {s : Set D} {x : D} (hs : IsOpen s) (hf : ContDiffAt ℝ (↑⊤) f x) (hx : x ∈ closure s) (hz : ∀ y ∈ s, f y = 0) (n : ℕ) : iteratedFDeriv ℝ n f x = 0

All actual tensors vanish at a closure point of an open zero region, provided the function is locally smooth at that point.

theorem NavierStokes.NativeBandExtension.scalar_support_endpoint_jets {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : Function.support f ⊆ Set.Ioo a b) (n : ℕ) : iteratedFDeriv ℝ n f a = 0 ∧ iteratedFDeriv ℝ n f b = 0

theorem NavierStokes.NativeBandExtension.dyadicProfile_endpoint_jets (n : ℕ) : iteratedFDeriv ℝ n SquaredPartition.dyadicProfile (1 / 2) = 0 ∧ iteratedFDeriv ℝ n SquaredPartition.dyadicProfile 2 = 0

theorem NavierStokes.NativeBandExtension.transverse_endpoint_jets {r : ℝ} (hr : 0 < r) (n : ℕ) : iteratedFDeriv ℝ n (PartitionedCovariance.cutoff r) (-r) = 0 ∧ iteratedFDeriv ℝ n (PartitionedCovariance.cutoff r) r = 0

theorem NavierStokes.NativeBandExtension.flat_comp_jets {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {g : ℝ → ℝ} {q : D → ℝ} {x : D} (hg : ContDiff ℝ (↑⊤) g) (hq : ContDiffAt ℝ (↑⊤) q x) (hz : ∀ (j : ℕ), iteratedFDeriv ℝ j g (q x) = 0) (n : ℕ) : iteratedFDeriv ℝ n (fun (y : D) => g (q y)) x = 0

Flatness of a scalar function survives an actual smooth pullback.

theorem NavierStokes.NativeBandExtension.flat_smul_jets {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {g : D → ℝ} {f : D → E} {x : D} (hg : ContDiffAt ℝ (↑⊤) g x) (hf : ContDiffAt ℝ (↑⊤) f x) (hz : ∀ (j : ℕ), iteratedFDeriv ℝ j g x = 0) (n : ℕ) : iteratedFDeriv ℝ n (fun (y : D) => g y • f y) x = 0

A flat scalar factor kills every tensor of the actual smooth product.

theorem NavierStokes.NativeBandExtension.dyadic_product_endpoint {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {q : D → ℝ} {f : D → E} {x : D} (hq : ContDiffAt ℝ (↑⊤) q x) (hf : ContDiffAt ℝ (↑⊤) f x) (he : q x = 1 / 2 ∨ q x = 2) : ContDiffAt ℝ (↑⊤) (fun (y : D) => SquaredPartition.dyadicProfile (q y) • f y) x ∧ ∀ (n : ℕ), iteratedFDeriv ℝ n (fun (y : D) => SquaredPartition.dyadicProfile (q y) • f y) x = 0

Local smoothness from the actual matrix and phase construction

theorem NavierStokes.NativeBandExtension.strictCone_eventually {D : Type u_1} [NormedAddCommGroup D] {H : D → SmoothCovariance.Mat2} {T : D → SmoothCovariance.Vec2} {x : D} (hH : ∀ (i j : Fin 2), ContinuousAt (fun (y : D) => H y i j) x) (hT : ∀ (i : Fin 2), ContinuousAt (fun (y : D) => T y i) x) (hx : SmoothCovariance.StrictCone (H x) (T x)) : ∀ᶠ (y : D) in nhds x, SmoothCovariance.StrictCone (H y) (T y)

theorem NavierStokes.NativeBandExtension.cramer_amplitude_contDiffAt {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {H : D → SmoothCovariance.Mat2} {T : D → SmoothCovariance.Vec2} {x : D} (hH : ∀ (i j : Fin 2), ContDiffAt ℝ (↑⊤) (fun (y : D) => H y i j) x) (hT : ∀ (i : Fin 2), ContDiffAt ℝ (↑⊤) (fun (y : D) => T y i) x) (hx : SmoothCovariance.StrictCone (H x) (T x)) (j : Fin 2) : ContDiffAt ℝ (↑⊤) (fun (y : D) => √(SmoothCovariance.weights (H y) (T y) j)) x

theorem NavierStokes.NativeBandExtension.projectedPressure_contDiffAt {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (frequency : ℝ) {N Ndot u action source : D → ProblemStatement.Space} {x : D} (hN : ContDiffAt ℝ (↑⊤) N x) (hNd : ContDiffAt ℝ (↑⊤) Ndot x) (hu : ContDiffAt ℝ (↑⊤) u x) (ha : ContDiffAt ℝ (↑⊤) action x) (hf : ContDiffAt ℝ (↑⊤) source x) (hn : N x ≠ 0) : ContDiffAt ℝ (↑⊤) (ParticularWaveBounds.projectedPressure frequency N Ndot u action source) x

noncomputable def NavierStokes.NativeBandExtension.nativeQ (h : ℝ) (x : Native) : ℝ

Native Q, given by SimilarityCoordinates.coordinateQ (2 * h) (x.1.2.2, x.1.2.1).

Equations

• NavierStokes.NativeBandExtension.nativeQ h x = NavierStokes.SimilarityCoordinates.coordinateQ (2 * h) (x.1.2.2, x.1.2.1)

theorem NavierStokes.NativeBandExtension.nativeQ_contDiffAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {x : Native} (hT : 0 < x.1.2.2) : ContDiffAt ℝ (↑⊤) (nativeQ h) x

theorem NavierStokes.NativeBandExtension.actualTarget_contDiffAt {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {p : Slow} (hT : 0 < p.2.2) (hX : 0 < (BaseChartJets.normalizedCoordinates F.data.h p).2.1) : ContDiffAt ℝ (↑⊤) (PrimaryTargetBounds.actualTarget v) p

theorem NavierStokes.NativeBandExtension.phaseCovariance_contDiffAt {ι : Type u_1} {U : PhaseJetBounds.Domain ι Slow} (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ι → ℝ) (hpref : ∀ (j : Fin 2), PhaseJetBounds.PolynomialJets U fun (i : ι) (x : Slow) => pref j i) (i : ι) {p : Slow} (hp : p ∈ U.carrier i) (r c : Fin 2) : ContDiffAt ℝ (↑⊤) (fun (q : PhaseJetBounds.Slow) => PrimaryPulseBounds.primaryCovariance pref (fun (j : Fin 2) => (F j).frame) (fun (j : Fin 2) => (F j).lam) (fun (j : Fin 2) => (F j).u) (fun (j : Fin 2) => (F j).L) i q r c) p

theorem NavierStokes.NativeBandExtension.normalizedPulse_contDiffAt {ι : Type u_1} {U : PhaseJetBounds.Domain ι Slow} (F : PrimaryPulseBounds.PhaseConstruction U) (i : ι) {z : Slow × ℝ} (hp : z.1 ∈ U.carrier i) (ht : z.2 ∈ Set.Ioo 0 1) : ContDiffAt ℝ (↑⊤) (PrimaryPulseBounds.normalizedPulse (F.frame i) (F.lam i) (F.u i) (F.L i)) z

theorem NavierStokes.NativeBandExtension.primaryVelocity_contDiffAt {ι : Type u_1} {U : PhaseJetBounds.Domain ι Slow} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (F : Fin 2 → PrimaryPulseBounds.PhaseConstruction U) (pref : Fin 2 → ι → ℝ) (hpref : ∀ (j : Fin 2), PhaseJetBounds.PolynomialJets U fun (i : ι) (x : Slow) => pref j i) (χ : ι → D → Slow × ℝ) (ε : ι → ℝ) (T : ι → D → SmoothCovariance.Vec2) (mask : ι → D → ℝ) (j : Fin 2) (i : ι) {x : D} (hχ : ContDiffAt ℝ (↑⊤) (χ i) x) (hT : ∀ (k : Fin 2), ContDiffAt ℝ (↑⊤) (fun (y : D) => T i y k) x) (hm : ContDiffAt ℝ (↑⊤) (mask i) x) (hp : (χ i x).1 ∈ U.carrier i) (ht : (χ i x).2 ∈ Set.Ioo 0 1) (hc : SmoothCovariance.StrictCone (PrimaryCopyBounds.pulseMatrix F pref χ i x) (T i x)) : ContDiffAt ℝ (↑⊤) (PrimaryCopyBounds.primaryVelocity F pref χ ε T mask j i) x

The actual Cramer square root and actual homogeneous ODE pulse are smooth at a strict-cone point, regardless of which side of a band boundary the neighboring points occupy.

theorem NavierStokes.NativeBandExtension.phasePressure_contDiffAt {ι : Type u_1} {U : PhaseJetBounds.Domain ι Slow} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (F : PrimaryPulseBounds.PhaseConstruction U) (χ : ι → D → Slow × ℝ) (frequency : ι → ℝ) (u : ι → D → ProblemStatement.Space) (i : ι) {x : D} (hχ : ContDiffAt ℝ (↑⊤) (χ i) x) (hp : (χ i x).1 ∈ U.carrier i) (ht : (χ i x).2 ∈ Set.Ioo 0 1) (hu : ContDiffAt ℝ (↑⊤) (u i) x) : ContDiffAt ℝ (↑⊤) (PrimaryCopyBounds.phasePressure F χ frequency u i) x

The same fixed prepared family at the closed band endpoints

structure NavierStokes.NativeBandExtension.ClosedMargins {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (vr vt : TorusInverse.Plane) : Type

These are precisely the closed-reference zeroth-order bounds of the already selected family. No new family or frequency threshold is selected.

• gap : ℝ

  Gap of ClosedMargins, of type ℝ.

• entry : ℝ

  Entry of ClosedMargins, of type ℝ.

• lower : ℝ

  Lower of ClosedMargins, of type ℝ.

• gap_pos : 0 < self.gap
• entry_one : 1 ≤ self.entry
• lower_pos : 0 < self.lower
• covariance (L : PrimaryGeometryAssembly.Index W a.N) (p : Slow) : p ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet W) → p ∈ (PrimaryGeometryAssembly.domain W a.N).carrier L → PrimaryCovarianceBounds.ZeroOrderBounds (√(ChartScales.S (BaseChartJets.cellBand L))) self.gap self.entry self.lower (PrimaryTargetBounds.movingWeight W p) (PrimaryTargetBounds.preparedCovariance H v a vr vt L p) fun (k : Fin 2) => (PrimaryTargetBounds.actualTarget v p).ofLp k

noncomputable def NavierStokes.NativeBandExtension.baseVelocity {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (j : Fin 2) : PrimaryGeometryAssembly.Index W a.N → Native → ProblemStatement.Space

Base velocity, constructed using primaryVelocity.

Equations

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

noncomputable def NavierStokes.NativeBandExtension.basePressure {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (j : Fin 2) : PrimaryGeometryAssembly.Index W a.N → Native → ℂ

Base pressure, constructed using phasePressure.

Equations

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

noncomputable def NavierStokes.NativeBandExtension.outerFactor {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : PrimaryGeometryAssembly.Index W a.N) (x : Native) : ℝ

Outer factor, constructed using outerCutoff.

Equations

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

noncomputable def NavierStokes.NativeBandExtension.bandVelocity {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) (x : Native) : ProblemStatement.Space

Band velocity, given by outerFactor H v a L x • baseVelocity H v a hr0 vr vt j L x.

Equations

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

noncomputable def NavierStokes.NativeBandExtension.bandPressure {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) (x : Native) : ℂ

Band pressure, given by outerFactor H v a L x • basePressure H v a hr0 vr vt j L x.

Equations

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

theorem NavierStokes.NativeBandExtension.coordinates_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : PrimaryGeometryAssembly.Index W a.N) : ContDiff ℝ (↑⊤) (ActualSignedGeometry.pulseCoordinates H v a L)

theorem NavierStokes.NativeBandExtension.outerFactor_contDiffAt {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hT : 0 < x.1.2.2) : ContDiffAt ℝ (↑⊤) (outerFactor H v a L) x

theorem NavierStokes.NativeBandExtension.bandPressure_eq_phasePressure {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) (x : Native) : bandPressure H v a hr0 vr vt j L x = PrimaryCopyBounds.phasePressure (PrimaryGeometryAssembly.construction H v a hr0 j) (ActualSignedGeometry.pulseCoordinates H v a) (fun (L : PrimaryGeometryAssembly.Index W a.N) => ↑(ChartScales.carrier F.data.h (BaseChartJets.cellBand L))) (bandVelocity H v a hr0 vr vt j) L x

noncomputable def NavierStokes.NativeBandExtension.radialInterior {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : Set Native

Radial interior, constructed using WaveEdgeExtension.windowDomain.

Equations

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

theorem NavierStokes.NativeBandExtension.radialInterior_open {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : IsOpen (radialInterior W)

theorem NavierStokes.NativeBandExtension.radialInterior_spec {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {x : Native} (hx : x ∈ radialInterior W) : 0 < x.1.2.2 ∧ 0 < x.1.1 ∧ (BaseChartJets.normalizedCoordinates F.data.h x.1).2.1 ∈ Set.Ioo (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W) ∧ 0 < PrimaryTargetBounds.movingWeight W x.1

theorem NavierStokes.NativeBandExtension.reference_of_closed_band {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {x : Native} (hx : x ∈ radialInterior W) (hq : nativeQ F.data.h x ∈ Set.Icc (1 / 2) 2) : x.1 ∈ PositiveRepresentatives.positivePart (PrimaryGeometryAssembly.referenceSet W)

theorem NavierStokes.NativeBandExtension.prepared_strictCone {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (M : ClosedMargins H v a vr vt) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hx : x ∈ radialInterior W) (hp : x.1 ∈ (PrimaryGeometryAssembly.domain W a.N).carrier L) (hq : nativeQ F.data.h x ∈ Set.Icc (1 / 2) 2) : SmoothCovariance.StrictCone (PrimaryCopyBounds.pulseMatrix (PrimaryGeometryAssembly.construction H v a hr0) (PrimaryCopyBounds.preparedPrefactor r0 vr vt) (ActualSignedGeometry.pulseCoordinates H v a) L x) fun (k : Fin 2) => (PrimaryTargetBounds.actualTarget v x.1).ofLp k

theorem NavierStokes.NativeBandExtension.baseVelocity_contDiffAt_closed {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (M : ClosedMargins H v a vr vt) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hx : x ∈ radialInterior W) (hp : x.1 ∈ (PrimaryGeometryAssembly.domain W a.N).carrier L) (hq : nativeQ F.data.h x ∈ Set.Icc (1 / 2) 2) (hslot : (ActualSignedGeometry.pulseCoordinates H v a L x).2 ∈ Set.Ioo 0 1) : ContDiffAt ℝ (↑⊤) (baseVelocity H v a hr0 vr vt j L) x

theorem NavierStokes.NativeBandExtension.basePressure_contDiffAt_closed {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (M : ClosedMargins H v a vr vt) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hx : x ∈ radialInterior W) (hp : x.1 ∈ (PrimaryGeometryAssembly.domain W a.N).carrier L) (hq : nativeQ F.data.h x ∈ Set.Icc (1 / 2) 2) (hslot : (ActualSignedGeometry.pulseCoordinates H v a L x).2 ∈ Set.Ioo 0 1) : ContDiffAt ℝ (↑⊤) (basePressure H v a hr0 vr vt j L) x

theorem NavierStokes.NativeBandExtension.band_pair_contDiffAt_closed {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (M : ClosedMargins H v a vr vt) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hx : x ∈ radialInterior W) (hp : x.1 ∈ (PrimaryGeometryAssembly.domain W a.N).carrier L) (hq : nativeQ F.data.h x ∈ Set.Icc (1 / 2) 2) (hslot : (ActualSignedGeometry.pulseCoordinates H v a L x).2 ∈ Set.Ioo 0 1) : ContDiffAt ℝ (↑⊤) (bandVelocity H v a hr0 vr vt j L) x ∧ ContDiffAt ℝ (↑⊤) (bandPressure H v a hr0 vr vt j L) x

theorem NavierStokes.NativeBandExtension.zero_germ_jets {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {f : D → E} {x : D} (h : f =ᶠ[nhds x] fun (x : D) => 0) : ContDiffAt ℝ (↑⊤) f x ∧ ∀ (n : ℕ), iteratedFDeriv ℝ n f x = 0

theorem NavierStokes.NativeBandExtension.scalar_zero_germ {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedAddCommGroup E] [NormedSpace ℝ E] {g : D → ℝ} (f : D → E) {x : D} (h : g =ᶠ[nhds x] fun (x : D) => 0) : (fun (y : D) => g y • f y) =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.NativeBandExtension.vector_zero_germ {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedAddCommGroup E] [NormedSpace ℝ E] (g : D → ℝ) {f : D → E} {x : D} (h : f =ᶠ[nhds x] fun (x : D) => 0) : (fun (y : D) => g y • f y) =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.NativeBandExtension.baseVelocity_zero_germ {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hT : 0 < x.1.2.2) (hp : x.1 ∉ (PrimaryGeometryAssembly.domain W a.N).carrier L) : baseVelocity H v a hr0 vr vt j L =ᶠ[nhds x] fun (x : Native) => 0

theorem NavierStokes.NativeBandExtension.basePressure_zero_germ {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hT : 0 < x.1.2.2) (hp : x.1 ∉ (PrimaryGeometryAssembly.domain W a.N).carrier L) : basePressure H v a hr0 vr vt j L =ᶠ[nhds x] fun (x : Native) => 0

theorem NavierStokes.NativeBandExtension.band_pair_zero_germ_cell {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hT : 0 < x.1.2.2) (hp : x.1 ∉ (PrimaryGeometryAssembly.domain W a.N).carrier L) : (bandVelocity H v a hr0 vr vt j L =ᶠ[nhds x] fun (x : Native) => 0) ∧ bandPressure H v a hr0 vr vt j L =ᶠ[nhds x] fun (x : Native) => 0

theorem NavierStokes.NativeBandExtension.factor_zero_germ_slot {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hslot : (ActualSignedGeometry.pulseCoordinates H v a L x).2 ∉ Set.Ioo 0 1) : outerFactor H v a L =ᶠ[nhds x] fun (x : Native) => 0

theorem NavierStokes.NativeBandExtension.factor_zero_germ_band {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hT : 0 < x.1.2.2) (hq : nativeQ F.data.h x ∉ Set.Icc (1 / 2) 2) : outerFactor H v a L =ᶠ[nhds x] fun (x : Native) => 0

theorem NavierStokes.NativeBandExtension.factor_zero_germ_transverse {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hu : x.2.1 ∉ Set.Icc (-r0) r0) : outerFactor H v a L =ᶠ[nhds x] fun (x : Native) => 0

theorem NavierStokes.NativeBandExtension.band_pair_zero_germ_factor {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hz : outerFactor H v a L =ᶠ[nhds x] fun (x : Native) => 0) : (bandVelocity H v a hr0 vr vt j L =ᶠ[nhds x] fun (x : Native) => 0) ∧ bandPressure H v a hr0 vr vt j L =ᶠ[nhds x] fun (x : Native) => 0

theorem NavierStokes.NativeBandExtension.outerFactor_band_jets {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hT : 0 < x.1.2.2) (he : nativeQ F.data.h x = 1 / 2 ∨ nativeQ F.data.h x = 2) (n : ℕ) : iteratedFDeriv ℝ n (outerFactor H v a L) x = 0

theorem NavierStokes.NativeBandExtension.outerFactor_transverse_jets {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hT : 0 < x.1.2.2) (he : x.2.1 = -r0 ∨ x.2.1 = r0) (n : ℕ) : iteratedFDeriv ℝ n (outerFactor H v a L) x = 0

theorem NavierStokes.NativeBandExtension.band_pair_contDiffAt {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (M : ClosedMargins H v a vr vt) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hx : x ∈ radialInterior W) : ContDiffAt ℝ (↑⊤) (bandVelocity H v a hr0 vr vt j L) x ∧ ContDiffAt ℝ (↑⊤) (bandPressure H v a hr0 vr vt j L) x

theorem NavierStokes.NativeBandExtension.band_pair_contDiffOn {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (M : ClosedMargins H v a vr vt) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) : ContDiffOn ℝ (↑⊤) (bandVelocity H v a hr0 vr vt j L) (radialInterior W) ∧ ContDiffOn ℝ (↑⊤) (bandPressure H v a hr0 vr vt j L) (radialInterior W)

theorem NavierStokes.NativeBandExtension.band_pair_edge_jets_closed {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (M : ClosedMargins H v a vr vt) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hx : x ∈ radialInterior W) (hp : x.1 ∈ (PrimaryGeometryAssembly.domain W a.N).carrier L) (hq : nativeQ F.data.h x ∈ Set.Icc (1 / 2) 2) (hslot : (ActualSignedGeometry.pulseCoordinates H v a L x).2 ∈ Set.Ioo 0 1) (he : (nativeQ F.data.h x = 1 / 2 ∨ nativeQ F.data.h x = 2) ∨ x.2.1 = -r0 ∨ x.2.1 = r0) (n : ℕ) : iteratedFDeriv ℝ n (bandVelocity H v a hr0 vr vt j L) x = 0 ∧ iteratedFDeriv ℝ n (bandPressure H v a hr0 vr vt j L) x = 0

theorem NavierStokes.NativeBandExtension.native_mem_of_data {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hx : x ∈ radialInterior W) (hp : x.1 ∈ (PrimaryGeometryAssembly.domain W a.N).carrier L) (hq : nativeQ F.data.h x ∈ Set.Ioo (1 / 2) 2) (hu : x.2.1 ∈ Set.Ioo (-r0) r0) (hslot : (ActualSignedGeometry.pulseCoordinates H v a L x).2 ∈ Set.Ioo 0 1) : x ∈ (ActualSignedGeometry.nativeDomain H v a).carrier L

theorem NavierStokes.NativeBandExtension.native_mem_band {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hx : x ∈ (ActualSignedGeometry.nativeDomain H v a).carrier L) : nativeQ F.data.h x ∈ Set.Ioo (1 / 2) 2

theorem NavierStokes.NativeBandExtension.band_pair_zero_jets_off_native {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (M : ClosedMargins H v a vr vt) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hx : x ∈ radialInterior W) (hn : x ∉ (ActualSignedGeometry.nativeDomain H v a).carrier L) (n : ℕ) : iteratedFDeriv ℝ n (bandVelocity H v a hr0 vr vt j L) x = 0 ∧ iteratedFDeriv ℝ n (bandPressure H v a hr0 vr vt j L) x = 0

theorem NavierStokes.NativeBandExtension.band_pair_band_edge_jets {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (M : ClosedMargins H v a vr vt) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hx : x ∈ radialInterior W) (he : nativeQ F.data.h x = 1 / 2 ∨ nativeQ F.data.h x = 2) (n : ℕ) : iteratedFDeriv ℝ n (bandVelocity H v a hr0 vr vt j L) x = 0 ∧ iteratedFDeriv ℝ n (bandPressure H v a hr0 vr vt j L) x = 0

noncomputable def NavierStokes.NativeBandExtension.radialDomain {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) : PrimaryCopyBounds.JetDomain (PrimaryGeometryAssembly.Index W a.N) Native

The full open radial domain, preserving the original native growth function exactly and adding the flat band/transverse boundary points.

Equations

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

theorem NavierStokes.NativeBandExtension.radialDomain_growth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (L : PrimaryGeometryAssembly.Index W a.N) (x : Native) : (radialDomain H v a).growth L x = BaseContextAssembly.slowScale (BaseChartJets.cellBand L) * WaveEdgeExtension.edgeGrowth (WaveEdgeExtension.nativeRadius F.data.h) (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W) x

theorem NavierStokes.NativeBandExtension.NativeJets.on_flat_cover {ι : Type u_1} {D : Type} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {V V' : PrimaryCopyBounds.JetDomain ι D} {w : ι → D → ℝ} {f : ι → D → E} (hf : PrimaryCopyBounds.NativeJets V w f) (hcover : ∀ (i : ι), ∀ x ∈ V'.carrier i, x ∈ V.carrier i ∨ ContDiffAt ℝ (↑⊤) (f i) x ∧ ∀ (n : ℕ), iteratedFDeriv ℝ n (f i) x = 0) (hw : ∀ (i : ι), ∀ x ∈ V'.carrier i, 0 ≤ w i x) (hG : ∀ (i : ι), ∀ x ∈ V'.carrier i, x ∈ V.carrier i → V.growth i x ≤ V'.growth i x) : PrimaryCopyBounds.NativeJets V' w f

Flat boundary points, unlike zero germs, can be covered by their proved local smoothness and exact zero tensors. Uniform constants are unchanged.

Uniform bounds and the final radial attachment

noncomputable def NavierStokes.NativeBandExtension.envelope {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (j : Fin 2) : PrimaryGeometryAssembly.Index W a.N → Native → ℝ

Envelope, given by pulseEnvelope (PrimaryGeometryAssembly.construction H v a hr0) (ActualSignedGeometry.pulseCoordinates H v a) j.

Equations

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

noncomputable def NavierStokes.NativeBandExtension.velocityWeight {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) (x : Native) : ℝ

Velocity weight, constructed using Real.sqrt.

Equations

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

noncomputable def NavierStokes.NativeBandExtension.pressureWeight {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) (x : Native) : ℝ

Pressure weight, constructed using ChartScales.epsilon.

Equations

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

theorem NavierStokes.NativeBandExtension.velocityWeight_nonneg {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) (x : Native) : 0 ≤ velocityWeight H v a hr0 j L x

theorem NavierStokes.NativeBandExtension.pressureWeight_nonneg {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) (x : Native) : 0 ≤ pressureWeight H v a hr0 j L x

theorem NavierStokes.NativeBandExtension.bandVelocity_radial_jets {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (M : ClosedMargins H v a vr vt) (j : Fin 2) (hu : PrimaryCopyBounds.NativeJets (ActualSignedGeometry.nativeDomain H v a) (velocityWeight H v a hr0 j) (bandVelocity H v a hr0 vr vt j)) : PrimaryCopyBounds.NativeJets (radialDomain H v a) (velocityWeight H v a hr0 j) (bandVelocity H v a hr0 vr vt j)

theorem NavierStokes.NativeBandExtension.bandPressure_radial_jets {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (M : ClosedMargins H v a vr vt) (j : Fin 2) (hp : PrimaryCopyBounds.NativeJets (ActualSignedGeometry.nativeDomain H v a) (pressureWeight H v a hr0 j) (bandPressure H v a hr0 vr vt j)) : PrimaryCopyBounds.NativeJets (radialDomain H v a) (pressureWeight H v a hr0 j) (bandPressure H v a hr0 vr vt j)

theorem NavierStokes.NativeBandExtension.band_pair_native_regular {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (M : ClosedMargins H v a vr vt) (j : Fin 2) (hu : PrimaryCopyBounds.NativeJets (ActualSignedGeometry.nativeDomain H v a) (velocityWeight H v a hr0 j) (bandVelocity H v a hr0 vr vt j)) (hp : PrimaryCopyBounds.NativeJets (ActualSignedGeometry.nativeDomain H v a) (pressureWeight H v a hr0 j) (bandPressure H v a hr0 vr vt j)) (L : PrimaryGeometryAssembly.Index W a.N) : WaveEdgeExtension.NativeRegularity W (bandVelocity H v a hr0 vr vt j L) ∧ WaveEdgeExtension.NativeRegularity W (bandPressure H v a hr0 vr vt j L)

After filling the flat band boundary, the radial attachment theorem applies at both radial edges, including their intersections with band edges.

noncomputable def NavierStokes.NativeBandExtension.preOuterVelocity {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) (x : Native) : ProblemStatement.Space

Pre outer velocity, given by (SquaredPartition.dyadicProfile (nativeQ F.data.h x) * PartitionedCovariance.cutoff r0 x.2.1) • baseVelocity H v a hr0 vr vt j L x.

Equations

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

noncomputable def NavierStokes.NativeBandExtension.preOuterPressure {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) (x : Native) : ℂ

Pre outer pressure, given by (SquaredPartition.dyadicProfile (nativeQ F.data.h x) * PartitionedCovariance.cutoff r0 x.2.1) • basePressure H v a hr0 vr vt j L x.

Equations

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

theorem NavierStokes.NativeBandExtension.preOuterPressure_eq_phasePressure {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) (x : Native) : preOuterPressure H v a hr0 vr vt j L x = PrimaryCopyBounds.phasePressure (PrimaryGeometryAssembly.construction H v a hr0 j) (ActualSignedGeometry.pulseCoordinates H v a) (fun (L : PrimaryGeometryAssembly.Index W a.N) => ↑(ChartScales.carrier F.data.h (BaseChartJets.cellBand L))) (preOuterVelocity H v a hr0 vr vt j) L x

theorem NavierStokes.NativeBandExtension.bandVelocity_eq_outer {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) (x : Native) : bandVelocity H v a hr0 vr vt j L x = PrimaryCopyBounds.outerCutoff (ActualSignedGeometry.pulseCoordinates H v a L x).2 • preOuterVelocity H v a hr0 vr vt j L x

theorem NavierStokes.NativeBandExtension.bandPressure_eq_outer {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) (x : Native) : bandPressure H v a hr0 vr vt j L x = PrimaryCopyBounds.outerCutoff (ActualSignedGeometry.pulseCoordinates H v a L x).2 • preOuterPressure H v a hr0 vr vt j L x

theorem NavierStokes.NativeBandExtension.gaussian_bandVelocity {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) (x : Native) : GaussianTailFlat.profile (ActualSignedGeometry.pulseCoordinates H v a L x).2 • bandVelocity H v a hr0 vr vt j L x = GaussianTailFlat.profile (ActualSignedGeometry.pulseCoordinates H v a L x).2 • preOuterVelocity H v a hr0 vr vt j L x

Applying the intended Gaussian after attachment still applies that Gaussian exactly once: the outer slot cutoff is one on its support.

theorem NavierStokes.NativeBandExtension.gaussian_bandPressure {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (j : Fin 2) (L : PrimaryGeometryAssembly.Index W a.N) (x : Native) : GaussianTailFlat.profile (ActualSignedGeometry.pulseCoordinates H v a L x).2 • bandPressure H v a hr0 vr vt j L x = GaussianTailFlat.profile (ActualSignedGeometry.pulseCoordinates H v a L x).2 • preOuterPressure H v a hr0 vr vt j L x

theorem NavierStokes.NativeBandExtension.outerCutoff_native_polynomial {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) : PhaseJetBounds.PolynomialJets (ActualSignedGeometry.nativeDomain H v a).toDomain fun (L : ActualSignedGeometry.Label H v a) (x : ActualSignedGeometry.Native) => PrimaryCopyBounds.outerCutoff (ActualSignedGeometry.pulseCoordinates H v a L x).2

theorem NavierStokes.NativeBandExtension.band_pair_native_regular_of_raw_jets {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (M : ClosedMargins H v a vr vt) (j : Fin 2) (hu : PrimaryCopyBounds.NativeJets (ActualSignedGeometry.nativeDomain H v a) (velocityWeight H v a hr0 j) (preOuterVelocity H v a hr0 vr vt j)) (hp : PrimaryCopyBounds.NativeJets (ActualSignedGeometry.nativeDomain H v a) (pressureWeight H v a hr0 j) (preOuterPressure H v a hr0 vr vt j)) (L : PrimaryGeometryAssembly.Index W a.N) : WaveEdgeExtension.NativeRegularity W (bandVelocity H v a hr0 vr vt j L) ∧ WaveEdgeExtension.NativeRegularity W (bandPressure H v a hr0 vr vt j L)

The endpoint consumed by the actual initialization: only the already proved raw interior jet estimates and the fixed family's closed margins enter. The outer time cutoff and all boundary regularity are derived here.

theorem NavierStokes.NativeBandExtension.attached_pair_band_edge_jets {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {upper : ℝ} {B : ℕ} {r0 : ℝ} {N0 : ℕ} (a : PrimaryGeometryAssembly.Prepared H v upper B r0 N0) (hr0 : 0 < r0) (vr vt : TorusInverse.Plane) (M : ClosedMargins H v a vr vt) (j : Fin 2) (hu : PrimaryCopyBounds.NativeJets (ActualSignedGeometry.nativeDomain H v a) (velocityWeight H v a hr0 j) (preOuterVelocity H v a hr0 vr vt j)) (hp : PrimaryCopyBounds.NativeJets (ActualSignedGeometry.nativeDomain H v a) (pressureWeight H v a hr0 j) (preOuterPressure H v a hr0 vr vt j)) (L : PrimaryGeometryAssembly.Index W a.N) {x : Native} (hT : 0 < x.1.2.2) (he : nativeQ F.data.h x = 1 / 2 ∨ nativeQ F.data.h x = 2) (n : ℕ) : iteratedFDeriv ℝ n (WaveEdgeExtension.nativeExtension W (bandVelocity H v a hr0 vr vt j L)) x = 0 ∧ iteratedFDeriv ℝ n (WaveEdgeExtension.nativeExtension W (bandPressure H v a hr0 vr vt j L)) x = 0

The band boundary tensors remain zero after the radial attachment, including the intersections of the band and radial boundaries.