The first slow-order stress at the terminal edge

The source is the angular axial-viscosity term. Its primitive is the actual backward integral with weight R². The coefficient chart is (η,δ), including both endpoints η=±1; its heat carrier uses the genuine smooth heat extension.

noncomputable def NavierStokes.SlowFirstOrderEdge.beta (d : OutgoingTail.TailData) (η : ℝ) : ℝ

Beta, given by (2 * CoordinateAlgebra.D d.h * η * profileChi d η - (1 - η ^ 2) * deriv (profileChi d) η) / profileL d η.

Equations

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

theorem NavierStokes.SlowFirstOrderEdge.beta_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (beta d)

noncomputable def NavierStokes.SlowFirstOrderEdge.taperSecondFactor (d : OutgoingTail.TailData) (x : ℝ) : ℝ

Taper second factor, given by `-8 * taperSlopeFactor d x + 3 * x ^ 2 * taperSlopeFactor d x

• x ^ 3 * deriv (taperSlopeFactor d) x`.

Equations

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

theorem NavierStokes.SlowFirstOrderEdge.taperSecondFactor_contDiff (d : OutgoingTail.TailData) : ContDiff ℝ (↑⊤) (taperSecondFactor d)

theorem NavierStokes.SlowFirstOrderEdge.taperSecond_factorization (d : OutgoingTail.TailData) (x : ℝ) : deriv (OutgoingTail.tailShapeDeriv d) (3 - x) = FlatCutoff.edge 4 x / x ^ 6 * taperSecondFactor d x

noncomputable def NavierStokes.SlowFirstOrderEdge.profileSource (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

The normalized negative axial-viscosity source, before radial integration.

Equations

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

noncomputable def NavierStokes.SlowFirstOrderEdge.sourceFactor (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Source factor, given by -profileCarrier C d y0 y * (profileChi d y.1 ^ 2 * taperSecondFactor d y.2 + beta d y.1 * y.2 ^ 3 * taperSlopeFactor d y.2).

Equations

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

theorem NavierStokes.SlowFirstOrderEdge.sourceFactor_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (sourceFactor C d y0)

theorem NavierStokes.SlowFirstOrderEdge.profileSource_factorization (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : profileSource C d y0 y = FlatCutoff.edge 4 y.2 / y.2 ^ 6 * sourceFactor C d y0 y

theorem NavierStokes.SlowFirstOrderEdge.profileSource_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (profileSource C d y0)

noncomputable def NavierStokes.SlowFirstOrderEdge.primitiveCoefficient (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Primitive coefficient, given by (profileRadius y0 y.2 ^ 3 / 2) * sourceFactor C d y0 y.

Equations

• NavierStokes.SlowFirstOrderEdge.primitiveCoefficient C d y0 y = NavierStokes.TerminalEdgeFactor.profileRadius y0 y.2 ^ 3 / 2 * NavierStokes.SlowFirstOrderEdge.sourceFactor C d y0 y

theorem NavierStokes.SlowFirstOrderEdge.primitiveCoefficient_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (primitiveCoefficient C d y0)

noncomputable def NavierStokes.SlowFirstOrderEdge.radialSource (C : ℝ) (d : OutgoingTail.TailData) (y0 η R : ℝ) : ℝ

The source in the positive normalized radial variable R=√(2X).

Equations

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

noncomputable def NavierStokes.SlowFirstOrderEdge.radialStress (C : ℝ) (d : OutgoingTail.TailData) (y0 η R : ℝ) : ℝ

The genuine backward weighted radial primitive, with the stress sign convention.

Equations

• NavierStokes.SlowFirstOrderEdge.radialStress C d y0 η R = NavierStokes.TerminalStress.backwardStress (NavierStokes.SlowFirstOrderEdge.radialSource C d y0 η) R

noncomputable def NavierStokes.SlowFirstOrderEdge.profileStress (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Profile stress, given by radialStress C d y0 y.1 (profileRadius y0 y.2).

Equations

• NavierStokes.SlowFirstOrderEdge.profileStress C d y0 y = NavierStokes.SlowFirstOrderEdge.radialStress C d y0 y.1 (NavierStokes.TerminalEdgeFactor.profileRadius y0 y.2)

noncomputable def NavierStokes.SlowFirstOrderEdge.stressFactor (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : ℝ

Stress factor, given by ParametricFlatFactor.factor 4 6 (primitiveCoefficient C d y0) y / profileRadius y0 y.2 ^ 2.

Equations

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

theorem NavierStokes.SlowFirstOrderEdge.stressFactor_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (stressFactor C d y0)

theorem NavierStokes.SlowFirstOrderEdge.profileRadius_eq (y0 x : ℝ) : TerminalEdgeFactor.profileRadius y0 x = TerminalEdgeFactor.profileRadius y0 0 * Real.exp (-x / 2)

theorem NavierStokes.SlowFirstOrderEdge.profileRadius_edgeCoordinate (y0 : ℝ) {R : ℝ} (hR : 0 < R) : TerminalEdgeFactor.profileRadius y0 (TerminalEdgeFactor.edgeCoordinate (TerminalEdgeFactor.profileRadius y0 0) R) = R

theorem NavierStokes.SlowFirstOrderEdge.edgeCoordinate_profileRadius (y0 x : ℝ) : TerminalEdgeFactor.edgeCoordinate (TerminalEdgeFactor.profileRadius y0 0) (TerminalEdgeFactor.profileRadius y0 x) = x

theorem NavierStokes.SlowFirstOrderEdge.radialSource_weight (C : ℝ) (d : OutgoingTail.TailData) (y0 η : ℝ) {R : ℝ} (hR : 0 < R) : R ^ 2 * radialSource C d y0 η R = TerminalEdgeFactor.radialFlatDensity 4 6 (fun (x : ℝ) => primitiveCoefficient C d y0 (η, x)) (TerminalEdgeFactor.profileRadius y0 0) R

theorem NavierStokes.SlowFirstOrderEdge.radialSource_weight_integrable (C : ℝ) (d : OutgoingTail.TailData) (y0 η : ℝ) {R : ℝ} (hR : 0 < R) : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * radialSource C d y0 η u) (Set.Ioi R) MeasureTheory.volume

theorem NavierStokes.SlowFirstOrderEdge.radialStress_eq_primitive (C : ℝ) (d : OutgoingTail.TailData) (y0 η : ℝ) {R : ℝ} (hR : 0 < R) : radialStress C d y0 η R = ParametricFlatFactor.primitive 4 6 (primitiveCoefficient C d y0) (η, TerminalEdgeFactor.edgeCoordinate (TerminalEdgeFactor.profileRadius y0 0) R) / R ^ 2

theorem NavierStokes.SlowFirstOrderEdge.profileStress_eq_primitive (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : profileStress C d y0 y = ParametricFlatFactor.primitive 4 6 (primitiveCoefficient C d y0) y / TerminalEdgeFactor.profileRadius y0 y.2 ^ 2

theorem NavierStokes.SlowFirstOrderEdge.profileStress_factorization (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (y : ℝ × ℝ) : profileStress C d y0 y = FlatCutoff.edge 4 y.2 / y.2 ^ 3 * stressFactor C d y0 y

theorem NavierStokes.SlowFirstOrderEdge.profileStress_contDiff (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiff ℝ (↑⊤) (profileStress C d y0)

theorem NavierStokes.SlowFirstOrderEdge.profileStress_zero_of_nonpos (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {y : ℝ × ℝ} (hy : y.2 ≤ 0) : profileStress C d y0 y = 0

theorem NavierStokes.SlowFirstOrderEdge.profileStress_edge_jets (C : ℝ) (d : OutgoingTail.TailData) (y0 η : ℝ) (n : ℕ) : iteratedFDeriv ℝ n (profileStress C d y0) (η, 0) = 0

theorem NavierStokes.SlowFirstOrderEdge.profileStress_jets (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (n : ℕ) {b : ℝ} (hb : 0 < b) : ∃ (M : ℝ), 0 < M ∧ ∃ (N : ℕ), ∀ i ≤ n, ∀ η ∈ Set.Icc (-1) 1, ∀ (x : ℝ), 0 < x → x ≤ b → ‖iteratedFDeriv ℝ i (profileStress C d y0) (η, x)‖ ≤ M * FlatCutoff.edge 4 x / x ^ N

All full joint derivative tensors, uniformly including both parameter endpoints.

The actual (X,η) profile coordinates

noncomputable def NavierStokes.SlowFirstOrderEdge.xChart (y0 : ℝ) (w : ℝ × ℝ) : ℝ × ℝ

X chart, given by (w.2, y0 + 3 - Real.log w.1).

Equations

• NavierStokes.SlowFirstOrderEdge.xChart y0 w = (w.2, y0 + 3 - Real.log w.1)

noncomputable def NavierStokes.SlowFirstOrderEdge.stressX (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (w : ℝ × ℝ) : ℝ

Stress X, given by profileStress C d y0 (xChart y0 w).

Equations

• NavierStokes.SlowFirstOrderEdge.stressX C d y0 w = NavierStokes.SlowFirstOrderEdge.profileStress C d y0 (NavierStokes.SlowFirstOrderEdge.xChart y0 w)

theorem NavierStokes.SlowFirstOrderEdge.xChart_contDiffOn (y0 : ℝ) : ContDiffOn ℝ (↑⊤) (xChart y0) {w : ℝ × ℝ | 0 < w.1}

theorem NavierStokes.SlowFirstOrderEdge.stressX_contDiffOn (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) : ContDiffOn ℝ (↑⊤) (stressX C d y0) {w : ℝ × ℝ | 0 < w.1}

theorem NavierStokes.SlowFirstOrderEdge.compact_jets_bound_on {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {S K : Set E} (hS : IsOpen S) (hf : ContDiffOn ℝ (↑⊤) f S) (hK : IsCompact K) (hKS : K ⊆ S) (n : ℕ) : ∃ (D : ℝ), 1 ≤ D ∧ ∀ i ≤ n, ∀ x ∈ K, ‖iteratedFDeriv ℝ i f x‖ ≤ D

theorem NavierStokes.SlowFirstOrderEdge.stressX_jets (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (n : ℕ) {b : ℝ} (hb : 0 < b) : ∃ (M : ℝ), 0 < M ∧ ∃ (N : ℕ), ∀ X ∈ Set.Ico (Real.exp (y0 + 3 - b)) (Real.exp (y0 + 3)), ∀ η ∈ Set.Icc (-1) 1, ‖iteratedFDeriv ℝ n (stressX C d y0) (X, η)‖ ≤ M * FlatCutoff.edge 4 (y0 + 3 - Real.log X) / (y0 + 3 - Real.log X) ^ N

noncomputable def NavierStokes.SlowFirstOrderEdge.zeta (cL a y0 X : ℝ) : ℝ

The two logarithmic Gaussian factors specified in (20).

Equations

• NavierStokes.SlowFirstOrderEdge.zeta cL a y0 X = NavierStokes.FlatCutoff.edge cL (Real.log (X / a)) * NavierStokes.FlatCutoff.edge 4 (y0 + 3 - Real.log X)

noncomputable def NavierStokes.SlowFirstOrderEdge.edgeDistance (a y0 X : ℝ) : ℝ

Edge distance, given by min 1 (min (Real.log (X / a)) (y0 + 3 - Real.log X)).

Equations

• NavierStokes.SlowFirstOrderEdge.edgeDistance a y0 X = min 1 (min (Real.log (X / a)) (y0 + 3 - Real.log X))

theorem NavierStokes.SlowFirstOrderEdge.stressX_zero_outside (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {X : ℝ} (hX : Real.exp (y0 + 3) ≤ X) (η : ℝ) : stressX C d y0 (X, η) = 0

theorem NavierStokes.SlowFirstOrderEdge.edge_mono_positive {c x y : ℝ} (hc : 0 ≤ c) (hx : 0 < x) (hxy : x ≤ y) : FlatCutoff.edge c x ≤ FlatCutoff.edge c y

theorem NavierStokes.SlowFirstOrderEdge.stressX_weighted_jets (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (n : ℕ) {b a cL : ℝ} (hb : 0 < b) (ha : 0 < a) (hcL : 0 < cL) (hcollar : a < Real.exp (y0 + 3 - b)) : ∃ (M : ℝ), 0 < M ∧ ∃ (N : ℕ), ∀ X ∈ Set.Ico (Real.exp (y0 + 3 - b)) (Real.exp (y0 + 3)), ∀ η ∈ Set.Icc (-1) 1, ‖iteratedFDeriv ℝ n (stressX C d y0) (X, η)‖ ≤ M * zeta cL a y0 X / edgeDistance a y0 X ^ N

The full weight from (20), with the lesser of the two log distances and one. The only geometric condition is that the closed outer collar avoids the inner edge.

Literal axial derivatives in physical coordinates

@[reducible, inline]

abbrev NavierStokes.SlowFirstOrderEdge.PhysicalPoint : Type

Physical point: an abbreviation for SimilarityProfile.PhysicalPoint.

Equations

• NavierStokes.SlowFirstOrderEdge.PhysicalPoint = NavierStokes.SimilarityProfile.PhysicalPoint

noncomputable def NavierStokes.SlowFirstOrderEdge.physicalChi (d : OutgoingTail.TailData) (p : PhysicalPoint) : ℝ

Physical chi, given by q d.h p ^ (-CoordinateAlgebra.D d.h) * profileChi d (eta d.h p).

Equations

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

theorem NavierStokes.SlowFirstOrderEdge.physicalChi_eq_logScale (d : OutgoingTail.TailData) {p : PhysicalPoint} (ht : p.1 < 1) : physicalChi d p = TerminalPressure.logScaleDerivative d.h p

theorem NavierStokes.SlowFirstOrderEdge.physicalChi_hasDerivAt_z (d : OutgoingTail.TailData) {p : PhysicalPoint} (ht : p.1 < 1) : HasDerivAt (fun (z : ℝ) => physicalChi d (p.1, p.2.1, z)) (-(SimilarityProfile.q d.h p ^ (-2 * CoordinateAlgebra.D d.h) * beta d (SimilarityProfile.eta d.h p))) p.2.2

noncomputable def NavierStokes.SlowFirstOrderEdge.physicalTaper (d : OutgoingTail.TailData) (y0 : ℝ) (p : PhysicalPoint) : ℝ

Physical taper, given by tailShape d (Real.log (X d.h p) - y0).

Equations

• NavierStokes.SlowFirstOrderEdge.physicalTaper d y0 p = NavierStokes.OutgoingTail.tailShape d (Real.log (NavierStokes.SimilarityProfile.X d.h p) - y0)

theorem NavierStokes.SlowFirstOrderEdge.physicalTaper_hasDerivAt_z (d : OutgoingTail.TailData) (y0 : ℝ) {p : PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : HasDerivAt (fun (z : ℝ) => physicalTaper d y0 (p.1, p.2.1, z)) (-physicalChi d p * OutgoingTail.tailShapeDeriv d (Real.log (SimilarityProfile.X d.h p) - y0)) p.2.2

theorem NavierStokes.SlowFirstOrderEdge.physicalTaper_second_z (d : OutgoingTail.TailData) (y0 : ℝ) {p : PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : deriv (deriv fun (z : ℝ) => physicalTaper d y0 (p.1, p.2.1, z)) p.2.2 = SimilarityProfile.q d.h p ^ (-2 * CoordinateAlgebra.D d.h) * (TerminalEdgeFactor.profileChi d (SimilarityProfile.eta d.h p) ^ 2 * deriv (OutgoingTail.tailShapeDeriv d) (Real.log (SimilarityProfile.X d.h p) - y0) + beta d (SimilarityProfile.eta d.h p) * OutgoingTail.tailShapeDeriv d (Real.log (SimilarityProfile.X d.h p) - y0))

theorem NavierStokes.SlowFirstOrderEdge.profileS_xChart (y0 : ℝ) {w : ℝ × ℝ} (hX : 0 < w.1) : TerminalEdgeFactor.profileS y0 (xChart y0 w).2 = w.1

theorem NavierStokes.SlowFirstOrderEdge.physicalHeat_eq_profileCarrier (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {p : PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : TerminalStress.physicalHeat C (1 + d.h) p = SimilarityProfile.q d.h p ^ (-CoordinateAlgebra.A d.h) * TerminalEdgeFactor.profileCarrier C d y0 (xChart y0 (SimilarityProfile.inner d.h p))

noncomputable def NavierStokes.SlowFirstOrderEdge.physicalAngular (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (p : PhysicalPoint) : ℝ

Literal physical angular velocity on the switched terminal collar.

Equations

• NavierStokes.SlowFirstOrderEdge.physicalAngular C d y0 p = NavierStokes.TerminalStress.physicalHeat C (1 + d.h) p * NavierStokes.SlowFirstOrderEdge.physicalTaper d y0 p

noncomputable def NavierStokes.SlowFirstOrderEdge.physicalSource (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) (p : PhysicalPoint) : ℝ

Literal negative second axial derivative; no independent jet is supplied.

Equations

• NavierStokes.SlowFirstOrderEdge.physicalSource C d y0 p = -deriv (deriv fun (z : ℝ) => NavierStokes.SlowFirstOrderEdge.physicalAngular C d y0 (p.1, p.2.1, z)) p.2.2

theorem NavierStokes.SlowFirstOrderEdge.physicalSource_eq (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {p : PhysicalPoint} : physicalSource C d y0 p = -TerminalStress.physicalHeat C (1 + d.h) p * deriv (deriv fun (z : ℝ) => physicalTaper d y0 (p.1, p.2.1, z)) p.2.2

theorem NavierStokes.SlowFirstOrderEdge.physicalSource_scaled (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {p : PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : physicalSource C d y0 p = SimilarityProfile.q d.h p ^ (-CoordinateAlgebra.A d.h - 1 + 2 * d.h) * profileSource C d y0 (xChart y0 (SimilarityProfile.inner d.h p))

The residual order is q^(-A-1+2h), before one radial integration.

theorem NavierStokes.SlowFirstOrderEdge.profileRadius_xChart (y0 : ℝ) {w : ℝ × ℝ} (hX : 0 < w.1) : TerminalEdgeFactor.profileRadius y0 (xChart y0 w).2 = √(2 * w.1)

theorem NavierStokes.SlowFirstOrderEdge.edgeCoordinate_eq_log (y0 : ℝ) {R : ℝ} (hR : 0 < R) : TerminalEdgeFactor.edgeCoordinate (TerminalEdgeFactor.profileRadius y0 0) R = y0 + 3 - Real.log (R ^ 2 / 2)

theorem NavierStokes.SlowFirstOrderEdge.stressX_eq_radialStress (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {w : ℝ × ℝ} (hX : 0 < w.1) : stressX C d y0 w = radialStress C d y0 w.2 √(2 * w.1)

noncomputable def NavierStokes.SlowFirstOrderEdge.physicalScale (d : OutgoingTail.TailData) (t z : ℝ) : ℝ

Physical scale, given by q d.h (t, (0, z)).

Equations

• NavierStokes.SlowFirstOrderEdge.physicalScale d t z = NavierStokes.SimilarityProfile.q d.h (t, 0, z)

noncomputable def NavierStokes.SlowFirstOrderEdge.physicalEta (d : OutgoingTail.TailData) (t z : ℝ) : ℝ

Physical eta, given by eta d.h (t, (0, z)).

Equations

• NavierStokes.SlowFirstOrderEdge.physicalEta d t z = NavierStokes.SimilarityProfile.eta d.h (t, 0, z)

theorem NavierStokes.SlowFirstOrderEdge.physicalScale_pos (d : OutgoingTail.TailData) {t z : ℝ} (ht : t < 1) : 0 < physicalScale d t z

theorem NavierStokes.SlowFirstOrderEdge.scaledRadius_identity {Q R : ℝ} (hQ : 0 < Q) : (R / √Q) ^ 2 / 2 = R ^ 2 / 2 / Q

theorem NavierStokes.SlowFirstOrderEdge.physicalSource_radial_scaled (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {t r z : ℝ} (ht : t < 1) (hr : 0 < r) : physicalSource C d y0 (TerminalStress.radiusPoint t r z) = physicalScale d t z ^ (-CoordinateAlgebra.A d.h - 1 + 2 * d.h) * radialSource C d y0 (physicalEta d t z) (r / √(physicalScale d t z))

theorem NavierStokes.SlowFirstOrderEdge.backwardStress_scale (b : ℝ) {Q r : ℝ} (hQ : 0 < Q) (hr : 0 < r) (g : ℝ → ℝ) : TerminalStress.backwardStress (fun (u : ℝ) => Q ^ b * g (u / √Q)) r = Q ^ (b + 1 / 2) * TerminalStress.backwardStress g (r / √Q)

Backward radial integration contributes exactly one half power of q.

noncomputable def NavierStokes.SlowFirstOrderEdge.physicalStress (C : ℝ) (d : OutgoingTail.TailData) (y0 t z r : ℝ) : ℝ

Physical stress, given by backwardStress (fun u => physicalSource C d y0 (radiusPoint t u z)) r.

Equations

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

theorem NavierStokes.SlowFirstOrderEdge.physicalStress_scaled_radial (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {t r z : ℝ} (ht : t < 1) (hr : 0 < r) : physicalStress C d y0 t z r = physicalScale d t z ^ (-CoordinateAlgebra.A d.h - 1 / 2 + 2 * d.h) * radialStress C d y0 (physicalEta d t z) (r / √(physicalScale d t z))

theorem NavierStokes.SlowFirstOrderEdge.physicalStress_scaled (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {t r z : ℝ} (ht : t < 1) (hr : 0 < r) : physicalStress C d y0 t z r = physicalScale d t z ^ (-CoordinateAlgebra.A d.h - 1 / 2 + 2 * d.h) * stressX C d y0 (r ^ 2 / 2 / physicalScale d t z, physicalEta d t z)

Identification of the actual physical backward primitive with the first-order profile coefficient, using the manuscript's exact tensor power.

theorem NavierStokes.SlowFirstOrderEdge.forward_eq_physicalStress (C : ℝ) (d : OutgoingTail.TailData) (y0 t z : ℝ) {F : ℝ → ℝ} {r : ℝ} (hr : 0 < r) (hi : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * F u) (Set.Ioi 0) MeasureTheory.volume) (hzero : ∫ (u : ℝ) in Set.Ioi 0, u ^ 2 * F u = 0) (hmatch : ∀ (u : ℝ), r ≤ u → F u = physicalSource C d y0 (TerminalStress.radiusPoint t u z)) : TerminalStress.forwardStress F r = physicalStress C d y0 t z r

Global moment closure is supplied by the separate renormalized-moment and slow-order moment theorems. Only agreement on the exterior ray is needed here.

theorem NavierStokes.SlowFirstOrderEdge.stressX_edge_jets (C : ℝ) (d : OutgoingTail.TailData) (y0 η : ℝ) (n : ℕ) : iteratedFDeriv ℝ n (stressX C d y0) (Real.exp (y0 + 3), η) = 0

theorem NavierStokes.SlowFirstOrderEdge.physicalSource_weight_integrable (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {t r z : ℝ} (ht : t < 1) (hr : 0 < r) : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * physicalSource C d y0 (TerminalStress.radiusPoint t u z)) (Set.Ioi r) MeasureTheory.volume

theorem NavierStokes.SlowFirstOrderEdge.editedAngular_eq_physicalAngular (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) {p : PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) (hfull : 1 / 2 ≤ Real.log (SimilarityProfile.X d.h p / K) + 1 / 5) : PhysicalHeatCoordinates.editedAngular d K p = physicalAngular (PhysicalHeatCoordinates.normalization d K) d (Real.log K - 1 / 5) p

The literal terminal velocity is the actual fully switched heat edit from the outgoing schedule, with its original amplitude and log origin.

theorem NavierStokes.SlowFirstOrderEdge.forward_eq_radialStress (C : ℝ) (d : OutgoingTail.TailData) (y0 η : ℝ) {F : ℝ → ℝ} {R : ℝ} (hR : 0 < R) (hi : MeasureTheory.IntegrableOn (fun (u : ℝ) => u ^ 2 * F u) (Set.Ioi 0) MeasureTheory.volume) (hzero : ∫ (u : ℝ) in Set.Ioi 0, u ^ 2 * F u = 0) (hmatch : ∀ (u : ℝ), R ≤ u → F u = radialSource C d y0 η u) : TerminalStress.forwardStress F R = radialStress C d y0 η R