Physical copy bounds from local native smoothness

Raw native coefficients and phase profiles are only used on their valid open patches. A smooth bump produces a globally smooth function with the exact same germ at one evaluation point. The physical carrier bound measures only jets at that point, so no bound on the extension away from it is needed.

def NavierStokes.LocalPhysicalCopyBounds.SmoothNear {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (x : E) : Prop

Smoothness on one genuine open neighborhood. Unlike a bare ContDiffAt ℝ ∞, the same neighborhood works for all derivative orders.

Equations

• NavierStokes.LocalPhysicalCopyBounds.SmoothNear f x = ∃ (U : Set E), IsOpen U ∧ x ∈ U ∧ ContDiffOn ℝ (↑⊤) f U

theorem NavierStokes.LocalPhysicalCopyBounds.SmoothNear.of_open {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {U : Set E} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) {x : E} (hx : x ∈ U) : SmoothNear f x

theorem NavierStokes.LocalPhysicalCopyBounds.SmoothNear.contDiffAt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {x : E} (hf : SmoothNear f x) : ContDiffAt ℝ (↑⊤) f x

theorem NavierStokes.LocalPhysicalCopyBounds.contDiff_of_patch_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {U : Set E} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) (hz : ∀ x ∉ U, f =ᶠ[nhds x] fun (x : E) => 0) : ContDiff ℝ (↑⊤) f

Local smoothness on an open patch and an actual zero germ off it suffice for global smoothness. No raw totalization is assumed smooth.

theorem NavierStokes.LocalPhysicalCopyBounds.contDiff_of_patch_tsupport {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {U : Set E} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) (hs : tsupport f ⊆ U) : ContDiff ℝ (↑⊤) f

theorem NavierStokes.LocalPhysicalCopyBounds.SmoothNear.exists_global_germ {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] {f : E → F} {x : E} (hf : SmoothNear f x) : ∃ (g : E → F), ContDiff ℝ (↑⊤) g ∧ f =ᶠ[nhds x] g

Construct the replacement using a smooth bump inside the actual open patch. Its values and all its derivatives agree with the raw input near x. No bound on the extension away from x is imposed or used.

theorem NavierStokes.LocalPhysicalCopyBounds.jet_bound_at_closure {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {U : Set E} {x : E} {B : ℝ} (hf : ContDiffAt ℝ (↑⊤) f x) (hx : x ∈ closure U) (j : ℕ) (hb : ∀ y ∈ U, ‖iteratedFDeriv ℝ j f y‖ ≤ B) : ‖iteratedFDeriv ℝ j f x‖ ≤ B

An interior native jet bound persists at a boundary point where the actual coefficient is locally smooth. This covers the zero-extended moving edges without requiring their points to belong to the open weighted strip.

noncomputable def NavierStokes.LocalPhysicalCopyBounds.replaceProfiles (c : PhysicalWaveSum.CarrierData) (F G : PhysicalGraphBounds.Slow → ℝ) : PhysicalWaveSum.CarrierData

Replace profiles, given by { c with F := F, G := G }.

Equations

• NavierStokes.LocalPhysicalCopyBounds.replaceProfiles c F G = { chart := c.chart, center := c.center, angular := c.angular, axial := c.axial, radial := c.radial, F := F, G := G }

noncomputable def NavierStokes.LocalPhysicalCopyBounds.slotSlow (c : PhysicalWaveSum.CarrierData) (a h : ℝ) (n : ℕ) (r0 : ℝ) (w : ProblemStatement.SpaceTime) : PhysicalGraphBounds.Slow

Slot slow as an element of PhysicalGraphBounds.Slow.

Equations

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

theorem NavierStokes.LocalPhysicalCopyBounds.slotSlow_continuousAt {a : ℝ} (ha : 0 < a) (c : PhysicalWaveSum.CarrierData) (h : ℝ) (n : ℕ) (r0 : ℝ) {w : ProblemStatement.SpaceTime} (hw : PhysicalGraphBounds.radialProjection w ≠ 0) : ContinuousAt (slotSlow c a h n r0) w

theorem NavierStokes.LocalPhysicalCopyBounds.commonWave_germ {a : ℝ} (ha : 0 < a) (h : ℝ) (n d : ℕ) (r0 : ℝ) (c : PhysicalWaveSum.CarrierData) (j : ℤ) {amp amp' : PhysicalWaveSum.LiftPoint → ℂ} {F G : PhysicalGraphBounds.Slow → ℝ} {w : ProblemStatement.SpaceTime} (hw : PhysicalGraphBounds.radialProjection w ≠ 0) (hamp : amp =ᶠ[nhds (PhysicalWaveSum.commonLift h n d w)] amp') (hF : c.F =ᶠ[nhds (slotSlow c a h n r0 w)] F) (hG : c.G =ᶠ[nhds (slotSlow c a h n r0 w)] G) : PhysicalWaveSum.commonWave a h n d r0 c amp j =ᶠ[nhds w] PhysicalWaveSum.commonWave a h n d r0 (replaceProfiles c F G) amp' j

Replacing native inputs by functions with the same germs preserves the actual physical carrier germ, including the full phase.

theorem NavierStokes.LocalPhysicalCopyBounds.commonWave_smoothAt_local {a : ℝ} (ha : 0 < a) (h : ℝ) (n d : ℕ) (r0 : ℝ) (c : PhysicalWaveSum.CarrierData) {amp : PhysicalWaveSum.LiftPoint → ℂ} (j : ℤ) {w : ProblemStatement.SpaceTime} (hw : PhysicalGraphBounds.radialProjection w ≠ 0) (hamp : SmoothNear amp (PhysicalWaveSum.commonLift h n d w)) (hF : SmoothNear c.F (slotSlow c a h n r0 w)) (hG : SmoothNear c.G (slotSlow c a h n r0 w)) : ContDiffAt ℝ (↑⊤) (PhysicalWaveSum.commonWave a h n d r0 c amp j) w

theorem NavierStokes.LocalPhysicalCopyBounds.common_carrier_physical_bound_local {h a b Z r0 P B eBase : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (hZ : 0 ≤ Z) (hr0 : 0 ≤ r0) (hP : 1 ≤ P) (hB : 1 ≤ B) (heBase : 0 ≤ eBase) (Δ m : ℕ) (g eAmp A H : ℝ) (hA : 0 ≤ A) (hH : 0 ≤ H) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ d ≤ Δ, ∀ (w : ProblemStatement.SpaceTime), (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b → |w.1| ≤ 1 → ‖PhysicalGraphBounds.liftZT (PhysicalGraphBounds.physicalLift h n w)‖ ≤ Z → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ∀ (c : PhysicalWaveSum.CarrierData) (amp : PhysicalWaveSum.LiftPoint → ℂ) (j : ℤ), |c.angular| ≤ P → |c.axial| ≤ P → |c.radial| ≤ P → |PhysicalGraphBounds.etaCoordinate (PhysicalGraphBounds.nativeGraph h n w - c.center)| ≤ r0 → SmoothNear amp (PhysicalWaveSum.commonLift h n d w) → SmoothNear c.F (slotSlow c a h n r0 w) → SmoothNear c.G (slotSlow c a h n r0 w) → |↑j| ≤ H → (∀ i ≤ m, ‖iteratedFDeriv ℝ i amp (PhysicalWaveSum.commonLift h n d w)‖ ≤ A * ChartScales.Q n ^ g * ChartScales.S n ^ eAmp) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i c.F (slotSlow c a h n r0 w)‖ ≤ B * ChartScales.S n ^ eBase) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i c.G (slotSlow c a h n r0 w)‖ ≤ B * ChartScales.S n ^ eBase) → ‖iteratedFDeriv ℝ m (PhysicalWaveSum.commonWave a h n d r0 c amp j) w‖ ≤ C * q ^ (g - PhysicalGraphBounds.waveLoss h m)

The pointwise global-carrier estimate applies to the constructed same-germ replacements. Its constants therefore remain unchanged.

Support-local families

structure NavierStokes.LocalPhysicalCopyBounds.SupportData {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a b h r0 Z : ℝ) (Δ : ℕ) : Prop

Only the primitive support geometry and angular integrality. There is no global smoothness condition in this record.

• gap_le (L : PhysicalWaveSum.BandLabel) : f.gap L ≤ Δ
• gap_native (L : PhysicalWaveSum.BandLabel) : f.gap L ≤ ChartScales.nativeIndex h (↑L).1
• angular_integer (k : K) (L : PhysicalWaveSum.BandLabel) : ∃ (m : ℤ), ↑(ChartScales.carrier h (↑L).1) * (f.carrier k L).angular = ↑m
• geometry_support (k : K) (I : PhysicalWaveSum.WaveIndex H) (y : ProblemStatement.SpaceTime) : f.amplitude k I (PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) y) ≠ 0 → (PhysicalGraphBounds.scaledRadial (↑I.1).1) y ∈ PhysicalGraphBounds.annulus a b ∧ ‖PhysicalGraphBounds.liftZT (PhysicalGraphBounds.physicalLift h (↑I.1).1 y)‖ ≤ Z ∧ |PhysicalGraphBounds.etaCoordinate (PhysicalGraphBounds.nativeGraph h (↑I.1).1 y - (f.carrier k I.1).center)| ≤ r0
• mask_support (k : K) (I : PhysicalWaveSum.WaveIndex H) (y : ProblemStatement.SpaceTime) : y ∈ PhysicalWaveSum.preterminal → f.amplitude k I (PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) y) ≠ 0 → PhysicalWaveSum.physicalMask (CoordinateAlgebra.D h) (↑I.1) (PhysicalWaveSum.physicalParams h y) ≠ 0

structure NavierStokes.LocalPhysicalCopyBounds.SmoothData {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) : Prop

The genuine raw inputs need be smooth only near points at which this copy has support. In particular, phase profiles need not be smooth at a singular totalization of coordinateQ outside the actual native patch.

• amplitude (k : K) (I : PhysicalWaveSum.WaveIndex H) (w : ProblemStatement.SpaceTime) : w ∈ PhysicalWaveSum.preterminal → w ∈ tsupport (f.term a h r0 I k) → SmoothNear (f.amplitude k I) (PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) w)
• profiles (k : K) (I : PhysicalWaveSum.WaveIndex H) (w : ProblemStatement.SpaceTime) : w ∈ PhysicalWaveSum.preterminal → w ∈ tsupport (f.term a h r0 I k) → ∀ (chart : PolarCharts.Index), (PhysicalGraphBounds.scaledRadial (↑I.1).1) w ∈ PolarCharts.chartDomain a chart → SmoothNear (f.carrier k I.1).F (slotSlow ((f.carrier k I.1).withChart chart) a h (↑I.1).1 r0 w) ∧ SmoothNear (f.carrier k I.1).G (slotSlow ((f.carrier k I.1).withChart chart) a h (↑I.1).1 r0 w)

structure NavierStokes.LocalPhysicalCopyBounds.JetData {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (hc : PhysicalCopyBounds.SupportCells f) (a b h r0 P A B g eAmp eBase : ℝ) (m : ℕ) : Prop

Native jets are needed only for a copy with nonzero local support. This permits zero germs outside the valid native patch.

• parameters (k : K) (L : PhysicalWaveSum.BandLabel) : |(f.carrier k L).angular| ≤ P ∧ |(f.carrier k L).axial| ≤ P ∧ |(f.carrier k L).radial| ≤ P
• jets (k : K) (I : PhysicalWaveSum.WaveIndex H) (w : ProblemStatement.SpaceTime) : w ∈ PhysicalWaveSum.preterminal → PhysicalWaveSum.physicalParams h w ∈ PhysicalWaveSum.labelRegion (CoordinateAlgebra.D h) ↑I.1 → (PhysicalGraphBounds.scaledRadial (↑I.1).1) w ∈ PhysicalGraphBounds.annulus a b → PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) w ∈ (hc.cells I.1).carrier (↑I.1).1 k → w ∈ tsupport (f.term a h r0 I k) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i (f.amplitude k I) (PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) w)‖ ≤ A * ChartScales.Q (↑I.1).1 ^ g * ChartScales.S (↑I.1).1 ^ eAmp) ∧ ∀ (chart : PolarCharts.Index), (PhysicalGraphBounds.scaledRadial (↑I.1).1) w ∈ PolarCharts.chartDomain a chart → (∀ i ≤ m, ‖iteratedFDeriv ℝ i (f.carrier k I.1).F (slotSlow ((f.carrier k I.1).withChart chart) a h (↑I.1).1 r0 w)‖ ≤ B * ChartScales.S (↑I.1).1 ^ eBase) ∧ ∀ i ≤ m, ‖iteratedFDeriv ℝ i (f.carrier k I.1).G (slotSlow ((f.carrier k I.1).withChart chart) a h (↑I.1).1 r0 w)‖ ≤ B * ChartScales.S (↑I.1).1 ^ eBase

theorem NavierStokes.LocalPhysicalCopyBounds.SupportData.tsupport_geometry {H Δ : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} (hr : SupportData f a b h r0 Z Δ) (I : PhysicalWaveSum.WaveIndex H) (k : K) {w : ProblemStatement.SpaceTime} (hw : w ∈ tsupport (f.term a h r0 I k)) : (PhysicalGraphBounds.scaledRadial (↑I.1).1) w ∈ PhysicalGraphBounds.annulus a b ∧ ‖PhysicalGraphBounds.liftZT (PhysicalGraphBounds.physicalLift h (↑I.1).1 w)‖ ≤ Z ∧ |PhysicalGraphBounds.etaCoordinate (PhysicalGraphBounds.nativeGraph h (↑I.1).1 w - (f.carrier k I.1).center)| ≤ r0

theorem NavierStokes.LocalPhysicalCopyBounds.SupportData.periodized_zero_off_annulus {H Δ : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} (hr : SupportData f a b h r0 Z Δ) (I : PhysicalWaveSum.WaveIndex H) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial (↑I.1).1) w ∉ PhysicalGraphBounds.annulus a b) : f.periodized a h r0 I =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.LocalPhysicalCopyBounds.SupportData.periodized_germ_cover {H Δ : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} (hr : SupportData f a b h r0 Z Δ) (hc : PhysicalCopyBounds.SupportCells f) (ha : 0 < a) (I : PhysicalWaveSum.WaveIndex H) (w : ProblemStatement.SpaceTime) : (∃ (k : K), PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) w ∈ (hc.cells I.1).carrier (↑I.1).1 k ∧ f.periodized a h r0 I =ᶠ[nhds w] f.term a h r0 I k) ∨ f.periodized a h r0 I =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.LocalPhysicalCopyBounds.SupportData.periodized_support {H Δ : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} (hr : SupportData f a b h r0 Z Δ) (I : PhysicalWaveSum.WaveIndex H) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) (hn : f.periodized a h r0 I w ≠ 0) : PhysicalWaveSum.physicalParams h w ∈ PhysicalWaveSum.labelRegion (CoordinateAlgebra.D h) ↑I.1

theorem NavierStokes.LocalPhysicalCopyBounds.SupportData.term_smoothAt {H Δ : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} (hr : SupportData f a b h r0 Z Δ) (hs : SmoothData f a h r0) (ha : 0 < a) (I : PhysicalWaveSum.WaveIndex H) (k : K) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) : ContDiffAt ℝ (↑⊤) (f.term a h r0 I k) w

Local native smoothness and the actual support geometry prove physical smoothness at every preterminal point. Outside support this uses the genuine zero germ, not regularity of an unused raw phase.

theorem NavierStokes.LocalPhysicalCopyBounds.SupportData.periodized_smoothAt {H Δ : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} (hr : SupportData f a b h r0 Z Δ) (hs : SmoothData f a h r0) (hc : PhysicalCopyBounds.SupportCells f) (ha : 0 < a) (I : PhysicalWaveSum.WaveIndex H) (w : ProblemStatement.SpaceTime) (hw : w ∈ PhysicalWaveSum.preterminal) : ContDiffAt ℝ (↑⊤) (f.periodized a h r0 I) w

theorem NavierStokes.LocalPhysicalCopyBounds.SupportData.sum_smooth {H Δ : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} (hr : SupportData f a b h r0 Z Δ) (hs : SmoothData f a h r0) (hc : PhysicalCopyBounds.SupportCells f) (ha : 0 < a) (hh : 0 < h) (hh1 : h < 1 / 2) : ContDiffOn ℝ (↑⊤) (f.sum a h r0) PhysicalWaveSum.preterminal

theorem NavierStokes.LocalPhysicalCopyBounds.physical_sum_jet_bound {K : Type u_1} {h a b Z r0 P B eBase : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hZ : 0 ≤ Z) (hr0 : 0 ≤ r0) (hP : 1 ≤ P) (hB : 1 ≤ B) (heBase : 0 ≤ eBase) (H Δ m : ℕ) (g eAmp A : ℝ) (hA : 0 ≤ A) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f : PhysicalCopyBounds.CopyFamily H K), SupportData f a b h r0 Z Δ → SmoothData f a h r0 → ∀ (hc : PhysicalCopyBounds.SupportCells f), JetData f hc a b h r0 P A B g eAmp eBase m → ∀ w ∈ PhysicalWaveSum.preterminal, |w.1| ≤ 1 → ‖iteratedFDeriv ℝ m (f.sum a h r0) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (g - PhysicalGraphBounds.waveLoss h m)

The same physical derivative loss as before, with only local raw input smoothness. The pointwise smooth replacements never enter the output field.

Deriving local smoothness from padded native patches

structure NavierStokes.LocalPhysicalCopyBounds.PatchData {H : ℕ} {K : Type u_1} (f : PhysicalCopyBounds.CopyFamily H K) (a h r0 : ℝ) : Type u_1

Actual native closed cores inside the open smooth patches. The core support fields concern input amplitudes and their native phase evaluation, not the smoothness or derivatives of a final physical output.

• amplitudeDomain : K → PhysicalWaveSum.WaveIndex H → Set PhysicalWaveSum.LiftPoint

  Amplitude domain of PatchData, of type K → WaveIndex H → Set LiftPoint.

• amplitudeCore : K → PhysicalWaveSum.WaveIndex H → Set PhysicalWaveSum.LiftPoint

  Amplitude core of PatchData, of type K → WaveIndex H → Set LiftPoint.

• amplitudeOpen (k : K) (I : PhysicalWaveSum.WaveIndex H) : IsOpen (self.amplitudeDomain k I)
• amplitudeClosed (k : K) (I : PhysicalWaveSum.WaveIndex H) : IsClosed (self.amplitudeCore k I)
• amplitudeSubset (k : K) (I : PhysicalWaveSum.WaveIndex H) : self.amplitudeCore k I ⊆ self.amplitudeDomain k I
• amplitudeSmooth (k : K) (I : PhysicalWaveSum.WaveIndex H) : ContDiffOn ℝ (↑⊤) (f.amplitude k I) (self.amplitudeDomain k I)
• amplitudeSupport (k : K) (I : PhysicalWaveSum.WaveIndex H) : Function.support (f.amplitude k I) ⊆ self.amplitudeCore k I
• slowDomain : K → PhysicalWaveSum.BandLabel → Set PhysicalGraphBounds.Slow

  Slow domain of PatchData, of type K → BandLabel → Set PhysicalGraphBounds.Slow.

• slowCore : K → PhysicalWaveSum.BandLabel → Set PhysicalGraphBounds.Slow

  Slow core of PatchData, of type K → BandLabel → Set PhysicalGraphBounds.Slow.

• slowOpen (k : K) (L : PhysicalWaveSum.BandLabel) : IsOpen (self.slowDomain k L)
• slowClosed (k : K) (L : PhysicalWaveSum.BandLabel) : IsClosed (self.slowCore k L)
• slowSubset (k : K) (L : PhysicalWaveSum.BandLabel) : self.slowCore k L ⊆ self.slowDomain k L
• FSmooth (k : K) (L : PhysicalWaveSum.BandLabel) : ContDiffOn ℝ (↑⊤) (f.carrier k L).F (self.slowDomain k L)
• GSmooth (k : K) (L : PhysicalWaveSum.BandLabel) : ContDiffOn ℝ (↑⊤) (f.carrier k L).G (self.slowDomain k L)
• slowSupport (k : K) (I : PhysicalWaveSum.WaveIndex H) (y : ProblemStatement.SpaceTime) : y ∈ PhysicalWaveSum.preterminal → f.amplitude k I (PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) y) ≠ 0 → ∀ (chart : PolarCharts.Index), (PhysicalGraphBounds.scaledRadial (↑I.1).1) y ∈ PolarCharts.chartDomain a chart → slotSlow ((f.carrier k I.1).withChart chart) a h (↑I.1).1 r0 y ∈ self.slowCore k I.1

theorem NavierStokes.LocalPhysicalCopyBounds.PatchData.amplitude_contDiff {H : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a h r0 : ℝ} (hp : PatchData f a h r0) (k : K) (I : PhysicalWaveSum.WaveIndex H) : ContDiff ℝ (↑⊤) (f.amplitude k I)

The constructed, already localized amplitude is globally smooth if its closed native support is contained in the local smooth patch. This is a conclusion; raw phase profiles retain only local smoothness.

theorem NavierStokes.LocalPhysicalCopyBounds.PatchData.smoothData {H Δ : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} (hp : PatchData f a h r0) (hr : SupportData f a b h r0 Z Δ) (ha : 0 < a) : SmoothData f a h r0

Closed cores keep every supported phase evaluation inside the genuine smooth patch even at the boundary of the amplitude's support.

theorem NavierStokes.LocalPhysicalCopyBounds.PatchData.sum_smooth {H Δ : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} (hp : PatchData f a h r0) (hr : SupportData f a b h r0 Z Δ) (hc : PhysicalCopyBounds.SupportCells f) (ha : 0 < a) (hh : 0 < h) (hh1 : h < 1 / 2) : ContDiffOn ℝ (↑⊤) (f.sum a h r0) PhysicalWaveSum.preterminal

theorem NavierStokes.LocalPhysicalCopyBounds.SupportData.sum_support {H Δ : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} (hr : SupportData f a b h r0 Z Δ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hn : f.sum a h r0 w ≠ 0) : ∃ (I : PhysicalWaveSum.WaveIndex H) (k : K), f.amplitude k I (PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) w) ≠ 0 ∧ (PhysicalGraphBounds.scaledRadial (↑I.1).1) w ∈ PhysicalGraphBounds.annulus a b ∧ PhysicalWaveSum.physicalParams h w ∈ PhysicalWaveSum.labelRegion (CoordinateAlgebra.D h) ↑I.1

The actual full sum still has a supported-copy witness. This statement needs no smoothness of the raw coefficient or phase totalizations.

theorem NavierStokes.LocalPhysicalCopyBounds.SupportData.sum_locally_finite {H Δ : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} (hr : SupportData f a b h r0 Z Δ) (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : ∃ (s : Finset (PhysicalWaveSum.WaveIndex H)), s.card ≤ 2250 * (2 * H + 1) ∧ f.sum a h r0 =ᶠ[nhds w] fun (y : ProblemStatement.SpaceTime) => ∑ I ∈ s, f.periodized a h r0 I y

theorem NavierStokes.LocalPhysicalCopyBounds.SupportData.periodized_germ_of_cell {H Δ : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} (hr : SupportData f a b h r0 Z Δ) (hc : PhysicalCopyBounds.SupportCells f) (ha : 0 < a) (I : PhysicalWaveSum.WaveIndex H) (k : K) {w : ProblemStatement.SpaceTime} (hk : PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) w ∈ (hc.cells I.1).carrier (↑I.1).1 k) : f.periodized a h r0 I =ᶠ[nhds w] f.term a h r0 I k

theorem NavierStokes.LocalPhysicalCopyBounds.SupportData.periodized_jet_eq {H Δ : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} (hr : SupportData f a b h r0 Z Δ) (hc : PhysicalCopyBounds.SupportCells f) (ha : 0 < a) (I : PhysicalWaveSum.WaveIndex H) (k : K) {w : ProblemStatement.SpaceTime} (hk : PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) w ∈ (hc.cells I.1).carrier (↑I.1).1 k) (m : ℕ) : iteratedFDeriv ℝ m (f.periodized a h r0 I) w = iteratedFDeriv ℝ m (f.term a h r0 I k) w

Weighted bounds confined to the genuine native strip

structure NavierStokes.LocalPhysicalCopyBounds.LocalSourceBounds {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} (s : WeightedClasses.StripData D) (h α : ℝ) (w : ι → ℕ → D → ℝ) (source : ι → ℕ → D → E) : Prop

The lower weighted input is only smooth on its actual open native strip. No global smoothness or global support condition on its raw totalization is included.

• uniform : LabelSumBounds.UniformClass s w α source
• flat_geometry : ∃ (cL : ℝ) (cR : ℝ) (L : ℝ) (ρ : D → ℝ), PhysicalClassBounds.FlatGeometry s cL cR L ρ
• weight_le : ∃ (c : ℝ), 0 < c ∧ ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, w l n x ≤ s.zeta x ^ c
• epsilon_eq (n : ℕ) : s.epsilon n = ChartScales.epsilon h n
• slow_le : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ), 4 ≤ n → s.slow n ≤ C * ChartScales.S n ^ p

theorem NavierStokes.LocalPhysicalCopyBounds.LocalSourceBounds.chart_bound {h : ℝ} {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_2} {s : WeightedClasses.StripData D} {α : ℝ} {w : ι → ℕ → D → ℝ} {source : ι → ℕ → D → E} (hs : LocalSourceBounds s h α w source) (m : ℕ) : ∃ (A : ℝ), 0 ≤ A ∧ ∃ (p : ℕ), ∀ (l : ι) (n : ℕ), 4 ≤ n → ∀ x ∈ s.domain, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (source l n) x‖ ≤ A * ChartScales.Q n ^ (h * α) * ChartScales.S n ^ p

Absorb the actual two flat edges and keep the estimate on the valid strip. Extending the raw source outside that strip is unnecessary.

theorem NavierStokes.LocalPhysicalCopyBounds.composition_jet_bound_on {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {X : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] {g : D → E} {φ : X → D} {U : Set X} {V : Set D} (hU : IsOpen U) (hV : IsOpen V) (hg : ContDiffOn ℝ (↑⊤) g V) (hφ : ContDiffOn ℝ (↑⊤) φ U) (hmap : Set.MapsTo φ U V) {x : X} (hx : x ∈ U) (m : ℕ) {A B : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hgb : ∀ i ≤ m, ‖iteratedFDeriv ℝ i g (φ x)‖ ≤ A) (hφb : ∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDeriv ℝ i φ x‖ ≤ B) (j : ℕ) : j ≤ m → ‖iteratedFDeriv ℝ j (g ∘ φ) x‖ ≤ ↑m.factorial * A * B ^ m

Higher chain-rule estimate using only open source and target patches.

structure NavierStokes.LocalPhysicalCopyBounds.CommonChart {H : ℕ} {K : Type u_1} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_2} (f : PhysicalCopyBounds.CopyFamily H K) (hc : PhysicalCopyBounds.SupportCells f) (a b h r0 σ : ℝ) (source : ι → ℕ → D → ℂ) : Type (max u_1 u_2)

The genuine common-chart formula holds on the open interior. Supported physical points may lie in its closure, including a moving radial edge.

• sourceIndex : K → PhysicalWaveSum.WaveIndex H → ι

  Source index of CommonChart, of type K → WaveIndex H → ι.

• map : K → PhysicalWaveSum.WaveIndex H → PhysicalWaveSum.LiftPoint → D

  Map of CommonChart, of type K → WaveIndex H → LiftPoint → D.

• domain : K → PhysicalWaveSum.WaveIndex H → Set PhysicalWaveSum.LiftPoint

  Domain of CommonChart, of type K → WaveIndex H → Set LiftPoint.

• open_domain (k : K) (I : PhysicalWaveSum.WaveIndex H) : IsOpen (self.domain k I)
• smooth (k : K) (I : PhysicalWaveSum.WaveIndex H) : ContDiffOn ℝ (↑⊤) (self.map k I) (self.domain k I)
• positive_jets (m : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∃ (q : ℕ), ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), ∀ x ∈ self.domain k I, ∀ (j : ℕ), 1 ≤ j → j ≤ m → ‖iteratedFDeriv ℝ j (self.map k I) x‖ ≤ B * ChartScales.S (↑I.1).1 ^ q
• amplitude_eq (k : K) (I : PhysicalWaveSum.WaveIndex H) : Set.EqOn (f.amplitude k I) (fun (x : PhysicalWaveSum.LiftPoint) => ChartScales.Q (↑I.1).1 ^ σ • source (self.sourceIndex k I) (↑I.1).1 (self.map k I x)) (self.domain k I)
• contains (k : K) (I : PhysicalWaveSum.WaveIndex H) (z : ProblemStatement.SpaceTime) : z ∈ PhysicalWaveSum.preterminal → PhysicalWaveSum.physicalParams h z ∈ PhysicalWaveSum.labelRegion (CoordinateAlgebra.D h) ↑I.1 → (PhysicalGraphBounds.scaledRadial (↑I.1).1) z ∈ PhysicalGraphBounds.annulus a b → PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) z ∈ (hc.cells I.1).carrier (↑I.1).1 k → z ∈ tsupport (f.term a h r0 I k) → PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) z ∈ closure (self.domain k I)

theorem NavierStokes.LocalPhysicalCopyBounds.commonChart_amplitude_bound {H : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_2} {s : WeightedClasses.StripData D} {α σ : ℝ} {w : ι → ℕ → D → ℝ} {source : ι → ℕ → D → ℂ} (hs : LocalSourceBounds s h α w source) {hc : PhysicalCopyBounds.SupportCells f} (hchart : CommonChart f hc a b h r0 σ source) (hmap : ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), Set.MapsTo (hchart.map k I) (hchart.domain k I) s.domain) (m : ℕ) : ∃ (A : ℝ), 0 ≤ A ∧ ∃ (p : ℕ), ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), ∀ x ∈ hchart.domain k I, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f.amplitude k I) x‖ ≤ A * ChartScales.Q (↑I.1).1 ^ (h * α + σ) * ChartScales.S (↑I.1).1 ^ p

theorem NavierStokes.LocalPhysicalCopyBounds.localStrippedClass_of_weighted {H : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_2} {s : WeightedClasses.StripData D} {α σ P : ℝ} {w : ι → ℕ → D → ℝ} {source : ι → ℕ → D → ℂ} (hs : LocalSourceBounds s h α w source) {hc : PhysicalCopyBounds.SupportCells f} (hchart : CommonChart f hc a b h r0 σ source) (hmap : ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), Set.MapsTo (hchart.map k I) (hchart.domain k I) s.domain) (hb : PhysicalCopyBounds.CarrierBounds f hc a b h r0) (hsmooth : SmoothData f a h r0) (hp : ∀ (k : K) (L : PhysicalWaveSum.BandLabel), |(f.carrier k L).angular| ≤ P ∧ |(f.carrier k L).axial| ≤ P ∧ |(f.carrier k L).radial| ≤ P) (m : ℕ) : ∃ (A : ℝ), 0 ≤ A ∧ ∃ (B : ℝ), 1 ≤ B ∧ ∃ (p : ℕ) (q : ℕ), JetData f hc a b h r0 P A B (h * α + σ) (↑p) (↑q) m

theorem NavierStokes.LocalPhysicalCopyBounds.physical_sum_jet_bound_of_weighted {H Δ : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 Z : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_2} {s : WeightedClasses.StripData D} {α σ P : ℝ} {w : ι → ℕ → D → ℝ} {source : ι → ℕ → D → ℂ} (hsource : LocalSourceBounds s h α w source) {hc : PhysicalCopyBounds.SupportCells f} (hchart : CommonChart f hc a b h r0 σ source) (hmap : ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), Set.MapsTo (hchart.map k I) (hchart.domain k I) s.domain) (hb : PhysicalCopyBounds.CarrierBounds f hc a b h r0) (hr : SupportData f a b h r0 Z Δ) (hs : SmoothData f a h r0) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hZ : 0 ≤ Z) (hr0 : 0 ≤ r0) (hP : 1 ≤ P) (hp : ∀ (k : K) (L : PhysicalWaveSum.BandLabel), |(f.carrier k L).angular| ≤ P ∧ |(f.carrier k L).axial| ≤ P ∧ |(f.carrier k L).radial| ≤ P) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ z ∈ PhysicalWaveSum.preterminal, |z.1| ≤ 1 → ‖iteratedFDeriv ℝ m (f.sum a h r0) z‖ ≤ C * PhysicalWaveSum.physicalQ h z ^ (h * α - PhysicalClassBounds.physicalLoss h σ m)

theorem NavierStokes.LocalPhysicalCopyBounds.SmoothData.of_open_patches {H : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a h r0 : ℝ} (UA : K → PhysicalWaveSum.WaveIndex H → Set PhysicalWaveSum.LiftPoint) (UP : K → PhysicalWaveSum.BandLabel → Set PhysicalGraphBounds.Slow) (hUA : ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), IsOpen (UA k I)) (hUP : ∀ (k : K) (L : PhysicalWaveSum.BandLabel), IsOpen (UP k L)) (hA : ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), ContDiffOn ℝ (↑⊤) (f.amplitude k I) (UA k I)) (hF : ∀ (k : K) (L : PhysicalWaveSum.BandLabel), ContDiffOn ℝ (↑⊤) (f.carrier k L).F (UP k L)) (hG : ∀ (k : K) (L : PhysicalWaveSum.BandLabel), ContDiffOn ℝ (↑⊤) (f.carrier k L).G (UP k L)) (haCover : ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), ∀ w ∈ PhysicalWaveSum.preterminal, w ∈ tsupport (f.term a h r0 I k) → PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) w ∈ UA k I) (hpCover : ∀ (k : K) (I : PhysicalWaveSum.WaveIndex H), ∀ w ∈ PhysicalWaveSum.preterminal, w ∈ tsupport (f.term a h r0 I k) → ∀ (chart : PolarCharts.Index), (PhysicalGraphBounds.scaledRadial (↑I.1).1) w ∈ PolarCharts.chartDomain a chart → slotSlow ((f.carrier k I.1).withChart chart) a h (↑I.1).1 r0 w ∈ UP k I.1) : SmoothData f a h r0

Direct interface for the actual valid native open patches, including patches whose raw totalizations need not be smooth on their boundary.

theorem NavierStokes.LocalPhysicalCopyBounds.JetData.of_stripped {H : ℕ} {K : Type u_1} {f : PhysicalCopyBounds.CopyFamily H K} {a b h r0 : ℝ} {hc : PhysicalCopyBounds.SupportCells f} {P A B g eAmp eBase : ℝ} {m : ℕ} (hb : PhysicalCopyBounds.LocalStrippedClass f hc a b h r0 P A B g eAmp eBase m) : JetData f hc a b h r0 P A B g eAmp eBase m

theorem NavierStokes.LocalPhysicalCopyBounds.supportData_of_native {H Δ : ℕ} {a b h r0 Z : ℝ} {F : PhysicalCopyBounds.CopyFamily H TorusInverse.Frequency} (g : PhysicalWaveSum.BandLabel → CommonCoverSolve.Geometry) (U : PhysicalWaveSum.BandLabel → Set PhysicalWaveSum.Plane) (hgap : ∀ (L : PhysicalWaveSum.BandLabel), (g L).gap = F.gap L) (hcenter : ∀ (k : TorusInverse.Frequency) (L : PhysicalWaveSum.BandLabel), (F.carrier k L).center = PhysicalCopyBounds.nativeCenter (g L) k) (hwidth : ∀ (L : PhysicalWaveSum.BandLabel), ∀ z ∈ U L, |PhysicalGraphBounds.etaCoordinate ((g L).basis z)| ≤ r0) (hs : ∀ (k : TorusInverse.Frequency) (I : PhysicalWaveSum.WaveIndex H) (x : PhysicalWaveSum.LiftPoint), F.amplitude k I x ≠ 0 → (g I.1).coordinates k x.2 ∈ U I.1) (hgap_le : ∀ (L : PhysicalWaveSum.BandLabel), F.gap L ≤ Δ) (hgap_native : ∀ (L : PhysicalWaveSum.BandLabel), F.gap L ≤ ChartScales.nativeIndex h (↑L).1) (hint : ∀ (k : TorusInverse.Frequency) (L : PhysicalWaveSum.BandLabel), ∃ (m : ℤ), ↑(ChartScales.carrier h (↑L).1) * (F.carrier k L).angular = ↑m) (hgeo : ∀ (k : TorusInverse.Frequency) (I : PhysicalWaveSum.WaveIndex H) (y : ProblemStatement.SpaceTime), F.amplitude k I (PhysicalWaveSum.commonLift h (↑I.1).1 (F.gap I.1) y) ≠ 0 → (PhysicalGraphBounds.scaledRadial (↑I.1).1) y ∈ PhysicalGraphBounds.annulus a b ∧ ‖PhysicalGraphBounds.liftZT (PhysicalGraphBounds.physicalLift h (↑I.1).1 y)‖ ≤ Z) (hmask : ∀ (k : TorusInverse.Frequency) (I : PhysicalWaveSum.WaveIndex H), ∀ y ∈ PhysicalWaveSum.preterminal, F.amplitude k I (PhysicalWaveSum.commonLift h (↑I.1).1 (F.gap I.1) y) ≠ 0 → PhysicalWaveSum.physicalMask (CoordinateAlgebra.D h) (↑I.1) (PhysicalWaveSum.physicalParams h y) ≠ 0) : SupportData F a b h r0 Z Δ

The native lattice-center construction proves the support data without any global smoothness hypotheses on amplitudes or phase profiles.

Real Cartesian vectors

theorem NavierStokes.LocalPhysicalCopyBounds.vectorSum_smooth {H Δ : ℕ} {K : Type u_1} {a b h r0 Z : ℝ} {f : Fin 3 → PhysicalCopyBounds.CopyFamily H K} (hr : ∀ (i : Fin 3), SupportData (f i) a b h r0 Z Δ) (hs : ∀ (i : Fin 3), SmoothData (f i) a h r0) (hc : (i : Fin 3) → PhysicalCopyBounds.SupportCells (f i)) (ha : 0 < a) (hh : 0 < h) (hh1 : h < 1 / 2) : ContDiffOn ℝ (↑⊤) (PhysicalCopyBounds.vectorSum f a h r0) PhysicalWaveSum.preterminal

theorem NavierStokes.LocalPhysicalCopyBounds.vectorSum_jet_bound {H Δ : ℕ} {K : Type u_1} {a b h r0 Z : ℝ} {f : Fin 3 → PhysicalCopyBounds.CopyFamily H K} (hr : ∀ (i : Fin 3), SupportData (f i) a b h r0 Z Δ) (hs : ∀ (i : Fin 3), SmoothData (f i) a h r0) (hc : (i : Fin 3) → PhysicalCopyBounds.SupportCells (f i)) (ha : 0 < a) (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (m : ℕ) {B : ℝ} (hb : ∀ (i : Fin 3), ‖iteratedFDeriv ℝ m ((f i).sum a h r0) w‖ ≤ B) : ‖iteratedFDeriv ℝ m (PhysicalCopyBounds.vectorSum f a h r0) w‖ ≤ 3 * B

theorem NavierStokes.LocalPhysicalCopyBounds.physical_vector_sum_jet_bound {K : Type u_1} {h a b Z r0 P B eBase : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hZ : 0 ≤ Z) (hr0 : 0 ≤ r0) (hP : 1 ≤ P) (hB : 1 ≤ B) (heBase : 0 ≤ eBase) (H Δ m : ℕ) (g eAmp A : ℝ) (hA : 0 ≤ A) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f : Fin 3 → PhysicalCopyBounds.CopyFamily H K), (∀ (i : Fin 3), SupportData (f i) a b h r0 Z Δ) → (∀ (i : Fin 3), SmoothData (f i) a h r0) → ∀ (hc : (i : Fin 3) → PhysicalCopyBounds.SupportCells (f i)), (∀ (i : Fin 3), JetData (f i) (hc i) a b h r0 P A B g eAmp eBase m) → ∀ w ∈ PhysicalWaveSum.preterminal, |w.1| ≤ 1 → ‖iteratedFDeriv ℝ m (PhysicalCopyBounds.vectorSum f a h r0) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (g - PhysicalGraphBounds.waveLoss h m)

theorem NavierStokes.LocalPhysicalCopyBounds.physical_vector_sum_jet_bound_of_weighted {H Δ : ℕ} {K : Type u_1} {a b h r0 Z : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_2} {s : WeightedClasses.StripData D} {α σ P : ℝ} {w : ι → ℕ → D → ℝ} {source : ι → ℕ → D → ℂ} (hsource : LocalSourceBounds s h α w source) {f : Fin 3 → PhysicalCopyBounds.CopyFamily H K} (hc : (i : Fin 3) → PhysicalCopyBounds.SupportCells (f i)) (hchart : (i : Fin 3) → CommonChart (f i) (hc i) a b h r0 σ source) (hmap : ∀ (i : Fin 3) (k : K) (I : PhysicalWaveSum.WaveIndex H), Set.MapsTo ((hchart i).map k I) ((hchart i).domain k I) s.domain) (hb : (i : Fin 3) → PhysicalCopyBounds.CarrierBounds (f i) (hc i) a b h r0) (hr : ∀ (i : Fin 3), SupportData (f i) a b h r0 Z Δ) (hs : ∀ (i : Fin 3), SmoothData (f i) a h r0) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hZ : 0 ≤ Z) (hr0 : 0 ≤ r0) (hP : 1 ≤ P) (hp : ∀ (i : Fin 3) (k : K) (L : PhysicalWaveSum.BandLabel), |((f i).carrier k L).angular| ≤ P ∧ |((f i).carrier k L).axial| ≤ P ∧ |((f i).carrier k L).radial| ≤ P) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ z ∈ PhysicalWaveSum.preterminal, |z.1| ≤ 1 → ‖iteratedFDeriv ℝ m (PhysicalCopyBounds.vectorSum f a h r0) z‖ ≤ C * PhysicalWaveSum.physicalQ h z ^ (h * α - PhysicalClassBounds.physicalLoss h σ m)