The compensated heat switch preserves the outgoing cone

The inverse entrance radius, the three compensation coefficients, and their actual parameter derivatives are finite-dimensional perturbation parameters. All estimates are on a fixed logarithmic interval, before the fully switched terminal edge. Constants are chosen after the outgoing profile and before the entrance radius.

theorem NavierStokes.HeatSwitchCone.compact_control_estimate {P : Type u_1} {B : Type u_2} {V : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set B} (hs : IsCompact s) (hc : Convex ℝ s) {u : Set (P × B)} (hu : IsOpen u) (hsub : {0} ×ˢ s ⊆ u) {f : P × B → V} (hf : ContDiffOn ℝ (↑⊤) f u) : ∃ (r : ℝ) (L : ℝ), 0 < r ∧ 0 ≤ L ∧ ∀ (p : P), ‖p‖ ≤ r → ∀ b ∈ s, (p, b) ∈ u ∧ ‖f (p, b) - f (0, b)‖ ≤ L * ‖p‖

A smooth finite-dimensional family has a uniform first-order estimate in its control variable near a compact convex set of base points.

@[reducible, inline]

abbrev NavierStokes.HeatSwitchCone.Point : Type

Point: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.HeatSwitchCone.Point = (ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.HeatSwitchCone.Coeff : Type

Coefficient: an abbreviation for TerminalCompensation.Coeff.

Equations

• NavierStokes.HeatSwitchCone.Coeff = NavierStokes.TerminalCompensation.Coeff

@[reducible, inline]

abbrev NavierStokes.HeatSwitchCone.Raw : Type

Raw: an abbreviation for (ℝ × Coeff) × Point.

Equations

• NavierStokes.HeatSwitchCone.Raw = ((ℝ × NavierStokes.HeatSwitchCone.Coeff) × NavierStokes.HeatSwitchCone.Point)

@[reducible, inline]

abbrev NavierStokes.HeatSwitchCone.Control : Type

Control: an abbreviation for ℝ × (Coeff × Coeff).

Equations

• NavierStokes.HeatSwitchCone.Control = (ℝ × NavierStokes.HeatSwitchCone.Coeff × NavierStokes.HeatSwitchCone.Coeff)

noncomputable def NavierStokes.HeatSwitchCone.freeE (F : OutgoingProfile.Profile) (z : Raw) : ℝ

The genuine heat multiplier, smoothly continued only in the auxiliary inverse-radius variable and outside the physical parameter band.

Equations

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

theorem NavierStokes.HeatSwitchCone.freeE_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (freeE F)

@[simp]

theorem NavierStokes.HeatSwitchCone.freeE_zero (F : OutgoingProfile.Profile) (p : Point) : freeE F ((0, 0), p) = F.logE p

noncomputable def NavierStokes.HeatSwitchCone.finitePrefix (F : OutgoingProfile.Profile) (f : Raw → ℝ) (z : Raw) : ℝ

The normalized integral of a perturbation, starting at the reserved patch.

Equations

• NavierStokes.HeatSwitchCone.finitePrefix F f z = ∫ (t : ℝ) in NavierStokes.OutgoingDilation.patchClock F..z.2.1, f (z.1, t, z.2.2)

theorem NavierStokes.HeatSwitchCone.finitePrefix_contDiff (F : OutgoingProfile.Profile) {f : Raw → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (finitePrefix F f)

noncomputable def NavierStokes.HeatSwitchCone.freeI (F : OutgoingProfile.Profile) (z : Raw) : ℝ

Free I, given by OutgoingHistories.I F.reset z.2 + finitePrefix F (fun q => Real.exp (3 * q.2.1 / 2) * (freeE F q - F.logE q.2)) z.

Equations

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

noncomputable def NavierStokes.HeatSwitchCone.freeS (F : OutgoingProfile.Profile) (z : Raw) : ℝ

Free S, constructed using OutgoingHistories.S.

Equations

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

noncomputable def NavierStokes.HeatSwitchCone.freePi (F : OutgoingProfile.Profile) (z : Raw) : ℝ

Free pi, given by OutgoingHistories.Pi F.reset z.2 + (1 / 2 : ℝ) * finitePrefix F (fun q => freeE F q ^ 2 - F.logE q.2 ^ 2) z.

Equations

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

theorem NavierStokes.HeatSwitchCone.freeI_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (freeI F)

theorem NavierStokes.HeatSwitchCone.freeS_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (freeS F)

theorem NavierStokes.HeatSwitchCone.freePi_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (freePi F)

@[simp]

theorem NavierStokes.HeatSwitchCone.freeI_zero (F : OutgoingProfile.Profile) (p : Point) : freeI F ((0, 0), p) = OutgoingHistories.I F.reset p

@[simp]

theorem NavierStokes.HeatSwitchCone.freeS_zero (F : OutgoingProfile.Profile) (p : Point) : freeS F ((0, 0), p) = OutgoingHistories.S F.reset F.amp p

@[simp]

theorem NavierStokes.HeatSwitchCone.freePi_zero (F : OutgoingProfile.Profile) (p : Point) : freePi F ((0, 0), p) = OutgoingHistories.Pi F.reset p

noncomputable def NavierStokes.HeatSwitchCone.rawPoint (z : Control × Point) : Raw

Raw point, given by ((z.1.1, z.1.2.1), z.2).

Equations

• NavierStokes.HeatSwitchCone.rawPoint z = ((z.1.1, z.1.2.1), z.2)

noncomputable def NavierStokes.HeatSwitchCone.value (f : Raw → ℝ) (z : Control × Point) : ℝ

Value, given by f (rawPoint z).

Equations

• NavierStokes.HeatSwitchCone.value f z = f (NavierStokes.HeatSwitchCone.rawPoint z)

noncomputable def NavierStokes.HeatSwitchCone.radialJet (f : Raw → ℝ) (z : Control × Point) : ℝ

Radial jet, given by fderiv ℝ f (rawPoint z) ((0, 0), (1, 0)).

Equations

• NavierStokes.HeatSwitchCone.radialJet f z = (fderiv ℝ f (NavierStokes.HeatSwitchCone.rawPoint z)) ((0, 0), 1, 0)

noncomputable def NavierStokes.HeatSwitchCone.parameterJet (f : Raw → ℝ) (z : Control × Point) : ℝ

Parameter jet, given by fderiv ℝ f (rawPoint z) ((0, z.1.2.2), (0, 1)).

Equations

• NavierStokes.HeatSwitchCone.parameterJet f z = (fderiv ℝ f (NavierStokes.HeatSwitchCone.rawPoint z)) ((0, z.1.2.2), 0, 1)

theorem NavierStokes.HeatSwitchCone.rawPoint_contDiff : ContDiff ℝ (↑⊤) rawPoint

theorem NavierStokes.HeatSwitchCone.value_contDiff {f : Raw → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (value f)

theorem NavierStokes.HeatSwitchCone.radialJet_contDiff {f : Raw → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (radialJet f)

theorem NavierStokes.HeatSwitchCone.parameterJet_contDiff {f : Raw → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (parameterJet f)

theorem NavierStokes.HeatSwitchCone.radialJet_hasDerivAt {f : Raw → ℝ} (hf : ContDiff ℝ (↑⊤) f) (v : Control) (p : Point) : HasDerivAt (fun (y : ℝ) => value f (v, y, p.2)) (radialJet f (v, p)) p.1

theorem NavierStokes.HeatSwitchCone.parameterJet_hasDerivWithinAt {f : Raw → ℝ} (hf : ContDiff ℝ (↑⊤) f) {c : ℝ → Coeff} {dc : Coeff} {s : Set ℝ} {eta : ℝ} (hc : HasDerivWithinAt c dc s eta) (delta y : ℝ) : HasDerivWithinAt (fun (t : ℝ) => f ((delta, c t), y, t)) (parameterJet f ((delta, c eta, dc), y, eta)) s eta

theorem NavierStokes.HeatSwitchCone.radialJet_zero {f : Raw → ℝ} {g : Point → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hzero : ∀ (p : Point), f ((0, 0), p) = g p) (p : Point) : radialJet f (0, p) = OutgoingHistories.dY g p

theorem NavierStokes.HeatSwitchCone.parameterJet_zero {f : Raw → ℝ} {g : Point → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hzero : ∀ (p : Point), f ((0, 0), p) = g p) (p : Point) : parameterJet f (0, p) = OutgoingHistories.dEta g p

theorem NavierStokes.HeatSwitchCone.radius_quotient (XR y a : ℝ) (hXR : 0 < XR) : XR * Real.exp y / (XR * Real.exp a) = Real.exp (y - a)

theorem NavierStokes.HeatSwitchCone.freeE_eq_physical (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (hXR : 0 < XR) (y eta : ℝ) (heta : eta ∈ HeatedOutgoing.parameterDomain) : freeE F ((1 / XR, c eta), y, eta) = HeatedOutgoing.E F XR c (XR * Real.exp y, eta)

Exact equality with the physical edit, including the actual diffusion 1 - eta^2 and all three additive compensation bumps.

noncomputable def NavierStokes.HeatSwitchCone.controls (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (eta : ℝ) : Control

Controls, given by (1 / XR, (w.coefficients eta, derivWithin w.coefficients HeatedOutgoing.parameterDomain eta)).

Equations

• NavierStokes.HeatSwitchCone.controls F w eta = (1 / XR, w.coefficients eta, derivWithin w.coefficients NavierStokes.HeatedOutgoing.parameterDomain eta)

theorem NavierStokes.HeatSwitchCone.controls_norm (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {eta : ℝ} (heta : eta ∈ HeatedOutgoing.parameterDomain) : ‖controls F w eta‖ ≤ max (Real.exp (HeatTailEdit.switchStart F.data)) C / OutgoingDilation.switchRadius F XR

noncomputable def NavierStokes.HeatSwitchCone.angularNumerator (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Angular numerator as an element of ℝ.

Equations

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

noncomputable def NavierStokes.HeatSwitchCone.radialNumerator (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Radial numerator, given by value (freeE F) z - 2 * radialJet (freeE F) z.

Equations

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

noncomputable def NavierStokes.HeatSwitchCone.familyQ (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family Q, given by angularNumerator F z / (Real.exp (3 * z.2.1 / 2) * value (freeE F) z).

Equations

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

noncomputable def NavierStokes.HeatSwitchCone.familyN (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family N as an element of ℝ.

Equations

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

noncomputable def NavierStokes.HeatSwitchCone.familyA (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family A, given by radialNumerator F z / value (freeE F) z.

Equations

• NavierStokes.HeatSwitchCone.familyA F z = NavierStokes.HeatSwitchCone.radialNumerator F z / NavierStokes.HeatSwitchCone.value (NavierStokes.HeatSwitchCone.freeE F) z

noncomputable def NavierStokes.HeatSwitchCone.familyB (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family B, given by 2 * OutgoingHistories.dY F.logU z.2 / value (freeE F) z.

Equations

• NavierStokes.HeatSwitchCone.familyB F z = 2 * NavierStokes.OutgoingHistories.dY F.logU z.2 / NavierStokes.HeatSwitchCone.value (NavierStokes.HeatSwitchCone.freeE F) z

noncomputable def NavierStokes.HeatSwitchCone.familyR (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family R, given by familyN F z / (value (freeE F) z * familyQ F z).

Equations

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

noncomputable def NavierStokes.HeatSwitchCone.familyC (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family C, given by 1 - familyB F z * familyR F z / familyA F z.

Equations

• NavierStokes.HeatSwitchCone.familyC F z = 1 - NavierStokes.HeatSwitchCone.familyB F z * NavierStokes.HeatSwitchCone.familyR F z / NavierStokes.HeatSwitchCone.familyA F z

noncomputable def NavierStokes.HeatSwitchCone.familyJ (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family J, given by familyR F z + familyB F z / familyA F z.

Equations

• NavierStokes.HeatSwitchCone.familyJ F z = NavierStokes.HeatSwitchCone.familyR F z + NavierStokes.HeatSwitchCone.familyB F z / NavierStokes.HeatSwitchCone.familyA F z

noncomputable def NavierStokes.HeatSwitchCone.familyV (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family V, given by familyA F z * (1 + (familyB F z / familyA F z) ^ 2).

Equations

• NavierStokes.HeatSwitchCone.familyV F z = NavierStokes.HeatSwitchCone.familyA F z * (1 + (NavierStokes.HeatSwitchCone.familyB F z / NavierStokes.HeatSwitchCone.familyA F z) ^ 2)

noncomputable def NavierStokes.HeatSwitchCone.familyGap (F : OutgoingProfile.Profile) (z : Control × Point) : ℝ

Family gap, given by 2 * familyC F z ^ 2 - (familyV F z - 2) * familyJ F z ^ 2.

Equations

• NavierStokes.HeatSwitchCone.familyGap F z = 2 * NavierStokes.HeatSwitchCone.familyC F z ^ 2 - (NavierStokes.HeatSwitchCone.familyV F z - 2) * NavierStokes.HeatSwitchCone.familyJ F z ^ 2

theorem NavierStokes.HeatSwitchCone.angularNumerator_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (angularNumerator F)

theorem NavierStokes.HeatSwitchCone.radialNumerator_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (radialNumerator F)

theorem NavierStokes.HeatSwitchCone.familyN_contDiff (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (familyN F)

noncomputable def NavierStokes.HeatSwitchCone.regular (F : OutgoingProfile.Profile) : Set (Control × Point)

This open set excludes only the denominators of the actual normalized cone coordinates. Its zero-control slice contains the clean true cone.

Equations

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

theorem NavierStokes.HeatSwitchCone.regular_isOpen (F : OutgoingProfile.Profile) : IsOpen (regular F)

theorem NavierStokes.HeatSwitchCone.familyQ_ne (F : OutgoingProfile.Profile) {z : Control × Point} (hz : z ∈ regular F) : familyQ F z ≠ 0

theorem NavierStokes.HeatSwitchCone.familyA_ne (F : OutgoingProfile.Profile) {z : Control × Point} (hz : z ∈ regular F) : familyA F z ≠ 0

theorem NavierStokes.HeatSwitchCone.familyQ_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (familyQ F) (regular F)

theorem NavierStokes.HeatSwitchCone.familyA_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (familyA F) (regular F)

theorem NavierStokes.HeatSwitchCone.familyB_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (familyB F) (regular F)

theorem NavierStokes.HeatSwitchCone.familyR_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (familyR F) (regular F)

theorem NavierStokes.HeatSwitchCone.familyC_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (familyC F) (regular F)

theorem NavierStokes.HeatSwitchCone.familyJ_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (familyJ F) (regular F)

theorem NavierStokes.HeatSwitchCone.familyV_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (familyV F) (regular F)

theorem NavierStokes.HeatSwitchCone.familyGap_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (familyGap F) (regular F)

@[simp]

theorem NavierStokes.HeatSwitchCone.familyQ_zero (F : OutgoingProfile.Profile) (p : Point) : familyQ F (0, p) = OutgoingHistories.Qs F.reset F.amp p

@[simp]

theorem NavierStokes.HeatSwitchCone.familyN_zero (F : OutgoingProfile.Profile) (p : Point) : familyN F (0, p) = OutgoingHistories.Ns F.reset F.amp p

@[simp]

theorem NavierStokes.HeatSwitchCone.familyA_zero (F : OutgoingProfile.Profile) (p : Point) : familyA F (0, p) = OutgoingEntranceCone.coneA F.reset p

@[simp]

theorem NavierStokes.HeatSwitchCone.familyB_zero (F : OutgoingProfile.Profile) (p : Point) : familyB F (0, p) = OutgoingEntranceCone.coneB F.reset F.amp p

@[simp]

theorem NavierStokes.HeatSwitchCone.familyR_zero (F : OutgoingProfile.Profile) (p : Point) : familyR F (0, p) = OutgoingEntranceCone.coneRatio F.reset F.amp p

@[simp]

theorem NavierStokes.HeatSwitchCone.familyC_zero (F : OutgoingProfile.Profile) (p : Point) : familyC F (0, p) = OutgoingCone.sourceC F.reset F.amp p

@[simp]

theorem NavierStokes.HeatSwitchCone.familyJ_zero (F : OutgoingProfile.Profile) (p : Point) : familyJ F (0, p) = OutgoingCone.sourceJ F.reset F.amp p

@[simp]

theorem NavierStokes.HeatSwitchCone.familyV_zero (F : OutgoingProfile.Profile) (p : Point) : familyV F (0, p) = OutgoingCone.normalV F.reset F.amp p

@[simp]

theorem NavierStokes.HeatSwitchCone.familyGap_zero (F : OutgoingProfile.Profile) (p : Point) : familyGap F (0, p) = OutgoingCone.leadingGap F.reset F.amp p

noncomputable def NavierStokes.HeatSwitchCone.realize (f : Raw → ℝ) (delta : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Evaluation at the actual compensation coefficients.

Equations

• NavierStokes.HeatSwitchCone.realize f delta c p = f ((delta, c p.2), p)

theorem NavierStokes.HeatSwitchCone.realize_radial_derivative {f : Raw → ℝ} (hf : ContDiff ℝ (↑⊤) f) (delta : ℝ) (c : ℝ → Coeff) (p : Point) (dc : Coeff) : deriv (fun (y : ℝ) => realize f delta c (y, p.2)) p.1 = radialJet f ((delta, c p.2, dc), p)

theorem NavierStokes.HeatSwitchCone.realize_parameter_derivative {f : Raw → ℝ} (hf : ContDiff ℝ (↑⊤) f) (delta : ℝ) {c : ℝ → Coeff} (hc : ContDiffOn ℝ (↑⊤) c HeatedOutgoing.parameterDomain) {p : Point} (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : derivWithin (fun (eta : ℝ) => realize f delta c (p.1, eta)) HeatedOutgoing.parameterDomain p.2 = parameterJet f ((delta, c p.2, derivWithin c HeatedOutgoing.parameterDomain p.2), p)

noncomputable def NavierStokes.HeatSwitchCone.logE (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

The actual angular velocity in the fixed logarithmic coordinate.

Equations

• NavierStokes.HeatSwitchCone.logE F XR c p = NavierStokes.HeatedOutgoing.E F XR c (XR * Real.exp p.1, p.2)

noncomputable def NavierStokes.HeatSwitchCone.logI (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Incoming histories are retained. Only the integrals of the actual changes beginning at the reserved patch are added.

Equations

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

noncomputable def NavierStokes.HeatSwitchCone.logS (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Log S, constructed using OutgoingHistories.S.

Equations

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

noncomputable def NavierStokes.HeatSwitchCone.logPi (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Log pi, constructed using OutgoingHistories.Pi.

Equations

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

theorem NavierStokes.HeatSwitchCone.logE_eq_realize (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (hXR : 0 < XR) (p : Point) (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : logE F XR c p = realize (freeE F) (1 / XR) c p

theorem NavierStokes.HeatSwitchCone.logI_eq_realize (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (hXR : 0 < XR) (p : Point) (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : logI F XR c p = realize (freeI F) (1 / XR) c p

theorem NavierStokes.HeatSwitchCone.logS_eq_realize (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (hXR : 0 < XR) (p : Point) (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : logS F XR c p = realize (freeS F) (1 / XR) c p

theorem NavierStokes.HeatSwitchCone.logPi_eq_realize (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (hXR : 0 < XR) (p : Point) (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : logPi F XR c p = realize (freePi F) (1 / XR) c p

theorem NavierStokes.HeatSwitchCone.logE_before_patch (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → Coeff) {p : Point} (hp : p.1 ≤ OutgoingDilation.patchClock F) : logE F XR c p = F.logE p

theorem NavierStokes.HeatSwitchCone.logE_parameter_derivative (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : Point} (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : derivWithin (fun (eta : ℝ) => logE F XR w.coefficients (p.1, eta)) HeatedOutgoing.parameterDomain p.2 = parameterJet (freeE F) (controls F w p.2, p)

theorem NavierStokes.HeatSwitchCone.logI_parameter_derivative (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : Point} (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : derivWithin (fun (eta : ℝ) => logI F XR w.coefficients (p.1, eta)) HeatedOutgoing.parameterDomain p.2 = parameterJet (freeI F) (controls F w p.2, p)

theorem NavierStokes.HeatSwitchCone.logS_parameter_derivative (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : Point} (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : derivWithin (fun (eta : ℝ) => logS F XR w.coefficients (p.1, eta)) HeatedOutgoing.parameterDomain p.2 = parameterJet (freeS F) (controls F w p.2, p)

theorem NavierStokes.HeatSwitchCone.logPi_parameter_derivative (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : Point} (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : derivWithin (fun (eta : ℝ) => logPi F XR w.coefficients (p.1, eta)) HeatedOutgoing.parameterDomain p.2 = parameterJet (freePi F) (controls F w p.2, p)

theorem NavierStokes.HeatSwitchCone.logE_radial_derivative (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : Point} (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : deriv (fun (y : ℝ) => logE F XR w.coefficients (y, p.2)) p.1 = radialJet (freeE F) (controls F w p.2, p)

theorem NavierStokes.HeatSwitchCone.zero_regular (F : OutgoingProfile.Profile) {anchor left : ℝ} (h : OutgoingCone.CleanOutgoingCone F.reset anchor left) (ha : 0 < anchor) {p : Point} (hp : p ∈ OutgoingCone.trueWindow F.data) : (0, p) ∈ regular F

noncomputable def NavierStokes.HeatSwitchCone.observations (F : OutgoingProfile.Profile) (z : Control × Point) : Fin 18 → ℝ

Values, all first jets needed in (9), both lags, and all normalized stress coordinates. The last coordinate is the leading strict cone gap.

Equations

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

theorem NavierStokes.HeatSwitchCone.observations_contDiffOn (F : OutgoingProfile.Profile) : ContDiffOn ℝ (↑⊤) (observations F) (regular F)

theorem NavierStokes.HeatSwitchCone.observations_estimate (F : OutgoingProfile.Profile) {anchor left : ℝ} (h : OutgoingCone.CleanOutgoingCone F.reset anchor left) (ha : 0 < anchor) : ∃ (r : ℝ) (L : ℝ), 0 < r ∧ 0 ≤ L ∧ ∀ (v : Control), ‖v‖ ≤ r → ∀ p ∈ OutgoingCone.trueWindow F.data, (v, p) ∈ regular F ∧ ‖observations F (v, p) - observations F (0, p)‖ ≤ L * ‖v‖

theorem NavierStokes.HeatSwitchCone.compensated_observations_bound (F : OutgoingProfile.Profile) {anchor left : ℝ} (h : OutgoingCone.CleanOutgoingCone F.reset anchor left) (ha : 0 < anchor) (C : ℝ) : ∃ (XR₀ : ℝ) (B : ℝ), 0 < XR₀ ∧ 0 < B ∧ ∀ (XR : ℝ), XR₀ ≤ XR → ∀ (w : HeatedOutgoing.CompensationWitness F XR C), ∀ p ∈ OutgoingCone.trueWindow F.data, (controls F w p.2, p) ∈ regular F ∧ ∀ (i : Fin 18), |observations F (controls F w p.2, p) i - observations F (0, p) i| ≤ B / OutgoingDilation.switchRadius F XR

A single constant controls the actual value, radial and parameter jets, histories, lags and normalized stresses. It is fixed before XR or the particular compensation witness at that radius is chosen.

theorem NavierStokes.HeatSwitchCone.cleanPi_eq (F : OutgoingProfile.Profile) (p : Point) : F.logPi p = OutgoingHistories.Pi F.reset p

theorem NavierStokes.HeatSwitchCone.cleanPi_increment (F : OutgoingProfile.Profile) (a y eta : ℝ) : 1 / 2 * ∫ (t : ℝ) in a..y, F.logE (t, eta) ^ 2 = OutgoingHistories.Pi F.reset (y, eta) - OutgoingHistories.Pi F.reset (a, eta)

theorem NavierStokes.HeatSwitchCone.logPi_eq_canonical (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (p : Point) (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : logPi F XR w.coefficients p = HeatedOutgoing.Pi F XR w.coefficients (XR * Real.exp p.1, p.2)

The pressure in the normalized histories is the actual canonical future integral. The proof uses exact three-row compensation through the existing pressure primitive, not an independently chosen pressure constant.

noncomputable def NavierStokes.HeatSwitchCone.Qs (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Qs as an element of ℝ.

Equations

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

noncomputable def NavierStokes.HeatSwitchCone.Ns (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Ns as an element of ℝ.

Equations

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

noncomputable def NavierStokes.HeatSwitchCone.radialA (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Radial A, given by 1 - 2 * deriv (fun y => logE F XR c (y, p.2)) p.1 / logE F XR c p.

Equations

• NavierStokes.HeatSwitchCone.radialA F XR c p = 1 - 2 * deriv (fun (y : ℝ) => NavierStokes.HeatSwitchCone.logE F XR c (y, p.2)) p.1 / NavierStokes.HeatSwitchCone.logE F XR c p

noncomputable def NavierStokes.HeatSwitchCone.radialB (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Radial B, given by 2 * OutgoingHistories.dY F.logU p / logE F XR c p.

Equations

• NavierStokes.HeatSwitchCone.radialB F XR c p = 2 * NavierStokes.OutgoingHistories.dY F.logU p / NavierStokes.HeatSwitchCone.logE F XR c p

noncomputable def NavierStokes.HeatSwitchCone.ratio (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Ratio, given by Ns F XR c p / (logE F XR c p * Qs F XR c p).

Equations

• NavierStokes.HeatSwitchCone.ratio F XR c p = NavierStokes.HeatSwitchCone.Ns F XR c p / (NavierStokes.HeatSwitchCone.logE F XR c p * NavierStokes.HeatSwitchCone.Qs F XR c p)

noncomputable def NavierStokes.HeatSwitchCone.sourceC (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Source C, given by 1 - radialB F XR c p * ratio F XR c p / radialA F XR c p.

Equations

• NavierStokes.HeatSwitchCone.sourceC F XR c p = 1 - NavierStokes.HeatSwitchCone.radialB F XR c p * NavierStokes.HeatSwitchCone.ratio F XR c p / NavierStokes.HeatSwitchCone.radialA F XR c p

noncomputable def NavierStokes.HeatSwitchCone.sourceJ (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Source J, given by ratio F XR c p + radialB F XR c p / radialA F XR c p.

Equations

• NavierStokes.HeatSwitchCone.sourceJ F XR c p = NavierStokes.HeatSwitchCone.ratio F XR c p + NavierStokes.HeatSwitchCone.radialB F XR c p / NavierStokes.HeatSwitchCone.radialA F XR c p

noncomputable def NavierStokes.HeatSwitchCone.normalV (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Normal V, given by radialA F XR c p * (1 + (radialB F XR c p / radialA F XR c p) ^ 2).

Equations

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

noncomputable def NavierStokes.HeatSwitchCone.leadingGap (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Leading gap, given by 2 * sourceC F XR c p ^ 2 - (normalV F XR c p - 2) * sourceJ F XR c p ^ 2.

Equations

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

theorem NavierStokes.HeatSwitchCone.Qs_eq_family (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : Point} (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : Qs F XR w.coefficients p = familyQ F (controls F w p.2, p)

theorem NavierStokes.HeatSwitchCone.Ns_eq_family (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : Point} (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : Ns F XR w.coefficients p = familyN F (controls F w p.2, p)

theorem NavierStokes.HeatSwitchCone.radialA_eq_family (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : Point} (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : radialA F XR w.coefficients p = familyA F (controls F w p.2, p)

theorem NavierStokes.HeatSwitchCone.normalized_eq_family (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : Point} (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : radialB F XR w.coefficients p = familyB F (controls F w p.2, p) ∧ ratio F XR w.coefficients p = familyR F (controls F w p.2, p) ∧ sourceC F XR w.coefficients p = familyC F (controls F w p.2, p) ∧ sourceJ F XR w.coefficients p = familyJ F (controls F w p.2, p) ∧ normalV F XR w.coefficients p = familyV F (controls F w p.2, p) ∧ leadingGap F XR w.coefficients p = familyGap F (controls F w p.2, p)

noncomputable def NavierStokes.HeatSwitchCone.actualObservations (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : Fin 18 → ℝ

Actual observations as an element of Fin 18 → ℝ.

Equations

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

theorem NavierStokes.HeatSwitchCone.actualObservations_eq (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {p : Point} (hp : p.2 ∈ HeatedOutgoing.parameterDomain) : actualObservations F XR w.coefficients p = observations F (controls F w p.2, p)

theorem NavierStokes.HeatSwitchCone.actual_observations_bound (F : OutgoingProfile.Profile) {anchor left : ℝ} (h : OutgoingCone.CleanOutgoingCone F.reset anchor left) (ha : 0 < anchor) (C : ℝ) : ∃ (XR₀ : ℝ) (B : ℝ), 0 < XR₀ ∧ 0 < B ∧ ∀ (XR : ℝ), XR₀ ≤ XR → ∀ (w : HeatedOutgoing.CompensationWitness F XR C), ∀ p ∈ OutgoingCone.trueWindow F.data, ∀ (i : Fin 18), |actualObservations F XR w.coefficients p i - observations F (0, p) i| ≤ B / OutgoingDilation.switchRadius F XR

theorem NavierStokes.HeatSwitchCone.div_switch_le (F : OutgoingProfile.Profile) {B eps XR : ℝ} (heps : 0 < eps) (hXR : 0 < XR) (hlarge : B / (eps * Real.exp (HeatTailEdit.switchStart F.data)) ≤ XR) : B / OutgoingDilation.switchRadius F XR ≤ eps

theorem NavierStokes.HeatSwitchCone.compensated_source_margins (F : OutgoingProfile.Profile) {anchor left : ℝ} (h : OutgoingCone.CleanOutgoingCone F.reset anchor left) (ha : 0 < anchor) (C : ℝ) : ∃ (XR₀ : ℝ) (m : ℝ) (T : ℝ), 0 < XR₀ ∧ 0 < m ∧ 0 < T ∧ ∀ (XR : ℝ), XR₀ ≤ XR → ∀ (w : HeatedOutgoing.CompensationWitness F XR C), ∀ p ∈ OutgoingCone.trueWindow F.data, m ≤ Qs F XR w.coefficients p ∧ m ≤ radialA F XR w.coefficients p ∧ m ≤ normalV F XR w.coefficients p - 2 ∧ m ≤ sourceC F XR w.coefficients p ∧ m ≤ leadingGap F XR w.coefficients p ∧ |sourceC F XR w.coefficients p| ≤ T ∧ |normalV F XR w.coefficients p| ≤ T

Uniform strict source margins for every sufficiently large physical radius, with a bound for the two coordinates entering the finite-radius quadratic test. All constants precede the radius and witness quantifiers.

noncomputable def NavierStokes.HeatSwitchCone.stressScale (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Stress scale, given by XR * Real.exp p.1 * Qs F XR c p / CoordinateAlgebra.L F.data.h p.2.

Equations

• NavierStokes.HeatSwitchCone.stressScale F XR c p = XR * Real.exp p.1 * NavierStokes.HeatSwitchCone.Qs F XR c p / NavierStokes.CoordinateAlgebra.L F.data.h p.2

noncomputable def NavierStokes.HeatSwitchCone.normalP (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Normal P, given by stressScale F XR c p * sourceC F XR c p.

Equations

• NavierStokes.HeatSwitchCone.normalP F XR c p = NavierStokes.HeatSwitchCone.stressScale F XR c p * NavierStokes.HeatSwitchCone.sourceC F XR c p

noncomputable def NavierStokes.HeatSwitchCone.normalJ (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : ℝ

Normal J, given by stressScale F XR c p * sourceJ F XR c p.

Equations

• NavierStokes.HeatSwitchCone.normalJ F XR c p = NavierStokes.HeatSwitchCone.stressScale F XR c p * NavierStokes.HeatSwitchCone.sourceJ F XR c p

def NavierStokes.HeatSwitchCone.TrueAt (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → Coeff) (p : Point) : Prop

The strict true cone, expressed in the same normalized stress coordinates as the clean outgoing theorem.

Equations

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

theorem NavierStokes.HeatSwitchCone.preserves_true_cone (F : OutgoingProfile.Profile) {anchor left : ℝ} (h : OutgoingCone.CleanOutgoingCone F.reset anchor left) (ha : 0 < anchor) (C : ℝ) : ∃ (XR₀ : ℝ), 0 < XR₀ ∧ ∀ (XR : ℝ), XR₀ ≤ XR → ∀ (w : HeatedOutgoing.CompensationWitness F XR C), ∀ p ∈ OutgoingCone.trueWindow F.data, TrueAt F XR w.coefficients p

Compensation and the full switch-on interval preserve the strict true cone. The outgoing profile, its reset and its axial amplitude remain fixed. The final radius threshold is uniform over all compensation witnesses having the previously fixed coefficient constant C.

theorem NavierStokes.HeatSwitchCone.exists_compensated_true_cone (F : OutgoingProfile.Profile) {anchor left : ℝ} (h : OutgoingCone.CleanOutgoingCone F.reset anchor left) (ha : 0 < anchor) : ∃ (XR₀ : ℝ) (C : ℝ), 0 < XR₀ ∧ 0 < C ∧ ∀ (XR : ℝ), XR₀ ≤ XR → ∃ (w : HeatedOutgoing.CompensationWitness F XR C), ∀ p ∈ OutgoingCone.trueWindow F.data, TrueAt F XR w.coefficients p

Existence uses the already constructed compensation branch for the same outgoing profile, after taking the maximum of its threshold and the cone threshold.

theorem NavierStokes.HeatSwitchCone.past_integrable_from {f : ℝ → ℝ} (hf : Continuous f) {a : ℝ} (ha : MeasureTheory.IntegrableOn f (Set.Iic a) MeasureTheory.volume) (y : ℝ) : MeasureTheory.IntegrableOn f (Set.Iic y) MeasureTheory.volume

theorem NavierStokes.HeatSwitchCone.past_integral_update {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) {a : ℝ} (ha : MeasureTheory.IntegrableOn f (Set.Iic a) MeasureTheory.volume) (he : ∀ t ≤ a, g t = f t) (y : ℝ) : MeasureTheory.IntegrableOn g (Set.Iic y) MeasureTheory.volume ∧ ∫ (t : ℝ) in Set.Iic y, g t = (∫ (t : ℝ) in Set.Iic y, f t) + ∫ (t : ℝ) in a..y, g t - f t

Updating an actual past integral by the finite integral of the change. The two functions agree throughout their entire incoming history.

theorem NavierStokes.HeatSwitchCone.logE_continuous_radial (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → Coeff) {eta : ℝ} (heta : eta ∈ HeatedOutgoing.parameterDomain) : Continuous fun (y : ℝ) => logE F XR c (y, eta)

theorem NavierStokes.HeatSwitchCone.logI_eq_past_integral (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → Coeff) {eta : ℝ} (heta : eta ∈ HeatedOutgoing.parameterDomain) (y : ℝ) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (3 * t / 2) * logE F XR c (t, eta)) (Set.Iic y) MeasureTheory.volume ∧ logI F XR c (y, eta) = ∫ (t : ℝ) in Set.Iic y, Real.exp (3 * t / 2) * logE F XR c (t, eta)

theorem NavierStokes.HeatSwitchCone.logS_eq_past_integral (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → Coeff) {eta : ℝ} (heta : eta ∈ HeatedOutgoing.parameterDomain) (y : ℝ) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp t * (F.logU (t, eta) ^ 2 - logE F XR c (t, eta) ^ 2 / 2)) (Set.Iic y) MeasureTheory.volume ∧ logS F XR c (y, eta) = ∫ (t : ℝ) in Set.Iic y, Real.exp t * (F.logU (t, eta) ^ 2 - logE F XR c (t, eta) ^ 2 / 2)

theorem NavierStokes.HeatSwitchCone.logE_mul_logU (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → Coeff) (p : Point) : logE F XR c p * F.logU p = F.logE p * F.logU p

theorem NavierStokes.HeatSwitchCone.J_eq_heated_past_integral (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → Coeff) (y eta : ℝ) : OutgoingHistories.J F.reset F.amp (y, eta) = ∫ (t : ℝ) in Set.Iic y, Real.exp (3 * t / 2) * logE F XR c (t, eta) * F.logU (t, eta)

theorem NavierStokes.HeatSwitchCone.changeRow_after_switch (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (c : ℝ → Coeff) (eta : ℝ) (i : Fin 3) {X : ℝ} (hX : OutgoingDilation.switchRadius F XR ≤ X) : HeatedOutgoing.changeRow F XR c eta i X = HeatedOutgoing.heatRow F XR eta i X

theorem NavierStokes.HeatSwitchCone.changeRow_prefix_eq_neg_future_heat (F : OutgoingProfile.Profile) {XR C : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) {eta : ℝ} (heta : eta ∈ HeatedOutgoing.parameterDomain) (i : Fin 3) {X : ℝ} (hX : OutgoingDilation.switchRadius F XR ≤ X) : ∫ (t : ℝ) in Set.Ioc 0 X, HeatedOutgoing.changeRow F XR w.coefficients eta i t = -∫ (t : ℝ) in Set.Ioi X, HeatedOutgoing.heatRow F XR eta i t

Exact restored total moments identify a finite-point change with the remaining future heat debt. In particular finite histories do not become equal merely because compensation is completed.