One clean outgoing cone on one reset witness

The shaped-hold estimate below is obtained from the actual angular floor and axial history. The later assembly keeps the same reset and corrected amplitude through every interval. The true additional inequality starts at the shaped hold; the early outgoing region only requires the relaxed cone.

theorem NavierStokes.OutgoingCone.coneA_eq_actualA {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (y eta : ℝ) : OutgoingEntranceCone.coneA w (y, eta) = TailCone.actualA w y eta

theorem NavierStokes.OutgoingCone.coneB_eq_actualBs {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (y eta : ℝ) : OutgoingEntranceCone.coneB w Amp (y, eta) = TailCone.actualBs w Amp y eta

theorem NavierStokes.OutgoingCone.hold_Qs_pos {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {eta t : ℝ} (hh1 : d.h ≤ 1 / 100) (hhlam : d.h ≤ d.core.lam / 4) (hhT : d.h ≤ Real.exp (-(d.core.holdStart + 3 / 5)) / 8) (heta : |eta| ≤ 1) (ht : 0 ≤ t) (htw : t ≤ d.core.wait) : 0 < OutgoingHistories.Qs w Amp (d.core.holdStart + t, eta)

noncomputable def NavierStokes.OutgoingCone.holdRatioConstant (P m : ℝ) : ℝ

Hold ratio constant, given by ShapedWaitBounds.axialWaitConstant P m / (2 * ShapedWaitBounds.holdFloor m).

Equations

• NavierStokes.OutgoingCone.holdRatioConstant P m = NavierStokes.ShapedWaitBounds.axialWaitConstant P m / (2 * NavierStokes.ShapedWaitBounds.holdFloor m)

theorem NavierStokes.OutgoingCone.holdRatioConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < holdRatioConstant P m

theorem NavierStokes.OutgoingCone.hold_ratio_bound {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {eta t : ℝ} (hh1 : d.h ≤ 1 / 100) (hhlam : d.h ≤ d.core.lam / 4) (hhT : d.h ≤ Real.exp (-(d.core.holdStart + 3 / 5)) / 8) (heta : |eta| ≤ 1) (ht : 0 ≤ t) (htw : t ≤ d.core.wait) : |OutgoingEntranceCone.coneRatio w Amp (d.core.holdStart + t, eta)| ≤ holdRatioConstant d.core.P d.core.m * (1 + t) * Real.exp (d.core.lam * t / 2)

The Gaussian part of the genuine angular floor cancels the parameter factor in the genuine axial history bound.

noncomputable def NavierStokes.OutgoingCone.holdSmallConstant (P m : ℝ) : ℝ

Hold small constant, given by 60 * Real.exp 30 * holdRatioConstant P m.

Equations

• NavierStokes.OutgoingCone.holdSmallConstant P m = 60 * Real.exp 30 * NavierStokes.OutgoingCone.holdRatioConstant P m

theorem NavierStokes.OutgoingCone.holdSmallConstant_pos {P : ℝ} (hP : 0 < P) (m : ℝ) : 0 < holdSmallConstant P m

theorem NavierStokes.OutgoingCone.hold_sqrt_ratio_bound {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) {eta t : ℝ} (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hh1 : d.h ≤ 1 / 100) (hhlam : d.h ≤ d.core.lam / 4) (hhT : d.h ≤ Real.exp (-(d.core.holdStart + 3 / 5)) / 8) (heta : |eta| ≤ 1) (ht : 0 ≤ t) (htw : t ≤ d.core.wait) : √d.core.lam * |OutgoingEntranceCone.coneRatio w Amp (d.core.holdStart + t, eta)| ≤ holdSmallConstant d.core.P d.core.m * PulseCone.coneRate d.core.lam

theorem NavierStokes.OutgoingCone.exists_hold_threshold (P m : ℝ) : ∃ (lam0 : ℝ), 0 < lam0 ∧ ∀ (lam : ℝ), 0 < lam → lam < lam0 → holdSmallConstant P m * PulseCone.coneRate lam ≤ 1 / 2

theorem NavierStokes.OutgoingCone.hold_coneA {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (eta : ℝ) {y : ℝ} (hy : d.core.holdStart ≤ y) (hy' : y ≤ d.core.pulseStart) : OutgoingEntranceCone.coneA w (y, eta) = 2 + 2 * d.core.lam

theorem NavierStokes.OutgoingCone.hold_coneB {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (eta : ℝ) {y : ℝ} (hy : d.core.holdStart ≤ y) (hy' : y ≤ d.core.pulseStart) : OutgoingEntranceCone.coneB w Amp (y, eta) = 0

theorem NavierStokes.OutgoingCone.hold_source_criterion {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hh1 : d.h ≤ 1 / 100) (hhlam : d.h ≤ d.core.lam / 4) (hhT : d.h ≤ Real.exp (-(d.core.holdStart + 3 / 5)) / 8) (hsmall : holdSmallConstant d.core.P d.core.m * PulseCone.coneRate d.core.lam ≤ 1 / 2) {eta y : ℝ} (heta : |eta| ≤ 1) (hy : d.core.holdStart ≤ y) (hy' : y ≤ d.core.pulseStart) : 0 < OutgoingHistories.Qs w Amp (y, eta) ∧ 0 < OutgoingEntranceCone.coneA w (y, eta) - OutgoingEntranceCone.coneB w Amp (y, eta) * OutgoingEntranceCone.coneRatio w Amp (y, eta) ∧ 2 * OutgoingEntranceCone.coneB w Amp (y, eta) * OutgoingEntranceCone.coneRatio w Amp (y, eta) + OutgoingEntranceCone.coneB w Amp (y, eta) ^ 2 / OutgoingEntranceCone.coneA w (y, eta) + (OutgoingEntranceCone.coneA w (y, eta) - 2) * OutgoingEntranceCone.coneRatio w Amp (y, eta) ^ 2 < 2 ∧ 2 < OutgoingEntranceCone.coneA w (y, eta)

Common actual cone coordinates and source tests

noncomputable def NavierStokes.OutgoingCone.normalV {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Normal V, given by coneA w p * (1 + (coneB w Amp p / coneA w p) ^ 2).

Equations

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

noncomputable def NavierStokes.OutgoingCone.normalP {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (XR : ℝ) (p : ℝ × ℝ) : ℝ

Normal P, given by OutgoingHistories.p1 XR w Amp p * (1 - coneB w Amp p * coneRatio w Amp p / coneA w p).

Equations

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

noncomputable def NavierStokes.OutgoingCone.normalJ {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (XR : ℝ) (p : ℝ × ℝ) : ℝ

Normal J, given by OutgoingHistories.p1 XR w Amp p * (coneRatio w Amp p + coneB w Amp p / coneA w p).

Equations

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

structure NavierStokes.OutgoingCone.SourceCriterion {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : ℝ × ℝ) : Prop

Source criterion data, collecting angular_positive, radial_positive, first_positive, second_strict.

• angular_positive : 0 < OutgoingHistories.Qs w Amp p
• radial_positive : 0 < OutgoingEntranceCone.coneA w p
• first_positive : 0 < OutgoingEntranceCone.coneA w p - OutgoingEntranceCone.coneB w Amp p * OutgoingEntranceCone.coneRatio w Amp p
• second_strict : 2 * OutgoingEntranceCone.coneB w Amp p * OutgoingEntranceCone.coneRatio w Amp p + OutgoingEntranceCone.coneB w Amp p ^ 2 / OutgoingEntranceCone.coneA w p + (OutgoingEntranceCone.coneA w p - 2) * OutgoingEntranceCone.coneRatio w Amp p ^ 2 < 2

structure NavierStokes.OutgoingCone.RelaxedAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (XR : ℝ) (p : ℝ × ℝ) : Prop

Relaxed at data, collecting angular_positive, radial_positive, stress_gt_two, root_strict.

• angular_positive : 0 < OutgoingHistories.Qs w Amp p
• radial_positive : 0 < OutgoingEntranceCone.coneA w p
• stress_gt_two : 2 < normalP w Amp XR p
• root_strict : normalV w Amp p < ConeAlgebra.coneBound (normalP w Amp XR p) (normalJ w Amp XR p)

noncomputable def NavierStokes.OutgoingCone.TrueAt {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (XR : ℝ) (p : ℝ × ℝ) : Prop

True at, given by RelaxedAt w Amp XR p ∧ 2 < normalV w Amp p.

Equations

• NavierStokes.OutgoingCone.TrueAt w Amp XR p = (NavierStokes.OutgoingCone.RelaxedAt w Amp XR p ∧ 2 < NavierStokes.OutgoingCone.normalV w Amp p)

theorem NavierStokes.OutgoingCone.normalV_gt_two_of_radial {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : ℝ × ℝ) (ha : 2 < OutgoingEntranceCone.coneA w p) : 2 < normalV w Amp p

theorem NavierStokes.OutgoingCone.sourceCriterion_before_endpoint {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (hwait : d.core.wait = 60 * Real.log (1 / d.core.lam)) (hh1 : d.h ≤ 1 / 100) (hhlam : d.h ≤ d.core.lam / 4) (hhT : d.h ≤ Real.exp (-(d.core.holdStart + 3 / 5)) / 8) (hP : Real.exp (d.core.dropLength + 1) ≤ d.core.P ^ 2) (hdrop : OutgoingEntranceCone.dropSpeed d.core.m ≤ OutgoingEntranceCone.dropThreshold) (hentrance : d.core.lam * OutgoingEntranceCone.entranceRatioBound d.core.P d.core.m ^ 2 ≤ 1 / 4) (hhold : holdSmallConstant d.core.P d.core.m * PulseCone.coneRate d.core.lam ≤ 1 / 2) (hpulse : ∀ (eta t : ℝ), |eta| ≤ 1 → 0 ≤ t → t ≤ d.core.pulseLength → PulseCone.PulseConeAt w Amp (d.core.pulseStart + t, eta)) {y eta : ℝ} (hy : y ≤ d.core.endpoint) (heta : |eta| ≤ 1) : SourceCriterion w Amp (y, eta)

theorem NavierStokes.OutgoingCone.true_radial_before_endpoint {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (hpulse : ∀ (eta t : ℝ), |eta| ≤ 1 → 0 ≤ t → t ≤ d.core.pulseLength → PulseCone.PulseConeAt w Amp (d.core.pulseStart + t, eta)) {y eta : ℝ} (hy : d.core.holdStart ≤ y) (hy' : y ≤ d.core.endpoint) (heta : |eta| ≤ 1) : 2 < normalV w Amp (y, eta)

noncomputable def NavierStokes.OutgoingCone.preWindow (d : OutgoingTail.TailData) (left : ℝ) : Set (ℝ × ℝ)

Pre window, given by Icc left d.core.endpoint ×ˢ Icc (-1) 1.

Equations

• NavierStokes.OutgoingCone.preWindow d left = Set.Icc left d.core.endpoint ×ˢ Set.Icc (-1) 1

theorem NavierStokes.OutgoingCone.actual_p1_pos {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) {y eta : ℝ} (heta : |eta| ≤ 1) (hQ : 0 < OutgoingHistories.Qs w Amp (y, eta)) : 0 < OutgoingHistories.p1 1 w Amp (y, eta)

theorem NavierStokes.OutgoingCone.compact_actual_pre_cone {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (left : ℝ) (hsource : ∀ p ∈ preWindow d left, SourceCriterion w Amp p) : ∃ (XR0 : ℝ), 0 < XR0 ∧ ∀ (XR : ℝ), XR0 < XR → ∀ p ∈ preWindow d left, RelaxedAt w Amp XR p

Compactness is applied to actual smooth data after the source tests have been established. It gives one radial scale for the whole pre-tail interval.

theorem NavierStokes.OutgoingCone.relaxed_of_zero_shear {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (XR y eta : ℝ) (heta : |eta| ≤ 1) (hQ : 0 < OutgoingHistories.Qs w Amp (y, eta)) (hA : 0 < OutgoingEntranceCone.coneA w (y, eta)) (hB : OutgoingEntranceCone.coneB w Amp (y, eta) = 0) (hP : 2 < OutgoingHistories.p1 XR w Amp (y, eta)) (hroot : OutgoingEntranceCone.coneA w (y, eta) < ConeAlgebra.coneBound (OutgoingHistories.p1 XR w Amp (y, eta)) (OutgoingHistories.p2 XR w Amp (y, eta))) : RelaxedAt w Amp XR (y, eta)

noncomputable def NavierStokes.OutgoingCone.cleanEnd (d : OutgoingTail.TailData) : ℝ

Clean end, given by tailStart d + 1 / 2.

Equations

• NavierStokes.OutgoingCone.cleanEnd d = NavierStokes.OutgoingTail.tailStart d + 1 / 2

noncomputable def NavierStokes.OutgoingCone.cleanWindow (d : OutgoingTail.TailData) (left : ℝ) : Set (ℝ × ℝ)

Clean window, given by Icc left (cleanEnd d) ×ˢ Icc (-1) 1.

Equations

• NavierStokes.OutgoingCone.cleanWindow d left = Set.Icc left (NavierStokes.OutgoingCone.cleanEnd d) ×ˢ Set.Icc (-1) 1

noncomputable def NavierStokes.OutgoingCone.trueWindow (d : OutgoingTail.TailData) : Set (ℝ × ℝ)

True window, given by Icc d.core.holdStart (cleanEnd d) ×ˢ Icc (-1) 1.

Equations

• NavierStokes.OutgoingCone.trueWindow d = Set.Icc d.core.holdStart (NavierStokes.OutgoingCone.cleanEnd d) ×ˢ Set.Icc (-1) 1

structure NavierStokes.OutgoingCone.CleanOutgoingCone {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (XR left : ℝ) : Prop

Clean outgoing cone data, collecting relaxed, true_from_hold.

• relaxed (p : ℝ × ℝ) : p ∈ cleanWindow d left → RelaxedAt w (CorrectedPulseAmplitude.amplitude d w.coefficients) XR p
• true_from_hold (p : ℝ × ℝ) : p ∈ trueWindow d → TrueAt w (CorrectedPulseAmplitude.amplitude d w.coefficients) XR p

theorem NavierStokes.OutgoingCone.clean_cone_of_components {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) (hsource : PulseCone.sourceConstant d.core.P d.core.m * d.core.lam ^ 29 ≤ 1 / 8) (hh1 : d.h ≤ 1 / 100) (hhlam : d.h ≤ d.core.lam / 4) (hhT : d.h ≤ Real.exp (-(d.core.holdStart + 3 / 5)) / 8) (hreset : TailCone.resetSourceError d K ≤ d.core.lam / 4) (hfinite : TailCone.finiteConeConstant d.core.P d.core.m * d.core.lam ^ 10 ≤ 1 / 2) (hrelease : TailCone.releaseConeConstant d.core.P d.core.m * d.core.lam ^ 29 ≤ 1 / 2) (hP : Real.exp (d.core.dropLength + 1) ≤ d.core.P ^ 2) (hdrop : OutgoingEntranceCone.dropSpeed d.core.m ≤ OutgoingEntranceCone.dropThreshold) (hentrance : d.core.lam * OutgoingEntranceCone.entranceRatioBound d.core.P d.core.m ^ 2 ≤ 1 / 4) (hhold : holdSmallConstant d.core.P d.core.m * PulseCone.coneRate d.core.lam ≤ 1 / 2) (hpulse : ∀ (eta t : ℝ), |eta| ≤ 1 → 0 ≤ t → t ≤ d.core.pulseLength → PulseCone.PulseConeAt w (CorrectedPulseAmplitude.amplitude d w.coefficients) (d.core.pulseStart + t, eta)) (left : ℝ) (hleft : left ≤ 0) : ∃ (XR0 : ℝ), 0 < XR0 ∧ ∀ (XR : ℝ), XR0 < XR → CleanOutgoingCone w XR left

Join the proved intervals without choosing another reset or amplitude.

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

Height threshold, given by min (OutgoingEntranceCone.heightThreshold m lam) (lam / 100000).

Equations

• NavierStokes.OutgoingCone.heightThreshold m lam = min (NavierStokes.OutgoingEntranceCone.heightThreshold m lam) (lam / 100000)

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

theorem NavierStokes.OutgoingCone.exists_ordered_clean_cone : ∃ (M : ℝ), 0 < M ∧ ∀ (m : ℝ), M ≤ m → ∀ (P : ℝ), OutgoingEntranceCone.amplitudeThreshold m ≤ P → ∀ (K : ℝ), 0 < K → ∃ (lam0 : ℝ), 0 < lam0 ∧ ∀ (d : OutgoingTail.TailData), d.core.P = P → d.core.m = m → d.core.wait = 60 * Real.log (1 / d.core.lam) → d.core.lam < lam0 → d.h ≤ heightThreshold m d.core.lam → ∀ (w : UniformAngularReset.ResetWitness d K), ∀ left ≤ 0, ∃ (XR0 : ℝ), 0 < XR0 ∧ ∀ (XR : ℝ), XR0 < XR → CleanOutgoingCone w XR left

First choose the drop parameter, then the entrance amplitude, then lambda, then the terminal height, and only then a finite radius. The theorem accepts any one existing reset witness throughout.

The existing profile object and compact margins

noncomputable def NavierStokes.OutgoingCone.ProfileCleanCone (F : OutgoingProfile.Profile) (XR left : ℝ) : Prop

Profile clean cone, given by CleanOutgoingCone F.reset XR left.

Equations

• NavierStokes.OutgoingCone.ProfileCleanCone F XR left = NavierStokes.OutgoingCone.CleanOutgoingCone F.reset XR left

theorem NavierStokes.OutgoingCone.exists_ordered_profile_cone : ∃ (M : ℝ), 0 < M ∧ ∀ (m : ℝ), M ≤ m → ∀ (P : ℝ), OutgoingEntranceCone.amplitudeThreshold m ≤ P → ∀ (K : ℝ), 0 < K → ∃ (lam0 : ℝ), 0 < lam0 ∧ ∀ (F : OutgoingProfile.Profile), F.data.core.P = P → F.data.core.m = m → F.coefficientBound = K → F.data.core.wait = 60 * Real.log (1 / F.data.core.lam) → F.data.core.lam < lam0 → F.data.h ≤ heightThreshold m F.data.core.lam → ∀ left ≤ 0, ∃ (XR0 : ℝ), 0 < XR0 ∧ ∀ (XR : ℝ), XR0 < XR → ProfileCleanCone F XR left

The profile wrapper retains the input profile, its reset, and its amplitude. It does not select a second profile satisfying separate estimates.

theorem NavierStokes.OutgoingCone.normal_data_continuousOn {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {Amp : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) Amp) (XR : ℝ) {s : Set (ℝ × ℝ)} (heta : ∀ p ∈ s, |p.2| ≤ 1) (hQ : ∀ p ∈ s, 0 < OutgoingHistories.Qs w Amp p) (hA : ∀ p ∈ s, 0 < OutgoingEntranceCone.coneA w p) : ContinuousOn (normalP w Amp XR) s ∧ ContinuousOn (normalJ w Amp XR) s ∧ ContinuousOn (normalV w Amp) s

theorem NavierStokes.OutgoingCone.clean_relaxed_margins {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {XR left : ℝ} (h : CleanOutgoingCone w XR left) : ∃ (eps : ℝ), 0 < eps ∧ ∀ p ∈ cleanWindow d left, eps ≤ OutgoingHistories.Qs w (CorrectedPulseAmplitude.amplitude d w.coefficients) p ∧ eps ≤ OutgoingEntranceCone.coneA w p ∧ eps ≤ normalP w (CorrectedPulseAmplitude.amplitude d w.coefficients) XR p - 2 ∧ eps ≤ ConeAlgebra.coneBound (normalP w (CorrectedPulseAmplitude.amplitude d w.coefficients) XR p) (normalJ w (CorrectedPulseAmplitude.amplitude d w.coefficients) XR p) - normalV w (CorrectedPulseAmplitude.amplitude d w.coefficients) p

Uniform relaxed margins on the full chosen finite outgoing interval.

theorem NavierStokes.OutgoingCone.clean_true_margins {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {XR left : ℝ} (h : CleanOutgoingCone w XR left) : ∃ (eps : ℝ), 0 < eps ∧ ∀ p ∈ trueWindow d, eps ≤ normalV w (CorrectedPulseAmplitude.amplitude d w.coefficients) p - 2 ∧ eps ≤ normalP w (CorrectedPulseAmplitude.amplitude d w.coefficients) XR p - 2 ∧ eps ≤ ConeAlgebra.coneBound (normalP w (CorrectedPulseAmplitude.amplitude d w.coefficients) XR p) (normalJ w (CorrectedPulseAmplitude.amplitude d w.coefficients) XR p) - normalV w (CorrectedPulseAmplitude.amplitude d w.coefficients) p

theorem NavierStokes.OutgoingCone.clean_true_stable {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {XR left : ℝ} (h : CleanOutgoingCone w XR left) : ∃ (rho : ℝ), 0 < rho ∧ ∀ p ∈ trueWindow d, ∀ (P' J' v' : ℝ), |P' - normalP w (CorrectedPulseAmplitude.amplitude d w.coefficients) XR p| ≤ rho → |J' - normalJ w (CorrectedPulseAmplitude.amplitude d w.coefficients) XR p| ≤ rho → |v' - normalV w (CorrectedPulseAmplitude.amplitude d w.coefficients) p| ≤ rho → 2 < v' ∧ v' < P' ∧ (v' - 2) * J' ^ 2 < 2 * (P' - v') ^ 2

A coordinate perturbation tolerance for later edits on the true region. The competing coordinates need not be continuous; their closeness must be proved separately for the actual edit.

Margins independent of the later entrance radius

noncomputable def NavierStokes.OutgoingCone.sourceC {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Source C, given by 1 - coneB w Amp p * coneRatio w Amp p / coneA w p.

Equations

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

noncomputable def NavierStokes.OutgoingCone.sourceJ {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Source J, given by coneRatio w Amp p + coneB w Amp p / coneA w p.

Equations

• NavierStokes.OutgoingCone.sourceJ w Amp p = NavierStokes.OutgoingEntranceCone.coneRatio w Amp p + NavierStokes.OutgoingEntranceCone.coneB w Amp p / NavierStokes.OutgoingEntranceCone.coneA w p

noncomputable def NavierStokes.OutgoingCone.leadingGap {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) (Amp : ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Leading gap, given by 2 * sourceC w Amp p ^ 2 - (normalV w Amp p - 2) * sourceJ w Amp p ^ 2.

Equations

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

theorem NavierStokes.OutgoingCone.leading_gap_of_finite {s c j v : ℝ} (hs : 0 < s) (hv : 2 < v) (hvP : v < s * c) (hquad : (v - 2) * (s * j) ^ 2 < 2 * (s * c - v) ^ 2) : 0 < c ∧ 0 < 2 * c ^ 2 - (v - 2) * j ^ 2

theorem NavierStokes.OutgoingCone.clean_true_source_positive {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {XR left : ℝ} (h : CleanOutgoingCone w XR left) (hXR : 0 < XR) {p : ℝ × ℝ} (hp : p ∈ trueWindow d) : 0 < OutgoingHistories.Qs w (CorrectedPulseAmplitude.amplitude d w.coefficients) p ∧ 0 < OutgoingEntranceCone.coneA w p ∧ 2 < normalV w (CorrectedPulseAmplitude.amplitude d w.coefficients) p ∧ 0 < sourceC w (CorrectedPulseAmplitude.amplitude d w.coefficients) p ∧ 0 < leadingGap w (CorrectedPulseAmplitude.amplitude d w.coefficients) p

theorem NavierStokes.OutgoingCone.clean_true_source_margins {d : OutgoingTail.TailData} {K : ℝ} (w : UniformAngularReset.ResetWitness d K) {XR left : ℝ} (h : CleanOutgoingCone w XR left) (hXR : 0 < XR) : ∃ (eps : ℝ), 0 < eps ∧ ∀ p ∈ trueWindow d, eps ≤ OutgoingHistories.Qs w (CorrectedPulseAmplitude.amplitude d w.coefficients) p ∧ eps ≤ OutgoingEntranceCone.coneA w p ∧ eps ≤ normalV w (CorrectedPulseAmplitude.amplitude d w.coefficients) p - 2 ∧ eps ≤ sourceC w (CorrectedPulseAmplitude.amplitude d w.coefficients) p ∧ eps ≤ leadingGap w (CorrectedPulseAmplitude.amplitude d w.coefficients) p

All five quantities in this margin are independent of XR. A single realized true cone therefore supplies a margin for later radius choices.