Identification and positivity of the actual natural-axis reference

The reference is the image of the unit datum under the constructed Banach-space resolvent. Its coefficient recurrence identifies its evaluation with the entire leading series. Uniform estimates for the actual nonlinear profiles then preserve positivity and a strict logarithmic-slope margin at one common parameter scale.

Convergent series for the leading natural axis profile

This module concerns the leading scaled linear equation of Proposition 5.1, not the nonlinear perturbation or the claimed uniform remainder estimates.

Algebraic checks for the natural axis profile

These theorems concern the scaled leading equations and the two explicit truncations in Proposition 5.1 of the candidate manuscript. They do not establish convergence of a formal power series, the nonlinear remainder estimates, the contraction argument, or the full profile's cone margin.

def NavierStokes.AxisProfile.radialOperatorCoeff (m : ℕ) (a : ℕ → ℝ) (n : ℕ) : ℝ

The coefficient of Y^n in (Y ∂YY + m ∂Y) a, at the formal coefficient level.

Equations

• NavierStokes.AxisProfile.radialOperatorCoeff m a n = (↑n + 1) * (↑n + ↑m) * a (n + 1)

noncomputable def NavierStokes.AxisProfile.radialInverseCoeff (m : ℕ) (f : ℕ → ℝ) : ℕ → ℝ

The regular zero-datum formal inverse used in the scaled equations.

Equations

• NavierStokes.AxisProfile.radialInverseCoeff m f 0 = 0
• NavierStokes.AxisProfile.radialInverseCoeff m f n.succ = f n / ((↑n + 1) * (↑n + ↑m))

@[simp]

theorem NavierStokes.AxisProfile.radialInverseCoeff_zero (m : ℕ) (f : ℕ → ℝ) : radialInverseCoeff m f 0 = 0

theorem NavierStokes.AxisProfile.radialOperator_inverse (m : ℕ) (hm : 0 < m) (f : ℕ → ℝ) (n : ℕ) : radialOperatorCoeff m (radialInverseCoeff m f) n = f n

For positive m, the stated shift really inverts the formal radial operator. No assertion about convergence is implicit in this theorem.

noncomputable def NavierStokes.AxisProfile.profileCoeff (χ : ℝ) (n : ℕ) : ℝ

The leading angular series coefficient from Proposition 5.1: (-χ/2)^n / (n! (n+1)!).

Equations

• NavierStokes.AxisProfile.profileCoeff χ n = (-χ / 2) ^ n / (↑n.factorial * ↑(n + 1).factorial)

@[simp]

theorem NavierStokes.AxisProfile.profileCoeff_zero (χ : ℝ) : profileCoeff χ 0 = 1

theorem NavierStokes.AxisProfile.profileCoeff_recurrence (χ : ℝ) (n : ℕ) : 2 * (↑n + 1) * (↑n + 2) * profileCoeff χ (n + 1) = -χ * profileCoeff χ n

Exact recurrence for the displayed regular series.

theorem NavierStokes.AxisProfile.profileCoeff_scaled_equation (χ : ℝ) (n : ℕ) : 2 * radialOperatorCoeff 2 (profileCoeff χ) n = -χ * profileCoeff χ n

The formal series solves the leading angular equation coefficient by coefficient. This does not identify an analytic solution.

theorem NavierStokes.AxisProfile.weighted_profileCoeff (χ : ℝ) (n : ℕ) : (↑n + 1) * profileCoeff χ n = (-χ / 2) ^ n / ↑n.factorial ^ 2

The coefficient transformation for the formal combination f + Yf' is exactly the factorial-square series used for the sign test.

noncomputable def NavierStokes.AxisProfile.cubicLower (t : ℝ) : ℝ

The cubic lower truncation in the manuscript, with t = Yχ/2.

Equations

• NavierStokes.AxisProfile.cubicLower t = 1 - t / 2 + t ^ 2 / 12 - t ^ 3 / 144

noncomputable def NavierStokes.AxisProfile.quarticUpper (t : ℝ) : ℝ

The quartic upper truncation for f₀ + s f₀', in the variable t=s/2.

Equations

• NavierStokes.AxisProfile.quarticUpper t = 1 - t + t ^ 2 / 4 - t ^ 3 / 36 + t ^ 4 / 576

theorem NavierStokes.AxisProfile.cubicLower_gt_quarter (t : ℝ) (ht : t ≤ 41 / 20) : 1 / 4 < cubicLower t

A rational positivity certificate for the lower truncation on t ≤ 2.05; the natural application also has t ≥ 0.

theorem NavierStokes.AxisProfile.quarticUpper_lt_neg_eighteen_hundredths (t : ℝ) (hlo : 99 / 50 ≤ t) (hhi : t ≤ 2) : quarticUpper t < -(18 / 100)

A direct rational verification of the numerical strict inequality used for the initial cone margin.

theorem NavierStokes.AxisProfile.first_four_terms_eq_cubic (χ Y : ℝ) : profileCoeff χ 0 + profileCoeff χ 1 * Y + profileCoeff χ 2 * Y ^ 2 + profileCoeff χ 3 * Y ^ 3 = cubicLower (Y * χ / 2)

The first four actual displayed series terms, for a concrete link between the coefficient calculation and the lower polynomial.

theorem NavierStokes.AxisProfile.first_five_weighted_terms_eq_quartic (χ Y : ℝ) : profileCoeff χ 0 + 2 * profileCoeff χ 1 * Y + 3 * profileCoeff χ 2 * Y ^ 2 + 4 * profileCoeff χ 3 * Y ^ 3 + 5 * profileCoeff χ 4 * Y ^ 4 = quarticUpper (Y * χ / 2)

The first five terms of the formal f + Yf' series give exactly the quartic sign-test polynomial.

noncomputable def NavierStokes.AxisProfile.leadingAxial (Z L Y : ℝ) : ℝ

The leading axial profile displayed in the scaled construction.

Equations

• NavierStokes.AxisProfile.leadingAxial Z L Y = -Y * Z / (2 * L)

theorem NavierStokes.AxisProfile.leadingAxial_zero (Z L : ℝ) : leadingAxial Z L 0 = 0

theorem NavierStokes.AxisProfile.hasDerivAt_leadingAxial (Z L Y : ℝ) : HasDerivAt (leadingAxial Z L) (-Z / (2 * L)) Y

theorem NavierStokes.AxisProfile.hasDerivAt_leadingAxial_derivative (Z L Y : ℝ) : HasDerivAt (fun (x : ℝ) => -Z / (2 * L)) 0 Y

The derivative of the linear leading axial solution is constant.

theorem NavierStokes.AxisProfile.deriv_leadingAxial (Z L : ℝ) : deriv (leadingAxial Z L) = fun (x : ℝ) => -Z / (2 * L)

The derivative as a function, permitting a second differentiation.

theorem NavierStokes.AxisProfile.leadingAxial_scaled_equation (Z L Y : ℝ) (hL : L ≠ 0) : 2 * (Y * deriv (deriv (leadingAxial Z L)) Y + deriv (leadingAxial Z L) Y) = -Z / L

The linear leading axial profile satisfies the actual scaled ODE.

noncomputable def NavierStokes.AxisSeries.term (k n : ℕ) (t : ℝ) : ℝ

Terms of a family of entire factorial-denominator series.

Equations

• NavierStokes.AxisSeries.term k n t = (-t) ^ n / (↑n.factorial * ↑(n + k).factorial)

noncomputable def NavierStokes.AxisSeries.bessel (k : ℕ) (t : ℝ) : ℝ

The generalized leading series; the axis profile uses k=1.

Equations

• NavierStokes.AxisSeries.bessel k t = ∑' (n : ℕ), NavierStokes.AxisSeries.term k n t

theorem NavierStokes.AxisSeries.term_norm_le (k n : ℕ) (t R : ℝ) (hR : 0 ≤ R) (ht : |t| ≤ R) : ‖term k n t‖ ≤ R ^ n / ↑n.factorial

theorem NavierStokes.AxisSeries.summable_term (k : ℕ) (t : ℝ) : Summable fun (n : ℕ) => term k n t

Absolute summability, proved by comparison with the exponential series.

theorem NavierStokes.AxisSeries.summable_norm_term (k : ℕ) (t : ℝ) : Summable fun (n : ℕ) => ‖term k n t‖

theorem NavierStokes.AxisSeries.summable_term_tail (k j : ℕ) (t : ℝ) : Summable fun (n : ℕ) => term k (n + j) t

theorem NavierStokes.AxisSeries.hasDerivAt_term_succ (k n : ℕ) (t : ℝ) : HasDerivAt (term k (n + 1)) (-term (k + 1) n t) t

Differentiating a successor-index term cancels one factorial factor.

theorem NavierStokes.AxisSeries.bessel_eq_constant_add_tail (k : ℕ) (t : ℝ) : bessel k t = 1 / ↑k.factorial + ∑' (n : ℕ), term k (n + 1) t

theorem NavierStokes.AxisSeries.hasDerivAt_bessel (k : ℕ) (t : ℝ) : HasDerivAt (bessel k) (-bessel (k + 1) t) t

Differentiation of the convergent infinite series on every real point.

theorem NavierStokes.AxisSeries.deriv_bessel (k : ℕ) : deriv (bessel k) = fun (t : ℝ) => -bessel (k + 1) t

theorem NavierStokes.AxisSeries.term_contiguous (k n : ℕ) (t : ℝ) : term k (n + 1) t = (↑k + 1) * term (k + 1) (n + 1) t - t * term (k + 2) n t

A termwise contiguous relation, with the constant term removed.

theorem NavierStokes.AxisSeries.factorial_reciprocal (k : ℕ) : 1 / ↑k.factorial = (↑k + 1) * (1 / ↑(k + 1).factorial)

theorem NavierStokes.AxisSeries.bessel_contiguous (k : ℕ) (t : ℝ) : bessel k t = (↑k + 1) * bessel (k + 1) t - t * bessel (k + 2) t

The convergent sums satisfy the contiguous relation underlying the ODE.

theorem NavierStokes.AxisSeries.second_deriv_bessel (k : ℕ) (t : ℝ) : deriv (deriv (bessel k)) t = bessel (k + 2) t

theorem NavierStokes.AxisSeries.bessel_ode (k : ℕ) (t : ℝ) : t * deriv (deriv (bessel k)) t + (↑k + 1) * deriv (bessel k) t + bessel k t = 0

An actual differential equation for the infinite function.

theorem NavierStokes.AxisSeries.bessel_zero (k : ℕ) : bessel k 0 = 1 / ↑k.factorial

noncomputable def NavierStokes.AxisSeries.profile (χ Y : ℝ) : ℝ

The leading regular angular profile in the manuscript's scaled radius.

Equations

• NavierStokes.AxisSeries.profile χ Y = NavierStokes.AxisSeries.bessel 1 (χ / 2 * Y)

theorem NavierStokes.AxisSeries.profile_eq_tsum (χ Y : ℝ) : profile χ Y = ∑' (n : ℕ), (-χ * Y / 2) ^ n / (↑n.factorial * ↑(n + 1).factorial)

theorem NavierStokes.AxisSeries.profile_zero (χ : ℝ) : profile χ 0 = 1

theorem NavierStokes.AxisSeries.hasDerivAt_profile (χ Y : ℝ) : HasDerivAt (profile χ) (-(χ / 2) * bessel 2 (χ / 2 * Y)) Y

theorem NavierStokes.AxisSeries.deriv_profile (χ : ℝ) : deriv (profile χ) = fun (Y : ℝ) => -(χ / 2) * bessel 2 (χ / 2 * Y)

theorem NavierStokes.AxisSeries.second_deriv_profile (χ Y : ℝ) : deriv (deriv (profile χ)) Y = (χ / 2) ^ 2 * bessel 3 (χ / 2 * Y)

theorem NavierStokes.AxisSeries.profile_scaled_ode (χ Y : ℝ) : 2 * (Y * deriv (deriv (profile χ)) Y + 2 * deriv (profile χ) Y) = -χ * profile χ Y

The leading regular equation 2(YΦ''+2Φ') = -χΦ, for the actual sum.

theorem NavierStokes.AxisSeries.term_succ_ratio (k n : ℕ) (t : ℝ) : term k (n + 1) t = -t / ((↑n + 1) * (↑n + ↑k + 1)) * term k n t

The exact successive-term ratio, including its sign.

theorem NavierStokes.AxisSeries.term_sign (k n : ℕ) (t : ℝ) : term k n t = (-1) ^ n * term k n (-t)

theorem NavierStokes.AxisSeries.magnitude_tail_antitone (k j : ℕ) (hj : 1 ≤ j) (t : ℝ) (ht0 : 0 ≤ t) (ht : t ≤ 4) : Antitone fun (n : ℕ) => term k (n + j) (-t)

Once at least the zeroth term is removed, the remaining magnitudes decrease on 0 ≤ t ≤ 4, for every nonnegative factorial offset.

theorem NavierStokes.AxisSeries.cubic_tail_antitone (t : ℝ) (ht0 : 0 ≤ t) (ht : t ≤ 41 / 20) : Antitone fun (n : ℕ) => term 1 (n + 4) (-t)

The cubic tail is an instance of the preceding magnitude estimate.

theorem NavierStokes.AxisSeries.cubic_tail_nonneg (t : ℝ) (ht0 : 0 ≤ t) (ht : t ≤ 41 / 20) : 0 ≤ ∑' (n : ℕ), term 1 (n + 4) t

The infinite alternating tail following the cubic has nonnegative sum.

theorem NavierStokes.AxisSeries.cubic_lower_le_bessel (t : ℝ) (ht0 : 0 ≤ t) (ht : t ≤ 41 / 20) : AxisProfile.cubicLower t ≤ bessel 1 t

theorem NavierStokes.AxisSeries.bessel_one_gt_quarter (t : ℝ) (ht0 : 0 ≤ t) (ht : t ≤ 41 / 20) : 1 / 4 < bessel 1 t

A uniform positive lower bound for the actual infinite leading series.

theorem NavierStokes.AxisSeries.profile_gt_quarter (χ Y : ℝ) (hχ0 : 0 ≤ χ) (hχ1 : χ ≤ 1) (hY0 : 0 ≤ Y) (hY1 : Y ≤ 41 / 10) : 1 / 4 < profile χ Y

Positivity on the entire axis interval requested in Proposition 5.1, for the leading profile rather than its nonlinear perturbation.

theorem NavierStokes.AxisSeries.profile_pos (χ Y : ℝ) (hχ0 : 0 ≤ χ) (hχ1 : χ ≤ 1) (hY0 : 0 ≤ Y) (hY1 : Y ≤ 41 / 10) : 0 < profile χ Y

theorem NavierStokes.AxisSeries.alternating_tail_nonneg (k j : ℕ) (hj : 1 ≤ j) (t : ℝ) (ht0 : 0 ≤ t) (ht : t ≤ 4) : 0 ≤ ∑' (n : ℕ), (-1) ^ n * term k (n + j) (-t)

A convergent alternating tail beginning with its positive sign has nonnegative total, for every offset starting after at least one term.

theorem NavierStokes.AxisSeries.bessel_le_odd_partial_sum (k j : ℕ) (hj : 1 ≤ j) (hodd : Odd j) (t : ℝ) (ht0 : 0 ≤ t) (ht : t ≤ 4) : bessel k t ≤ ∑ n ∈ Finset.range j, term k n t

Every odd-length truncation with at least one term is an upper bound on the actual series on this interval.

theorem NavierStokes.AxisSeries.bessel_one_le_one (t : ℝ) (ht0 : 0 ≤ t) (ht : t ≤ 4) : bessel 1 t ≤ 1

theorem NavierStokes.AxisSeries.bessel_zero_lt_neg_eighteen_hundredths (t : ℝ) (ht0 : 99 / 50 ≤ t) (ht1 : t ≤ 2) : bessel 0 t < -(18 / 100)

The quartic upper bound controls the actual factorial-square series.

theorem NavierStokes.AxisSeries.bessel_one_add_mul_deriv (t : ℝ) : bessel 1 t + t * deriv (bessel 1) t = bessel 0 t

The derivative combination used in the manuscript's sign test is now an identity of differentiable infinite functions.

theorem NavierStokes.AxisSeries.bessel_one_log_slope_gt (t : ℝ) (ht0 : 99 / 50 ≤ t) (ht1 : t ≤ 2) : 236 / 100 < -2 * t * deriv (bessel 1) t / bessel 1 t

theorem NavierStokes.AxisSeries.profile_log_slope_at_four (χ : ℝ) (hχ0 : 99 / 100 ≤ χ) (hχ1 : χ ≤ 1) : 236 / 100 < -8 * deriv (profile χ) 4 / profile χ 4

The exact leading profile has the stated 2.36 slope margin at Y=4 when χ≥0.99. No perturbation estimate is asserted.

theorem NavierStokes.AxisReference.coefficient_naturalOperator_zero (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ A : ↥(AxisCoefficientSpace.AxisSpace I ε)) {η : ℝ} (hη : η ∈ I.interval) : AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) ((AxisResolvent.naturalOperator I hε χ) A) 0 η = 0

theorem NavierStokes.AxisReference.coefficient_naturalOperator_succ (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ A : ↥(AxisCoefficientSpace.AxisSpace I ε)) (hχ : NaturalAxisBridge.RadiallyConstant I ε χ) (n : ℕ) {η : ℝ} (hη : η ∈ I.interval) : AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) ((AxisResolvent.naturalOperator I hε χ) A) (n + 1) η = 1 / 2 * (AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) χ 0 η * AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) A n η / AxisWeightEstimates.radialDivisor 2 n)

theorem NavierStokes.AxisReference.reference_coefficient_zero (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ e : ↥(AxisCoefficientSpace.AxisSpace I ε)) {η : ℝ} (hη : η ∈ I.interval) (he : AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) e 0 η = 1) : AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) ((AxisResolvent.naturalResolvent I hε χ) e) 0 η = 1

The unit datum is preserved at the axis by the actual resolvent.

theorem NavierStokes.AxisReference.reference_coefficient_succ (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ e : ↥(AxisCoefficientSpace.AxisSpace I ε)) (hχ : NaturalAxisBridge.RadiallyConstant I ε χ) (he : NaturalAxisBridge.RadiallyConstant I ε e) (n : ℕ) {η : ℝ} (hη : η ∈ I.interval) : AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) ((AxisResolvent.naturalResolvent I hε χ) e) (n + 1) η = -AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) χ 0 η / 2 * AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) ((AxisResolvent.naturalResolvent I hε χ) e) n η / AxisWeightEstimates.radialDivisor 2 n

Every higher coefficient is forced by the resolvent equation; the recurrence is derived from the bounded operators, rather than postulated.

theorem NavierStokes.AxisReference.reference_coefficient (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ e : ↥(AxisCoefficientSpace.AxisSpace I ε)) (hχ : NaturalAxisBridge.RadiallyConstant I ε χ) (he : NaturalAxisBridge.RadiallyConstant I ε e) {η : ℝ} (hη : η ∈ I.interval) (he0 : AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) e 0 η = 1) (n : ℕ) : AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) ((AxisResolvent.naturalResolvent I hε χ) e) n η = (-AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) χ 0 η / 2) ^ n / (↑n.factorial * ↑(n + 1).factorial)

The constructed resolvent has the factorial coefficients of the regular Bessel-type reference.

theorem NavierStokes.AxisReference.reference_profile_eq_series (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ e : ↥(AxisCoefficientSpace.AxisSpace I ε)) (hχ : NaturalAxisBridge.RadiallyConstant I ε χ) (he : NaturalAxisBridge.RadiallyConstant I ε e) {η : ℝ} (hη : η ∈ I.interval) (he0 : AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) e 0 η = 1) (Y : ℝ) : AxisEvaluation.profile I ε ((AxisResolvent.naturalResolvent I hε χ) e) (Y, η) = AxisSeries.profile (AxisCoefficientSpace.coefficient I (AxisWeightEstimates.weight ε) χ 0 η) Y

Evaluation of the actual coefficient-space reference equals the entire leading series at every real radius.

theorem NavierStokes.AxisReference.referenceCoefficients_profile_eq_series (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (hd : NaturalAxisBridge.CompatibleData I ε χ d) {η : ℝ} (hη : η ∈ I.interval) (Y : ℝ) : AxisEvaluation.profile I ε (NaturalAxisBridge.referenceCoefficients I hε χ d).1 (Y, η) = AxisSeries.profile (NaturalAxisBridge.inputValue I ε χ η) Y

In particular, the leading pair used by the nonlinear existence theorem has exactly this angular series.

theorem NavierStokes.AxisReference.referenceCoefficients_deriv_Y_eq (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (hd : NaturalAxisBridge.CompatibleData I ε χ d) {η : ℝ} (hη : η ∈ I.interval) (Y : ℝ) : deriv (fun (y : ℝ) => AxisEvaluation.profile I ε (NaturalAxisBridge.referenceCoefficients I hε χ d).1 (y, η)) Y = deriv (AxisSeries.profile (NaturalAxisBridge.inputValue I ε χ η)) Y

theorem NavierStokes.AxisReference.referenceCoefficients_gt_quarter (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (hd : NaturalAxisBridge.CompatibleData I ε χ d) {η Y : ℝ} (hη : η ∈ I.interval) (hχ0 : 0 ≤ NaturalAxisBridge.inputValue I ε χ η) (hχ1 : NaturalAxisBridge.inputValue I ε χ η ≤ 1) (hY0 : 0 ≤ Y) (hY1 : Y ≤ 41 / 10) : 1 / 4 < AxisEvaluation.profile I ε (NaturalAxisBridge.referenceCoefficients I hε χ d).1 (Y, η)

The lower bound concerns the reference constructed by the resolvent, not a separately declared comparison function.

theorem NavierStokes.AxisReference.referenceCoefficients_log_slope_at_four (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (hd : NaturalAxisBridge.CompatibleData I ε χ d) {η : ℝ} (hη : η ∈ I.interval) (hχ99 : 99 / 100 ≤ NaturalAxisBridge.inputValue I ε χ η) (hχ1 : NaturalAxisBridge.inputValue I ε χ η ≤ 1) : 236 / 100 < -8 * deriv (fun (y : ℝ) => AxisEvaluation.profile I ε (NaturalAxisBridge.referenceCoefficients I hε χ d).1 (y, η)) 4 / AxisEvaluation.profile I ε (NaturalAxisBridge.referenceCoefficients I hε χ d).1 (4, η)

theorem NavierStokes.AxisReference.log_slope_stability {v₀ v d₀ d : ℝ} (hv₀ : 1 / 4 < v₀) (hvalue : |v - v₀| ≤ 1 / 1000) (hderiv : |d - d₀| ≤ 1 / 1000) (hslope : 236 / 100 < -8 * d₀ / v₀) : 1 / 8 < v ∧ 23 / 10 < -8 * d / v

Quantitative stability of the strict slope margin under simultaneous value and first-derivative errors of at most 1/1000.

theorem NavierStokes.AxisReference.scaled_error_le {C C₀ C₁ K Λ : ℝ} (hCsum : C ≤ C₀ + C₁) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hK : 0 ≤ K) (hΛ : 1 + 500 * (C₀ + C₁) * K ≤ Λ) : C * (K / (2 * Λ)) ≤ 1 / 1000

A single lower bound on the scale makes both evaluation constants small enough for positivity and logarithmic-slope stability.

noncomputable def NavierStokes.AxisReference.stabilityScale (ε K : ℝ) : ℝ

This explicit threshold controls both values and first radial derivatives on |Y|≤5, uniformly over the parameter interval.

Equations

• NavierStokes.AxisReference.stabilityScale ε K = 1 + 500 * (NavierStokes.AxisEvaluation.jetBound ε 5 0 0 + NavierStokes.AxisEvaluation.jetBound ε 5 1 0) * K

theorem NavierStokes.AxisReference.stabilityScale_pos {ε K : ℝ} (hε : 0 < ε) (hK : 0 ≤ K) : 0 < stabilityScale ε K

theorem NavierStokes.AxisReference.value_error_le (I : AxisCoefficientSpace.Window) {ε K Λ : ℝ} (hε : 0 < ε) (hK : 0 ≤ K) (hΛ : stabilityScale ε K ≤ Λ) {Φ u Φ₀ u₀ : ℝ × ℝ → ℝ} (herr : NaturalAxisBridge.UniformMixedError I ε (K / (2 * Λ)) Φ u Φ₀ u₀) {p : ℝ × ℝ} (hY : |p.1| ≤ 5) (hη : p.2 ∈ Set.Ioo I.left I.right) : |Φ p - Φ₀ p| ≤ 1 / 1000

theorem NavierStokes.AxisReference.radial_deriv_error_le (I : AxisCoefficientSpace.Window) {ε K Λ : ℝ} (hε : 0 < ε) (hK : 0 ≤ K) (hΛ : stabilityScale ε K ≤ Λ) {Φ u Φ₀ u₀ : ℝ × ℝ → ℝ} (herr : NaturalAxisBridge.UniformMixedError I ε (K / (2 * Λ)) Φ u Φ₀ u₀) {p : ℝ × ℝ} (hY : |p.1| ≤ 5) (hη : p.2 ∈ Set.Ioo I.left I.right) : |NaturalAxisBridge.partialY Φ p - NaturalAxisBridge.partialY Φ₀ p| ≤ 1 / 1000

theorem NavierStokes.AxisReference.positive_of_uniformMixedError (I : AxisCoefficientSpace.Window) {ε K Λ : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (hd : NaturalAxisBridge.CompatibleData I ε χ d) (hK : 0 ≤ K) (hΛ : stabilityScale ε K ≤ Λ) {Φ u u₀ : ℝ × ℝ → ℝ} (herr : NaturalAxisBridge.UniformMixedError I ε (K / (2 * Λ)) Φ u (AxisEvaluation.profile I ε (NaturalAxisBridge.referenceCoefficients I hε χ d).1) u₀) {Y η : ℝ} (hY0 : 0 ≤ Y) (hY1 : Y ≤ 41 / 10) (hη : η ∈ Set.Ioo I.left I.right) (hχ0 : 0 ≤ NaturalAxisBridge.inputValue I ε χ η) (hχ1 : NaturalAxisBridge.inputValue I ε χ η ≤ 1) : 1 / 8 < Φ (Y, η)

Uniform closeness to the actual reference preserves a positive margin on the full closed radial interval.

theorem NavierStokes.AxisReference.log_slope_of_uniformMixedError (I : AxisCoefficientSpace.Window) {ε K Λ : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (hd : NaturalAxisBridge.CompatibleData I ε χ d) (hK : 0 ≤ K) (hΛ : stabilityScale ε K ≤ Λ) {Φ u u₀ : ℝ × ℝ → ℝ} (herr : NaturalAxisBridge.UniformMixedError I ε (K / (2 * Λ)) Φ u (AxisEvaluation.profile I ε (NaturalAxisBridge.referenceCoefficients I hε χ d).1) u₀) {η : ℝ} (hη : η ∈ Set.Ioo I.left I.right) (hχ99 : 99 / 100 ≤ NaturalAxisBridge.inputValue I ε χ η) (hχ1 : NaturalAxisBridge.inputValue I ε χ η ≤ 1) : 23 / 10 < -8 * NaturalAxisBridge.partialY Φ (4, η) / Φ (4, η)

The same scale preserves a strict slope greater than 2.3 wherever the parameter coefficient is at least 0.99.

theorem NavierStokes.AxisReference.exists_positive_scaled_profiles (I : AxisCoefficientSpace.Window) {ε : ℝ} (hε : 0 < ε) (χ : ↥(AxisCoefficientSpace.AxisSpace I ε)) (d : AxisContraction.AxisData ↥(AxisCoefficientSpace.AxisSpace I ε)) (hd : NaturalAxisBridge.CompatibleData I ε χ d) (hχ : ∀ η ∈ I.interval, 0 ≤ NaturalAxisBridge.inputValue I ε χ η ∧ NaturalAxisBridge.inputValue I ε χ η ≤ 1) (M : ℝ) (hM : 0 ≤ M) : ∃ (Λ₀ : ℝ), 0 < Λ₀ ∧ ∀ (Λ : ℝ), Λ₀ ≤ Λ → ∀ (a : ↥(AxisCoefficientSpace.AxisSpace I ε)), ‖a‖ ≤ M → NaturalAxisBridge.RadiallyConstant I ε a → ∃ (Φ : ℝ × ℝ → ℝ) (u : ℝ × ℝ → ℝ) (B : ℝ × ℝ → ℝ) (P : ℝ × ℝ → ℝ), NaturalAxisBridge.IsScaledSolution I (NaturalAxisBridge.parameters I ε χ d) (1 / Λ) (NaturalAxisBridge.inputValue I ε a) Φ u B P ∧ NaturalAxisBridge.UniformMixedError I ε (NaturalAxisBridge.errorConstant I hε χ d M hM / (2 * Λ)) Φ u (AxisEvaluation.profile I ε (NaturalAxisBridge.referenceCoefficients I hε χ d).1) (AxisEvaluation.profile I ε (NaturalAxisBridge.referenceCoefficients I hε χ d).2) ∧ (∀ Y ∈ Set.Icc 0 (41 / 10), ∀ η ∈ Set.Ioo I.left I.right, 1 / 8 < Φ (Y, η)) ∧ ∀ η ∈ Set.Ioo I.left I.right, 99 / 100 ≤ NaturalAxisBridge.inputValue I ε χ η → 23 / 10 < -8 * NaturalAxisBridge.partialY Φ (4, η) / Φ (4, η)

One sufficiently large scale gives the actual smooth nonlinear profiles, all mixed-derivative estimates, uniform positivity, and the strict angular slope bound, simultaneously for the full amplitude norm ball.