Initial activation cone estimates

The scalar estimates keep every error proportional to the activation itself. In particular, none of their constants involves the inverse of the retained damping parameter. The later results use the constructed activation fields.

noncomputable def NavierStokes.ActivationCone.inverseRelativeError (L : ProfileHistories.Field) (q : ActivationBounds.ScaledPoint) : ℝ

Actual smooth factor in the reciprocal angular-field ratio.

Equations

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

theorem NavierStokes.ActivationCone.inverseRelativeError_smooth {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (inverseRelativeError L) (ActivationBounds.scaledDomain J)

theorem NavierStokes.ActivationCone.inverse_relative_scaled_factor {T : ℝ} (hT : T ≠ 0) (κ : ℝ) {J : Set ℝ} (hJ : IsOpen J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (u : ℝ) {η : ℝ} (hη : η ∈ J) : StressActivation.referenceAngular L (T * u, η) / StressActivation.activatedAngular T κ L (T * u, η) - 1 = ActivationBounds.scaledDistance ((κ, T), u, η) * inverseRelativeError L ((κ, T), u, η)

theorem NavierStokes.ActivationCone.inverse_relative_uniform_jets {J K : Set ℝ} (hJ : IsOpen J) (hK : IsCompact K) (hKJ : K ⊆ J) {L : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (T0 : ℝ) (n : ℕ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ T ∈ Set.Ioc 0 T0, ∀ κ ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 T, ∀ η ∈ K, |iteratedDeriv n (fun (ξ : ℝ) => StressActivation.referenceAngular L (y, ξ) / StressActivation.activatedAngular T κ L (y, ξ) - 1) η| ≤ M * y * StressActivation.activation T κ y

All fixed parameter jets of this actual ratio have uniform C*y*ea bounds as the ramp width and retained damping tend to zero.

theorem NavierStokes.ActivationCone.ramp_cone_of_errors {c B r e s P J v : ℝ} (hc : 0 < c) (hr : 2 + c ≤ r) (hrB : r ≤ B) (he : 0 < e) (he1 : e ≤ 1) (hs : 0 ≤ s) (hsquarter : s ≤ 1 / 4) (hsc : s ≤ c / 2) (hsB : (B + 1) * s ≤ 1 / 4) (hP : |P - r| ≤ s * e) (hv : |v - (1 - e) * r| ≤ s * e) (hJ : |J| ≤ s * e) : e ≤ P - v ∧ 2 + c / 4 < P ∧ (v - 2) * J ^ 2 < 2 * (P - v) ^ 2

A quantitative cone estimate retaining the small activation factor. The error scale s is C*y in the activation ramp.

theorem NavierStokes.ActivationCone.collar_lower_of_errors {c B r e s v : ℝ} (hc : 0 < c) (hr : 2 + c ≤ r) (hrB : r ≤ B) (he : 0 ≤ e) (hs : s ≤ 1) (heB : e * (B + 1) ≤ c / 4) (hv : |v - (1 - e) * r| ≤ s * e) : 2 + c / 2 < v

A small activation preserves a uniform part of the reference v > 2 margin. There is no inverse-damping loss.

theorem NavierStokes.ActivationCone.true_collar_of_errors {c B r e s P J v : ℝ} (hc : 0 < c) (hr : 2 + c ≤ r) (hrB : r ≤ B) (he : 0 < e) (he1 : e ≤ 1) (hs : 0 ≤ s) (hsquarter : s ≤ 1 / 4) (hsc : s ≤ c / 2) (hsB : (B + 1) * s ≤ 1 / 4) (heB : e * (B + 1) ≤ c / 4) (hP : |P - r| ≤ s * e) (hv : |v - (1 - e) * r| ≤ s * e) (hJ : |J| ≤ s * e) : e ≤ P - v ∧ 2 + c / 2 < v ∧ 2 < P ∧ v < ConeAlgebra.coneBound P J

Combining the ramp and collar estimates gives the actual lower-root criterion, including the strict lower bound on v.

noncomputable def NavierStokes.ActivationCone.errorTolerance (c B : ℝ) : ℝ

A single error tolerance is chosen from the fixed reference bounds.

Equations

• NavierStokes.ActivationCone.errorTolerance c B = min (1 / 4) (min (c / 2) (1 / (4 * (B + 1))))

theorem NavierStokes.ActivationCone.errorTolerance_pos {c B : ℝ} (hc : 0 < c) (hB : 0 ≤ B) : 0 < errorTolerance c B

theorem NavierStokes.ActivationCone.errorTolerance_bounds {c B s : ℝ} (hB : 0 ≤ B) (hs : s ≤ errorTolerance c B) : s ≤ 1 / 4 ∧ s ≤ c / 2 ∧ (B + 1) * s ≤ 1 / 4

theorem NavierStokes.ActivationCone.activation_pos {T κ y : ℝ} (hT : 0 < T) (hκ : κ < 1) (hy : 0 < y) : 0 < StressActivation.activation T κ y

Positivity of the actual flat activation on the nonzero ramp.

theorem NavierStokes.ActivationCone.activation_uniform_collar {m : ℝ} (hm : 0 < m) : ∃ (θ : ℝ), 0 < θ ∧ θ ≤ 1 ∧ ∀ (T : ℝ), 0 < T → ∀ κ ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 (θ * T), StressActivation.activation T κ y < m

For any requested small activation, a fixed fraction of the ramp works uniformly in its width and in every retained damping κ ∈ [0,1].

theorem NavierStokes.ActivationCone.uniform_ramp_from_comparison {K : Set ℝ} {r : ProfileHistories.Field} {P J v : ℝ → ℝ → ProfileHistories.Field} {c B C T0 : ℝ} (hc : 0 < c) (hB : 0 ≤ B) (hC : 0 ≤ C) (hT0 : 0 < T0) (href : ∀ y ∈ Set.Icc 0 T0, ∀ η ∈ K, 2 + c ≤ r (y, η) ∧ r (y, η) ≤ B) (herr : ∀ T ∈ Set.Ioc 0 T0, ∀ κ ∈ Set.Ioo 0 1, ∀ y ∈ Set.Icc 0 T, ∀ η ∈ K, |P T κ (y, η) - r (y, η)| ≤ C * y * StressActivation.activation T κ y ∧ |v T κ (y, η) - StressActivation.damping T κ y * r (y, η)| ≤ C * y * StressActivation.activation T κ y ∧ |J T κ (y, η)| ≤ C * y * StressActivation.activation T κ y) : ∃ (Tstar : ℝ) (θ : ℝ), 0 < Tstar ∧ Tstar ≤ T0 ∧ 0 < θ ∧ θ ≤ 1 ∧ ∀ T ∈ Set.Ioc 0 Tstar, ∀ κ ∈ Set.Ioo 0 1, ∀ y ∈ Set.Ioc 0 T, ∀ η ∈ K, StressActivation.activation T κ y ≤ P T κ (y, η) - v T κ (y, η) ∧ 2 + c / 4 < P T κ (y, η) ∧ (v T κ (y, η) - 2) * J T κ (y, η) ^ 2 < 2 * (P T κ (y, η) - v T κ (y, η)) ^ 2 ∧ v T κ (y, η) < ConeAlgebra.coneBound (P T κ (y, η)) (J T κ (y, η)) ∧ (y ≤ θ * T → 2 + c / 2 < v T κ (y, η))

Uniform conversion of proved comparison estimates into a complete initial ramp and a first true-cone collar. The constants are chosen before the retained damping parameter.

theorem NavierStokes.ActivationCone.stress_factorization (F A B κ y e dA dB dR : ℝ) (hκ : κ = 1 - e) : (F * (A + y * e * dA - κ * A), F * (B + y * e * dB - κ * B * (1 + y * e * dR))) = (e * (F * (A + y * dA)), e * (F * (B + y * (dB - κ * B * dR))))

Exact stress factorization when stock and shear-ratio errors carry the constructed factor y*e. Neither component divides by the damping.

noncomputable def NavierStokes.ActivationCone.reducedStress (F A B κ y dA dB dR : ℝ) : ℝ × ℝ

The smooth extension of stress divided by the activation factor.

Equations

• NavierStokes.ActivationCone.reducedStress F A B κ y dA dB dR = (F * (A + y * dA), F * (B + y * (dB - κ * B * dR)))

@[simp]

theorem NavierStokes.ActivationCone.reducedStress_at_edge (F A B κ dA dB dR : ℝ) : reducedStress F A B κ 0 dA dB dR = (F * A, F * B)

theorem NavierStokes.ActivationCone.reducedStress_smooth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {S : Set E} {F A B κ y dA dB dR : E → ℝ} (hF : ContDiffOn ℝ (↑⊤) F S) (hA : ContDiffOn ℝ (↑⊤) A S) (hB : ContDiffOn ℝ (↑⊤) B S) (hκ : ContDiffOn ℝ (↑⊤) κ S) (hy : ContDiffOn ℝ (↑⊤) y S) (hdA : ContDiffOn ℝ (↑⊤) dA S) (hdB : ContDiffOn ℝ (↑⊤) dB S) (hdR : ContDiffOn ℝ (↑⊤) dR S) : ContDiffOn ℝ (↑⊤) (fun (p : E) => reducedStress (F p) (A p) (B p) (κ p) (y p) (dA p) (dB p) (dR p)) S

This extension is smooth without dividing by either activation or damping.

theorem NavierStokes.ActivationCone.reducedStress_first_positive {F A B κ y dA dB dR α M : ℝ} (hF : 0 < F) (hα : 0 < α) (hA : α ≤ A) (hy : 0 ≤ y) (hdA : |dA| ≤ M) (hsmall : y * M ≤ α / 2) : 0 < (reducedStress F A B κ y dA dB dR).1

A common coefficient bound makes the normalized stress direction nonzero on a uniform first collar; the bound does not involve inverse damping.

theorem NavierStokes.ActivationCone.reducedStress_nonzero {F A B κ y dA dB dR α M : ℝ} (hF : 0 < F) (hα : 0 < α) (hA : α ≤ A) (hy : 0 ≤ y) (hdA : |dA| ≤ M) (hsmall : y * M ≤ α / 2) : reducedStress F A B κ y dA dB dR ≠ 0

theorem NavierStokes.ActivationCone.reducedStress_edge_projection (F A B κ dA dB dR : ℝ) : (reducedStress F A B κ 0 dA dB dR).1 + B / A * (reducedStress F A B κ 0 dA dB dR).2 = F * (A + B ^ 2 / A)

theorem NavierStokes.ActivationCone.reducedStress_edge_margin {F A B c κ dA dB dR : ℝ} (hF : 0 < F) (hc : 0 < c) (hr : 2 + c ≤ A + B ^ 2 / A) : 2 * F < (reducedStress F A B κ 0 dA dB dR).1 + B / A * (reducedStress F A B κ 0 dA dB dR).2

The true angular directional margin has a strictly positive edge limit.

noncomputable def NavierStokes.ActivationCone.normalizedConeGap (r v y dP dv dJ : ℝ) : ℝ

The quadratic cone gap after removing the square of the flat activation.

Equations

• NavierStokes.ActivationCone.normalizedConeGap r v y dP dv dJ = 2 * (r + y * (dP - dv)) ^ 2 - (v - 2) * (y * dJ) ^ 2

theorem NavierStokes.ActivationCone.cone_gap_factorization (r e y dP dv dJ : ℝ) : 2 * (r + y * e * dP - ((1 - e) * r + y * e * dv)) ^ 2 - ((1 - e) * r + y * e * dv - 2) * (y * e * dJ) ^ 2 = e ^ 2 * normalizedConeGap r ((1 - e) * r + y * e * dv) y dP dv dJ

@[simp]

theorem NavierStokes.ActivationCone.normalizedConeGap_at_edge (r v dP dv dJ : ℝ) : normalizedConeGap r v 0 dP dv dJ = 2 * r ^ 2

theorem NavierStokes.ActivationCone.normalizedConeGap_edge_positive {r : ℝ} (hr : r ≠ 0) (v dP dv dJ : ℝ) : 0 < normalizedConeGap r v 0 dP dv dJ

noncomputable def NavierStokes.ActivationCone.stockProjection (p q t : ℝ) : ℝ

The actual cone coordinates formed from two stock coordinates and a shear ratio.

Equations

• NavierStokes.ActivationCone.stockProjection p q t = p + q * t

noncomputable def NavierStokes.ActivationCone.stockCross (p q t : ℝ) : ℝ

Stock cross, given by q - p * t.

Equations

• NavierStokes.ActivationCone.stockCross p q t = q - p * t

noncomputable def NavierStokes.ActivationCone.projectionError (A B z dA dB dR : ℝ) : ℝ

Projection error, given by dA + dB * (B / A) * (1 + z * dR) + (B ^ 2 / A) * dR.

Equations

• NavierStokes.ActivationCone.projectionError A B z dA dB dR = dA + dB * (B / A) * (1 + z * dR) + B ^ 2 / A * dR

noncomputable def NavierStokes.ActivationCone.crossError (A B z dA dB dR : ℝ) : ℝ

Cross error, given by dB - B * dR - dA * (B / A) * (1 + z * dR).

Equations

• NavierStokes.ActivationCone.crossError A B z dA dB dR = dB - B * dR - dA * (B / A) * (1 + z * dR)

noncomputable def NavierStokes.ActivationCone.sizeError (κ A B z dR : ℝ) : ℝ

Size error, given by κ * (B ^ 2 / A) * dR * (2 + z * dR).

Equations

• NavierStokes.ActivationCone.sizeError κ A B z dR = κ * (B ^ 2 / A) * dR * (2 + z * dR)

theorem NavierStokes.ActivationCone.cone_error_factorizations (κ A B z dA dB dR : ℝ) (hA : A ≠ 0) : stockProjection (A + z * dA) (B + z * dB) (B / A * (1 + z * dR)) - (A + B ^ 2 / A) = z * projectionError A B z dA dB dR ∧ stockCross (A + z * dA) (B + z * dB) (B / A * (1 + z * dR)) = z * crossError A B z dA dB dR ∧ κ * (A + B ^ 2 / A * (1 + z * dR) ^ 2) - κ * (A + B ^ 2 / A) = z * sizeError κ A B z dR

Passing from stock errors to cone errors preserves the exact common factor. This computation contains no division by the damping κ.

noncomputable def NavierStokes.ActivationCone.comparisonConstant (M : ℝ) : ℝ

Comparison constant, given by M + 2 * M ^ 2 + M ^ 3.

Equations

• NavierStokes.ActivationCone.comparisonConstant M = M + 2 * M ^ 2 + M ^ 3

theorem NavierStokes.ActivationCone.cone_error_bounds {κ A B z dA dB dR M : ℝ} (hM : 0 ≤ M) (hκ : |κ| ≤ 1) (hz : |z| ≤ 1) (hB : |B| ≤ M) (hBA : |B / A| ≤ M) (hB2A : |B ^ 2 / A| ≤ M) (hdA : |dA| ≤ M) (hdB : |dB| ≤ M) (hdR : |dR| ≤ M) : |projectionError A B z dA dB dR| ≤ comparisonConstant M ∧ |crossError A B z dA dB dR| ≤ comparisonConstant M ∧ |sizeError κ A B z dR| ≤ comparisonConstant M

One bound for the transported error factors, depending only on the reference and primitive-factor bounds. It is uniform down to κ = 0.

theorem NavierStokes.ActivationCone.cone_comparison_from_stock_bounds {κ A B z p q R M : ℝ} (hM : 0 ≤ M) (hA : A ≠ 0) (hκ : |κ| ≤ 1) (hz : 0 ≤ z) (hz1 : z ≤ 1) (hB : |B| ≤ M) (hBA : |B / A| ≤ M) (hB2A : |B ^ 2 / A| ≤ M) (hp : |p - A| ≤ M * z) (hq : |q - B| ≤ M * z) (hR : |R - 1| ≤ M * z) : |stockProjection p q (B / A * R) - (A + B ^ 2 / A)| ≤ comparisonConstant M * z ∧ |κ * (A + B ^ 2 / A * R ^ 2) - κ * (A + B ^ 2 / A)| ≤ comparisonConstant M * z ∧ |stockCross p q (B / A * R)| ≤ comparisonConstant M * z

Explicit transport of actual stock and reciprocal-field error bounds to the three cone-coordinate error bounds.

theorem NavierStokes.ActivationCone.shearSize_eq (T : ℝ) {κ X0 : ℝ} (hκ : κ ∈ Set.Ioc 0 1) (hX0 : 0 < X0) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (y : ℝ) {η : ℝ} (hη : η ∈ J) (hA : StressActivation.referenceP1 L (y, η) ≠ 0) : StressActivation.shearSize T κ X0 L U (y, η) = StressActivation.damping T κ y * (StressActivation.referenceP1 L (y, η) + StressActivation.referenceP2 X0 L U (y, η) ^ 2 / StressActivation.referenceP1 L (y, η) * (StressActivation.referenceAngular L (y, η) / StressActivation.activatedAngular T κ L (y, η)) ^ 2)

The genuine derivative-defined shear size has the cancellation form used in the error transport.

noncomputable def NavierStokes.ActivationCone.activatedStockOne (h X0 : ℝ) (initial : StressActivation.HistoryRow → ℝ → ℝ) (L U : ProfileHistories.Field) (T κ : ℝ) : ProfileHistories.Field

Activated stock one, given by ActivationStocks.logViewOne h X0 (activatedAngular T κ L) (logHistory X0 initial (activatedAngular T κ L) (controlled T κ U)).

Equations

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

noncomputable def NavierStokes.ActivationCone.activatedStockTwo (h X0 : ℝ) (initial : StressActivation.HistoryRow → ℝ → ℝ) (L U : ProfileHistories.Field) (T κ : ℝ) : ProfileHistories.Field

Activated stock two, constructed using ActivationStocks.logViewTwo.

Equations

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

noncomputable def NavierStokes.ActivationCone.activatedProjection (h X0 : ℝ) (initial : StressActivation.HistoryRow → ℝ → ℝ) (L U : ProfileHistories.Field) (T κ : ℝ) : ProfileHistories.Field

Activated projection, defined pointwise by stockProjection (activatedStockOne h X0 initial L U T κ p) (activatedStockTwo h X0 initial L U T κ p) (shearSlope T κ X0 L U p).

Equations

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

noncomputable def NavierStokes.ActivationCone.activatedCross (h X0 : ℝ) (initial : StressActivation.HistoryRow → ℝ → ℝ) (L U : ProfileHistories.Field) (T κ : ℝ) : ProfileHistories.Field

Activated cross, defined pointwise by stockCross (activatedStockOne h X0 initial L U T κ p) (activatedStockTwo h X0 initial L U T κ p) (shearSlope T κ X0 L U p).

Equations

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

noncomputable def NavierStokes.ActivationCone.activatedStress (h X0 : ℝ) (initial : StressActivation.HistoryRow → ℝ → ℝ) (L U : ProfileHistories.Field) (T κ : ℝ) (p : ProfileHistories.Point) : ℝ × ℝ

Activated stress as an element of ℝ × ℝ.

Equations

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

theorem NavierStokes.ActivationCone.reference_coordinates_smooth {X0 : ℝ} (hX0 : 0 < X0) {J : Set ℝ} (hJ : IsOpen J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) : ContDiffOn ℝ (↑⊤) (StressActivation.referenceP1 L) (StressActivation.logDomain J hJ).carrier ∧ ContDiffOn ℝ (↑⊤) (StressActivation.referenceP2 X0 L U) (StressActivation.logDomain J hJ).carrier

theorem NavierStokes.ActivationCone.exists_actual_stress_direction (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (initial : StressActivation.HistoryRow → ℝ → ℝ) {J K : Set ℝ} (hJ : IsOpen J) (hKJ : K ⊆ J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hi : ∀ (r : StressActivation.HistoryRow), ContDiffOn ℝ (↑⊤) (initial r) J) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) {T0 : ℝ} (hmatch : ∀ y ∈ Set.Icc 0 T0, ∀ η ∈ K, ActivationStocks.logViewOne h X0 (StressActivation.referenceAngular L) (StressActivation.logHistory X0 initial (StressActivation.referenceAngular L) U) (y, η) = StressActivation.referenceP1 L (y, η) ∧ ActivationStocks.logViewTwo h X0 (StressActivation.referenceAngular L) U (StressActivation.logHistory X0 initial (StressActivation.referenceAngular L) U) (y, η) = StressActivation.referenceP2 X0 L U (y, η)) : ∃ (D : ActivationBounds.ScaledPoint → ℝ × ℝ), ContDiffOn ℝ (↑⊤) D (ActivationBounds.scaledDomain J) ∧ (∀ (κ T η : ℝ), D ((κ, T), 0, η) = (StressActivation.referenceAngular L (0, η) * StressActivation.referenceP1 L (0, η), StressActivation.referenceAngular L (0, η) * StressActivation.referenceP2 X0 L U (0, η))) ∧ ∀ (T : ℝ), 0 < T → ∀ (κ u η : ℝ), T * u ∈ Set.Icc 0 T0 → η ∈ K → activatedStress h X0 initial L U T κ (T * u, η) = (StressActivation.activation 1 κ u * (D ((κ, T), u, η)).1, StressActivation.activation 1 κ u * (D ((κ, T), u, η)).2)

The actual integral-history stress has a smooth factor after division by the flat activation. Its inner-edge value is the positive reference direction.

theorem NavierStokes.ActivationCone.actual_comparisons (h : ℝ) {X0 : ℝ} (hX0 : 0 < X0) (initial : StressActivation.HistoryRow → ℝ → ℝ) {J K : Set ℝ} (hJ : IsOpen J) (hK : IsCompact K) (hKJ : K ⊆ J) {L U : ProfileHistories.Field} (hL : ContDiffOn ℝ (↑⊤) L (StressActivation.logDomain J hJ).carrier) (hU : ContDiffOn ℝ (↑⊤) U (StressActivation.logDomain J hJ).carrier) (hi : ∀ (r : StressActivation.HistoryRow), ContDiffOn ℝ (↑⊤) (initial r) J) (hcoef : ∀ η ∈ J, NaturalAxisData.L h η ≠ 0) {T0 Mref : ℝ} (hT0 : T0 ≤ 1) (hMref : 0 ≤ Mref) (href : ∀ y ∈ Set.Icc 0 T0, ∀ η ∈ K, StressActivation.referenceP1 L (y, η) ≠ 0 ∧ |StressActivation.referenceP2 X0 L U (y, η)| ≤ Mref ∧ |StressActivation.referenceP2 X0 L U (y, η) / StressActivation.referenceP1 L (y, η)| ≤ Mref ∧ |StressActivation.referenceP2 X0 L U (y, η) ^ 2 / StressActivation.referenceP1 L (y, η)| ≤ Mref) (hmatch : ∀ y ∈ Set.Icc 0 T0, ∀ η ∈ K, ActivationStocks.logViewOne h X0 (StressActivation.referenceAngular L) (StressActivation.logHistory X0 initial (StressActivation.referenceAngular L) U) (y, η) = StressActivation.referenceP1 L (y, η) ∧ ActivationStocks.logViewTwo h X0 (StressActivation.referenceAngular L) U (StressActivation.logHistory X0 initial (StressActivation.referenceAngular L) U) (y, η) = StressActivation.referenceP2 X0 L U (y, η)) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ T ∈ Set.Ioc 0 T0, ∀ κ ∈ Set.Ioo 0 1, ∀ y ∈ Set.Icc 0 T, ∀ η ∈ K, |activatedProjection h X0 initial L U T κ (y, η) - StressActivation.referenceSize X0 L U (y, η)| ≤ C * y * StressActivation.activation T κ y ∧ |StressActivation.shearSize T κ X0 L U (y, η) - StressActivation.damping T κ y * StressActivation.referenceSize X0 L U (y, η)| ≤ C * y * StressActivation.activation T κ y ∧ |activatedCross h X0 initial L U T κ (y, η)| ≤ C * y * StressActivation.activation T κ y

The comparison estimates are derived from genuine log histories and the constructed reciprocal-field factor. Uniform stock estimates are obtained internally from their proved smooth factors.

theorem NavierStokes.ActivationCone.compact_reference_collar {K : Set ℝ} (hK : IsCompact K) {T c : ℝ} (hT : 0 < T) (hc : 0 < c) {r : ProfileHistories.Field} (hr : ContinuousOn r (Set.Icc 0 T ×ˢ K)) (hzero : ∀ η ∈ K, 2 + 2 * c ≤ r (0, η)) : ∃ (τ : ℝ), 0 < τ ∧ τ ≤ T ∧ ∀ y ∈ Set.Icc 0 τ, ∀ η ∈ K, 2 + c < r (y, η)

A strict initial reference margin persists on one common radial collar. The collar is obtained from actual uniform continuity on a compact set.

theorem NavierStokes.ActivationCone.compact_reference_bounds {K : Set ℝ} (hK : IsCompact K) {T c : ℝ} (hT : 0 < T) (hc : 0 < c) {A B : ProfileHistories.Field} (hA : ContinuousOn A (Set.Icc 0 T ×ˢ K)) (hB : ContinuousOn B (Set.Icc 0 T ×ˢ K)) (hApos : ∀ p ∈ Set.Icc 0 T ×ˢ K, 0 < A p) (hzero : ∀ η ∈ K, 2 + 2 * c ≤ A (0, η) + B (0, η) ^ 2 / A (0, η)) : ∃ (τ : ℝ) (α : ℝ) (M : ℝ), 0 < τ ∧ τ ≤ T ∧ 0 < α ∧ 1 ≤ M ∧ ∀ y ∈ Set.Icc 0 τ, ∀ η ∈ K, α ≤ A (y, η) ∧ 2 + c < A (y, η) + B (y, η) ^ 2 / A (y, η) ∧ A (y, η) + B (y, η) ^ 2 / A (y, η) ≤ M ∧ |B (y, η)| ≤ M ∧ |B (y, η) / A (y, η)| ≤ M ∧ |B (y, η) ^ 2 / A (y, η)| ≤ M

Compact reference data provide all fixed bounds needed by the algebraic error transport and a genuine common initial cone collar.

theorem NavierStokes.ActivationCone.referenceP1_natural (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδlim : 2 * δ < ReferencePath.rampLimit) {y η : ℝ} (hy : y ≤ δ) (hη : η ∈ ReferencePath.parameterInterval) : StressActivation.referenceP1 (StressActivation.FromReference.refLog N δ) (y, η) = NaturalEntrance.p1 N.f (N.fromLog (y, η))

theorem NavierStokes.ActivationCone.referenceP2_natural (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδlim : 2 * δ < ReferencePath.rampLimit) {y η : ℝ} (hy : y ≤ δ) (hη : η ∈ ReferencePath.parameterInterval) : StressActivation.referenceP2 N.endpoint (StressActivation.FromReference.refLog N δ) (StressActivation.FromReference.refAxial N δ) (y, η) = NaturalEntrance.p2 N.f N.U (N.fromLog (y, η))

theorem NavierStokes.ActivationCone.referenceP1_smooth (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδlim : 2 * δ < ReferencePath.rampLimit) : ContDiffOn ℝ (↑⊤) (StressActivation.referenceP1 (StressActivation.FromReference.refLog N δ)) (StressActivation.logDomain ReferencePath.parameterInterval ReferencePath.parameterInterval_open).carrier

theorem NavierStokes.ActivationCone.referenceP2_smooth (N : ReferencePath.Input) {δ : ℝ} (hδ : 0 < δ) (hδlim : 2 * δ < ReferencePath.rampLimit) : ContDiffOn ℝ (↑⊤) (StressActivation.referenceP2 N.endpoint (StressActivation.FromReference.refLog N δ) (StressActivation.FromReference.refAxial N δ)) (StressActivation.logDomain ReferencePath.parameterInterval ReferencePath.parameterInterval_open).carrier

theorem NavierStokes.ActivationCone.natural_reference_bounds {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hΛ : 0 < Λ) (F : NaturalEntrance.EntranceProfile d Λ C) {δ : ℝ} (hδ : 0 < δ) (hδlim : 2 * δ < ReferencePath.rampLimit) : have N := ReferencePath.Input.ofNatural hΛ F.profile.family; have A := StressActivation.referenceP1 (StressActivation.FromReference.refLog N δ); have B := StressActivation.referenceP2 N.endpoint (StressActivation.FromReference.refLog N δ) (StressActivation.FromReference.refAxial N δ); ∃ (τ : ℝ) (α : ℝ) (M : ℝ), 0 < τ ∧ τ ≤ δ ∧ 0 < α ∧ 1 ≤ M ∧ ∀ y ∈ Set.Icc 0 τ, ∀ η ∈ Set.Icc (-1) 1, α ≤ A (y, η) ∧ 2 + 1 / 8 < A (y, η) + B (y, η) ^ 2 / A (y, η) ∧ A (y, η) + B (y, η) ^ 2 / A (y, η) ≤ M ∧ |B (y, η)| ≤ M ∧ |B (y, η) / A (y, η)| ≤ M ∧ |B (y, η) ^ 2 / A (y, η)| ≤ M

The compact reference bounds are obtained for the actual constructed natural entrance profile, not supplied as extra estimates. The reference cutoff width is fixed while the later activation width is allowed to shrink.

theorem NavierStokes.ActivationCone.natural_reference_log_match {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hΛ : 0 < Λ) (F : NaturalProfile.ProfileFamily d Λ C) (hP0 : ContDiff ℝ (↑⊤) P0) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδlim : 2 * δ < ReferencePath.rampLimit) {y η : ℝ} (hy : y ≤ δ) (hη : η ∈ Set.Icc (-1) 1) : have N := ReferencePath.Input.ofNatural hΛ F; have L := StressActivation.FromReference.refLog N δ; have U := StressActivation.FromReference.refAxial N δ; have I := ActivationStocks.FromReference.initial N hδ hδlim P0 hP0; ActivationStocks.logViewOne h N.endpoint (StressActivation.referenceAngular L) (StressActivation.logHistory N.endpoint I (StressActivation.referenceAngular L) U) (y, η) = StressActivation.referenceP1 L (y, η) ∧ ActivationStocks.logViewTwo h N.endpoint (StressActivation.referenceAngular L) U (StressActivation.logHistory N.endpoint I (StressActivation.referenceAngular L) U) (y, η) = StressActivation.referenceP2 N.endpoint L U (y, η)

theorem NavierStokes.ActivationCone.natural_initial_activation {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hΛ : 0 < Λ) (F : NaturalEntrance.EntranceProfile d Λ C) (hP0 : ContDiff ℝ (↑⊤) P0) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδlim : 2 * δ < ReferencePath.rampLimit) : have N := ReferencePath.Input.ofNatural hΛ F.profile.family; have L := StressActivation.FromReference.refLog N δ; have U := StressActivation.FromReference.refAxial N δ; have I := ActivationStocks.FromReference.initial N hδ hδlim P0 hP0; ∃ (Tstar : ℝ) (θ : ℝ), 0 < Tstar ∧ Tstar ≤ δ ∧ 0 < θ ∧ θ ≤ 1 ∧ ∀ T ∈ Set.Ioc 0 Tstar, ∀ κ ∈ Set.Ioo 0 1, ∀ y ∈ Set.Ioc 0 T, ∀ η ∈ Set.Icc (-1) 1, StressActivation.activation T κ y ≤ activatedProjection h N.endpoint I L U T κ (y, η) - StressActivation.shearSize T κ N.endpoint L U (y, η) ∧ 2 + 1 / 32 < activatedProjection h N.endpoint I L U T κ (y, η) ∧ (StressActivation.shearSize T κ N.endpoint L U (y, η) - 2) * activatedCross h N.endpoint I L U T κ (y, η) ^ 2 < 2 * (activatedProjection h N.endpoint I L U T κ (y, η) - StressActivation.shearSize T κ N.endpoint L U (y, η)) ^ 2 ∧ StressActivation.shearSize T κ N.endpoint L U (y, η) < ConeAlgebra.coneBound (activatedProjection h N.endpoint I L U T κ (y, η)) (activatedCross h N.endpoint I L U T κ (y, η)) ∧ (y ≤ θ * T → 2 + 1 / 16 < StressActivation.shearSize T κ N.endpoint L U (y, η))

The initial activation assertion is proved for the actual natural entrance and its actual recomputed lag histories. Both the ramp width and the first collar fraction are chosen uniformly in κ₀ ∈ (0,1).

theorem NavierStokes.ActivationCone.natural_activation_direction {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (hΛ : 0 < Λ) (F : NaturalEntrance.EntranceProfile d Λ C) (hP0 : ContDiff ℝ (↑⊤) P0) (hsmall : NaturalAxisData.SmallParameters h j) {δ : ℝ} (hδ : 0 < δ) (hδlim : 2 * δ < ReferencePath.rampLimit) : have N := ReferencePath.Input.ofNatural hΛ F.profile.family; have L := StressActivation.FromReference.refLog N δ; have U := StressActivation.FromReference.refAxial N δ; have I := ActivationStocks.FromReference.initial N hδ hδlim P0 hP0; ∃ (D : ActivationBounds.ScaledPoint → ℝ × ℝ) (ε : ℝ), ContDiffOn ℝ (↑⊤) D (ActivationBounds.scaledDomain ReferencePath.parameterInterval) ∧ 0 < ε ∧ (∀ (κ T η : ℝ), η ∈ Set.Icc (-1) 1 → ε ≤ (D ((κ, T), 0, η)).1 ∧ ε ≤ (D ((κ, T), 0, η)).1 + StressActivation.referenceP2 N.endpoint L U (0, η) / StressActivation.referenceP1 L (0, η) * (D ((κ, T), 0, η)).2 - 2 * StressActivation.referenceAngular L (0, η)) ∧ ∀ (T : ℝ), 0 < T → ∀ (κ u η : ℝ), T * u ∈ Set.Icc 0 δ → η ∈ Set.Icc (-1) 1 → activatedStress h N.endpoint I L U T κ (T * u, η) = (StressActivation.activation 1 κ u * (D ((κ, T), u, η)).1, StressActivation.activation 1 κ u * (D ((κ, T), u, η)).2)

The normalized stress of the actual activation extends smoothly to the inner edge, where its first component and angular directional margin have one positive lower bound, uniform in all activation parameters.