Physical derivatives of the native graph

The graph, the integer covering, and the rounded carrier here are the actual ones of Definition 8.1 and equation (26). Bounds use actual Fréchet jets.

Four genuine polar charts with uniform finite-jet bounds

The globally smooth functions constructed below equal the actual local polar inverse on neighborhoods of four compact sectors. Their global extensions are not asserted to be a global choice of angle.

@[reducible, inline]

abbrev NavierStokes.PolarCharts.Plane : Type

Plane: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.PolarCharts.Plane = (ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.PolarCharts.Index : Type

Index: an abbreviation for Fin 4.

Equations

• NavierStokes.PolarCharts.Index = Fin 4

noncomputable def NavierStokes.PolarCharts.rotate (j : Index) (p : Plane) : Plane

Rotation by the negative of the chart offset.

Equations

• NavierStokes.PolarCharts.rotate j p = ![(p.1, p.2), (p.2, -p.1), (-p.1, -p.2), (-p.2, p.1)] j

noncomputable def NavierStokes.PolarCharts.unrotate (j : Index) (p : Plane) : Plane

Unrotate, given by ![(p.1, p.2), (-p.2, p.1), (-p.1, -p.2), (p.2, -p.1)] j.

Equations

• NavierStokes.PolarCharts.unrotate j p = ![(p.1, p.2), (-p.2, p.1), (-p.1, -p.2), (p.2, -p.1)] j

noncomputable def NavierStokes.PolarCharts.offset (j : Index) : ℝ

Offset, given by ![0, Real.pi / 2, Real.pi, Real.pi + Real.pi / 2] j.

Equations

• NavierStokes.PolarCharts.offset j = ![0, Real.pi / 2, Real.pi, Real.pi + Real.pi / 2] j

theorem NavierStokes.PolarCharts.rotate_contDiff (j : Index) : ContDiff ℝ (↑⊤) (rotate j)

theorem NavierStokes.PolarCharts.unrotate_rotate (j : Index) (p : Plane) : unrotate j (rotate j p) = p

theorem NavierStokes.PolarCharts.rotate_unrotate (j : Index) (p : Plane) : rotate j (unrotate j p) = p

theorem NavierStokes.PolarCharts.norm_rotate (j : Index) (p : Plane) : ‖rotate j p‖ = ‖p‖

theorem NavierStokes.PolarCharts.rotate_sum_sq (j : Index) (p : Plane) : (rotate j p).1 ^ 2 + (rotate j p).2 ^ 2 = p.1 ^ 2 + p.2 ^ 2

noncomputable def NavierStokes.PolarCharts.radius (p : Plane) : ℝ

Radius, given by Real.sqrt (p.1 ^ 2 + p.2 ^ 2).

Equations

• NavierStokes.PolarCharts.radius p = √(p.1 ^ 2 + p.2 ^ 2)

theorem NavierStokes.PolarCharts.radius_nonneg (p : Plane) : 0 ≤ radius p

theorem NavierStokes.PolarCharts.radius_sq (p : Plane) : radius p ^ 2 = p.1 ^ 2 + p.2 ^ 2

theorem NavierStokes.PolarCharts.radius_continuous : Continuous radius

theorem NavierStokes.PolarCharts.norm_le_radius (p : Plane) : ‖p‖ ≤ radius p

theorem NavierStokes.PolarCharts.radius_le_two_norm (p : Plane) : radius p ≤ 2 * ‖p‖

theorem NavierStokes.PolarCharts.radius_pos_of_fst_pos {p : Plane} (hp : 0 < p.1) : 0 < radius p

theorem NavierStokes.PolarCharts.radius_rotate (j : Index) (p : Plane) : radius (rotate j p) = radius p

noncomputable def NavierStokes.PolarCharts.polar (q : Plane) : Plane

The genuine Cartesian map, with radius in the first coordinate.

Equations

• NavierStokes.PolarCharts.polar q = (q.1 * Real.cos q.2, q.1 * Real.sin q.2)

theorem NavierStokes.PolarCharts.polar_contDiff : ContDiff ℝ (↑⊤) polar

theorem NavierStokes.PolarCharts.radius_polar (r θ : ℝ) : radius (polar (r, θ)) = |r|

theorem NavierStokes.PolarCharts.polar_add_offset (j : Index) (r θ : ℝ) : polar (r, θ + offset j) = unrotate j (polar (r, θ))

noncomputable def NavierStokes.PolarCharts.baseChart (p : Plane) : Plane

Base chart, given by (radius p, Real.arctan (p.2 / p.1)).

Equations

• NavierStokes.PolarCharts.baseChart p = (NavierStokes.PolarCharts.radius p, Real.arctan (p.2 / p.1))

theorem NavierStokes.PolarCharts.polar_baseChart {p : Plane} (hp : 0 < p.1) : polar (baseChart p) = p

theorem NavierStokes.PolarCharts.baseChart_polar {r θ : ℝ} (hr : 0 < r) (hθ : θ ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) : baseChart (polar (r, θ)) = (r, θ)

noncomputable def NavierStokes.PolarCharts.localChart (j : Index) (p : Plane) : Plane

A local angle in the interval centered at the fixed chart offset.

Equations

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

theorem NavierStokes.PolarCharts.localChart_apply (j : Index) (p : Plane) : localChart j p = (radius p, Real.arctan ((rotate j p).2 / (rotate j p).1) + offset j)

theorem NavierStokes.PolarCharts.polar_localChart (j : Index) {p : Plane} (hp : 0 < (rotate j p).1) : polar (localChart j p) = p

theorem NavierStokes.PolarCharts.localChart_polar (j : Index) {r θ : ℝ} (hr : 0 < r) (hθ : θ - offset j ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) : localChart j (polar (r, θ)) = (r, θ)

theorem NavierStokes.PolarCharts.localChart_contDiffAt (j : Index) {p : Plane} (hp : 0 < (rotate j p).1) : ContDiffAt ℝ (↑⊤) (localChart j) p

noncomputable def NavierStokes.PolarCharts.annulus (a b : ℝ) : Set Plane

The original normalized compact annulus uses the product norm.

Equations

• NavierStokes.PolarCharts.annulus a b = Metric.closedBall 0 b ∩ {p : NavierStokes.PolarCharts.Plane | a ≤ ‖p‖}

noncomputable def NavierStokes.PolarCharts.sector (a b : ℝ) (j : Index) : Set Plane

Compact sectors are strictly inside their chart domains.

Equations

• NavierStokes.PolarCharts.sector a b j = Metric.closedBall 0 b ∩ {p : NavierStokes.PolarCharts.Plane | a / 2 ≤ (NavierStokes.PolarCharts.rotate j p).1}

noncomputable def NavierStokes.PolarCharts.chartDomain (a : ℝ) (j : Index) : Set Plane

Chart domain, given by {p | a / 4 < (rotate j p).1}.

Equations

• NavierStokes.PolarCharts.chartDomain a j = {p : NavierStokes.PolarCharts.Plane | a / 4 < (NavierStokes.PolarCharts.rotate j p).1}

theorem NavierStokes.PolarCharts.chartDomain_open (a : ℝ) (j : Index) : IsOpen (chartDomain a j)

theorem NavierStokes.PolarCharts.sector_isCompact (a b : ℝ) (j : Index) : IsCompact (sector a b j)

theorem NavierStokes.PolarCharts.sector_subset_chartDomain {a b : ℝ} (ha : 0 < a) (j : Index) : sector a b j ⊆ chartDomain a j

theorem NavierStokes.PolarCharts.exists_rotate_fst_ge {a : ℝ} {p : Plane} (hp : a ≤ ‖p‖) : ∃ (j : Index), a ≤ (rotate j p).1

theorem NavierStokes.PolarCharts.annulus_covered {a b : ℝ} (ha : 0 < a) {p : Plane} (hp : p ∈ annulus a b) : ∃ (j : Index), p ∈ sector a b j

theorem NavierStokes.PolarCharts.euclidean_annulus_covered {a b : ℝ} {p : Plane} (hlo : a ≤ radius p) (hhi : radius p ≤ b) : ∃ (j : Index), p ∈ sector a b j

The same four sectors cover a compact annulus defined by the Euclidean radius, with the stated margin rotated x ≥ a/2.

noncomputable def NavierStokes.PolarCharts.extendedBase (a : ℝ) (p : Plane) : Plane

A concrete global extension of the base polar chart.

Equations

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

theorem NavierStokes.PolarCharts.extendedBase_contDiff {a : ℝ} (ha : 0 < a) : ContDiff ℝ (↑⊤) (extendedBase a)

theorem NavierStokes.PolarCharts.extendedBase_eq {a : ℝ} (ha : 0 < a) {p : Plane} (hp : a / 4 < p.1) : extendedBase a p = baseChart p

noncomputable def NavierStokes.PolarCharts.chart (a : ℝ) (j : Index) (p : Plane) : Plane

Globally smooth chart extension; its polar inverse meaning is local.

Equations

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

theorem NavierStokes.PolarCharts.chart_contDiff {a : ℝ} (ha : 0 < a) (j : Index) : ContDiff ℝ (↑⊤) (chart a j)

theorem NavierStokes.PolarCharts.chart_eq_localChart {a : ℝ} (ha : 0 < a) (j : Index) {p : Plane} (hp : p ∈ chartDomain a j) : chart a j p = localChart j p

theorem NavierStokes.PolarCharts.chart_eventuallyEq_localChart {a : ℝ} (ha : 0 < a) (j : Index) {p : Plane} (hp : p ∈ chartDomain a j) : chart a j =ᶠ[nhds p] localChart j

theorem NavierStokes.PolarCharts.polar_chart {a : ℝ} (ha : 0 < a) (j : Index) {p : Plane} (hp : p ∈ chartDomain a j) : polar (chart a j p) = p

theorem NavierStokes.PolarCharts.chart_polar {a : ℝ} (ha : 0 < a) (j : Index) {r θ : ℝ} (hr : 0 < r) (hθ : θ - offset j ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) (hp : polar (r, θ) ∈ chartDomain a j) : chart a j (polar (r, θ)) = (r, θ)

theorem NavierStokes.PolarCharts.chart_jet_eq_localChart {a : ℝ} (ha : 0 < a) (j : Index) {p : Plane} (hp : p ∈ chartDomain a j) (k : ℕ) : iteratedFDeriv ℝ k (chart a j) p = iteratedFDeriv ℝ k (localChart j) p

On the compact sectors every actual derivative of the global extension equals the derivative of the genuine local polar inverse.

theorem NavierStokes.PolarCharts.chart_finiteJets_uniform {a : ℝ} (ha : 0 < a) (b : ℝ) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (j : Index), ∀ k ≤ m, ∀ p ∈ Metric.closedBall 0 b, ‖iteratedFDeriv ℝ k (chart a j) p‖ ≤ C

A single constant bounds all actual jets up to the given order for all four explicit chart extensions on the fixed closed ball.

theorem NavierStokes.PolarCharts.localChart_finiteJets_uniform {a : ℝ} (ha : 0 < a) (b : ℝ) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (j : Index), ∀ k ≤ m, ∀ p ∈ sector a b j, ‖iteratedFDeriv ℝ k (localChart j) p‖ ≤ C

The compact sectors cover the annulus and carry one uniform bound for the actual local inverse jets, not merely for a prescribed jet family.

theorem NavierStokes.PolarCharts.norm_jet_comp_linear {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : Plane → Plane} (hf : ContDiff ℝ (↑⊤) f) (L : E →L[ℝ] Plane) (p : E) (k : ℕ) : ‖iteratedFDeriv ℝ k (f ∘ ⇑L) p‖ ≤ ‖iteratedFDeriv ℝ k f (L p)‖ * ‖L‖ ^ k

The exact multilinear chain rule for a linear input change.

theorem NavierStokes.PolarCharts.chart_comp_linear_finiteJets {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} (ha : 0 < a) (b : ℝ) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (j : Index), ∀ k ≤ m, ∀ (L : E →L[ℝ] Plane) (p : E), L p ∈ Metric.closedBall 0 b → ‖iteratedFDeriv ℝ k (chart a j ∘ ⇑L) p‖ ≤ C * ‖L‖ ^ k

noncomputable def NavierStokes.PolarCharts.scalePlane (Q : ℝ) : Plane →L[ℝ] Plane

Scale plane, given by Q ^ (-(1 / 2 : ℝ)) • ContinuousLinearMap.id ℝ Plane.

Equations

• NavierStokes.PolarCharts.scalePlane Q = Q ^ (-(1 / 2)) • ContinuousLinearMap.id ℝ NavierStokes.PolarCharts.Plane

@[simp]

theorem NavierStokes.PolarCharts.scalePlane_apply (Q : ℝ) (p : Plane) : (scalePlane Q) p = Q ^ (-(1 / 2)) • p

theorem NavierStokes.PolarCharts.norm_scalePlane_le {Q : ℝ} (hQ : 0 < Q) : ‖scalePlane Q‖ ≤ Q ^ (-(1 / 2))

noncomputable def NavierStokes.PolarCharts.physicalChart (a : ℝ) (j : Index) (Q : ℝ) : Plane → Plane

The physical input is scaled by 1 / sqrt Q before taking the polar chart.

Equations

• NavierStokes.PolarCharts.physicalChart a j Q = NavierStokes.PolarCharts.chart a j ∘ ⇑(NavierStokes.PolarCharts.scalePlane Q)

theorem NavierStokes.PolarCharts.physicalChart_contDiff {a : ℝ} (ha : 0 < a) (j : Index) (Q : ℝ) : ContDiff ℝ (↑⊤) (physicalChart a j Q)

theorem NavierStokes.PolarCharts.physicalChart_finiteJets_uniform {a : ℝ} (ha : 0 < a) (b : ℝ) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (Q : ℝ), 0 < Q → ∀ (j : Index), ∀ k ≤ m, ∀ (p : Plane), (scalePlane Q) p ∈ Metric.closedBall 0 b → ‖iteratedFDeriv ℝ k (physicalChart a j Q) p‖ ≤ C * Q ^ (-↑k / 2)

Each physical derivative costs exactly the fixed half-power of Q. The constant is chosen before Q, the chart, and the evaluation point.

theorem NavierStokes.PolarCharts.rotate_smul (j : Index) (c : ℝ) (p : Plane) : rotate j (c • p) = c • rotate j p

theorem NavierStokes.PolarCharts.radius_smul {c : ℝ} (hc : 0 < c) (p : Plane) : radius (c • p) = c * radius p

theorem NavierStokes.PolarCharts.localChart_smul (j : Index) {c : ℝ} (hc : 0 < c) (p : Plane) : localChart j (c • p) = (c * (localChart j p).1, (localChart j p).2)

theorem NavierStokes.PolarCharts.scalePlane_eq_inv_sqrt {Q : ℝ} (hQ : 0 < Q) (p : Plane) : (scalePlane Q) p = (√Q)⁻¹ • p

theorem NavierStokes.PolarCharts.physicalChart_eq {a Q : ℝ} (ha : 0 < a) (hQ : 0 < Q) (j : Index) {p : Plane} (hp : (scalePlane Q) p ∈ chartDomain a j) : physicalChart a j Q p = (radius p / √Q, (localChart j p).2)

theorem NavierStokes.PolarCharts.physicalChart_inverse {a Q : ℝ} (ha : 0 < a) (hQ : 0 < Q) (j : Index) {p : Plane} (hp : (scalePlane Q) p ∈ chartDomain a j) : √Q • polar (physicalChart a j Q p) = p

theorem NavierStokes.PolarCharts.localChart_angle_difference (i j : Index) {p : Plane} (hi : 0 < (rotate i p).1) (hj : 0 < (rotate j p).1) : ∃ (n : ℤ), (localChart i p).2 - (localChart j p).2 = 2 * Real.pi * ↑n

Angles from two valid local inverse charts differ by an integer full turn.

theorem NavierStokes.PolarCharts.localChart_periodic_agree {V : Type u_1} (f : Plane → V) (hf : ∀ (r : ℝ), Function.Periodic (fun (θ : ℝ) => f (r, θ)) (2 * Real.pi)) (i j : Index) {p : Plane} (hi : 0 < (rotate i p).1) (hj : 0 < (rotate j p).1) : f (localChart i p) = f (localChart j p)

Any function periodic in its angular coordinate has the same chart value. This applies to integer angular harmonics, not to an unexponentiated phase.

theorem NavierStokes.PolarCharts.chart_periodic_agree {V : Type u_1} {a : ℝ} (ha : 0 < a) (f : Plane → V) (hf : ∀ (r : ℝ), Function.Periodic (fun (θ : ℝ) => f (r, θ)) (2 * Real.pi)) (i j : Index) {p : Plane} (hi : p ∈ chartDomain a i) (hj : p ∈ chartDomain a j) : f (chart a i p) = f (chart a j p)

theorem NavierStokes.PolarCharts.chart_periodic_eventuallyEq {V : Type u_1} {a : ℝ} (ha : 0 < a) (f : Plane → V) (hf : ∀ (r : ℝ), Function.Periodic (fun (θ : ℝ) => f (r, θ)) (2 * Real.pi)) (i j : Index) {p : Plane} (hi : p ∈ chartDomain a i) (hj : p ∈ chartDomain a j) : f ∘ chart a i =ᶠ[nhds p] f ∘ chart a j

theorem NavierStokes.PolarCharts.chart_periodic_jets_agree {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℝ} (ha : 0 < a) (f : Plane → V) (hf : ∀ (r : ℝ), Function.Periodic (fun (θ : ℝ) => f (r, θ)) (2 * Real.pi)) (i j : Index) {p : Plane} (hi : p ∈ chartDomain a i) (hj : p ∈ chartDomain a j) (k : ℕ) : iteratedFDeriv ℝ k (f ∘ chart a i) p = iteratedFDeriv ℝ k (f ∘ chart a j) p

@[reducible, inline]

abbrev NavierStokes.PhysicalGraphBounds.Plane : Type

Plane: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.PhysicalGraphBounds.Plane = (ℝ × ℝ)

noncomputable def NavierStokes.PhysicalGraphBounds.radialDirection : Plane

Radial direction, given by (1, 1 - Real.sqrt 2).

Equations

• NavierStokes.PhysicalGraphBounds.radialDirection = (1, 1 - √2)

noncomputable def NavierStokes.PhysicalGraphBounds.timeDirection : Plane

Time direction, given by (Real.sqrt 2 - 1, 1).

Equations

• NavierStokes.PhysicalGraphBounds.timeDirection = (√2 - 1, 1)

theorem NavierStokes.PhysicalGraphBounds.cover_radialDirection : SlotGeometry.cover radialDirection = ChartScales.Lambda • radialDirection

theorem NavierStokes.PhysicalGraphBounds.cover_timeDirection : SlotGeometry.cover timeDirection = ChartScales.Tg • timeDirection

theorem NavierStokes.PhysicalGraphBounds.cover_pow_radialDirection (i : ℕ) : (SlotGeometry.cover ^ i) radialDirection = ChartScales.Lambda ^ i • radialDirection

theorem NavierStokes.PhysicalGraphBounds.cover_pow_timeDirection (i : ℕ) : (SlotGeometry.cover ^ i) timeDirection = ChartScales.Tg ^ i • timeDirection

noncomputable def NavierStokes.PhysicalGraphBounds.radialProjection : ProblemStatement.SpaceTime →L[ℝ] Plane

Radial projection as an element of SpaceTime →L[ℝ] Plane.

Equations

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

@[simp]

theorem NavierStokes.PhysicalGraphBounds.radialProjection_apply (p : ProblemStatement.SpaceTime) : radialProjection p = (p.2.ofLp 0, p.2.ofLp 1)

theorem NavierStokes.PhysicalGraphBounds.norm_radialProjection_le : ‖radialProjection‖ ≤ 1

noncomputable def NavierStokes.PhysicalGraphBounds.radiusPower (d : ℝ) (y : Plane) : ℝ

Radius power, given by (y.1 ^ 2 + y.2 ^ 2) ^ (d / 2).

Equations

• NavierStokes.PhysicalGraphBounds.radiusPower d y = (y.1 ^ 2 + y.2 ^ 2) ^ (d / 2)

noncomputable def NavierStokes.PhysicalGraphBounds.radialProfile (d : ℝ) (y : Plane) : Plane

Radial profile, given by radiusPower d y • radialDirection.

Equations

• NavierStokes.PhysicalGraphBounds.radialProfile d y = NavierStokes.PhysicalGraphBounds.radiusPower d y • NavierStokes.PhysicalGraphBounds.radialDirection

theorem NavierStokes.PhysicalGraphBounds.radiusPower_eq (d : ℝ) (y : Plane) : radiusPower d y = √(y.1 ^ 2 + y.2 ^ 2) ^ d

theorem NavierStokes.PhysicalGraphBounds.sum_sq_pos {y : Plane} (hy : y ≠ 0) : 0 < y.1 ^ 2 + y.2 ^ 2

theorem NavierStokes.PhysicalGraphBounds.contDiffOn_radialProfile (d : ℝ) : ContDiffOn ℝ (↑⊤) (radialProfile d) {y : Plane | y ≠ 0}

theorem NavierStokes.PhysicalGraphBounds.radiusPower_smul (d : ℝ) {a : ℝ} (ha : 0 < a) (y : Plane) : radiusPower d (a • y) = a ^ d * radiusPower d y

noncomputable def NavierStokes.PhysicalGraphBounds.nativeGraph (h : ℝ) (n : ℕ) (p : ProblemStatement.SpaceTime) : Plane

The universal-cover representative of Y_i=J_g^i(v_r r^d+v_t t).

Equations

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

theorem NavierStokes.PhysicalGraphBounds.nativeGraph_eq (h : ℝ) (n : ℕ) (p : ProblemStatement.SpaceTime) : nativeGraph h n p = ChartScales.Lambda ^ ChartScales.nativeIndex h n • radialProfile (ChartScales.radialExponent h) (radialProjection p) + ChartScales.Tg ^ ChartScales.nativeIndex h n • p.1 • timeDirection

noncomputable def NavierStokes.PhysicalGraphBounds.scaledRadial (n : ℕ) : ProblemStatement.SpaceTime →L[ℝ] Plane

Scaled radial, given by ChartScales.Q n ^ (-(1 / 2 : ℝ)) • radialProjection.

Equations

• NavierStokes.PhysicalGraphBounds.scaledRadial n = NavierStokes.ChartScales.Q n ^ (-(1 / 2)) • NavierStokes.PhysicalGraphBounds.radialProjection

theorem NavierStokes.PhysicalGraphBounds.norm_scaledRadial_le (n : ℕ) : ‖scaledRadial n‖ ≤ ChartScales.Q n ^ (-(1 / 2))

theorem NavierStokes.PhysicalGraphBounds.unscale_radial (n : ℕ) (p : ProblemStatement.SpaceTime) : ChartScales.Q n ^ (1 / 2) • (scaledRadial n) p = radialProjection p

theorem NavierStokes.PhysicalGraphBounds.nativeGraph_normalized (h : ℝ) (n : ℕ) (p : ProblemStatement.SpaceTime) : nativeGraph h n p = ChartScales.radialCoefficient h n • radialProfile (ChartScales.radialExponent h) ((scaledRadial n) p) + ChartScales.Tg ^ ChartScales.nativeIndex h n • p.1 • timeDirection

noncomputable def NavierStokes.PhysicalGraphBounds.annulus (a b : ℝ) : Set Plane

A fixed compact transverse annulus in normalized Cartesian coordinates.

Equations

• NavierStokes.PhysicalGraphBounds.annulus a b = Metric.closedBall 0 b ∩ {y : NavierStokes.PhysicalGraphBounds.Plane | a ≤ ‖y‖}

theorem NavierStokes.PhysicalGraphBounds.isCompact_annulus (a b : ℝ) : IsCompact (annulus a b)

theorem NavierStokes.PhysicalGraphBounds.annulus_axisFree {a b : ℝ} (ha : 0 < a) : annulus a b ⊆ {y : Plane | y ≠ 0}

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

Compactness is used only for one fixed smooth profile on one fixed annulus.

theorem NavierStokes.PhysicalGraphBounds.norm_jet_comp_linear {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : F → G} {U : Set F} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) (L : E →L[ℝ] F) {x : E} (hx : L x ∈ U) (k : ℕ) : ‖iteratedFDeriv ℝ k (f ∘ ⇑L) x‖ ≤ ‖iteratedFDeriv ℝ k f (L x)‖ * ‖L‖ ^ k

Exact linear-rescaling estimate for actual higher derivatives on an open domain.

theorem NavierStokes.PhysicalGraphBounds.axisFree_open : IsOpen {y : Plane | y ≠ 0}

theorem NavierStokes.PhysicalGraphBounds.S_ge_one {n : ℕ} (hn : 1 ≤ n) : 1 ≤ ChartScales.S n

theorem NavierStokes.PhysicalGraphBounds.native_time_power_le {h : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1) {n : ℕ} (hn : 4 ≤ n) : ChartScales.Tg ^ ChartScales.nativeIndex h n ≤ ChartScales.Q n ^ (-2)

The actual floor index has a fixed time-frequency power bound.

theorem NavierStokes.PhysicalGraphBounds.native_radial_power_le {h : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1) {n : ℕ} (hn : 4 ≤ n) : ChartScales.radialCoefficient h n ≤ ChartScales.Q n ^ (-1)

A coarse fixed power controls the actual normalized radial graph frequency.

theorem NavierStokes.PhysicalGraphBounds.norm_scaledRadial_coarse_le (n : ℕ) : ‖scaledRadial n‖ ≤ ChartScales.Q n ^ (-1)

theorem NavierStokes.PhysicalGraphBounds.norm_positive_jet_linear_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) (x : E) {k : ℕ} (hk : 1 ≤ k) : ‖iteratedFDeriv ℝ k (⇑L) x‖ ≤ ‖L‖

noncomputable def NavierStokes.PhysicalGraphBounds.timeProfile : ProblemStatement.SpaceTime →L[ℝ] Plane

Time profile, given by (ContinuousLinearMap.fst ℝ ℝ Space).smulRight timeDirection.

Equations

• NavierStokes.PhysicalGraphBounds.timeProfile = (ContinuousLinearMap.fst ℝ ℝ NavierStokes.ProblemStatement.Space).smulRight NavierStokes.PhysicalGraphBounds.timeDirection

@[simp]

theorem NavierStokes.PhysicalGraphBounds.timeProfile_apply (p : ProblemStatement.SpaceTime) : timeProfile p = p.1 • timeDirection

theorem NavierStokes.PhysicalGraphBounds.norm_timeProfile_le : ‖timeProfile‖ ≤ ‖timeDirection‖

theorem NavierStokes.PhysicalGraphBounds.timeProfile_jet_bound (p : ProblemStatement.SpaceTime) (ht : |p.1| ≤ 1) (k : ℕ) : ‖iteratedFDeriv ℝ k (⇑timeProfile) p‖ ≤ ‖timeDirection‖

theorem NavierStokes.PhysicalGraphBounds.contDiffAt_nativeGraph (h : ℝ) (n : ℕ) {p : ProblemStatement.SpaceTime} (hp : radialProjection p ≠ 0) : ContDiffAt ℝ (↑⊤) (nativeGraph h n) p

theorem NavierStokes.PhysicalGraphBounds.scaledRadial_ne_zero {n : ℕ} {p : ProblemStatement.SpaceTime} (hp : (scaledRadial n) p ≠ 0) : radialProjection p ≠ 0

theorem NavierStokes.PhysicalGraphBounds.nativeGraph_jet_bound {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1) (ha : 0 < a) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ (p : ProblemStatement.SpaceTime), (scaledRadial n) p ∈ annulus a b → |p.1| ≤ 1 → ∀ k ≤ m, ‖iteratedFDeriv ℝ k (nativeGraph h n) p‖ ≤ C * ChartScales.Q n ^ (-(↑m + 2))

The bound is uniform in the dyadic band and contains no stage index. The compact annulus supplies constants; all powers come from the actual covering index and the actual physical rescaling.

@[reducible, inline]

abbrev NavierStokes.PhysicalGraphBounds.ChartPoint : Type

Chart point: an abbreviation for ℝ × (ℝ × (ℝ × ℝ)).

Equations

• NavierStokes.PhysicalGraphBounds.ChartPoint = (ℝ × ℝ × ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.PhysicalGraphBounds.LiftPoint : Type

Lift point: an abbreviation for ChartPoint × Plane.

Equations

• NavierStokes.PhysicalGraphBounds.LiftPoint = (NavierStokes.PhysicalGraphBounds.ChartPoint × NavierStokes.PhysicalGraphBounds.Plane)

noncomputable def NavierStokes.PhysicalGraphBounds.coordinateProjection (j : Fin 3) : ProblemStatement.SpaceTime →L[ℝ] ℝ

Coordinate projection, given by (AxisymmetricFields.projection j).comp (ContinuousLinearMap.snd ℝ ℝ Space).

Equations

• NavierStokes.PhysicalGraphBounds.coordinateProjection j = NavierStokes.AxisymmetricFields.projection j ∘SL ContinuousLinearMap.snd ℝ ℝ NavierStokes.ProblemStatement.Space

@[simp]

theorem NavierStokes.PhysicalGraphBounds.coordinateProjection_apply (j : Fin 3) (p : ProblemStatement.SpaceTime) : (coordinateProjection j) p = p.2.ofLp j

noncomputable def NavierStokes.PhysicalGraphBounds.chartLinear (h : ℝ) (n : ℕ) : ProblemStatement.SpaceTime →L[ℝ] ChartPoint

Cartesian form of the exact chart (T, R cos θ, R sin θ, Z).

Equations

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

@[simp]

theorem NavierStokes.PhysicalGraphBounds.chartLinear_apply (h : ℝ) (n : ℕ) (p : ProblemStatement.SpaceTime) : (chartLinear h n) p = (-ChartScales.Q n ^ (-1) * p.1, ChartScales.Q n ^ (-(1 / 2)) * p.2.ofLp 0, ChartScales.Q n ^ (-(1 / 2)) * p.2.ofLp 1, ChartScales.Q n ^ (-CoordinateAlgebra.D h) * p.2.ofLp 2)

noncomputable def NavierStokes.PhysicalGraphBounds.physicalChart (h : ℝ) (n : ℕ) (p : ProblemStatement.SpaceTime) : ChartPoint

Physical chart, given by chartLinear h n p + (ChartScales.Q n ^ (-1 : ℝ), 0).

Equations

• NavierStokes.PhysicalGraphBounds.physicalChart h n p = (NavierStokes.PhysicalGraphBounds.chartLinear h n) p + (NavierStokes.ChartScales.Q n ^ (-1), 0)

theorem NavierStokes.PhysicalGraphBounds.physicalChart_time (h : ℝ) (n : ℕ) (p : ProblemStatement.SpaceTime) : (physicalChart h n p).1 = (1 - p.1) / ChartScales.Q n

theorem NavierStokes.PhysicalGraphBounds.norm_chartLinear_le {h : ℝ} (hh : 0 ≤ h) (n : ℕ) : ‖chartLinear h n‖ ≤ ChartScales.Q n ^ (-1)

theorem NavierStokes.PhysicalGraphBounds.physicalChart_smooth (h : ℝ) (n : ℕ) : ContDiff ℝ (↑⊤) (physicalChart h n)

theorem NavierStokes.PhysicalGraphBounds.physicalChart_jet_bound {h : ℝ} (hh : 0 ≤ h) (n : ℕ) (p : ProblemStatement.SpaceTime) {k : ℕ} (hk : 1 ≤ k) : ‖iteratedFDeriv ℝ k (physicalChart h n) p‖ ≤ ChartScales.Q n ^ (-1)

theorem NavierStokes.PhysicalGraphBounds.iteratedFDeriv_pair {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → F} {g : E → G} {x : E} {k : ℕ} (hf : ContDiffAt ℝ (↑k) f x) (hg : ContDiffAt ℝ (↑k) g x) : iteratedFDeriv ℝ k (fun (y : E) => (f y, g y)) x = (iteratedFDeriv ℝ k f x).prod (iteratedFDeriv ℝ k g x)

noncomputable def NavierStokes.PhysicalGraphBounds.physicalLift (h : ℝ) (n : ℕ) (p : ProblemStatement.SpaceTime) : LiftPoint

Actual graph restriction together with the exact physical chart scaling.

Equations

• NavierStokes.PhysicalGraphBounds.physicalLift h n p = (NavierStokes.PhysicalGraphBounds.physicalChart h n p, NavierStokes.PhysicalGraphBounds.nativeGraph h n p)

theorem NavierStokes.PhysicalGraphBounds.physicalLift_smooth (h : ℝ) (n : ℕ) : ContDiffOn ℝ (↑⊤) (physicalLift h n) {p : ProblemStatement.SpaceTime | radialProjection p ≠ 0}

theorem NavierStokes.PhysicalGraphBounds.physicalLift_positive_jet_bound {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ (p : ProblemStatement.SpaceTime), (scaledRadial n) p ∈ annulus a b → |p.1| ≤ 1 → ∀ (k : ℕ), 1 ≤ k → k ≤ m → ‖iteratedFDeriv ℝ k (physicalLift h n) p‖ ≤ C * ChartScales.Q n ^ (-(↑m + 2))

noncomputable def NavierStokes.PhysicalGraphBounds.graphLoss (m : ℕ) : ℝ

The fixed derivative loss for graph composition; it depends on jet order alone.

Equations

• NavierStokes.PhysicalGraphBounds.graphLoss m = ↑m * (↑m + 2)

theorem NavierStokes.PhysicalGraphBounds.graphRestriction_jet_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ (p : ProblemStatement.SpaceTime), (scaledRadial n) p ∈ annulus a b → |p.1| ≤ 1 → ∀ (F : LiftPoint → E), ContDiff ℝ (↑⊤) F → ∀ (B : ℝ), 0 ≤ B → (∀ k ≤ m, ‖iteratedFDeriv ℝ k F (physicalLift h n p)‖ ≤ B) → ‖iteratedFDeriv ℝ m (F ∘ physicalLift h n) p‖ ≤ C * B * ChartScales.Q n ^ (-graphLoss m)

A genuine all-order chain estimate for the concrete native graph. The stripped coefficient is an actual smooth function; its stage-dependent jet bound enters only multiplicatively.

noncomputable def NavierStokes.PhysicalGraphBounds.etaCoordinate : Plane →L[ℝ] ℝ

The dual coordinate along v_t in the manuscript's slot rectangle.

Equations

• NavierStokes.PhysicalGraphBounds.etaCoordinate = (1 + (√2 - 1) ^ 2)⁻¹ • ((√2 - 1) • ContinuousLinearMap.fst ℝ ℝ ℝ + ContinuousLinearMap.snd ℝ ℝ ℝ)

theorem NavierStokes.PhysicalGraphBounds.etaCoordinate_radial : etaCoordinate radialDirection = 0

theorem NavierStokes.PhysicalGraphBounds.etaCoordinate_time : etaCoordinate timeDirection = 1

theorem NavierStokes.PhysicalGraphBounds.etaCoordinate_nativeGraph (h : ℝ) (n : ℕ) (p : ProblemStatement.SpaceTime) : etaCoordinate (nativeGraph h n p) = ChartScales.Tg ^ ChartScales.nativeIndex h n * p.1

noncomputable def NavierStokes.PhysicalGraphBounds.slotTime (h : ℝ) (n : ℕ) (center : Plane) (r0 : ℝ) (p : ProblemStatement.SpaceTime) : ℝ

center includes the periodically reindexed lattice-copy translation.

Equations

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

theorem NavierStokes.PhysicalGraphBounds.slotTime_affine (h : ℝ) (n : ℕ) (center : Plane) (r0 : ℝ) (p : ProblemStatement.SpaceTime) : slotTime h n center r0 p = ChartScales.Q n ^ (-1 - h) * p.1 + (r0 - etaCoordinate center) / ChartScales.timeCoefficient h n

theorem NavierStokes.PhysicalGraphBounds.hasFDerivAt_slotTime (h : ℝ) (n : ℕ) (center : Plane) (r0 : ℝ) (p : ProblemStatement.SpaceTime) : HasFDerivAt (slotTime h n center r0) (ChartScales.Q n ^ (-1 - h) • ContinuousLinearMap.fst ℝ ℝ ProblemStatement.Space) p

theorem NavierStokes.PhysicalGraphBounds.slotTime_derivative (h : ℝ) (n : ℕ) (center : Plane) (r0 : ℝ) (p v : ProblemStatement.SpaceTime) : (fderiv ℝ (slotTime h n center r0) p) v = ChartScales.Q n ^ (-1 - h) * v.1

theorem NavierStokes.PhysicalGraphBounds.slotTime_spatial_derivative (h : ℝ) (n : ℕ) (center : Plane) (r0 : ℝ) (p : ProblemStatement.SpaceTime) (v : ProblemStatement.Space) : (fderiv ℝ (slotTime h n center r0) p) (0, v) = 0

theorem NavierStokes.PhysicalGraphBounds.carrier_upper {h : ℝ} (hh : 0 ≤ h) (n : ℕ) : ↑(ChartScales.carrier h n) ≤ 2 * ChartScales.Q n ^ (-h / 2)

Exact integer rounding gives a uniform upper carrier power.

noncomputable def NavierStokes.PhysicalGraphBounds.phaseFactor (c : ℝ) : ℂ

Phase factor, given by (c : ℂ) * Complex.I.

Equations

• NavierStokes.PhysicalGraphBounds.phaseFactor c = ↑c * Complex.I

noncomputable def NavierStokes.PhysicalGraphBounds.character (c t : ℝ) : ℂ

Character, given by Complex.exp (phaseFactor c * (t : ℂ)).

Equations

• NavierStokes.PhysicalGraphBounds.character c t = Complex.exp (NavierStokes.PhysicalGraphBounds.phaseFactor c * ↑t)

@[simp]

theorem NavierStokes.PhysicalGraphBounds.norm_character (c t : ℝ) : ‖character c t‖ = 1

theorem NavierStokes.PhysicalGraphBounds.character_smooth (c : ℝ) : ContDiff ℝ (↑⊤) (character c)

theorem NavierStokes.PhysicalGraphBounds.hasDerivAt_character (c t : ℝ) : HasDerivAt (character c) (phaseFactor c * character c t) t

theorem NavierStokes.PhysicalGraphBounds.iteratedDeriv_character (c : ℝ) (m : ℕ) : iteratedDeriv m (character c) = fun (t : ℝ) => phaseFactor c ^ m * character c t

theorem NavierStokes.PhysicalGraphBounds.norm_character_jet (c : ℝ) (m : ℕ) (t : ℝ) : ‖iteratedFDeriv ℝ m (character c) t‖ = |c| ^ m

Every carrier derivative is computed exactly, including derivative order zero.

theorem NavierStokes.PhysicalGraphBounds.rounded_carrier_jet_bound {h : ℝ} (hh : 0 ≤ h) (n m : ℕ) (j : ℤ) {H : ℝ} (hH : |↑j| ≤ H) (t : ℝ) : ‖iteratedFDeriv ℝ m (character (↑(ChartScales.carrier h n) * ↑j)) t‖ ≤ (2 * H) ^ m * ChartScales.Q n ^ (-(h * ↑m / 2))

Stage harmonics change the multiplicative constant, never the power loss.

theorem NavierStokes.PhysicalGraphBounds.pointwise_product_jet_bound {E : Type u_1} {A : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedRing A] [NormedAlgebra ℝ A] {f g : E → A} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (x : E) {m k : ℕ} (hk : k ≤ m) {P Q : ℝ} (hP : 0 ≤ P) (hQ : 0 ≤ Q) (hfb : ∀ i ≤ m, ‖iteratedFDeriv ℝ i f x‖ ≤ P) (hgb : ∀ i ≤ m, ‖iteratedFDeriv ℝ i g x‖ ≤ Q) : ‖iteratedFDeriv ℝ k (fun (y : E) => f y * g y) x‖ ≤ 2 ^ m * P * Q

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

The actual oscillatory exponential obeys a finite-jet bound in any smooth real phase. No formal carrier derivative is substituted for a real derivative.

theorem NavierStokes.PhysicalGraphBounds.carrier_graph_jet_bound {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ (p : ProblemStatement.SpaceTime), (scaledRadial n) p ∈ annulus a b → |p.1| ≤ 1 → ∀ (A : LiftPoint → ℂ) (Φ : LiftPoint → ℝ), ContDiff ℝ (↑⊤) A → ContDiff ℝ (↑⊤) Φ → ∀ (P B H : ℝ) (j : ℤ), 0 ≤ P → 1 ≤ B → |↑j| ≤ H → (∀ i ≤ m, ‖iteratedFDeriv ℝ i A (physicalLift h n p)‖ ≤ P) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i Φ (physicalLift h n p)‖ ≤ B) → ‖iteratedFDeriv ℝ m ((fun (y : LiftPoint) => A y * character (↑(ChartScales.carrier h n) * ↑j) (Φ y)) ∘ physicalLift h n) p‖ ≤ C * P * B ^ m * (1 + 2 * H) ^ m * ChartScales.Q n ^ (-(graphLoss m + h * ↑m / 2))

Combining amplitude, the actual rounded carrier, and the actual native graph gives a physical loss independent of the harmonic cutoff H.

theorem NavierStokes.PhysicalGraphBounds.comparable_rpow {Q q : ℝ} (hQ : 0 < Q) (hq : 0 < q) (hlo : q / 2 ≤ Q) (hhi : Q ≤ 2 * q) (e : ℝ) : Q ^ e ≤ 2 ^ |e| * q ^ e

Every real power transfers across the actual factor-two dyadic overlap. Its exponent can contain the stage gain; only the constant changes.

theorem NavierStokes.PhysicalGraphBounds.slow_power_absorption (a : ℝ) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), ChartScales.S n ^ a ≤ C * ChartScales.Q n ^ (-1)

Arbitrary fixed powers of the slow scale can be absorbed with one fixed power loss; the constant may depend on the slow power.

theorem NavierStokes.PhysicalGraphBounds.stripped_class_physical_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (m : ℕ) (g d A : ℝ) (hA : 0 ≤ A) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ (p : ProblemStatement.SpaceTime), (scaledRadial n) p ∈ annulus a b → |p.1| ≤ 1 → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ∀ (F : LiftPoint → E), ContDiff ℝ (↑⊤) F → (∀ i ≤ m, ‖iteratedFDeriv ℝ i F (physicalLift h n p)‖ ≤ A * ChartScales.Q n ^ g * ChartScales.S n ^ d) → ‖iteratedFDeriv ℝ m (F ∘ physicalLift h n) p‖ ≤ C * q ^ (g - (graphLoss m + 1))

A stripped coefficient class with arbitrary stage-dependent slow powers has a fixed physical loss graphLoss m + 1 on dyadic active supports.

theorem NavierStokes.PhysicalGraphBounds.norm_jet_const_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (x : E) (c : ℝ) (k : ℕ) : ‖iteratedFDeriv ℝ k (fun (y : E) => c * f y) x‖ = |c| * ‖iteratedFDeriv ℝ k f x‖

theorem NavierStokes.PhysicalGraphBounds.linear_jet_bound {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) (x : E) {M N : ℝ} (hM : 1 ≤ M) (hx : ‖x‖ ≤ M) (hN : 0 ≤ N) (hL : ‖L‖ ≤ N) (k : ℕ) : ‖iteratedFDeriv ℝ k (⇑L) x‖ ≤ N * M

theorem NavierStokes.PhysicalGraphBounds.norm_fstCLM_le (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : ‖ContinuousLinearMap.fst ℝ E F‖ ≤ 1

theorem NavierStokes.PhysicalGraphBounds.norm_sndCLM_le (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : ‖ContinuousLinearMap.snd ℝ E F‖ ≤ 1

theorem NavierStokes.PhysicalGraphBounds.jet_comp_linear_bound {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : F → G} (hf : ContDiff ℝ (↑⊤) f) (L : E →L[ℝ] F) (hL : ‖L‖ ≤ 1) (x : E) {B : ℝ} (hB : 0 ≤ B) (m : ℕ) (hb : ∀ k ≤ m, ‖iteratedFDeriv ℝ k f (L x)‖ ≤ B) (k : ℕ) : k ≤ m → ‖iteratedFDeriv ℝ k (f ∘ ⇑L) x‖ ≤ B

@[reducible, inline]

abbrev NavierStokes.PhysicalGraphBounds.Slot : Type

Slot: an abbreviation for PhaseCalculus.Slot.

Equations

• NavierStokes.PhysicalGraphBounds.Slot = NavierStokes.PhaseCalculus.Slot

@[reducible, inline]

abbrev NavierStokes.PhysicalGraphBounds.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.PhysicalGraphBounds.Slow = NavierStokes.PhaseCalculus.Slow

noncomputable def NavierStokes.PhysicalGraphBounds.slotR : Slot →L[ℝ] ℝ

Slot R, given by (ContinuousLinearMap.fst ℝ ℝ (ℝ × ℝ)).comp (ContinuousLinearMap.fst ℝ Slow (ℝ × ℝ)).

Equations

• NavierStokes.PhysicalGraphBounds.slotR = ContinuousLinearMap.fst ℝ ℝ (ℝ × ℝ) ∘SL ContinuousLinearMap.fst ℝ NavierStokes.PhysicalGraphBounds.Slow (ℝ × ℝ)

noncomputable def NavierStokes.PhysicalGraphBounds.slotZ : Slot →L[ℝ] ℝ

Slot Z, given by (ContinuousLinearMap.fst ℝ ℝ ℝ).comp ((ContinuousLinearMap.snd ℝ ℝ (ℝ × ℝ)).comp (ContinuousLinearMap.fst ℝ Slow (ℝ × ℝ))).

Equations

• NavierStokes.PhysicalGraphBounds.slotZ = ContinuousLinearMap.fst ℝ ℝ ℝ ∘SL ContinuousLinearMap.snd ℝ ℝ (ℝ × ℝ) ∘SL ContinuousLinearMap.fst ℝ NavierStokes.PhysicalGraphBounds.Slow (ℝ × ℝ)

noncomputable def NavierStokes.PhysicalGraphBounds.slotTheta : Slot →L[ℝ] ℝ

Slot theta, given by (ContinuousLinearMap.fst ℝ ℝ ℝ).comp (ContinuousLinearMap.snd ℝ Slow (ℝ × ℝ)).

Equations

• NavierStokes.PhysicalGraphBounds.slotTheta = ContinuousLinearMap.fst ℝ ℝ ℝ ∘SL ContinuousLinearMap.snd ℝ NavierStokes.PhysicalGraphBounds.Slow (ℝ × ℝ)

noncomputable def NavierStokes.PhysicalGraphBounds.slotV : Slot →L[ℝ] ℝ

Slot V, given by (ContinuousLinearMap.snd ℝ ℝ ℝ).comp (ContinuousLinearMap.snd ℝ Slow (ℝ × ℝ)).

Equations

• NavierStokes.PhysicalGraphBounds.slotV = ContinuousLinearMap.snd ℝ ℝ ℝ ∘SL ContinuousLinearMap.snd ℝ NavierStokes.PhysicalGraphBounds.Slow (ℝ × ℝ)

theorem NavierStokes.PhysicalGraphBounds.norm_slotV_le : ‖slotV‖ ≤ 1

noncomputable def NavierStokes.PhysicalGraphBounds.phaseLinear (ε p pz x0 : ℝ) : Slot →L[ℝ] ℝ

Phase linear, given by p • slotTheta + (pz / ε) • slotZ + x0 • slotR.

Equations

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

theorem NavierStokes.PhysicalGraphBounds.norm_phaseLinear_le (ε p pz x0 : ℝ) : ‖phaseLinear ε p pz x0‖ ≤ |p| + |pz / ε| + |x0|

theorem NavierStokes.PhysicalGraphBounds.phase_slot_jet_bound (ε p pz x0 : ℝ) {F G : Slow → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (q : Slot) (m : ℕ) {M B : ℝ} (hM : 1 ≤ M) (hq : ‖q‖ ≤ M) (hB : 0 ≤ B) (hFb : ∀ k ≤ m, ‖iteratedFDeriv ℝ k F q.1‖ ≤ B) (hGb : ∀ k ≤ m, ‖iteratedFDeriv ℝ k G q.1‖ ≤ B) (k : ℕ) : k ≤ m → ‖iteratedFDeriv ℝ k (PhaseCalculus.phase ε p pz x0 F G) q‖ ≤ (|p| + |pz / ε| + |x0|) * M + 2 ^ m * M * ((|p| + |pz|) * B)

All jets of the exact phase (26) are bounded directly from genuine base profile jets. The only inverse fast scale is the displayed pz/ε term.

theorem NavierStokes.PhysicalGraphBounds.pointwise_composition_jet_bound {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → F} {g : F → G} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (x : E) (m : ℕ) {B D : ℝ} (hB : 0 ≤ B) (hD : 1 ≤ D) (hgb : ∀ i ≤ m, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ B) (hfb : ∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDeriv ℝ i f x‖ ≤ D) (k : ℕ) : k ≤ m → ‖iteratedFDeriv ℝ k (g ∘ f) x‖ ≤ ↑m.factorial * B * D ^ m

theorem NavierStokes.PhysicalGraphBounds.norm_jet_linear_comp {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → F} (hf : ContDiff ℝ (↑⊤) f) (L : F →L[ℝ] G) (x : E) (k : ℕ) : ‖iteratedFDeriv ℝ k (⇑L ∘ f) x‖ ≤ ‖L‖ * ‖iteratedFDeriv ℝ k f x‖

noncomputable def NavierStokes.PhysicalGraphBounds.liftXY : LiftPoint →L[ℝ] Plane

Lift XY as an element of LiftPoint →L[ℝ] Plane.

Equations

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

noncomputable def NavierStokes.PhysicalGraphBounds.liftZT : LiftPoint →L[ℝ] Plane

Lift ZT as an element of LiftPoint →L[ℝ] Plane.

Equations

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

@[simp]

theorem NavierStokes.PhysicalGraphBounds.liftXY_apply (y : LiftPoint) : liftXY y = (y.1.2.1, y.1.2.2.1)

@[simp]

theorem NavierStokes.PhysicalGraphBounds.liftZT_apply (y : LiftPoint) : liftZT y = (y.1.2.2.2, y.1.1)

theorem NavierStokes.PhysicalGraphBounds.norm_liftXY_le : ‖liftXY‖ ≤ 1

theorem NavierStokes.PhysicalGraphBounds.norm_liftZT_le : ‖liftZT‖ ≤ 1

noncomputable def NavierStokes.PhysicalGraphBounds.embedPolar : Plane →L[ℝ] Slot

Embed polar, given by ((ContinuousLinearMap.fst ℝ ℝ ℝ).prod (0 : Plane →L[ℝ] Plane)).prod ((ContinuousLinearMap.snd ℝ ℝ ℝ).prod (0 : Plane →L[ℝ] ℝ)).

Equations

• NavierStokes.PhysicalGraphBounds.embedPolar = ((ContinuousLinearMap.fst ℝ ℝ ℝ).prod 0).prod ((ContinuousLinearMap.snd ℝ ℝ ℝ).prod 0)

theorem NavierStokes.PhysicalGraphBounds.norm_embedPolar_le : ‖embedPolar‖ ≤ 1

noncomputable def NavierStokes.PhysicalGraphBounds.slotLinear (ci : ℝ) : LiftPoint →L[ℝ] Slot

Slot linear as an element of LiftPoint →L[ℝ] Slot.

Equations

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

noncomputable def NavierStokes.PhysicalGraphBounds.slotConstant (ci : ℝ) (center : Plane) (r0 : ℝ) : Slot

Slot constant, given by ((0, (0, 0)), (0, (r0 - etaCoordinate center) / ci)).

Equations

• NavierStokes.PhysicalGraphBounds.slotConstant ci center r0 = ((0, 0, 0), 0, (r0 - NavierStokes.PhysicalGraphBounds.etaCoordinate center) / ci)

noncomputable def NavierStokes.PhysicalGraphBounds.slotMap (κ : Plane → Plane) (ci : ℝ) (center : Plane) (r0 : ℝ) (y : LiftPoint) : Slot

The actual native slot coordinates, using a chosen smooth polar chart.

Equations

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

theorem NavierStokes.PhysicalGraphBounds.slotMap_formula (κ : Plane → Plane) (ci : ℝ) (center : Plane) (r0 : ℝ) (y : LiftPoint) : slotMap κ ci center r0 y = (((κ (liftXY y)).1, y.1.2.2.2, y.1.1), (κ (liftXY y)).2, (etaCoordinate (y.2 - center) + r0) / ci)

theorem NavierStokes.PhysicalGraphBounds.slotMap_smooth {κ : Plane → Plane} (hκ : ContDiff ℝ (↑⊤) κ) (ci : ℝ) (center : Plane) (r0 : ℝ) : ContDiff ℝ (↑⊤) (slotMap κ ci center r0)

theorem NavierStokes.PhysicalGraphBounds.norm_slotLinear_le (ci : ℝ) : ‖slotLinear ci‖ ≤ 1 + |ci⁻¹| * ‖etaCoordinate‖

theorem NavierStokes.PhysicalGraphBounds.positive_jet_affine_bound {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) (c : F) (x : E) {k : ℕ} (hk : 1 ≤ k) : ‖iteratedFDeriv ℝ k (fun (y : E) => L y + c) x‖ ≤ ‖L‖

theorem NavierStokes.PhysicalGraphBounds.slotMap_positive_jet_bound {κ : Plane → Plane} (hκ : ContDiff ℝ (↑⊤) κ) (ci : ℝ) (center : Plane) (r0 : ℝ) (y : LiftPoint) (m : ℕ) {K : ℝ} (hK : 0 ≤ K) (hκb : ∀ i ≤ m, ‖iteratedFDeriv ℝ i κ (liftXY y)‖ ≤ K) (i : ℕ) : 1 ≤ i → i ≤ m → ‖iteratedFDeriv ℝ i (slotMap κ ci center r0) y‖ ≤ K + 1 + |ci⁻¹| * ‖etaCoordinate‖

theorem NavierStokes.PhysicalGraphBounds.slotMap_physical (κ : Plane → Plane) (h : ℝ) (n : ℕ) (center : Plane) (r0 : ℝ) (p : ProblemStatement.SpaceTime) : slotMap κ (ChartScales.timeCoefficient h n) center r0 (physicalLift h n p) = (((κ ((scaledRadial n) p)).1, ChartScales.Q n ^ (-CoordinateAlgebra.D h) * p.2.ofLp 2, (1 - p.1) / ChartScales.Q n), (κ ((scaledRadial n) p)).2, slotTime h n center r0 p)

noncomputable def NavierStokes.PhysicalGraphBounds.liftedPhase (κ : Plane → Plane) (h : ℝ) (n : ℕ) (center : Plane) (r0 p pz x0 : ℝ) (F G : Slow → ℝ) : LiftPoint → ℝ

Composition of (26) with the actual native slot map. This is the phase whose exponential is used in the physical carrier estimate.

Equations

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

theorem NavierStokes.PhysicalGraphBounds.liftedPhase_jet_bound {κ : Plane → Plane} (hκ : ContDiff ℝ (↑⊤) κ) (h : ℝ) (n : ℕ) (center : Plane) (r0 p pz x0 : ℝ) {F G : Slow → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (y : LiftPoint) (m : ℕ) {K M B : ℝ} (hK : 0 ≤ K) (hM : 1 ≤ M) (hB : 0 ≤ B) (hκb : ∀ i ≤ m, ‖iteratedFDeriv ℝ i κ (liftXY y)‖ ≤ K) (hpoint : ‖slotMap κ (ChartScales.timeCoefficient h n) center r0 y‖ ≤ M) (hFb : ∀ i ≤ m, ‖iteratedFDeriv ℝ i F (slotMap κ (ChartScales.timeCoefficient h n) center r0 y).1‖ ≤ B) (hGb : ∀ i ≤ m, ‖iteratedFDeriv ℝ i G (slotMap κ (ChartScales.timeCoefficient h n) center r0 y).1‖ ≤ B) (i : ℕ) : i ≤ m → ‖iteratedFDeriv ℝ i (liftedPhase κ h n center r0 p pz x0 F G) y‖ ≤ ↑m.factorial * ((|p| + |pz / ChartScales.epsilon h n| + |x0|) * M + 2 ^ m * M * ((|p| + |pz|) * B)) * (K + 1 + |(ChartScales.timeCoefficient h n)⁻¹| * ‖etaCoordinate‖) ^ m

theorem NavierStokes.PhysicalGraphBounds.slotMap_norm_bound (κ : Plane → Plane) (ci : ℝ) (center : Plane) (r0 : ℝ) (y : LiftPoint) {K Z V : ℝ} (hK : 0 ≤ K) (hZ : 0 ≤ Z) (hV : 0 ≤ V) (hk : ‖κ (liftXY y)‖ ≤ K) (hz : ‖liftZT y‖ ≤ Z) (hv : |(etaCoordinate (y.2 - center) + r0) / ci| ≤ V) : ‖slotMap κ ci center r0 y‖ ≤ K + Z + V

theorem NavierStokes.PhysicalGraphBounds.Q_inv_ge_one (n : ℕ) : 1 ≤ ChartScales.Q n ^ (-1)

theorem NavierStokes.PhysicalGraphBounds.epsilon_inv_le {h : ℝ} (hh : h ≤ 1) (n : ℕ) : (ChartScales.epsilon h n)⁻¹ ≤ ChartScales.Q n ^ (-1)

theorem NavierStokes.PhysicalGraphBounds.liftedPhase_power_bound {h K Z r0 P B d : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1) (hK : 1 ≤ K) (hZ : 0 ≤ Z) (hr0 : 0 ≤ r0) (hP : 1 ≤ P) (hB : 1 ≤ B) (hd : 0 ≤ d) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (κ : Plane → Plane), ContDiff ℝ (↑⊤) κ → ∀ (n : ℕ), 4 ≤ n → ∀ (center : Plane) (p pz x0 : ℝ), |p| ≤ P → |pz| ≤ P → |x0| ≤ P → ∀ (F G : Slow → ℝ), ContDiff ℝ (↑⊤) F → ContDiff ℝ (↑⊤) G → ∀ (y : LiftPoint), (∀ i ≤ m, ‖iteratedFDeriv ℝ i κ (liftXY y)‖ ≤ K) → ‖liftZT y‖ ≤ Z → |etaCoordinate (y.2 - center)| ≤ r0 → (∀ i ≤ m, ‖iteratedFDeriv ℝ i F (slotMap κ (ChartScales.timeCoefficient h n) center r0 y).1‖ ≤ B * ChartScales.S n ^ d) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i G (slotMap κ (ChartScales.timeCoefficient h n) center r0 y).1‖ ≤ B * ChartScales.S n ^ d) → ∀ i ≤ m, ‖iteratedFDeriv ℝ i (liftedPhase κ h n center r0 p pz x0 F G) y‖ ≤ C * ChartScales.S n ^ (d + ↑m + 1) * ChartScales.Q n ^ (-1)

The exact phase (26) has one fixed inverse-Q loss. The integer degree of the slow factor may grow with the base profile class; it affects no power of Q. Slot translations and the choice of polar chart are uniform.

noncomputable def NavierStokes.PhysicalGraphBounds.waveLoss (h : ℝ) (m : ℕ) : ℝ

Wave loss, given by graphLoss m + (m : ℝ) + h * (m : ℝ) / 2 + 1.

Equations

• NavierStokes.PhysicalGraphBounds.waveLoss h m = NavierStokes.PhysicalGraphBounds.graphLoss m + ↑m + h * ↑m / 2 + 1

theorem NavierStokes.PhysicalGraphBounds.carrier_weight_identity {q S : ℝ} (hq : 0 < q) (hS : 0 < S) (C A B H g d e E : ℝ) (m : ℕ) : C * (A * q ^ g * S ^ d) * (B * S ^ e * q ^ (-1)) ^ m * (1 + 2 * H) ^ m * q ^ (-E) = C * A * B ^ m * (1 + 2 * H) ^ m * S ^ (d + e * ↑m) * q ^ (g - E - ↑m)

theorem NavierStokes.PhysicalGraphBounds.carrier_class_physical_bound {h a b : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (m : ℕ) (g d e A B H : ℝ) (hA : 0 ≤ A) (hB : 1 ≤ B) (he : 0 ≤ e) (hH : 0 ≤ H) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ (p : ProblemStatement.SpaceTime), (scaledRadial n) p ∈ annulus a b → |p.1| ≤ 1 → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ∀ (amp : LiftPoint → ℂ) (Φ : LiftPoint → ℝ) (j : ℤ), ContDiff ℝ (↑⊤) amp → ContDiff ℝ (↑⊤) Φ → |↑j| ≤ H → (∀ i ≤ m, ‖iteratedFDeriv ℝ i amp (physicalLift h n p)‖ ≤ A * ChartScales.Q n ^ g * ChartScales.S n ^ d) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i Φ (physicalLift h n p)‖ ≤ B * ChartScales.S n ^ e * ChartScales.Q n ^ (-1)) → ‖iteratedFDeriv ℝ m ((fun (y : LiftPoint) => amp y * character (↑(ChartScales.carrier h n) * ↑j) (Φ y)) ∘ physicalLift h n) p‖ ≤ C * q ^ (g - waveLoss h m)

The complete fixed loss for waves with the exact carrier frequency. Amplitude gain g, harmonic cutoff H, and slow degrees d,e affect only the final constant. The phase class is supplied by liftedPhase_power_bound.

theorem NavierStokes.PhysicalGraphBounds.physical_polar_chart_available {a b : ℝ} (ha : 0 < a) (m : ℕ) : ∃ (K : ℝ), 1 ≤ K ∧ ∀ (n : ℕ) (p : ProblemStatement.SpaceTime), (scaledRadial n) p ∈ annulus a b → ∃ (j : PolarCharts.Index), (scaledRadial n) p ∈ PolarCharts.sector a b j ∧ ContDiff ℝ (↑⊤) (PolarCharts.chart a j) ∧ (∀ k ≤ m, ‖iteratedFDeriv ℝ k (PolarCharts.chart a j) ((scaledRadial n) p)‖ ≤ K) ∧ PolarCharts.polar (PolarCharts.chart a j ((scaledRadial n) p)) = (scaledRadial n) p

The four actual polar chart extensions supply one common constant for all normalized Cartesian phase derivatives; a sector always exists.

theorem NavierStokes.PhysicalGraphBounds.liftXY_physicalLift (h : ℝ) (n : ℕ) (p : ProblemStatement.SpaceTime) : liftXY (physicalLift h n p) = (scaledRadial n) p

theorem NavierStokes.PhysicalGraphBounds.liftedPhase_smooth {κ : Plane → Plane} (hκ : ContDiff ℝ (↑⊤) κ) (h : ℝ) (n : ℕ) (center : Plane) (r0 p pz x0 : ℝ) {F G : Slow → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) : ContDiff ℝ (↑⊤) (liftedPhase κ h n center r0 p pz x0 F G)

theorem NavierStokes.PhysicalGraphBounds.character_phase_eq_harmonic (k : ℝ) (j : ℤ) (ε p pz x0 : ℝ) (F G : Slow → ℝ) (s : Slot) : character (k * ↑j) (PhaseCalculus.phase ε p pz x0 F G s) = PhaseCalculus.harmonic k j ε p pz x0 F G s

theorem NavierStokes.PhysicalGraphBounds.liftedPhase_physical_formula {a b : ℝ} (ha : 0 < a) (chart : PolarCharts.Index) (h : ℝ) (n : ℕ) (center : Plane) (r0 p pz x0 : ℝ) (F G : Slow → ℝ) (w : ProblemStatement.SpaceTime) (hw : (scaledRadial n) w ∈ PolarCharts.sector a b chart) : have R := PolarCharts.radius ((scaledRadial n) w); have θ := Real.arctan ((PolarCharts.rotate chart ((scaledRadial n) w)).2 / (PolarCharts.rotate chart ((scaledRadial n) w)).1) + PolarCharts.offset chart; have Z := ChartScales.Q n ^ (-CoordinateAlgebra.D h) * w.2.ofLp 2; have T := (1 - w.1) / ChartScales.Q n; liftedPhase (PolarCharts.chart a chart) h n center r0 p pz x0 F G (physicalLift h n w) = p * θ + pz / ChartScales.epsilon h n * Z + x0 * R - slotTime h n center r0 w * (p * F (R, Z, T) + pz * G (R, Z, T))

On a covering sector, the phase is the literal Cartesian realization of (26), with R=√(x²+y²)/√Q and an actual local arctangent angle.

theorem NavierStokes.PhysicalGraphBounds.native_carrier_physical_bound {h a b Z r0 P B dBase : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 2) (ha : 0 < a) (hZ : 0 ≤ Z) (hr0 : 0 ≤ r0) (hP : 1 ≤ P) (hB : 1 ≤ B) (hdBase : 0 ≤ dBase) (m : ℕ) (g dAmp A H : ℝ) (hA : 0 ≤ A) (hH : 0 ≤ H) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), 4 ≤ n → ∀ (w : ProblemStatement.SpaceTime), (scaledRadial n) w ∈ annulus a b → |w.1| ≤ 1 → ‖liftZT (physicalLift h n w)‖ ≤ Z → ∀ (q : ℝ), 0 < q → q / 2 ≤ ChartScales.Q n → ChartScales.Q n ≤ 2 * q → ∀ (chart : PolarCharts.Index) (center : Plane) (p pz x0 : ℝ), |p| ≤ P → |pz| ≤ P → |x0| ≤ P → |etaCoordinate (nativeGraph h n w - center)| ≤ r0 → ∀ (amp : LiftPoint → ℂ) (F G : Slow → ℝ) (j : ℤ), ContDiff ℝ (↑⊤) amp → ContDiff ℝ (↑⊤) F → ContDiff ℝ (↑⊤) G → |↑j| ≤ H → (∀ i ≤ m, ‖iteratedFDeriv ℝ i amp (physicalLift h n w)‖ ≤ A * ChartScales.Q n ^ g * ChartScales.S n ^ dAmp) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i F (slotMap (PolarCharts.chart a chart) (ChartScales.timeCoefficient h n) center r0 (physicalLift h n w)).1‖ ≤ B * ChartScales.S n ^ dBase) → (∀ i ≤ m, ‖iteratedFDeriv ℝ i G (slotMap (PolarCharts.chart a chart) (ChartScales.timeCoefficient h n) center r0 (physicalLift h n w)).1‖ ≤ B * ChartScales.S n ^ dBase) → ‖iteratedFDeriv ℝ m ((fun (y : LiftPoint) => amp y * character (↑(ChartScales.carrier h n) * ↑j) (liftedPhase (PolarCharts.chart a chart) h n center r0 p pz x0 F G y)) ∘ physicalLift h n) w‖ ≤ C * q ^ (g - waveLoss h m)

All polar branches share the same physical bound for the actual phase (26). No derivative hypothesis on the phase or on the native graph occurs: only the stripped amplitude and base profiles have class hypotheses.