Physical bounds for locally finite native copies

Each native copy retains its own center and its own full oscillatory carrier. We sum these waves, not their amplitudes under one unwrapped phase. Closed, locally finite, disjoint native cells give an actual single-copy germ. The physical estimate is then the center-independent single-carrier estimate, followed by the existing bounded overlap estimate for the outer labels.

theorem NavierStokes.PhysicalCopyBounds.copySum_pullback_germ {X : Type u_1} {Y : Type u_2} {E : Type u_3} {I : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [NormedAddCommGroup E] (K : PeriodizedWaveBounds.Cells Y I) (n : ℕ) (φ : X → Y) (f : I → X → E) (hs : ∀ (i : I) (x : X), f i x ≠ 0 → φ x ∈ K.carrier n i) {x : X} (hφ : ContinuousAt φ x) {i : I} (hi : φ x ∈ K.carrier n i) : (fun (y : X) => ∑' (k : I), f k y) =ᶠ[nhds x] f i

Pull back the native cells only near the evaluation point. Global continuity of the physical graph at the axis is not needed.

theorem NavierStokes.PhysicalCopyBounds.copySum_pullback_zero_germ {X : Type u_1} {Y : Type u_2} {E : Type u_3} {I : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [NormedAddCommGroup E] (K : PeriodizedWaveBounds.Cells Y I) (n : ℕ) (φ : X → Y) (f : I → X → E) (hs : ∀ (i : I) (x : X), f i x ≠ 0 → φ x ∈ K.carrier n i) {x : X} (hφ : ContinuousAt φ x) (hi : ∀ (i : I), φ x ∉ K.carrier n i) : (fun (y : X) => ∑' (k : I), f k y) =ᶠ[nhds x] fun (x : X) => 0

theorem NavierStokes.PhysicalCopyBounds.copySum_pullback_germ_cover {X : Type u_1} {Y : Type u_2} {E : Type u_3} {I : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [NormedAddCommGroup E] (K : PeriodizedWaveBounds.Cells Y I) (n : ℕ) (φ : X → Y) (f : I → X → E) (hs : ∀ (i : I) (x : X), f i x ≠ 0 → φ x ∈ K.carrier n i) {x : X} (hφ : ContinuousAt φ x) : (∃ (i : I), φ x ∈ K.carrier n i ∧ (fun (y : X) => ∑' (k : I), f k y) =ᶠ[nhds x] f i) ∨ (fun (y : X) => ∑' (k : I), f k y) =ᶠ[nhds x] fun (x : X) => 0

structure NavierStokes.PhysicalCopyBounds.CopyFamily (H : ℕ) (K : Type u_1) : Type u_1

The lattice copy is a separate index. In particular, neither the center nor the phase profiles have to agree between different copies.

• gap : PhysicalWaveSum.BandLabel → ℕ

  Gap of CopyFamily, of type BandLabel → ℕ.

• carrier : K → PhysicalWaveSum.BandLabel → PhysicalWaveSum.CarrierData

  Carrier of CopyFamily, of type K → BandLabel → CarrierData.

• amplitude : K → PhysicalWaveSum.WaveIndex H → PhysicalWaveSum.LiftPoint → ℂ

  Amplitude of CopyFamily, of type K → WaveIndex H → LiftPoint → ℂ.

noncomputable def NavierStokes.PhysicalCopyBounds.CopyFamily.copy {H : ℕ} {K : Type u_1} (f : CopyFamily H K) (k : K) : PhysicalWaveSum.WaveFamily H

Copy, given by ⟨f.gap, f.carrier k, f.amplitude k⟩.

Equations

• f.copy k = { gap := f.gap, carrier := f.carrier k, amplitude := f.amplitude k }

noncomputable def NavierStokes.PhysicalCopyBounds.CopyFamily.term {H : ℕ} {K : Type u_1} (f : CopyFamily H K) (a h r0 : ℝ) (I : PhysicalWaveSum.WaveIndex H) (k : K) : ProblemStatement.SpaceTime → ℂ

Term, given by (f.copy k).term a h r0 I.

Equations

• f.term a h r0 I k = (f.copy k).term a h r0 I

noncomputable def NavierStokes.PhysicalCopyBounds.CopyFamily.periodized {H : ℕ} {K : Type u_1} (f : CopyFamily H K) (a h r0 : ℝ) (I : PhysicalWaveSum.WaveIndex H) (w : ProblemStatement.SpaceTime) : ℂ

Sum full local carriers, including their individual phases.

Equations

• f.periodized a h r0 I w = ∑' (k : K), f.term a h r0 I k w

noncomputable def NavierStokes.PhysicalCopyBounds.CopyFamily.sum {H : ℕ} {K : Type u_1} (f : CopyFamily H K) (a h r0 : ℝ) (w : ProblemStatement.SpaceTime) : ℂ

Sum, given by ∑ᶠ I, f.periodized a h r0 I w.

Equations

• f.sum a h r0 w = ∑ᶠ (I : NavierStokes.PhysicalWaveSum.WaveIndex H), f.periodized a h r0 I w

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

The old single-copy regularity hypotheses are imposed separately on each actual copy. No support condition is imposed using one center for the whole periodized amplitude.

• copy (k : K) : PhysicalWaveSum.RegularFamily (f.copy k) a b h r0 Z Δ

structure NavierStokes.PhysicalCopyBounds.SupportCells {H : ℕ} {K : Type u_1} (f : CopyFamily H K) : Type u_1

Native support cells can depend on the outer label. Their index is independent of both the harmonic and the physical point.

• cells : PhysicalWaveSum.BandLabel → PeriodizedWaveBounds.Cells PhysicalWaveSum.LiftPoint K

  Cells of SupportCells, of type BandLabel → PeriodizedWaveBounds.Cells LiftPoint K.

• support (I : PhysicalWaveSum.WaveIndex H) (k : K) : Function.support (f.amplitude k I) ⊆ (self.cells I.1).carrier (↑I.1).1 k

theorem NavierStokes.PhysicalCopyBounds.RegularFamily.term_smooth {H Δ : ℕ} {K : Type u_1} {f : CopyFamily H K} {a b h r0 Z : ℝ} (hr : RegularFamily f a b h r0 Z Δ) (ha : 0 < a) (I : PhysicalWaveSum.WaveIndex H) (k : K) : ContDiff ℝ (↑⊤) (f.term a h r0 I k)

theorem NavierStokes.PhysicalCopyBounds.SupportCells.term_mem {H : ℕ} {K : Type u_1} {f : CopyFamily H K} {a h r0 : ℝ} (hc : SupportCells f) (I : PhysicalWaveSum.WaveIndex H) (k : K) (w : ProblemStatement.SpaceTime) (hw : f.term a h r0 I k w ≠ 0) : PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) w ∈ (hc.cells I.1).carrier (↑I.1).1 k

theorem NavierStokes.PhysicalCopyBounds.RegularFamily.periodized_zero_off_annulus {H Δ : ℕ} {K : Type u_1} {f : CopyFamily H K} {a b h r0 Z : ℝ} (hr : RegularFamily 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

Off the fixed radial annulus, all copies vanish on one common neighborhood. This also handles the axis without a smooth graph there.

theorem NavierStokes.PhysicalCopyBounds.commonLift_continuousAt_of_annulus {a b h : ℝ} (ha : 0 < a) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b) : ContinuousAt (PhysicalWaveSum.commonLift h n d) w

theorem NavierStokes.PhysicalCopyBounds.RegularFamily.periodized_germ_cover {H Δ : ℕ} {K : Type u_1} {f : CopyFamily H K} {a b h r0 Z : ℝ} (hr : RegularFamily f a b h r0 Z Δ) (hc : 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.PhysicalCopyBounds.RegularFamily.periodized_smooth {H Δ : ℕ} {K : Type u_1} {f : CopyFamily H K} {a b h r0 Z : ℝ} (hr : RegularFamily f a b h r0 Z Δ) (hc : SupportCells f) (ha : 0 < a) (I : PhysicalWaveSum.WaveIndex H) : ContDiff ℝ (↑⊤) (f.periodized a h r0 I)

theorem NavierStokes.PhysicalCopyBounds.SupportCells.periodized_eq {H : ℕ} {K : Type u_1} {f : CopyFamily H K} {a h r0 : ℝ} (hc : SupportCells f) (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 w = f.term a h r0 I k w

On a specified native copy cell, the full sum equals that full copy. The identity keeps the copy's own phase as well as its amplitude.

theorem NavierStokes.PhysicalCopyBounds.RegularFamily.periodized_germ_of_cell {H Δ : ℕ} {K : Type u_1} {f : CopyFamily H K} {a b h r0 Z : ℝ} (hr : RegularFamily f a b h r0 Z Δ) (hc : 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.PhysicalCopyBounds.RegularFamily.periodized_jet_eq {H Δ : ℕ} {K : Type u_1} {f : CopyFamily H K} {a b h r0 Z : ℝ} (hr : RegularFamily f a b h r0 Z Δ) (hc : 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

Actual full derivative tensors agree with the selected local copy.

theorem NavierStokes.PhysicalCopyBounds.RegularFamily.periodized_support {H Δ : ℕ} {K : Type u_1} {f : CopyFamily H K} {a b h r0 Z : ℝ} (hr : RegularFamily 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.PhysicalCopyBounds.RegularFamily.sum_smooth {H Δ : ℕ} {K : Type u_1} {f : CopyFamily H K} {a b h r0 Z : ℝ} (hr : RegularFamily f a b h r0 Z Δ) (hc : SupportCells f) (ha : 0 < a) (hh : 0 < h) (hh1 : h < 1 / 2) : ContDiffOn ℝ (↑⊤) (f.sum a h r0) PhysicalWaveSum.preterminal

theorem NavierStokes.PhysicalCopyBounds.RegularFamily.sum_locally_finite {H Δ : ℕ} {K : Type u_1} {f : CopyFamily H K} {a b h r0 Z : ℝ} (hr : RegularFamily 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.PhysicalCopyBounds.SupportCells.term_tsupport_mem {H : ℕ} {K : Type u_1} {f : CopyFamily H K} {a b h r0 : ℝ} (hc : SupportCells f) (ha : 0 < a) (I : PhysicalWaveSum.WaveIndex H) (k : K) {w : ProblemStatement.SpaceTime} (hann : (PhysicalGraphBounds.scaledRadial (↑I.1).1) w ∈ PhysicalGraphBounds.annulus a b) (hw : w ∈ tsupport (f.term a h r0 I k)) : PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) w ∈ (hc.cells I.1).carrier (↑I.1).1 k

Closed-cell membership holds at every point where a copy can have a nonzero jet, including the boundary of its amplitude support.

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

Only native jets on a copy's own closed cell are used. No bounds for uncut data far from that copy are required.

• parameters (k : K) (L : PhysicalWaveSum.BandLabel) : |(f.carrier k L).angular| ≤ P ∧ |(f.carrier k L).axial| ≤ P ∧ |(f.carrier k L).radial| ≤ P
• amplitude (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 → ∀ 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
• base_F (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 → ∀ (chart : PolarCharts.Index), (PhysicalGraphBounds.scaledRadial (↑I.1).1) w ∈ PolarCharts.chartDomain a chart → ∀ i ≤ m, ‖iteratedFDeriv ℝ i (f.carrier k I.1).F (PhysicalGraphBounds.slotMap (PolarCharts.chart a chart) (ChartScales.timeCoefficient h (↑I.1).1) (f.carrier k I.1).center r0 (PhysicalGraphBounds.physicalLift h (↑I.1).1 w)).1‖ ≤ B * ChartScales.S (↑I.1).1 ^ eBase
• base_G (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 → ∀ (chart : PolarCharts.Index), (PhysicalGraphBounds.scaledRadial (↑I.1).1) w ∈ PolarCharts.chartDomain a chart → ∀ i ≤ m, ‖iteratedFDeriv ℝ i (f.carrier k I.1).G (PhysicalGraphBounds.slotMap (PolarCharts.chart a chart) (ChartScales.timeCoefficient h (↑I.1).1) (f.carrier k I.1).center r0 (PhysicalGraphBounds.physicalLift h (↑I.1).1 w)).1‖ ≤ B * ChartScales.S (↑I.1).1 ^ eBase

theorem NavierStokes.PhysicalCopyBounds.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 : CopyFamily H K), RegularFamily f a b h r0 Z Δ → ∀ (hc : SupportCells f), LocalStrippedClass 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 number of native copies does not enter the constant or the power loss. At a physical point the actual wave has just one copy germ.

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

Actual cutoff amplitudes, pulled from their weighted native coefficient through the common-coordinate map. Only the map's positive jets are bounded; its values and the copy centers may be unbounded.

• 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) : 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)
• 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 → PhysicalWaveSum.commonLift h (↑I.1).1 (f.gap I.1) z ∈ self.domain k I

theorem NavierStokes.PhysicalCopyBounds.CommonChart.amplitude_bound {H : ℕ} {K : Type u_1} {f : CopyFamily H K} {a b h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_2} {s : WeightedClasses.StripData D} {α σ : ℝ} {w : ι → ℕ → D → ℝ} {source : ι → ℕ → D → ℂ} (hs : PhysicalClassBounds.SourceBounds s h α w source) {hc : SupportCells f} (hchart : CommonChart f hc a b h σ source) (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

The native weighted bound is converted using the genuine higher chain rule. The same constants work for every label and every native copy.

noncomputable def NavierStokes.PhysicalCopyBounds.copyBandDomain {K : Type u_1} {V : Type u_3} [NormedAddCommGroup V] (U : K → PhysicalWaveSum.BandLabel → Set V) (hU : ∀ (k : K) (L : PhysicalWaveSum.BandLabel), IsOpen (U k L)) : PhaseJetBounds.Domain (K × PhysicalWaveSum.BandLabel) V

Copy band domain, bundling scale, carrier, isOpen, one_le_scale.

Equations

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

structure NavierStokes.PhysicalCopyBounds.CarrierBounds {H : ℕ} {K : Type u_1} (f : CopyFamily H K) (hc : SupportCells f) (a b h r0 : ℝ) : Type u_1

The carrier profiles are estimated on their actual local slow regions. The regions need contain a point only when that point belongs to this copy.

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

  Region of CarrierBounds, of type K → BandLabel → Set PhysicalGraphBounds.Slow.

• open_region (k : K) (L : PhysicalWaveSum.BandLabel) : IsOpen (self.region k L)
• jets : PhaseJetBounds.PolynomialJets (copyBandDomain self.region ⋯) fun (i : K × PhysicalWaveSum.BandLabel) (x : PhysicalGraphBounds.Slow) => ((f.carrier i.1 i.2).F x, (f.carrier i.1 i.2).G x)
• 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 → ∀ (chart : PolarCharts.Index), (PhysicalGraphBounds.scaledRadial (↑I.1).1) z ∈ PolarCharts.chartDomain a chart → (PhysicalGraphBounds.slotMap (PolarCharts.chart a chart) (ChartScales.timeCoefficient h (↑I.1).1) (f.carrier k I.1).center r0 (PhysicalGraphBounds.physicalLift h (↑I.1).1 z)).1 ∈ self.region k I.1

theorem NavierStokes.PhysicalCopyBounds.CarrierBounds.profile_bound {H : ℕ} {K : Type u_1} {f : CopyFamily H K} {a b h r0 : ℝ} {hc : SupportCells f} (hb : CarrierBounds f hc a b h r0) (m : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∃ (p : ℕ), ∀ (k : K) (L : PhysicalWaveSum.BandLabel), ∀ x ∈ hb.region k L, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f.carrier k L).F x‖ ≤ B * ChartScales.S (↑L).1 ^ p ∧ ‖iteratedFDeriv ℝ j (f.carrier k L).G x‖ ≤ B * ChartScales.S (↑L).1 ^ p

theorem NavierStokes.PhysicalCopyBounds.localStrippedClass {H : ℕ} {K : Type u_1} {f : 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 : PhysicalClassBounds.SourceBounds s h α w source) {hc : SupportCells f} (hchart : CommonChart f hc a b h σ source) (hb : CarrierBounds f hc a b 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 : ℕ), LocalStrippedClass f hc a b h r0 P A B (h * α + σ) (↑p) (↑q) m

Lower weighted coefficient classes and actual phase jets supply all inputs of the physical theorem; no physical derivative estimate is assumed.

theorem NavierStokes.PhysicalCopyBounds.physical_sum_jet_bound_of_weighted {H Δ : ℕ} {K : Type u_1} {f : 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 → ℂ} (hs : PhysicalClassBounds.SourceBounds s h α w source) {hc : SupportCells f} (hchart : CommonChart f hc a b h σ source) (hb : CarrierBounds f hc a b h r0) (hr : RegularFamily f a b h r0 Z Δ) (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)

All actual physical jets of the full copy and label sum, from the lower weighted class. Slow polynomial degrees and copy count do not enter the derivative-loss function.

Literal native cells and their lattice centers

noncomputable def NavierStokes.PhysicalCopyBounds.nativeCenter (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) : PhysicalWaveSum.Plane

Native center, given by g.center + TorusAverages.latticePoint k.

Equations

• NavierStokes.PhysicalCopyBounds.nativeCenter g k = g.center + NavierStokes.TorusAverages.latticePoint k

theorem NavierStokes.PhysicalCopyBounds.native_offset (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (Y : PhysicalWaveSum.Plane) : (CommonCoverSolve.coverPower g.gap) Y - nativeCenter g k = g.basis (g.coordinates k Y)

The center used by a copy is its own lattice translate.

theorem NavierStokes.PhysicalCopyBounds.nativeGraph_eq_cover_commonLift (h : ℝ) (n d : ℕ) (w : ProblemStatement.SpaceTime) : PhysicalGraphBounds.nativeGraph h n w = (CommonCoverSolve.coverPower d) (PhysicalWaveSum.commonLift h n d w).2

theorem NavierStokes.PhysicalCopyBounds.physical_native_offset (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (h : ℝ) (n d : ℕ) (hgap : g.gap = d) (w : ProblemStatement.SpaceTime) : PhysicalGraphBounds.nativeGraph h n w - nativeCenter g k = g.basis (g.coordinates k (PhysicalWaveSum.commonLift h n d w).2)

theorem NavierStokes.PhysicalCopyBounds.physical_native_width (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (h : ℝ) (n d : ℕ) (hgap : g.gap = d) {U : Set PhysicalWaveSum.Plane} {r0 : ℝ} (hU : ∀ z ∈ U, |PhysicalGraphBounds.etaCoordinate (g.basis z)| ≤ r0) (w : ProblemStatement.SpaceTime) (hw : g.coordinates k (PhysicalWaveSum.commonLift h n d w).2 ∈ U) : |PhysicalGraphBounds.etaCoordinate (PhysicalGraphBounds.nativeGraph h n w - nativeCenter g k)| ≤ r0

The physical slot-width bound follows from the native cell width and the exact cover map, rather than being assumed for a periodized field.

noncomputable def NavierStokes.PhysicalCopyBounds.nativeSupportCells {H : ℕ} {F : CopyFamily H TorusInverse.Frequency} (g : PhysicalWaveSum.BandLabel → CommonCoverSolve.Geometry) (U : PhysicalWaveSum.BandLabel → Set PhysicalWaveSum.Plane) (hU : ∀ (L : PhysicalWaveSum.BandLabel), IsCompact (U L)) (hinj : ∀ (L : PhysicalWaveSum.BandLabel), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (g L).center + (g L).basis z) '' U L)) (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) : SupportCells F

Build the abstract support cells from the actual native affine lattice charts. Compactness gives local finiteness; quotient injectivity gives disjointness, both through PeriodizedWaveBounds.nativeCells.

Equations

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

@[simp]

theorem NavierStokes.PhysicalCopyBounds.nativeSupportCells_mem {H : ℕ} {F : CopyFamily H TorusInverse.Frequency} (g : PhysicalWaveSum.BandLabel → CommonCoverSolve.Geometry) (U : PhysicalWaveSum.BandLabel → Set PhysicalWaveSum.Plane) (hU : ∀ (L : PhysicalWaveSum.BandLabel), IsCompact (U L)) (hinj : ∀ (L : PhysicalWaveSum.BandLabel), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (g L).center + (g L).basis z) '' U L)) (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) (I : PhysicalWaveSum.WaveIndex H) (k : TorusInverse.Frequency) (x : PhysicalWaveSum.LiftPoint) : x ∈ ((nativeSupportCells g U hU hinj hs).cells I.1).carrier (↑I.1).1 k ↔ (g I.1).coordinates k x.2 ∈ U I.1

noncomputable def NavierStokes.PhysicalCopyBounds.nativeCutoffSupportCells {H : ℕ} {F : CopyFamily H TorusInverse.Frequency} (g : PhysicalWaveSum.BandLabel → CommonCoverSolve.Geometry) (U : PhysicalWaveSum.BandLabel → Set PhysicalWaveSum.Plane) (hU : ∀ (L : PhysicalWaveSum.BandLabel), IsCompact (U L)) (hinj : ∀ (L : PhysicalWaveSum.BandLabel), Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (g L).center + (g L).basis z) '' U L)) (κ : PhysicalWaveSum.BandLabel → PhysicalWaveSum.Plane → ℝ) (hκ : ∀ (L : PhysicalWaveSum.BandLabel), Function.support (κ L) ⊆ U L) (v : TorusInverse.Frequency → PhysicalWaveSum.WaveIndex H → PhysicalWaveSum.LiftPoint → ℂ) (he : ∀ (k : TorusInverse.Frequency) (I : PhysicalWaveSum.WaveIndex H) (x : PhysicalWaveSum.LiftPoint), F.amplitude k I x = κ I.1 ((g I.1).coordinates k x.2) • v k I x) : SupportCells F

For the actual localized coefficients, the support premise is itself derived from the literal cutoff factor.

Equations

• NavierStokes.PhysicalCopyBounds.nativeCutoffSupportCells g U hU hinj κ hκ v he = NavierStokes.PhysicalCopyBounds.nativeSupportCells g U hU hinj ⋯

theorem NavierStokes.PhysicalCopyBounds.regular_of_native {H Δ : ℕ} {a b h r0 Z : ℝ} {F : 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 = 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) (hamp : ∀ (k : TorusInverse.Frequency) (I : PhysicalWaveSum.WaveIndex H), ContDiff ℝ (↑⊤) (F.amplitude k I)) (hF : ∀ (k : TorusInverse.Frequency) (L : PhysicalWaveSum.BandLabel), ContDiff ℝ (↑⊤) (F.carrier k L).F) (hG : ∀ (k : TorusInverse.Frequency) (L : PhysicalWaveSum.BandLabel), ContDiff ℝ (↑⊤) (F.carrier k L).G) (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) : RegularFamily F a b h r0 Z Δ

A native cell description proves all copy-width support conditions in the regularity record. The radial annulus, slow mask, and smooth coefficient inputs are separate, as in the original construction.

Exact support and vector-valued consequences

theorem NavierStokes.PhysicalCopyBounds.CopyFamily.sum_nonzero_term {H : ℕ} {K : Type u_1} (f : CopyFamily H K) {a h r0 : ℝ} {w : ProblemStatement.SpaceTime} (hw : f.sum a h r0 w ≠ 0) : ∃ (I : PhysicalWaveSum.WaveIndex H) (k : K), f.term a h r0 I k w ≠ 0

theorem NavierStokes.PhysicalCopyBounds.RegularFamily.sum_support {H Δ : ℕ} {K : Type u_1} {f : CopyFamily H K} {a b h r0 Z : ℝ} (hr : RegularFamily 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

A nonzero full sum has a genuine supported copy witness. This is the primitive support statement needed for the shrinking physical annulus.

noncomputable def NavierStokes.PhysicalCopyBounds.vectorSum {H : ℕ} {K : Type u_1} (f : Fin 3 → CopyFamily H K) (a h r0 : ℝ) (w : ProblemStatement.SpaceTime) : ProblemStatement.Space

Vector sum, given by ∑ i : Fin 3, realCoordinate i ((f i).sum a h r0 w).

Equations

• NavierStokes.PhysicalCopyBounds.vectorSum f a h r0 w = ∑ i : Fin 3, (NavierStokes.PhysicalWaveSum.realCoordinate i) ((f i).sum a h r0 w)

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

theorem NavierStokes.PhysicalCopyBounds.vectorSum_jet_bound {H Δ : ℕ} {K : Type u_1} {a b h r0 Z : ℝ} {f : Fin 3 → CopyFamily H K} (hr : ∀ (i : Fin 3), RegularFamily (f i) a b h r0 Z Δ) (hc : (i : Fin 3) → 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 (vectorSum f a h r0) w‖ ≤ 3 * B

theorem NavierStokes.PhysicalCopyBounds.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 → CopyFamily H K), (∀ (i : Fin 3), RegularFamily (f i) a b h r0 Z Δ) → ∀ (hc : (i : Fin 3) → SupportCells (f i)), (∀ (i : Fin 3), LocalStrippedClass (f i) (hc i) a b h r0 P A B g eAmp eBase m) → ∀ w ∈ PhysicalWaveSum.preterminal, |w.1| ≤ 1 → ‖iteratedFDeriv ℝ m (vectorSum f a h r0) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (g - PhysicalGraphBounds.waveLoss h m)

Uniform scalar input bounds give the actual real three-component physical estimate with the same loss exponent.

theorem NavierStokes.PhysicalCopyBounds.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 → ℂ} (hs : PhysicalClassBounds.SourceBounds s h α w source) {f : Fin 3 → CopyFamily H K} (hc : (i : Fin 3) → SupportCells (f i)) (hchart : (i : Fin 3) → CommonChart (f i) (hc i) a b h σ source) (hb : (i : Fin 3) → CarrierBounds (f i) (hc i) a b h r0) (hr : ∀ (i : Fin 3), RegularFamily (f i) a b h r0 Z Δ) (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 (vectorSum f a h r0) z‖ ≤ C * PhysicalWaveSum.physicalQ h z ^ (h * α - PhysicalClassBounds.physicalLoss h σ m)