The leading stress and its genuine divergence

The lag variables in this file are the regular primitives constructed in ProfileHistories. Every profile and physical derivative is a Fréchet derivative. The physical identities keep the axial-viscosity remainder.

noncomputable def NavierStokes.LeadingStress.sourceTheta {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) (w : ProfileHistories.Point) : ℝ

The angular source S_q; Profiles.angularSource is H S_q.

Equations

• NavierStokes.LeadingStress.sourceTheta P h w = P.angularSource h w / P.H w

noncomputable def NavierStokes.LeadingStress.sourceAxial {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) (w : ProfileHistories.Point) : ℝ

The axial source S_n.

Equations

• NavierStokes.LeadingStress.sourceAxial P h w = P.axialSource h w

noncomputable def NavierStokes.LeadingStress.theta {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) (w : ProfileHistories.Point) : ℝ

The coefficient of the angular radial stress in Proposition 3.2.

Equations

• NavierStokes.LeadingStress.theta P h w = P.f w * w.1 * P.angularLag h w / NavierStokes.CoordinateAlgebra.L h w.2 + 2 * w.1 * NavierStokes.SimilarityProfile.partialX P.f w

noncomputable def NavierStokes.LeadingStress.axial {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) (w : ProfileHistories.Point) : ℝ

The coefficient of the axial radial stress in Proposition 3.2.

Equations

• NavierStokes.LeadingStress.axial P h w = √(2 * w.1) * (NavierStokes.SimilarityProfile.partialX P.U w + P.axialLag h w / (2 * NavierStokes.CoordinateAlgebra.L h w.2))

noncomputable def NavierStokes.LeadingStress.slopeA {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (w : ProfileHistories.Point) : ℝ

Slope A, given by -2 * w.1 * partialX P.f w / P.f w.

Equations

• NavierStokes.LeadingStress.slopeA P w = -2 * w.1 * NavierStokes.SimilarityProfile.partialX P.f w / P.f w

noncomputable def NavierStokes.LeadingStress.slopeB {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (w : ProfileHistories.Point) : ℝ

Slope B, given by 2 * w.1 * partialX P.U w / P.E w.

Equations

• NavierStokes.LeadingStress.slopeB P w = 2 * w.1 * NavierStokes.SimilarityProfile.partialX P.U w / P.E w

theorem NavierStokes.LeadingStress.theta_eq_lag_minus_slope {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {w : ProfileHistories.Point} (hf : P.f w ≠ 0) : theta P h w = P.f w * (w.1 * P.angularLag h w / CoordinateAlgebra.L h w.2 - slopeA P w)

theorem NavierStokes.LeadingStress.axial_eq_lag_plus_slope {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {w : ProfileHistories.Point} (hX : 0 < w.1) (hf : P.f w ≠ 0) : axial P h w = P.f w * (w.1 * P.axialLag h w / (CoordinateAlgebra.L h w.2 * P.E w) + slopeB P w)

theorem NavierStokes.LeadingStress.partialX_hasDerivAt {f : ProfileHistories.Field} {w : ProfileHistories.Point} (hf : DifferentiableAt ℝ f w) : HasDerivAt (fun (x : ℝ) => f (x, w.2)) (SimilarityProfile.partialX f w) w.1

theorem NavierStokes.LeadingStress.partialX_H {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) {w : ProfileHistories.Point} (hw : w ∈ Ω.carrier) : SimilarityProfile.partialX P.H w = 2 * P.f w + 2 * w.1 * SimilarityProfile.partialX P.f w

theorem NavierStokes.LeadingStress.theta_smoothAt {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {w : ProfileHistories.Point} (hw : w ∈ Ω.carrier) (hX : w.1 ≠ 0) (hf : P.f w ≠ 0) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : ContDiffAt ℝ (↑⊤) (theta P h) w

theorem NavierStokes.LeadingStress.axial_smoothAt {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {w : ProfileHistories.Point} (hw : w ∈ Ω.carrier) (hX : w.1 ≠ 0) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : ContDiffAt ℝ (↑⊤) (axial P h) w

theorem NavierStokes.LeadingStress.partialX_theta {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {w : ProfileHistories.Point} (hw : w ∈ Ω.carrier) (hX : w.1 ≠ 0) (hf : P.f w ≠ 0) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : SimilarityProfile.partialX (theta P h) w = (SimilarityProfile.partialX P.f w * w.1 * P.angularLag h w + P.f w * P.angularLag h w + P.f w * w.1 * SimilarityProfile.partialX (P.angularLag h) w) / CoordinateAlgebra.L h w.2 + 2 * SimilarityProfile.partialX P.f w + 2 * w.1 * SimilarityProfile.partialX (SimilarityProfile.partialX P.f) w

theorem NavierStokes.LeadingStress.theta_divergence_coefficient {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {w : ProfileHistories.Point} (hw : w ∈ Ω.carrier) (hX : w.1 ≠ 0) (hf : P.f w ≠ 0) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : SimilarityProfile.partialX (theta P h) w + theta P h w / w.1 = P.f w * sourceTheta P h w / CoordinateAlgebra.L h w.2 + 2 * (w.1 * SimilarityProfile.partialX (SimilarityProfile.partialX P.f) w + 2 * SimilarityProfile.partialX P.f w)

The unweighted angular identity, using the actual regular lag equation.

theorem NavierStokes.LeadingStress.theta_divergence {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {w : ProfileHistories.Point} (hw : w ∈ Ω.carrier) (hX : 0 < w.1) (hf : P.f w ≠ 0) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : √(2 * w.1) * (SimilarityProfile.partialX (theta P h) w + theta P h w / w.1) = √(2 * w.1) * (P.f w * sourceTheta P h w / CoordinateAlgebra.L h w.2 + 2 * (w.1 * SimilarityProfile.partialX (SimilarityProfile.partialX P.f) w + 2 * SimilarityProfile.partialX P.f w))

The angular profile divergence in Proposition 3.2.

theorem NavierStokes.LeadingStress.partialX_axial {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {w : ProfileHistories.Point} (hw : w ∈ Ω.carrier) (hX : 0 < w.1) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : SimilarityProfile.partialX (axial P h) w = (SimilarityProfile.partialX P.U w + P.axialLag h w / (2 * CoordinateAlgebra.L h w.2)) / √(2 * w.1) + √(2 * w.1) * (SimilarityProfile.partialX (SimilarityProfile.partialX P.U) w + SimilarityProfile.partialX (P.axialLag h) w / (2 * CoordinateAlgebra.L h w.2))

theorem NavierStokes.LeadingStress.axial_divergence {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {w : ProfileHistories.Point} (hw : w ∈ Ω.carrier) (hX : 0 < w.1) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : √(2 * w.1) * SimilarityProfile.partialX (axial P h) w + axial P h w / √(2 * w.1) = sourceAxial P h w / CoordinateAlgebra.L h w.2 + 2 * (w.1 * SimilarityProfile.partialX (SimilarityProfile.partialX P.U) w + SimilarityProfile.partialX P.U w)

The axial profile divergence, obtained from the primitive-defined N_s.

theorem NavierStokes.LeadingStress.theta_transport_coefficient {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {w : ProfileHistories.Point} (hw : w ∈ Ω.carrier) (hX : w.1 ≠ 0) (hf : P.f w ≠ 0) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : SimilarityProfile.T h (-CoordinateAlgebra.A h - 1 / 2) P.f w + SlowDivergence.radialFlux h 0 P.U w * (SimilarityProfile.partialX P.f w + P.f w / w.1) + P.U w * SimilarityProfile.Z h (-CoordinateAlgebra.A h - 1 / 2) P.f w = -P.f w * sourceTheta P h w / CoordinateAlgebra.L h w.2

The coefficient of the angular inviscid residual is the negative lag source.

theorem NavierStokes.LeadingStress.axial_transport_coefficient {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) {w : ProfileHistories.Point} (hw : w ∈ Ω.carrier) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : SimilarityProfile.T h (-CoordinateAlgebra.A h) P.U w + SlowDivergence.radialFlux h 0 P.U w * SimilarityProfile.partialX P.U w + P.U w * SimilarityProfile.Z h (-CoordinateAlgebra.A h) P.U w + SimilarityProfile.Z h (-2 * CoordinateAlgebra.A h) P.pressure w = -sourceAxial P h w / CoordinateAlgebra.L h w.2

The axial inviscid residual includes the actual derivative of the constructed pressure.

theorem NavierStokes.LeadingStress.transport_pullback_add_axialViscosity {h e : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (α m : ℝ) (v u f source : ProfileHistories.Field) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (hs : 0 < p.2.1) (hf : ContDiffAt ℝ 2 f (SimilarityProfile.inner h p)) : SlowExpansionResidual.transportResidual α m (SimilarityProfile.pullback h 0 v) (SimilarityProfile.pullback h (-CoordinateAlgebra.A h) u) (SimilarityProfile.pullback h e f) (SimilarityProfile.pullback h (e - 1) source) p + SimilarityProfile.partialZ (SimilarityProfile.partialZ (SimilarityProfile.pullback h e f)) p = SimilarityProfile.q h p ^ (e - 1) * (SimilarityProfile.T h e f (SimilarityProfile.inner h p) + v (SimilarityProfile.inner h p) * (SimilarityProfile.partialX f (SimilarityProfile.inner h p) + α * f (SimilarityProfile.inner h p) / (SimilarityProfile.inner h p).1) + u (SimilarityProfile.inner h p) * SimilarityProfile.Z h e f (SimilarityProfile.inner h p) - 2 * ((SimilarityProfile.inner h p).1 * SimilarityProfile.partialX (SimilarityProfile.partialX f) (SimilarityProfile.inner h p) + m * SimilarityProfile.partialX f (SimilarityProfile.inner h p)) + source (SimilarityProfile.inner h p))

The exact zeroth-order transport formula. The added term is the full axial viscosity, not an estimate or a discarded remainder.

noncomputable def NavierStokes.LeadingStress.radialDivergence (k : ℝ) (S : SimilarityProfile.PhysicalProfile) (p : SimilarityProfile.PhysicalPoint) : ℝ

Cylindrical radial divergence (∂r + k/r)S, in the regular coordinate s=r²/2.

Equations

• NavierStokes.LeadingStress.radialDivergence k S p = √(2 * p.2.1) * NavierStokes.SimilarityProfile.partialS S p + k * S p / √(2 * p.2.1)

theorem NavierStokes.LeadingStress.hasDerivAt_radialSlice {S : SimilarityProfile.PhysicalProfile} {p : SimilarityProfile.PhysicalPoint} (hs : 0 ≤ p.2.1) (hS : DifferentiableAt ℝ S p) : HasDerivAt (fun (r : ℝ) => S (p.1, r ^ 2 / 2, p.2.2)) (√(2 * p.2.1) * SimilarityProfile.partialS S p) √(2 * p.2.1)

The regular-coordinate radial derivative is the derivative of the actual cylindrical slice, with the radius variable reconstructed by s=r²/2.

theorem NavierStokes.LeadingStress.radialDivergence_eq_deriv (k : ℝ) {S : SimilarityProfile.PhysicalProfile} {p : SimilarityProfile.PhysicalPoint} (hs : 0 ≤ p.2.1) (hS : DifferentiableAt ℝ S p) : radialDivergence k S p = deriv (fun (r : ℝ) => S (p.1, r ^ 2 / 2, p.2.2)) √(2 * p.2.1) + k * S p / √(2 * p.2.1)

theorem NavierStokes.LeadingStress.physical_radius {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) : √(2 * p.2.1) = SimilarityProfile.q h p ^ (1 / 2) * √(2 * (SimilarityProfile.inner h p).1)

theorem NavierStokes.LeadingStress.radialDivergence_pullback {h b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (k : ℝ) {S : ProfileHistories.Field} {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (hS : DifferentiableAt ℝ S (SimilarityProfile.inner h p)) : radialDivergence k (SimilarityProfile.pullback h b S) p = SimilarityProfile.q h p ^ (b - 1 / 2) * (√(2 * (SimilarityProfile.inner h p).1) * SimilarityProfile.partialX S (SimilarityProfile.inner h p) + k * S (SimilarityProfile.inner h p) / √(2 * (SimilarityProfile.inner h p).1))

The physical stress scaling produces exactly the cylindrical profile divergence.

theorem NavierStokes.LeadingStress.radius_mul_rpow {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (b : ℝ) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) : √(2 * p.2.1) * SimilarityProfile.q h p ^ b = SimilarityProfile.q h p ^ (b + 1 / 2) * √(2 * (SimilarityProfile.inner h p).1)

theorem NavierStokes.LeadingStress.sqrt_radial_two {X : ℝ} (hX : 0 < X) (S SX : ℝ) : √(2 * X) * SX + 2 * S / √(2 * X) = √(2 * X) * (SX + S / X)

noncomputable def NavierStokes.LeadingStress.fluxProfile {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) : SimilarityProfile.PhysicalProfile

Flux profile, given by pullback h 0 (SlowDivergence.radialFlux h 0 P.U).

Equations

• NavierStokes.LeadingStress.fluxProfile P h = NavierStokes.SimilarityProfile.pullback h 0 (NavierStokes.SlowDivergence.radialFlux h 0 P.U)

noncomputable def NavierStokes.LeadingStress.swirlProfile {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) : SimilarityProfile.PhysicalProfile

Swirl profile, given by pullback h (-A h - 1 / 2) P.f.

Equations

• NavierStokes.LeadingStress.swirlProfile P h = NavierStokes.SimilarityProfile.pullback h (-NavierStokes.CoordinateAlgebra.A h - 1 / 2) P.f

noncomputable def NavierStokes.LeadingStress.axialProfile {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) : SimilarityProfile.PhysicalProfile

Axial profile, given by pullback h (-A h) P.U.

Equations

• NavierStokes.LeadingStress.axialProfile P h = NavierStokes.SimilarityProfile.pullback h (-NavierStokes.CoordinateAlgebra.A h) P.U

noncomputable def NavierStokes.LeadingStress.pressureProfile {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) : SimilarityProfile.PhysicalProfile

Pressure profile, given by pullback h (-2 * A h) P.pressure.

Equations

• NavierStokes.LeadingStress.pressureProfile P h = NavierStokes.SimilarityProfile.pullback h (-2 * NavierStokes.CoordinateAlgebra.A h) P.pressure

noncomputable def NavierStokes.LeadingStress.physicalStressTheta {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) : SimilarityProfile.PhysicalProfile

Physical stress theta, given by pullback h (-A h - 1 / 2) (theta P h).

Equations

• NavierStokes.LeadingStress.physicalStressTheta P h = NavierStokes.SimilarityProfile.pullback h (-NavierStokes.CoordinateAlgebra.A h - 1 / 2) (NavierStokes.LeadingStress.theta P h)

noncomputable def NavierStokes.LeadingStress.physicalStressAxial {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) : SimilarityProfile.PhysicalProfile

Physical stress axial, given by pullback h (-A h - 1 / 2) (axial P h).

Equations

• NavierStokes.LeadingStress.physicalStressAxial P h = NavierStokes.SimilarityProfile.pullback h (-NavierStokes.CoordinateAlgebra.A h - 1 / 2) (NavierStokes.LeadingStress.axial P h)

noncomputable def NavierStokes.LeadingStress.physicalVelocity {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) : ProblemStatement.VelocityField

Physical velocity, given by AxisymmetricResidual.velocity (RadialFluxResidual.radialB (fluxProfile P h)) (swirlProfile P h) (axialProfile P h).

Equations

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

noncomputable def NavierStokes.LeadingStress.physicalPressure {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) : ProblemStatement.PressureField

Physical pressure, given by AxisymmetricResidual.pressure (pressureProfile P h).

Equations

• NavierStokes.LeadingStress.physicalPressure P h = NavierStokes.AxisymmetricResidual.pressure (NavierStokes.LeadingStress.pressureProfile P h)

noncomputable def NavierStokes.LeadingStress.thetaAxialViscosity {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) (p : SimilarityProfile.PhysicalPoint) : ℝ

The angular axial-viscosity term omitted from the leading radial balance.

Equations

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

noncomputable def NavierStokes.LeadingStress.axialAxialViscosity {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) (h : ℝ) (p : SimilarityProfile.PhysicalPoint) : ℝ

The axial axial-viscosity term omitted from the leading radial balance.

Equations

• NavierStokes.LeadingStress.axialAxialViscosity P h p = NavierStokes.SimilarityProfile.partialZ (NavierStokes.SimilarityProfile.partialZ (NavierStokes.LeadingStress.axialProfile P h)) p

theorem NavierStokes.LeadingStress.inner_X_pos {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (hs : 0 < p.2.1) : 0 < (SimilarityProfile.inner h p).1

theorem NavierStokes.LeadingStress.radialDivergence_physicalStressTheta {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (hs : 0 < p.2.1) (hw : SimilarityProfile.inner h p ∈ Ω.carrier) (hf : P.f (SimilarityProfile.inner h p) ≠ 0) : radialDivergence 2 (physicalStressTheta P h) p = SimilarityProfile.q h p ^ (-CoordinateAlgebra.A h - 1) * (√(2 * (SimilarityProfile.inner h p).1) * (P.f (SimilarityProfile.inner h p) * sourceTheta P h (SimilarityProfile.inner h p) / CoordinateAlgebra.L h (SimilarityProfile.inner h p).2 + 2 * ((SimilarityProfile.inner h p).1 * SimilarityProfile.partialX (SimilarityProfile.partialX P.f) (SimilarityProfile.inner h p) + 2 * SimilarityProfile.partialX P.f (SimilarityProfile.inner h p))))

theorem NavierStokes.LeadingStress.radialDivergence_physicalStressAxial {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (hs : 0 < p.2.1) (hw : SimilarityProfile.inner h p ∈ Ω.carrier) : radialDivergence 1 (physicalStressAxial P h) p = SimilarityProfile.q h p ^ (-CoordinateAlgebra.A h - 1) * (sourceAxial P h (SimilarityProfile.inner h p) / CoordinateAlgebra.L h (SimilarityProfile.inner h p).2 + 2 * ((SimilarityProfile.inner h p).1 * SimilarityProfile.partialX (SimilarityProfile.partialX P.U) (SimilarityProfile.inner h p) + SimilarityProfile.partialX P.U (SimilarityProfile.inner h p)))

theorem NavierStokes.LeadingStress.thetaAxialViscosity_eq {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (hw : SimilarityProfile.inner h p ∈ Ω.carrier) : thetaAxialViscosity P h p = SimilarityProfile.q h p ^ (-CoordinateAlgebra.A h - 1 + 2 * h) * (√(2 * (SimilarityProfile.inner h p).1) * SlowExpansionResidual.Z2 h (-CoordinateAlgebra.A h - 1 / 2) P.f (SimilarityProfile.inner h p))

theorem NavierStokes.LeadingStress.axialAxialViscosity_eq {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (hw : SimilarityProfile.inner h p ∈ Ω.carrier) : axialAxialViscosity P h p = SimilarityProfile.q h p ^ (-CoordinateAlgebra.A h - 1 + 2 * h) * SlowExpansionResidual.Z2 h (-CoordinateAlgebra.A h) P.U (SimilarityProfile.inner h p)

theorem NavierStokes.LeadingStress.theta_transport_stress {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (hs : 0 < p.2.1) (hw : SimilarityProfile.inner h p ∈ Ω.carrier) (hf : P.f (SimilarityProfile.inner h p) ≠ 0) : √(2 * p.2.1) * SlowExpansionResidual.transportResidual 1 2 (fluxProfile P h) (axialProfile P h) (swirlProfile P h) (fun (x : AxisymmetricFields.ProfilePoint) => 0) p + thetaAxialViscosity P h p = -radialDivergence 2 (physicalStressTheta P h) p

theorem NavierStokes.LeadingStress.partialZ_pressureProfile {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (hw : SimilarityProfile.inner h p ∈ Ω.carrier) : SimilarityProfile.partialZ (pressureProfile P h) p = SimilarityProfile.pullback h (-CoordinateAlgebra.A h - 1) (SimilarityProfile.Z h (-2 * CoordinateAlgebra.A h) P.pressure) p

theorem NavierStokes.LeadingStress.axial_transport_stress {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (hs : 0 < p.2.1) (hw : SimilarityProfile.inner h p ∈ Ω.carrier) : SlowExpansionResidual.transportResidual 0 1 (fluxProfile P h) (axialProfile P h) (axialProfile P h) (SimilarityProfile.partialZ (pressureProfile P h)) p + axialAxialViscosity P h p = -radialDivergence 1 (physicalStressAxial P h) p

theorem NavierStokes.LeadingStress.physical_swirl_value {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) : √(2 * p.2.1) * swirlProfile P h p = SimilarityProfile.pullback h (-CoordinateAlgebra.A h) P.E p

The regular swirl coefficient reconstructs precisely u_theta=q^(-A) E.

noncomputable def NavierStokes.LeadingStress.angularComponent (x v : ProblemStatement.Space) : ℝ

Cylindrical angular component of a genuine Cartesian vector.

Equations

• NavierStokes.LeadingStress.angularComponent x v = (x.ofLp 0 * v.ofLp 1 - x.ofLp 1 * v.ofLp 0) / √(2 * NavierStokes.AxisymmetricFields.radialEnergy x)

theorem NavierStokes.LeadingStress.angularComponent_pack {x : ProblemStatement.Space} (hs : 0 < AxisymmetricFields.radialEnergy x) (R T Z : ℝ) : angularComponent x (AxisymmetricResidual.pack (x.ofLp 0 * R + x.ofLp 1 * T) (x.ofLp 1 * R - x.ofLp 0 * T) Z) = -√(2 * AxisymmetricFields.radialEnergy x) * T

theorem NavierStokes.LeadingStress.navierStokesResidual_tangential {Ω : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles Ω) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {t : ℝ} {x : ProblemStatement.Space} (ht : t < 1) (hs : 0 < AxisymmetricFields.radialEnergy x) (hw : SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x) ∈ Ω.carrier) (hf : P.f (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x)) ≠ 0) : angularComponent x (ProblemStatement.navierStokesResidual (physicalVelocity P h) (physicalPressure P h) t x) + thetaAxialViscosity P h (AxisymmetricFields.profilePoint t x) = -radialDivergence 2 (physicalStressTheta P h) (AxisymmetricFields.profilePoint t x) ∧ (ProblemStatement.navierStokesResidual (physicalVelocity P h) (physicalPressure P h) t x).ofLp 2 + axialAxialViscosity P h (AxisymmetricFields.profilePoint t x) = -radialDivergence 1 (physicalStressAxial P h) (AxisymmetricFields.profilePoint t x)

Proposition 3.2 for the actual Cartesian Navier--Stokes residual.

The local hypotheses avoid extending the quotient defining radial velocity across the axis. The two added terms are the exact axial-viscosity terms; their explicit similarity formulas are thetaAxialViscosity_eq and axialAxialViscosity_eq.