The heat edit in the actual implicit physical coordinates

The parameter is eta = z / q^(1/2-h), where the positive implicit branch satisfies 1-t = q - z^2*q^(2*h). The quadratic-coordinate helper with q = tau + z^2 is not used here. These identities connect the actual heat edit to the terminal angular velocity, including its normalization.

theorem NavierStokes.PhysicalHeatCoordinates.diffusion_eq_ratio {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) : ParametricHeatTail.diffusion (SimilarityProfile.eta h p) = (1 - p.1) / SimilarityProfile.q h p

theorem NavierStokes.PhysicalHeatCoordinates.heat_argument {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) : 2 * ParametricHeatTail.diffusion (SimilarityProfile.eta h p) / SimilarityProfile.X h p = 2 * (1 - p.1) / p.2.1

noncomputable def NavierStokes.PhysicalHeatCoordinates.normalization (d : OutgoingTail.TailData) (K : ℝ) : ℝ

Normalization, given by HeatTailEdit.outgoingAmplitude d * K ^ HeatTailEdit.exponent d.h.

Equations

• NavierStokes.PhysicalHeatCoordinates.normalization d K = NavierStokes.HeatTailEdit.outgoingAmplitude d * K ^ NavierStokes.HeatTailEdit.exponent d.h

theorem NavierStokes.PhysicalHeatCoordinates.normalization_pos (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) : 0 < normalization d K

noncomputable def NavierStokes.PhysicalHeatCoordinates.editedAngular (d : OutgoingTail.TailData) (K : ℝ) (p : SimilarityProfile.PhysicalPoint) : ℝ

Edited angular, given by q d.h p ^ (-HeatTailEdit.exponent d.h) * ParametricHeatTail.physicalEdit d K (eta d.h p) (X d.h p).

Equations

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

noncomputable def NavierStokes.PhysicalHeatCoordinates.shape (d : OutgoingTail.TailData) (K y : ℝ) : ℝ

Shape, given by OutgoingTail.tailShape d (y - Real.log K + 1 / 5).

Equations

• NavierStokes.PhysicalHeatCoordinates.shape d K y = NavierStokes.OutgoingTail.tailShape d (y - Real.log K + 1 / 5)

theorem NavierStokes.PhysicalHeatCoordinates.editedAngular_eq_heat (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) (hh1 : d.h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) (hfull : 1 / 2 ≤ Real.log (SimilarityProfile.X d.h p / K) + 1 / 5) : editedAngular d K p = TerminalStress.physicalHeat (normalization d K) (1 + d.h) p * TerminalStress.flattening d.h (shape d K) p

theorem NavierStokes.PhysicalHeatCoordinates.editedAngular_eq_pure_heat (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) (hh1 : d.h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) (hlate : 3 ≤ Real.log (SimilarityProfile.X d.h p / K) + 1 / 5) : editedAngular d K p = TerminalStress.physicalHeat (normalization d K) (1 + d.h) p

theorem NavierStokes.PhysicalHeatCoordinates.editedAngular_div_radius (d : OutgoingTail.TailData) {K : ℝ} (hK : 0 < K) (hh1 : d.h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (ht : p.1 < 1) (hs : 0 < p.2.1) (hfull : 1 / 2 ≤ Real.log (SimilarityProfile.X d.h p / K) + 1 / 5) : editedAngular d K p / √(2 * p.2.1) = TerminalStress.swirlCoefficient (normalization d K) d.h (shape d K) p

noncomputable def NavierStokes.PhysicalHeatCoordinates.normalizedSection (x e : ℝ) : SimilarityProfile.PhysicalPoint

The normalized section is used only inside the physical time domain. It supplies a direct profile-parameter comparison without log(1-eta^2). Endpoint extensions of profile factors are proved separately.

Equations

• NavierStokes.PhysicalHeatCoordinates.normalizedSection x e = (e ^ 2, x, e)

theorem NavierStokes.PhysicalHeatCoordinates.q_normalizedSection {h e : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (he : e ^ 2 < 1) (x : ℝ) : SimilarityProfile.q h (normalizedSection x e) = 1

theorem NavierStokes.PhysicalHeatCoordinates.eta_normalizedSection {h e : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (he : e ^ 2 < 1) (x : ℝ) : SimilarityProfile.eta h (normalizedSection x e) = e

theorem NavierStokes.PhysicalHeatCoordinates.X_normalizedSection {h e : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (he : e ^ 2 < 1) (x : ℝ) : SimilarityProfile.X h (normalizedSection x e) = x

theorem NavierStokes.PhysicalHeatCoordinates.editedAngular_normalizedSection (d : OutgoingTail.TailData) (hh1 : d.h < 1 / 2) {e : ℝ} (he : e ^ 2 < 1) (K x : ℝ) : editedAngular d K (normalizedSection x e) = ParametricHeatTail.physicalEdit d K e x