Actual polar graph coverage of the nominal active annulus

The geometric hypotheses are the nominal closed active annulus and the strict dyadic choice q ≤ Q n < 2 * q. Chart coverage is a conclusion. The native open domain allows every positive radius and retains the actual slow region; the smaller weighted strip is reached through its closure at radial endpoints.

Physical jets of the actual finite-state residual

The estimates are on genuine Fréchet derivatives. Harmonic coefficients, mean residuals and excluded errors are combined before the physical graph restriction. Phase regularity is needed only on coefficient support.

@[reducible, inline]

abbrev NavierStokes.PhysicalResidualJetBounds.Point : Type

Point: an abbreviation for PhysicalMeanJetBounds.Point.

Equations

• NavierStokes.PhysicalResidualJetBounds.Point = NavierStokes.PhysicalMeanJetBounds.Point

@[reducible, inline]

abbrev NavierStokes.PhysicalResidualJetBounds.Cylinder : Type

Cylinder: an abbreviation for Point × ℝ.

Equations

• NavierStokes.PhysicalResidualJetBounds.Cylinder = (NavierStokes.PhysicalResidualJetBounds.Point × ℝ)

@[reducible, inline]

abbrev NavierStokes.PhysicalResidualJetBounds.Components : Type

Components: an abbreviation for Fin 3 → ℝ.

Equations

• NavierStokes.PhysicalResidualJetBounds.Components = (Fin 3 → ℝ)

Local harmonic calculus

theorem NavierStokes.PhysicalResidualJetBounds.character_positive_jet_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {Φ : E → ℝ} {x : E} (hΦ : LocalPhysicalCopyBounds.SmoothNear Φ x) (m : ℕ) {c B M : ℝ} (hB : 1 ≤ B) (hM : 1 ≤ M) (hc : |c| ≤ M) (hΦb : ∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDeriv ℝ i Φ x‖ ≤ B) (k : ℕ) : k ≤ m → ‖iteratedFDeriv ℝ k (PhysicalGraphBounds.character c ∘ Φ) x‖ ≤ ↑m.factorial * M ^ m * B ^ m

A constant shift of the phase costs nothing: only positive phase jets are needed, even when the phase value itself is unbounded.

theorem NavierStokes.PhysicalResidualJetBounds.product_jet_bound_local {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {a b : E → ℂ} {x : E} (ha : LocalPhysicalCopyBounds.SmoothNear a x) (hb : LocalPhysicalCopyBounds.SmoothNear b x) {m k : ℕ} (hk : k ≤ m) {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (haB : ∀ i ≤ m, ‖iteratedFDeriv ℝ i a x‖ ≤ A) (hbB : ∀ i ≤ m, ‖iteratedFDeriv ℝ i b x‖ ≤ B) : ‖iteratedFDeriv ℝ k (fun (y : E) => a y * b y) x‖ ≤ 2 ^ m * A * B

theorem NavierStokes.PhysicalResidualJetBounds.mode_jet_bound_local {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {a : E → ℂ} {Φ : E → ℝ} {x : E} (ha : LocalPhysicalCopyBounds.SmoothNear a x) (hΦ : LocalPhysicalCopyBounds.SmoothNear Φ x) (m : ℕ) {c A B M : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hM : 1 ≤ M) (hc : |c| ≤ M) (haB : ∀ i ≤ m, ‖iteratedFDeriv ℝ i a x‖ ≤ A) (hΦb : ∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDeriv ℝ i Φ x‖ ≤ B) (k : ℕ) : k ≤ m → ‖iteratedFDeriv ℝ k (fun (y : E) => a y * PhysicalGraphBounds.character c (Φ y)) x‖ ≤ 2 ^ m * A * (↑m.factorial * M ^ m * B ^ m)

Actual residual reconstruction and Cartesian scaling

noncomputable def NavierStokes.PhysicalResidualJetBounds.vectorMap : Components →L[ℝ] ProblemStatement.Space

Vector map as an element of Components →L[ℝ] Space.

Equations

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

@[simp]

theorem NavierStokes.PhysicalResidualJetBounds.vectorMap_apply (v : Components) (i : Fin 3) : (vectorMap v).ofLp i = v i

noncomputable def NavierStokes.PhysicalResidualJetBounds.residualDegree (h : ℝ) : ℝ

Residual degree, given by 2 * CoordinateAlgebra.A h + 1 / 2.

Equations

• NavierStokes.PhysicalResidualJetBounds.residualDegree h = 2 * NavierStokes.CoordinateAlgebra.A h + 1 / 2

theorem NavierStokes.PhysicalResidualJetBounds.physical_vector_of_components {Q : ℝ} (hQ : 0 < Q) (h θ : ℝ) (a : Components) (R : ProblemStatement.Space) (ha : ∀ (i : Fin 3), a i = Q ^ residualDegree h * ((CylindricalResidual.frame (-θ)) R).ofLp i) : R = Q ^ (-residualDegree h) • (CylindricalResidual.frame θ) (vectorMap a)

Invert the actual residual scaling and cylindrical frame.

theorem NavierStokes.PhysicalResidualJetBounds.state_fullResidual_reconstructed {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} {U : Set D} (hU : IsOpen U) {c : CorrectionState.Context D} {s : CorrectionState.State D} {labels : ℕ → Finset ι} {b : ι → CorrectionState.HarmonicBlock D} {G A : ι → HarmonicResidual.BlockCoefficients D} (hrep : HarmonicResidual.BlockRepresentation labels b G A s) (hmean : LiftedMeanResidual.MeanHypotheses U c s) {n : ℕ} (hreg : HarmonicResidual.ExtractionRegular U c s labels b G A n) {x : D × ℝ} (hx : x ∈ HarmonicResidual.liftDomain U) (i : Fin 3) : LiftedMeanResidual.fullResidual c s n x i = ∑ l ∈ labels n, (HarmonicResidual.residualBlock c s (b l) (G l) (A l)).oscillation n x i + s.meanGoodResidual c n x.1 i + s.errors.total n x i

The actual polar common graph and rotating Cartesian basis

noncomputable def NavierStokes.PhysicalResidualJetBounds.polarAssoc : PhysicalGraphBounds.Plane × (ℝ × ℝ) × PhysicalGraphBounds.Plane ≃ₗᵢ[ℝ] Cylinder

Polar assoc, bundling toFun, invFun, left_inv, right_inv and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.PhysicalResidualJetBounds.polarLift (a : ℝ) (j : PolarCharts.Index) (x : PhysicalWaveSum.LiftPoint) : Cylinder

Polar lift, given by polarAssoc (PolarCharts.chart a j (PhysicalGraphBounds.liftXY x), PhysicalClassBounds.slowFast x).

Equations

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

noncomputable def NavierStokes.PhysicalResidualJetBounds.polarGraph (a h : ℝ) (j : PolarCharts.Index) (n d : ℕ) : ProblemStatement.SpaceTime → Cylinder

Polar graph, given by polarLift a j ∘ commonLift h n d.

Equations

• NavierStokes.PhysicalResidualJetBounds.polarGraph a h j n d = NavierStokes.PhysicalResidualJetBounds.polarLift a j ∘ NavierStokes.PhysicalWaveSum.commonLift h n d

theorem NavierStokes.PhysicalResidualJetBounds.polarLift_smooth {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) : ContDiff ℝ (↑⊤) (polarLift a j)

theorem NavierStokes.PhysicalResidualJetBounds.polarLift_positiveJets {a b : ℝ} (ha : 0 < a) (m : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ (j : PolarCharts.Index) (x : PhysicalWaveSum.LiftPoint), PhysicalGraphBounds.liftXY x ∈ Metric.closedBall 0 b → ∀ (k : ℕ), 1 ≤ k → k ≤ m → ‖iteratedFDeriv ℝ k (polarLift a j) x‖ ≤ B

noncomputable def NavierStokes.PhysicalResidualJetBounds.rotationBase (a : ℝ) (j : PolarCharts.Index) (x : PhysicalGraphBounds.Plane) : Components →L[ℝ] ProblemStatement.Space

Rotation base, given by (CylindricalResidual.frame (PolarCharts.chart a j x).2).comp vectorMap.

Equations

• NavierStokes.PhysicalResidualJetBounds.rotationBase a j x = NavierStokes.CylindricalResidual.frame (NavierStokes.PolarCharts.chart a j x).2 ∘SL NavierStokes.PhysicalResidualJetBounds.vectorMap

theorem NavierStokes.PhysicalResidualJetBounds.rotationBase_smooth {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) : ContDiff ℝ (↑⊤) (rotationBase a j)

theorem NavierStokes.PhysicalResidualJetBounds.finite_compact_jet_bound {ι : Type u_1} {E : Type u_2} {F : Type u_3} [Finite ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ι → E → F} {U K : Set E} (hU : IsOpen U) (hf : ∀ (i : ι), ContDiffOn ℝ (↑⊤) (f i) U) (hK : IsCompact K) (hKU : K ⊆ U) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (i : ι), ∀ k ≤ m, ∀ x ∈ K, ‖iteratedFDeriv ℝ k (f i) x‖ ≤ C

theorem NavierStokes.PhysicalResidualJetBounds.rotationLift_jet_bound {a : ℝ} (ha : 0 < a) (b : ℝ) (m : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ (j : PolarCharts.Index) (x : PhysicalWaveSum.LiftPoint), PhysicalGraphBounds.liftXY x ∈ Metric.closedBall 0 b → ∀ k ≤ m, ‖iteratedFDeriv ℝ k (rotationBase a j ∘ ⇑PhysicalGraphBounds.liftXY) x‖ ≤ B

theorem NavierStokes.PhysicalResidualJetBounds.clm_apply_jet_bound {D : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : D → E →L[ℝ] F} {g : D → E} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (x : D) {m k : ℕ} (hk : k ≤ m) {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hfa : ∀ i ≤ m, ‖iteratedFDeriv ℝ i f x‖ ≤ A) (hgb : ∀ i ≤ m, ‖iteratedFDeriv ℝ i g x‖ ≤ B) : ‖iteratedFDeriv ℝ k (fun (y : D) => (f y) (g y)) x‖ ≤ 2 ^ m * A * B

noncomputable def NavierStokes.PhysicalResidualJetBounds.cartesianPull (a h : ℝ) (j : PolarCharts.Index) (n d : ℕ) (degree : ℝ) (F : Cylinder → Components) : ProblemStatement.SpaceTime → ProblemStatement.Space

The Cartesian reconstruction keeps the exact residual degree and the actual rotating basis, before any derivative estimate is applied.

Equations

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

theorem NavierStokes.PhysicalResidualJetBounds.cartesianPull_jet_bound {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (Δ m : ℕ) (gain degree e A : ℝ) (hA : 0 ≤ A) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ d ≤ Δ, ∀ (w : ProblemStatement.SpaceTime), (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b → |w.1| ≤ 1 → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ∀ (j : PolarCharts.Index) (F : Cylinder → Components), LocalPhysicalCopyBounds.SmoothNear F (polarGraph a h j n d w) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i F (polarGraph a h j n d w)‖ ≤ A * ChartScales.Q n ^ gain * ChartScales.S n ^ e) → ‖iteratedFDeriv ℝ m (cartesianPull a h j n d degree F) w‖ ≤ C * q ^ (gain - PhysicalMeanJetBounds.loss degree m)

The actual angular graph and Cartesian basis add only an order-dependent constant. The displayed loss retains the exact physical scaling degree.

Uniform native jets and support-local harmonic synthesis

theorem NavierStokes.PhysicalResidualJetBounds.finite_pi_iteratedFDeriv_norm_le {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] {f : E → ι → ℝ} {x : E} {m : ℕ} {C : ℝ} (hf : ContDiffAt ℝ (↑m) f x) (hC : 0 ≤ C) (hb : ∀ (i : ι), ‖iteratedFDeriv ℝ m (fun (y : E) => f y i) x‖ ≤ C) : ‖iteratedFDeriv ℝ m f x‖ ≤ C

structure NavierStokes.PhysicalResidualJetBounds.NativeBounds {D : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (N : ℕ) (U : Set D) (gain : ℝ) (loss : ℕ → ℝ) (f : ι → ℕ → D → E) : Prop

Constants are chosen before the label and band. loss is allowed to depend on the derivative order; it never depends on the correction stage.

• smooth (l : ι) (n : ℕ) : N ≤ n → ContDiffOn ℝ (↑⊤) (f l n) U
• bounds (m : ℕ) : ∃ (A : ℝ), 0 ≤ A ∧ ∃ (p : ℕ), ∀ (l : ι) (n : ℕ), N ≤ n → ∀ x ∈ U, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (f l n) x‖ ≤ A * ChartScales.Q n ^ (gain - loss m) * ChartScales.S n ^ p

theorem NavierStokes.PhysicalResidualJetBounds.NativeBounds.zero {D : Type} {E : Type u_1} {ι : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {U : Set D} {gain : ℝ} {loss : ℕ → ℝ} : NativeBounds N U gain loss fun (x : ι) (x_1 : ℕ) (x_2 : D) => 0

theorem NavierStokes.PhysicalResidualJetBounds.NativeBounds.reindex {D : Type} {E : Type u_1} {ι : Type u_3} {κ : Type u_4} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {U : Set D} {gain : ℝ} {loss : ℕ → ℝ} {f : ι → ℕ → D → E} (hf : NativeBounds N U gain loss f) (a : κ → ι) : NativeBounds N U gain loss fun (l : κ) => f (a l)

theorem NavierStokes.PhysicalResidualJetBounds.NativeBounds.map {D : Type} {E : Type u_1} {F : Type u_2} {ι : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {N : ℕ} {U : Set D} {gain : ℝ} {loss : ℕ → ℝ} {f : ι → ℕ → D → E} (hf : NativeBounds N U gain loss f) (hU : IsOpen U) (L : E →L[ℝ] F) : NativeBounds N U gain loss fun (l : ι) (n : ℕ) (x : D) => L (f l n x)

theorem NavierStokes.PhysicalResidualJetBounds.NativeBounds.add {D : Type} {E : Type u_1} {ι : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {U : Set D} {gain : ℝ} {loss : ℕ → ℝ} {f g : ι → ℕ → D → E} (hN : 1 ≤ N) (hU : IsOpen U) (hf : NativeBounds N U gain loss f) (hg : NativeBounds N U gain loss g) : NativeBounds N U gain loss fun (l : ι) (n : ℕ) (x : D) => f l n x + g l n x

theorem NavierStokes.PhysicalResidualJetBounds.NativeBounds.sum {D : Type} {E : Type u_1} {ι : Type u_3} {κ : Type u_4} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {U : Set D} {gain : ℝ} {loss : ℕ → ℝ} (hN : 1 ≤ N) (hU : IsOpen U) (K : Finset κ) (a : κ → ι → ℕ → D → E) (ha : ∀ k ∈ K, NativeBounds N U gain loss (a k)) : NativeBounds N U gain loss fun (l : ι) (n : ℕ) (x : D) => ∑ k ∈ K, a k l n x

theorem NavierStokes.PhysicalResidualJetBounds.NativeBounds.congr {D : Type} {E : Type u_1} {ι : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {U : Set D} {gain : ℝ} {loss : ℕ → ℝ} {f g : ι → ℕ → D → E} (hU : IsOpen U) (hf : NativeBounds N U gain loss f) (hfg : ∀ (l : ι) (n : ℕ), N ≤ n → Set.EqOn (f l n) (g l n) U) : NativeBounds N U gain loss g

theorem NavierStokes.PhysicalResidualJetBounds.NativeBounds.weaken {D : Type} {E : Type u_1} {ι : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {U : Set D} {gain : ℝ} {loss : ℕ → ℝ} {f : ι → ℕ → D → E} (hN : 1 ≤ N) (hf : NativeBounds N U gain loss f) {gain' : ℝ} {loss' : ℕ → ℝ} (he : ∀ (m : ℕ), gain' - loss' m ≤ gain - loss m) : NativeBounds N U gain' loss' f

theorem NavierStokes.PhysicalResidualJetBounds.NativeBounds.of_localSource {ι : Type u_3} {N : ℕ} {D' E' : Type} [NormedAddCommGroup D'] [NormedSpace ℝ D'] [NormedAddCommGroup E'] [NormedSpace ℝ E'] {s : WeightedClasses.StripData D'} {h α : ℝ} {w : ι → ℕ → D' → ℝ} {a : ι → ℕ → D' → E'} {V : Set D'} (hN : 4 ≤ N) (hV : IsOpen V) (ha : LocalPhysicalCopyBounds.LocalSourceBounds s h α w a) (hsm : ∀ (l : ι) (n : ℕ), N ≤ n → ContDiffOn ℝ (↑⊤) (a l n) V) (hcover : ∀ (l : ι) (n : ℕ), N ≤ n → ∀ x ∈ V, x ∈ closure s.domain ∨ x ∉ tsupport (a l n)) : NativeBounds N V (h * α) (fun (x : ℕ) => 0) a

Genuine edge extensions retain the interior weighted estimate on the closure; outside that closure the actual zero germ is used.

theorem NavierStokes.PhysicalResidualJetBounds.NativeBounds.window_sum {D : Type} {E : Type u_1} {ι : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {U : Set D} {gain : ℝ} {loss : ℕ → ℝ} {f : ι → ℕ → D → E} (hU : IsOpen U) (hf : NativeBounds N U gain loss f) (labels : ℕ → Finset ι) (label : ℕ → ι → SlotColoring.Label) (hinj : ∀ (n : ℕ), N ≤ n → Set.InjOn (label n) ↑(labels n)) (hlevel : ∀ (n : ℕ), N ≤ n → ∀ l ∈ labels n, 1 ≤ (label n l).1) (d : ℝ) (χ : ℕ → D → LabelSumBounds.WindowPoint) (hχ : ∀ (n : ℕ), N ≤ n → ContinuousOn (χ n) U) (hs : ∀ (n : ℕ), N ≤ n → ∀ l ∈ labels n, ∀ x ∈ U, f l n x ≠ 0 → χ n x ∈ LabelSumBounds.closedWindow d (label n l)) : NativeBounds N U gain loss fun (x : Unit) (n : ℕ) (x_1 : D) => ∑ l ∈ labels n, f l n x_1

Closed label windows, not the size of the active finite set, control the spatial sum. The constant multiplier is the proved overlap 2250.

structure NavierStokes.PhysicalResidualJetBounds.SupportedPhaseBounds {D : Type u_1} {ι : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] (N : ℕ) (U : Set D) (β : ℝ) (a : ι → ℕ → D → ℂ) (Φ : ι → ℕ → D → ℝ) : Prop

Only positive derivatives of the literal phase are bounded, only on the actual coefficient support. Copy-dependent phase germs fit this interface.

• smooth (l : ι) (n : ℕ) : N ≤ n → ∀ x ∈ U, x ∈ tsupport (a l n) → LocalPhysicalCopyBounds.SmoothNear (Φ l n) x
• bounds (m : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∃ (p : ℕ), ∀ (l : ι) (n : ℕ), N ≤ n → ∀ x ∈ U, x ∈ tsupport (a l n) → ∀ (j : ℕ), 1 ≤ j → j ≤ m → ‖iteratedFDeriv ℝ j (Φ l n) x‖ ≤ B * ChartScales.S n ^ p * ChartScales.Q n ^ (-β)

theorem NavierStokes.PhysicalResidualJetBounds.mode_zero_germ {D : Type u_1} [NormedAddCommGroup D] {a : D → ℂ} (Φ : D → ℝ) (c : ℝ) {x : D} (hx : x ∉ tsupport a) : (fun (y : D) => a y * PhysicalGraphBounds.character c (Φ y)) =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.PhysicalResidualJetBounds.mode_contDiffOn {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {a : D → ℂ} {Φ : D → ℝ} (c : ℝ) (ha : ContDiffOn ℝ (↑⊤) a U) (hΦ : ∀ x ∈ U, x ∈ tsupport a → LocalPhysicalCopyBounds.SmoothNear Φ x) : ContDiffOn ℝ (↑⊤) (fun (y : D) => a y * PhysicalGraphBounds.character c (Φ y)) U

theorem NavierStokes.PhysicalResidualJetBounds.NativeBounds.mode {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] [FiniteDimensional ℝ D] {N : ℕ} {U : Set D} {gain β : ℝ} {loss : ℕ → ℝ} {a : ι → ℕ → D → ℂ} {Φ : ι → ℕ → D → ℝ} (hN : 1 ≤ N) (hU : IsOpen U) (hβ : 0 ≤ β) (ha : NativeBounds N U gain loss a) (hΦ : SupportedPhaseBounds N U β a Φ) : NativeBounds N U gain (fun (m : ℕ) => loss m + β * ↑m) fun (l : ι) (n : ℕ) (x : D) => a l n x * PhysicalGraphBounds.character 1 (Φ l n x)

theorem NavierStokes.PhysicalResidualJetBounds.NativeBounds.pi {D : Type u_1} {ι : Type u_2} {κ : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [Fintype κ] {N : ℕ} {U : Set D} {gain : ℝ} {loss : ℕ → ℝ} {f : ι → ℕ → D → κ → ℝ} (hN : 1 ≤ N) (hU : IsOpen U) (hf : ∀ (i : κ), NativeBounds N U gain loss fun (l : ι) (n : ℕ) (x : D) => f l n x i) : NativeBounds N U gain loss f

theorem NavierStokes.PhysicalResidualJetBounds.NativeBounds.pull_linear {D E F ι : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] {N : ℕ} {U : Set E} {gain : ℝ} {loss : ℕ → ℝ} {f : ι → ℕ → E → F} (hU : IsOpen U) (hf : NativeBounds N U gain loss f) (L : D →L[ℝ] E) (hL : ‖L‖ ≤ 1) : NativeBounds N (⇑L ⁻¹' U) gain loss fun (l : ι) (n : ℕ) => f l n ∘ ⇑L

Pull a genuine local bound through a fixed contraction, including the angular projection. No global extension estimate is needed.

noncomputable def NavierStokes.PhysicalResidualJetBounds.fullPhase (b : CorrectionState.HarmonicBlock Point) (j : ℤ) (n : ℕ) (x : Cylinder) : ℝ

Full phase, given by `(j : ℝ) * (b.frequency n * b.phase n x.1 + (b.angularFrequency n : ℝ)

• x.2)`.

Equations

• NavierStokes.PhysicalResidualJetBounds.fullPhase b j n x = ↑j * (b.frequency n * b.phase n x.1 + ↑(b.angularFrequency n) * x.2)

theorem NavierStokes.PhysicalResidualJetBounds.character_fullPhase (j : ℤ) (t : ℝ) : PhysicalGraphBounds.character 1 (↑j * t) = HarmonicFields.character j t

theorem NavierStokes.PhysicalResidualJetBounds.block_expansion (b : CorrectionState.HarmonicBlock Point) (J : Finset ℤ) (n : ℕ) (i : Fin 3) (hs : (b.velocity n i).support ⊆ J) (x : Cylinder) : b.oscillation n x i = ∑ j ∈ J, ((b.velocity n i).coeff j x.1 * PhysicalGraphBounds.character 1 (fullPhase b j n x)).re

theorem NavierStokes.PhysicalResidualJetBounds.block_nativeBounds {ι : Type} {N : ℕ} {U : Set Cylinder} {gain β : ℝ} (hN : 1 ≤ N) (hU : IsOpen U) (hβ : 0 ≤ β) (b : ι → CorrectionState.HarmonicBlock Point) (J : Finset ℤ) (hs : ∀ (l : ι) (n : ℕ), N ≤ n → ∀ (i : Fin 3), ((b l).velocity n i).support ⊆ J) (ha : ∀ (i : Fin 3), ∀ j ∈ J, NativeBounds N U gain (fun (x : ℕ) => 0) fun (l : ι) (n : ℕ) (x : Cylinder) => ((b l).velocity n i).coeff j x.1) (hΦ : ∀ (i : Fin 3), ∀ j ∈ J, SupportedPhaseBounds N U β (fun (l : ι) (n : ℕ) (x : Cylinder) => ((b l).velocity n i).coeff j x.1) fun (l : ι) => fullPhase (b l) j) : NativeBounds N U gain (fun (m : ℕ) => β * ↑m) fun (l : ι) => (b l).oscillation

The actual finite group-algebra block, not a separate modeled wave, inherits the coefficient bounds. The fixed harmonic set affects constants.

theorem NavierStokes.PhysicalResidualJetBounds.state_nativeBounds {ι : Type} {N : ℕ} {V : Set Point} (hN : 1 ≤ N) (hV : IsOpen V) {gain β : ℝ} {c : CorrectionState.Context Point} {s : CorrectionState.State Point} (labels : ℕ → Finset ι) (b : ι → CorrectionState.HarmonicBlock Point) (G A : ι → HarmonicResidual.BlockCoefficients Point) (hrep : HarmonicResidual.BlockRepresentation labels b G A s) (hmean : LiftedMeanResidual.MeanHypotheses V c s) (hreg : ∀ (n : ℕ), N ≤ n → HarmonicResidual.ExtractionRegular V c s labels b G A n) (hb : NativeBounds N (HarmonicResidual.liftDomain V) gain (fun (m : ℕ) => β * ↑m) fun (l : ι) => (HarmonicResidual.residualBlock c s (b l) (G l) (A l)).oscillation) (label : ℕ → ι → SlotColoring.Label) (hinj : ∀ (n : ℕ), N ≤ n → Set.InjOn (label n) ↑(labels n)) (hlevel : ∀ (n : ℕ), N ≤ n → ∀ l ∈ labels n, 1 ≤ (label n l).1) (d : ℝ) (χ : ℕ → Cylinder → LabelSumBounds.WindowPoint) (hχ : ∀ (n : ℕ), N ≤ n → ContinuousOn (χ n) (HarmonicResidual.liftDomain V)) (hs : ∀ (n : ℕ), N ≤ n → ∀ l ∈ labels n, ∀ x ∈ HarmonicResidual.liftDomain V, (HarmonicResidual.residualBlock c s (b l) (G l) (A l)).oscillation n x ≠ 0 → χ n x ∈ LabelSumBounds.closedWindow d (label n l)) (hm : NativeBounds N (HarmonicResidual.liftDomain V) gain (fun (m : ℕ) => β * ↑m) fun (x : Unit) (n : ℕ) (x_1 : Cylinder) => s.meanGoodResidual c n x_1.1) (he : NativeBounds N (HarmonicResidual.liftDomain V) gain (fun (m : ℕ) => β * ↑m) fun (x : Unit) => s.errors.total) : NativeBounds N (HarmonicResidual.liftDomain V) gain (fun (m : ℕ) => β * ↑m) fun (x : Unit) => LiftedMeanResidual.fullResidual c s

The exact reconstructed state residual is controlled by the true label overlap, the mean-good residual and the three excluded errors.

One physical residual, selected comparable bands, and the base patch

noncomputable def NavierStokes.PhysicalResidualJetBounds.residual (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) : ProblemStatement.SpaceTime → ProblemStatement.Space

Residual, defined pointwise by navierStokesResidual u p w.1 w.2.

Equations

• NavierStokes.PhysicalResidualJetBounds.residual u p w = NavierStokes.ProblemStatement.navierStokesResidual u p w.1 w.2

noncomputable def NavierStokes.PhysicalResidualJetBounds.changedSupport (u u₀ : ProblemStatement.VelocityField) (p p₀ : ProblemStatement.PressureField) : Set ProblemStatement.SpaceTime

Changed support, given by tsupport (fun w => u w - u₀ w) ∪ tsupport (fun w => p w - p₀ w).

Equations

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

theorem NavierStokes.PhysicalResidualJetBounds.residual_germ_off_changedSupport {u u₀ : ProblemStatement.VelocityField} {p p₀ : ProblemStatement.PressureField} {w : ProblemStatement.SpaceTime} (hw : w ∉ changedSupport u u₀ p p₀) : residual u p =ᶠ[nhds w] residual u₀ p₀

noncomputable def NavierStokes.PhysicalResidualJetBounds.physicalLoss (h β : ℝ) (m : ℕ) : ℝ

The loss contains the actual physical residual degree, graph derivative loss, one polynomial-in-band absorption, and the fixed phase loss.

Equations

• NavierStokes.PhysicalResidualJetBounds.physicalLoss h β m = NavierStokes.PhysicalMeanJetBounds.loss (NavierStokes.PhysicalResidualJetBounds.residualDegree h) m + β * ↑m

def NavierStokes.PhysicalResidualJetBounds.ChartIdentity (a h : ℝ) (N : ℕ) (gap : ℕ → ℕ) (U : Set Cylinder) (F : ℕ → Cylinder → Components) (R : ProblemStatement.SpaceTime → ProblemStatement.Space) : Prop

Exact realization on the true polar charts. This is a value identity, not a derivative or size estimate; a primitive-state constructor is below.

Equations

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

theorem NavierStokes.PhysicalResidualJetBounds.ChartIdentity.germ {a b h : ℝ} {N : ℕ} {gap : ℕ → ℕ} {U : Set Cylinder} {F : ℕ → Cylinder → Components} {R : ProblemStatement.SpaceTime → ProblemStatement.Space} (ha : 0 < a) (hU : IsOpen U) (hreal : ChartIdentity a h N gap U F R) {n : ℕ} (hn : N ≤ n) (j : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hann : (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b) (hj : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) (hx : polarGraph a h j n (gap n) w ∈ U) : R =ᶠ[nhds w] cartesianPull a h j n (gap n) (residualDegree h) (F n)

structure NavierStokes.PhysicalResidualJetBounds.ResidualChartData (a b h : ℝ) (N Δ : ℕ) (U : Set Cylinder) (F : ℕ → Cylinder → Components) (u u₀ : ProblemStatement.VelocityField) (p p₀ : ProblemStatement.PressureField) : Type

Geometric support and exact coherent realization of the same physical fields. No physical residual bound or global raw smoothness is a field.

• active : Set ProblemStatement.SpaceTime

  Active of ResidualChartData, of type Set SpaceTime.

• changed_subset : changedSupport u u₀ p p₀ ⊆ self.active
• gap : ℕ → ℕ

  Gap of ResidualChartData, of type ℕ → ℕ.

• gap_le (n : ℕ) : N ≤ n → self.gap n ≤ Δ
• realization : ChartIdentity a h N self.gap U F (residual u p)
• annulus (n : ℕ) : N ≤ n → ∀ w ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h w / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * PhysicalWaveSum.physicalQ h w → w ∈ self.active → (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus a b
• in_domain (n : ℕ) : N ≤ n → ∀ w ∈ PhysicalWaveSum.preterminal, PhysicalWaveSum.physicalQ h w / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * PhysicalWaveSum.physicalQ h w → w ∈ self.active → ∀ (j : PolarCharts.Index), (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j → polarGraph a h j n (self.gap n) w ∈ U

theorem NavierStokes.PhysicalResidualJetBounds.ResidualChartData.residual_jet_bound {a b h gain β : ℝ} {N Δ : ℕ} {U : Set Cylinder} {F : ℕ → Cylinder → Components} {u u₀ : ProblemStatement.VelocityField} {p p₀ : ProblemStatement.PressureField} (d : ResidualChartData a b h N Δ U F u u₀ p p₀) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hN : 4 ≤ N) (hU : IsOpen U) (hF : NativeBounds N U gain (fun (m : ℕ) => β * ↑m) fun (x : Unit) => F) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ w ∈ PhysicalWaveSum.preterminal, |w.1| ≤ 1 → PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q N → w ∈ d.active → ‖iteratedFDeriv ℝ m (residual u p) w‖ ≤ C * PhysicalWaveSum.physicalQ h w ^ (gain - physicalLoss h β m)

A comparable band is proved to exist at each supported point. Outside the correction support the actual finite residual has the base residual germ.

theorem NavierStokes.PhysicalResidualJetBounds.eventually_time_small (x : ProblemStatement.Space) : ∀ᶠ (w : ProblemStatement.SpaceTime) in nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1), |w.1| ≤ 1

theorem NavierStokes.PhysicalResidualJetBounds.ResidualChartData.residual_jetRate {a b h gain β : ℝ} {N Δ : ℕ} {U : Set Cylinder} {F : ℕ → Cylinder → Components} {u u₀ : ProblemStatement.VelocityField} {p p₀ : ProblemStatement.PressureField} (d : ResidualChartData a b h N Δ U F u u₀ p p₀) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hN : 4 ≤ N) (hU : IsOpen U) (hF : NativeBounds N U gain (fun (m : ℕ) => β * ↑m) fun (x : Unit) => F) (m : ℕ) (hbase : DiagonalResidual.JetRate (nhdsWithin (1, 0) (SpacetimeEndpoint.openPast 1) ⊓ Filter.principal d.activeᶜ) (PhysicalWaveSum.physicalQ h) (residual u₀ p₀) m (gain - physicalLoss h β m)) : DiagonalResidual.JetRate (nhdsWithin (1, 0) (SpacetimeEndpoint.openPast 1)) (PhysicalWaveSum.physicalQ h) (residual u p) m (gain - physicalLoss h β m)

The finite-residual rate consumed by the diagonal assembly. The same physicalLoss h β m works for every stage and every native exponent gain.

Primitive physical-state realization

noncomputable def NavierStokes.PhysicalResidualJetBounds.bandGraph (h : ℝ) (n d : ℕ) : PhysicalResidualBridge.ScaledGraph

Band graph, given by PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (ChartScales.nativeIndex h n - d).

Equations

• NavierStokes.PhysicalResidualJetBounds.bandGraph h n d = NavierStokes.PhysicalResidualBridge.commonGraph (NavierStokes.ChartScales.Q n) h (NavierStokes.ChartScales.nativeIndex h n - d)

theorem NavierStokes.PhysicalResidualJetBounds.polarGraph_eq_meanGraph {a : ℝ} (ha : 0 < a) (h : ℝ) (j : PolarCharts.Index) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : polarGraph a h j n d w = (PhysicalMeanJetBounds.graph h n d w, ResidualPolarGraph.angle a j n w)

structure NavierStokes.PhysicalResidualJetBounds.StateRealization (h : ℝ) (N : ℕ) (gap : ℕ → ℕ) (U : Set Cylinder) (c : CorrectionState.Context Point) (s : CorrectionState.State Point) (p₀ : ℕ → Cylinder → ℝ) (u : ProblemStatement.VelocityField) (P : ProblemStatement.PressureField) : Prop

All assumptions refer to the primitive physical fields or the already fixed base-pressure equation. No residual equality or estimate is assumed.

• domain_open : IsOpen U
• radius_ne (x : Cylinder) : x ∈ U → x.1.1 ≠ 0
• gap_native (n : ℕ) : N ≤ n → gap n ≤ ChartScales.nativeIndex h n
• matching (n : ℕ) : N ≤ n → PhysicalResidualTZ.MatchesAtTZ c.operators (bandGraph h n (gap n)) n
• base_smooth (n : ℕ) : N ≤ n → ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (x : PhysicalResidualBridge.Cylinder) => PhysicalResidualBridge.baseComponents c n x i) U
• increment_smooth (n : ℕ) : N ≤ n → ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (x : PhysicalResidualBridge.Cylinder) => PhysicalResidualBridge.incrementComponents s n x i) U
• base_pressure_smooth (n : ℕ) : N ≤ n → ContDiffOn ℝ (↑⊤) (p₀ n) U
• pressure_smooth (n : ℕ) : N ≤ n → ContDiffOn ℝ (↑⊤) (s.totalPressureIncrement n) U
• base_equation (n : ℕ) : N ≤ n → ∀ x ∈ U, ∀ (i : Fin 3), PhysicalResidualBridge.graphResidual (ChartScales.Q n ^ h) PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualTZ.graphRadialTZ (bandGraph h n (gap n))) PhysicalResidualTZ.graphAngularTZ (PhysicalResidualTZ.graphAxialTZ (bandGraph h n (gap n))) (PhysicalResidualTZ.graphTemporalTZ (bandGraph h n (gap n))) (PhysicalResidualBridge.baseComponents c n) (p₀ n) x i = LiftedMeanResidual.virtualDivergence c n x i + s.errors.base n x i
• physical_velocity_smooth (n : ℕ) : N ≤ n → ∀ z ∈ PhysicalWaveSum.preterminal, z ∈ PhysicalResidualTZ.graphSourceTZ (bandGraph h n (gap n)) U → ContDiffAt ℝ 2 u (z.1, CylindricalResidual.chart z.2)
• physical_pressure_differentiable (n : ℕ) : N ≤ n → ∀ z ∈ PhysicalWaveSum.preterminal, z ∈ PhysicalResidualTZ.graphSourceTZ (bandGraph h n (gap n)) U → DifferentiableAt ℝ P (z.1, CylindricalResidual.chart z.2)
• velocity_germ (n : ℕ) : N ≤ n → ∀ z ∈ PhysicalWaveSum.preterminal, z ∈ PhysicalResidualTZ.graphSourceTZ (bandGraph h n (gap n)) U → (fun (y : ProblemStatement.SpaceTime) => u (y.1, CylindricalResidual.chart y.2)) =ᶠ[nhds z] fun (y : ProblemStatement.SpaceTime) => (CylindricalResidual.frame (y.2.ofLp 1)) (PhysicalResidualTZ.velocityTZ (bandGraph h n (gap n)) (fun (x : PhysicalResidualTZ.Cylinder) (i : Fin 3) => PhysicalResidualBridge.baseComponents c n x i + PhysicalResidualBridge.incrementComponents s n x i) y)
• pressure_germ (n : ℕ) : N ≤ n → ∀ z ∈ PhysicalWaveSum.preterminal, z ∈ PhysicalResidualTZ.graphSourceTZ (bandGraph h n (gap n)) U → CylindricalResidual.pressurePullback P =ᶠ[nhds z] PhysicalResidualTZ.pressureTZ (bandGraph h n (gap n)) fun (x : PhysicalResidualTZ.Cylinder) => p₀ n x + s.totalPressureIncrement n x

theorem NavierStokes.PhysicalResidualJetBounds.StateRealization.chartIdentity {a h : ℝ} {N : ℕ} {gap : ℕ → ℕ} {U : Set Cylinder} {c : CorrectionState.Context Point} {s : CorrectionState.State Point} {p₀ : ℕ → Cylinder → ℝ} {u : ProblemStatement.VelocityField} {P : ProblemStatement.PressureField} (ha : 0 < a) (r : StateRealization h N gap U c s p₀ u P) : ChartIdentity a h N gap U (LiftedMeanResidual.fullResidual c s) (residual u P)

The exact Cartesian reconstruction follows from the concrete Navier--Stokes operator identity, after the genuine polar inverse.

Weighted invariant and finite-stage consumers

theorem NavierStokes.PhysicalResidualJetBounds.coefficient_source_of_uniformVelocity {ι : Type} {s : WeightedClasses.StripData Point} {h α : ℝ} {P : ι → ℕ → Point → ℝ} {b : ι → CorrectionState.HarmonicBlock Point} (hb : UniformHarmonicInteraction.UniformVelocity s P α b) (hflat : ∃ (cL : ℝ) (cR : ℝ) (L : ℝ) (ρ : Point → ℝ), PhysicalClassBounds.FlatGeometry s cL cR L ρ) (hw : ∃ (c : ℝ), 0 < c ∧ ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, √(s.zeta x) * P l n x ≤ s.zeta x ^ c) (he : ∀ (n : ℕ), s.epsilon n = ChartScales.epsilon h n) (hslow : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (p : ℕ), ∀ (n : ℕ), 4 ≤ n → s.slow n ≤ C * ChartScales.S n ^ p) (i : Fin 3) (j : ℤ) (hj : j ≠ 0) : LocalPhysicalCopyBounds.LocalSourceBounds s h α (fun (l : ι) (n : ℕ) (x : Point) => √(s.zeta x) * P l n x) fun (l : ι) (n : ℕ) (x : Point) => ((b l).velocity n i).coeff j x

The concrete uniform harmonic invariant supplies the uniform part of each weighted coefficient input; all remaining hypotheses are geometry.

theorem NavierStokes.PhysicalResidualJetBounds.block_nativeBounds_of_weighted {ι : Type} {N : ℕ} {V : Set Point} {h α β : ℝ} {s : WeightedClasses.StripData Point} {w : ι → ℕ → Point → ℝ} (hN : 4 ≤ N) (hV : IsOpen V) (hβ : 0 ≤ β) (b : ι → CorrectionState.HarmonicBlock Point) (J : Finset ℤ) (hs : ∀ (l : ι) (n : ℕ), N ≤ n → ∀ (i : Fin 3), ((b l).velocity n i).support ⊆ J) (ha : ∀ (i : Fin 3), ∀ j ∈ J, LocalPhysicalCopyBounds.LocalSourceBounds s h α w fun (l : ι) (n : ℕ) (x : Point) => ((b l).velocity n i).coeff j x) (hsm : ∀ (i : Fin 3), ∀ j ∈ J, ∀ (l : ι) (n : ℕ), N ≤ n → ContDiffOn ℝ (↑⊤) (((b l).velocity n i).coeff j) V) (hcover : ∀ (i : Fin 3), ∀ j ∈ J, ∀ (l : ι) (n : ℕ), N ≤ n → ∀ x ∈ V, x ∈ closure s.domain ∨ x ∉ tsupport (((b l).velocity n i).coeff j)) (hΦ : ∀ (i : Fin 3), ∀ j ∈ J, SupportedPhaseBounds N (HarmonicResidual.liftDomain V) β (fun (l : ι) (n : ℕ) (x : Cylinder) => ((b l).velocity n i).coeff j x.1) fun (l : ι) => fullPhase (b l) j) : NativeBounds N (HarmonicResidual.liftDomain V) (h * α) (fun (m : ℕ) => β * ↑m) fun (l : ι) => (b l).oscillation

This adapter uses the actual smooth edge extension of each coefficient, then lifts it to the angular product. The raw totalization need not be smooth.

theorem NavierStokes.PhysicalResidualJetBounds.NativeBounds.to_phaseLoss {D E ι : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {U : Set D} {gain gain' β : ℝ} {f : ι → ℕ → D → E} (hf : NativeBounds N U gain (fun (x : ℕ) => 0) f) (hN : 1 ≤ N) (hβ : 0 ≤ β) (hg : gain' ≤ gain) : NativeBounds N U gain' (fun (m : ℕ) => β * ↑m) f

Raising the fixed derivative loss never changes a coefficient field.

theorem NavierStokes.PhysicalResidualJetBounds.excluded_nativeBounds {N : ℕ} {U : Set Cylinder} {gain : ℝ} {loss : ℕ → ℝ} (hN : 1 ≤ N) (hU : IsOpen U) (e : CorrectionState.ExcludedErrors Point) (hb : NativeBounds N U gain loss fun (x : Unit) => e.base) (hg : NativeBounds N U gain loss fun (x : Unit) => e.gaussian) (ha : NativeBounds N U gain loss fun (x : Unit) => e.aliasError) : NativeBounds N U gain loss fun (x : Unit) => e.total

theorem NavierStokes.PhysicalResidualJetBounds.jetRate_of_zero_germs {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {R : ProblemStatement.SpaceTime → ProblemStatement.Space} (hz : ∀ᶠ (w : ProblemStatement.SpaceTime) in l, R =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0) (m : ℕ) (r : ℝ) : DiagonalResidual.JetRate l q R m r

An actual exterior zero germ proves every exterior residual rate.

theorem NavierStokes.PhysicalResidualJetBounds.finite_residual_rates {a b h β : ℝ} {N Δ : ℕ} {gain : ℕ → ℝ} {U : ℕ → Set Cylinder} {F : ℕ → ℕ → Cylinder → Components} {u : ℕ → ProblemStatement.VelocityField} {p : ℕ → ProblemStatement.PressureField} {u₀ : ProblemStatement.VelocityField} {p₀ : ProblemStatement.PressureField} (d : (J : ℕ) → ResidualChartData a b h N Δ (U J) (F J) (u J) u₀ (p J) p₀) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hN : 4 ≤ N) (hU : ∀ (J : ℕ), IsOpen (U J)) (hF : ∀ (J : ℕ), NativeBounds N (U J) (gain J) (fun (m : ℕ) => β * ↑m) fun (x : Unit) => F J) (hbase : ∀ (J m : ℕ), DiagonalResidual.JetRate (nhdsWithin (1, 0) (SpacetimeEndpoint.openPast 1) ⊓ Filter.principal (d J).activeᶜ) (PhysicalWaveSum.physicalQ h) (residual u₀ p₀) m (gain J - physicalLoss h β m)) (J m : ℕ) : DiagonalResidual.JetRate (nhdsWithin (1, 0) (SpacetimeEndpoint.openPast 1)) (PhysicalWaveSum.physicalQ h) (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual (u J) (p J) z.1 z.2) m (gain J - physicalLoss h β m)

One fixed loss function applies to the actual residual after every finite correction stage. Constants and the finite harmonic cutoff may vary with the stage; the band floor, cover gap and phase loss stay fixed.

@[reducible, inline]

abbrev NavierStokes.ActualPolarCoverage.Point : Type

Point: an abbreviation for PhysicalMeanJetBounds.Point.

Equations

• NavierStokes.ActualPolarCoverage.Point = NavierStokes.PhysicalMeanJetBounds.Point

@[reducible, inline]

abbrev NavierStokes.ActualPolarCoverage.Cylinder : Type

Cylinder: an abbreviation for PhysicalResidualJetBounds.Cylinder.

Equations

• NavierStokes.ActualPolarCoverage.Cylinder = NavierStokes.PhysicalResidualJetBounds.Cylinder

noncomputable def NavierStokes.ActualPolarCoverage.active : Set ProblemStatement.SpaceTime

Active as an element of Set SpaceTime.

Equations

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

noncomputable def NavierStokes.ActualPolarCoverage.inner : ℝ

Inner, given by PrimaryTargetBounds.leftRadius ActualPrimary.nominal / 4.

Equations

• NavierStokes.ActualPolarCoverage.inner = NavierStokes.PrimaryTargetBounds.leftRadius NavierStokes.CorrectionInitialization.ActualPrimary.nominal / 4

noncomputable def NavierStokes.ActualPolarCoverage.outer : ℝ

Outer, given by 2 * PrimaryTargetBounds.rightRadius ActualPrimary.nominal.

Equations

• NavierStokes.ActualPolarCoverage.outer = 2 * NavierStokes.PrimaryTargetBounds.rightRadius NavierStokes.CorrectionInitialization.ActualPrimary.nominal

noncomputable def NavierStokes.ActualPolarCoverage.nativeDomain : Set Cylinder

Native domain, given by HarmonicResidual.liftDomain (ActualInitialization.geometry.domain ∩ {x : Point | 0 < x.1}).

Equations

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

theorem NavierStokes.ActualPolarCoverage.inner_pos : 0 < inner

theorem NavierStokes.ActualPolarCoverage.outer_pos : 0 < outer

theorem NavierStokes.ActualPolarCoverage.inner_lt_outer : inner < outer

theorem NavierStokes.ActualPolarCoverage.nativeDomain_open : IsOpen nativeDomain

theorem NavierStokes.ActualPolarCoverage.nativeDomain_radius_pos {x : Cylinder} (hx : x ∈ nativeDomain) : 0 < x.1.1

theorem NavierStokes.ActualPolarCoverage.nativeDomain_radius_ne {x : Cylinder} (hx : x ∈ nativeDomain) : x.1.1 ≠ 0

Scale identities independent of the particular actual profile

theorem NavierStokes.ActualPolarCoverage.graph_radius_nonneg (h : ℝ) (n d : ℕ) (w : ProblemStatement.SpaceTime) : 0 ≤ (PhysicalMeanJetBounds.graph h n d w).1

theorem NavierStokes.ActualPolarCoverage.graph_radius_sq (h : ℝ) (n d : ℕ) (w : ProblemStatement.SpaceTime) : (PhysicalMeanJetBounds.graph h n d w).1 ^ 2 = (w.2.ofLp 0 ^ 2 + w.2.ofLp 1 ^ 2) / ChartScales.Q n

theorem NavierStokes.ActualPolarCoverage.graph_profileRadius_sq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) : ((PhysicalMeanJetBounds.graph h n d w).1 / VariableGaugeMean.qLength (2 * h) (PhysicalMeanJetBounds.graph h n d w).2.1) ^ 2 / 2 = (SlowBorelBase.cartesianChart h w).2.1

theorem NavierStokes.ActualPolarCoverage.graph_profileRadius_mem {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hactive : (SlowBorelBase.cartesianChart F.data.h w).2.1 ∈ Set.Icc (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W)) : (PhysicalMeanJetBounds.graph F.data.h n d w).1 / VariableGaugeMean.qLength (2 * F.data.h) (PhysicalMeanJetBounds.graph F.data.h n d w).2.1 ∈ Set.Icc (PrimaryTargetBounds.leftRadius W) (PrimaryTargetBounds.rightRadius W)

Closure of a moving strip, including both radial endpoints

theorem NavierStokes.ActualPolarCoverage.mem_closure_strip (G : SignedMeanGain.Geometry) {x : Point} (hx : x ∈ G.domain) (hr : (LocalSignedRequest.profileMap G.coord x).1 ∈ Set.Icc G.patch.a G.patch.b) : x ∈ closure G.strip.domain

theorem NavierStokes.ActualPolarCoverage.mem_closure_liftStrip (G : SignedMeanGain.Geometry) {x : Point} (hx : x ∈ G.domain) (hr : (LocalSignedRequest.profileMap G.coord x).1 ∈ Set.Icc G.patch.a G.patch.b) (theta : ℝ) : (x, theta) ∈ closure (HarmonicResidual.liftDomain G.strip.domain)

The actual selected band belongs to the native slow window

theorem NavierStokes.ActualPolarCoverage.graph_slow_mem_standard {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hqQ : PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q n) (hQq : ChartScales.Q n < 2 * PhysicalWaveSum.physicalQ h w) : (PhysicalMeanJetBounds.graph h n d w).2.1 ∈ (ActualSignedGeometry.standardSlowRegion hh hh1).carrier

theorem NavierStokes.ActualPolarCoverage.selected_mean_domain (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hqQ : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q n) (hQq : ChartScales.Q n < 2 * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w) : PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w ∈ ActualInitialization.geometry.domain

theorem NavierStokes.ActualPolarCoverage.selected_mean_radius_pos (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hactive : w ∈ active) : 0 < (PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n d w).1

theorem NavierStokes.ActualPolarCoverage.selected_annulus (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hactive : w ∈ active) (hqQ : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q n) (hQq : ChartScales.Q n < 2 * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w) : (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus inner outer

theorem NavierStokes.ActualPolarCoverage.selected_chart_exists (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hactive : w ∈ active) (hqQ : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q n) (hQq : ChartScales.Q n < 2 * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w) : ∃ (j : PolarCharts.Index), (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain inner j

theorem NavierStokes.ActualPolarCoverage.selected_polar_nativeDomain (j : PolarCharts.Index) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hactive : w ∈ active) (hqQ : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q n) (hQq : ChartScales.Q n < 2 * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w) (hj : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain inner j) : PhysicalResidualJetBounds.polarGraph inner CorrectionInitialization.ActualPrimary.h j n d w ∈ nativeDomain

theorem NavierStokes.ActualPolarCoverage.selected_polar_closure (j : PolarCharts.Index) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hactive : w ∈ active) (hqQ : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q n) (hQq : ChartScales.Q n < 2 * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w) (hj : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain inner j) : PhysicalResidualJetBounds.polarGraph inner CorrectionInitialization.ActualPrimary.h j n d w ∈ closure (HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain)

Selection above an arbitrary certified floor

theorem NavierStokes.ActualPolarCoverage.exists_selected_band (N : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hactive : w ∈ active) (hsmall : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q N) : ∃ (n : ℕ), N ≤ n ∧ PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q n ∧ ChartScales.Q n < 2 * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ∧ (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus inner outer ∧ ∀ (j : PolarCharts.Index) (d : ℕ), (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain inner j → PhysicalResidualJetBounds.polarGraph inner CorrectionInitialization.ActualPrimary.h j n d w ∈ nativeDomain ∧ PhysicalResidualJetBounds.polarGraph inner CorrectionInitialization.ActualPrimary.h j n d w ∈ closure (HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain)

theorem NavierStokes.ActualPolarCoverage.exists_selected_band_of_qbig (firstBand : ℕ) {qbig : ℝ} {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (hactive : w ∈ active) (hsmall : PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ qbig) (hfloor : qbig ≤ ChartScales.Q firstBand) : ∃ (n : ℕ), firstBand ≤ n ∧ PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ≤ ChartScales.Q n ∧ ChartScales.Q n < 2 * PhysicalWaveSum.physicalQ CorrectionInitialization.ActualPrimary.h w ∧ (PhysicalGraphBounds.scaledRadial n) w ∈ PhysicalGraphBounds.annulus inner outer ∧ ∀ (j : PolarCharts.Index) (d : ℕ), (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain inner j → PhysicalResidualJetBounds.polarGraph inner CorrectionInitialization.ActualPrimary.h j n d w ∈ nativeDomain ∧ PhysicalResidualJetBounds.polarGraph inner CorrectionInitialization.ActualPrimary.h j n d w ∈ closure (HarmonicResidual.liftDomain ActualInitialization.geometry.strip.domain)