Four disjoint reservations on the actual outgoing shaped wait

The log intervals are the four examples in the manuscript: (-25,-20), (-20,-15), (-14,-9), and (-8,-3), relative to the pulse entrance. The first is the five-row repair after radial modulation. The second is the existing heat-compensation patch. The last two remain pure powers after that heat correction. All fields below use the same outgoing profile.

inductive NavierStokes.ReservedPatches.Slot : Type

Slot data for reserved patches.

• modulation : Slot
• heat : Slot
• positive : Slot
• mean : Slot

@[instance_reducible]

instance NavierStokes.ReservedPatches.instDecidableEqSlot : DecidableEq Slot

Equations

• NavierStokes.ReservedPatches.instDecidableEqSlot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

noncomputable def NavierStokes.ReservedPatches.leftOffset : Slot → ℝ

Left offset as an element of Slot → ℝ | .modulation => -25 | .heat => -20 | .positive => -14 | .mean => -8.

Equations

• NavierStokes.ReservedPatches.leftOffset NavierStokes.ReservedPatches.Slot.modulation = -25
• NavierStokes.ReservedPatches.leftOffset NavierStokes.ReservedPatches.Slot.heat = -20
• NavierStokes.ReservedPatches.leftOffset NavierStokes.ReservedPatches.Slot.positive = -14
• NavierStokes.ReservedPatches.leftOffset NavierStokes.ReservedPatches.Slot.mean = -8

noncomputable def NavierStokes.ReservedPatches.rightOffset : Slot → ℝ

Right offset as an element of Slot → ℝ | .modulation => -20 | .heat => -15 | .positive => -9 | .mean => -3.

Equations

• NavierStokes.ReservedPatches.rightOffset NavierStokes.ReservedPatches.Slot.modulation = -20
• NavierStokes.ReservedPatches.rightOffset NavierStokes.ReservedPatches.Slot.heat = -15
• NavierStokes.ReservedPatches.rightOffset NavierStokes.ReservedPatches.Slot.positive = -9
• NavierStokes.ReservedPatches.rightOffset NavierStokes.ReservedPatches.Slot.mean = -3

theorem NavierStokes.ReservedPatches.offset_width (s : Slot) : rightOffset s = leftOffset s + 5

theorem NavierStokes.ReservedPatches.offset_bounds (s : Slot) : -25 ≤ leftOffset s ∧ leftOffset s < rightOffset s ∧ rightOffset s ≤ -3

theorem NavierStokes.ReservedPatches.offsets_separated {s t : Slot} (hst : s ≠ t) : rightOffset s ≤ leftOffset t ∨ rightOffset t ≤ leftOffset s

noncomputable def NavierStokes.ReservedPatches.leftClock (F : OutgoingProfile.Profile) (s : Slot) : ℝ

Left clock, given by F.data.core.pulseStart + leftOffset s.

Equations

• NavierStokes.ReservedPatches.leftClock F s = F.data.core.pulseStart + NavierStokes.ReservedPatches.leftOffset s

noncomputable def NavierStokes.ReservedPatches.rightClock (F : OutgoingProfile.Profile) (s : Slot) : ℝ

Right clock, given by F.data.core.pulseStart + rightOffset s.

Equations

• NavierStokes.ReservedPatches.rightClock F s = F.data.core.pulseStart + NavierStokes.ReservedPatches.rightOffset s

noncomputable def NavierStokes.ReservedPatches.left (F : OutgoingProfile.Profile) (XR : ℝ) (s : Slot) : ℝ

Left, given by OutgoingDilation.radius XR (leftClock F s).

Equations

• NavierStokes.ReservedPatches.left F XR s = NavierStokes.OutgoingDilation.radius XR (NavierStokes.ReservedPatches.leftClock F s)

noncomputable def NavierStokes.ReservedPatches.right (F : OutgoingProfile.Profile) (XR : ℝ) (s : Slot) : ℝ

Right, given by OutgoingDilation.radius XR (rightClock F s).

Equations

• NavierStokes.ReservedPatches.right F XR s = NavierStokes.OutgoingDilation.radius XR (NavierStokes.ReservedPatches.rightClock F s)

noncomputable def NavierStokes.ReservedPatches.window (F : OutgoingProfile.Profile) (XR : ℝ) (s : Slot) : Set ℝ

Window, given by Ioo (left F XR s) (right F XR s).

Equations

• NavierStokes.ReservedPatches.window F XR s = Set.Ioo (NavierStokes.ReservedPatches.left F XR s) (NavierStokes.ReservedPatches.right F XR s)

theorem NavierStokes.ReservedPatches.radius_strictMono (XR : ℝ) (hXR : 0 < XR) : StrictMono (OutgoingDilation.radius XR)

theorem NavierStokes.ReservedPatches.left_pos (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) : 0 < left F XR s

theorem NavierStokes.ReservedPatches.left_lt_right (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) : left F XR s < right F XR s

theorem NavierStokes.ReservedPatches.right_pos (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) : 0 < right F XR s

theorem NavierStokes.ReservedPatches.mem_window_pos (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) {X : ℝ} (hX : X ∈ window F XR s) : 0 < X

theorem NavierStokes.ReservedPatches.window_nonempty (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) : (window F XR s).Nonempty

theorem NavierStokes.ReservedPatches.windows_disjoint (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) {s t : Slot} (hst : s ≠ t) : Disjoint (window F XR s) (window F XR t)

theorem NavierStokes.ReservedPatches.clock_bounds (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) {X : ℝ} (hX : X ∈ window F XR s) : leftClock F s < OutgoingDilation.clock XR X ∧ OutgoingDilation.clock XR X < rightClock F s

theorem NavierStokes.ReservedPatches.clock_inside_wait (F : OutgoingProfile.Profile) (s : Slot) : F.data.core.holdStart < leftClock F s ∧ rightClock F s < F.data.core.pulseStart

theorem NavierStokes.ReservedPatches.window_inside_wait (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) {X : ℝ} (hX : X ∈ window F XR s) : F.data.core.holdStart < OutgoingDilation.clock XR X ∧ OutgoingDilation.clock XR X < F.data.core.pulseStart

theorem NavierStokes.ReservedPatches.canonical_wait_gt_54 {lam : ℝ} (hlam : 0 < lam) (hlam' : lam < 1 / 10) : 54 < 60 * Real.log (1 / lam)

An explicit small-lambda threshold for the canonical sixty-log wait.

theorem NavierStokes.ReservedPatches.canonical_margins (F : OutgoingProfile.Profile) (hw : F.data.core.wait = 60 * Real.log (1 / F.data.core.lam)) (s : Slot) : F.data.core.holdStart + 29 < leftClock F s ∧ rightClock F s ≤ F.data.core.pulseStart - 3

The earliest reserved boundary has over twenty-nine log units of entrance margin. The latest boundary has three log units before the pulse.

theorem NavierStokes.ReservedPatches.pulse_before_switch (F : OutgoingProfile.Profile) : F.data.core.pulseStart < HeatTailEdit.switchStart F.data

theorem NavierStokes.ReservedPatches.right_before_switch (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) : right F XR s < OutgoingDilation.switchRadius F XR

theorem NavierStokes.ReservedPatches.heat_left (F : OutgoingProfile.Profile) (XR : ℝ) : left F XR Slot.heat = OutgoingDilation.patchRadius F XR

theorem NavierStokes.ReservedPatches.right_eq_left_mul_exp (F : OutgoingProfile.Profile) (XR : ℝ) (s : Slot) : right F XR s = left F XR s * Real.exp 5

theorem NavierStokes.ReservedPatches.heat_right (F : OutgoingProfile.Profile) (XR : ℝ) : right F XR Slot.heat = OutgoingDilation.patchRadius F XR * OutgoingDilation.compensationPatch.right

Closed support regions with strict margins in the four windows

noncomputable def NavierStokes.ReservedPatches.innerLower : Slot → ℝ

Inner lower as an element of Slot → ℝ | .heat => TerminalCompensation.lower OutgoingDilation.compensationPatch 0 | _ => Real.exp 1.

Equations

• NavierStokes.ReservedPatches.innerLower NavierStokes.ReservedPatches.Slot.heat = NavierStokes.TerminalCompensation.lower NavierStokes.OutgoingDilation.compensationPatch 0
• NavierStokes.ReservedPatches.innerLower x✝ = Real.exp 1

noncomputable def NavierStokes.ReservedPatches.innerUpper : Slot → ℝ

Inner upper as an element of Slot → ℝ | .heat => TerminalCompensation.upper OutgoingDilation.compensationPatch 2 | _ => Real.exp 4.

Equations

• NavierStokes.ReservedPatches.innerUpper NavierStokes.ReservedPatches.Slot.heat = NavierStokes.TerminalCompensation.upper NavierStokes.OutgoingDilation.compensationPatch 2
• NavierStokes.ReservedPatches.innerUpper x✝ = Real.exp 4

theorem NavierStokes.ReservedPatches.inner_bounds (s : Slot) : 1 < innerLower s ∧ innerLower s < innerUpper s ∧ innerUpper s < Real.exp 5

noncomputable def NavierStokes.ReservedPatches.supportLeft (F : OutgoingProfile.Profile) (XR : ℝ) (s : Slot) : ℝ

Support left, given by left F XR s * innerLower s.

Equations

• NavierStokes.ReservedPatches.supportLeft F XR s = NavierStokes.ReservedPatches.left F XR s * NavierStokes.ReservedPatches.innerLower s

noncomputable def NavierStokes.ReservedPatches.supportRight (F : OutgoingProfile.Profile) (XR : ℝ) (s : Slot) : ℝ

Support right, given by left F XR s * innerUpper s.

Equations

• NavierStokes.ReservedPatches.supportRight F XR s = NavierStokes.ReservedPatches.left F XR s * NavierStokes.ReservedPatches.innerUpper s

noncomputable def NavierStokes.ReservedPatches.closedPatch (F : OutgoingProfile.Profile) (XR : ℝ) (s : Slot) : Set ℝ

Closed patch, given by Icc (supportLeft F XR s) (supportRight F XR s).

Equations

• NavierStokes.ReservedPatches.closedPatch F XR s = Set.Icc (NavierStokes.ReservedPatches.supportLeft F XR s) (NavierStokes.ReservedPatches.supportRight F XR s)

theorem NavierStokes.ReservedPatches.supportLeft_formula (F : OutgoingProfile.Profile) (XR : ℝ) {s : Slot} (hs : s ≠ Slot.heat) : supportLeft F XR s = OutgoingDilation.radius XR (leftClock F s + 1)

theorem NavierStokes.ReservedPatches.supportRight_formula (F : OutgoingProfile.Profile) (XR : ℝ) {s : Slot} (hs : s ≠ Slot.heat) : supportRight F XR s = OutgoingDilation.radius XR (rightClock F s - 1)

theorem NavierStokes.ReservedPatches.support_margins (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) : left F XR s < supportLeft F XR s ∧ supportLeft F XR s < supportRight F XR s ∧ supportRight F XR s < right F XR s

theorem NavierStokes.ReservedPatches.supportLeft_pos (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) : 0 < supportLeft F XR s

theorem NavierStokes.ReservedPatches.closedPatch_subset (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) : closedPatch F XR s ⊆ window F XR s

theorem NavierStokes.ReservedPatches.closedPatch_nonempty (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) : (closedPatch F XR s).Nonempty

theorem NavierStokes.ReservedPatches.closedPatches_disjoint (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) {s t : Slot} (hst : s ≠ t) : Disjoint (closedPatch F XR s) (closedPatch F XR t)

noncomputable def NavierStokes.ReservedPatches.momentPatch (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) : FiveProfileMoments.Patch

Moment patch, bundling left, right, left_pos, ordered.

Equations

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

Exact fields on the actual, common outgoing profile

noncomputable def NavierStokes.ReservedPatches.xAmplitude (F : OutgoingProfile.Profile) (XR eta : ℝ) : ℝ

X amplitude, constructed using OutgoingSchedule.radialAmplitude.

Equations

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

theorem NavierStokes.ReservedPatches.xAmplitude_pos (F : OutgoingProfile.Profile) (XR eta : ℝ) : 0 < xAmplitude F XR eta

theorem NavierStokes.ReservedPatches.xAmplitude_contDiff (F : OutgoingProfile.Profile) (XR : ℝ) : ContDiff ℝ (↑⊤) (xAmplitude F XR)

theorem NavierStokes.ReservedPatches.xAmplitude_shape (F : OutgoingProfile.Profile) (XR eta : ℝ) : xAmplitude F XR eta = xAmplitude F XR 0 / (1 + eta ^ 2)

theorem NavierStokes.ReservedPatches.clean_E_shaped (F : OutgoingProfile.Profile) (XR eta X : ℝ) (hXR : 0 < XR) (hX : 0 < X) (hlo : F.data.core.holdStart ≤ OutgoingDilation.clock XR X) (hhi : OutgoingDilation.clock XR X ≤ F.data.core.pulseStart) : OutgoingDilation.E F XR (X, eta) = xAmplitude F XR eta * X ^ (-(1 / 2 + F.data.core.lam))

theorem NavierStokes.ReservedPatches.clean_fields (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) (eta : ℝ) {X : ℝ} (hX : X ∈ window F XR s) : OutgoingDilation.U F XR (X, eta) = 0 ∧ OutgoingDilation.E F XR (X, eta) = xAmplitude F XR eta * X ^ (-(1 / 2 + F.data.core.lam))

theorem NavierStokes.ReservedPatches.heated_E_eq_clean (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {s : Slot} (hs : s ≠ Slot.heat) (eta : ℝ) {X : ℝ} (hX : X ∈ window F XR s) : HeatedOutgoing.E F XR c (X, eta) = OutgoingDilation.E F XR (X, eta)

theorem NavierStokes.ReservedPatches.heated_fields (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {s : Slot} (hs : s ≠ Slot.heat) (eta : ℝ) {X : ℝ} (hX : X ∈ window F XR s) : HeatedOutgoing.U F XR (X, eta) = 0 ∧ HeatedOutgoing.E F XR c (X, eta) = xAmplitude F XR eta * X ^ (-(1 / 2 + F.data.core.lam))

The heat slot is deliberately excluded: its additive correction is real.

theorem NavierStokes.ReservedPatches.heated_fields_on_closedPatch (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {s : Slot} (hs : s ≠ Slot.heat) (eta : ℝ) {X : ℝ} (hX : X ∈ closedPatch F XR s) : HeatedOutgoing.U F XR (X, eta) = 0 ∧ HeatedOutgoing.E F XR c (X, eta) = xAmplitude F XR eta * X ^ (-(1 / 2 + F.data.core.lam))

theorem NavierStokes.ReservedPatches.heat_slot_actual_formula (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) (eta : ℝ) {X : ℝ} (hX : X ∈ window F XR Slot.heat) : HeatedOutgoing.E F XR c (X, eta) = xAmplitude F XR eta * X ^ (-(1 / 2 + F.data.core.lam)) + HeatedOutgoing.patchIncrement F XR c (X, eta)

theorem NavierStokes.ReservedPatches.witness_fields {F : OutgoingProfile.Profile} {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {s : Slot} (hs : s ≠ Slot.heat) (eta : ℝ) {X : ℝ} (hX : X ∈ window F XR s) : HeatedOutgoing.U F XR (X, eta) = 0 ∧ HeatedOutgoing.E F XR w.coefficients (X, eta) = xAmplitude F XR eta * X ^ (-(1 / 2 + F.data.core.lam))

The heat correction lies in its own closed interior support region

theorem NavierStokes.ReservedPatches.terminal_lower_min (P : TerminalCompensation.Patch) (j : Fin 3) : TerminalCompensation.lower P 0 ≤ TerminalCompensation.lower P j

theorem NavierStokes.ReservedPatches.terminal_upper_max (P : TerminalCompensation.Patch) (j : Fin 3) : TerminalCompensation.upper P j ≤ TerminalCompensation.upper P 2

theorem NavierStokes.ReservedPatches.terminal_correction_inner_support (P : TerminalCompensation.Patch) (c : TerminalCompensation.Coeff) : Function.support (TerminalCompensation.correction P c) ⊆ Set.Icc (TerminalCompensation.lower P 0) (TerminalCompensation.upper P 2)

theorem NavierStokes.ReservedPatches.heat_increment_support (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) (eta : ℝ) : (Function.support fun (X : ℝ) => HeatedOutgoing.patchIncrement F XR c (X, eta)) ⊆ closedPatch F XR Slot.heat

theorem NavierStokes.ReservedPatches.heat_increment_tsupport (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) (eta : ℝ) : (tsupport fun (X : ℝ) => HeatedOutgoing.patchIncrement F XR c (X, eta)) ⊆ closedPatch F XR Slot.heat

Conversion to the similarity radius R, where X = R squared / 2

noncomputable def NavierStokes.ReservedPatches.radialLeft (F : OutgoingProfile.Profile) (XR : ℝ) (s : Slot) : ℝ

Radial left, given by Real.sqrt (2 * left F XR s).

Equations

• NavierStokes.ReservedPatches.radialLeft F XR s = √(2 * NavierStokes.ReservedPatches.left F XR s)

noncomputable def NavierStokes.ReservedPatches.radialRight (F : OutgoingProfile.Profile) (XR : ℝ) (s : Slot) : ℝ

Radial right, given by Real.sqrt (2 * right F XR s).

Equations

• NavierStokes.ReservedPatches.radialRight F XR s = √(2 * NavierStokes.ReservedPatches.right F XR s)

noncomputable def NavierStokes.ReservedPatches.radialSupportLeft (F : OutgoingProfile.Profile) (XR : ℝ) (s : Slot) : ℝ

Radial support left, given by Real.sqrt (2 * supportLeft F XR s).

Equations

• NavierStokes.ReservedPatches.radialSupportLeft F XR s = √(2 * NavierStokes.ReservedPatches.supportLeft F XR s)

noncomputable def NavierStokes.ReservedPatches.radialSupportRight (F : OutgoingProfile.Profile) (XR : ℝ) (s : Slot) : ℝ

Radial support right, given by Real.sqrt (2 * supportRight F XR s).

Equations

• NavierStokes.ReservedPatches.radialSupportRight F XR s = √(2 * NavierStokes.ReservedPatches.supportRight F XR s)

noncomputable def NavierStokes.ReservedPatches.radialWindow (F : OutgoingProfile.Profile) (XR : ℝ) (s : Slot) : Set ℝ

Radial window, given by Ioo (radialLeft F XR s) (radialRight F XR s).

Equations

• NavierStokes.ReservedPatches.radialWindow F XR s = Set.Ioo (NavierStokes.ReservedPatches.radialLeft F XR s) (NavierStokes.ReservedPatches.radialRight F XR s)

noncomputable def NavierStokes.ReservedPatches.radialClosedPatch (F : OutgoingProfile.Profile) (XR : ℝ) (s : Slot) : Set ℝ

Radial closed patch, given by Icc (radialSupportLeft F XR s) (radialSupportRight F XR s).

Equations

• NavierStokes.ReservedPatches.radialClosedPatch F XR s = Set.Icc (NavierStokes.ReservedPatches.radialSupportLeft F XR s) (NavierStokes.ReservedPatches.radialSupportRight F XR s)

theorem NavierStokes.ReservedPatches.radialLeft_pos (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) : 0 < radialLeft F XR s

theorem NavierStokes.ReservedPatches.radial_left_lt_right (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) : radialLeft F XR s < radialRight F XR s

theorem NavierStokes.ReservedPatches.radial_support_margins (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) : radialLeft F XR s < radialSupportLeft F XR s ∧ radialSupportLeft F XR s < radialSupportRight F XR s ∧ radialSupportRight F XR s < radialRight F XR s

theorem NavierStokes.ReservedPatches.radialSupportLeft_pos (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) : 0 < radialSupportLeft F XR s

theorem NavierStokes.ReservedPatches.square_half_mem_Ioo {a b R : ℝ} (ha : 0 < a) (hR : R ∈ Set.Ioo √(2 * a) √(2 * b)) : R ^ 2 / 2 ∈ Set.Ioo a b

theorem NavierStokes.ReservedPatches.square_half_mem_Icc {a b R : ℝ} (ha : 0 < a) (hR : R ∈ Set.Icc √(2 * a) √(2 * b)) : R ^ 2 / 2 ∈ Set.Icc a b

theorem NavierStokes.ReservedPatches.radial_mem_window (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) {R : ℝ} (hR : R ∈ radialWindow F XR s) : R ^ 2 / 2 ∈ window F XR s

theorem NavierStokes.ReservedPatches.radial_mem_closedPatch (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) {R : ℝ} (hR : R ∈ radialClosedPatch F XR s) : R ^ 2 / 2 ∈ closedPatch F XR s

theorem NavierStokes.ReservedPatches.radial_closedPatch_subset (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) : radialClosedPatch F XR s ⊆ radialWindow F XR s

theorem NavierStokes.ReservedPatches.radial_windows_disjoint (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) {s t : Slot} (hst : s ≠ t) : Disjoint (radialWindow F XR s) (radialWindow F XR t)

theorem NavierStokes.ReservedPatches.radial_closedPatches_disjoint (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) {s t : Slot} (hst : s ≠ t) : Disjoint (radialClosedPatch F XR s) (radialClosedPatch F XR t)

noncomputable def NavierStokes.ReservedPatches.radialAmplitude (F : OutgoingProfile.Profile) (XR eta : ℝ) : ℝ

Radial amplitude, given by xAmplitude F XR eta * (2 : ℝ) ^ (1 / 2 + F.data.core.lam).

Equations

• NavierStokes.ReservedPatches.radialAmplitude F XR eta = NavierStokes.ReservedPatches.xAmplitude F XR eta * 2 ^ (1 / 2 + F.data.core.lam)

theorem NavierStokes.ReservedPatches.radialAmplitude_pos (F : OutgoingProfile.Profile) (XR eta : ℝ) : 0 < radialAmplitude F XR eta

theorem NavierStokes.ReservedPatches.radialAmplitude_contDiff (F : OutgoingProfile.Profile) (XR : ℝ) : ContDiff ℝ (↑⊤) (radialAmplitude F XR)

theorem NavierStokes.ReservedPatches.radialAmplitude_shape (F : OutgoingProfile.Profile) (XR eta : ℝ) : radialAmplitude F XR eta = radialAmplitude F XR 0 / (1 + eta ^ 2)

theorem NavierStokes.ReservedPatches.square_half_power (lam R : ℝ) (hR : 0 < R) : (R ^ 2 / 2) ^ (-(1 / 2 + lam)) = 2 ^ (1 / 2 + lam) * R ^ (-1 - 2 * lam)

theorem NavierStokes.ReservedPatches.radial_heated_fields (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {s : Slot} (hs : s ≠ Slot.heat) (eta : ℝ) {R : ℝ} (hR : R ∈ radialWindow F XR s) : HeatedOutgoing.U F XR (R ^ 2 / 2, eta) = 0 ∧ HeatedOutgoing.E F XR c (R ^ 2 / 2, eta) = FiveRowRank.background F.data.core.lam (radialAmplitude F XR eta) R

This is the precise R-power interface used by positive-order and mean repairs.

theorem NavierStokes.ReservedPatches.radial_witness_fields {F : OutgoingProfile.Profile} {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {s : Slot} (hs : s ≠ Slot.heat) (eta : ℝ) {R : ℝ} (hR : R ∈ radialWindow F XR s) : HeatedOutgoing.U F XR (R ^ 2 / 2, eta) = 0 ∧ HeatedOutgoing.E F XR w.coefficients (R ^ 2 / 2, eta) = FiveRowRank.background F.data.core.lam (radialAmplitude F XR eta) R

theorem NavierStokes.ReservedPatches.radial_heated_fields_on_closedPatch (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {s : Slot} (hs : s ≠ Slot.heat) (eta : ℝ) {R : ℝ} (hR : R ∈ radialClosedPatch F XR s) : HeatedOutgoing.U F XR (R ^ 2 / 2, eta) = 0 ∧ HeatedOutgoing.E F XR c (R ^ 2 / 2, eta) = FiveRowRank.background F.data.core.lam (radialAmplitude F XR eta) R

Supported perturbations preserve the other complete open windows

def NavierStokes.ReservedPatches.Supported (F : OutgoingProfile.Profile) (XR : ℝ) (s : Slot) (v : ℝ × ℝ → ℝ) : Prop

Supported, given by ∀ eta, support (fun X => v (X, eta)) ⊆ closedPatch F XR s.

Equations

• NavierStokes.ReservedPatches.Supported F XR s v = ∀ (eta : ℝ), (Function.support fun (X : ℝ) => v (X, eta)) ⊆ NavierStokes.ReservedPatches.closedPatch F XR s

theorem NavierStokes.ReservedPatches.heat_increment_supported (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) : Supported F XR Slot.heat (HeatedOutgoing.patchIncrement F XR c)

theorem NavierStokes.ReservedPatches.five_row_updates_supported (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (s : Slot) (A : ℝ → ℝ) (c : ℝ → FiveProfileMoments.Coeff) : (Supported F XR s fun (p : ℝ × ℝ) => A p.2 * FiveProfileMoments.u (momentPatch F XR hXR s) (c p.2) p.1) ∧ Supported F XR s fun (p : ℝ × ℝ) => A p.2 * FiveProfileMoments.e (momentPatch F XR hXR s) (c p.2) p.1

The actual five-row bump formulas satisfy the support premise, for arbitrary amplitude and coefficient functions. Smoothness is irrelevant to this identity.

theorem NavierStokes.ReservedPatches.supported_vanishes (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) {s t : Slot} (hst : s ≠ t) {v : ℝ × ℝ → ℝ} (hv : Supported F XR s v) (eta : ℝ) {X : ℝ} (hX : X ∈ window F XR t) : v (X, eta) = 0

theorem NavierStokes.ReservedPatches.supported_update_eqOn (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) {s t : Slot} (hst : s ≠ t) {v : ℝ × ℝ → ℝ} (hv : Supported F XR s v) (g : ℝ × ℝ → ℝ) : Set.EqOn (fun (p : ℝ × ℝ) => g p + v p) g (window F XR t ×ˢ Set.univ)

theorem NavierStokes.ReservedPatches.supported_update_germ (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) {s t : Slot} (hst : s ≠ t) {v : ℝ × ℝ → ℝ} (hv : Supported F XR s v) (g : ℝ × ℝ → ℝ) {p : ℝ × ℝ} (hp : p.1 ∈ window F XR t) : (fun (q : ℝ × ℝ) => g q + v q) =ᶠ[nhds p] g

theorem NavierStokes.ReservedPatches.supported_update_jets (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) {s t : Slot} (hst : s ≠ t) {v : ℝ × ℝ → ℝ} (hv : Supported F XR s v) (g : ℝ × ℝ → ℝ) {p : ℝ × ℝ} (hp : p.1 ∈ window F XR t) (n : ℕ) : iteratedFDeriv ℝ n (fun (q : ℝ × ℝ) => g q + v q) p = iteratedFDeriv ℝ n g p

theorem NavierStokes.ReservedPatches.supported_updates_preserve_fields (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {s t : Slot} (hst : s ≠ t) (ht : t ≠ Slot.heat) {vU vE : ℝ × ℝ → ℝ} (hu : Supported F XR s vU) (he : Supported F XR s vE) (eta : ℝ) {X : ℝ} (hX : X ∈ window F XR t) : HeatedOutgoing.U F XR (X, eta) + vU (X, eta) = 0 ∧ HeatedOutgoing.E F XR c (X, eta) + vE (X, eta) = xAmplitude F XR eta * X ^ (-(1 / 2 + F.data.core.lam))

theorem NavierStokes.ReservedPatches.finite_updates_eqOn {ι : Type u_1} [Fintype ι] (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (t : Slot) (s : ι → Slot) (v : ι → ℝ × ℝ → ℝ) (hs : ∀ (i : ι), s i ≠ t) (hv : ∀ (i : ι), Supported F XR (s i) (v i)) (g : ℝ × ℝ → ℝ) : Set.EqOn (fun (p : ℝ × ℝ) => g p + ∑ i : ι, v i p) g (window F XR t ×ˢ Set.univ)

def NavierStokes.ReservedPatches.RadialSupported (F : OutgoingProfile.Profile) (XR : ℝ) (s : Slot) (v : ℝ × ℝ → ℝ) : Prop

Radial supported, given by ∀ eta, support (fun R => v (R, eta)) ⊆ radialWindow F XR s.

Equations

• NavierStokes.ReservedPatches.RadialSupported F XR s v = ∀ (eta : ℝ), (Function.support fun (R : ℝ) => v (R, eta)) ⊆ NavierStokes.ReservedPatches.radialWindow F XR s

theorem NavierStokes.ReservedPatches.radial_supported_vanishes (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) {s t : Slot} (hst : s ≠ t) {v : ℝ × ℝ → ℝ} (hv : RadialSupported F XR s v) (eta : ℝ) {R : ℝ} (hR : R ∈ radialWindow F XR t) : v (R, eta) = 0

This premise is exactly the open-support conclusion of the positive-order and mean bump solvers. They may use the full window or any smaller subpatch.

theorem NavierStokes.ReservedPatches.radial_supported_update_germ (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) {s t : Slot} (hst : s ≠ t) {v : ℝ × ℝ → ℝ} (hv : RadialSupported F XR s v) (g : ℝ × ℝ → ℝ) {p : ℝ × ℝ} (hp : p.1 ∈ radialWindow F XR t) : (fun (q : ℝ × ℝ) => g q + v q) =ᶠ[nhds p] g

theorem NavierStokes.ReservedPatches.radial_supported_updates_preserve_fields (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (c : ℝ → HeatedOutgoing.Coeff) {s t : Slot} (hst : s ≠ t) (ht : t ≠ Slot.heat) {vU vE : ℝ × ℝ → ℝ} (hu : RadialSupported F XR s vU) (he : RadialSupported F XR s vE) (eta : ℝ) {R : ℝ} (hR : R ∈ radialWindow F XR t) : HeatedOutgoing.U F XR (R ^ 2 / 2, eta) + vU (R, eta) = 0 ∧ HeatedOutgoing.E F XR c (R ^ 2 / 2, eta) + vE (R, eta) = FiveRowRank.background F.data.core.lam (radialAmplitude F XR eta) R

theorem NavierStokes.ReservedPatches.radial_finite_updates_eqOn {ι : Type u_1} [Fintype ι] (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (t : Slot) (s : ι → Slot) (v : ι → ℝ × ℝ → ℝ) (hs : ∀ (i : ι), s i ≠ t) (hv : ∀ (i : ι), RadialSupported F XR (s i) (v i)) (g : ℝ × ℝ → ℝ) : Set.EqOn (fun (p : ℝ × ℝ) => g p + ∑ i : ι, v i p) g (radialWindow F XR t ×ˢ Set.univ)