Actual outgoing histories through the axial drop

All lags below include the ideal incoming history. The scalar averages are integrals of the constructed schedule, and no cone estimate is assumed.

theorem NavierStokes.OutgoingEntranceCone.integral_exp_mul_real {a : ℝ} (ha : a ≠ 0) (y : ℝ) : ∫ (t : ℝ) in 0..y, Real.exp (a * t) = (Real.exp (a * y) - 1) / a

noncomputable def NavierStokes.OutgoingEntranceCone.historyAverage (b : ℝ → ℝ) (b₀ y : ℝ) : ℝ

Exponential averaging with the actual incoming history at clock zero.

Equations

• NavierStokes.OutgoingEntranceCone.historyAverage b b₀ y = NavierStokes.OutgoingTail.linearLag (fun (x : ℝ) => 1) b b₀ y

theorem NavierStokes.OutgoingEntranceCone.historyAverage_formula (b : ℝ → ℝ) (b₀ y : ℝ) : historyAverage b b₀ y = Real.exp (-y) * (b₀ + ∫ (t : ℝ) in 0..y, Real.exp t * b t)

theorem NavierStokes.OutgoingEntranceCone.historyAverage_initial (b : ℝ → ℝ) (b₀ : ℝ) : historyAverage b b₀ 0 = b₀

theorem NavierStokes.OutgoingEntranceCone.historyAverage_hasDerivAt {b : ℝ → ℝ} (hb : Continuous b) (b₀ y : ℝ) : HasDerivAt (historyAverage b b₀) (b y - historyAverage b b₀ y) y

theorem NavierStokes.OutgoingEntranceCone.historyAverage_contDiff {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (b₀ : ℝ) : ContDiff ℝ (↑⊤) (historyAverage b b₀)

theorem NavierStokes.OutgoingEntranceCone.historyAverage_constant {b : ℝ → ℝ} {b₀ y : ℝ} (hb : ∀ t ∈ Set.uIcc 0 y, b t = b₀) : historyAverage b b₀ y = b₀

theorem NavierStokes.OutgoingEntranceCone.historyAverage_nonneg {b : ℝ → ℝ} {b₀ y : ℝ} (h₀ : 0 ≤ b₀) (hy : 0 ≤ y) (hb : ∀ t ∈ Set.Icc 0 y, 0 ≤ b t) : 0 ≤ historyAverage b b₀ y

theorem NavierStokes.OutgoingEntranceCone.historyAverage_le {b : ℝ → ℝ} (hbc : Continuous b) {b₀ K y : ℝ} (h₀ : b₀ ≤ K) (hy : 0 ≤ y) (hb : ∀ t ∈ Set.Icc 0 y, b t ≤ K) : historyAverage b b₀ y ≤ K

theorem NavierStokes.OutgoingEntranceCone.historyAverage_late {b : ℝ → ℝ} (hbc : Continuous b) {b₀ a y : ℝ} (hay : a ≤ y) (hb : ∀ (t : ℝ), a ≤ t → b t = 0) : historyAverage b b₀ y = Real.exp (-(y - a)) * historyAverage b b₀ a

noncomputable def NavierStokes.OutgoingEntranceCone.averagedDrop (c : OutgoingSchedule.Parameters) : ℝ → ℝ

The actual average axial coefficient; the incoming value integrates k=4.

Equations

• NavierStokes.OutgoingEntranceCone.averagedDrop c = NavierStokes.OutgoingEntranceCone.historyAverage (NavierStokes.OutgoingSchedule.dropCoefficient c.m) 4

noncomputable def NavierStokes.OutgoingEntranceCone.averagedDropSquare (c : OutgoingSchedule.Parameters) : ℝ → ℝ

The squared axial history; the incoming value integrates k²=16.

Equations

• NavierStokes.OutgoingEntranceCone.averagedDropSquare c = NavierStokes.OutgoingEntranceCone.historyAverage (fun (y : ℝ) => NavierStokes.OutgoingSchedule.dropCoefficient c.m y ^ 2) 16

theorem NavierStokes.OutgoingEntranceCone.averagedDrop_contDiff (c : OutgoingSchedule.Parameters) : ContDiff ℝ (↑⊤) (averagedDrop c)

theorem NavierStokes.OutgoingEntranceCone.averagedDrop_hasDerivAt (c : OutgoingSchedule.Parameters) (y : ℝ) : HasDerivAt (averagedDrop c) (OutgoingSchedule.dropCoefficient c.m y - averagedDrop c y) y

theorem NavierStokes.OutgoingEntranceCone.averagedDrop_early (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : y ≤ 1) : averagedDrop c y = 4

theorem NavierStokes.OutgoingEntranceCone.averagedDrop_bounds (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : 0 ≤ y) : 0 ≤ averagedDrop c y ∧ averagedDrop c y ≤ 4

theorem NavierStokes.OutgoingEntranceCone.averagedDropSquare_bounds (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : 0 ≤ y) : 0 ≤ averagedDropSquare c y ∧ averagedDropSquare c y ≤ 16

theorem NavierStokes.OutgoingEntranceCone.averagedDrop_is_mass_history (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (η : ℝ) {y : ℝ} (hy : y ≤ c.pulseStart) : OutgoingSchedule.massMoment c amp η y / Real.exp y = averagedDrop c y * η

theorem NavierStokes.OutgoingEntranceCone.averagedDrop_small_on_second_ramp (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : c.dropLength + 1 ≤ y) : averagedDrop c y ≤ 1 / 2

noncomputable def NavierStokes.OutgoingEntranceCone.shapeGradient (η : ℝ) : ℝ

Shape gradient, given by 2 * η / (1 + η ^ 2).

Equations

• NavierStokes.OutgoingEntranceCone.shapeGradient η = 2 * η / (1 + η ^ 2)

theorem NavierStokes.OutgoingEntranceCone.shapeGradient_contDiff : ContDiff ℝ (↑⊤) shapeGradient

theorem NavierStokes.OutgoingEntranceCone.parameter_square_le_one {η : ℝ} (hη : |η| ≤ 1) : η ^ 2 ≤ 1

theorem NavierStokes.OutgoingEntranceCone.eta_shapeGradient_bounds {η : ℝ} (hη : |η| ≤ 1) : η ^ 2 ≤ η * shapeGradient η ∧ η * shapeGradient η ≤ 1

theorem NavierStokes.OutgoingEntranceCone.abs_shapeGradient_le (η : ℝ) : |shapeGradient η| ≤ 2 * |η|

theorem NavierStokes.OutgoingEntranceCone.dropCoefficient_hasDerivAt {m y : ℝ} (hm : 0 < m) (hy : 0 < y) : HasDerivAt (OutgoingSchedule.dropCoefficient m) (-(4 * deriv OutgoingSchedule.sigma (Real.log y / m) / (m * y))) y

noncomputable def NavierStokes.OutgoingEntranceCone.dropSpeed (m : ℝ) : ℝ

Drop speed, given by 4 * stepBound / m.

Equations

• NavierStokes.OutgoingEntranceCone.dropSpeed m = 4 * NavierStokes.OutgoingTail.stepBound / m

theorem NavierStokes.OutgoingEntranceCone.dropSpeed_pos {m : ℝ} (hm : 0 < m) : 0 < dropSpeed m

theorem NavierStokes.OutgoingEntranceCone.dropCoefficient_deriv_bound {m y : ℝ} (hm : 0 < m) (hy : 0 < y) : |deriv (OutgoingSchedule.dropCoefficient m) y| ≤ dropSpeed m / y

theorem NavierStokes.OutgoingEntranceCone.exists_small_dropSpeed {e : ℝ} (he : 0 < e) : ∃ (M : ℝ), 0 < M ∧ ∀ (m : ℝ), M ≤ m → dropSpeed m ≤ e

The actual angular source and its ideal incoming lag

noncomputable def NavierStokes.OutgoingEntranceCone.transportW (c : OutgoingSchedule.Parameters) (h y η : ℝ) : ℝ

Transport W, given by 1 - L h η * averagedDrop c y.

Equations

• NavierStokes.OutgoingEntranceCone.transportW c h y η = 1 - NavierStokes.NaturalAxisData.L h η * NavierStokes.OutgoingEntranceCone.averagedDrop c y

noncomputable def NavierStokes.OutgoingEntranceCone.angularRate (c : OutgoingSchedule.Parameters) (y : ℝ) : ℝ

Angular rate, given by 1 + slope c.dropLength c.lam y.

Equations

• NavierStokes.OutgoingEntranceCone.angularRate c y = 1 + NavierStokes.OutgoingSchedule.slope c.dropLength c.lam y

noncomputable def NavierStokes.OutgoingEntranceCone.angularSource (c : OutgoingSchedule.Parameters) (h η y : ℝ) : ℝ

Angular source as an element of ℝ.

Equations

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

noncomputable def NavierStokes.OutgoingEntranceCone.idealAngularSource (h η : ℝ) : ℝ

Ideal angular source, given by (3 / 5) * (4 * L h η - 1) - h * (1 - 8 * η ^ 2) + (D h + 4 * d η) * η * shapeGradient η.

Equations

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

noncomputable def NavierStokes.OutgoingEntranceCone.idealAngularLag (h η : ℝ) : ℝ

Ideal angular lag, given by idealAngularSource h η / (8 / 5).

Equations

• NavierStokes.OutgoingEntranceCone.idealAngularLag h η = NavierStokes.OutgoingEntranceCone.idealAngularSource h η / (8 / 5)

noncomputable def NavierStokes.OutgoingEntranceCone.angularLag (c : OutgoingSchedule.Parameters) (h η : ℝ) : ℝ → ℝ

Angular lag, given by linearLag (angularRate c) (angularSource c h η) (idealAngularLag h η).

Equations

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

theorem NavierStokes.OutgoingEntranceCone.angularRate_contDiff (c : OutgoingSchedule.Parameters) : ContDiff ℝ (↑⊤) (angularRate c)

theorem NavierStokes.OutgoingEntranceCone.angularSource_contDiff (c : OutgoingSchedule.Parameters) (h η : ℝ) : ContDiff ℝ (↑⊤) (angularSource c h η)

theorem NavierStokes.OutgoingEntranceCone.angularLag_hasDerivAt (c : OutgoingSchedule.Parameters) (h η y : ℝ) : HasDerivAt (angularLag c h η) (angularSource c h η y - angularRate c y * angularLag c h η y) y

theorem NavierStokes.OutgoingEntranceCone.angularSource_ideal (c : OutgoingSchedule.Parameters) (h η : ℝ) {y : ℝ} (hy : y ≤ 0) : angularSource c h η y = idealAngularSource h η

theorem NavierStokes.OutgoingEntranceCone.idealAngularLag_is_incoming_integral (h η : ℝ) : ∫ (t : ℝ) in Set.Iic 0, Real.exp (8 / 5 * t) * idealAngularSource h η = idealAngularLag h η

theorem NavierStokes.OutgoingEntranceCone.natural_L_bounds {h η : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (hη : |η| ≤ 1) : 49 / 50 ≤ NaturalAxisData.L h η ∧ NaturalAxisData.L h η ≤ 1

theorem NavierStokes.OutgoingEntranceCone.idealAngularLag_lower {h η : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (hη : |η| ≤ 1) : 1 ≤ idealAngularLag h η

theorem NavierStokes.OutgoingEntranceCone.angularRate_bounds (c : OutgoingSchedule.Parameters) (y : ℝ) : 9 / 10 ≤ angularRate c y ∧ angularRate c y ≤ 8 / 5

theorem NavierStokes.OutgoingEntranceCone.slope_nonneg_before_dropEnd (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : y ≤ c.dropLength + 1) : 0 ≤ OutgoingSchedule.slope c.dropLength c.lam y

theorem NavierStokes.OutgoingEntranceCone.slope_nonpos_after_first_ramp (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : 1 ≤ y) : OutgoingSchedule.slope c.dropLength c.lam y ≤ 0

theorem NavierStokes.OutgoingEntranceCone.transportW_bounds (c : OutgoingSchedule.Parameters) {h y η : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (hy : 0 ≤ y) (hη : |η| ≤ 1) : -3 ≤ transportW c h y η ∧ transportW c h y η ≤ 1

theorem NavierStokes.OutgoingEntranceCone.transportW_second_ramp (c : OutgoingSchedule.Parameters) {h y η : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (hy : c.dropLength + 1 ≤ y) (hη : |η| ≤ 1) : 1 / 2 ≤ transportW c h y η

theorem NavierStokes.OutgoingEntranceCone.angularSource_lower (c : OutgoingSchedule.Parameters) {h η y : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (_hy : 0 ≤ y) (hη : |η| ≤ 1) : 49 / 100 * η ^ 2 - h ≤ angularSource c h η y

theorem NavierStokes.OutgoingEntranceCone.primitive_continuous_of_continuous {r : ℝ → ℝ} (hr : Continuous r) : Continuous (OutgoingSchedule.primitive r)

theorem NavierStokes.OutgoingEntranceCone.integral_integratingFactor_rate {r : ℝ → ℝ} (hr : Continuous r) (y : ℝ) : ∫ (t : ℝ) in 0..y, Real.exp (OutgoingSchedule.primitive r t) * r t = Real.exp (OutgoingSchedule.primitive r y) - 1

theorem NavierStokes.OutgoingEntranceCone.linearLag_constant {r b : ℝ → ℝ} (hr : Continuous r) {q₀ y : ℝ} (hb : ∀ t ∈ Set.uIcc 0 y, b t = r t * q₀) : OutgoingTail.linearLag r b q₀ y = q₀

theorem NavierStokes.OutgoingEntranceCone.angularLag_ideal (c : OutgoingSchedule.Parameters) (h η : ℝ) {y : ℝ} (hy : y ≤ 0) : angularLag c h η y = idealAngularLag h η

theorem NavierStokes.OutgoingEntranceCone.linearLag_lower_barrier {r b : ℝ → ℝ} (hr : Continuous r) (hb : Continuous b) {q₀ β κ y : ℝ} (hy : 0 ≤ y) (hq : β + κ ≤ q₀) (hsource : ∀ t ∈ Set.Icc 0 y, r t * β ≤ b t) : β + κ * Real.exp (-OutgoingSchedule.primitive r y) ≤ OutgoingTail.linearLag r b q₀ y

theorem NavierStokes.OutgoingEntranceCone.slope_integral_upper (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : 0 ≤ y) : OutgoingSchedule.primitive (OutgoingSchedule.slope c.dropLength c.lam) y ≤ 3 / 5

theorem NavierStokes.OutgoingEntranceCone.angularRate_primitive (c : OutgoingSchedule.Parameters) (y : ℝ) : OutgoingSchedule.primitive (angularRate c) y = y + OutgoingSchedule.primitive (OutgoingSchedule.slope c.dropLength c.lam) y

theorem NavierStokes.OutgoingEntranceCone.angularRate_primitive_upper (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : 0 ≤ y) : OutgoingSchedule.primitive (angularRate c) y ≤ y + 3 / 5

theorem NavierStokes.OutgoingEntranceCone.angularSource_barrier (c : OutgoingSchedule.Parameters) {h η y : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (hy : 0 ≤ y) (hη : |η| ≤ 1) : angularRate c y * (η ^ 2 / 4 - 2 * h) ≤ angularSource c h η y

theorem NavierStokes.OutgoingEntranceCone.angularLag_barrier (c : OutgoingSchedule.Parameters) {h η y : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (hy : 0 ≤ y) (hη : |η| ≤ 1) : η ^ 2 / 4 - 2 * h + 1 / 2 * Real.exp (-(y + 3 / 5)) ≤ angularLag c h η y

noncomputable def NavierStokes.OutgoingEntranceCone.coneFloor : ℝ

Cone floor, given by Real.exp (-(3 / 5 : ℝ)) / 4.

Equations

• NavierStokes.OutgoingEntranceCone.coneFloor = Real.exp (-(3 / 5)) / 4

theorem NavierStokes.OutgoingEntranceCone.coneFloor_pos : 0 < coneFloor

theorem NavierStokes.OutgoingEntranceCone.coneFloor_le_quarter : coneFloor ≤ 1 / 4

theorem NavierStokes.OutgoingEntranceCone.angularLag_lower (c : OutgoingSchedule.Parameters) {h η y T : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (hy : 0 ≤ y) (hyT : y ≤ T) (hη : |η| ≤ 1) (hhT : h ≤ Real.exp (-(T + 3 / 5)) / 8) : coneFloor * (η ^ 2 + Real.exp (-y)) ≤ angularLag c h η y

The positive angular lag is derived from its incoming ideal integral and the true source. The constant is absolute and uniform in P, λ, h, m.

theorem NavierStokes.OutgoingEntranceCone.angularLag_pos (c : OutgoingSchedule.Parameters) {h η y T : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (hy : 0 ≤ y) (hyT : y ≤ T) (hη : |η| ≤ 1) (hhT : h ≤ Real.exp (-(T + 3 / 5)) / 8) : 0 < angularLag c h η y

The actual angular-energy history

noncomputable def NavierStokes.OutgoingEntranceCone.clockEnergy (c : OutgoingSchedule.Parameters) (y : ℝ) : ℝ

Clock energy, given by radialAmplitude c.P c.dropLength c.lam y ^ 2.

Equations

• NavierStokes.OutgoingEntranceCone.clockEnergy c y = NavierStokes.OutgoingSchedule.radialAmplitude c.P c.dropLength c.lam y ^ 2

noncomputable def NavierStokes.OutgoingEntranceCone.weightedClockEnergy (c : OutgoingSchedule.Parameters) (y : ℝ) : ℝ

Weighted clock energy, given by Real.exp y * clockEnergy c y.

Equations

• NavierStokes.OutgoingEntranceCone.weightedClockEnergy c y = Real.exp y * NavierStokes.OutgoingEntranceCone.clockEnergy c y

noncomputable def NavierStokes.OutgoingEntranceCone.averagedClockEnergy (c : OutgoingSchedule.Parameters) : ℝ → ℝ

Averaged clock energy, given by historyAverage (clockEnergy c) ((5 / 6) * c.P ^ 2).

Equations

• NavierStokes.OutgoingEntranceCone.averagedClockEnergy c = NavierStokes.OutgoingEntranceCone.historyAverage (NavierStokes.OutgoingEntranceCone.clockEnergy c) (5 / 6 * c.P ^ 2)

noncomputable def NavierStokes.OutgoingEntranceCone.averagedEnergy (c : OutgoingSchedule.Parameters) (y η : ℝ) : ℝ

Averaged energy, given by shape η ^ 2 * averagedClockEnergy c y.

Equations

• NavierStokes.OutgoingEntranceCone.averagedEnergy c y η = NavierStokes.OutgoingSchedule.shape η ^ 2 * NavierStokes.OutgoingEntranceCone.averagedClockEnergy c y

theorem NavierStokes.OutgoingEntranceCone.clockEnergy_contDiff (c : OutgoingSchedule.Parameters) : ContDiff ℝ (↑⊤) (clockEnergy c)

theorem NavierStokes.OutgoingEntranceCone.clockEnergy_pos (c : OutgoingSchedule.Parameters) (y : ℝ) : 0 < clockEnergy c y

theorem NavierStokes.OutgoingEntranceCone.clockEnergy_initial (c : OutgoingSchedule.Parameters) : clockEnergy c 0 = c.P ^ 2

theorem NavierStokes.OutgoingEntranceCone.clockEnergy_hasDerivAt (c : OutgoingSchedule.Parameters) (y : ℝ) : HasDerivAt (clockEnergy c) ((2 * OutgoingSchedule.slope c.dropLength c.lam y - 1) * clockEnergy c y) y

theorem NavierStokes.OutgoingEntranceCone.weightedClockEnergy_hasDerivAt (c : OutgoingSchedule.Parameters) (y : ℝ) : HasDerivAt (weightedClockEnergy c) (2 * OutgoingSchedule.slope c.dropLength c.lam y * weightedClockEnergy c y) y

theorem NavierStokes.OutgoingEntranceCone.weightedClockEnergy_monotone (c : OutgoingSchedule.Parameters) : MonotoneOn (weightedClockEnergy c) (Set.Iic (c.dropLength + 1))

theorem NavierStokes.OutgoingEntranceCone.clockEnergy_lower (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ c.dropLength + 1) : c.P ^ 2 * Real.exp (-y) ≤ clockEnergy c y

theorem NavierStokes.OutgoingEntranceCone.averagedClockEnergy_nonneg (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : 0 ≤ y) : 0 ≤ averagedClockEnergy c y

theorem NavierStokes.OutgoingEntranceCone.averagedClockEnergy_upper (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ c.dropLength + 1) : averagedClockEnergy c y ≤ (y + 5 / 6) * clockEnergy c y

theorem NavierStokes.OutgoingEntranceCone.averagedEnergy_upper (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ c.dropLength + 1) (η : ℝ) : averagedEnergy c y η ≤ (y + 5 / 6) * OutgoingSchedule.angular c.P c.dropLength c.lam (y, η) ^ 2

theorem NavierStokes.OutgoingEntranceCone.angular_square_lower (c : OutgoingSchedule.Parameters) {y η : ℝ} (hy : 0 ≤ y) (hy' : y ≤ c.dropLength + 1) (hη : |η| ≤ 1) : c.P ^ 2 / 4 * Real.exp (-y) ≤ OutgoingSchedule.angular c.P c.dropLength c.lam (y, η) ^ 2

theorem NavierStokes.OutgoingEntranceCone.clockEnergy_ideal (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : y ≤ 0) : clockEnergy c y = c.P ^ 2 * Real.exp (1 / 5 * y)

theorem NavierStokes.OutgoingEntranceCone.averagedClockEnergy_ideal (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : y ≤ 0) : averagedClockEnergy c y = 5 / 6 * clockEnergy c y

Pressure and the axial lag with the full ideal incoming history

noncomputable def NavierStokes.OutgoingEntranceCone.pressureClock (c : OutgoingSchedule.Parameters) (y : ℝ) : ℝ

Pressure clock, given by (5 / 2) * c.P ^ 2 + (1 / 2) * OutgoingSchedule.primitive (clockEnergy c) y.

Equations

• NavierStokes.OutgoingEntranceCone.pressureClock c y = 5 / 2 * c.P ^ 2 + 1 / 2 * NavierStokes.OutgoingSchedule.primitive (NavierStokes.OutgoingEntranceCone.clockEnergy c) y

noncomputable def NavierStokes.OutgoingEntranceCone.entrancePressure (v : OutgoingTail.TailData) (y η : ℝ) : ℝ

Entrance pressure, given by SchedulePressure.axisPressure v η + shape η ^ 2 * pressureClock v.core y.

Equations

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

noncomputable def NavierStokes.OutgoingEntranceCone.pressureGradient (v : OutgoingTail.TailData) (y η : ℝ) : ℝ

Pressure gradient, given by `deriv (SchedulePressure.axisPressure v) η - 2 * shapeGradient η

• shape η ^ 2 * pressureClock v.core y`.

Equations

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

theorem NavierStokes.OutgoingEntranceCone.shape_hasDerivAt (η : ℝ) : HasDerivAt OutgoingSchedule.shape (-shapeGradient η * OutgoingSchedule.shape η) η

theorem NavierStokes.OutgoingEntranceCone.shapeSquare_hasDerivAt (η : ℝ) : HasDerivAt (fun (t : ℝ) => OutgoingSchedule.shape t ^ 2) (-2 * shapeGradient η * OutgoingSchedule.shape η ^ 2) η

theorem NavierStokes.OutgoingEntranceCone.pressureClock_hasDerivAt (c : OutgoingSchedule.Parameters) (y : ℝ) : HasDerivAt (pressureClock c) (1 / 2 * clockEnergy c y) y

theorem NavierStokes.OutgoingEntranceCone.entrancePressure_hasDerivAt_eta (v : OutgoingTail.TailData) (y η : ℝ) : HasDerivAt (entrancePressure v y) (pressureGradient v y η) η

theorem NavierStokes.OutgoingEntranceCone.entrancePressure_hasDerivAt_y (v : OutgoingTail.TailData) (y η : ℝ) : HasDerivAt (fun (t : ℝ) => entrancePressure v t η) (1 / 2 * OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (y, η) ^ 2) y

theorem NavierStokes.OutgoingEntranceCone.pressureGradient_hasDerivAt_y (v : OutgoingTail.TailData) (y η : ℝ) : HasDerivAt (fun (t : ℝ) => pressureGradient v t η) (-shapeGradient η * OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (y, η) ^ 2) y

theorem NavierStokes.OutgoingEntranceCone.pressureClock_ideal (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : y ≤ 0) : pressureClock c y = 5 / 2 * clockEnergy c y

theorem NavierStokes.OutgoingEntranceCone.averagedDropSquare_early (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : y ≤ 1) : averagedDropSquare c y = 16

theorem NavierStokes.OutgoingEntranceCone.averagedDropSquare_hasDerivAt (c : OutgoingSchedule.Parameters) (y : ℝ) : HasDerivAt (averagedDropSquare c) (OutgoingSchedule.dropCoefficient c.m y ^ 2 - averagedDropSquare c y) y

theorem NavierStokes.OutgoingEntranceCone.averagedEnergy_hasDerivAt_y (c : OutgoingSchedule.Parameters) (y η : ℝ) : HasDerivAt (fun (t : ℝ) => averagedEnergy c t η) (OutgoingSchedule.angular c.P c.dropLength c.lam (y, η) ^ 2 - averagedEnergy c y η) y

theorem NavierStokes.OutgoingEntranceCone.averagedEnergy_hasDerivAt_eta (c : OutgoingSchedule.Parameters) (y η : ℝ) : HasDerivAt (averagedEnergy c y) (-2 * shapeGradient η * averagedEnergy c y η) η

theorem NavierStokes.OutgoingEntranceCone.transportW_hasDerivAt (c : OutgoingSchedule.Parameters) (h y η : ℝ) : HasDerivAt (fun (t : ℝ) => transportW c h t η) (-NaturalAxisData.L h η * (OutgoingSchedule.dropCoefficient c.m y - averagedDrop c y)) y

noncomputable def NavierStokes.OutgoingEntranceCone.geometricAxialLag (c : OutgoingSchedule.Parameters) (h y η : ℝ) : ℝ

The part of the axial lag arising from the actual mass and squared-axial histories.

Equations

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

noncomputable def NavierStokes.OutgoingEntranceCone.pressureAxialLag (v : OutgoingTail.TailData) (y η : ℝ) : ℝ

The pressure and angular-energy part of the integrated axial lag.

Equations

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

noncomputable def NavierStokes.OutgoingEntranceCone.axialLag (v : OutgoingTail.TailData) (y η : ℝ) : ℝ

Axial lag, given by geometricAxialLag v.core v.h y η + pressureAxialLag v y η.

Equations

• NavierStokes.OutgoingEntranceCone.axialLag v y η = NavierStokes.OutgoingEntranceCone.geometricAxialLag v.core v.h y η + NavierStokes.OutgoingEntranceCone.pressureAxialLag v y η

noncomputable def NavierStokes.OutgoingEntranceCone.geometricAxialSource (c : OutgoingSchedule.Parameters) (h y η : ℝ) : ℝ

Geometric axial source as an element of ℝ.

Equations

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

noncomputable def NavierStokes.OutgoingEntranceCone.pressureAxialSource (v : OutgoingTail.TailData) (y η : ℝ) : ℝ

Pressure axial source as an element of ℝ.

Equations

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

noncomputable def NavierStokes.OutgoingEntranceCone.axialSource (v : OutgoingTail.TailData) (y η : ℝ) : ℝ

Axial source, given by geometricAxialSource v.core v.h y η + pressureAxialSource v y η.

Equations

• NavierStokes.OutgoingEntranceCone.axialSource v y η = NavierStokes.OutgoingEntranceCone.geometricAxialSource v.core v.h y η + NavierStokes.OutgoingEntranceCone.pressureAxialSource v y η

theorem NavierStokes.OutgoingEntranceCone.geometricAxialLag_hasDerivAt (c : OutgoingSchedule.Parameters) (h y η : ℝ) : HasDerivAt (fun (t : ℝ) => geometricAxialLag c h t η) (geometricAxialSource c h y η - geometricAxialLag c h y η) y

theorem NavierStokes.OutgoingEntranceCone.pressureAxialLag_hasDerivAt (v : OutgoingTail.TailData) (y η : ℝ) : HasDerivAt (fun (t : ℝ) => pressureAxialLag v t η) (pressureAxialSource v y η - pressureAxialLag v y η) y

theorem NavierStokes.OutgoingEntranceCone.axialLag_hasDerivAt (v : OutgoingTail.TailData) (y η : ℝ) : HasDerivAt (fun (t : ℝ) => axialLag v t η) (axialSource v y η - axialLag v y η) y

noncomputable def NavierStokes.OutgoingEntranceCone.normalizedEnergyHistory (c : OutgoingSchedule.Parameters) (y η : ℝ) : ℝ

Normalized energy history S/X, including both ideal-prefix integrals.

Equations

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

theorem NavierStokes.OutgoingEntranceCone.normalizedEnergyHistory_hasDerivAt_eta (c : OutgoingSchedule.Parameters) (y η : ℝ) : HasDerivAt (normalizedEnergyHistory c y) (2 * η * averagedDropSquare c y + shapeGradient η * averagedEnergy c y η) η

theorem NavierStokes.OutgoingEntranceCone.axialLag_integrated_history (v : OutgoingTail.TailData) (y η : ℝ) : axialLag v y η = -transportW v.core v.h y η * (OutgoingSchedule.dropCoefficient v.core.m y * η) + 4 * v.h * η * normalizedEnergyHistory v.core y η - NaturalAxisData.d η * deriv (normalizedEnergyHistory v.core y) η + 4 * NaturalAxisData.A v.h * η * entrancePressure v y η - NaturalAxisData.d η * deriv (entrancePressure v y) η

This is precisely the axial integrated-history formula (9); the linear mass-history contribution D(M-η Mη)/X vanishes for U=k(y)η.

theorem NavierStokes.OutgoingEntranceCone.geometricAxialLag_ideal (c : OutgoingSchedule.Parameters) (h η : ℝ) {y : ℝ} (hy : y ≤ 0) : geometricAxialLag c h y η = -20 * η + (32 + 32 * h) * η ^ 3

theorem NavierStokes.OutgoingEntranceCone.pressureAxialLag_ideal (v : OutgoingTail.TailData) (η : ℝ) {y : ℝ} (hy : y ≤ 0) : pressureAxialLag v y η = 4 * NaturalAxisData.A v.h * η * SchedulePressure.axisPressure v η - NaturalAxisData.d η * deriv (SchedulePressure.axisPressure v) η + 5 / 6 * (5 * NaturalAxisData.d η * shapeGradient η + (10 * NaturalAxisData.A v.h + 1) * η) * OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (y, η) ^ 2

theorem NavierStokes.OutgoingEntranceCone.entrancePressure_eq_future (v : OutgoingTail.TailData) {y : ℝ} (hy : 0 ≤ y) (hyend : y ≤ v.core.endpoint) : entrancePressure v y = FuturePressureBounds.Pi v y

theorem NavierStokes.OutgoingEntranceCone.pressureGradient_eq_future (v : OutgoingTail.TailData) {y : ℝ} (hy : 0 ≤ y) (hyend : y ≤ v.core.endpoint) : pressureGradient v y = deriv (FuturePressureBounds.Pi v y)

noncomputable def NavierStokes.OutgoingEntranceCone.pressureBound : ℝ

Pressure bound, given by 10 * FuturePressureBounds.envelopeConstant.

Equations

• NavierStokes.OutgoingEntranceCone.pressureBound = 10 * NavierStokes.FuturePressureBounds.envelopeConstant

theorem NavierStokes.OutgoingEntranceCone.pressureBound_pos : 0 < pressureBound

theorem NavierStokes.OutgoingEntranceCone.actual_pressure_bounds (v : OutgoingTail.TailData) {y η : ℝ} (hy : 0 ≤ y) (hyend : y ≤ v.core.endpoint) (hη : |η| ≤ 1) : |entrancePressure v y η| ≤ pressureBound * OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (y, η) ^ 2 ∧ |pressureGradient v y η| ≤ pressureBound * |η| * OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (y, η) ^ 2 ∧ |deriv (pressureGradient v y) η| ≤ pressureBound * OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (y, η) ^ 2

theorem NavierStokes.OutgoingEntranceCone.geometricAxialLag_bound (c : OutgoingSchedule.Parameters) {h y η : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (hy : 0 ≤ y) (hη : |η| ≤ 1) : |geometricAxialLag c h y η| ≤ 64 * |η|

theorem NavierStokes.OutgoingEntranceCone.pressure_coefficient_bound {h η : ℝ} (hh : 0 ≤ h) (hh1 : h ≤ 1 / 100) (hη : |η| ≤ 1) : |2 * h * η + NaturalAxisData.d η * shapeGradient η| ≤ 3 * |η|

theorem NavierStokes.OutgoingEntranceCone.pressureAxialLag_bound (v : OutgoingTail.TailData) {y η : ℝ} (hh1 : v.h ≤ 1 / 100) (hy : 0 ≤ y) (hy' : y ≤ v.core.dropLength + 1) (hη : |η| ≤ 1) : |pressureAxialLag v y η| ≤ (3 * (y + 1) + 4 * pressureBound) * |η| * OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (y, η) ^ 2

noncomputable def NavierStokes.OutgoingEntranceCone.axialBound : ℝ

Axial bound, given by 259 + 4 * pressureBound.

Equations

• NavierStokes.OutgoingEntranceCone.axialBound = 259 + 4 * NavierStokes.OutgoingEntranceCone.pressureBound

theorem NavierStokes.OutgoingEntranceCone.axialBound_pos : 0 < axialBound

theorem NavierStokes.OutgoingEntranceCone.axialLag_drop_bound (v : OutgoingTail.TailData) {y η : ℝ} (hh1 : v.h ≤ 1 / 100) (hy : 0 ≤ y) (hy' : y ≤ v.core.dropLength + 1) (hη : |η| ≤ 1) (hP : Real.exp (v.core.dropLength + 1) ≤ v.core.P ^ 2) : |axialLag v y η| ≤ axialBound * |η| * (1 + y) * OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (y, η) ^ 2

The actual full axial lag has the required normalized drop bound. The geometric part is suppressed by choosing the fixed prefix amplitude first.

The two small shear quantities in the cone test

noncomputable def NavierStokes.OutgoingEntranceCone.shear (c : OutgoingSchedule.Parameters) (y η : ℝ) : ℝ

Shear, given by 2 * deriv (dropCoefficient c.m) y * η / angular c.P c.dropLength c.lam (y, η).

Equations

• NavierStokes.OutgoingEntranceCone.shear c y η = 2 * deriv (NavierStokes.OutgoingSchedule.dropCoefficient c.m) y * η / NavierStokes.OutgoingSchedule.angular c.P c.dropLength c.lam (y, η)

noncomputable def NavierStokes.OutgoingEntranceCone.directionRatio (v : OutgoingTail.TailData) (y η : ℝ) : ℝ

Direction ratio, given by axialLag v y η / (angular v.core.P v.core.dropLength v.core.lam (y, η) * angularLag v.core v.h η y).

Equations

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

noncomputable def NavierStokes.OutgoingEntranceCone.radialA (c : OutgoingSchedule.Parameters) (y : ℝ) : ℝ

Radial A, given by 2 - 2 * slope c.dropLength c.lam y.

Equations

• NavierStokes.OutgoingEntranceCone.radialA c y = 2 - 2 * NavierStokes.OutgoingSchedule.slope c.dropLength c.lam y

theorem NavierStokes.OutgoingEntranceCone.shear_is_actual (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) {y : ℝ} (hy : y < c.pulseStart) (η : ℝ) : shear c y η = 2 * deriv (fun (t : ℝ) => OutgoingSchedule.axial c amp (t, η)) y / OutgoingSchedule.angular c.P c.dropLength c.lam (y, η)

theorem NavierStokes.OutgoingEntranceCone.angular_square_ge_quarter (c : OutgoingSchedule.Parameters) {y η : ℝ} (hy : 0 ≤ y) (hy' : y ≤ c.dropLength + 1) (hη : |η| ≤ 1) (hP : Real.exp (c.dropLength + 1) ≤ c.P ^ 2) : 1 / 4 ≤ OutgoingSchedule.angular c.P c.dropLength c.lam (y, η) ^ 2

theorem NavierStokes.OutgoingEntranceCone.shear_drop_abs (c : OutgoingSchedule.Parameters) {y η : ℝ} (hy : 1 ≤ y) (hy' : y ≤ c.dropLength + 1) (hη : |η| ≤ 1) (hP : Real.exp (c.dropLength + 1) ≤ c.P ^ 2) : |shear c y η| ≤ 4 * dropSpeed c.m

theorem NavierStokes.OutgoingEntranceCone.shear_drop_square (c : OutgoingSchedule.Parameters) {y η : ℝ} (hy : 1 ≤ y) (hy' : y ≤ c.dropLength + 1) (hη : |η| ≤ 1) (hP : Real.exp (c.dropLength + 1) ≤ c.P ^ 2) : shear c y η ^ 2 ≤ 16 * dropSpeed c.m ^ 2

theorem NavierStokes.OutgoingEntranceCone.shear_direction_identity (v : OutgoingTail.TailData) (y η : ℝ) (hQ : 0 < angularLag v.core v.h η y) : |shear v.core y η * directionRatio v y η| = 2 * |deriv (OutgoingSchedule.dropCoefficient v.core.m) y| * |η| * |axialLag v y η| / (OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (y, η) ^ 2 * angularLag v.core v.h η y)

theorem NavierStokes.OutgoingEntranceCone.shear_direction_drop_bound (v : OutgoingTail.TailData) {y η : ℝ} (hh1 : v.h ≤ 1 / 100) (hy : 1 ≤ y) (hy' : y ≤ v.core.dropLength + 1) (hη : |η| ≤ 1) (hP : Real.exp (v.core.dropLength + 1) ≤ v.core.P ^ 2) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) : |shear v.core y η * directionRatio v y η| ≤ 4 * axialBound / coneFloor * dropSpeed v.core.m

theorem NavierStokes.OutgoingEntranceCone.radialA_drop (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : 1 ≤ y) (hy' : y ≤ c.dropLength + 1) : radialA c y = 2

theorem NavierStokes.OutgoingEntranceCone.drop_cone_margins (v : OutgoingTail.TailData) {y η : ℝ} (hh1 : v.h ≤ 1 / 100) (hy : 1 ≤ y) (hy' : y ≤ v.core.dropLength + 1) (hη : |η| ≤ 1) (hP : Real.exp (v.core.dropLength + 1) ≤ v.core.P ^ 2) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) (he : dropSpeed v.core.m ≤ min (1 / 8) (coneFloor / (16 * axialBound))) : 7 / 4 ≤ radialA v.core y - shear v.core y η * directionRatio v y η ∧ 2 * shear v.core y η * directionRatio v y η + shear v.core y η ^ 2 / radialA v.core y + (radialA v.core y - 2) * directionRatio v y η ^ 2 ≤ 5 / 8

Quantified strict margins in the preliminary drop cone.

theorem NavierStokes.OutgoingEntranceCone.linearLag_pos_after {r b : ℝ → ℝ} (hr : Continuous r) (hb : Continuous b) {q₀ a y : ℝ} (hay : a ≤ y) (ha : 0 < OutgoingTail.linearLag r b q₀ a) (hs : ∀ t ∈ Set.Icc a y, 0 ≤ b t) : 0 < OutgoingTail.linearLag r b q₀ y

theorem NavierStokes.OutgoingEntranceCone.angularSource_hold_lower (v : OutgoingTail.TailData) {y η : ℝ} (hh1 : v.h ≤ 1 / 100) (hy : v.core.holdStart ≤ y) (hη : |η| ≤ 1) : v.core.lam / 2 - v.h ≤ angularSource v.core v.h η y

theorem NavierStokes.OutgoingEntranceCone.angularLag_pos_on_hold (v : OutgoingTail.TailData) {y η : ℝ} (hh1 : v.h ≤ 1 / 100) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) (hy : v.core.holdStart ≤ y) (hη : |η| ≤ 1) : 0 < angularLag v.core v.h η y

Positive incoming angular lag at every point of the unedited shaped hold.

theorem NavierStokes.OutgoingEntranceCone.angularLag_pos_at_pulseStart (v : OutgoingTail.TailData) {η : ℝ} (hh1 : v.h ≤ 1 / 100) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) (hη : |η| ≤ 1) : 0 < angularLag v.core v.h η v.core.pulseStart

A parameter-uniform bound at the shaped-wait entrance

theorem NavierStokes.OutgoingEntranceCone.shape_interval {η : ℝ} (hη : |η| ≤ 1) : 1 / 2 ≤ OutgoingSchedule.shape η ∧ OutgoingSchedule.shape η ≤ 1

noncomputable def NavierStokes.OutgoingEntranceCone.entranceTime (m : ℝ) : ℝ

Entrance time, given by Real.exp m + 12.

Equations

• NavierStokes.OutgoingEntranceCone.entranceTime m = Real.exp m + 12

theorem NavierStokes.OutgoingEntranceCone.holdStart_eq_entranceTime (c : OutgoingSchedule.Parameters) : c.holdStart = entranceTime c.m

noncomputable def NavierStokes.OutgoingEntranceCone.energyEnvelope (P T : ℝ) : ℝ

Energy envelope, given by P ^ 2 * Real.exp (2 * T).

Equations

• NavierStokes.OutgoingEntranceCone.energyEnvelope P T = P ^ 2 * Real.exp (2 * T)

theorem NavierStokes.OutgoingEntranceCone.clockEnergy_le_envelope (c : OutgoingSchedule.Parameters) {y T : ℝ} (hy : 0 ≤ y) (hyT : y ≤ T) : clockEnergy c y ≤ energyEnvelope c.P T

theorem NavierStokes.OutgoingEntranceCone.angular_square_le_envelope (c : OutgoingSchedule.Parameters) {y T η : ℝ} (hy : 0 ≤ y) (hyT : y ≤ T) (hη : |η| ≤ 1) : OutgoingSchedule.angular c.P c.dropLength c.lam (y, η) ^ 2 ≤ energyEnvelope c.P T

theorem NavierStokes.OutgoingEntranceCone.averagedEnergy_le_envelope (c : OutgoingSchedule.Parameters) {y T η : ℝ} (hy : 0 ≤ y) (hyT : y ≤ T) (hη : |η| ≤ 1) : averagedEnergy c y η ≤ energyEnvelope c.P T

theorem NavierStokes.OutgoingEntranceCone.angular_lower_envelope (c : OutgoingSchedule.Parameters) {y T η : ℝ} (hy : 0 ≤ y) (hyT : y ≤ T) (hη : |η| ≤ 1) : c.P * Real.exp (-T) / 2 ≤ OutgoingSchedule.angular c.P c.dropLength c.lam (y, η)

theorem NavierStokes.OutgoingEntranceCone.pressureAxialLag_le_envelope (v : OutgoingTail.TailData) {y T η : ℝ} (hh1 : v.h ≤ 1 / 100) (hy : 0 ≤ y) (hyT : y ≤ T) (hyend : y ≤ v.core.endpoint) (hη : |η| ≤ 1) : |pressureAxialLag v y η| ≤ (3 + 4 * pressureBound) * |η| * energyEnvelope v.core.P T

theorem NavierStokes.OutgoingEntranceCone.axialLag_le_envelope (v : OutgoingTail.TailData) {y T η : ℝ} (hh1 : v.h ≤ 1 / 100) (hy : 0 ≤ y) (hyT : y ≤ T) (hyend : y ≤ v.core.endpoint) (hη : |η| ≤ 1) : |axialLag v y η| ≤ 64 + (3 + 4 * pressureBound) * energyEnvelope v.core.P T

noncomputable def NavierStokes.OutgoingEntranceCone.entranceRatioBound (P m : ℝ) : ℝ

Entrance ratio bound as an element of ℝ.

Equations

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

theorem NavierStokes.OutgoingEntranceCone.entranceRatioBound_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < entranceRatioBound P m

theorem NavierStokes.OutgoingEntranceCone.directionRatio_entrance_bound (v : OutgoingTail.TailData) {y η : ℝ} (hh1 : v.h ≤ 1 / 100) (hy : 0 ≤ y) (hyT : y ≤ v.core.holdStart) (hη : |η| ≤ 1) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) : |directionRatio v y η| ≤ entranceRatioBound v.core.P v.core.m

A fixed pre-λ bound on the ratio throughout the first ramp, drop, and shaped-wait entrance. It depends only on the already fixed P,m.

Identification with the canonical, incoming-history fields

theorem NavierStokes.OutgoingEntranceCone.linearLag_eq_of_solution {r b f : ℝ → ℝ} (hr : Continuous r) (hb : Continuous b) {q₀ y : ℝ} (hf₀ : f 0 = q₀) (hf : ∀ t ∈ Set.uIcc 0 y, HasDerivAt f (b t - r t * f t) t) : f y = OutgoingTail.linearLag r b q₀ y

theorem NavierStokes.OutgoingEntranceCone.canonical_Ubar_before (v : OutgoingTail.TailData) (Amp : ℝ → ℝ) {y : ℝ} (hy : y ≤ v.core.pulseStart) (η : ℝ) : OutgoingHistories.Ubar v Amp (y, η) = averagedDrop v.core y * η

theorem NavierStokes.OutgoingEntranceCone.canonical_Ubar_parameter_before (v : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {y : ℝ} (hy : y ≤ v.core.pulseStart) (η : ℝ) : OutgoingHistories.dEta (OutgoingHistories.Ubar v Amp) (y, η) = averagedDrop v.core y

theorem NavierStokes.OutgoingEntranceCone.canonical_W_before (v : OutgoingTail.TailData) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {y : ℝ} (hy : y ≤ v.core.pulseStart) (η : ℝ) : OutgoingHistories.W v Amp (y, η) = transportW v.core v.h y η

theorem NavierStokes.OutgoingEntranceCone.canonical_E_parameter_ratio {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {y : ℝ} (hy : y ≤ v.core.endpoint) (η : ℝ) : OutgoingHistories.dEta (OutgoingHistories.E w) (y, η) / OutgoingHistories.E w (y, η) = -shapeGradient η

theorem NavierStokes.OutgoingEntranceCone.canonical_H_radial_ratio {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {y : ℝ} (hy : y < v.core.endpoint) (η : ℝ) : OutgoingHistories.dY (OutgoingHistories.H w) (y, η) / OutgoingHistories.H w (y, η) = OutgoingSchedule.slope v.core.dropLength v.core.lam y

theorem NavierStokes.OutgoingEntranceCone.canonical_Sq_before {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {y : ℝ} (hy : y ≤ v.core.pulseStart) (η : ℝ) : OutgoingHistories.Sq w Amp (y, η) = angularSource v.core v.h η y

theorem NavierStokes.OutgoingEntranceCone.canonical_Qs_before {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ v.core.pulseStart) (η : ℝ) : OutgoingHistories.Qs w Amp (y, η) = angularLag v.core v.h η y

The positive scalar lag is exactly the canonical integrated angular stress. No positivity or cone assumption is used in this identification.

theorem NavierStokes.OutgoingEntranceCone.canonical_Qs_pos_at_pulseStart {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hh1 : v.h ≤ 1 / 100) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) {η : ℝ} (hη : |η| ≤ 1) : 0 < OutgoingHistories.Qs w Amp (v.core.pulseStart, η)

theorem NavierStokes.OutgoingEntranceCone.canonical_Pi_before {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {y : ℝ} (hy : y ≤ v.core.endpoint) (η : ℝ) : OutgoingHistories.Pi w (y, η) = entrancePressure v y η

theorem NavierStokes.OutgoingEntranceCone.canonical_S_before {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) (Amp : ℝ → ℝ) {y : ℝ} (hy : y ≤ v.core.pulseStart) (η : ℝ) : OutgoingHistories.S w Amp (y, η) / Real.exp y = normalizedEnergyHistory v.core y η

theorem NavierStokes.OutgoingEntranceCone.canonical_M_before (v : OutgoingTail.TailData) (Amp : ℝ → ℝ) {y : ℝ} (hy : y ≤ v.core.pulseStart) (η : ℝ) : OutgoingHistories.M v Amp (y, η) = Real.exp y * (averagedDrop v.core y * η)

theorem NavierStokes.OutgoingEntranceCone.canonical_Ns_before {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {y : ℝ} (hy : y ≤ v.core.pulseStart) (η : ℝ) : OutgoingHistories.Ns w Amp (y, η) = axialLag v y η

The first and last preliminary ramps

theorem NavierStokes.OutgoingEntranceCone.dropCoefficient_deriv_early {m y : ℝ} (hm : 0 < m) (hy : y ≤ 1) : deriv (OutgoingSchedule.dropCoefficient m) y = 0

theorem NavierStokes.OutgoingEntranceCone.dropCoefficient_deriv_late {m y : ℝ} (hm : 0 < m) (hy : Real.exp m < y) : deriv (OutgoingSchedule.dropCoefficient m) y = 0

theorem NavierStokes.OutgoingEntranceCone.shear_early (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : y ≤ 1) (η : ℝ) : shear c y η = 0

theorem NavierStokes.OutgoingEntranceCone.shear_second_ramp (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : c.dropLength + 1 ≤ y) (η : ℝ) : shear c y η = 0

theorem NavierStokes.OutgoingEntranceCone.radialA_bounds (c : OutgoingSchedule.Parameters) (y : ℝ) : 4 / 5 ≤ radialA c y ∧ radialA c y ≤ 11 / 5

theorem NavierStokes.OutgoingEntranceCone.radialA_upper_lam (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : 1 ≤ y) : radialA c y ≤ 2 + 2 * c.lam

theorem NavierStokes.OutgoingEntranceCone.first_ramp_cone_margins (v : OutgoingTail.TailData) {y : ℝ} (hy : y ≤ 1) (η : ℝ) : 4 / 5 ≤ radialA v.core y - shear v.core y η * directionRatio v y η ∧ 2 * shear v.core y η * directionRatio v y η + shear v.core y η ^ 2 / radialA v.core y + (radialA v.core y - 2) * directionRatio v y η ^ 2 ≤ 0

theorem NavierStokes.OutgoingEntranceCone.second_ramp_cone_margins (v : OutgoingTail.TailData) {y η : ℝ} (hh1 : v.h ≤ 1 / 100) (hy : v.core.dropLength + 1 ≤ y) (hyT : y ≤ v.core.holdStart) (hη : |η| ≤ 1) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) (hlam : v.core.lam * entranceRatioBound v.core.P v.core.m ^ 2 ≤ 1 / 4) : 2 ≤ radialA v.core y - shear v.core y η * directionRatio v y η ∧ 2 * shear v.core y η * directionRatio v y η + shear v.core y η ^ 2 / radialA v.core y + (radialA v.core y - 2) * directionRatio v y η ^ 2 ≤ 1 / 2

Uniform pressure-source estimates

theorem NavierStokes.OutgoingEntranceCone.pressureGradient_contDiff_eta (v : OutgoingTail.TailData) (y : ℝ) : ContDiff ℝ (↑⊤) (pressureGradient v y)

theorem NavierStokes.OutgoingEntranceCone.angularSquare_hasDerivAt_eta (c : OutgoingSchedule.Parameters) (y η : ℝ) : HasDerivAt (fun (t : ℝ) => OutgoingSchedule.angular c.P c.dropLength c.lam (y, t) ^ 2) (-2 * shapeGradient η * OutgoingSchedule.angular c.P c.dropLength c.lam (y, η) ^ 2) η

theorem NavierStokes.OutgoingEntranceCone.pressureAxialSource_hasDerivAt_eta (v : OutgoingTail.TailData) (y η : ℝ) : HasDerivAt (pressureAxialSource v y) ((2 + 4 * NaturalAxisData.A v.h) * η * pressureGradient v y η - NaturalAxisData.d η * deriv (pressureGradient v y) η + 4 * NaturalAxisData.A v.h * entrancePressure v y η + (1 - 2 * η * shapeGradient η) * OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (y, η) ^ 2) η

noncomputable def NavierStokes.OutgoingEntranceCone.pressureSourceBound : ℝ

Pressure source bound, given by 10 * pressureBound + 10.

Equations

• NavierStokes.OutgoingEntranceCone.pressureSourceBound = 10 * NavierStokes.OutgoingEntranceCone.pressureBound + 10

theorem NavierStokes.OutgoingEntranceCone.pressureSourceBound_pos : 0 < pressureSourceBound

theorem NavierStokes.OutgoingEntranceCone.pressureAxialSource_bound (v : OutgoingTail.TailData) {y η : ℝ} (hh1 : v.h ≤ 1 / 100) (hy : 0 ≤ y) (hyend : y ≤ v.core.endpoint) (hη : |η| ≤ 1) : |pressureAxialSource v y η| ≤ pressureSourceBound * |η| * OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (y, η) ^ 2

theorem NavierStokes.OutgoingEntranceCone.pressureAxialSource_deriv_bound (v : OutgoingTail.TailData) {y η : ℝ} (hh1 : v.h ≤ 1 / 100) (hy : 0 ≤ y) (hyend : y ≤ v.core.endpoint) (hη : |η| ≤ 1) : |deriv (pressureAxialSource v y) η| ≤ pressureSourceBound * OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (y, η) ^ 2

A single ordered choice of the preliminary parameters

noncomputable def NavierStokes.OutgoingEntranceCone.dropThreshold : ℝ

Drop threshold, given by min (1 / 8) (coneFloor / (16 * axialBound)).

Equations

• NavierStokes.OutgoingEntranceCone.dropThreshold = min (1 / 8) (NavierStokes.OutgoingEntranceCone.coneFloor / (16 * NavierStokes.OutgoingEntranceCone.axialBound))

noncomputable def NavierStokes.OutgoingEntranceCone.amplitudeThreshold (m : ℝ) : ℝ

Amplitude threshold, given by Real.exp (Real.exp m + 11) + 1.

Equations

• NavierStokes.OutgoingEntranceCone.amplitudeThreshold m = Real.exp (Real.exp m + 11) + 1

noncomputable def NavierStokes.OutgoingEntranceCone.lambdaThreshold (P m : ℝ) : ℝ

Lambda threshold, given by min (1 / 20) (1 / (4 * (entranceRatioBound P m ^ 2 + 1))).

Equations

• NavierStokes.OutgoingEntranceCone.lambdaThreshold P m = min (1 / 20) (1 / (4 * (NavierStokes.OutgoingEntranceCone.entranceRatioBound P m ^ 2 + 1)))

noncomputable def NavierStokes.OutgoingEntranceCone.heightThreshold (m lam : ℝ) : ℝ

Height threshold, given by min (1 / 100) (min (lam / 4) (Real.exp (-(entranceTime m + 3 / 5)) / 8)).

Equations

• NavierStokes.OutgoingEntranceCone.heightThreshold m lam = min (1 / 100) (min (lam / 4) (Real.exp (-(NavierStokes.OutgoingEntranceCone.entranceTime m + 3 / 5)) / 8))

theorem NavierStokes.OutgoingEntranceCone.dropThreshold_pos : 0 < dropThreshold

theorem NavierStokes.OutgoingEntranceCone.amplitudeThreshold_pos (m : ℝ) : 0 < amplitudeThreshold m

theorem NavierStokes.OutgoingEntranceCone.lambdaThreshold_pos (P m : ℝ) : 0 < lambdaThreshold P m

theorem NavierStokes.OutgoingEntranceCone.heightThreshold_pos (m : ℝ) {lam : ℝ} (hlam : 0 < lam) : 0 < heightThreshold m lam

theorem NavierStokes.OutgoingEntranceCone.preliminary_cone_margins (v : OutgoingTail.TailData) {y η : ℝ} (hh1 : v.h ≤ 1 / 100) (_hy : 0 ≤ y) (hyT : y ≤ v.core.holdStart) (hη : |η| ≤ 1) (hP : Real.exp (v.core.dropLength + 1) ≤ v.core.P ^ 2) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) (he : dropSpeed v.core.m ≤ dropThreshold) (hlam : v.core.lam * entranceRatioBound v.core.P v.core.m ^ 2 ≤ 1 / 4) : 4 / 5 ≤ radialA v.core y - shear v.core y η * directionRatio v y η ∧ 2 * shear v.core y η * directionRatio v y η + shear v.core y η ^ 2 / radialA v.core y + (radialA v.core y - 2) * directionRatio v y η ^ 2 ≤ 5 / 8

theorem NavierStokes.OutgoingEntranceCone.chosen_parameters_bounds (v : OutgoingTail.TailData) (hP : amplitudeThreshold v.core.m ≤ v.core.P) (hlam : v.core.lam ≤ lambdaThreshold v.core.P v.core.m) (hh : v.h ≤ heightThreshold v.core.m v.core.lam) : Real.exp (v.core.dropLength + 1) ≤ v.core.P ^ 2 ∧ v.core.lam * entranceRatioBound v.core.P v.core.m ^ 2 ≤ 1 / 4 ∧ v.h ≤ 1 / 100 ∧ v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8

theorem NavierStokes.OutgoingEntranceCone.exists_ordered_preliminary_bounds : ∃ (M : ℝ), 0 < M ∧ ∀ (v : OutgoingTail.TailData), M ≤ v.core.m → amplitudeThreshold v.core.m ≤ v.core.P → v.core.lam ≤ lambdaThreshold v.core.P v.core.m → v.h ≤ heightThreshold v.core.m v.core.lam → ∀ (y η : ℝ), 0 ≤ y → y ≤ v.core.holdStart → |η| ≤ 1 → coneFloor * (η ^ 2 + Real.exp (-y)) ≤ angularLag v.core v.h η y ∧ 4 / 5 ≤ radialA v.core y - shear v.core y η * directionRatio v y η ∧ 2 * shear v.core y η * directionRatio v y η + shear v.core y η ^ 2 / radialA v.core y + (radialA v.core y - 2) * directionRatio v y η ^ 2 ≤ 5 / 8

The drop is chosen first. All subsequent cutoffs display precisely which earlier parameters they depend on; the cone constants are absolute.

The actual stress-cone fields and finite amplitude

noncomputable def NavierStokes.OutgoingEntranceCone.coneA {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) (p : ℝ × ℝ) : ℝ

Cone A, given by 2 - 2 * (OutgoingHistories.dY (OutgoingHistories.H w) p / OutgoingHistories.H w p).

Equations

• NavierStokes.OutgoingEntranceCone.coneA w p = 2 - 2 * (NavierStokes.OutgoingHistories.dY (NavierStokes.OutgoingHistories.H w) p / NavierStokes.OutgoingHistories.H w p)

noncomputable def NavierStokes.OutgoingEntranceCone.coneB {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) (Amp : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Cone B, given by 2 * OutgoingHistories.dY (OutgoingHistories.U v Amp) p / OutgoingHistories.E w p.

Equations

• NavierStokes.OutgoingEntranceCone.coneB w Amp p = 2 * NavierStokes.OutgoingHistories.dY (NavierStokes.OutgoingHistories.U v Amp) p / NavierStokes.OutgoingHistories.E w p

noncomputable def NavierStokes.OutgoingEntranceCone.coneRatio {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) (Amp : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Cone ratio, given by OutgoingHistories.Ns w Amp p / (OutgoingHistories.E w p * OutgoingHistories.Qs w Amp p).

Equations

• NavierStokes.OutgoingEntranceCone.coneRatio w Amp p = NavierStokes.OutgoingHistories.Ns w Amp p / (NavierStokes.OutgoingHistories.E w p * NavierStokes.OutgoingHistories.Qs w Amp p)

noncomputable def NavierStokes.OutgoingEntranceCone.preliminaryWindow (v : OutgoingTail.TailData) : Set (ℝ × ℝ)

Preliminary window, given by Icc 0 v.core.holdStart ×ˢ Icc (-1) 1.

Equations

• NavierStokes.OutgoingEntranceCone.preliminaryWindow v = Set.Icc 0 v.core.holdStart ×ˢ Set.Icc (-1) 1

theorem NavierStokes.OutgoingEntranceCone.coneA_before {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {y : ℝ} (hy : y < v.core.endpoint) (η : ℝ) : coneA w (y, η) = radialA v.core y

theorem NavierStokes.OutgoingEntranceCone.coneB_before {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {y : ℝ} (hy : y < v.core.pulseStart) (η : ℝ) : coneB w Amp (y, η) = shear v.core y η

theorem NavierStokes.OutgoingEntranceCone.coneRatio_before {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ v.core.pulseStart) (η : ℝ) : coneRatio w Amp (y, η) = directionRatio v y η

theorem NavierStokes.OutgoingEntranceCone.canonical_Qs_lower {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {y η : ℝ} (hh1 : v.h ≤ 1 / 100) (hy : 0 ≤ y) (hyT : y ≤ v.core.holdStart) (hη : |η| ≤ 1) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) : coneFloor * (η ^ 2 + Real.exp (-y)) ≤ OutgoingHistories.Qs w Amp (y, η)

theorem NavierStokes.OutgoingEntranceCone.canonical_Qs_pos {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {y η : ℝ} (hh1 : v.h ≤ 1 / 100) (hy : 0 ≤ y) (hyT : y ≤ v.core.holdStart) (hη : |η| ≤ 1) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) : 0 < OutgoingHistories.Qs w Amp (y, η)

theorem NavierStokes.OutgoingEntranceCone.coneA_continuous {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) : Continuous (coneA w)

theorem NavierStokes.OutgoingEntranceCone.coneB_continuous {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) : Continuous (coneB w Amp)

theorem NavierStokes.OutgoingEntranceCone.coneRatio_continuousOn {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hh1 : v.h ≤ 1 / 100) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) : ContinuousOn (coneRatio w Amp) (preliminaryWindow v)

theorem NavierStokes.OutgoingEntranceCone.actual_preliminary_margins {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hh1 : v.h ≤ 1 / 100) (hP : Real.exp (v.core.dropLength + 1) ≤ v.core.P ^ 2) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) (he : dropSpeed v.core.m ≤ dropThreshold) (hlam : v.core.lam * entranceRatioBound v.core.P v.core.m ^ 2 ≤ 1 / 4) {p : ℝ × ℝ} (hp : p ∈ preliminaryWindow v) : 4 / 5 ≤ coneA w p - coneB w Amp p * coneRatio w Amp p ∧ 2 * coneB w Amp p * coneRatio w Amp p + coneB w Amp p ^ 2 / coneA w p + (coneA w p - 2) * coneRatio w Amp p ^ 2 ≤ 5 / 8

theorem NavierStokes.OutgoingEntranceCone.compact_actual_preliminary_cone {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hh1 : v.h ≤ 1 / 100) (hP : Real.exp (v.core.dropLength + 1) ≤ v.core.P ^ 2) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) (he : dropSpeed v.core.m ≤ dropThreshold) (hlam : v.core.lam * entranceRatioBound v.core.P v.core.m ^ 2 ≤ 1 / 4) : ∃ (gap : ℝ) (p₀ : ℝ), 0 < gap ∧ 0 ≤ p₀ ∧ ∀ (s : ℝ), p₀ < s → ∀ p ∈ preliminaryWindow v, 2 + gap < s * (1 - coneB w Amp p * coneRatio w Amp p / coneA w p) ∧ coneA w p * (1 + (coneB w Amp p / coneA w p) ^ 2) + gap < ConeAlgebra.coneBound (s * (1 - coneB w Amp p * coneRatio w Amp p / coneA w p)) (s * (coneRatio w Amp p + coneB w Amp p / coneA w p))

Uniform finite-amplitude relaxed cone for the actual history stresses on the whole preliminary interval. Both root inequalities have a common gap.

theorem NavierStokes.OutgoingEntranceCone.actual_stress_amplitude_lower {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hh1 : v.h ≤ 1 / 100) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) {XR : ℝ} (hXR : 0 ≤ XR) {p : ℝ × ℝ} (hp : p ∈ preliminaryWindow v) : XR * coneFloor ≤ OutgoingHistories.p1 XR w Amp p

theorem NavierStokes.OutgoingEntranceCone.exists_actual_preliminary_cone_scale {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hh1 : v.h ≤ 1 / 100) (hP : Real.exp (v.core.dropLength + 1) ≤ v.core.P ^ 2) (hhT : v.h ≤ Real.exp (-(v.core.holdStart + 3 / 5)) / 8) (he : dropSpeed v.core.m ≤ dropThreshold) (hlam : v.core.lam * entranceRatioBound v.core.P v.core.m ^ 2 ≤ 1 / 4) : ∃ (gap : ℝ) (XR₀ : ℝ), 0 < gap ∧ 0 < XR₀ ∧ ∀ (XR : ℝ), XR₀ < XR → ∀ p ∈ preliminaryWindow v, 2 + gap < OutgoingHistories.p1 XR w Amp p * (1 - coneB w Amp p * coneRatio w Amp p / coneA w p) ∧ coneA w p * (1 + (coneB w Amp p / coneA w p) ^ 2) + gap < ConeAlgebra.coneBound (OutgoingHistories.p1 XR w Amp p * (1 - coneB w Amp p * coneRatio w Amp p / coneA w p)) (OutgoingHistories.p1 XR w Amp p * (coneRatio w Amp p + coneB w Amp p / coneA w p))

A single large physical radial scale gives the actual relaxed cone, uniformly in the complete first-ramp/drop/entrance region.

theorem NavierStokes.OutgoingEntranceCone.canonical_Qs_before_all {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {y : ℝ} (hy : y ≤ v.core.pulseStart) (η : ℝ) : OutgoingHistories.Qs w Amp (y, η) = angularLag v.core v.h η y

The same canonical identification is valid to the left of clock zero.

theorem NavierStokes.OutgoingEntranceCone.canonical_Qs_ideal {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {y : ℝ} (hy : y ≤ 0) (η : ℝ) : OutgoingHistories.Qs w Amp (y, η) = idealAngularLag v.h η

theorem NavierStokes.OutgoingEntranceCone.canonical_Qs_ideal_lower {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hh1 : v.h ≤ 1 / 100) {y η : ℝ} (hy : y ≤ 0) (hη : |η| ≤ 1) : 1 ≤ OutgoingHistories.Qs w Amp (y, η)

theorem NavierStokes.OutgoingEntranceCone.canonical_Ns_ideal {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {y : ℝ} (hy : y ≤ 0) (η : ℝ) : OutgoingHistories.Ns w Amp (y, η) = -20 * η + (32 + 32 * v.h) * η ^ 3 + (4 * NaturalAxisData.A v.h * η * SchedulePressure.axisPressure v η - NaturalAxisData.d η * deriv (SchedulePressure.axisPressure v) η + 5 / 6 * (5 * NaturalAxisData.d η * shapeGradient η + (10 * NaturalAxisData.A v.h + 1) * η) * OutgoingSchedule.angular v.core.P v.core.dropLength v.core.lam (y, η) ^ 2)

theorem NavierStokes.OutgoingEntranceCone.actual_ideal_cone_margins {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {y : ℝ} (hy : y ≤ 0) (η : ℝ) : coneA w (y, η) = 4 / 5 ∧ coneB w Amp (y, η) = 0 ∧ 0 < coneA w (y, η) - coneB w Amp (y, η) * coneRatio w Amp (y, η) ∧ 2 * coneB w Amp (y, η) * coneRatio w Amp (y, η) + coneB w Amp (y, η) ^ 2 / coneA w (y, η) + (coneA w (y, η) - 2) * coneRatio w Amp (y, η) ^ 2 ≤ 0

theorem NavierStokes.OutgoingEntranceCone.coneA_eq_E_derivative {v : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness v K) (p : ℝ × ℝ) : coneA w p = 1 - 2 * OutgoingHistories.dY (OutgoingHistories.E w) p / OutgoingHistories.E w p

The radial normal coefficient agrees with the logarithmic derivative of the true angular field E, rather than a declared slope proxy.

theorem NavierStokes.OutgoingEntranceCone.exists_ordered_actual_preliminary_cone : ∃ (M : ℝ), 0 < M ∧ ∀ (v : OutgoingTail.TailData), M ≤ v.core.m → amplitudeThreshold v.core.m ≤ v.core.P → v.core.lam ≤ lambdaThreshold v.core.P v.core.m → v.h ≤ heightThreshold v.core.m v.core.lam → ∀ {K : ℝ} (w : UniformAngularReset.ResetWitness v K) {Amp : ℝ → ℝ}, ContDiff ℝ (↑⊤) Amp → (∀ (y η : ℝ), 0 ≤ y → y ≤ v.core.holdStart → |η| ≤ 1 → coneFloor * (η ^ 2 + Real.exp (-y)) ≤ OutgoingHistories.Qs w Amp (y, η)) ∧ ∃ (gap : ℝ) (XR₀ : ℝ), 0 < gap ∧ 0 < XR₀ ∧ ∀ (XR : ℝ), XR₀ < XR → ∀ p ∈ preliminaryWindow v, 2 + gap < OutgoingHistories.p1 XR w Amp p * (1 - coneB w Amp p * coneRatio w Amp p / coneA w p) ∧ coneA w p * (1 + (coneB w Amp p / coneA w p) ^ 2) + gap < ConeAlgebra.coneBound (OutgoingHistories.p1 XR w Amp p * (1 - coneB w Amp p * coneRatio w Amp p / coneA w p)) (OutgoingHistories.p1 XR w Amp p * (coneRatio w Amp p + coneB w Amp p / coneA w p))

Ordered parameter selection for actual histories, followed by the final physical radial-scale choice. All thresholds before XR are explicit.