Entrance estimates for the actual natural profiles

The source and cone coordinates below are expressions in the actual smooth profiles. Uniform estimates and the regular radial integral are used to check the entrance test before any outgoing controlled continuation.

@[instance_reducible]

noncomputable def NavierStokes.NaturalEntrance.instNaturalEntrance1 (I : AxisCoefficientSpace.Window) (ε : ℝ) : NormedAddCommGroup ↥(AxisCoefficientSpace.AxisSpace I ε)

Cache the standard NormedAddCommGroup (AxisCoefficientSpace.AxisSpace I ε) instance to shorten typeclass synthesis.

Equations

• NavierStokes.NaturalEntrance.instNaturalEntrance1 I ε = inferInstance

@[instance_reducible]

noncomputable def NavierStokes.NaturalEntrance.instNaturalEntrance2 (I : AxisCoefficientSpace.Window) (ε : ℝ) : NormedSpace ℝ ↥(AxisCoefficientSpace.AxisSpace I ε)

Cache the standard NormedSpace ℝ (AxisCoefficientSpace.AxisSpace I ε) instance to shorten typeclass synthesis.

Equations

• NavierStokes.NaturalEntrance.instNaturalEntrance2 I ε = inferInstance

noncomputable def NavierStokes.NaturalEntrance.Sq (h : ℝ) (f U V : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Sq, given by -transportW h V p * (1 + p.1 * partialY f p / f p) - h * (1 - 2 * p.2 * U p) - transportH h U p * (partialEta f p / f p).

Equations

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

noncomputable def NavierStokes.NaturalEntrance.p1 (f : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

P1, given by -2 * p.1 * partialY f p / f p.

Equations

• NavierStokes.NaturalEntrance.p1 f p = -2 * p.1 * NavierStokes.NaturalAxisBridge.partialY f p / f p

noncomputable def NavierStokes.NaturalEntrance.ns (U : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Ns, given by -2 * partialY U p.

Equations

• NavierStokes.NaturalEntrance.ns U p = -2 * NavierStokes.NaturalAxisBridge.partialY U p

noncomputable def NavierStokes.NaturalEntrance.angularVelocity (f : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Angular velocity, given by Real.sqrt (2 * p.1) * f p.

Equations

• NavierStokes.NaturalEntrance.angularVelocity f p = √(2 * p.1) * f p

noncomputable def NavierStokes.NaturalEntrance.p2 (f U : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

P2, given by p.1 * ns U p / angularVelocity f p.

Equations

• NavierStokes.NaturalEntrance.p2 f U p = p.1 * NavierStokes.NaturalEntrance.ns U p / NavierStokes.NaturalEntrance.angularVelocity f p

noncomputable def NavierStokes.NaturalEntrance.coneSize (f U : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Cone size, given by p1 f p + (p2 f U p) ^ 2 / p1 f p.

Equations

• NavierStokes.NaturalEntrance.coneSize f U p = NavierStokes.NaturalEntrance.p1 f p + NavierStokes.NaturalEntrance.p2 f U p ^ 2 / NavierStokes.NaturalEntrance.p1 f p

theorem NavierStokes.NaturalEntrance.Sq_eq_radial {h j Λ : ℝ} {P0 a₀ : ℝ → ℝ} {f U V Pr : ℝ × ℝ → ℝ} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a₀ f U V Pr) {p : ℝ × ℝ} (hp : p ∈ NaturalProfile.domain Λ) (hf : f p ≠ 0) : Sq h f U V p = -2 * NaturalAxisData.L h p.2 * NaturalAxisBridge.radialDifferential 2 f p / f p

theorem NavierStokes.NaturalEntrance.base_source_lower {h j : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) {η : ℝ} (hη : η ∈ Set.Icc (-1) 1) : 29 / 10 < -NaturalAxisData.W h j η - h * (1 - 2 * η * NaturalAxisData.U j η)

The strictly positive axis contribution is quantitative on the entire original parameter interval.

theorem NavierStokes.NaturalEntrance.chi_zero_imp_H_zero (h j : ℝ) {σ η : ℝ} (hσ : 0 < σ) (hchi : NaturalAxisData.chi h j σ η = 0) : NaturalAxisData.H h j η = 0

theorem NavierStokes.NaturalEntrance.gradient_zero_of_chi_zero (h j : ℝ) {σ η : ℝ} (hσ : 0 < σ) (hchi : NaturalAxisData.chi h j σ η = 0) : NaturalAxisCoefficients.realGradient h j σ η = 0

theorem NavierStokes.NaturalEntrance.cone_size_of_second_large {a b : ℝ} (ha : 0 < a) (hb : (6 / 5) ^ 2 < b ^ 2) : 12 / 5 < a + b ^ 2 / a

A large second coordinate yields a strict cone-size margin uniformly over every positive first coordinate.

theorem NavierStokes.NaturalEntrance.compact_absorption {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (χ R : K → ℝ) (hχ : Continuous χ) (hR : Continuous R) (hnonneg : ∀ (p : K), 0 ≤ χ p) (b : ℝ) (hzero : ∀ (p : K), χ p = 0 → b < R p) : ∃ (M : ℝ), 0 < M ∧ ∀ (Λ : ℝ), M ≤ Λ → ∀ (p : K), b < Λ * χ p + R p

Compactness supplies one absorption scale when the limiting remainder is already positive on the zero set of the nonnegative growing coefficient.

theorem NavierStokes.NaturalEntrance.compact_small_perturbation {K : Type u_1} {E : Type u_2} [MetricSpace K] [CompactSpace K] [NormedAddCommGroup E] [ProperSpace E] (F : K × E → ℝ) (hF : Continuous F) {ε : ℝ} (hε : 0 < ε) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (p : K) (e : E), ‖e‖ < δ → |F (p, e) - F (p, 0)| < ε

A continuous expression satisfies a uniform small-perturbation estimate around its zero-perturbation graph over a compact parameter set.

theorem NavierStokes.NaturalEntrance.radial_flux_hasDerivAt {f : ℝ → ℝ} {X : ℝ} (hf : ContDiffAt ℝ 2 f X) : HasDerivAt (fun (x : ℝ) => x ^ 2 * deriv f x) (X * (X * deriv (deriv f) X + 2 * deriv f X)) X

theorem NavierStokes.NaturalEntrance.derivative_neg_of_regular_source {f : ℝ → ℝ} {R L : ℝ} (hR : 0 < R) (hL : 0 < L) (hf : ∀ x ∈ Set.Icc 0 R, ContDiffAt ℝ 2 f x) (hpos : ∀ x ∈ Set.Icc 0 R, 0 < f x) (hsource : ∀ x ∈ Set.Ioo 0 R, 0 < -2 * L * (x * deriv (deriv f) x + 2 * deriv f x) / f x) : deriv f R < 0

The regular branch starts with zero radial flux. A positive source therefore forces a strictly negative radial derivative away from the axis.

def NavierStokes.NaturalEntrance.entranceSet : Set (ℝ × ℝ)

Entrance set, constructed using Icc.

Equations

• NavierStokes.NaturalEntrance.entranceSet = Set.Icc 0 (41 / 10) ×ˢ Set.Icc (-1) 1

instance NavierStokes.NaturalEntrance.instCompactSpaceElemProdRealEntranceSet : CompactSpace ↑entranceSet

theorem NavierStokes.NaturalEntrance.entrance_mem_strip {p : ℝ × ℝ} (hp : p ∈ entranceSet) : p ∈ AxisEvaluation.strip NaturalAxisCoefficients.window 20

theorem NavierStokes.NaturalEntrance.entrance_abs_le_five {p : ℝ × ℝ} (hp : p ∈ entranceSet) : |p.1| ≤ 5

@[reducible, inline]

abbrev NavierStokes.NaturalEntrance.CoefficientPair (ε : ℝ) : Type

Coefficient pair: an abbreviation for AxisCoefficientSpace.AxisSpace window ε × AxisCoefficientSpace.AxisSpace window ε.

Equations

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

noncomputable def NavierStokes.NaturalEntrance.sourceJets {ε : ℝ} (hε : 0 < ε) (x : CoefficientPair ε) (p : ℝ × ℝ) : Fin 6 → ℝ

The finite jets needed by the angular source, including the genuine bounded average operator.

Equations

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

noncomputable def NavierStokes.NaturalEntrance.sourceJetConstant (ε : ℝ) : ℝ

Source jet constant, given by 1 + AxisEvaluation.jetBound ε 5 0 0 + AxisEvaluation.jetBound ε 5 1 0 + AxisEvaluation.jetBound ε 5 0 1.

Equations

• NavierStokes.NaturalEntrance.sourceJetConstant ε = 1 + NavierStokes.AxisEvaluation.jetBound ε 5 0 0 + NavierStokes.AxisEvaluation.jetBound ε 5 1 0 + NavierStokes.AxisEvaluation.jetBound ε 5 0 1

theorem NavierStokes.NaturalEntrance.sourceJetConstant_pos {ε : ℝ} (hε : 0 < ε) : 0 < sourceJetConstant ε

theorem NavierStokes.NaturalEntrance.sourceJets_sub_bound {ε : ℝ} (hε : 0 < ε) (x y : CoefficientPair ε) {p : ℝ × ℝ} (hp : p ∈ entranceSet) : ‖sourceJets hε x p - sourceJets hε y p‖ ≤ sourceJetConstant ε * ‖x - y‖

theorem NavierStokes.NaturalEntrance.sourceJets_continuous {ε : ℝ} (hε : 0 < ε) (x : CoefficientPair ε) : Continuous fun (p : ↑entranceSet) => sourceJets hε x ↑p

noncomputable def NavierStokes.NaturalEntrance.sourceRemainder (h j σ : ℝ) (p : ℝ × ℝ) (t : ℝ) (v : Fin 6 → ℝ) : ℝ

Subtracting the growing term L Λ χ leaves this continuous expression. The clipped denominator agrees with every profile used below and makes the finite-dimensional uniform-continuity argument global.

Equations

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

theorem NavierStokes.NaturalEntrance.realGradient_continuous (h j : ℝ) {σ : ℝ} (hσ : 0 < σ) : Continuous (NaturalAxisCoefficients.realGradient h j σ)

theorem NavierStokes.NaturalEntrance.sourceRemainder_continuous (h j : ℝ) {σ : ℝ} (hσ : 0 < σ) : Continuous fun (z : (ℝ × ℝ) × ℝ × (Fin 6 → ℝ)) => sourceRemainder h j σ z.1 z.2.1 z.2.2

noncomputable def NavierStokes.NaturalEntrance.referencePair {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) : CoefficientPair v.epsilon

Reference pair, given by referenceCoefficients window v.epsilon_pos (v.elements .chi) v.axisData.

Equations

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

noncomputable def NavierStokes.NaturalEntrance.referenceRemainder {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (p : ↑entranceSet) : ℝ

Reference remainder, given by sourceRemainder h j σ p 0 (sourceJets v.epsilon_pos (referencePair v) p).

Equations

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

theorem NavierStokes.NaturalEntrance.reference_phi_value {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (p : ↑entranceSet) : sourceJets ⋯ (referencePair v) (↑p) 0 = AxisSeries.profile (NaturalAxisData.chi h j σ (↑p).2) (↑p).1

theorem NavierStokes.NaturalEntrance.reference_phi_lower {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (hσ : 0 < σ) (p : ↑entranceSet) : 1 / 4 < sourceJets ⋯ (referencePair v) (↑p) 0

theorem NavierStokes.NaturalEntrance.reference_phiY_zero {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (p : ↑entranceSet) (hchi : NaturalAxisData.chi h j σ (↑p).2 = 0) : sourceJets ⋯ (referencePair v) (↑p) 1 = 0

theorem NavierStokes.NaturalEntrance.referenceRemainder_continuous {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (hσ : 0 < σ) : Continuous (referenceRemainder v)

theorem NavierStokes.NaturalEntrance.referenceRemainder_at_chi_zero {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (hσ : 0 < σ) (p : ↑entranceSet) (hchi : NaturalAxisData.chi h j σ (↑p).2 = 0) : referenceRemainder v p = -NaturalAxisData.W h j (↑p).2 - h * (1 - 2 * (↑p).2 * NaturalAxisData.U j (↑p).2)

theorem NavierStokes.NaturalEntrance.chi_continuous (h j : ℝ) {σ : ℝ} (hσ : 0 < σ) : Continuous (NaturalAxisData.chi h j σ)

theorem NavierStokes.NaturalEntrance.reference_source_absorption {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) : ∃ (M : ℝ), 0 < M ∧ ∀ (Λ : ℝ), M ≤ Λ → ∀ (p : ↑entranceSet), 27 / 10 < Λ * (1 / 20 * NaturalAxisData.L h (↑p).2 * NaturalAxisData.chi h j σ (↑p).2) + referenceRemainder v p

noncomputable def NavierStokes.NaturalEntrance.perturbationSource {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (q : ↑entranceSet × ℝ × (Fin 6 → ℝ)) : ℝ

Perturbation source, given by sourceRemainder h j σ q.1 q.2.1 (sourceJets v.epsilon_pos (referencePair v) q.1 + q.2.2).

Equations

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

theorem NavierStokes.NaturalEntrance.perturbationSource_continuous {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (hσ : 0 < σ) : Continuous (perturbationSource v)

theorem NavierStokes.NaturalEntrance.sourceRemainder_uniform_limit {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (hσ : 0 < σ) {K : ℝ} (hK : 0 ≤ K) : ∃ (M : ℝ), 0 < M ∧ ∀ (Λ : ℝ), M ≤ Λ → ∀ (x : CoefficientPair v.epsilon), ‖x - referencePair v‖ ≤ K / (2 * Λ) → ∀ (p : ↑entranceSet), |sourceRemainder h j σ (↑p) (1 / Λ) (sourceJets ⋯ x ↑p) - referenceRemainder v p| < 1 / 10

The finite-dimensional source correction converges uniformly, using the proved evaluation operator bounds and the actual coefficient-space norm error.

theorem NavierStokes.NaturalEntrance.source_uniform_lower {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {K : ℝ} (hK : 0 ≤ K) : ∃ (M : ℝ), 0 < M ∧ ∀ (Λ : ℝ), M ≤ Λ → ∀ (x : CoefficientPair v.epsilon), ‖x - referencePair v‖ ≤ K / (2 * Λ) → ∀ (p : ↑entranceSet), 19 / 20 * NaturalAxisData.L h (↑p).2 * Λ * NaturalAxisData.chi h j σ (↑p).2 + 5 / 2 < NaturalAxisData.L h (↑p).2 * Λ * NaturalAxisData.chi h j σ (↑p).2 + sourceRemainder h j σ (↑p) (1 / Λ) (sourceJets ⋯ x ↑p)

The exact coefficient-space approximation gives the desired quantitative source bound after one common large-scale choice.

theorem NavierStokes.NaturalEntrance.angularProfile_radial_log_derivative {a : ℝ → ℝ} {Λ : ℝ} {Φ : ℝ × ℝ → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) {p : ℝ × ℝ} (hp : p ∈ NaturalProfile.domain Λ) (ha : a p.2 ≠ 0) (_hval : Φ (NaturalProfile.rescalePoint Λ p) ≠ 0) : p.1 * NaturalAxisBridge.partialY (NaturalProfile.angularProfile a Λ Φ) p / NaturalProfile.angularProfile a Λ Φ p = (NaturalProfile.rescalePoint Λ p).1 * NaturalAxisBridge.partialY Φ (NaturalProfile.rescalePoint Λ p) / Φ (NaturalProfile.rescalePoint Λ p)

theorem NavierStokes.NaturalEntrance.angularProfile_parameter_log_derivative {a : ℝ → ℝ} {Λ κ : ℝ} {Φ : ℝ × ℝ → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) {p : ℝ × ℝ} (hp : p ∈ NaturalProfile.domain Λ) (ha : a p.2 ≠ 0) (hval : Φ (NaturalProfile.rescalePoint Λ p) ≠ 0) (had : HasDerivAt a (Λ * κ * a p.2) p.2) : NaturalAxisBridge.partialEta (NaturalProfile.angularProfile a Λ Φ) p / NaturalProfile.angularProfile a Λ Φ p = Λ * κ + NaturalAxisBridge.partialEta Φ (NaturalProfile.rescalePoint Λ p) / Φ (NaturalProfile.rescalePoint Λ p)

theorem NavierStokes.NaturalEntrance.Sq_reconstruction {h j σ Λ : ℝ} (P0 : ℝ → ℝ) {a : ℝ → ℝ} {Φ u B : ℝ × ℝ → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) (hB : ContDiffOn ℝ (↑⊤) B (AxisEvaluation.strip NaturalAxisCoefficients.window 20)) (hΛ : Λ ≠ 0) {p : ℝ × ℝ} (hp : p ∈ NaturalProfile.domain Λ) (ha : a p.2 ≠ 0) (hval : 1 / 8 ≤ Φ (NaturalProfile.rescalePoint Λ p)) (had : HasDerivAt a (Λ * NaturalAxisCoefficients.realGradient h j σ p.2 * a p.2) p.2) : Sq h (NaturalProfile.angularProfile a Λ Φ) (NaturalProfile.affineProfile (NaturalAxisData.U j) (1 / Λ) Λ u) (NaturalProfile.affineProfile (NaturalAxisData.U j) (1 / Λ) Λ B) p = NaturalAxisData.L h p.2 * Λ * NaturalAxisData.chi h j σ p.2 + sourceRemainder h j σ (NaturalProfile.rescalePoint Λ p) (1 / Λ) ![Φ (NaturalProfile.rescalePoint Λ p), NaturalAxisBridge.partialY Φ (NaturalProfile.rescalePoint Λ p), NaturalAxisBridge.partialEta Φ (NaturalProfile.rescalePoint Λ p), u (NaturalProfile.rescalePoint Λ p), B (NaturalProfile.rescalePoint Λ p), NaturalAxisBridge.partialEta B (NaturalProfile.rescalePoint Λ p)]

theorem NavierStokes.NaturalEntrance.sourceJets_eq {ε : ℝ} (hε : 0 < ε) (x : CoefficientPair ε) {p : ℝ × ℝ} (hp : p ∈ AxisEvaluation.strip NaturalAxisCoefficients.window 20) : sourceJets hε x p = ![AxisEvaluation.profile NaturalAxisCoefficients.window ε x.1 p, NaturalAxisBridge.partialY (AxisEvaluation.profile NaturalAxisCoefficients.window ε x.1) p, NaturalAxisBridge.partialEta (AxisEvaluation.profile NaturalAxisCoefficients.window ε x.1) p, AxisEvaluation.profile NaturalAxisCoefficients.window ε x.2 p, AxisEvaluation.profile NaturalAxisCoefficients.window ε ((AxisOperators.average NaturalAxisCoefficients.window hε) x.2) p, NaturalAxisBridge.partialEta (AxisEvaluation.profile NaturalAxisCoefficients.window ε ((AxisOperators.average NaturalAxisCoefficients.window hε) x.2)) p]

noncomputable def NavierStokes.NaturalEntrance.angularField (h j σ Λ C : ℝ) {ε : ℝ} (x : CoefficientPair ε) : ℝ × ℝ → ℝ

Angular field, given by angularProfile (realAmplitude h j σ Λ C) Λ (AxisEvaluation.profile window ε x.1).

Equations

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

noncomputable def NavierStokes.NaturalEntrance.axialField (j Λ : ℝ) {ε : ℝ} (x : CoefficientPair ε) : ℝ × ℝ → ℝ

Axial field, given by affineProfile (NaturalAxisData.U j) (1 / Λ) Λ (AxisEvaluation.profile window ε x.2).

Equations

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

noncomputable def NavierStokes.NaturalEntrance.averageField (j Λ : ℝ) {ε : ℝ} (hε : 0 < ε) (x : CoefficientPair ε) : ℝ × ℝ → ℝ

Average field, given by affineProfile (NaturalAxisData.U j) (1 / Λ) Λ (AxisEvaluation.profile window ε (AxisOperators.average window hε x.2)).

Equations

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

theorem NavierStokes.NaturalEntrance.Sq_coefficient_identity {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (x : CoefficientPair d.coefficients.epsilon) (hΛ : 0 < Λ) (hC : 0 < C) {p : ℝ × ℝ} (hp : p ∈ NaturalProfile.domain Λ) (hval : 1 / 8 ≤ AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon x.1 (NaturalProfile.rescalePoint Λ p)) : Sq h (angularField h j σ Λ C x) (axialField j Λ x) (averageField j Λ ⋯ x) p = NaturalAxisData.L h p.2 * Λ * NaturalAxisData.chi h j σ p.2 + sourceRemainder h j σ (NaturalProfile.rescalePoint Λ p) (1 / Λ) (sourceJets ⋯ x (NaturalProfile.rescalePoint Λ p))

theorem NavierStokes.NaturalEntrance.physical_mem_domain {Λ X η : ℝ} (hY0 : 0 ≤ Λ * X) (hY1 : Λ * X ≤ 41 / 10) (hη : η ∈ Set.Icc (-1) 1) : (X, η) ∈ NaturalProfile.domain Λ

theorem NavierStokes.NaturalEntrance.p1_pos_of_source {h j Λ R η : ℝ} {P0 a : ℝ → ℝ} {f U V Pr : ℝ × ℝ → ℝ} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a f U V Pr) (hΛ : 0 < Λ) (hR : 0 < R) (hYR : Λ * R ≤ 41 / 10) (hη : η ∈ Set.Icc (-1) 1) (hL : 0 < NaturalAxisData.L h η) (hpos : ∀ X ∈ Set.Icc 0 R, 0 < f (X, η)) (hsource : ∀ X ∈ Set.Icc 0 R, 0 < Sq h f U V (X, η)) : 0 < p1 f (R, η)

The source estimate forces the actual logarithmic radial slope to be strictly positive on the regular branch, including every positive radius up to the entrance.

theorem NavierStokes.NaturalEntrance.regularInverse_one_constant {ε : ℝ} (hε : 0 < ε) (A : ↥(AxisCoefficientSpace.AxisSpace NaturalAxisCoefficients.window ε)) (hA : NaturalAxisBridge.RadiallyConstant NaturalAxisCoefficients.window ε A) (Y : ℝ) {η : ℝ} (hη : η ∈ NaturalAxisCoefficients.window.interval) : AxisEvaluation.profile NaturalAxisCoefficients.window ε ((AxisOperators.regularInverse NaturalAxisCoefficients.window hε 1 regularInverse_one_constant._proof_1) A) (Y, η) = Y * NaturalAxisBridge.inputValue NaturalAxisCoefficients.window ε A η

Applying the actual regular inverse to radially constant data gives exactly its degree-one polynomial.

theorem NavierStokes.NaturalEntrance.reference_u_value {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (Y : ℝ) {η : ℝ} (hη : η ∈ NaturalAxisCoefficients.window.interval) : AxisEvaluation.profile NaturalAxisCoefficients.window v.epsilon (referencePair v).2 (Y, η) = -(Y * NaturalAxisData.Z h j P0 η / (2 * NaturalAxisData.L h η))

theorem NavierStokes.NaturalEntrance.reference_u_derivative {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) {p : ℝ × ℝ} (hη : p.2 ∈ NaturalAxisCoefficients.window.interval) : NaturalAxisBridge.partialY (AxisEvaluation.profile NaturalAxisCoefficients.window v.epsilon (referencePair v).2) p = -NaturalAxisData.Z h j P0 p.2 / (2 * NaturalAxisData.L h p.2)

theorem NavierStokes.NaturalEntrance.coefficient_phi_lower {h j σ Λ K : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (hσ : 0 < σ) (hK : 0 ≤ K) (hscale : AxisReference.stabilityScale v.epsilon K ≤ Λ) (x : CoefficientPair v.epsilon) (hx : ‖x - referencePair v‖ ≤ K / (2 * Λ)) {Y η : ℝ} (hY0 : 0 ≤ Y) (hY1 : Y ≤ 41 / 10) (hη : η ∈ Set.Ioo NaturalAxisCoefficients.window.left NaturalAxisCoefficients.window.right) : 1 / 8 < AxisEvaluation.profile NaturalAxisCoefficients.window v.epsilon x.1 (Y, η)

theorem NavierStokes.NaturalEntrance.actual_source_lower {h j σ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) {K : ℝ} (hK : 0 ≤ K) : ∃ (M : ℝ), 0 < M ∧ ∀ (Λ : ℝ), M ≤ Λ → ∀ (C : ℝ), 0 < C → ∀ (x : CoefficientPair d.coefficients.epsilon), ‖x - referencePair d.coefficients‖ ≤ K / (2 * Λ) → ∀ (p : ℝ × ℝ), NaturalProfile.rescalePoint Λ p ∈ entranceSet → 19 / 20 * NaturalAxisData.L h p.2 * Λ * NaturalAxisData.chi h j σ p.2 + 5 / 2 < Sq h (angularField h j σ Λ C x) (axialField j Λ x) (averageField j Λ ⋯ x) p

The quantitative source inequality is proved for every actual coefficient-space profile in the solver's error ball. The scale is chosen before the normalization C.

theorem NavierStokes.NaturalEntrance.axialField_partialY {j Λ ε : ℝ} (hε : 0 < ε) (hΛ : Λ ≠ 0) (x : CoefficientPair ε) {p : ℝ × ℝ} (hp : p ∈ NaturalProfile.domain Λ) : NaturalAxisBridge.partialY (axialField j Λ x) p = NaturalAxisBridge.partialY (AxisEvaluation.profile NaturalAxisCoefficients.window ε x.2) (NaturalProfile.rescalePoint Λ p)

theorem NavierStokes.NaturalEntrance.ns_error {h j σ Λ K : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (hΛ : 0 < Λ) (_hK : 0 ≤ K) (x : CoefficientPair v.epsilon) (hx : ‖x - referencePair v‖ ≤ K / (2 * Λ)) {p : ℝ × ℝ} (hp : NaturalProfile.rescalePoint Λ p ∈ entranceSet) (hL : NaturalAxisData.L h p.2 ≠ 0) : |ns (axialField j Λ x) p - NaturalAxisData.Z h j P0 p.2 / NaturalAxisData.L h p.2| ≤ AxisEvaluation.jetBound v.epsilon 5 1 0 * K / Λ

The actual axial slope converges uniformly to the explicitly computed reference slope, with the coefficient-space error constant.

theorem NavierStokes.NaturalEntrance.L_le_one {h j : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) (η : ℝ) : NaturalAxisData.L h η ≤ 1

theorem NavierStokes.NaturalEntrance.ns_separated {h j σ Λ K δ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (hsmall : NaturalAxisData.SmallParameters h j) (hK : 0 ≤ K) (hδ : 0 < δ) (hscale : 1 + 2 * AxisEvaluation.jetBound v.epsilon 5 1 0 * K / δ ≤ Λ) (x : CoefficientPair v.epsilon) (hx : ‖x - referencePair v‖ ≤ K / (2 * Λ)) {p : ℝ × ℝ} (hp : NaturalProfile.rescalePoint Λ p ∈ entranceSet) (hZ : δ < |NaturalAxisData.Z h j P0 p.2|) : δ / 2 < |ns (axialField j Λ x) p|

Where Z* is separated from zero, the actual axial shear is separated from zero uniformly in the normalization.

noncomputable def NavierStokes.NaturalEntrance.profileBound {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) : ℝ

Profile bound, given by 1 + AxisEvaluation.jetBound v.epsilon 5 0 0 * (‖referencePair v‖ + 1).

Equations

• NavierStokes.NaturalEntrance.profileBound v = 1 + NavierStokes.AxisEvaluation.jetBound v.epsilon 5 0 0 * (‖NavierStokes.NaturalEntrance.referencePair v‖ + 1)

theorem NavierStokes.NaturalEntrance.profileBound_pos {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) : 0 < profileBound v

theorem NavierStokes.NaturalEntrance.coefficient_profile_le {h j σ : ℝ} {P0 : ℝ → ℝ} (v : NaturalAxisCoefficients.CoefficientFamily h j σ P0) (x : CoefficientPair v.epsilon) (hx : ‖x - referencePair v‖ ≤ 1) {p : ℝ × ℝ} (hp : |p.1| ≤ 5) : |AxisEvaluation.profile NaturalAxisCoefficients.window v.epsilon x.1 p| ≤ profileBound v

theorem NavierStokes.NaturalEntrance.realAmplitude_le_threshold {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hΛ : 0 ≤ Λ) (hC : 0 < C) {η : ℝ} (hη : η ∈ NaturalAxisCoefficients.window.interval) : NaturalAxisCoefficients.realAmplitude h j σ Λ C η ≤ d.normalizationThreshold Λ / C

noncomputable def NavierStokes.NaturalEntrance.entranceNormalization {h j σ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (Λ δ : ℝ) : ℝ

The normalization threshold is selected only after the scale. It retains the analytic-amplitude threshold and supplies a uniform small swirl bound without changing any coefficient-space constants.

Equations

• NavierStokes.NaturalEntrance.entranceNormalization d Λ δ = d.normalizationThreshold Λ * (1 + 100 * Λ * NavierStokes.NaturalEntrance.profileBound d.coefficients / δ)

theorem NavierStokes.NaturalEntrance.entranceNormalization_ge {h j σ Λ δ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hΛ : 0 < Λ) (hδ : 0 < δ) : d.normalizationThreshold Λ ≤ entranceNormalization d Λ δ

theorem NavierStokes.NaturalEntrance.angularField_small {h j σ Λ C δ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hΛ : 0 < Λ) (hδ : 0 < δ) (hC : entranceNormalization d Λ δ ≤ C) (x : CoefficientPair d.coefficients.epsilon) (hx : ‖x - referencePair d.coefficients‖ ≤ 1) {p : ℝ × ℝ} (hp : NaturalProfile.rescalePoint Λ p ∈ entranceSet) : 100 * Λ * angularField h j σ Λ C x p ≤ δ

theorem NavierStokes.NaturalEntrance.second_coordinate_large {Λ δ f n : ℝ} (hΛ : 1 ≤ Λ) (hδ : 0 < δ) (hf : 0 < f) (hsmall : 100 * Λ * f ≤ δ) (hn : δ / 2 < |n|) : (6 / 5) ^ 2 < (4 / Λ * n / (√(2 * (4 / Λ)) * f)) ^ 2

structure NavierStokes.NaturalEntrance.CoefficientProfile {h j σ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (Λ C : ℝ) : Type

A natural profile with its actual coefficient-space witness retained. The witness supplies all radial and parameter jet bounds needed by later continuation estimates.

• family : NaturalProfile.ProfileFamily d Λ C

  Family of CoefficientProfile, of type ProfileFamily d Λ C.

• coefficients : CoefficientPair d.coefficients.epsilon

  Coefficients of CoefficientProfile, of type CoefficientPair d.coefficients.epsilon.

• phi_eq : self.family.phi = AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon self.coefficients.1
• u_eq : self.family.u = AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon self.coefficients.2
• average_eq : self.family.average = AxisEvaluation.profile NaturalAxisCoefficients.window d.coefficients.epsilon ((AxisOperators.average NaturalAxisCoefficients.window ⋯) self.coefficients.2)
• norm_ball : ‖self.coefficients - referencePair d.coefficients‖ ≤ 1
• norm_error : ‖self.coefficients - referencePair d.coefficients‖ ≤ NaturalProfile.profileErrorConstant d / (2 * Λ)
• scaled : NaturalAxisBridge.IsScaledSolution NaturalAxisCoefficients.window (NaturalProfile.actualData h j σ P0) (1 / Λ) (NaturalAxisCoefficients.realAmplitude h j σ Λ C) self.family.phi self.family.u self.family.average self.family.pressure

theorem NavierStokes.NaturalEntrance.CoefficientProfile.f_eq {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : CoefficientProfile d Λ C) : F.family.f = angularField h j σ Λ C F.coefficients

theorem NavierStokes.NaturalEntrance.CoefficientProfile.U_eq {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : CoefficientProfile d Λ C) : F.family.U = axialField j Λ F.coefficients

theorem NavierStokes.NaturalEntrance.CoefficientProfile.Ubar_eq {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : CoefficientProfile d Λ C) : F.family.Ubar = averageField j Λ ⋯ F.coefficients

theorem NavierStokes.NaturalEntrance.profileErrorConstant_nonneg {h j σ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) : 0 ≤ NaturalProfile.profileErrorConstant d

theorem NavierStokes.NaturalEntrance.exists_coefficientProfile {h j σ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) (hP0 : ContDiff ℝ (↑⊤) P0) : ∃ (M : ℝ), 0 < M ∧ ∀ (Λ : ℝ), M ≤ Λ → ∀ (C : ℝ), d.normalizationThreshold Λ ≤ C → Nonempty (CoefficientProfile d Λ C)

The fixed-point theorem constructs the retained witness uniformly throughout the full allowed normalization range.

theorem NavierStokes.NaturalEntrance.CoefficientProfile.p1_pos {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : CoefficientProfile d Λ C) (hsmall : NaturalAxisData.SmallParameters h j) (hΛ : 0 < Λ) (hsource : ∀ (p : ℝ × ℝ), NaturalProfile.rescalePoint Λ p ∈ entranceSet → 0 < Sq h F.family.f F.family.U F.family.Ubar p) {p : ℝ × ℝ} (hp : NaturalProfile.rescalePoint Λ p ∈ entranceSet) (hX : 0 < p.1) : 0 < p1 F.family.f p

theorem NavierStokes.NaturalEntrance.CoefficientProfile.cone_at_four {h j σ Λ C δ : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : CoefficientProfile d Λ C) (hsmall : NaturalAxisData.SmallParameters h j) (hδ : 0 < δ) (hΛ : 1 ≤ Λ) (hscale : 1 + 2 * AxisEvaluation.jetBound d.coefficients.epsilon 5 1 0 * NaturalProfile.profileErrorConstant d / δ ≤ Λ) (hC : entranceNormalization d Λ δ ≤ C) (hcut : ∀ η ∈ Set.Icc (-1) 1, |NaturalAxisData.Z h j P0 η| ≤ δ → 99 / 100 < NaturalAxisData.chi h j σ η) {η : ℝ} (hη : η ∈ Set.Icc (-1) 1) (hp1 : 0 < p1 F.family.f (4 / Λ, η)) : 9 / 4 < coneSize F.family.f F.family.U (4 / Λ, η)

structure NavierStokes.NaturalEntrance.EntranceProfile {h j σ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (Λ C : ℝ) : Type

The actual natural profiles satisfy the entrance test, with a fixed strict cone margin and their complete coefficient-space witness.

• profile : CoefficientProfile d Λ C

  Profile of EntranceProfile, of type CoefficientProfile d Λ C.

• source_lower (p : ℝ × ℝ) : NaturalProfile.rescalePoint Λ p ∈ entranceSet → 19 / 20 * NaturalAxisData.L h p.2 * Λ * NaturalAxisData.chi h j σ p.2 + 5 / 2 < Sq h self.profile.family.f self.profile.family.U self.profile.family.Ubar p
• slope_positive (p : ℝ × ℝ) : NaturalProfile.rescalePoint Λ p ∈ entranceSet → 0 < p.1 → 0 < p1 self.profile.family.f p
• cone_margin (η : ℝ) : η ∈ Set.Icc (-1) 1 → 9 / 4 < coneSize self.profile.family.f self.profile.family.U (4 / Λ, η)

theorem NavierStokes.NaturalEntrance.exists_entranceProfile {h j σ δ : ℝ} {P0 : ℝ → ℝ} (d : NaturalAxisCoefficients.AnalyticInputs h j σ P0) (hsmall : NaturalAxisData.SmallParameters h j) (hσ : 0 < σ) (hP0 : ContDiff ℝ (↑⊤) P0) (hδ : 0 < δ) (hcut : ∀ η ∈ Set.Icc (-1) 1, |NaturalAxisData.Z h j P0 η| ≤ δ → 99 / 100 < NaturalAxisData.chi h j σ η) : ∃ (M : ℝ), 0 < M ∧ ∀ (Λ : ℝ), M ≤ Λ → ∀ (C : ℝ), entranceNormalization d Λ δ ≤ C → Nonempty (EntranceProfile d Λ C)

A single large scale works for every subsequent sufficiently large normalization. Both choices are made from the constructed analytic inputs.

theorem NavierStokes.NaturalEntrance.ideal_prefix_entranceProfile {h j : ℝ} (hsmall : NaturalAxisData.SmallParameters h j) {g a : ℝ → ℝ} {cap B : ℝ} (hp : PressureDatum.Admissible g a cap) (hB : 2 ≤ B) (hg : ∀ y ≤ 0, g y = B ^ 2 * Real.exp (1 / 5 * y)) (ha : ∀ y ≤ 0, a y = 1) : ∃ (δ : ℝ) (σ : ℝ), 0 < δ ∧ 0 < σ ∧ ∃ (d : NaturalAxisCoefficients.AnalyticInputs h j σ (PressureDatum.pressure g a)) (M : ℝ), 0 < M ∧ ∀ (Λ : ℝ), M ≤ Λ → ∀ (C : ℝ), entranceNormalization d Λ δ ≤ C → Nonempty (EntranceProfile d Λ C)

Ideal-prefix pressure data produce the actual initial stress-free cone test in the prescribed order: cutoff, common analytic radius, scale, and only then normalization.

theorem NavierStokes.NaturalEntrance.angular_flux_integral {g : ℝ → ℝ} (L R : ℝ) (hg : ∀ x ∈ Set.uIcc 0 R, ContDiffAt ℝ 2 g x) : ∫ (x : ℝ) in 0..R, -4 * L * x * (x * deriv (deriv g) x + 2 * deriv g x) = -4 * L * R ^ 2 * deriv g R

theorem NavierStokes.NaturalEntrance.axial_flux_integral {g : ℝ → ℝ} (L R : ℝ) (hg : ∀ x ∈ Set.uIcc 0 R, ContDiffAt ℝ 2 g x) : ∫ (x : ℝ) in 0..R, -2 * L * (x * deriv (deriv g) x + deriv g x) = -2 * L * R * deriv g R

noncomputable def NavierStokes.NaturalEntrance.regularAngularLag (h : ℝ) (f U V : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

The regular angular primitive of the actual source. This is the manuscript's Q_s, before multiplication by X/L.

Equations

• NavierStokes.NaturalEntrance.regularAngularLag h f U V p = (∫ (x : ℝ) in 0..p.1, 2 * x * f (x, p.2) * NavierStokes.NaturalEntrance.Sq h f U V (x, p.2)) / (p.1 * (2 * p.1 * f p))

theorem NavierStokes.NaturalEntrance.angular_source_integral {h j Λ : ℝ} {P0 a : ℝ → ℝ} {f U V Pr : ℝ × ℝ → ℝ} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a f U V Pr) (hΛ : 0 < Λ) {p : ℝ × ℝ} (hp : p ∈ NaturalProfile.domain Λ) (hf : ∀ x ∈ Set.uIcc 0 p.1, f (x, p.2) ≠ 0) : ∫ (x : ℝ) in 0..p.1, 2 * x * f (x, p.2) * Sq h f U V (x, p.2) = -4 * NaturalAxisData.L h p.2 * p.1 ^ 2 * NaturalAxisBridge.partialY f p

theorem NavierStokes.NaturalEntrance.regularAngularLag_eq {h j Λ : ℝ} {P0 a : ℝ → ℝ} {f U V Pr : ℝ × ℝ → ℝ} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a f U V Pr) (hΛ : 0 < Λ) {p : ℝ × ℝ} (hp : p ∈ NaturalProfile.domain Λ) (hX : p.1 ≠ 0) (hf : ∀ x ∈ Set.uIcc 0 p.1, f (x, p.2) ≠ 0) : regularAngularLag h f U V p = -2 * NaturalAxisData.L h p.2 * NaturalAxisBridge.partialY f p / f p

theorem NavierStokes.NaturalEntrance.p1_eq_scaled_regularAngularLag {h j Λ : ℝ} {P0 a : ℝ → ℝ} {f U V Pr : ℝ × ℝ → ℝ} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a f U V Pr) (hΛ : 0 < Λ) {p : ℝ × ℝ} (hp : p ∈ NaturalProfile.domain Λ) (hX : p.1 ≠ 0) (hL : NaturalAxisData.L h p.2 ≠ 0) (hf : ∀ x ∈ Set.uIcc 0 p.1, f (x, p.2) ≠ 0) : p1 f p = p.1 * regularAngularLag h f U V p / NaturalAxisData.L h p.2

The positive first coordinate is the actual scaled regular lag, not an independently supplied slope.

noncomputable def NavierStokes.NaturalEntrance.Sn (h : ℝ) (U V Pr : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Sn as an element of ℝ.

Equations

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

noncomputable def NavierStokes.NaturalEntrance.regularAxialLag (h : ℝ) (U V Pr : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Regular axial lag, given by (∫ x in (0 : ℝ)..p.1, Sn h U V Pr (x, p.2)) / p.1.

Equations

• NavierStokes.NaturalEntrance.regularAxialLag h U V Pr p = (∫ (x : ℝ) in 0..p.1, NavierStokes.NaturalEntrance.Sn h U V Pr (x, p.2)) / p.1

theorem NavierStokes.NaturalEntrance.Sn_eq_radial {h j Λ : ℝ} {P0 a : ℝ → ℝ} {f U V Pr : ℝ × ℝ → ℝ} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a f U V Pr) {p : ℝ × ℝ} (hp : p ∈ NaturalProfile.domain Λ) : Sn h U V Pr p = -2 * NaturalAxisData.L h p.2 * NaturalAxisBridge.radialDifferential 1 U p

theorem NavierStokes.NaturalEntrance.axial_source_integral {h j Λ : ℝ} {P0 a : ℝ → ℝ} {f U V Pr : ℝ × ℝ → ℝ} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a f U V Pr) (hΛ : 0 < Λ) {p : ℝ × ℝ} (hp : p ∈ NaturalProfile.domain Λ) : ∫ (x : ℝ) in 0..p.1, Sn h U V Pr (x, p.2) = -2 * NaturalAxisData.L h p.2 * p.1 * NaturalAxisBridge.partialY U p

theorem NavierStokes.NaturalEntrance.regularAxialLag_eq {h j Λ : ℝ} {P0 a : ℝ → ℝ} {f U V Pr : ℝ × ℝ → ℝ} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a f U V Pr) (hΛ : 0 < Λ) {p : ℝ × ℝ} (hp : p ∈ NaturalProfile.domain Λ) (hX : p.1 ≠ 0) : regularAxialLag h U V Pr p = -2 * NaturalAxisData.L h p.2 * NaturalAxisBridge.partialY U p

theorem NavierStokes.NaturalEntrance.ns_eq_scaled_regularAxialLag {h j Λ : ℝ} {P0 a : ℝ → ℝ} {f U V Pr : ℝ × ℝ → ℝ} (hs : NaturalProfile.IsNaturalSolution h j Λ P0 a f U V Pr) (hΛ : 0 < Λ) {p : ℝ × ℝ} (hp : p ∈ NaturalProfile.domain Λ) (hX : p.1 ≠ 0) (hL : NaturalAxisData.L h p.2 ≠ 0) : ns U p = regularAxialLag h U V Pr p / NaturalAxisData.L h p.2

theorem NavierStokes.NaturalEntrance.EntranceProfile.regular_lag_coordinates {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : EntranceProfile d Λ C) (hsmall : NaturalAxisData.SmallParameters h j) (hΛ : 0 < Λ) {p : ℝ × ℝ} (hp : NaturalProfile.rescalePoint Λ p ∈ entranceSet) (hX : 0 < p.1) : p1 F.profile.family.f p = p.1 * regularAngularLag h F.profile.family.f F.profile.family.U F.profile.family.Ubar p / NaturalAxisData.L h p.2 ∧ p2 F.profile.family.f F.profile.family.U p = p.1 * regularAxialLag h F.profile.family.U F.profile.family.Ubar F.profile.family.Pi p / (NaturalAxisData.L h p.2 * angularVelocity F.profile.family.f p)

The constructed entrance coordinates are the dimensionless stocks of the actual regular angular and axial primitives.

theorem NavierStokes.NaturalEntrance.EntranceProfile.regular_cone_at_four {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (F : EntranceProfile d Λ C) (hsmall : NaturalAxisData.SmallParameters h j) (hΛ : 0 < Λ) {η : ℝ} (hη : η ∈ Set.Icc (-1) 1) : have p := (4 / Λ, η); have q := p.1 * regularAngularLag h F.profile.family.f F.profile.family.U F.profile.family.Ubar p / NaturalAxisData.L h η; have n := p.1 * regularAxialLag h F.profile.family.U F.profile.family.Ubar F.profile.family.Pi p / (NaturalAxisData.L h η * angularVelocity F.profile.family.f p); 9 / 4 < q + n ^ 2 / q

The strict entrance inequality also holds when written entirely in terms of the source-integral stocks, with no independent stock hypotheses.