The actual pulse contribution to the outgoing stress cone

The endpoint lower bound, pulse stress expansions, and numerical cone margins are derived from the actual corrected fields and their histories. One small-parameter threshold preserves every prechosen reset witness.

The actual outgoing pulse lag

The exponential convolution is expanded by two integrations by parts. The resulting remainder is controlled by the actual second derivative of the forcing, with constants uniform in the pulse duration.

noncomputable def NavierStokes.PulseLag.kernel (β y t : ℝ) : ℝ

Kernel, given by Real.exp (-β * (y - t)).

Equations

• NavierStokes.PulseLag.kernel β y t = Real.exp (-β * (y - t))

noncomputable def NavierStokes.PulseLag.convolution (β : ℝ) (f : ℝ → ℝ) (y : ℝ) : ℝ

Convolution, given by ∫ t in (0 : ℝ)..y, kernel β y t * f t.

Equations

• NavierStokes.PulseLag.convolution β f y = ∫ (t : ℝ) in 0..y, NavierStokes.PulseLag.kernel β y t * f t

noncomputable def NavierStokes.PulseLag.lag (β m₀ : ℝ) (f : ℝ → ℝ) (y : ℝ) : ℝ

Lag, given by m₀ * Real.exp (-β * y) + convolution β f y.

Equations

• NavierStokes.PulseLag.lag β m₀ f y = m₀ * Real.exp (-β * y) + NavierStokes.PulseLag.convolution β f y

theorem NavierStokes.PulseLag.kernel_pos (β y t : ℝ) : 0 < kernel β y t

theorem NavierStokes.PulseLag.kernel_continuous (β y : ℝ) : Continuous (kernel β y)

theorem NavierStokes.PulseLag.kernel_hasDerivAt (β y t : ℝ) : HasDerivAt (kernel β y) (β * kernel β y t) t

theorem NavierStokes.PulseLag.convolution_eq_weighted (β : ℝ) (f : ℝ → ℝ) (y : ℝ) : convolution β f y = Real.exp (-β * y) * ∫ (t : ℝ) in 0..y, Real.exp (β * t) * f t

theorem NavierStokes.PulseLag.kernel_integral {β : ℝ} (hβ : β ≠ 0) (y : ℝ) : ∫ (t : ℝ) in 0..y, kernel β y t = (1 - Real.exp (-β * y)) / β

theorem NavierStokes.PulseLag.convolution_abs_le {β M y : ℝ} (hβ : 0 < β) (hM : 0 ≤ M) (hy : 0 ≤ y) {f : ℝ → ℝ} (hf : Continuous f) (hbound : ∀ t ∈ Set.Icc 0 y, |f t| ≤ M) : |convolution β f y| ≤ M / β

theorem NavierStokes.PulseLag.convolution_second_order {β : ℝ} (hβ : β ≠ 0) {f f₁ f₂ : ℝ → ℝ} (hf : ∀ (t : ℝ), HasDerivAt f (f₁ t) t) (hf₁ : ∀ (t : ℝ), HasDerivAt f₁ (f₂ t) t) (hf₂ : Continuous f₂) (y : ℝ) : convolution β f y = f y / β - f₁ y / β ^ 2 - Real.exp (-β * y) * (f 0 / β - f₁ 0 / β ^ 2) + convolution β f₂ y / β ^ 2

Exact second-order integration-by-parts identity, including the initial boundary terms.

theorem NavierStokes.PulseLag.lag_second_order_error {β M y : ℝ} (hβ : 0 < β) (hM : 0 ≤ M) (hy : 0 ≤ y) {f f₁ f₂ : ℝ → ℝ} (hf : ∀ (t : ℝ), HasDerivAt f (f₁ t) t) (hf₁ : ∀ (t : ℝ), HasDerivAt f₁ (f₂ t) t) (hf₂ : Continuous f₂) (hzero : f 0 = 0) (hzero₁ : f₁ 0 = 0) (hbound : ∀ t ∈ Set.Icc 0 y, |f₂ t| ≤ M) (m₀ : ℝ) : |lag β m₀ f y - (f y / β - f₁ y / β ^ 2 + m₀ * Real.exp (-β * y))| ≤ M / β ^ 3

theorem NavierStokes.PulseLag.convolution_linear (β q A y : ℝ) {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) : convolution β (fun (t : ℝ) => q * f t + A * g t) y = q * convolution β f y + A * convolution β g y

theorem NavierStokes.PulseLag.lag_eq_linearLag (β m₀ : ℝ) (f : ℝ → ℝ) (y : ℝ) : lag β m₀ f y = OutgoingTail.linearLag (fun (x : ℝ) => β) f m₀ y

theorem NavierStokes.PulseLag.lag_hasDerivAt (β m₀ : ℝ) {f : ℝ → ℝ} (hf : Continuous f) (y : ℝ) : HasDerivAt (lag β m₀ f) (f y - β * lag β m₀ f y) y

noncomputable def NavierStokes.PulseLag.decay (c : OutgoingSchedule.Parameters) : ℝ

Decay, given by 1 / 2 - c.lam.

Equations

• NavierStokes.PulseLag.decay c = 1 / 2 - c.lam

theorem NavierStokes.PulseLag.decay_pos (c : OutgoingSchedule.Parameters) : 0 < decay c

theorem NavierStokes.PulseLag.decay_inv_cube_le (c : OutgoingSchedule.Parameters) {M : ℝ} (hM : 0 ≤ M) : M / decay c ^ 3 ≤ 16 * M

theorem NavierStokes.PulseLag.exponential_correction_quadratic {lam : ℝ} (hlam : 0 < lam) : Real.exp (-(1 / (4 * lam))) ≤ 64 * lam ^ 2

The exponential correction is smaller than a fixed quadratic rate, uniformly for every positive lambda.

noncomputable def NavierStokes.PulseLag.mainSecondBound : ℝ

Main second bound, choosing the witness provided by LocalizedMomentRepair.smooth_compact_derivative_bound.

Equations

• NavierStokes.PulseLag.mainSecondBound = 1 + Classical.choose NavierStokes.PulseLag.mainSecondBound._proof_1

theorem NavierStokes.PulseLag.mainSecondBound_pos : 0 < mainSecondBound

theorem NavierStokes.PulseLag.main_second_le (z : ℝ) : |iteratedDeriv 2 OutgoingSchedule.mainPulse z| ≤ mainSecondBound

noncomputable def NavierStokes.PulseLag.forcing (c : OutgoingSchedule.Parameters) (q A y : ℝ) : ℝ

Forcing, given by A * mainPulse (c.lam * y) + affineProfile c q A y.

Equations

• NavierStokes.PulseLag.forcing c q A y = A * NavierStokes.OutgoingSchedule.mainPulse (c.lam * y) + NavierStokes.OutgoingPulseBounds.affineProfile c q A y

theorem NavierStokes.PulseLag.forcing_contDiff (c : OutgoingSchedule.Parameters) (q A : ℝ) : ContDiff ℝ (↑⊤) (forcing c q A)

theorem NavierStokes.PulseLag.forcing_eq_pulseRatio (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : forcing c (OutgoingPulseBounds.parameterPolynomial eta) (amp eta) y = OutgoingSchedule.pulseRatio c amp (y, eta)

theorem NavierStokes.PulseLag.affineProfile_zero_left (c : OutgoingSchedule.Parameters) (q A : ℝ) {y : ℝ} (hy : y ≤ 0) : OutgoingPulseBounds.affineProfile c q A y = 0

theorem NavierStokes.PulseLag.forcing_zero_left (c : OutgoingSchedule.Parameters) (q A : ℝ) {y : ℝ} (hy : y ≤ 0) : forcing c q A y = 0

theorem NavierStokes.PulseLag.deriv_zero_of_zero_left {f : ℝ → ℝ} (hf : ∀ y ≤ 0, f y = 0) : deriv f 0 = 0

theorem NavierStokes.PulseLag.forcing_jet_formula (c : OutgoingSchedule.Parameters) (q A : ℝ) (k : ℕ) (y : ℝ) : iteratedDeriv k (forcing c q A) y = A * c.lam ^ k * iteratedDeriv k OutgoingSchedule.mainPulse (c.lam * y) + iteratedDeriv k (OutgoingPulseBounds.affineProfile c q A) y

noncomputable def NavierStokes.PulseLag.forcingBound (P m : ℝ) : ℝ

Forcing bound, given by mainSecondBound + 64 * correctionJetBound P m 2.

Equations

• NavierStokes.PulseLag.forcingBound P m = NavierStokes.PulseLag.mainSecondBound + 64 * NavierStokes.OutgoingPulseBounds.correctionJetBound P m 2

theorem NavierStokes.PulseLag.forcingBound_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < forcingBound P m

theorem NavierStokes.PulseLag.forcing_second_bound (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (q A y : ℝ) : |iteratedDeriv 2 (forcing c q A) y| ≤ forcingBound c.P c.m * (|q| + |A|) * c.lam ^ 2

noncomputable def NavierStokes.PulseLag.affineLag (c : OutgoingSchedule.Parameters) (q A y : ℝ) : ℝ

Affine lag, given by lag (decay c) (prefixCoefficient c 0 * q) (forcing c q A) y.

Equations

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

noncomputable def NavierStokes.PulseLag.lagBound (P m : ℝ) : ℝ

Lag bound, given by 16 * forcingBound P m.

Equations

• NavierStokes.PulseLag.lagBound P m = 16 * NavierStokes.PulseLag.forcingBound P m

theorem NavierStokes.PulseLag.lagBound_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < lagBound P m

theorem NavierStokes.PulseLag.affineLag_error (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (q A : ℝ) {y : ℝ} (hy : 0 ≤ y) : |affineLag c q A y - (forcing c q A y / decay c - deriv (forcing c q A) y / decay c ^ 2 + OutgoingSchedule.prefixCoefficient c 0 * q * Real.exp (-decay c * y))| ≤ lagBound c.P c.m * (|q| + |A|) * c.lam ^ 2

noncomputable def NavierStokes.PulseLag.normalizedLag (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : ℝ

The actual radial mass average divided by the actual angular profile, at pulse-relative log time y.

Equations

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

theorem NavierStokes.PulseLag.pulse_denominator (c : OutgoingSchedule.Parameters) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) : Real.exp (c.pulseStart + y) * OutgoingSchedule.angular c.P c.dropLength c.lam (c.pulseStart + y, eta) = OutgoingSchedule.momentScale c 0 * OutgoingSchedule.shape eta * Real.exp (decay c * y)

theorem NavierStokes.PulseLag.massMoment_pulse (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) : OutgoingSchedule.massMoment c amp eta (c.pulseStart + y) = OutgoingSchedule.massMoment c amp eta c.pulseStart + OutgoingSchedule.momentScale c 0 * OutgoingSchedule.shape eta * ∫ (t : ℝ) in 0..y, Real.exp (decay c * t) * forcing c (OutgoingPulseBounds.parameterPolynomial eta) (amp eta) t

theorem NavierStokes.PulseLag.normalizedLag_eq_affineLag (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) : normalizedLag c amp eta y = affineLag c (OutgoingPulseBounds.parameterPolynomial eta) (amp eta) y

The exact exponential-convolution representation of the actual lag; it is derived from the radial mass integral.

theorem NavierStokes.PulseLag.normalizedLag_hasDerivWithinAt (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) : HasDerivWithinAt (normalizedLag c amp eta) (OutgoingSchedule.pulseRatio c amp (y, eta) - decay c * normalizedLag c amp eta y) (Set.Ici 0) y

The actual mass lag satisfies the pulse ODE, including its right derivative at pulse time zero.

theorem NavierStokes.PulseLag.normalizedLag_ode (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : 0 < y) : deriv (normalizedLag c amp eta) y + decay c * normalizedLag c amp eta y = OutgoingSchedule.pulseRatio c amp (y, eta)

theorem NavierStokes.PulseLag.normalizedLag_error (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (amp : ℝ → ℝ) {eta : ℝ} (heta : |eta| ≤ 1) {y : ℝ} (hy : 0 ≤ y) : |normalizedLag c amp eta y - (OutgoingSchedule.pulseRatio c amp (y, eta) / decay c - deriv (fun (t : ℝ) => OutgoingSchedule.pulseRatio c amp (t, eta)) y / decay c ^ 2 + OutgoingSchedule.prefixCoefficient c 0 * OutgoingPulseBounds.parameterPolynomial eta * Real.exp (-decay c * y))| ≤ lagBound c.P c.m * (2 + |amp eta|) * c.lam ^ 2

theorem NavierStokes.PulseLag.forcing_jet_decomposition (c : OutgoingSchedule.Parameters) (q A : ℝ) (k : ℕ) (y : ℝ) : iteratedDeriv k (forcing c q A) y = q * iteratedDeriv k (forcing c 1 0) y + A * iteratedDeriv k (forcing c 0 1) y

theorem NavierStokes.PulseLag.affineLag_decomposition (c : OutgoingSchedule.Parameters) (q A y : ℝ) : affineLag c q A y = q * affineLag c 1 0 y + A * affineLag c 0 1 y

theorem NavierStokes.PulseLag.affineLag_eta_hasDerivAt (c : OutgoingSchedule.Parameters) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) (y : ℝ) : HasDerivAt (fun (t : ℝ) => affineLag c (OutgoingPulseBounds.parameterPolynomial t) (amp t) y) (affineLag c (1 + 3 * eta ^ 2) amp' y) eta

theorem NavierStokes.PulseLag.normalizedLag_eta_hasDerivAt (c : OutgoingSchedule.Parameters) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) {y : ℝ} (hy : 0 ≤ y) : HasDerivAt (fun (t : ℝ) => normalizedLag c amp t y) (affineLag c (1 + 3 * eta ^ 2) amp' y) eta

noncomputable def NavierStokes.PulseLag.affineError (c : OutgoingSchedule.Parameters) (q A y : ℝ) : ℝ

Affine error, constructed using affineLag.

Equations

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

theorem NavierStokes.PulseLag.affineError_decomposition (c : OutgoingSchedule.Parameters) (q A y : ℝ) : affineError c q A y = q * affineError c 1 0 y + A * affineError c 0 1 y

theorem NavierStokes.PulseLag.affineError_eta_hasDerivAt (c : OutgoingSchedule.Parameters) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) (y : ℝ) : HasDerivAt (fun (t : ℝ) => affineError c (OutgoingPulseBounds.parameterPolynomial t) (amp t) y) (affineError c (1 + 3 * eta ^ 2) amp' y) eta

noncomputable def NavierStokes.PulseLag.pulseError (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : ℝ

Error in the two-term expansion of the actual normalized mass lag, with its exact exponentially decaying initial value retained.

Equations

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

theorem NavierStokes.PulseLag.pulseError_eq_affineError (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) : pulseError c amp eta y = affineError c (OutgoingPulseBounds.parameterPolynomial eta) (amp eta) y

theorem NavierStokes.PulseLag.pulseError_eta_hasDerivAt (c : OutgoingSchedule.Parameters) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) {y : ℝ} (hy : 0 ≤ y) : HasDerivAt (fun (t : ℝ) => pulseError c amp t y) (affineError c (1 + 3 * eta ^ 2) amp' y) eta

theorem NavierStokes.PulseLag.pulseError_eta_bound (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) (heta : |eta| ≤ 1) {y : ℝ} (hy : 0 ≤ y) : |deriv (fun (t : ℝ) => pulseError c amp t y) eta| ≤ lagBound c.P c.m * (4 + |amp'|) * c.lam ^ 2

noncomputable def NavierStokes.PulseLag.scaledPulse (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta z : ℝ) : ℝ

Scaled pulse, given by pulseRatio c amp (z / c.lam, eta).

Equations

• NavierStokes.PulseLag.scaledPulse c amp eta z = NavierStokes.OutgoingSchedule.pulseRatio c amp (z / c.lam, eta)

theorem NavierStokes.PulseLag.scaledPulse_deriv (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : c.lam * deriv (scaledPulse c amp eta) (c.lam * y) = deriv (fun (t : ℝ) => OutgoingSchedule.pulseRatio c amp (t, eta)) y

theorem NavierStokes.PulseLag.pulseError_scaled (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : pulseError c amp eta y = normalizedLag c amp eta y - (OutgoingSchedule.pulseRatio c amp (y, eta) / decay c - c.lam * deriv (scaledPulse c amp eta) (c.lam * y) / decay c ^ 2 + OutgoingSchedule.prefixCoefficient c 0 * OutgoingPulseBounds.parameterPolynomial eta * Real.exp (-decay c * y))

noncomputable def NavierStokes.PulseLag.fullError (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : ℝ

Full error, constructed using normalizedLag.

Equations

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

theorem NavierStokes.PulseLag.fullError_eq (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : fullError c amp eta y = pulseError c amp eta y + OutgoingSchedule.prefixCoefficient c 0 * OutgoingPulseBounds.parameterPolynomial eta * Real.exp (-decay c * y)

theorem NavierStokes.PulseLag.fullError_eta_hasDerivAt (c : OutgoingSchedule.Parameters) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) {y : ℝ} (hy : 0 ≤ y) : HasDerivAt (fun (t : ℝ) => fullError c amp t y) (affineError c (1 + 3 * eta ^ 2) amp' y + OutgoingSchedule.prefixCoefficient c 0 * (1 + 3 * eta ^ 2) * Real.exp (-decay c * y)) eta

theorem NavierStokes.PulseLag.initial_memory_bound (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) (hsmall : c.lam ≤ 1 / 120) (q : ℝ) {y : ℝ} (hy : 0 ≤ y) : |OutgoingSchedule.prefixCoefficient c 0 * q * Real.exp (-decay c * y)| ≤ OutgoingPulseBounds.prefixBound c.P c.m 0 * |q| * c.lam ^ 2

noncomputable def NavierStokes.PulseLag.fullLagBound (P m : ℝ) : ℝ

Full lag bound, given by 5 * lagBound P m + 4 * prefixBound P m 0.

Equations

• NavierStokes.PulseLag.fullLagBound P m = 5 * NavierStokes.PulseLag.lagBound P m + 4 * NavierStokes.OutgoingPulseBounds.prefixBound P m 0

theorem NavierStokes.PulseLag.fullLagBound_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < fullLagBound P m

theorem NavierStokes.PulseLag.fullError_bounds_of_amplitude_bounds (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) (hsmall : c.lam ≤ 1 / 120) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |amp'| ≤ 1) {y : ℝ} (hy : 0 ≤ y) : |fullError c amp eta y| ≤ fullLagBound c.P c.m * c.lam ^ 2 ∧ |deriv (fun (t : ℝ) => fullError c amp t y) eta| ≤ fullLagBound c.P c.m * c.lam ^ 2

A common explicit constant bounds the actual lag error and its first parameter derivative on the full nonnegative pulse-time half-line.

theorem NavierStokes.PulseLag.amplitude_fullError_bounds (d : OutgoingTail.TailData) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 120) (hscale : PulseAmplitude.errorScale d.core ≤ 1 / 1000) {eta y : ℝ} (heta : eta ^ 2 ≤ 1) (hy : 0 ≤ y) : |fullError d.core (PulseAmplitude.amplitude d) eta y| ≤ fullLagBound d.core.P d.core.m * d.core.lam ^ 2 ∧ |deriv (fun (t : ℝ) => fullError d.core (PulseAmplitude.amplitude d) t y) eta| ≤ fullLagBound d.core.P d.core.m * d.core.lam ^ 2

The concrete energy-closing amplitude satisfies the lag estimate.

theorem NavierStokes.PulseLag.exists_uniform_lag_threshold (P m : ℝ) (hP : 0 < P) : ∃ (lam₀ : ℝ) (C : ℝ), 0 < lam₀ ∧ 0 < C ∧ ∀ (d : OutgoingTail.TailData), d.core.P = P → d.core.m = m → d.core.wait = 60 * Real.log (1 / d.core.lam) → d.core.lam < lam₀ → ∀ (eta y : ℝ), eta ^ 2 ≤ 1 → 0 ≤ y → |fullError d.core (PulseAmplitude.amplitude d) eta y| ≤ C * d.core.lam ^ 2 ∧ |deriv (fun (t : ℝ) => fullError d.core (PulseAmplitude.amplitude d) t y) eta| ≤ C * d.core.lam ^ 2

One positive threshold and one constant, selected before lambda, control the lag and its first parameter derivative throughout the pulse.

theorem NavierStokes.PulseLag.smooth_amplitude_fullError_bounds (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) (hsmall : c.lam ≤ 1 / 120) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) (hamp : ∀ (eta : ℝ), eta ^ 2 ≤ 1 → |amp eta| ≤ 6 / 5) (hamp' : ∀ (eta : ℝ), eta ^ 2 ≤ 1 → |deriv amp eta| ≤ 1) (eta y : ℝ) : eta ^ 2 ≤ 1 → 0 ≤ y → |fullError c amp eta y| ≤ fullLagBound c.P c.m * c.lam ^ 2 ∧ |deriv (fun (t : ℝ) => fullError c amp t y) eta| ≤ fullLagBound c.P c.m * c.lam ^ 2

theorem NavierStokes.PulseLag.corrected_amplitude_fullError_bounds {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hK : 0 < K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 120) (hscale : CorrectedPulseAmplitude.combinedScale d K ≤ 1 / 1000) (eta y : ℝ) : eta ^ 2 ≤ 1 → 0 ≤ y → |fullError d.core (CorrectedPulseAmplitude.amplitude d w.coefficients) eta y| ≤ fullLagBound d.core.P d.core.m * d.core.lam ^ 2 ∧ |deriv (fun (t : ℝ) => fullError d.core (CorrectedPulseAmplitude.amplitude d w.coefficients) t y) eta| ≤ fullLagBound d.core.P d.core.m * d.core.lam ^ 2

The same lag estimate for the amplitude which closes the energy after the actual angular-moment reset.

theorem NavierStokes.PulseLag.exists_corrected_uniform_lag_threshold (P m : ℝ) (hP : 0 < P) : ∃ (lam₀ : ℝ) (K : ℝ) (C : ℝ), 0 < lam₀ ∧ 0 < K ∧ 0 < C ∧ ∀ (d : OutgoingTail.TailData), d.core.P = P → d.core.m = m → d.core.wait = 60 * Real.log (1 / d.core.lam) → d.core.lam < lam₀ → ∃ (w : UniformAngularReset.ResetWitness d K), ContDiff ℝ (↑⊤) (CorrectedPulseAmplitude.amplitude d w.coefficients) ∧ ∀ (eta : ℝ), eta ^ 2 ≤ 1 → 9 / 10 < CorrectedPulseAmplitude.amplitude d w.coefficients eta ∧ CorrectedPulseAmplitude.amplitude d w.coefficients eta < 6 / 5 ∧ CorrectedPulseAmplitude.totalEnergy d w.coefficients (CorrectedPulseAmplitude.amplitude d w.coefficients eta) eta = 0 ∧ ∀ (y : ℝ), 0 ≤ y → |fullError d.core (CorrectedPulseAmplitude.amplitude d w.coefficients) eta y| ≤ C * d.core.lam ^ 2 ∧ |deriv (fun (t : ℝ) => fullError d.core (CorrectedPulseAmplitude.amplitude d w.coefficients) t y) eta| ≤ C * d.core.lam ^ 2

The corrected amplitude and reset witness are actually constructed by exists_corrected_amplitude; an additional fixed threshold makes their first derivative at most one. The common lag constant is independent of lambda, the terminal parameter, eta, and pulse time.

Actual outgoing energy histories during the pulse

The history and its parameter derivative retain the actual incoming prefix. Bounds come from their source integrals and the explicit pulse energy weight.

noncomputable def NavierStokes.PulseEnergyHistory.pulseNormalization (c : OutgoingSchedule.Parameters) (eta : ℝ) : ℝ

Pulse normalization, given by PulseAmplitude.normalization c * shape eta ^ 2.

Equations

• NavierStokes.PulseEnergyHistory.pulseNormalization c eta = NavierStokes.PulseAmplitude.normalization c * NavierStokes.OutgoingSchedule.shape eta ^ 2

theorem NavierStokes.PulseEnergyHistory.pulseNormalization_pos (c : OutgoingSchedule.Parameters) (eta : ℝ) : 0 < pulseNormalization c eta

theorem NavierStokes.PulseEnergyHistory.pulse_time_le_endpoint (c : OutgoingSchedule.Parameters) {y : ℝ} (hy : y ≤ c.pulseLength) : c.pulseStart + y ≤ c.endpoint

theorem NavierStokes.PulseEnergyHistory.pulse_weight {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : OutgoingHistories.X (d.core.pulseStart + y, eta) * OutgoingHistories.E w (d.core.pulseStart + y, eta) ^ 2 = pulseNormalization d.core eta * PulseAmplitude.pulseWeight d.core y

The actual reset leaves the pulse angular field unchanged.

theorem NavierStokes.PulseEnergyHistory.pulse_U_eq {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : OutgoingHistories.U d amp (d.core.pulseStart + y, eta) = OutgoingHistories.E w (d.core.pulseStart + y, eta) * OutgoingSchedule.pulseRatio d.core amp (y, eta)

theorem NavierStokes.PulseEnergyHistory.energyWeight_pulse {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : OutgoingHistories.energyWeight w amp (d.core.pulseStart + y, eta) = pulseNormalization d.core eta * PulseAmplitude.pulseWeight d.core y * (OutgoingSchedule.pulseRatio d.core amp (y, eta) ^ 2 - 1 / 2)

Exact source of the actual energy history throughout the pulse.

theorem NavierStokes.PulseEnergyHistory.dEta_energyWeight_pulse {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : OutgoingHistories.dEta (OutgoingHistories.energyWeight w amp) (d.core.pulseStart + y, eta) = pulseNormalization d.core eta * PulseAmplitude.pulseWeight d.core y * (2 * OutgoingSchedule.pulseRatio d.core amp (y, eta) * deriv (fun (t : ℝ) => OutgoingSchedule.pulseRatio d.core amp (y, t)) eta - 2 * OutgoingHistories.shapeRate eta * (OutgoingSchedule.pulseRatio d.core amp (y, eta) ^ 2 - 1 / 2))

Exact parameter derivative of the pulse energy source.

theorem NavierStokes.PulseEnergyHistory.S_at_pulseStart {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) (eta : ℝ) : OutgoingHistories.S w amp (d.core.pulseStart, eta) = PulseAmplitude.prefixEnergy d.core eta

The pulse starts with the actual incoming energy, including the ideal past.

theorem NavierStokes.PulseEnergyHistory.prefixEnergy_hasDerivAt (c : OutgoingSchedule.Parameters) (eta : ℝ) : HasDerivAt (PulseAmplitude.prefixEnergy c) (2 * PulseAmplitude.prefixAxialEnergy c * eta + 2 * PulseAmplitude.prefixAngularEnergy c * OutgoingSchedule.shape eta ^ 2 * OutgoingHistories.shapeRate eta) eta

theorem NavierStokes.PulseEnergyHistory.dEta_S_at_pulseStart {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) (eta : ℝ) : OutgoingHistories.dEta (OutgoingHistories.S w amp) (d.core.pulseStart, eta) = 2 * PulseAmplitude.prefixAxialEnergy d.core * eta + 2 * PulseAmplitude.prefixAngularEnergy d.core * OutgoingSchedule.shape eta ^ 2 * OutgoingHistories.shapeRate eta

theorem NavierStokes.PulseEnergyHistory.logarithmicRate_le_one (c : OutgoingSchedule.Parameters) : PulseAmplitude.logarithmicRate c.lam ≤ 1

theorem NavierStokes.PulseEnergyHistory.prefix_sum_bound (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) : PulseAmplitude.prefixAxialEnergy c + PulseAmplitude.prefixAngularEnergy c ≤ PulseAmplitude.normalization c * PulseAmplitude.prefixBoundConstant c.P c.m / c.lam

theorem NavierStokes.PulseEnergyHistory.shape_bounds {eta : ℝ} (heta : |eta| ≤ 1) : 1 / 4 ≤ OutgoingSchedule.shape eta ^ 2 ∧ OutgoingSchedule.shape eta ^ 2 ≤ 1 ∧ |OutgoingHistories.shapeRate eta| ≤ 2

theorem NavierStokes.PulseEnergyHistory.source_factor_bounds {R Reta rate B : ℝ} (hB : 0 ≤ B) (hR : |R| ≤ B) (hReta : |Reta| ≤ B) (hrate : |rate| ≤ 2) : |R ^ 2 - 1 / 2| ≤ 6 * B ^ 2 + 2 ∧ |2 * R * Reta - 2 * rate * (R ^ 2 - 1 / 2)| ≤ 6 * B ^ 2 + 2

One bound covers both normalized source factors.

theorem NavierStokes.PulseEnergyHistory.energy_sources_bound {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) {eta y B : ℝ} (heta : |eta| ≤ 1) (hB : 0 ≤ B) (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) (hR : |OutgoingSchedule.pulseRatio d.core amp (y, eta)| ≤ B) (hReta : |deriv (fun (t : ℝ) => OutgoingSchedule.pulseRatio d.core amp (y, t)) eta| ≤ B) : |OutgoingHistories.energyWeight w amp (d.core.pulseStart + y, eta)| ≤ pulseNormalization d.core eta * (6 * B ^ 2 + 2) ∧ |OutgoingHistories.dEta (OutgoingHistories.energyWeight w amp) (d.core.pulseStart + y, eta)| ≤ pulseNormalization d.core eta * (6 * B ^ 2 + 2)

The actual energy source and its actual parameter derivative have a common bound.

theorem NavierStokes.PulseEnergyHistory.initial_history_bounds {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) {eta : ℝ} (heta : |eta| ≤ 1) : |OutgoingHistories.S w amp (d.core.pulseStart, eta)| ≤ pulseNormalization d.core eta * (16 * PulseAmplitude.prefixBoundConstant d.core.P d.core.m) / d.core.lam ∧ |OutgoingHistories.dEta (OutgoingHistories.S w amp) (d.core.pulseStart, eta)| ≤ pulseNormalization d.core eta * (16 * PulseAmplitude.prefixBoundConstant d.core.P d.core.m) / d.core.lam

Prefix bounds include the incoming ideal history and its parameter derivative.

theorem NavierStokes.PulseEnergyHistory.normalized_history_bound {H g : ℝ → ℝ} {lam N C M y : ℝ} (hlam : 0 < lam) (hN : 0 < N) (hC : 0 ≤ C) (hM : 0 ≤ M) (hy : 0 ≤ y) (hy' : y ≤ 13 / lam) (hg : Continuous g) (hd : ∀ t ∈ Set.Icc 0 y, HasDerivAt H (g t) t) (hsource : ∀ t ∈ Set.Icc 0 y, |g t| ≤ N * M) (hinit : |H 0| ≤ N * C / lam) : |H y| / (N * Real.exp (-2 * lam * y)) ≤ (C + 13 * M) * Real.exp 26 / lam

Integrating an actual history source over a pulse of length 13 / lam. The final denominator is its exponentially decaying pulse energy weight.

theorem NavierStokes.PulseEnergyHistory.pulse_history_bounds_of_ratio_bounds {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) {eta B y : ℝ} (heta : |eta| ≤ 1) (hB : 0 ≤ B) (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) (hR : ∀ t ∈ Set.Icc 0 d.core.pulseLength, |OutgoingSchedule.pulseRatio d.core amp (t, eta)| ≤ B) (hReta : ∀ t ∈ Set.Icc 0 d.core.pulseLength, |deriv (fun (e : ℝ) => OutgoingSchedule.pulseRatio d.core amp (t, e)) eta| ≤ B) : |OutgoingHistories.S w amp (d.core.pulseStart + y, eta)| / (OutgoingHistories.X (d.core.pulseStart + y, eta) * OutgoingHistories.E w (d.core.pulseStart + y, eta) ^ 2) ≤ (16 * PulseAmplitude.prefixBoundConstant d.core.P d.core.m + 13 * (6 * B ^ 2 + 2)) * Real.exp 26 / d.core.lam ∧ |OutgoingHistories.dEta (OutgoingHistories.S w amp) (d.core.pulseStart + y, eta)| / (OutgoingHistories.X (d.core.pulseStart + y, eta) * OutgoingHistories.E w (d.core.pulseStart + y, eta) ^ 2) ≤ (16 * PulseAmplitude.prefixBoundConstant d.core.P d.core.m + 13 * (6 * B ^ 2 + 2)) * Real.exp 26 / d.core.lam

Genuine normalized energy-history bounds from explicit pulse-ratio data. No energy-history estimate appears among the hypotheses.

noncomputable def NavierStokes.PulseEnergyHistory.forceConstant (P m : ℝ) : ℝ

A common bound for the main pulse and its actual affine moment repair.

Equations

• NavierStokes.PulseEnergyHistory.forceConstant P m = NavierStokes.OutgoingPulseBounds.mainBound + NavierStokes.OutgoingPulseBounds.correctionJetBound P m 0

theorem NavierStokes.PulseEnergyHistory.forceConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < forceConstant P m

theorem NavierStokes.PulseEnergyHistory.forcing_abs_bound (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (q A y : ℝ) : |PulseLag.forcing c q A y| ≤ forceConstant c.P c.m * (|q| + |A|)

theorem NavierStokes.PulseEnergyHistory.pulseRatio_eta_hasDerivAt (c : OutgoingSchedule.Parameters) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) (y : ℝ) : HasDerivAt (fun (t : ℝ) => OutgoingSchedule.pulseRatio c amp (y, t)) (PulseLag.forcing c (1 + 3 * eta ^ 2) amp' y) eta

The parameter derivative includes the derivative of the actual moment repair.

theorem NavierStokes.PulseEnergyHistory.pulse_ratio_bounds (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |amp'| ≤ 1) (y : ℝ) : |OutgoingSchedule.pulseRatio c amp (y, eta)| ≤ 6 * forceConstant c.P c.m ∧ |deriv (fun (t : ℝ) => OutgoingSchedule.pulseRatio c amp (y, t)) eta| ≤ 6 * forceConstant c.P c.m

noncomputable def NavierStokes.PulseEnergyHistory.historyConstant (P m : ℝ) : ℝ

This constant depends only on the fixed parameters P,m.

Equations

• NavierStokes.PulseEnergyHistory.historyConstant P m = 16 * NavierStokes.PulseAmplitude.prefixBoundConstant P m + 13 * (6 * (6 * NavierStokes.PulseEnergyHistory.forceConstant P m) ^ 2 + 2)

theorem NavierStokes.PulseEnergyHistory.historyConstant_pos (P m : ℝ) : 0 < historyConstant P m

theorem NavierStokes.PulseEnergyHistory.pulse_history_bounds {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 120) {eta y : ℝ} (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |deriv amp eta| ≤ 1) (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : |OutgoingHistories.S w amp (d.core.pulseStart + y, eta)| / (OutgoingHistories.X (d.core.pulseStart + y, eta) * OutgoingHistories.E w (d.core.pulseStart + y, eta) ^ 2) ≤ historyConstant d.core.P d.core.m * Real.exp 26 / d.core.lam ∧ |OutgoingHistories.dEta (OutgoingHistories.S w amp) (d.core.pulseStart + y, eta)| / (OutgoingHistories.X (d.core.pulseStart + y, eta) * OutgoingHistories.E w (d.core.pulseStart + y, eta) ^ 2) ≤ historyConstant d.core.P d.core.m * Real.exp 26 / d.core.lam

Both requested actual history bounds, with the actual repaired pulse source.

theorem NavierStokes.PulseEnergyHistory.corrected_pulse_history_bounds {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hK : 0 < K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 120) (hscale : CorrectedPulseAmplitude.combinedScale d K ≤ 1 / 1000) {eta y : ℝ} (heta : |eta| ≤ 1) (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : |OutgoingHistories.S w (CorrectedPulseAmplitude.amplitude d w.coefficients) (d.core.pulseStart + y, eta)| / (OutgoingHistories.X (d.core.pulseStart + y, eta) * OutgoingHistories.E w (d.core.pulseStart + y, eta) ^ 2) ≤ historyConstant d.core.P d.core.m * Real.exp 26 / d.core.lam ∧ |OutgoingHistories.dEta (OutgoingHistories.S w (CorrectedPulseAmplitude.amplitude d w.coefficients)) (d.core.pulseStart + y, eta)| / (OutgoingHistories.X (d.core.pulseStart + y, eta) * OutgoingHistories.E w (d.core.pulseStart + y, eta) ^ 2) ≤ historyConstant d.core.P d.core.m * Real.exp 26 / d.core.lam

Specialization to the corrected amplitude supplied by the proved energy solve.

noncomputable def NavierStokes.PulseCone.forceConstant (P m : ℝ) : ℝ

Force constant, given by mainBound + correctionJetBound P m 0.

Equations

• NavierStokes.PulseCone.forceConstant P m = NavierStokes.OutgoingPulseBounds.mainBound + NavierStokes.OutgoingPulseBounds.correctionJetBound P m 0

theorem NavierStokes.PulseCone.forceConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < forceConstant P m

theorem NavierStokes.PulseCone.forcing_abs_le (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (q A y : ℝ) : |PulseLag.forcing c q A y| ≤ forceConstant c.P c.m * (|q| + |A|)

theorem NavierStokes.PulseCone.initial_coefficient_le (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) (hsmall : c.lam ≤ 1 / 120) : |OutgoingSchedule.prefixCoefficient c 0| ≤ OutgoingPulseBounds.prefixBound c.P c.m 0

theorem NavierStokes.PulseCone.decay_div_le_three (c : OutgoingSchedule.Parameters) {M : ℝ} (hM : 0 ≤ M) : M / PulseLag.decay c ≤ 3 * M

theorem NavierStokes.PulseCone.affineLag_abs_le (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) (hsmall : c.lam ≤ 1 / 120) (q A : ℝ) {y : ℝ} (hy : 0 ≤ y) : |PulseLag.affineLag c q A y| ≤ OutgoingPulseBounds.prefixBound c.P c.m 0 * |q| + 3 * forceConstant c.P c.m * (|q| + |A|)

noncomputable def NavierStokes.PulseCone.averageConstant (P m : ℝ) : ℝ

Average constant, given by 4 * prefixBound P m 0 + 18 * forceConstant P m.

Equations

• NavierStokes.PulseCone.averageConstant P m = 4 * NavierStokes.OutgoingPulseBounds.prefixBound P m 0 + 18 * NavierStokes.PulseCone.forceConstant P m

theorem NavierStokes.PulseCone.averageConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < averageConstant P m

theorem NavierStokes.PulseCone.pulse_data_bounds (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) (hsmall : c.lam ≤ 1 / 120) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |amp'| ≤ 1) {y : ℝ} (hy : 0 ≤ y) : |OutgoingSchedule.pulseRatio c amp (y, eta)| ≤ 6 * forceConstant c.P c.m ∧ |PulseLag.normalizedLag c amp eta y| ≤ averageConstant c.P c.m ∧ |deriv (fun (t : ℝ) => PulseLag.normalizedLag c amp t y) eta| ≤ averageConstant c.P c.m

Uniform bounds for the actual pulse ratio, normalized mass history, and its first parameter derivative.

noncomputable def NavierStokes.PulseCone.energyConstant (P m : ℝ) : ℝ

Energy constant, given by P * Real.exp (Real.exp m + 12).

Equations

• NavierStokes.PulseCone.energyConstant P m = P * Real.exp (Real.exp m + 12)

theorem NavierStokes.PulseCone.energyConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < energyConstant P m

theorem NavierStokes.PulseCone.shape_le_one (eta : ℝ) : OutgoingSchedule.shape eta ≤ 1

theorem NavierStokes.PulseCone.pulse_angular_small (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) : OutgoingSchedule.angular c.P c.dropLength c.lam (c.pulseStart + y, eta) ≤ energyConstant c.P c.m * c.lam ^ 30

noncomputable def NavierStokes.PulseCone.shapeGradient (eta : ℝ) : ℝ

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

Equations

• NavierStokes.PulseCone.shapeGradient eta = 2 * eta / (1 + eta ^ 2)

theorem NavierStokes.PulseCone.shapeGradient_bound {eta : ℝ} (heta : |eta| ≤ 1) : |shapeGradient eta| ≤ 2

theorem NavierStokes.PulseCone.source_remainder_bound {E lam a b c m mp R M F : ℝ} (hE : 0 ≤ E) (hlam : 0 ≤ lam) (hlam' : lam ≤ 1) (ha : |a| ≤ 3) (hb : |b| ≤ 1) (hc : |c| ≤ 3) (hm : |m| ≤ M) (hmp : |mp| ≤ M) (hR : |R| ≤ F) : |E * (-lam * (a * m + b * mp) + c * R)| ≤ E * (4 * M + 3 * F)

theorem NavierStokes.PulseCone.geometric_coefficient_bounds {h eta : ℝ} (hh : 0 ≤ h) (hh' : h ≤ 1 / 2) (heta : |eta| ≤ 1) : |2 * (1 / 2 - h) * eta - (1 - eta ^ 2) * shapeGradient eta| ≤ 3 ∧ |1 - eta ^ 2| ≤ 1 ∧ |2 * h * eta + (1 - eta ^ 2) * shapeGradient eta| ≤ 3

noncomputable def NavierStokes.PulseCone.pulseAngularSource (c : OutgoingSchedule.Parameters) (h : ℝ) (amp : ℝ → ℝ) (eta y : ℝ) : ℝ

Pulse angular source as an element of ℝ.

Equations

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

theorem NavierStokes.PulseCone.pulseAngularSource_error_identity (c : OutgoingSchedule.Parameters) (h : ℝ) (amp : ℝ → ℝ) (eta y : ℝ) : pulseAngularSource c h amp eta y - (c.lam - h + (1 / 2 - h) * eta * shapeGradient eta) = OutgoingSchedule.angular c.P c.dropLength c.lam (c.pulseStart + y, eta) * (-c.lam * ((2 * (1 / 2 - h) * eta - (1 - eta ^ 2) * shapeGradient eta) * PulseLag.normalizedLag c amp eta y + (1 - eta ^ 2) * deriv (fun (t : ℝ) => PulseLag.normalizedLag c amp t y) eta) + (2 * h * eta + (1 - eta ^ 2) * shapeGradient eta) * OutgoingSchedule.pulseRatio c amp (y, eta))

noncomputable def NavierStokes.PulseCone.sourceConstant (P m : ℝ) : ℝ

Source constant, given by energyConstant P m * (4 * averageConstant P m + 18 * forceConstant P m).

Equations

• NavierStokes.PulseCone.sourceConstant P m = NavierStokes.PulseCone.energyConstant P m * (4 * NavierStokes.PulseCone.averageConstant P m + 18 * NavierStokes.PulseCone.forceConstant P m)

theorem NavierStokes.PulseCone.sourceConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < sourceConstant P m

theorem NavierStokes.PulseCone.pulseAngularSource_error_bound (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) (hsmall : c.lam ≤ 1 / 120) {h : ℝ} (hh : 0 ≤ h) (hh' : h ≤ 1 / 2) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |amp'| ≤ 1) {y : ℝ} (hy : 0 ≤ y) : |pulseAngularSource c h amp eta y - (c.lam - h + (1 / 2 - h) * eta * shapeGradient eta)| ≤ sourceConstant c.P c.m * c.lam ^ 30

theorem NavierStokes.PulseCone.pulseAngularSource_lower (d : OutgoingTail.TailData) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 120) (herr : sourceConstant d.core.P d.core.m * d.core.lam ^ 29 ≤ 1 / 8) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |amp'| ≤ 1) {y : ℝ} (hy : 0 ≤ y) : 3 * d.core.lam / 8 ≤ pulseAngularSource d.core d.h amp eta y

theorem NavierStokes.PulseCone.ode_lower_barrier {r s L : ℝ} (hr : 0 < r) (hL : 0 ≤ L) {Q S : ℝ → ℝ} (hQ : ∀ t ∈ Set.Icc 0 L, HasDerivAt Q (S t - r * Q t) t) (hS : ∀ t ∈ Set.Icc 0 L, s ≤ S t) : s / r + (Q 0 - s / r) * Real.exp (-r * L) ≤ Q L

A lower barrier for the exact scalar lag equation on a finite interval. Only the differential equation and a lower source bound are used.

theorem NavierStokes.PulseCone.pulse_memory_small (c : OutgoingSchedule.Parameters) : Real.exp (-(1 - c.lam) * c.pulseLength) ≤ 1 / 3

theorem NavierStokes.PulseCone.pulse_endpoint_lower (c : OutgoingSchedule.Parameters) {Q S : ℝ → ℝ} (hQ₀ : 0 ≤ Q 0) (hQ : ∀ t ∈ Set.Icc 0 c.pulseLength, HasDerivAt Q (S t - (1 - c.lam) * Q t) t) (hS : ∀ t ∈ Set.Icc 0 c.pulseLength, 3 * c.lam / 8 ≤ S t) : c.lam / 4 ≤ Q c.pulseLength

The long actual pulse turns a nonnegative incoming angular lag and the lower source 3*lambda/8 into the endpoint bound needed by the tail.

Binding the pulse formulas to the actual corrected histories

theorem NavierStokes.PulseCone.E_radial_before {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : y ≤ d.core.endpoint) : OutgoingHistories.dY (OutgoingHistories.E w) (y, eta) = OutgoingSchedule.angular d.core.P d.core.dropLength d.core.lam (y, eta) * (OutgoingSchedule.slope d.core.dropLength d.core.lam y - 1 / 2)

One-sided equality before the endpoint determines the true radial derivative there as well, since both profiles are smooth.

theorem NavierStokes.PulseCone.E_parameter_before {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : y ≤ d.core.endpoint) : OutgoingHistories.dEta (OutgoingHistories.E w) (y, eta) = OutgoingHistories.E w (y, eta) * -shapeGradient eta

theorem NavierStokes.PulseCone.E_parameter_ratio_before {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : y ≤ d.core.endpoint) : OutgoingHistories.dEta (OutgoingHistories.E w) (y, eta) / OutgoingHistories.E w (y, eta) = -shapeGradient eta

theorem NavierStokes.PulseCone.H_radial_ratio_before {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : y ≤ d.core.endpoint) : OutgoingHistories.dY (OutgoingHistories.H w) (y, eta) / OutgoingHistories.H w (y, eta) = OutgoingSchedule.slope d.core.dropLength d.core.lam y

theorem NavierStokes.PulseCone.H_radial_ratio_pulse {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : OutgoingHistories.dY (OutgoingHistories.H w) (d.core.pulseStart + y, eta) / OutgoingHistories.H w (d.core.pulseStart + y, eta) = -d.core.lam

theorem NavierStokes.PulseCone.U_pulse {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : OutgoingHistories.U d amp (d.core.pulseStart + y, eta) = OutgoingHistories.E w (d.core.pulseStart + y, eta) * OutgoingSchedule.pulseRatio d.core amp (y, eta)

theorem NavierStokes.PulseCone.Ubar_pulse {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (amp : ℝ → ℝ) (eta : ℝ) {y : ℝ} (hy' : y ≤ d.core.pulseLength) : OutgoingHistories.Ubar d amp (d.core.pulseStart + y, eta) = OutgoingHistories.E w (d.core.pulseStart + y, eta) * PulseLag.normalizedLag d.core amp eta y

theorem NavierStokes.PulseCone.Ubar_parameter_pulse {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : OutgoingHistories.dEta (OutgoingHistories.Ubar d amp) (d.core.pulseStart + y, eta) = OutgoingHistories.E w (d.core.pulseStart + y, eta) * (deriv (fun (t : ℝ) => PulseLag.normalizedLag d.core amp t y) eta - shapeGradient eta * PulseLag.normalizedLag d.core amp eta y)

theorem NavierStokes.PulseCone.Sq_pulse {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : OutgoingHistories.Sq w amp (d.core.pulseStart + y, eta) = pulseAngularSource d.core d.h amp eta y

The source estimate is for the actual stress history: no source formula or lag approximation is an input.

theorem NavierStokes.PulseCone.Qs_pulse_hasDerivAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : HasDerivAt (fun (t : ℝ) => OutgoingHistories.Qs w amp (d.core.pulseStart + t, eta)) (pulseAngularSource d.core d.h amp eta y - (1 - d.core.lam) * OutgoingHistories.Qs w amp (d.core.pulseStart + y, eta)) y

theorem NavierStokes.PulseCone.Qs_endpoint_lower_of_nonnegative_entry {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 120) (herr : sourceConstant d.core.P d.core.m * d.core.lam ^ 29 ≤ 1 / 8) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) {eta : ℝ} (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |deriv amp eta| ≤ 1) (hentry : 0 ≤ OutgoingHistories.Qs w amp (d.core.pulseStart, eta)) : d.core.lam / 4 ≤ OutgoingHistories.Qs w amp (d.core.endpoint, eta)

The actual angular lag at the endpoint, initially conditional only on its incoming sign and explicit schedule/amplitude bounds.

noncomputable def NavierStokes.PulseCone.sourceThreshold (P m : ℝ) : ℝ

A positive threshold selected from the two fixed prefix parameters.

Equations

• NavierStokes.PulseCone.sourceThreshold P m = min (1 / 120) (1 / (8 * NavierStokes.PulseCone.sourceConstant P m))

theorem NavierStokes.PulseCone.sourceThreshold_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < sourceThreshold P m

theorem NavierStokes.PulseCone.source_error_small (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ sourceThreshold c.P c.m) : sourceConstant c.P c.m * c.lam ^ 29 ≤ 1 / 8

theorem NavierStokes.PulseCone.ode_equilibrium_error {r s δ L : ℝ} (hr : 0 < r) (hδ : 0 ≤ δ) (hL : 0 ≤ L) {Q S : ℝ → ℝ} (hQ : ∀ t ∈ Set.Icc 0 L, HasDerivAt Q (S t - r * Q t) t) (hS : ∀ t ∈ Set.Icc 0 L, |S t - s| ≤ δ) : |Q L - s / r| ≤ |Q 0 - s / r| * Real.exp (-r * L) + δ / r

Exact stability estimate for a scalar lag around a constant source. The source error is allowed to have either sign.

theorem NavierStokes.PulseCone.Qs_pulse_equilibrium_error {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 120) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) {eta y : ℝ} (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |deriv amp eta| ≤ 1) (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : |OutgoingHistories.Qs w amp (d.core.pulseStart + y, eta) - (d.core.lam - d.h + (1 / 2 - d.h) * eta * shapeGradient eta) / (1 - d.core.lam)| ≤ |OutgoingHistories.Qs w amp (d.core.pulseStart, eta) - (d.core.lam - d.h + (1 / 2 - d.h) * eta * shapeGradient eta) / (1 - d.core.lam)| * Real.exp (-(1 - d.core.lam) * y) + sourceConstant d.core.P d.core.m * d.core.lam ^ 30 / (1 - d.core.lam)

Uniform angular-lag error throughout the actual pulse; the incoming error is retained explicitly for the shaped-wait theorem to supply.

theorem NavierStokes.PulseCone.Qs_endpoint_lower {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 120) (hpulse : sourceConstant d.core.P d.core.m * d.core.lam ^ 29 ≤ 1 / 8) (hh₁ : d.h ≤ 1 / 100) (hhT : d.h ≤ Real.exp (-(d.core.holdStart + 3 / 5)) / 8) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) {eta : ℝ} (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |deriv amp eta| ≤ 1) : d.core.lam / 4 ≤ OutgoingHistories.Qs w amp (d.core.endpoint, eta)

The actual endpoint lower bound follows from the constructed incoming history and numerical parameter restrictions, with no incoming-lag or source estimate assumed.

theorem NavierStokes.PulseCone.Qs_endpoint_lower_of_threshold {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ sourceThreshold d.core.P d.core.m) (hh₁ : d.h ≤ 1 / 100) (hhT : d.h ≤ Real.exp (-(d.core.holdStart + 3 / 5)) / 8) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) {eta : ℝ} (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |deriv amp eta| ≤ 1) : d.core.lam / 4 ≤ OutgoingHistories.Qs w amp (d.core.endpoint, eta)

theorem NavierStokes.PulseCone.corrected_Qs_endpoint_lower {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hK : 0 < K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 120) (hscale : CorrectedPulseAmplitude.combinedScale d K ≤ 1 / 1000) (hpulse : sourceConstant d.core.P d.core.m * d.core.lam ^ 29 ≤ 1 / 8) (hh₁ : d.h ≤ 1 / 100) (hhT : d.h ≤ Real.exp (-(d.core.holdStart + 3 / 5)) / 8) {eta : ℝ} (heta : |eta| ≤ 1) : d.core.lam / 4 ≤ OutgoingHistories.Qs w (CorrectedPulseAmplitude.amplitude d w.coefficients) (d.core.endpoint, eta)

The final energy-closing amplitude, including the angular reset, is the amplitude used in this endpoint theorem.

The axial identity and the genuine pressure remainder

theorem NavierStokes.PulseCone.Ns_integrated_Ubar {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) (p : OutgoingHistories.Point) : OutgoingHistories.Ns w amp p = -OutgoingHistories.W d amp p * OutgoingHistories.U d amp p + StressAlgebra.axialExponent d.h * (OutgoingHistories.Ubar d amp p - p.2 * OutgoingHistories.dEta (OutgoingHistories.Ubar d amp) p) + (4 * d.h * p.2 * OutgoingHistories.S w amp p - StressAlgebra.coordinateFactor p.2 * OutgoingHistories.dEta (OutgoingHistories.S w amp) p) / OutgoingHistories.X p + 4 * StressAlgebra.velocityExponent d.h * p.2 * OutgoingHistories.Pi w p - StressAlgebra.coordinateFactor p.2 * OutgoingHistories.dEta (OutgoingHistories.Pi w) p

noncomputable def NavierStokes.PulseCone.axialHistoryError {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (amp : ℝ → ℝ) (eta y : ℝ) : ℝ

Axial history error as an element of ℝ.

Equations

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

theorem NavierStokes.PulseCone.Ns_pulse_identity {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : OutgoingHistories.Ns w amp (d.core.pulseStart + y, eta) / OutgoingHistories.E w (d.core.pulseStart + y, eta) = -OutgoingSchedule.pulseRatio d.core amp (y, eta) + (1 / 2 - d.h + (1 / 2 - d.h) * eta * shapeGradient eta) * PulseLag.normalizedLag d.core amp eta y - (1 / 2 - d.h) * eta * deriv (fun (t : ℝ) => PulseLag.normalizedLag d.core amp t y) eta + axialHistoryError w amp eta y

Exact substitution in the integrated axial stress. The error is an explicit expression in the same constructed energy and pressure histories.

theorem NavierStokes.PulseCone.Pi_before {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.endpoint) : OutgoingHistories.Pi w (y, eta) = FuturePressureBounds.Pi d y eta

theorem NavierStokes.PulseCone.Pi_parameter_before {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.endpoint) : OutgoingHistories.dEta (OutgoingHistories.Pi w) (y, eta) = deriv (FuturePressureBounds.Pi d y) eta

theorem NavierStokes.PulseCone.pulse_pressure_bounds {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {eta y : ℝ} (heta : |eta| ≤ 1) (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : |OutgoingHistories.Pi w (d.core.pulseStart + y, eta)| ≤ FuturePressureBounds.envelopeConstant / 2 * OutgoingHistories.E w (d.core.pulseStart + y, eta) ^ 2 ∧ |OutgoingHistories.dEta (OutgoingHistories.Pi w) (d.core.pulseStart + y, eta)| ≤ 2 * FuturePressureBounds.envelopeConstant * |eta| * OutgoingHistories.E w (d.core.pulseStart + y, eta) ^ 2

Uniform value and first parameter derivative bounds for the actual canonical pressure throughout the pulse.

Actual viscous coefficients on the pulse

noncomputable def NavierStokes.PulseCone.radialA {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (p : OutgoingHistories.Point) : ℝ

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

Equations

• NavierStokes.PulseCone.radialA w p = 2 - 2 * (NavierStokes.OutgoingHistories.dY (NavierStokes.OutgoingHistories.H w) p / NavierStokes.OutgoingHistories.H w p)

noncomputable def NavierStokes.PulseCone.shearB {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (amp : ℝ → ℝ) (p : OutgoingHistories.Point) : ℝ

Shear B, given by 2 * dY (U d amp) p / E w p.

Equations

• NavierStokes.PulseCone.shearB w amp p = 2 * NavierStokes.OutgoingHistories.dY (NavierStokes.OutgoingHistories.U d amp) p / NavierStokes.OutgoingHistories.E w p

noncomputable def NavierStokes.PulseCone.directionRatio {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (amp : ℝ → ℝ) (p : OutgoingHistories.Point) : ℝ

Direction ratio, given by Ns w amp p / (E w p * Qs w amp p).

Equations

• NavierStokes.PulseCone.directionRatio w amp p = NavierStokes.OutgoingHistories.Ns w amp p / (NavierStokes.OutgoingHistories.E w p * NavierStokes.OutgoingHistories.Qs w amp p)

theorem NavierStokes.PulseCone.radialA_pulse {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : radialA w (d.core.pulseStart + y, eta) = 2 + 2 * d.core.lam

theorem NavierStokes.PulseCone.E_radial_pulse {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : OutgoingHistories.dY (OutgoingHistories.E w) (d.core.pulseStart + y, eta) = OutgoingHistories.E w (d.core.pulseStart + y, eta) * -(1 / 2 + d.core.lam)

theorem NavierStokes.PulseCone.U_radial_pulse {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : OutgoingHistories.dY (OutgoingHistories.U d amp) (d.core.pulseStart + y, eta) = OutgoingHistories.E w (d.core.pulseStart + y, eta) * (deriv (fun (t : ℝ) => OutgoingSchedule.pulseRatio d.core amp (t, eta)) y - (1 / 2 + d.core.lam) * OutgoingSchedule.pulseRatio d.core amp (y, eta))

theorem NavierStokes.PulseCone.shearB_pulse {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : shearB w amp (d.core.pulseStart + y, eta) = -OutgoingSchedule.pulseRatio d.core amp (y, eta) + 2 * d.core.lam * (deriv (PulseLag.scaledPulse d.core amp eta) (d.core.lam * y) - OutgoingSchedule.pulseRatio d.core amp (y, eta))

Quantitative pulse jets and parameter sensitivity

theorem NavierStokes.PulseCone.mainPulse_deriv_formula (z : ℝ) : deriv OutgoingSchedule.mainPulse z = OutgoingSchedule.sigma (50 * z) * (1 - OutgoingSchedule.sigma (z - 10)) - OutgoingSchedule.pulseRamp z * deriv OutgoingSchedule.sigma (z - 10)

theorem NavierStokes.PulseCone.mainPulse_deriv_le_one {z : ℝ} (hz : 0 ≤ z) : deriv OutgoingSchedule.mainPulse z ≤ 1

Only this upper derivative bound is used for the favorable cutoff sign.

noncomputable def NavierStokes.PulseCone.mainFirstBound : ℝ

Main first bound, choosing the witness provided by LocalizedMomentRepair.smooth_compact_derivative_bound.

Equations

• NavierStokes.PulseCone.mainFirstBound = 1 + Classical.choose NavierStokes.PulseCone.mainFirstBound._proof_1

theorem NavierStokes.PulseCone.mainFirstBound_pos : 0 < mainFirstBound

theorem NavierStokes.PulseCone.main_first_le (z : ℝ) : |deriv OutgoingSchedule.mainPulse z| ≤ mainFirstBound

theorem NavierStokes.PulseCone.scaledPulse_deriv_formula (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : deriv (PulseLag.scaledPulse c amp eta) (c.lam * y) = amp eta * deriv OutgoingSchedule.mainPulse (c.lam * y) + deriv (OutgoingPulseBounds.affineProfile c (OutgoingPulseBounds.parameterPolynomial eta) (amp eta)) y / c.lam

noncomputable def NavierStokes.PulseCone.valueRepairConstant (P m : ℝ) : ℝ

Value repair constant, given by 384 * correctionJetBound P m 0.

Equations

• NavierStokes.PulseCone.valueRepairConstant P m = 384 * NavierStokes.OutgoingPulseBounds.correctionJetBound P m 0

noncomputable def NavierStokes.PulseCone.derivativeRepairConstant (P m : ℝ) : ℝ

Derivative repair constant, given by 384 * correctionJetBound P m 1.

Equations

• NavierStokes.PulseCone.derivativeRepairConstant P m = 384 * NavierStokes.OutgoingPulseBounds.correctionJetBound P m 1

theorem NavierStokes.PulseCone.valueRepairConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < valueRepairConstant P m

theorem NavierStokes.PulseCone.derivativeRepairConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < derivativeRepairConstant P m

theorem NavierStokes.PulseCone.scaledPulse_correction_bounds (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (amp : ℝ → ℝ) {eta : ℝ} (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (y : ℝ) : |OutgoingSchedule.pulseRatio c amp (y, eta) - amp eta * OutgoingSchedule.mainPulse (c.lam * y)| ≤ valueRepairConstant c.P c.m * c.lam ^ 2 ∧ |deriv (PulseLag.scaledPulse c amp eta) (c.lam * y) - amp eta * deriv OutgoingSchedule.mainPulse (c.lam * y)| ≤ derivativeRepairConstant c.P c.m * c.lam

noncomputable def NavierStokes.PulseCone.derivativeConstant (P m : ℝ) : ℝ

Derivative constant, given by 2 * mainFirstBound + derivativeRepairConstant P m.

Equations

• NavierStokes.PulseCone.derivativeConstant P m = 2 * NavierStokes.PulseCone.mainFirstBound + NavierStokes.PulseCone.derivativeRepairConstant P m

theorem NavierStokes.PulseCone.derivativeConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < derivativeConstant P m

theorem NavierStokes.PulseCone.scaledPulse_deriv_abs_le (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (amp : ℝ → ℝ) {eta : ℝ} (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (y : ℝ) : |deriv (PulseLag.scaledPulse c amp eta) (c.lam * y)| ≤ derivativeConstant c.P c.m

theorem NavierStokes.PulseCone.forcing_fine_abs_le (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (q A y : ℝ) : |PulseLag.forcing c q A y| ≤ OutgoingPulseBounds.mainBound * |A| + 64 * OutgoingPulseBounds.correctionJetBound c.P c.m 0 * (|q| + |A|) * c.lam ^ 2

theorem NavierStokes.PulseCone.affineLag_fine_abs_le (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) (hsmall : c.lam ≤ 1 / 120) (q A : ℝ) {y : ℝ} (hy : 0 ≤ y) : |PulseLag.affineLag c q A y| ≤ 3 * OutgoingPulseBounds.mainBound * |A| + (OutgoingPulseBounds.prefixBound c.P c.m 0 * |q| + 192 * OutgoingPulseBounds.correctionJetBound c.P c.m 0 * (|q| + |A|)) * c.lam ^ 2

noncomputable def NavierStokes.PulseCone.parameterLagConstant (P m : ℝ) : ℝ

Parameter lag constant, given by 4 * prefixBound P m 0 + 960 * correctionJetBound P m 0.

Equations

• NavierStokes.PulseCone.parameterLagConstant P m = 4 * NavierStokes.OutgoingPulseBounds.prefixBound P m 0 + 960 * NavierStokes.OutgoingPulseBounds.correctionJetBound P m 0

theorem NavierStokes.PulseCone.parameterLagConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < parameterLagConstant P m

theorem NavierStokes.PulseCone.normalizedLag_parameter_fine_bound (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) (hsmall : c.lam ≤ 1 / 120) {amp : ℝ → ℝ} {eta amp' : ℝ} (ha : HasDerivAt amp amp' eta) (heta : |eta| ≤ 1) (hamp' : |amp'| ≤ 1) {y : ℝ} (hy : 0 ≤ y) : |deriv (fun (t : ℝ) => PulseLag.normalizedLag c amp t y) eta| ≤ 3 * OutgoingPulseBounds.mainBound * |amp'| + parameterLagConstant c.P c.m * c.lam ^ 2

The parameter derivative has the small amplitude-derivative factor; the remaining dependence is quadratically small in lambda.

The coefficient in the pulse-direction expansion

noncomputable def NavierStokes.PulseCone.geometricSource (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Geometric source, given by (1 / 2 - d.h) * eta * shapeGradient eta.

Equations

• NavierStokes.PulseCone.geometricSource d eta = (1 / 2 - d.h) * eta * NavierStokes.PulseCone.shapeGradient eta

noncomputable def NavierStokes.PulseCone.equilibriumNumerator (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Equilibrium numerator, given by d.core.lam - d.h + geometricSource d eta.

Equations

• NavierStokes.PulseCone.equilibriumNumerator d eta = d.core.lam - d.h + NavierStokes.PulseCone.geometricSource d eta

noncomputable def NavierStokes.PulseCone.angularEquilibrium (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Angular equilibrium, given by equilibriumNumerator d eta / (1 - d.core.lam).

Equations

• NavierStokes.PulseCone.angularEquilibrium d eta = NavierStokes.PulseCone.equilibriumNumerator d eta / (1 - d.core.lam)

noncomputable def NavierStokes.PulseCone.derivativeCoefficient (d : OutgoingTail.TailData) (eta : ℝ) : ℝ

Derivative coefficient, given by `d.core.lam * ((1 / 2 - d.h) + geometricSource d eta) * (1

• d.core.lam) / (decay d.core ^ 2 * equilibriumNumerator d eta)`.

Equations

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

theorem NavierStokes.PulseCone.eta_shapeGradient_nonneg (eta : ℝ) : 0 ≤ eta * shapeGradient eta

theorem NavierStokes.PulseCone.eta_shapeGradient_bounds {eta : ℝ} (heta : |eta| ≤ 1) : eta ^ 2 ≤ eta * shapeGradient eta ∧ eta * shapeGradient eta ≤ 1

theorem NavierStokes.PulseCone.geometricSource_nonneg (d : OutgoingTail.TailData) (eta : ℝ) : 0 ≤ geometricSource d eta

theorem NavierStokes.PulseCone.equilibriumNumerator_pos (d : OutgoingTail.TailData) (eta : ℝ) : 0 < equilibriumNumerator d eta

theorem NavierStokes.PulseCone.pulse_geometric_bounds (d : OutgoingTail.TailData) {eta : ℝ} (heta : |eta| ≤ 1) : 1 / 2 - d.h + geometricSource d eta ≤ 1 ∧ d.core.lam / 2 + 2 / 5 * eta ^ 2 ≤ equilibriumNumerator d eta

theorem NavierStokes.PulseCone.derivativeCoefficient_nonneg (d : OutgoingTail.TailData) (eta : ℝ) : 0 ≤ derivativeCoefficient d eta

theorem NavierStokes.PulseCone.derivativeCoefficient_le (d : OutgoingTail.TailData) (hsmall : d.core.lam ≤ 1 / 100000) (hh : d.h ≤ d.core.lam / 100000) (eta : ℝ) : derivativeCoefficient d eta ≤ 2001 / 1000

A concrete version of C_d <= 2+o(1), uniform in the parameter.

noncomputable def NavierStokes.PulseCone.mainDirection (d : OutgoingTail.TailData) (amp : ℝ → ℝ) (eta y : ℝ) : ℝ

Main direction as an element of ℝ.

Equations

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

theorem NavierStokes.PulseCone.mainDirection_identity (d : OutgoingTail.TailData) (eta R Z : ℝ) : -R + (1 / 2 - d.h + geometricSource d eta) * (R / PulseLag.decay d.core - d.core.lam * Z / PulseLag.decay d.core ^ 2) = angularEquilibrium d eta * ((1 - d.core.lam) / PulseLag.decay d.core * R - derivativeCoefficient d eta * Z)

theorem NavierStokes.PulseCone.Ns_pulse_expansion {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) (eta : ℝ) {y : ℝ} (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : OutgoingHistories.Ns w amp (d.core.pulseStart + y, eta) / OutgoingHistories.E w (d.core.pulseStart + y, eta) = angularEquilibrium d eta * mainDirection d amp eta y + (1 / 2 - d.h + geometricSource d eta) * PulseLag.fullError d.core amp eta y - (1 / 2 - d.h) * eta * deriv (fun (t : ℝ) => PulseLag.normalizedLag d.core amp t y) eta + axialHistoryError w amp eta y

The actual mass expansion is inserted into the actual axial history.

Strict numerical margins, stable under quantified errors

theorem NavierStokes.PulseCone.first_quadratic_margin (R : ℝ) : -2 * R ^ 2 + 241 / 100 * R ≤ 73 / 100

theorem NavierStokes.PulseCone.second_quadratic_margin (R : ℝ) : -(7 / 2) * R ^ 2 + 241 / 50 * R ≤ 167 / 100

theorem NavierStokes.PulseCone.ideal_cross_bound {R C Z : ℝ} (hR : 0 ≤ R) (hC : 0 ≤ C) (hC' : C ≤ 2001 / 1000) (hZ : Z ≤ 6 / 5) : -R * (2 * R - C * Z) ≤ -2 * R ^ 2 + 241 / 100 * R

noncomputable def NavierStokes.PulseCone.coneErrorBudget (F M eps lam : ℝ) : ℝ

Cone error budget, given by `2 * eps * (M + F + 1) + eps * (2 * F + 1) / 2 + 2 * lam * (M +

1. ^ 2`.

Equations

• NavierStokes.PulseCone.coneErrorBudget F M eps lam = 2 * eps * (M + F + 1) + eps * (2 * F + 1) / 2 + 2 * lam * (M + 1) ^ 2

theorem NavierStokes.PulseCone.perturbed_cone_margins {lam R C Z b v eps F M : ℝ} (hlam : 0 ≤ lam) (hF : 0 ≤ F) (hM : 0 ≤ M) (heps : 0 ≤ eps) (heps' : eps ≤ 1) (hR : 0 ≤ R) (hR' : R ≤ F) (hC : 0 ≤ C) (hC' : C ≤ 2001 / 1000) (hZ : Z ≤ 6 / 5) (hmain : |2 * R - C * Z| ≤ M) (hb : |b + R| ≤ eps) (hv : |v - (2 * R - C * Z)| ≤ eps) (hbudget : coneErrorBudget F M eps lam ≤ 1 / 100) : b * v ≤ 74 / 100 ∧ 2 * b * v + b ^ 2 / (2 + 2 * lam) + 2 * lam * v ^ 2 ≤ 168 / 100

A completely numerical perturbation lemma. The actual profile estimates below supply both errors and the small budget.

theorem NavierStokes.PulseCone.perturbed_true_cone {lam R C Z b v eps F M : ℝ} (hlam : 0 < lam) (hF : 0 ≤ F) (hM : 0 ≤ M) (heps : 0 ≤ eps) (heps' : eps ≤ 1) (hR : 0 ≤ R) (hR' : R ≤ F) (hC : 0 ≤ C) (hC' : C ≤ 2001 / 1000) (hZ : Z ≤ 6 / 5) (hmain : |2 * R - C * Z| ≤ M) (hb : |b + R| ≤ eps) (hv : |v - (2 * R - C * Z)| ≤ eps) (hbudget : coneErrorBudget F M eps lam ≤ 1 / 100) : 0 < 2 + 2 * lam - b * v ∧ 2 * b * v + b ^ 2 / (2 + 2 * lam) + (2 + 2 * lam - 2) * v ^ 2 < 2 ∧ 2 < (2 + 2 * lam) * (1 + (b / (2 + 2 * lam)) ^ 2)

The axial history error is derived from actual moments

theorem NavierStokes.PulseCone.W_pulse_error_bound {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 120) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) {eta y : ℝ} (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |deriv amp eta| ≤ 1) (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : |1 - OutgoingHistories.W d amp (d.core.pulseStart + y, eta)| ≤ 4 * averageConstant d.core.P d.core.m * OutgoingHistories.E w (d.core.pulseStart + y, eta)

noncomputable def NavierStokes.PulseCone.axialErrorConstant (P m : ℝ) : ℝ

Axial error constant, constructed using energyConstant.

Equations

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

theorem NavierStokes.PulseCone.axialErrorConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < axialErrorConstant P m

theorem NavierStokes.PulseCone.axialHistoryError_bound {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 120) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) {eta y : ℝ} (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |deriv amp eta| ≤ 1) (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : |axialHistoryError w amp eta y| ≤ axialErrorConstant d.core.P d.core.m * d.core.lam ^ 29

Division by the angular lag near the equator

theorem NavierStokes.PulseCone.denominator_bounds (d : OutgoingTail.TailData) {eta Q : ℝ} (heta : |eta| ≤ 1) (hQ : equilibriumNumerator d eta / 2 ≤ Q) : 0 < Q ∧ 1 / Q ≤ 4 / d.core.lam ∧ |eta| / Q ≤ 4 / √d.core.lam

noncomputable def NavierStokes.PulseCone.mainDirectionBound (P m : ℝ) : ℝ

Main direction bound, given by 18 * forceConstant P m + 3 * derivativeConstant P m.

Equations

• NavierStokes.PulseCone.mainDirectionBound P m = 18 * NavierStokes.PulseCone.forceConstant P m + 3 * NavierStokes.PulseCone.derivativeConstant P m

theorem NavierStokes.PulseCone.mainDirectionBound_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < mainDirectionBound P m

theorem NavierStokes.PulseCone.mainDirection_abs_le (d : OutgoingTail.TailData) (hsmall : d.core.lam ≤ 1 / 100000) (hh : d.h ≤ d.core.lam / 100000) {amp : ℝ → ℝ} {eta : ℝ} (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (y : ℝ) : |mainDirection d amp eta y| ≤ mainDirectionBound d.core.P d.core.m

theorem NavierStokes.PulseCone.directionRatio_error_bound {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 100000) (hh : d.h ≤ d.core.lam / 100000) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) {eta y Cq : ℝ} (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |deriv amp eta| ≤ 1) (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) (hQlow : equilibriumNumerator d eta / 2 ≤ OutgoingHistories.Qs w amp (d.core.pulseStart + y, eta)) (hQerr : |OutgoingHistories.Qs w amp (d.core.pulseStart + y, eta) - angularEquilibrium d eta| ≤ Cq * d.core.lam ^ 28) : |directionRatio w amp (d.core.pulseStart + y, eta) - mainDirection d amp eta y| ≤ 4 / d.core.lam * (Cq * d.core.lam ^ 28 * mainDirectionBound d.core.P d.core.m + PulseLag.fullLagBound d.core.P d.core.m * d.core.lam ^ 2 + axialErrorConstant d.core.P d.core.m * d.core.lam ^ 29) + 4 / √d.core.lam * (3 * OutgoingPulseBounds.mainBound * |deriv amp eta| + parameterLagConstant d.core.P d.core.m * d.core.lam ^ 2)

A quantified division step retaining every error term. Its two angular-lag hypotheses are supplied by the shaped-wait estimate.

noncomputable def NavierStokes.PulseCone.mainRatio (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : ℝ

Main ratio, given by amp eta * mainPulse (c.lam * y).

Equations

• NavierStokes.PulseCone.mainRatio c amp eta y = amp eta * NavierStokes.OutgoingSchedule.mainPulse (c.lam * y)

noncomputable def NavierStokes.PulseCone.mainSlope (c : OutgoingSchedule.Parameters) (amp : ℝ → ℝ) (eta y : ℝ) : ℝ

Main slope, given by amp eta * deriv mainPulse (c.lam * y).

Equations

• NavierStokes.PulseCone.mainSlope c amp eta y = amp eta * deriv NavierStokes.OutgoingSchedule.mainPulse (c.lam * y)

noncomputable def NavierStokes.PulseCone.idealDirection (d : OutgoingTail.TailData) (amp : ℝ → ℝ) (eta y : ℝ) : ℝ

Ideal direction, given by 2 * mainRatio d.core amp eta y - derivativeCoefficient d eta * mainSlope d.core amp eta y.

Equations

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

noncomputable def NavierStokes.PulseCone.mainRatioBound : ℝ

Main ratio bound, given by 2 * mainBound.

Equations

• NavierStokes.PulseCone.mainRatioBound = 2 * NavierStokes.OutgoingPulseBounds.mainBound

noncomputable def NavierStokes.PulseCone.idealDirectionBound : ℝ

Ideal direction bound, given by 4 * mainBound + 6 * mainFirstBound.

Equations

• NavierStokes.PulseCone.idealDirectionBound = 4 * NavierStokes.OutgoingPulseBounds.mainBound + 6 * NavierStokes.PulseCone.mainFirstBound

theorem NavierStokes.PulseCone.mainRatioBound_pos : 0 < mainRatioBound

theorem NavierStokes.PulseCone.idealDirectionBound_pos : 0 < idealDirectionBound

theorem NavierStokes.PulseCone.main_profile_bounds (d : OutgoingTail.TailData) (hsmall : d.core.lam ≤ 1 / 100000) (hh : d.h ≤ d.core.lam / 100000) {amp : ℝ → ℝ} {eta y : ℝ} (hamp₀ : 0 ≤ amp eta) (hamp : |amp eta| ≤ 6 / 5) (hy : 0 ≤ y) : 0 ≤ mainRatio d.core amp eta y ∧ mainRatio d.core amp eta y ≤ mainRatioBound ∧ mainSlope d.core amp eta y ≤ 6 / 5 ∧ |idealDirection d amp eta y| ≤ idealDirectionBound

theorem NavierStokes.PulseCone.pulseRatio_abs_le (c : OutgoingSchedule.Parameters) (hsmall : c.lam ≤ 1 / 120) (amp : ℝ → ℝ) {eta : ℝ} (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (y : ℝ) : |OutgoingSchedule.pulseRatio c amp (y, eta)| ≤ 6 * forceConstant c.P c.m

noncomputable def NavierStokes.PulseCone.shearErrorConstant (P m : ℝ) : ℝ

Shear error constant, given by valueRepairConstant P m + 2 * derivativeConstant P m + 12 * forceConstant P m.

Equations

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

noncomputable def NavierStokes.PulseCone.directionMainErrorConstant (P m : ℝ) : ℝ

Direction main error constant, given by 18 * forceConstant P m + 2 * valueRepairConstant P m + 3 * derivativeRepairConstant P m.

Equations

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

theorem NavierStokes.PulseCone.shearErrorConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < shearErrorConstant P m

theorem NavierStokes.PulseCone.directionMainErrorConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < directionMainErrorConstant P m

theorem NavierStokes.PulseCone.shearB_main_error {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hsmall : d.core.lam ≤ 1 / 120) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) {eta y : ℝ} (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : |shearB w amp (d.core.pulseStart + y, eta) + mainRatio d.core amp eta y| ≤ shearErrorConstant d.core.P d.core.m * d.core.lam

theorem NavierStokes.PulseCone.mainDirection_ideal_error (d : OutgoingTail.TailData) (hsmall : d.core.lam ≤ 1 / 100000) (hh : d.h ≤ d.core.lam / 100000) {amp : ℝ → ℝ} {eta : ℝ} (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (y : ℝ) : |mainDirection d amp eta y - idealDirection d amp eta y| ≤ directionMainErrorConstant d.core.P d.core.m * d.core.lam

The shaped wait supplies the actual angular equilibrium error

theorem NavierStokes.PulseCone.canonical_wait_for_power28 (c : OutgoingSchedule.Parameters) (hwait : c.wait = 60 * Real.log (1 / c.lam)) : ShapedWaitBounds.waitForPower c 28 ≤ c.wait

noncomputable def NavierStokes.PulseCone.angularErrorConstant (P m : ℝ) : ℝ

Angular error constant, given by 19 + 2 * sourceConstant P m.

Equations

• NavierStokes.PulseCone.angularErrorConstant P m = 19 + 2 * NavierStokes.PulseCone.sourceConstant P m

theorem NavierStokes.PulseCone.angularErrorConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < angularErrorConstant P m

theorem NavierStokes.PulseCone.actual_Qs_pulse_error {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 120) (hh : d.h ≤ 1 / 100) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) {eta y : ℝ} (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |deriv amp eta| ≤ 1) (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : |OutgoingHistories.Qs w amp (d.core.pulseStart + y, eta) - angularEquilibrium d eta| ≤ angularErrorConstant d.core.P d.core.m * d.core.lam ^ 28

The equilibrium approximation now has no initial-error hypothesis.

theorem NavierStokes.PulseCone.actual_Qs_pulse_lower {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 120) (hh : d.h ≤ 1 / 100) (hnum : angularErrorConstant d.core.P d.core.m * d.core.lam ^ 27 ≤ 1 / 4) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) {eta y : ℝ} (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |deriv amp eta| ≤ 1) (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : equilibriumNumerator d eta / 2 ≤ OutgoingHistories.Qs w amp (d.core.pulseStart + y, eta)

A single explicit vanishing rate for the cone errors

noncomputable def NavierStokes.PulseCone.coneRate (lam : ℝ) : ℝ

Cone rate, given by lam + Real.sqrt lam * (1 + Real.log (1 / lam)).

Equations

• NavierStokes.PulseCone.coneRate lam = lam + √lam * (1 + Real.log (1 / lam))

theorem NavierStokes.PulseCone.coneRate_parts {lam : ℝ} (hlam : 0 < lam) (hsmall : lam ≤ 1) : 0 ≤ coneRate lam ∧ lam ≤ coneRate lam ∧ √lam * (1 + Real.log (1 / lam)) ≤ coneRate lam

theorem NavierStokes.PulseCone.coneRate_tendsto_zero : Filter.Tendsto coneRate (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

noncomputable def NavierStokes.PulseCone.directionErrorConstant (P m A : ℝ) : ℝ

Direction error constant, constructed using 4.

Equations

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

theorem NavierStokes.PulseCone.directionErrorConstant_pos {P A : ℝ} (hP : 0 < P) (m : ℝ) (hA : 0 ≤ A) : 0 < directionErrorConstant P m A

noncomputable def NavierStokes.PulseCone.componentConstant (P m A : ℝ) : ℝ

Component constant, given by `directionErrorConstant P m A + directionMainErrorConstant P m

• shearErrorConstant P m + 1`.

Equations

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

theorem NavierStokes.PulseCone.componentConstant_pos {P A : ℝ} (hP : 0 < P) (m : ℝ) (hA : 0 ≤ A) : 0 < componentConstant P m A

theorem NavierStokes.PulseCone.actual_component_errors {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 100000) (hh : d.h ≤ d.core.lam / 100000) (hnum : angularErrorConstant d.core.P d.core.m * d.core.lam ^ 27 ≤ 1 / 4) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) {eta y A : ℝ} (hA : 0 ≤ A) (heta : |eta| ≤ 1) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |deriv amp eta| ≤ 1) (hamprate : |deriv amp eta| ≤ A * d.core.lam * (1 + Real.log (1 / d.core.lam))) (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : |shearB w amp (d.core.pulseStart + y, eta) + mainRatio d.core amp eta y| ≤ componentConstant d.core.P d.core.m A * coneRate d.core.lam ∧ |directionRatio w amp (d.core.pulseStart + y, eta) - idealDirection d amp eta y| ≤ componentConstant d.core.P d.core.m A * coneRate d.core.lam

noncomputable def NavierStokes.PulseCone.pulseBudget (P m A lam : ℝ) : ℝ

Pulse budget, given by coneErrorBudget mainRatioBound idealDirectionBound (componentConstant P m A * coneRate lam) lam.

Equations

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

structure NavierStokes.PulseCone.PulseConeAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (amp : ℝ → ℝ) (p : OutgoingHistories.Point) : Prop

The numerical margins refer only to the actual global stress histories and the actual first radial derivatives of the corrected fields.

• angular_positive : 0 < OutgoingHistories.Qs w amp p
• first_margin : shearB w amp p * directionRatio w amp p ≤ 74 / 100
• second_margin : 2 * shearB w amp p * directionRatio w amp p + shearB w amp p ^ 2 / radialA w p + (radialA w p - 2) * directionRatio w amp p ^ 2 ≤ 168 / 100
• radial_gt_two : 2 < radialA w p

theorem NavierStokes.PulseCone.PulseConeAt.true_criterion {d : OutgoingTail.TailData} {K : ℝ} {w : UniformAngularReset.ResetWitness d K} {amp : ℝ → ℝ} {p : OutgoingHistories.Point} (h : PulseConeAt w amp p) : 0 < radialA w p - shearB w amp p * directionRatio w amp p ∧ 2 * shearB w amp p * directionRatio w amp p + shearB w amp p ^ 2 / radialA w p + (radialA w p - 2) * directionRatio w amp p ^ 2 < 2 ∧ 2 < radialA w p * (1 + (shearB w amp p / radialA w p) ^ 2)

theorem NavierStokes.PulseCone.actual_pulse_cone {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 100000) (hh : d.h ≤ d.core.lam / 100000) (hnum : angularErrorConstant d.core.P d.core.m * d.core.lam ^ 27 ≤ 1 / 4) {amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) amp) {eta y A : ℝ} (hA : 0 ≤ A) (heta : |eta| ≤ 1) (hamp₀ : 0 ≤ amp eta) (hamp : |amp eta| ≤ 6 / 5) (hamp' : |deriv amp eta| ≤ 1) (hamprate : |deriv amp eta| ≤ A * d.core.lam * (1 + Real.log (1 / d.core.lam))) (hbudget : pulseBudget d.core.P d.core.m A d.core.lam ≤ 1 / 100) (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : PulseConeAt w amp (d.core.pulseStart + y, eta)

The full pulse cone for any smooth amplitude with the proved size and first-derivative rate. Every further hypothesis is a scalar parameter bound.

noncomputable def NavierStokes.PulseCone.amplitudeDerivativeConstant (P m K : ℝ) : ℝ

Amplitude derivative constant, given by 128 * CorrectedPulseAmplitude.combinedConstant P m K.

Equations

• NavierStokes.PulseCone.amplitudeDerivativeConstant P m K = 128 * NavierStokes.CorrectedPulseAmplitude.combinedConstant P m K

theorem NavierStokes.PulseCone.amplitudeDerivativeConstant_pos {P K : ℝ} (hP : 0 < P) (m : ℝ) (hK : 0 < K) : 0 < amplitudeDerivativeConstant P m K

noncomputable def NavierStokes.PulseCone.correctedPulseBudget (P m K lam : ℝ) : ℝ

Corrected pulse budget, given by pulseBudget P m (amplitudeDerivativeConstant P m K) lam.

Equations

• NavierStokes.PulseCone.correctedPulseBudget P m K lam = NavierStokes.PulseCone.pulseBudget P m (NavierStokes.PulseCone.amplitudeDerivativeConstant P m K) lam

theorem NavierStokes.PulseCone.corrected_pulse_cone {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (hK : 0 < K) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hsmall : d.core.lam ≤ 1 / 100000) (hh : d.h ≤ d.core.lam / 100000) (hscale : CorrectedPulseAmplitude.combinedScale d K ≤ 1 / 1000) (hnum : angularErrorConstant d.core.P d.core.m * d.core.lam ^ 27 ≤ 1 / 4) (hbudget : correctedPulseBudget d.core.P d.core.m K d.core.lam ≤ 1 / 100) {eta y : ℝ} (heta : |eta| ≤ 1) (hy : 0 ≤ y) (hy' : y ≤ d.core.pulseLength) : PulseConeAt w (CorrectedPulseAmplitude.amplitude d w.coefficients) (d.core.pulseStart + y, eta)

The full actual pulse cone for the same corrected amplitude and reset witness as the global schedule. No stress or cone estimate is assumed.

theorem NavierStokes.PulseCone.pulseBudget_tendsto_zero (P m A : ℝ) : Filter.Tendsto (pulseBudget P m A) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

theorem NavierStokes.PulseCone.exists_pulseBudget_threshold (P m A : ℝ) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (lam : ℝ), 0 < lam → lam < δ → pulseBudget P m A lam ≤ 1 / 100

theorem NavierStokes.PulseCone.exists_corrected_pulse_threshold (P m K : ℝ) (hP : 0 < P) (hK : 0 < K) : ∃ (lam₀ : ℝ), 0 < lam₀ ∧ ∀ (d : OutgoingTail.TailData), d.core.P = P → d.core.m = m → d.core.wait = 60 * Real.log (1 / d.core.lam) → d.core.lam < lam₀ → d.h ≤ d.core.lam / 100000 → ∀ (w : UniformAngularReset.ResetWitness d K) (eta y : ℝ), |eta| ≤ 1 → 0 ≤ y → y ≤ d.core.pulseLength → PulseConeAt w (CorrectedPulseAmplitude.amplitude d w.coefficients) (d.core.pulseStart + y, eta)

One threshold is chosen after the fixed prefix and reset constant. It works for every supplied reset witness, keeps its actual energy-closing amplitude, and is uniform over the full pulse and the physical parameter band.