Exact algebra of the stress cone

This formalizes the square-root criterion and quadratic equivalence in Lemma 3.5 of the candidate manuscript, together with the normalized factorization used in equation (11). It does not construct any stress profile.

noncomputable def NavierStokes.ConeAlgebra.coneBound (P J : ℝ) : ℝ

The lower root appearing in equation (10).

Equations

• NavierStokes.ConeAlgebra.coneBound P J = P + J ^ 2 / 4 - |J| * √((P - 2) / 2 + J ^ 2 / 16)

noncomputable def NavierStokes.ConeAlgebra.rootTerm (P J : ℝ) : ℝ

The discriminant term in the displayed root formula.

Equations

• NavierStokes.ConeAlgebra.rootTerm P J = |J| * √((P - 2) / 2 + J ^ 2 / 16)

theorem NavierStokes.ConeAlgebra.rootTerm_nonneg (P J : ℝ) : 0 ≤ rootTerm P J

theorem NavierStokes.ConeAlgebra.rootTerm_sq {P J : ℝ} (hP : 2 < P) : rootTerm P J ^ 2 = J ^ 2 * ((P - 2) / 2 + J ^ 2 / 16)

theorem NavierStokes.ConeAlgebra.boundary_polynomial (P J v : ℝ) : 2 * (P - v) ^ 2 - (v - 2) * J ^ 2 = 2 * v ^ 2 - (4 * P + J ^ 2) * v + 2 * P ^ 2 + 2 * J ^ 2

theorem NavierStokes.ConeAlgebra.square_difference (P J v : ℝ) : (P + J ^ 2 / 4 - v) ^ 2 - J ^ 2 * ((P - 2) / 2 + J ^ 2 / 16) = (P - v) ^ 2 - (v - 2) * J ^ 2 / 2

theorem NavierStokes.ConeAlgebra.rootTerm_ge_quarter {P J : ℝ} (hP : 2 < P) : J ^ 2 / 4 ≤ rootTerm P J

theorem NavierStokes.ConeAlgebra.coneBound_le_parameter {P J : ℝ} (hP : 2 < P) : coneBound P J ≤ P

theorem NavierStokes.ConeAlgebra.coneBound_gt_two {P J : ℝ} (hP : 2 < P) : 2 < coneBound P J

The lower root is strictly above two for every finite J and P > 2.

theorem NavierStokes.ConeAlgebra.true_cone_iff {P J v : ℝ} (hv : 2 < v) : 2 < P ∧ v < coneBound P J ↔ v < P ∧ (v - 2) * J ^ 2 < 2 * (P - v) ^ 2

Lemma 3.5: the full square-root criterion is equivalent to the quadratic test.

theorem NavierStokes.ConeAlgebra.relaxed_cone_of_le_two {P J v : ℝ} (hP : 2 < P) (hv : v ≤ 2) : v < coneBound P J

At and below two, P > 2 alone implies the relaxed root inequality.

theorem NavierStokes.ConeAlgebra.normalized_factorization (a b w : ℝ) (ha : a ≠ 0) : (a * (1 + (b / a) ^ 2) - 2) * (w + b / a) ^ 2 - 2 * (1 - b * w / a) ^ 2 = (1 + (b / a) ^ 2) * ((a - 2) * w ^ 2 + 2 * b * w + b ^ 2 / a - 2)

The exact factorization behind the limiting sufficient criterion (11).

theorem NavierStokes.ConeAlgebra.normalized_test_negative {a b w : ℝ} (ha : 0 < a) (hcriterion : 2 * b * w + b ^ 2 / a + (a - 2) * w ^ 2 < 2) : (a * (1 + (b / a) ^ 2) - 2) * (w + b / a) ^ 2 - 2 * (1 - b * w / a) ^ 2 < 0

Strict negativity in equation (11) gives strict negativity of its factored test.

theorem NavierStokes.ConeAlgebra.finite_amplitude_cone {c j v p : ℝ} (hp : 0 < p) (hP : 2 < p * c) (hvP : v < p * c) (hscale : 4 * c * v < p * (2 * c ^ 2 - (v - 2) * j ^ 2)) : v < coneBound (p * c) (p * j)

An explicit finite-amplitude sufficient condition, prior to taking any limit.

theorem NavierStokes.ConeAlgebra.sufficiently_large_amplitude_cone {c j v : ℝ} (hc : 0 < c) (hmargin : (v - 2) * j ^ 2 < 2 * c ^ 2) : ∃ (p₀ : ℝ), ∀ (p : ℝ), p₀ < p → 2 < p * c ∧ v < coneBound (p * c) (p * j)

For fixed normalized parameters, a positive leading coefficient and strict quadratic margin give the relaxed cone at every sufficiently large amplitude.

theorem NavierStokes.ConeAlgebra.equation_eleven_sufficient {a b w : ℝ} (ha : 0 < a) (hfirst : 0 < a - b * w) (hsecond : 2 * b * w + b ^ 2 / a + (a - 2) * w ^ 2 < 2) : ∃ (p₀ : ℝ), ∀ (p : ℝ), p₀ < p → 2 < p * (1 - b * w / a) ∧ a * (1 + (b / a) ^ 2) < coneBound (p * (1 - b * w / a)) (p * (w + b / a))

Equation (11) is sufficient at all sufficiently large positive stress amplitudes for each fixed triple of parameters.