Raw physical stage estimates from native wave and mean data

The data below describe the actual copy families and coherent native mean fields. Physical derivative estimates are consequences of their native classes, support and chart identities. No RawStageBounds is an input.

theorem NavierStokes.PhysicalStageBounds.abs_time_le_one {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ h w ≤ 1) : |w.1| ≤ 1

Small physical q automatically restricts time to the interval on which the existing physical-copy estimates are uniform.

structure NavierStokes.PhysicalStageBounds.WaveData (h : ℝ) (D : Type) [NormedAddCommGroup D] [NormedSpace ℝ D] (I : Type u_1) (K : Type u_2) (J : Type u_3) : Type (max (max u_1 u_2) u_3)

A native source and its actual physical copy representation. All regularity is confined to the valid native patches. The number of harmonics and the cover gap may vary between stages.

• lowerRadius : ℝ

  Lower radius of WaveData, of type ℝ.

• upperRadius : ℝ

  Upper radius of WaveData, of type ℝ.

• nativeWidth : ℝ

  Native width of WaveData, of type ℝ.

• slowBound : ℝ

  Slow bound of WaveData, of type ℝ.

• frequencyBound : ℝ

  Frequency bound of WaveData, of type ℝ.

• alpha : ℝ

  Alpha of WaveData, of type ℝ.

• shift : ℝ

  Shift of WaveData, of type ℝ.

• harmonics : ℕ

  Harmonics of WaveData, of type ℕ.

• gapBound : ℕ

  Gap bound of WaveData, of type ℕ.

• lower_pos : 0 < self.lowerRadius
• width_nonneg : 0 ≤ self.nativeWidth
• slow_nonneg : 0 ≤ self.slowBound
• frequency_one_le : 1 ≤ self.frequencyBound
• strip : WeightedClasses.StripData D

  Strip of WaveData, of type WeightedClasses.StripData D.

• weight : I → ℕ → D → ℝ

  Weight of WaveData, of type I → ℕ → D → ℝ.

• source : I → ℕ → D → ℂ

  Source of WaveData, of type I → ℕ → D → ℂ.

• source_bounds : LocalPhysicalCopyBounds.LocalSourceBounds self.strip h self.alpha self.weight self.source
• copies : J → PhysicalCopyBounds.CopyFamily self.harmonics K

  Copies of WaveData, of type J → PhysicalCopyBounds.CopyFamily harmonics K.

• cells (i : J) : PhysicalCopyBounds.SupportCells (self.copies i)

  Cells of WaveData, of type ∀ i, PhysicalCopyBounds.SupportCells (copies i).

• chart (i : J) : LocalPhysicalCopyBounds.CommonChart (self.copies i) (self.cells i) self.lowerRadius self.upperRadius h self.nativeWidth self.shift self.source

  Chart supplied by WaveData.

• chart_maps (i : J) (k : K) (L : PhysicalWaveSum.WaveIndex self.harmonics) : Set.MapsTo ((self.chart i).map k L) ((self.chart i).domain k L) self.strip.domain
• carrier (i : J) : PhysicalCopyBounds.CarrierBounds (self.copies i) (self.cells i) self.lowerRadius self.upperRadius h self.nativeWidth

  Carrier supplied by WaveData.

• support (i : J) : LocalPhysicalCopyBounds.SupportData (self.copies i) self.lowerRadius self.upperRadius h self.nativeWidth self.slowBound self.gapBound
• smooth (i : J) : LocalPhysicalCopyBounds.SmoothData (self.copies i) self.lowerRadius h self.nativeWidth
• frequencies (i : J) (k : K) (L : PhysicalWaveSum.BandLabel) : |((self.copies i).carrier k L).angular| ≤ self.frequencyBound ∧ |((self.copies i).carrier k L).axial| ≤ self.frequencyBound ∧ |((self.copies i).carrier k L).radial| ≤ self.frequencyBound

noncomputable def NavierStokes.PhysicalStageBounds.WaveData.scalar {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} {J : Type u_3} (W : WaveData h D I K J) (i : J) : ProblemStatement.SpaceTime → ℂ

Scalar, given by (W.copies i).sum W.lowerRadius h W.nativeWidth.

Equations

• W.scalar i = (W.copies i).sum W.lowerRadius h W.nativeWidth

theorem NavierStokes.PhysicalStageBounds.WaveData.scalar_smooth {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} {J : Type u_3} (W : WaveData h D I K J) (hh : 0 < h) (hh1 : h < 1 / 2) (i : J) : ContDiffOn ℝ (↑⊤) (W.scalar i) PhysicalWaveSum.preterminal

theorem NavierStokes.PhysicalStageBounds.WaveData.scalar_bound {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} {J : Type u_3} (W : WaveData h D I K J) (hh : 0 < h) (hh1 : h < 1 / 2) (i : J) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m (W.scalar i) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (h * W.alpha - PhysicalClassBounds.physicalLoss h W.shift m)

The physical exponent and loss are obtained from the native weighted source and actual chart map, not from a physical-bound hypothesis.

noncomputable def NavierStokes.PhysicalStageBounds.WaveData.vector {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : WaveData h D I K (Fin 3)) : ProblemStatement.VelocityField

Vector, given by PhysicalCopyBounds.vectorSum W.copies W.lowerRadius h W.nativeWidth.

Equations

• W.vector = NavierStokes.PhysicalCopyBounds.vectorSum W.copies W.lowerRadius h W.nativeWidth

theorem NavierStokes.PhysicalStageBounds.WaveData.vector_smooth {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : WaveData h D I K (Fin 3)) (hh : 0 < h) (hh1 : h < 1 / 2) : ContDiffOn ℝ (↑⊤) W.vector PhysicalWaveSum.preterminal

theorem NavierStokes.PhysicalStageBounds.WaveData.vector_bound {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : WaveData h D I K (Fin 3)) (hh : 0 < h) (hh1 : h < 1 / 2) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m W.vector w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (h * W.alpha - PhysicalClassBounds.physicalLoss h W.shift m)

noncomputable def NavierStokes.PhysicalStageBounds.WaveData.pressure {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : WaveData h D I K Unit) : ProblemStatement.PressureField

Pressure, defined pointwise by (W.scalar () w).re.

Equations

• W.pressure w = (W.scalar () w).re

theorem NavierStokes.PhysicalStageBounds.WaveData.pressure_smooth {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : WaveData h D I K Unit) (hh : 0 < h) (hh1 : h < 1 / 2) : ContDiffOn ℝ (↑⊤) W.pressure PhysicalWaveSum.preterminal

theorem NavierStokes.PhysicalStageBounds.WaveData.pressure_bound {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : WaveData h D I K Unit) (hh : 0 < h) (hh1 : h < 1 / 2) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m W.pressure w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (h * W.alpha - PhysicalClassBounds.physicalLoss h W.shift m)

structure NavierStokes.PhysicalStageBounds.MeanData (h degree : ℝ) : Type

Actual coherent mean fields with native local-band classes. The construction keeps a single physical field represented by all valid bands.

• firstBand : ℕ

  First band of MeanData, of type ℕ.

• gapBound : ℕ

  Gap bound of MeanData, of type ℕ.

• region : Set PhysicalGraphBounds.Plane

  Region of MeanData, of type Set PhysicalGraphBounds.Plane.

• lowerRadius : ℝ

  Lower radius of MeanData, of type ℝ.

• upperRadius : ℝ

  Upper radius of MeanData, of type ℝ.

• alpha : ℝ

  Alpha of MeanData, of type ℝ.

• slow : ℕ → ℝ

  Slow of MeanData, of type ℕ → ℝ.

• family : PhysicalMeanJetBounds.CoherentFamily h degree self.firstBand self.gapBound self.region ℝ

  Family of MeanData, of type PhysicalMeanJetBounds.CoherentFamily h degree firstBand gapBound region ℝ.

• band_four : 4 ≤ self.firstBand
• lower_pos : 0 < self.lowerRadius
• radii_lt : self.lowerRadius < self.upperRadius
• region_open : IsOpen self.region
• region_covers : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 4) 4 ⊆ self.region
• smooth (n : ℕ) : n ≥ self.firstBand → ContDiffOn ℝ (↑⊤) (self.family.native n) (PhysicalMeanDomain.slowDomain self.region)
• support : PhysicalMeanJetBounds.NativeSupport h self.lowerRadius self.upperRadius self.firstBand self.region self.family.native
• slow_nonneg (n : ℕ) : n ≥ self.firstBand → 0 ≤ self.slow n
• slow_growth : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ n ≥ self.firstBand, self.slow n ≤ C * ChartScales.S n ^ p
• native_class : PhysicalMeanDomain.LocalBandJets self.region (ChartScales.epsilon h) self.slow self.alpha self.family.native

theorem NavierStokes.PhysicalStageBounds.MeanData.nativeJets {h degree : ℝ} (M : MeanData h degree) : PhysicalMeanJetBounds.NativeJets M.firstBand M.region (h * M.alpha) M.family.native

theorem NavierStokes.PhysicalStageBounds.MeanData.field_smooth {h degree qbig : ℝ} (M : MeanData h degree) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) : ContDiffOn ℝ (↑⊤) M.family.field (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.PhysicalStageBounds.MeanData.angular_smooth {h degree qbig : ℝ} (M : MeanData h degree) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) : ContDiffOn ℝ (↑⊤) M.family.angularField (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.PhysicalStageBounds.MeanData.field_bound {h degree qbig : ℝ} (M : MeanData h degree) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m M.family.field w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (h * M.alpha - PhysicalMeanJetBounds.loss degree m)

theorem NavierStokes.PhysicalStageBounds.MeanData.angular_bound {h degree qbig : ℝ} (M : MeanData h degree) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m M.family.angularField w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (h * M.alpha - PhysicalMeanJetBounds.loss degree m)

theorem NavierStokes.PhysicalStageBounds.WaveData.vector_bound_with_gain {h g delta : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : WaveData h D I K (Fin 3)) (hh : 0 < h) (hh1 : h < 1 / 2) (hg : g ≤ h * W.alpha + W.shift + delta) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m W.vector w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (g - (PhysicalGraphBounds.waveLoss h m + delta))

theorem NavierStokes.PhysicalStageBounds.WaveData.pressure_bound_with_gain {h g delta : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : WaveData h D I K Unit) (hh : 0 < h) (hh1 : h < 1 / 2) (hg : g ≤ h * W.alpha + W.shift + delta) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m W.pressure w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (g - (PhysicalGraphBounds.waveLoss h m + delta))

theorem NavierStokes.PhysicalStageBounds.MeanData.field_bound_with_gain {h g delta degree qbig : ℝ} (M : MeanData h degree) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) (hg : g ≤ h * M.alpha + delta) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m M.family.field w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (g - (PhysicalMeanJetBounds.loss degree m + delta))

theorem NavierStokes.PhysicalStageBounds.MeanData.angular_bound_with_gain {h g delta degree qbig : ℝ} (M : MeanData h degree) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) (hg : g ≤ h * M.alpha + delta) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m M.family.angularField w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (g - (PhysicalMeanJetBounds.loss degree m + delta))

noncomputable def NavierStokes.PhysicalStageBounds.potentialIncrement {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : WaveData h D I K (Fin 3)) (M : MeanData h (CoordinateAlgebra.A h - 1 / 2)) : ProblemStatement.VelocityField

Potential increment, defined pointwise by W.vector w + M.family.angularField w.

Equations

• NavierStokes.PhysicalStageBounds.potentialIncrement W M w = W.vector w + M.family.angularField w

noncomputable def NavierStokes.PhysicalStageBounds.pressureIncrement {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (W : WaveData h D I K Unit) (M : MeanData h (2 * CoordinateAlgebra.A h)) : ProblemStatement.PressureField

Pressure increment, defined pointwise by W.pressure w + M.family.field w.

Equations

• NavierStokes.PhysicalStageBounds.pressureIncrement W M w = W.pressure w + M.family.field w

noncomputable def NavierStokes.PhysicalStageBounds.potentialLoss (h waveOffset meanOffset : ℝ) (m : ℕ) : ℝ

These losses depend only on fixed physical parameters and jet order. The five offsets are fixed once for the whole stage sequence.

Equations

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

noncomputable def NavierStokes.PhysicalStageBounds.directLoss (h meanOffset : ℝ) (m : ℕ) : ℝ

Direct loss, given by PhysicalMeanJetBounds.loss (CoordinateAlgebra.A h) m + meanOffset.

Equations

• NavierStokes.PhysicalStageBounds.directLoss h meanOffset m = NavierStokes.PhysicalMeanJetBounds.loss (NavierStokes.CoordinateAlgebra.A h) m + meanOffset

noncomputable def NavierStokes.PhysicalStageBounds.pressureLoss (h waveOffset meanOffset : ℝ) (m : ℕ) : ℝ

Pressure loss, given by max (PhysicalGraphBounds.waveLoss h m + waveOffset) (PhysicalMeanJetBounds.loss (2 * CoordinateAlgebra.A h) m + meanOffset).

Equations

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

theorem NavierStokes.PhysicalStageBounds.potentialIncrement_smooth {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} {qbig : ℝ} (W : WaveData h D I K (Fin 3)) (M : MeanData h (CoordinateAlgebra.A h - 1 / 2)) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) : ContDiffOn ℝ (↑⊤) (potentialIncrement W M) (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.PhysicalStageBounds.pressureIncrement_smooth {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} {qbig : ℝ} (W : WaveData h D I K Unit) (M : MeanData h (2 * CoordinateAlgebra.A h)) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) : ContDiffOn ℝ (↑⊤) (pressureIncrement W M) (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.PhysicalStageBounds.potentialIncrement_bound {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} {qbig g waveOffset meanOffset : ℝ} (W : WaveData h D I K (Fin 3)) (M : MeanData h (CoordinateAlgebra.A h - 1 / 2)) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) (hwave : g ≤ h * W.alpha + W.shift + waveOffset) (hmean : g ≤ h * M.alpha + meanOffset) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m (potentialIncrement W M) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (g - potentialLoss h waveOffset meanOffset m)

theorem NavierStokes.PhysicalStageBounds.pressureIncrement_bound {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} {qbig g waveOffset meanOffset : ℝ} (W : WaveData h D I K Unit) (M : MeanData h (2 * CoordinateAlgebra.A h)) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : qbig ≤ ChartScales.Q M.firstBand) (hwave : g ≤ h * W.alpha + W.shift + waveOffset) (hmean : g ≤ h * M.alpha + meanOffset) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ CutStageEstimates.physicalSublevel h qbig, PhysicalWaveSum.physicalQ h w ≤ 1 → ‖iteratedFDeriv ℝ m (pressureIncrement W M) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (g - pressureLoss h waveOffset meanOffset m)

noncomputable def NavierStokes.PhysicalStageBounds.addBaseAtZero {X : Type u_1} {V : Type u_2} [Add V] (base : X → V) (increments : ℕ → X → V) (j : ℕ) (x : X) : V

The zeroth increment is the base plus finite initialization. Positive indices keep the supplied correction increments exactly.

Equations

• NavierStokes.PhysicalStageBounds.addBaseAtZero base increments j x = if j = 0 then base x + increments 0 x else increments j x

@[simp]

theorem NavierStokes.PhysicalStageBounds.addBaseAtZero_zero {X : Type u_1} {V : Type u_2} [Add V] (base : X → V) (increments : ℕ → X → V) : addBaseAtZero base increments 0 = fun (x : X) => base x + increments 0 x

theorem NavierStokes.PhysicalStageBounds.addBaseAtZero_pos {X : Type u_1} {V : Type u_2} [Add V] (base : X → V) (increments : ℕ → X → V) {j : ℕ} (hj : 1 ≤ j) : addBaseAtZero base increments j = increments j

noncomputable def NavierStokes.PhysicalStageBounds.potentialStages {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (base : ProblemStatement.VelocityField) (W : ℕ → WaveData h D I K (Fin 3)) (M : ℕ → MeanData h (CoordinateAlgebra.A h - 1 / 2)) : ℕ → ProblemStatement.VelocityField

Potential stages, given by addBaseAtZero base (fun j => potentialIncrement (W j) (M j)).

Equations

• NavierStokes.PhysicalStageBounds.potentialStages base W M = NavierStokes.PhysicalStageBounds.addBaseAtZero base fun (j : ℕ) => NavierStokes.PhysicalStageBounds.potentialIncrement (W j) (M j)

noncomputable def NavierStokes.PhysicalStageBounds.directStages {h : ℝ} (M : ℕ → MeanData h (CoordinateAlgebra.A h)) : ℕ → ProblemStatement.VelocityField

Direct stages, defined pointwise by (M j).family.angularField.

Equations

• NavierStokes.PhysicalStageBounds.directStages M j = (M j).family.angularField

noncomputable def NavierStokes.PhysicalStageBounds.pressureStages {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (base : ProblemStatement.PressureField) (W : ℕ → WaveData h D I K Unit) (M : ℕ → MeanData h (2 * CoordinateAlgebra.A h)) : ℕ → ProblemStatement.PressureField

Pressure stages, given by addBaseAtZero base (fun j => pressureIncrement (W j) (M j)).

Equations

• NavierStokes.PhysicalStageBounds.pressureStages base W M = NavierStokes.PhysicalStageBounds.addBaseAtZero base fun (j : ℕ) => NavierStokes.PhysicalStageBounds.pressureIncrement (W j) (M j)

theorem NavierStokes.PhysicalStageBounds.potentialStages_zero {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (base : ProblemStatement.VelocityField) (W : ℕ → WaveData h D I K (Fin 3)) (M : ℕ → MeanData h (CoordinateAlgebra.A h - 1 / 2)) : potentialStages base W M 0 = fun (w : ProblemStatement.SpaceTime) => base w + ((W 0).vector w + (M 0).family.angularField w)

theorem NavierStokes.PhysicalStageBounds.pressureStages_zero {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (base : ProblemStatement.PressureField) (W : ℕ → WaveData h D I K Unit) (M : ℕ → MeanData h (2 * CoordinateAlgebra.A h)) : pressureStages base W M 0 = fun (w : ProblemStatement.SpaceTime) => base w + ((W 0).pressure w + (M 0).family.field w)

theorem NavierStokes.PhysicalStageBounds.potentialStages_smooth {h qbig : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (base : ProblemStatement.VelocityField) (W : ℕ → WaveData h D I K (Fin 3)) (M : ℕ → MeanData h (CoordinateAlgebra.A h - 1 / 2)) (hh : 0 < h) (hh1 : h < 1 / 2) (hbase : ContDiffOn ℝ (↑⊤) base (CutStageEstimates.physicalSublevel h qbig)) (hq : ∀ (j : ℕ), qbig ≤ ChartScales.Q (M j).firstBand) (j : ℕ) : ContDiffOn ℝ (↑⊤) (potentialStages base W M j) (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.PhysicalStageBounds.pressureStages_smooth {h qbig : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (base : ProblemStatement.PressureField) (W : ℕ → WaveData h D I K Unit) (M : ℕ → MeanData h (2 * CoordinateAlgebra.A h)) (hh : 0 < h) (hh1 : h < 1 / 2) (hbase : ContDiffOn ℝ (↑⊤) base (CutStageEstimates.physicalSublevel h qbig)) (hq : ∀ (j : ℕ), qbig ≤ ChartScales.Q (M j).firstBand) (j : ℕ) : ContDiffOn ℝ (↑⊤) (pressureStages base W M j) (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.PhysicalStageBounds.directStages_smooth {h qbig : ℝ} (M : ℕ → MeanData h (CoordinateAlgebra.A h)) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : ∀ (j : ℕ), qbig ≤ ChartScales.Q (M j).firstBand) (j : ℕ) : ContDiffOn ℝ (↑⊤) (directStages M j) (CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.PhysicalStageBounds.potentialStages_raw {h qbig : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (base : ProblemStatement.VelocityField) (W : ℕ → WaveData h D I K (Fin 3)) (M : ℕ → MeanData h (CoordinateAlgebra.A h - 1 / 2)) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : ∀ (j : ℕ), qbig ≤ ChartScales.Q (M j).firstBand) (g : ℕ → ℝ) (waveOffset meanOffset : ℝ) (hwave : ∀ (j : ℕ), 1 ≤ j → g j ≤ h * (W j).alpha + (W j).shift + waveOffset) (hmean : ∀ (j : ℕ), 1 ≤ j → g j ≤ h * (M j).alpha + meanOffset) : ∃ (C : ℕ → ℕ → ℝ), (∀ (j m : ℕ), 0 ≤ C j m) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) (potentialStages base W M) g (potentialLoss h waveOffset meanOffset) C (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig)

All potential-stage raw estimates are derived from the actual wave copies and azimuthal stream representations.

theorem NavierStokes.PhysicalStageBounds.pressureStages_raw {h qbig : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} (base : ProblemStatement.PressureField) (W : ℕ → WaveData h D I K Unit) (M : ℕ → MeanData h (2 * CoordinateAlgebra.A h)) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : ∀ (j : ℕ), qbig ≤ ChartScales.Q (M j).firstBand) (g : ℕ → ℝ) (waveOffset meanOffset : ℝ) (hwave : ∀ (j : ℕ), 1 ≤ j → g j ≤ h * (W j).alpha + (W j).shift + waveOffset) (hmean : ∀ (j : ℕ), 1 ≤ j → g j ≤ h * (M j).alpha + meanOffset) : ∃ (C : ℕ → ℕ → ℝ), (∀ (j m : ℕ), 0 ≤ C j m) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) (pressureStages base W M) g (pressureLoss h waveOffset meanOffset) C (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.PhysicalStageBounds.directStages_raw {h qbig : ℝ} (M : ℕ → MeanData h (CoordinateAlgebra.A h)) (hh : 0 < h) (hh1 : h < 1 / 2) (hq : ∀ (j : ℕ), qbig ≤ ChartScales.Q (M j).firstBand) (g : ℕ → ℝ) (meanOffset : ℝ) (hmean : ∀ (j : ℕ), 1 ≤ j → g j ≤ h * (M j).alpha + meanOffset) : ∃ (C : ℕ → ℕ → ℝ), (∀ (j m : ℕ), 0 ≤ C j m) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) (directStages M) g (directLoss h meanOffset) C (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig)

theorem NavierStokes.PhysicalStageBounds.derived_stage_inputs {h qbig : ℝ} {DA DP : Type} [NormedAddCommGroup DA] [NormedSpace ℝ DA] [NormedAddCommGroup DP] [NormedSpace ℝ DP] {IA : Type u_1} {KA : Type u_2} {IP : Type u_3} {KP : Type u_4} (baseA : ProblemStatement.VelocityField) (baseP : ProblemStatement.PressureField) (WA : ℕ → WaveData h DA IA KA (Fin 3)) (MA : ℕ → MeanData h (CoordinateAlgebra.A h - 1 / 2)) (MB : ℕ → MeanData h (CoordinateAlgebra.A h)) (WP : ℕ → WaveData h DP IP KP Unit) (MP : ℕ → MeanData h (2 * CoordinateAlgebra.A h)) (hh : 0 < h) (hh1 : h < 1 / 2) (hbaseA : ContDiffOn ℝ (↑⊤) baseA (CutStageEstimates.physicalSublevel h qbig)) (hbaseP : ContDiffOn ℝ (↑⊤) baseP (CutStageEstimates.physicalSublevel h qbig)) (hqA : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MA j).firstBand) (hqB : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MB j).firstBand) (hqP : ∀ (j : ℕ), qbig ≤ ChartScales.Q (MP j).firstBand) (g : ℕ → ℝ) (deltaWA deltaMA deltaB deltaWP deltaMP : ℝ) (hWA : ∀ (j : ℕ), 1 ≤ j → g j ≤ h * (WA j).alpha + (WA j).shift + deltaWA) (hMA : ∀ (j : ℕ), 1 ≤ j → g j ≤ h * (MA j).alpha + deltaMA) (hMB : ∀ (j : ℕ), 1 ≤ j → g j ≤ h * (MB j).alpha + deltaB) (hWP : ∀ (j : ℕ), 1 ≤ j → g j ≤ h * (WP j).alpha + (WP j).shift + deltaWP) (hMP : ∀ (j : ℕ), 1 ≤ j → g j ≤ h * (MP j).alpha + deltaMP) : ∃ (CA : ℕ → ℕ → ℝ) (CB : ℕ → ℕ → ℝ) (CP : ℕ → ℕ → ℝ), (∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (potentialStages baseA WA MA j) (CutStageEstimates.physicalSublevel h qbig)) ∧ (∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (directStages MB j) (CutStageEstimates.physicalSublevel h qbig)) ∧ (∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (pressureStages baseP WP MP j) (CutStageEstimates.physicalSublevel h qbig)) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) (potentialStages baseA WA MA) g (potentialLoss h deltaWA deltaMA) CA (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) (directStages MB) g (directLoss h deltaB) CB (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig) ∧ CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) (pressureStages baseP WP MP) g (pressureLoss h deltaWP deltaMP) CP (fun (x x_1 : ℕ) => 0) (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig)

The six raw-stage inputs needed by the mixed diagonal construction, derived together for one gain sequence. The losses contain only the fixed five offsets and the derivative order. Initialization remains in stage zero. No finite-residual estimate or choice of the gain sequence is hidden here.

theorem NavierStokes.PhysicalStageBounds.jets_eq_of_eqOn_open {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {f g : E → V} {U : Set E} (hU : IsOpen U) (he : Set.EqOn f g U) {x : E} (hx : x ∈ U) (m : ℕ) : iteratedFDeriv ℝ m f x = iteratedFDeriv ℝ m g x

Actual field equality on the valid open physical domain identifies all ambient derivatives. No regularity of either totalization outside the domain is required.

theorem NavierStokes.PhysicalStageBounds.rawStageBounds_congr_on {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {F G : ℕ → E → V} {U S : Set E} {q : E → ℝ} {g L : ℕ → ℝ} {C p : ℕ → ℕ → ℝ} (hU : IsOpen U) (hSU : S ⊆ U) (he : ∀ (j : ℕ), Set.EqOn (F j) (G j) U) (hb : CutStageEstimates.RawStageBounds q G g L C p S) : CutStageEstimates.RawStageBounds q F g L C p S

Transfer the proved raw estimates to a separately defined family by its literal representation on the valid physical neighborhood.

theorem NavierStokes.PhysicalStageBounds.stage_smooth_congr_on {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {F G : ℕ → E → V} {U : Set E} (he : ∀ (j : ℕ), Set.EqOn (F j) (G j) U) (hs : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (G j) U) (j : ℕ) : ContDiffOn ℝ (↑⊤) (F j) U

theorem NavierStokes.PhysicalStageBounds.actual_potential_base_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (upper : ℝ) (bandFloor : ℕ) (qbig : ℝ) : ContDiffOn ℝ (↑⊤) (TailGaugePotential.finalPotential H v upper bandFloor) (CutStageEstimates.physicalSublevel F.data.h qbig)

theorem NavierStokes.PhysicalStageBounds.actual_pressure_base_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (upper : ℝ) (bandFloor : ℕ) (qbig : ℝ) : ContDiffOn ℝ (↑⊤) (FinalSlowBase.pressure H v upper bandFloor) (CutStageEstimates.physicalSublevel F.data.h qbig)