A common witness for nominal-profile assembly

The outgoing schedule, angular reset, corrected amplitude, and pressure datum are fixed first. The natural-axis construction below uses exactly that datum and that value of h. The five-row correction is a fixed, constructed local inverse applied to the actual debt of the assembled prefix.

@[reducible, inline]

abbrev NavierStokes.NominalProfile.Point : Type

Point: an abbreviation for ℝ × ℝ.

Equations

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

@[reducible, inline]

abbrev NavierStokes.NominalProfile.Field : Type

Field: an abbreviation for Point → ℝ.

Equations

• NavierStokes.NominalProfile.Field = (NavierStokes.NominalProfile.Point → ℝ)

@[reducible, inline]

abbrev NavierStokes.NominalProfile.Debt : Type

Debt: an abbreviation for FiveProfileMoments.Debt.

Equations

• NavierStokes.NominalProfile.Debt = NavierStokes.FiveProfileMoments.Debt

@[reducible, inline]

abbrev NavierStokes.NominalProfile.Coeff : Type

Coefficient: an abbreviation for FiveProfileMoments.Coeff.

Equations

• NavierStokes.NominalProfile.Coeff = NavierStokes.FiveProfileMoments.Coeff

structure NavierStokes.NominalProfile.AxisPreparation (F : OutgoingProfile.Profile) (j : ℝ) : Type

The axis choices are made after fixing this particular outgoing profile.

• delta : ℝ

  Delta of AxisPreparation, of type ℝ.

• sigma : ℝ

  Sigma of AxisPreparation, of type ℝ.

• delta_pos : 0 < self.delta
• sigma_pos : 0 < self.sigma
• inputs : NaturalAxisCoefficients.AnalyticInputs F.data.h j self.sigma F.axisDatum

  Inputs of AxisPreparation, of type NaturalAxisCoefficients.AnalyticInputs F.data.h j sigma F.axisDatum.

• scaleBound : ℝ

  Scale bound of AxisPreparation, of type ℝ.

• scaleBound_pos : 0 < self.scaleBound
• entrances (Λ : ℝ) : self.scaleBound ≤ Λ → ∀ (C : ℝ), NaturalEntrance.entranceNormalization self.inputs Λ self.delta ≤ C → Nonempty (NaturalEntrance.EntranceProfile self.inputs Λ C)

theorem NavierStokes.NominalProfile.prepare_axis (F : OutgoingProfile.Profile) (hP : 2 ≤ F.data.core.P) {j : ℝ} (hj : NaturalAxisData.SmallParameters F.data.h j) : Nonempty (AxisPreparation F j)

structure NavierStokes.NominalProfile.AxisStage (F : OutgoingProfile.Profile) : Type

The scale is selected before the normalization; both retain the same outgoing profile and the same analytic axis data.

• j : ℝ

  J of AxisStage, of type ℝ.

• small : NaturalAxisData.SmallParameters F.data.h self.j
• preparation : AxisPreparation F self.j

  Preparation of AxisStage, of type AxisPreparation F j.

• scale : ℝ

  Scale of AxisStage, of type ℝ.

• normalization : ℝ

  Normalization of AxisStage, of type ℝ.

• scale_large : self.preparation.scaleBound ≤ self.scale
• normalization_large : NaturalEntrance.entranceNormalization self.preparation.inputs self.scale self.preparation.delta ≤ self.normalization
• chosenNatural : NaturalEntrance.EntranceProfile self.preparation.inputs self.scale self.normalization

  Chosen natural of AxisStage, of type NaturalEntrance.EntranceProfile preparation.inputs scale normalization.

theorem NavierStokes.NominalProfile.AxisStage.scale_pos {F : OutgoingProfile.Profile} (A : AxisStage F) : 0 < A.scale

theorem NavierStokes.NominalProfile.AxisStage.normalization_pos {F : OutgoingProfile.Profile} (A : AxisStage F) : 0 < A.normalization

noncomputable def NavierStokes.NominalProfile.AxisStage.natural {F : OutgoingProfile.Profile} (A : AxisStage F) : NaturalEntrance.EntranceProfile A.preparation.inputs A.scale A.normalization

Natural, given by A.chosenNatural.

Equations

• A.natural = A.chosenNatural

noncomputable def NavierStokes.NominalProfile.AxisStage.referenceInput {F : OutgoingProfile.Profile} (A : AxisStage F) : ReferencePath.Input

Reference input, given by ReferencePath.Input.ofNatural A.scale_pos A.natural.profile.family.

Equations

• A.referenceInput = NavierStokes.ReferencePath.Input.ofNatural ⋯ A.natural.profile.family

theorem NavierStokes.NominalProfile.AxisStage.reference_scale {F : OutgoingProfile.Profile} (A : AxisStage F) : A.referenceInput.scale = A.scale

theorem NavierStokes.NominalProfile.AxisStage.reference_f {F : OutgoingProfile.Profile} (A : AxisStage F) : A.referenceInput.f = A.natural.profile.family.f

theorem NavierStokes.NominalProfile.AxisStage.reference_U {F : OutgoingProfile.Profile} (A : AxisStage F) : A.referenceInput.U = A.natural.profile.family.U

noncomputable def NavierStokes.NominalProfile.AxisStage.reference {F : OutgoingProfile.Profile} (A : AxisStage F) (δ : ℝ) (hδ : 0 < δ) (hδsmall : 2 * δ < ReferencePath.rampLimit) : ProfileHistories.Profiles A.referenceInput.radialDomain

Reference, given by A.referenceInput.histories hδ hδsmall F.axisDatum F.axisDatum_contDiff.

Equations

• A.reference δ hδ hδsmall = A.referenceInput.histories hδ hδsmall F.axisDatum ⋯

theorem NavierStokes.NominalProfile.AxisStage.reference_pressure0 {F : OutgoingProfile.Profile} (A : AxisStage F) (δ : ℝ) (hδ : 0 < δ) (hδsmall : 2 * δ < ReferencePath.rampLimit) : (A.reference δ hδ hδsmall).pressure0 = F.axisDatum

noncomputable def NavierStokes.NominalProfile.AxisStage.activation {F : OutgoingProfile.Profile} (A : AxisStage F) (δ : ℝ) (hδ : 0 < δ) (hδsmall : 2 * δ < ReferencePath.rampLimit) : TransitionRamp.StockReference ReferencePath.parameterInterval

The stocks used in ACT come from this exact REF profile.

Equations

• A.activation δ hδ hδsmall = NavierStokes.TransitionRamp.ofNatural A.natural.profile.family ⋯ ⋯ hδ hδsmall ⋯

theorem NavierStokes.NominalProfile.AxisStage.activation_profiles {F : OutgoingProfile.Profile} (A : AxisStage F) (δ : ℝ) (hδ : 0 < δ) (hδsmall : 2 * δ < ReferencePath.rampLimit) : (A.activation δ hδ hδsmall).profiles = A.reference δ hδ hδsmall

theorem NavierStokes.NominalProfile.AxisStage.activation_radius {F : OutgoingProfile.Profile} (A : AxisStage F) (δ : ℝ) (hδ : 0 < δ) (hδsmall : 2 * δ < ReferencePath.rampLimit) : (A.activation δ hδ hδsmall).radius0 = 4 / A.scale

theorem NavierStokes.NominalProfile.AxisStage.activation_initial {F : OutgoingProfile.Profile} (A : AxisStage F) (δ : ℝ) (hδ : 0 < δ) (hδsmall : 2 * δ < ReferencePath.rampLimit) (T κ w₁ w₂ : ℝ) {p : Point} (hp : p.1 ≤ 4 / A.scale) : (A.activation δ hδ hδsmall).physicalF T κ w₁ w₂ p = A.natural.profile.family.f p ∧ (A.activation δ hδ hδsmall).physicalU T κ w₁ p = A.natural.profile.family.U p

theorem NavierStokes.NominalProfile.exists_axis_stage (F : OutgoingProfile.Profile) (hP : 2 ≤ F.data.core.P) {j : ℝ} (hj : NaturalAxisData.SmallParameters F.data.h j) (scaleFloor normFloor : ℝ) : ∃ (A : AxisStage F), A.j = j ∧ scaleFloor ≤ A.scale ∧ normFloor ≤ A.normalization

Matching geometry: the radius is derived from the same normalization

noncomputable def NavierStokes.NominalProfile.Xi : ℝ

Xi, given by 110.

Equations

• NavierStokes.NominalProfile.Xi = 110

noncomputable def NavierStokes.NominalProfile.matchingRadius (F : OutgoingProfile.Profile) (C : ℝ) : ℝ

Matching radius, given by ShapeTransition.resetRadius Xi C F.data.core.P.

Equations

• NavierStokes.NominalProfile.matchingRadius F C = NavierStokes.ShapeTransition.resetRadius NavierStokes.NominalProfile.Xi C F.data.core.P

noncomputable def NavierStokes.NominalProfile.matchFraction : ℝ

Match fraction, given by Real.exp (-5).

Equations

• NavierStokes.NominalProfile.matchFraction = Real.exp (-5)

noncomputable def NavierStokes.NominalProfile.matchRadius (F : OutgoingProfile.Profile) (C : ℝ) : ℝ

Match radius, given by matchingRadius F C * matchFraction.

Equations

• NavierStokes.NominalProfile.matchRadius F C = NavierStokes.NominalProfile.matchingRadius F C * NavierStokes.NominalProfile.matchFraction

theorem NavierStokes.NominalProfile.Xi_pos : 0 < Xi

theorem NavierStokes.NominalProfile.matchingRadius_pos (F : OutgoingProfile.Profile) {C : ℝ} (hC : 0 < C) : 0 < matchingRadius F C

theorem NavierStokes.NominalProfile.matchFraction_pos : 0 < matchFraction

theorem NavierStokes.NominalProfile.matchFraction_lt_one : matchFraction < 1

theorem NavierStokes.NominalProfile.matchingRadius_tendsto (F : OutgoingProfile.Profile) : Filter.Tendsto (matchingRadius F) Filter.atTop Filter.atTop

theorem NavierStokes.NominalProfile.eventually_matching_geometry (F : OutgoingProfile.Profile) (T radiusFloor normFloor : ℝ) : ∀ᶠ (C : ℝ) in Filter.atTop, 0 < C ∧ normFloor ≤ C ∧ radiusFloor < matchingRadius F C ∧ ShapeTransition.separation T C F.data.core.P < Real.exp (-8)

Any fixed outgoing radius bound and shape-separation test can be met by the later choice of C; no outgoing parameter is reselected.

noncomputable def NavierStokes.NominalProfile.resetPatch : FiveProfileMoments.Patch

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

Equations

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

noncomputable def NavierStokes.NominalProfile.idealAmplitude (F : OutgoingProfile.Profile) (eta : ℝ) : ℝ

Ideal amplitude, given by F.data.core.P * OutgoingSchedule.shape eta.

Equations

• NavierStokes.NominalProfile.idealAmplitude F eta = F.data.core.P * NavierStokes.OutgoingSchedule.shape eta

noncomputable def NavierStokes.NominalProfile.idealU (eta : ℝ) : ℝ

Ideal U, given by 4 * eta.

Equations

• NavierStokes.NominalProfile.idealU eta = 4 * eta

noncomputable def NavierStokes.NominalProfile.idealE (F : OutgoingProfile.Profile) (p : Point) : ℝ

Ideal E, given by idealAmplitude F p.2 * p.1 ^ (1 / 10 : ℝ).

Equations

• NavierStokes.NominalProfile.idealE F p = NavierStokes.NominalProfile.idealAmplitude F p.2 * p.1 ^ (1 / 10)

theorem NavierStokes.NominalProfile.idealAmplitude_pos (F : OutgoingProfile.Profile) (eta : ℝ) : 0 < idealAmplitude F eta

theorem NavierStokes.NominalProfile.idealAmplitude_smooth (F : OutgoingProfile.Profile) : ContDiff ℝ (↑⊤) (idealAmplitude F)

theorem NavierStokes.NominalProfile.idealU_smooth : ContDiff ℝ (↑⊤) idealU

structure NavierStokes.NominalProfile.ResetSolver : Type

One normalized inverse is fixed before the prefix debt is supplied.

• solve : Coeff → Coeff

  Solve of ResetSolver, of type Coeff → Coeff.

• radius : ℝ

  Radius of ResetSolver, of type ℝ.

• bound : ℝ

  Bound of ResetSolver, of type ℝ.

• radius_pos : 0 < self.radius
• bound_pos : 0 < self.bound
• smooth : ContDiffOn ℝ (↑⊤) self.solve (Metric.ball 0 self.radius)
• at_zero : self.solve 0 = 0
• equation (q : Coeff) : q ∈ Metric.ball 0 self.radius → FiveProfileMoments.normalizedMap resetPatch (1 / 10) (self.solve q) = q
• positive (q : Coeff) : q ∈ Metric.ball 0 self.radius → ∀ (x : ℝ), 0 < x → 0 < x ^ (1 / 10) + FiveProfileMoments.e resetPatch (self.solve q) x
• norm_bound (q : Coeff) : q ∈ Metric.ball 0 self.radius → ‖self.solve q‖ ≤ self.bound * ‖q‖

theorem NavierStokes.NominalProfile.resetSolver_exists : Nonempty ResetSolver

noncomputable def NavierStokes.NominalProfile.resetSolver : ResetSolver

Reset solver, given by Classical.choice resetSolver_exists.

Equations

• NavierStokes.NominalProfile.resetSolver = Classical.choice NavierStokes.NominalProfile.resetSolver_exists

noncomputable def NavierStokes.NominalProfile.normalizedDebt (F : OutgoingProfile.Profile) (debt : ℝ → Debt) (eta : ℝ) : Coeff

Normalized debt, given by FiveProfileMoments.normalizedDebt (idealAmplitude F eta) (idealU eta) (debt eta).

Equations

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

noncomputable def NavierStokes.NominalProfile.resetCoefficients (F : OutgoingProfile.Profile) (debt : ℝ → Debt) (eta : ℝ) : Coeff

Reset coefficients, given by resetSolver.solve (normalizedDebt F debt eta).

Equations

• NavierStokes.NominalProfile.resetCoefficients F debt eta = NavierStokes.NominalProfile.resetSolver.solve (NavierStokes.NominalProfile.normalizedDebt F debt eta)

def NavierStokes.NominalProfile.SmallDebt (F : OutgoingProfile.Profile) (debt : ℝ → Debt) (eta : ℝ) : Prop

Small debt, given by ‖normalizedDebt F debt eta‖ < resetSolver.radius.

Equations

• NavierStokes.NominalProfile.SmallDebt F debt eta = (‖NavierStokes.NominalProfile.normalizedDebt F debt eta‖ < NavierStokes.NominalProfile.resetSolver.radius)

theorem NavierStokes.NominalProfile.smallDebt_mem {F : OutgoingProfile.Profile} {debt : ℝ → Debt} {eta : ℝ} (h : SmallDebt F debt eta) : normalizedDebt F debt eta ∈ Metric.ball 0 resetSolver.radius

theorem NavierStokes.NominalProfile.resetCoefficients_equation (F : OutgoingProfile.Profile) (debt : ℝ → Debt) (eta : ℝ) (hs : SmallDebt F debt eta) : FiveProfileMoments.physicalMoments resetPatch (1 / 10) (idealAmplitude F eta) (idealU eta) (resetCoefficients F debt eta) = debt eta

theorem NavierStokes.NominalProfile.resetCoefficients_smooth (F : OutgoingProfile.Profile) {debt : ℝ → Debt} {V : Set ℝ} (hd : ContDiffOn ℝ (↑⊤) debt V) (hs : ∀ eta ∈ V, SmallDebt F debt eta) : ContDiffOn ℝ (↑⊤) (resetCoefficients F debt) V

Literal row densities and compact edits

noncomputable def NavierStokes.NominalProfile.density (U E : ℝ → ℝ) (x : ℝ) : Debt

Density, given by ![U x, Real.sqrt (2 * x) * E x, U x * Real.sqrt (2 * x) * E x, U x ^ 2 - E x ^ 2 / 2, E x ^ 2 / (2 * x)].

Equations

• NavierStokes.NominalProfile.density U E x = ![U x, √(2 * x) * E x, U x * √(2 * x) * E x, U x ^ 2 - E x ^ 2 / 2, E x ^ 2 / (2 * x)]

noncomputable def NavierStokes.NominalProfile.moments (U E : Field) (r eta : ℝ) : Debt

Moments, defined pointwise by ∫ x in Ioc 0 r, density (fun x => U (x, eta)) (fun x => E (x, eta)) x i.

Equations

• NavierStokes.NominalProfile.moments U E r eta i = ∫ (x : ℝ) in Set.Ioc 0 r, NavierStokes.NominalProfile.density (fun (x : ℝ) => U (x, eta)) (fun (x : ℝ) => E (x, eta)) x i

noncomputable def NavierStokes.NominalProfile.correctedU (F : OutgoingProfile.Profile) (U : Field) (debt : ℝ → Debt) (p : Point) : ℝ

Corrected U, given by U p + idealAmplitude F p.2 * FiveProfileMoments.u resetPatch (resetCoefficients F debt p.2) p.1.

Equations

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

noncomputable def NavierStokes.NominalProfile.correctedE (F : OutgoingProfile.Profile) (E : Field) (debt : ℝ → Debt) (p : Point) : ℝ

Corrected E, given by E p + idealAmplitude F p.2 * FiveProfileMoments.e resetPatch (resetCoefficients F debt p.2) p.1.

Equations

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

theorem NavierStokes.NominalProfile.corrected_unchanged (F : OutgoingProfile.Profile) (U E : Field) (debt : ℝ → Debt) (p : Point) (hp : p.1 ∉ Set.Ioo resetPatch.left resetPatch.right) : correctedU F U debt p = U p ∧ correctedE F E debt p = E p

theorem NavierStokes.NominalProfile.density_change (U E dU dE : ℝ → ℝ) (x : ℝ) (i : Fin 5) : density (fun (t : ℝ) => U t + dU t) (fun (t : ℝ) => E t + dE t) x i = density U E x i + FiveProfileMoments.profileChangeDensity U E dU dE x i

theorem NavierStokes.NominalProfile.corrected_density (F : OutgoingProfile.Profile) (U E : Field) (debt : ℝ → Debt) (eta x : ℝ) (hU : ∀ x ∈ Set.Ioo resetPatch.left resetPatch.right, U (x, eta) = idealU eta) (hE : ∀ x ∈ Set.Ioo resetPatch.left resetPatch.right, E (x, eta) = idealE F (x, eta)) (i : Fin 5) : density (fun (t : ℝ) => correctedU F U debt (t, eta)) (fun (t : ℝ) => correctedE F E debt (t, eta)) x i = density (fun (t : ℝ) => U (t, eta)) (fun (t : ℝ) => E (t, eta)) x i + FiveProfileMoments.physicalDensity resetPatch (1 / 10) (idealAmplitude F eta) (idealU eta) (resetCoefficients F debt eta) x i

theorem NavierStokes.NominalProfile.physicalDensity_integral_prefix (F : OutgoingProfile.Profile) (debt : ℝ → Debt) (eta r : ℝ) (hr : resetPatch.right ≤ r) (i : Fin 5) : ∫ (x : ℝ) in Set.Ioc 0 r, FiveProfileMoments.physicalDensity resetPatch (1 / 10) (idealAmplitude F eta) (idealU eta) (resetCoefficients F debt eta) x i = FiveProfileMoments.physicalMoments resetPatch (1 / 10) (idealAmplitude F eta) (idealU eta) (resetCoefficients F debt eta) i

theorem NavierStokes.NominalProfile.corrected_moments (F : OutgoingProfile.Profile) (U E : Field) (debt : ℝ → Debt) (eta r : ℝ) (hr : resetPatch.right ≤ r) (hs : SmallDebt F debt eta) (hU : ∀ x ∈ Set.Ioo resetPatch.left resetPatch.right, U (x, eta) = idealU eta) (hE : ∀ x ∈ Set.Ioo resetPatch.left resetPatch.right, E (x, eta) = idealE F (x, eta)) (hint : ∀ (i : Fin 5), MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => U (t, eta)) (fun (t : ℝ) => E (t, eta)) x i) (Set.Ioc 0 r) MeasureTheory.volume) : moments (correctedU F U debt) (correctedE F E debt) r eta = moments U E r eta + debt eta

Shape restoration in the same physical radius

noncomputable def NavierStokes.NominalProfile.restoredU (XR : ℝ) (old : Field) (p : Point) : ℝ

Restored U, given by let s := ShapeTransition.radialSwitch (XR * Real.exp (-8)) 1 p.1 (1 - s) * old p + s * idealU p.2.

Equations

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

theorem NavierStokes.NominalProfile.restoredU_before {XR X : ℝ} (hXR : 0 < XR) (hX : X ≤ XR * Real.exp (-8)) (old : Field) (eta : ℝ) : restoredU XR old (X, eta) = old (X, eta)

theorem NavierStokes.NominalProfile.restoredU_scaled {XR x : ℝ} (hXR : 0 < XR) (hx : 0 < x) (old : Field) (eta : ℝ) : restoredU XR old (XR * x, eta) = (1 - OutgoingSchedule.sigma (Real.log x + 8)) * old (XR * x, eta) + OutgoingSchedule.sigma (Real.log x + 8) * idealU eta

theorem NavierStokes.NominalProfile.restoredU_after {XR x : ℝ} (hXR : 0 < XR) (hx : Real.exp (-7) ≤ x) (old : Field) (eta : ℝ) : restoredU XR old (XR * x, eta) = idealU eta

noncomputable def NavierStokes.NominalProfile.preparedE (F : OutgoingProfile.Profile) (C T : ℝ) (li : ℝ → ℝ) (oldf : Field) (p : Point) : ℝ

Prepared E, given by Real.sqrt (2 * (matchingRadius F C * p.1)) * ShapeTransition.shapeField Xi T li oldf (matchingRadius F C * p.1, p.2).

Equations

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

noncomputable def NavierStokes.NominalProfile.preparedU (F : OutgoingProfile.Profile) (C : ℝ) (oldU : Field) (p : Point) : ℝ

Prepared U, given by restoredU (matchingRadius F C) oldU (matchingRadius F C * p.1, p.2).

Equations

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

theorem NavierStokes.NominalProfile.matching_clock (F : OutgoingProfile.Profile) {C x : ℝ} (hC : 0 < C) (hx : 0 < x) : ShapeTransition.resetClock C F.data.core.P (Real.log (matchingRadius F C * x / Xi)) = Real.log x

theorem NavierStokes.NominalProfile.separation_clock (F : OutgoingProfile.Profile) {C T x : ℝ} (hC : 0 < C) (hx : ShapeTransition.separation T C F.data.core.P ≤ x) : T ≤ Real.log (matchingRadius F C * x / Xi)

theorem NavierStokes.NominalProfile.preparedE_ideal (F : OutgoingProfile.Profile) {C T x : ℝ} (hC : 0 < C) (hT : 0 < T) (hx : ShapeTransition.separation T C F.data.core.P ≤ x) (li : ℝ → ℝ) (oldf : Field) (eta : ℝ) (hold : oldf (matchingRadius F C * x, eta) = C⁻¹ * Real.exp (Real.log (matchingRadius F C * x / Xi) / 10 + li eta) / √(2 * (matchingRadius F C * x))) : preparedE F C T li oldf (x, eta) = idealE F (x, eta)

theorem NavierStokes.NominalProfile.preparedU_ideal (F : OutgoingProfile.Profile) {C x : ℝ} (hC : 0 < C) (hx : Real.exp (-7) ≤ x) (oldU : Field) (eta : ℝ) : preparedU F C oldU (x, eta) = idealU eta

Splicing and the actual five-row debt

noncomputable def NavierStokes.NominalProfile.splice (r : ℝ) (inner outer : Field) (p : Point) : ℝ

Splice, with branches according to p.1 ≤ r.

Equations

• NavierStokes.NominalProfile.splice r inner outer p = if p.1 ≤ r then inner p else outer p

theorem NavierStokes.NominalProfile.splice_inner {r : ℝ} (inner outer : Field) {p : Point} (hp : p.1 ≤ r) : splice r inner outer p = inner p

theorem NavierStokes.NominalProfile.splice_outer {r : ℝ} (inner outer : Field) {p : Point} (hp : r < p.1) : splice r inner outer p = outer p

noncomputable def NavierStokes.NominalProfile.baseU (F : OutgoingProfile.Profile) (C : ℝ) (oldU : Field) : Field

Base U, given by splice matchFraction (preparedU F C oldU) F.U.

Equations

• NavierStokes.NominalProfile.baseU F C oldU = NavierStokes.NominalProfile.splice NavierStokes.NominalProfile.matchFraction (NavierStokes.NominalProfile.preparedU F C oldU) F.U

noncomputable def NavierStokes.NominalProfile.baseE (F : OutgoingProfile.Profile) (C T : ℝ) (li : ℝ → ℝ) (oldf : Field) : Field

Base E, given by splice matchFraction (preparedE F C T li oldf) F.E.

Equations

• NavierStokes.NominalProfile.baseE F C T li oldf = NavierStokes.NominalProfile.splice NavierStokes.NominalProfile.matchFraction (NavierStokes.NominalProfile.preparedE F C T li oldf) F.E

noncomputable def NavierStokes.NominalProfile.actualDebt (F : OutgoingProfile.Profile) (C T : ℝ) (li : ℝ → ℝ) (oldf oldU : Field) (eta : ℝ) : Debt

This is the literal discrepancy of the five histories at the join.

Equations

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

noncomputable def NavierStokes.NominalProfile.joinedU (F : OutgoingProfile.Profile) (C T : ℝ) (li : ℝ → ℝ) (oldf oldU : Field) : Field

Joined U, given by correctedU F (baseU F C oldU) (actualDebt F C T li oldf oldU).

Equations

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

noncomputable def NavierStokes.NominalProfile.joinedE (F : OutgoingProfile.Profile) (C T : ℝ) (li : ℝ → ℝ) (oldf oldU : Field) : Field

Joined E, given by correctedE F (baseE F C T li oldf) (actualDebt F C T li oldf oldU).

Equations

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

theorem NavierStokes.NominalProfile.baseU_ideal (F : OutgoingProfile.Profile) {C x : ℝ} (hC : 0 < C) (hx : x ∈ Set.Ioo resetPatch.left resetPatch.right) (oldU : Field) (eta : ℝ) : baseU F C oldU (x, eta) = idealU eta

theorem NavierStokes.NominalProfile.baseE_ideal (F : OutgoingProfile.Profile) {C T : ℝ} (hC : 0 < C) (hT : 0 < T) (hsep : ShapeTransition.separation T C F.data.core.P ≤ Real.exp (-8)) (li : ℝ → ℝ) (oldf : Field) (eta : ℝ) (hold : ∀ x ∈ Set.Ioo resetPatch.left resetPatch.right, oldf (matchingRadius F C * x, eta) = C⁻¹ * Real.exp (Real.log (matchingRadius F C * x / Xi) / 10 + li eta) / √(2 * (matchingRadius F C * x))) (x : ℝ) : x ∈ Set.Ioo resetPatch.left resetPatch.right → baseE F C T li oldf (x, eta) = idealE F (x, eta)

theorem NavierStokes.NominalProfile.joined_moments_at_match (F : OutgoingProfile.Profile) {C T : ℝ} (hC : 0 < C) (hT : 0 < T) (hsep : ShapeTransition.separation T C F.data.core.P ≤ Real.exp (-8)) (li : ℝ → ℝ) (oldf oldU : Field) (eta : ℝ) (hs : SmallDebt F (actualDebt F C T li oldf oldU) eta) (hold : ∀ x ∈ Set.Ioo resetPatch.left resetPatch.right, oldf (matchingRadius F C * x, eta) = C⁻¹ * Real.exp (Real.log (matchingRadius F C * x / Xi) / 10 + li eta) / √(2 * (matchingRadius F C * x))) (hint : ∀ (i : Fin 5), MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => baseU F C oldU (t, eta)) (fun (t : ℝ) => baseE F C T li oldf (t, eta)) x i) (Set.Ioc 0 matchFraction) MeasureTheory.volume) : moments (joinedU F C T li oldf oldU) (joinedE F C T li oldf oldU) matchFraction eta = moments F.U F.E matchFraction eta

theorem NavierStokes.NominalProfile.joined_after_match (F : OutgoingProfile.Profile) (C T : ℝ) (li : ℝ → ℝ) (oldf oldU : Field) {p : Point} (hp : matchFraction < p.1) : joinedU F C T li oldf oldU p = F.U p ∧ joinedE F C T li oldf oldU p = F.E p

theorem NavierStokes.NominalProfile.prefix_integral_propagate {f g : ℝ → ℝ} {a r : ℝ} (har : a ≤ r) (hf : MeasureTheory.IntegrableOn f (Set.Ioc 0 r) MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g (Set.Ioc 0 r) MeasureTheory.volume) (head : ∫ (x : ℝ) in Set.Ioc 0 a, f x = ∫ (x : ℝ) in Set.Ioc 0 a, g x) (tail : ∀ (x : ℝ), a < x → f x = g x) : ∫ (x : ℝ) in Set.Ioc 0 r, f x = ∫ (x : ℝ) in Set.Ioc 0 r, g x

Equality of one prefix integral propagates along an identical exterior.

theorem NavierStokes.NominalProfile.moments_propagate {U E V G : Field} {a r eta : ℝ} (har : a ≤ r) (hU : ∀ (i : Fin 5), MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => U (t, eta)) (fun (t : ℝ) => E (t, eta)) x i) (Set.Ioc 0 r) MeasureTheory.volume) (hV : ∀ (i : Fin 5), MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => V (t, eta)) (fun (t : ℝ) => G (t, eta)) x i) (Set.Ioc 0 r) MeasureTheory.volume) (head : moments U E a eta = moments V G a eta) (tail : ∀ (x : ℝ), a < x → U (x, eta) = V (x, eta) ∧ E (x, eta) = G (x, eta)) : moments U E r eta = moments V G r eta

theorem NavierStokes.NominalProfile.corrected_density_integrable (F : OutgoingProfile.Profile) (U E : Field) (debt : ℝ → Debt) (eta r : ℝ) (hU : ∀ x ∈ Set.Ioo resetPatch.left resetPatch.right, U (x, eta) = idealU eta) (hE : ∀ x ∈ Set.Ioo resetPatch.left resetPatch.right, E (x, eta) = idealE F (x, eta)) (hint : ∀ (i : Fin 5), MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => U (t, eta)) (fun (t : ℝ) => E (t, eta)) x i) (Set.Ioc 0 r) MeasureTheory.volume) (i : Fin 5) : MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => correctedU F U debt (t, eta)) (fun (t : ℝ) => correctedE F E debt (t, eta)) x i) (Set.Ioc 0 r) MeasureTheory.volume

theorem NavierStokes.NominalProfile.joined_moments (F : OutgoingProfile.Profile) {C T r : ℝ} (hC : 0 < C) (hT : 0 < T) (hr : matchFraction ≤ r) (hsep : ShapeTransition.separation T C F.data.core.P ≤ Real.exp (-8)) (li : ℝ → ℝ) (oldf oldU : Field) (eta : ℝ) (hs : SmallDebt F (actualDebt F C T li oldf oldU) eta) (hold : ∀ x ∈ Set.Ioo resetPatch.left resetPatch.right, oldf (matchingRadius F C * x, eta) = C⁻¹ * Real.exp (Real.log (matchingRadius F C * x / Xi) / 10 + li eta) / √(2 * (matchingRadius F C * x))) (hint : ∀ (i : Fin 5), MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => baseU F C oldU (t, eta)) (fun (t : ℝ) => baseE F C T li oldf (t, eta)) x i) (Set.Ioc 0 r) MeasureTheory.volume) (hout : ∀ (i : Fin 5), MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => F.U (t, eta)) (fun (t : ℝ) => F.E (t, eta)) x i) (Set.Ioc 0 r) MeasureTheory.volume) : moments (joinedU F C T li oldf oldU) (joinedE F C T li oldf oldU) r eta = moments F.U F.E r eta

theorem NavierStokes.NominalProfile.joined_before_patch (F : OutgoingProfile.Profile) (C T : ℝ) (li : ℝ → ℝ) (oldf oldU : Field) {p : Point} (hp : p.1 ≤ resetPatch.left) : joinedU F C T li oldf oldU p = preparedU F C oldU p ∧ joinedE F C T li oldf oldU p = preparedE F C T li oldf p

A concrete continuation of this axis witness

structure NavierStokes.NominalProfile.Controls {F : OutgoingProfile.Profile} (A : AxisStage F) : Type

These are only scalar clock choices. No cone inequality or moment compatibility is included in the data.

• referenceWidth : ℝ

  Reference width of Controls, of type ℝ.

• referenceWidth_pos : 0 < self.referenceWidth
• referenceWidth_small : 2 * self.referenceWidth < ReferencePath.rampLimit
• activationTime : ℝ

  Activation time of Controls, of type ℝ.

• activationTime_pos : 0 < self.activationTime
• activationTime_le : self.activationTime ≤ self.referenceWidth
• kappa : ℝ

  Kappa of Controls, of type ℝ.

• kappa_pos : 0 < self.kappa
• kappa_le_one : self.kappa ≤ 1
• axialWidth : ℝ

  Axial width of Controls, of type ℝ.

• axialWidth_pos : 0 < self.axialWidth
• angularWidth : ℝ

  Angular width of Controls, of type ℝ.

• angularWidth_pos : 0 < self.angularWidth
• before_big : self.referenceWidth ≤ (A.activation self.referenceWidth ⋯ ⋯).bigTime
• finish : (A.activation self.referenceWidth ⋯ ⋯).bigTime + self.axialWidth + self.angularWidth ≤ (A.activation self.referenceWidth ⋯ ⋯).finalTime
• shapeTime : ℝ

  Shape time of Controls, of type ℝ.

• shapeTime_pos : 0 < self.shapeTime

noncomputable def NavierStokes.NominalProfile.Controls.reference {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : TransitionRamp.StockReference ReferencePath.parameterInterval

Reference, given by A.activation c.referenceWidth c.referenceWidth_pos c.referenceWidth_small.

Equations

• c.reference = A.activation c.referenceWidth ⋯ ⋯

noncomputable def NavierStokes.NominalProfile.Controls.seedF {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : Field

Seed F, given by c.reference.physicalF c.activationTime c.kappa c.axialWidth c.angularWidth.

Equations

• c.seedF = c.reference.physicalF c.activationTime c.kappa c.axialWidth c.angularWidth

noncomputable def NavierStokes.NominalProfile.Controls.seedU {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : Field

Seed U, given by c.reference.physicalU c.activationTime c.kappa c.axialWidth.

Equations

• c.seedU = c.reference.physicalU c.activationTime c.kappa c.axialWidth

noncomputable def NavierStokes.NominalProfile.Controls.initialShape {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ℝ → ℝ

Initial shape, given by c.reference.endpointLog c.activationTime c.kappa c.axialWidth c.angularWidth A.normalization.

Equations

• c.initialShape = c.reference.endpointLog c.activationTime c.kappa c.axialWidth c.angularWidth A.normalization

noncomputable def NavierStokes.NominalProfile.Controls.initialAxial {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ℝ → ℝ

Initial axial, given by c.reference.endpointU c.activationTime c.kappa c.axialWidth.

Equations

• c.initialAxial = c.reference.endpointU c.activationTime c.kappa c.axialWidth

theorem NavierStokes.NominalProfile.Controls.reference_radius {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : c.reference.radius0 = 4 / A.scale

theorem NavierStokes.NominalProfile.Controls.reference_profiles {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : c.reference.profiles = A.reference c.referenceWidth ⋯ ⋯

theorem NavierStokes.NominalProfile.Controls.reference_pressure {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : c.reference.profiles.pressure0 = F.axisDatum

theorem NavierStokes.NominalProfile.Controls.reference_before_big {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : 0 < c.reference.bigTime

theorem NavierStokes.NominalProfile.Controls.radius_before_Xi {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : c.reference.radius0 < 110

theorem NavierStokes.NominalProfile.Controls.seedF_smooth {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ContDiffOn ℝ (↑⊤) c.seedF A.referenceInput.radialDomain.carrier

theorem NavierStokes.NominalProfile.Controls.seedU_smooth {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ContDiffOn ℝ (↑⊤) c.seedU A.referenceInput.radialDomain.carrier

theorem NavierStokes.NominalProfile.Controls.seedF_positive {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {p : Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hX : 0 ≤ p.1) : 0 < c.seedF p

theorem NavierStokes.NominalProfile.Controls.seed_initial {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {p : Point} (hp : p.1 ≤ 4 / A.scale) : c.seedF p = A.natural.profile.family.f p ∧ c.seedU p = A.natural.profile.family.U p

theorem NavierStokes.NominalProfile.Controls.seed_activation {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {p : Point} (hη : p.2 ∈ ReferencePath.parameterInterval) (hp : p.1 ≤ 4 / A.scale * Real.exp c.referenceWidth) : c.seedF p = StressActivation.FromReference.f A.referenceInput c.activationTime c.kappa c.referenceWidth p ∧ c.seedU p = StressActivation.FromReference.U A.referenceInput c.activationTime c.kappa c.referenceWidth p

theorem NavierStokes.NominalProfile.Controls.initialShape_smooth {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ContDiffOn ℝ (↑⊤) c.initialShape ReferencePath.parameterInterval

theorem NavierStokes.NominalProfile.Controls.initialAxial_smooth {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ContDiffOn ℝ (↑⊤) c.initialAxial ReferencePath.parameterInterval

theorem NavierStokes.NominalProfile.Controls.seedF_held {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {X eta : ℝ} (hX : Xi ≤ X) (hη : eta ∈ ReferencePath.parameterInterval) : c.seedF (X, eta) = A.normalization⁻¹ * Real.exp (Real.log (X / Xi) / 10 + c.initialShape eta) / √(2 * X)

theorem NavierStokes.NominalProfile.Controls.seedU_held {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {X eta : ℝ} (hX : Xi ≤ X) (hη : eta ∈ ReferencePath.parameterInterval) : c.seedU (X, eta) = c.initialAxial eta

theorem NavierStokes.NominalProfile.Controls.initialShape_value {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {eta : ℝ} (hη : eta ∈ ReferencePath.parameterInterval) : c.initialShape eta = Real.log (A.normalization * (√(2 * Xi) * c.seedF (Xi, eta)))

noncomputable def NavierStokes.NominalProfile.Controls.debt {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ℝ → Debt

The nominal fields are functions of the actual stock-controlled seed.

Equations

• c.debt = NavierStokes.NominalProfile.actualDebt F A.normalization c.shapeTime c.initialShape c.seedF c.seedU

noncomputable def NavierStokes.NominalProfile.Controls.normalizedE {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : Field

Normalized E, given by joinedE F A.normalization c.shapeTime c.initialShape c.seedF c.seedU.

Equations

• c.normalizedE = NavierStokes.NominalProfile.joinedE F A.normalization c.shapeTime c.initialShape c.seedF c.seedU

noncomputable def NavierStokes.NominalProfile.Controls.normalizedU {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : Field

Normalized U, given by joinedU F A.normalization c.shapeTime c.initialShape c.seedF c.seedU.

Equations

• c.normalizedU = NavierStokes.NominalProfile.joinedU F A.normalization c.shapeTime c.initialShape c.seedF c.seedU

noncomputable def NavierStokes.NominalProfile.Controls.radius {F : OutgoingProfile.Profile} {A : AxisStage F} (_c : Controls A) : ℝ

Radius, given by matchingRadius F A.normalization.

Equations

• _c.radius = NavierStokes.NominalProfile.matchingRadius F A.normalization

noncomputable def NavierStokes.NominalProfile.Controls.E {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (p : Point) : ℝ

E, given by c.normalizedE (p.1 / c.radius, p.2).

Equations

• c.E p = c.normalizedE (p.1 / c.radius, p.2)

noncomputable def NavierStokes.NominalProfile.Controls.U {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (p : Point) : ℝ

U, given by c.normalizedU (p.1 / c.radius, p.2).

Equations

• c.U p = c.normalizedU (p.1 / c.radius, p.2)

noncomputable def NavierStokes.NominalProfile.Controls.H {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (p : Point) : ℝ

H, given by Real.sqrt (2 * p.1) * c.E p.

Equations

• c.H p = √(2 * p.1) * c.E p

noncomputable def NavierStokes.NominalProfile.Controls.Pi {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (p : Point) : ℝ

Pi, given by F.axisDatum p.2 + moments c.U c.E p.1 p.2 4.

Equations

• c.Pi p = F.axisDatum p.2 + NavierStokes.NominalProfile.moments c.U c.E p.1 p.2 4

theorem NavierStokes.NominalProfile.Controls.radius_pos {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : 0 < c.radius

theorem NavierStokes.NominalProfile.Controls.normalized_after_match {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {p : Point} (hp : matchFraction < p.1) : c.normalizedU p = F.U p ∧ c.normalizedE p = F.E p

theorem NavierStokes.NominalProfile.Controls.physical_after_match {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {p : Point} (hp : c.radius * matchFraction < p.1) : c.U p = OutgoingDilation.U F c.radius p ∧ c.E p = OutgoingDilation.E F c.radius p

theorem NavierStokes.NominalProfile.Controls.shape_clock_after_Xi {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {x : ℝ} (hx : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ x) : Xi ≤ c.radius * x

theorem NavierStokes.NominalProfile.Controls.held_on_patch {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {eta : ℝ} (hη : eta ∈ ReferencePath.parameterInterval) (x : ℝ) : x ∈ Set.Ioo resetPatch.left resetPatch.right → c.seedF (c.radius * x, eta) = A.normalization⁻¹ * Real.exp (Real.log (c.radius * x / Xi) / 10 + c.initialShape eta) / √(2 * (c.radius * x))

theorem NavierStokes.NominalProfile.Controls.physical_before_Xi {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {p : Point} (hp : p.1 ≤ Xi) : c.U p = c.seedU p ∧ c.E p = √(2 * p.1) * c.seedF p

noncomputable def NavierStokes.NominalProfile.Controls.f {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (p : Point) : ℝ

F, with branches according to p.1 ≤ Xi.

Equations

• c.f p = if p.1 ≤ NavierStokes.NominalProfile.Xi then c.seedF p else c.E p / √(2 * p.1)

theorem NavierStokes.NominalProfile.Controls.f_before_Xi {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {p : Point} (hp : p.1 ≤ Xi) : c.f p = c.seedF p

theorem NavierStokes.NominalProfile.Controls.E_eq_sqrt_mul_f {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {p : Point} (hX : 0 < p.1) : c.E p = √(2 * p.1) * c.f p

theorem NavierStokes.NominalProfile.Controls.natural_prefix {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) (hscale : 1 ≤ A.scale) {p : Point} (hp : p.1 ≤ 4 / A.scale) : c.f p = A.natural.profile.family.f p ∧ c.U p = A.natural.profile.family.U p

theorem NavierStokes.NominalProfile.controls_exist {F : OutgoingProfile.Profile} (A : AxisStage F) (hscale : 1 ≤ A.scale) (T : ℝ) (hT : 0 < T) {eps : ℝ} (heps : 0 < eps) : ∃ (c : Controls A), c.shapeTime = T ∧ c.referenceWidth < eps ∧ c.activationTime < eps ∧ c.kappa < eps ∧ c.axialWidth < eps ∧ c.angularWidth < eps

All elementary clock constraints can be achieved with arbitrarily small widths after the axis profile and its normalization have been fixed.

Regular parameter-dependent prefix integrals

noncomputable def NavierStokes.NominalProfile.scaledDomain (D : ProfileHistories.RadialDomain) (R : ℝ) : ProfileHistories.RadialDomain

Scaled domain, bundling carrier, isOpen, scale_mem, have.

Equations

• NavierStokes.NominalProfile.scaledDomain D R = { carrier := {p : NavierStokes.ProfileHistories.Point | (R * p.1, p.2) ∈ D.carrier}, isOpen := ⋯, scale_mem := ⋯ }

noncomputable def NavierStokes.NominalProfile.regularDensity {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : Point) : Debt

Regular density, given by ![P.U p, P.H p, P.transportDensity p, P.energyDensity p, P.f p ^ 2].

Equations

• NavierStokes.NominalProfile.regularDensity P p = ![P.U p, P.H p, P.transportDensity p, P.energyDensity p, P.f p ^ 2]

theorem NavierStokes.NominalProfile.regularDensity_smooth {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (i : Fin 5) : ContDiffOn ℝ (↑⊤) (fun (p : Point) => regularDensity P p i) D.carrier

theorem NavierStokes.NominalProfile.regularDensity_eq {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {x : ℝ} (hx : 0 < x) (eta : ℝ) : density (fun (t : ℝ) => P.U (t, eta)) (fun (t : ℝ) => P.E (t, eta)) x = regularDensity P (x, eta)

theorem NavierStokes.NominalProfile.regularDensity_integrable {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {r eta : ℝ} (hp : (r, eta) ∈ D.carrier) (i : Fin 5) : MeasureTheory.IntegrableOn (fun (x : ℝ) => regularDensity P (x, eta) i) (Set.Ioc 0 r) MeasureTheory.volume

noncomputable def NavierStokes.NominalProfile.Controls.shapedF {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : Field

Shaped F, given by ShapeTransition.shapeField Xi c.shapeTime c.initialShape c.seedF.

Equations

• c.shapedF = NavierStokes.ShapeTransition.shapeField NavierStokes.NominalProfile.Xi c.shapeTime c.initialShape c.seedF

theorem NavierStokes.NominalProfile.Controls.shapedF_smooth {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ContDiffOn ℝ (↑⊤) c.shapedF A.referenceInput.radialDomain.carrier

theorem NavierStokes.NominalProfile.Controls.restored_seed_smooth {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ContDiffOn ℝ (↑⊤) (restoredU c.radius c.seedU) A.referenceInput.radialDomain.carrier

noncomputable def NavierStokes.NominalProfile.Controls.preparedDomain {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ProfileHistories.RadialDomain

Prepared domain, given by scaledDomain A.referenceInput.radialDomain c.radius.

Equations

• c.preparedDomain = NavierStokes.NominalProfile.scaledDomain A.referenceInput.radialDomain c.radius

theorem NavierStokes.NominalProfile.Controls.preparedDomain_nonnegative {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {p : Point} (hX : 0 ≤ p.1) (hη : p.2 ∈ ReferencePath.parameterInterval) : p ∈ c.preparedDomain.carrier

noncomputable def NavierStokes.NominalProfile.Controls.preparedProfiles {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ProfileHistories.Profiles c.preparedDomain

Prepared profiles, bundling f, U, f_smooth, U_smooth and the required compatibility proofs.

Equations

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

theorem NavierStokes.NominalProfile.Controls.preparedProfiles_U {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (p : Point) : c.preparedProfiles.U p = preparedU F A.normalization c.seedU p

theorem NavierStokes.NominalProfile.Controls.preparedProfiles_E {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {p : Point} (hX : 0 < p.1) : c.preparedProfiles.E p = preparedE F A.normalization c.shapeTime c.initialShape c.seedF p

theorem NavierStokes.NominalProfile.Controls.base_density_before {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {x : ℝ} (hx : x ∈ Set.Ioc 0 matchFraction) (eta : ℝ) : density (fun (t : ℝ) => baseU F A.normalization c.seedU (t, eta)) (fun (t : ℝ) => baseE F A.normalization c.shapeTime c.initialShape c.seedF (t, eta)) x = regularDensity c.preparedProfiles (x, eta)

theorem NavierStokes.NominalProfile.Controls.base_density_integrable_before {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {eta : ℝ} (hη : eta ∈ ReferencePath.parameterInterval) (i : Fin 5) : MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => baseU F A.normalization c.seedU (t, eta)) (fun (t : ℝ) => baseE F A.normalization c.shapeTime c.initialShape c.seedF (t, eta)) x i) (Set.Ioc 0 matchFraction) MeasureTheory.volume

theorem NavierStokes.NominalProfile.Controls.base_moments_before {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (eta : ℝ) : moments (baseU F A.normalization c.seedU) (baseE F A.normalization c.shapeTime c.initialShape c.seedF) matchFraction eta = fun (i : Fin 5) => ProfileHistories.primitive (fun (p : ProfileHistories.Point) => regularDensity c.preparedProfiles p i) (matchFraction, eta)

theorem NavierStokes.NominalProfile.Controls.base_moments_smooth {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ContDiffOn ℝ (↑⊤) (fun (eta : ℝ) => moments (baseU F A.normalization c.seedU) (baseE F A.normalization c.shapeTime c.initialShape c.seedF) matchFraction eta) ReferencePath.parameterInterval

noncomputable def NavierStokes.NominalProfile.idealPrefixRows (F : OutgoingProfile.Profile) (r eta : ℝ) : Debt

Ideal prefix rows as an element of Debt.

Equations

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

theorem NavierStokes.NominalProfile.outgoing_moments_ideal (F : OutgoingProfile.Profile) {r : ℝ} (hr : r ≤ 1) (eta : ℝ) : moments F.U F.E r eta = idealPrefixRows F r eta

theorem NavierStokes.NominalProfile.outgoing_prefix_smooth (F : OutgoingProfile.Profile) {r : ℝ} (hr : r ≤ 1) : ContDiff ℝ ↑⊤ fun (eta : ℝ) => moments F.U F.E r eta

theorem NavierStokes.NominalProfile.Controls.debt_smooth {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ContDiffOn ℝ (↑⊤) c.debt ReferencePath.parameterInterval

theorem NavierStokes.NominalProfile.Controls.repair_coefficients_smooth {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hs : ∀ eta ∈ ReferencePath.parameterInterval, SmallDebt F c.debt eta) : ContDiffOn ℝ (↑⊤) (resetCoefficients F c.debt) ReferencePath.parameterInterval

theorem NavierStokes.NominalProfile.Controls.moments_at_match {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {eta : ℝ} (hη : eta ∈ ReferencePath.parameterInterval) (hs : SmallDebt F c.debt eta) : moments c.normalizedU c.normalizedE matchFraction eta = moments F.U F.E matchFraction eta

Smooth gluing on a genuine overlap

theorem NavierStokes.NominalProfile.splice_smoothOn {V : Set Point} (hV : IsOpen V) {r b : ℝ} (hr : 0 < r) (hrb : r < b) {inner outer : Field} (hi : ContDiffOn ℝ (↑⊤) inner V) (ho : ContDiffOn ℝ (↑⊤) outer (V ∩ {p : Point | 0 < p.1})) (he : ∀ p ∈ V, r < p.1 → p.1 < b → inner p = outer p) : ContDiffOn ℝ (↑⊤) (splice r inner outer) V

theorem NavierStokes.NominalProfile.Controls.prepared_overlap {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {x eta : ℝ} (hx : matchFraction ≤ x) (hx1 : x ≤ 1) (hη : eta ∈ ReferencePath.parameterInterval) : c.preparedProfiles.U (x, eta) = F.U (x, eta) ∧ c.preparedProfiles.E (x, eta) = F.E (x, eta)

noncomputable def NavierStokes.NominalProfile.Controls.baseRegularF {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : Field

Base regular F, given by splice matchFraction c.preparedProfiles.f (fun p => F.E p / Real.sqrt (2 * p.1)).

Equations

• c.baseRegularF = NavierStokes.NominalProfile.splice NavierStokes.NominalProfile.matchFraction c.preparedProfiles.f fun (p : NavierStokes.NominalProfile.Point) => F.E p / √(2 * p.1)

theorem NavierStokes.NominalProfile.Controls.baseRegularF_smooth {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) : ContDiffOn ℝ (↑⊤) c.baseRegularF c.preparedDomain.carrier

theorem NavierStokes.NominalProfile.Controls.baseU_smooth {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) : ContDiffOn ℝ (↑⊤) (baseU F A.normalization c.seedU) c.preparedDomain.carrier

noncomputable def NavierStokes.NominalProfile.Controls.baseProfiles {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) : ProfileHistories.Profiles c.preparedDomain

Base profiles, bundling f, U, f_smooth, U_smooth and the required compatibility proofs.

Equations

• c.baseProfiles hsep = { f := c.baseRegularF, U := NavierStokes.NominalProfile.baseU F A.normalization c.seedU, f_smooth := ⋯, U_smooth := ⋯, pressure0 := F.axisDatum, pressure0_smooth := ⋯ }

theorem NavierStokes.NominalProfile.Controls.baseProfiles_E {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {p : Point} (hX : 0 < p.1) : (c.baseProfiles hsep).E p = baseE F A.normalization c.shapeTime c.initialShape c.seedF p

theorem NavierStokes.NominalProfile.Controls.base_density_eq {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {x : ℝ} (hx : 0 < x) (eta : ℝ) : density (fun (t : ℝ) => baseU F A.normalization c.seedU (t, eta)) (fun (t : ℝ) => baseE F A.normalization c.shapeTime c.initialShape c.seedF (t, eta)) x = regularDensity (c.baseProfiles hsep) (x, eta)

theorem NavierStokes.NominalProfile.Controls.base_density_integrable {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {r eta : ℝ} (hr : 0 ≤ r) (hη : eta ∈ ReferencePath.parameterInterval) (i : Fin 5) : MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => baseU F A.normalization c.seedU (t, eta)) (fun (t : ℝ) => baseE F A.normalization c.shapeTime c.initialShape c.seedF (t, eta)) x i) (Set.Ioc 0 r) MeasureTheory.volume

theorem NavierStokes.NominalProfile.Controls.baseE_smoothAt {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {p : Point} (hX : 0 < p.1) (hη : p.2 ∈ ReferencePath.parameterInterval) : ContDiffAt ℝ (↑⊤) (baseE F A.normalization c.shapeTime c.initialShape c.seedF) p

theorem NavierStokes.NominalProfile.Controls.coefficients_smoothAt {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {eta : ℝ} (hη : eta ∈ ReferencePath.parameterInterval) (hs : SmallDebt F c.debt eta) : ContDiffAt ℝ (↑⊤) (resetCoefficients F c.debt) eta

theorem NavierStokes.NominalProfile.correction_smoothAt {n : ℕ} (P : FiveProfileMoments.Patch) {coef : ℝ → Fin n → ℝ} {p : Point} (hc : ContDiffAt ℝ (↑⊤) coef p.2) : ContDiffAt ℝ (↑⊤) (fun (q : Point) => FiveProfileMoments.correction P (coef q.2) q.1) p

theorem NavierStokes.NominalProfile.Controls.normalizedU_smoothAt {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {p : Point} (hp : p ∈ c.preparedDomain.carrier) (hs : SmallDebt F c.debt p.2) : ContDiffAt ℝ (↑⊤) c.normalizedU p

theorem NavierStokes.NominalProfile.Controls.normalizedE_smoothAt {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {p : Point} (hX : 0 < p.1) (hη : p.2 ∈ ReferencePath.parameterInterval) (hs : SmallDebt F c.debt p.2) : ContDiffAt ℝ (↑⊤) c.normalizedE p

theorem NavierStokes.NominalProfile.Controls.U_smoothAt {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {p : Point} (hp : p ∈ A.referenceInput.radialDomain.carrier) (hs : SmallDebt F c.debt p.2) : ContDiffAt ℝ (↑⊤) c.U p

theorem NavierStokes.NominalProfile.Controls.E_smoothAt {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {p : Point} (hX : 0 < p.1) (hη : p.2 ∈ ReferencePath.parameterInterval) (hs : SmallDebt F c.debt p.2) : ContDiffAt ℝ (↑⊤) c.E p

theorem NavierStokes.NominalProfile.Controls.f_smoothAt {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {p : Point} (hp : p ∈ A.referenceInput.radialDomain.carrier) (hs : SmallDebt F c.debt p.2) : ContDiffAt ℝ (↑⊤) c.f p

theorem NavierStokes.NominalProfile.Controls.preparedE_positive {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {p : Point} (hX : 0 < p.1) (hη : p.2 ∈ ReferencePath.parameterInterval) : 0 < preparedE F A.normalization c.shapeTime c.initialShape c.seedF p

theorem NavierStokes.NominalProfile.Controls.normalizedE_positive {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {p : Point} (hX : 0 < p.1) (hη : p.2 ∈ ReferencePath.parameterInterval) (hs : SmallDebt F c.debt p.2) : 0 < c.normalizedE p

theorem NavierStokes.NominalProfile.Controls.E_positive {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {p : Point} (hX : 0 < p.1) (hη : p.2 ∈ ReferencePath.parameterInterval) (hs : SmallDebt F c.debt p.2) : 0 < c.E p

theorem NavierStokes.NominalProfile.outgoing_H_integrable_prefix (F : OutgoingProfile.Profile) (eta r : ℝ) : MeasureTheory.IntegrableOn (fun (x : ℝ) => F.H (x, eta)) (Set.Ioc 0 r) MeasureTheory.volume

theorem NavierStokes.NominalProfile.outgoing_density_integrable (F : OutgoingProfile.Profile) (eta r : ℝ) (i : Fin 5) : MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => F.U (t, eta)) (fun (t : ℝ) => F.E (t, eta)) x i) (Set.Ioc 0 r) MeasureTheory.volume

noncomputable def NavierStokes.NominalProfile.dilateField (R : ℝ) (f : Field) (p : Point) : ℝ

Dilate field, given by f (p.1 / R, p.2).

Equations

• NavierStokes.NominalProfile.dilateField R f p = f (p.1 / R, p.2)

noncomputable def NavierStokes.NominalProfile.dilationFactor (R : ℝ) : Debt

Dilation factor, given by ![R, R * Real.sqrt R, R * Real.sqrt R, R, 1].

Equations

• NavierStokes.NominalProfile.dilationFactor R = ![R, R * √R, R * √R, R, 1]

theorem NavierStokes.NominalProfile.density_dilate (R : ℝ) (hR : 0 < R) (U E : Field) (eta : ℝ) {x : ℝ} (hx : 0 < x) (i : Fin 5) : R * density (fun (t : ℝ) => dilateField R U (t, eta)) (fun (t : ℝ) => dilateField R E (t, eta)) (R * x) i = dilationFactor R i * density (fun (t : ℝ) => U (t, eta)) (fun (t : ℝ) => E (t, eta)) x i

theorem NavierStokes.NominalProfile.moments_dilate (R : ℝ) (hR : 0 < R) (U E : Field) (X eta : ℝ) : moments (dilateField R U) (dilateField R E) X eta = fun (i : Fin 5) => dilationFactor R i * moments U E (X / R) eta i

theorem NavierStokes.NominalProfile.Controls.normalized_moments {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {r eta : ℝ} (hr : matchFraction ≤ r) (hη : eta ∈ ReferencePath.parameterInterval) (hs : SmallDebt F c.debt eta) : moments c.normalizedU c.normalizedE r eta = moments F.U F.E r eta

theorem NavierStokes.NominalProfile.Controls.physical_moments {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {X eta : ℝ} (hX : c.radius * matchFraction ≤ X) (hη : eta ∈ ReferencePath.parameterInterval) (hs : SmallDebt F c.debt eta) : moments c.U c.E X eta = moments (OutgoingDilation.U F c.radius) (OutgoingDilation.E F c.radius) X eta

theorem NavierStokes.NominalProfile.Controls.physical_mass_after {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : ShapeTransition.separation c.shapeTime A.normalization F.data.core.P ≤ Real.exp (-8)) {X eta : ℝ} (hX : c.radius * matchFraction ≤ X) (hη : eta ∈ ReferencePath.parameterInterval) (hs : SmallDebt F c.debt eta) : ∫ (x : ℝ) in Set.Ioc 0 X, c.U (x, eta) = OutgoingDilation.M F c.radius eta X

theorem NavierStokes.NominalProfile.prefix_integral_split {f : ℝ → ℝ} {r b : ℝ} (hr : 0 ≤ r) (hrb : r ≤ b) (hf : MeasureTheory.IntegrableOn f (Set.Ioc 0 b) MeasureTheory.volume) : ∫ (x : ℝ) in Set.Ioc 0 b, f x = (∫ (x : ℝ) in Set.Ioc 0 r, f x) + ∫ (x : ℝ) in Set.Ioc r b, f x

theorem NavierStokes.NominalProfile.moment_difference_split (U E V G : Field) (eta : ℝ) {r b : ℝ} (hr : 0 ≤ r) (hrb : r ≤ b) (hU : ∀ (i : Fin 5), MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => U (t, eta)) (fun (t : ℝ) => E (t, eta)) x i) (Set.Ioc 0 b) MeasureTheory.volume) (hV : ∀ (i : Fin 5), MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => V (t, eta)) (fun (t : ℝ) => G (t, eta)) x i) (Set.Ioc 0 b) MeasureTheory.volume) : moments U E b eta - moments V G b eta = moments U E r eta - moments V G r eta + fun (i : Fin 5) => ∫ (x : ℝ) in Set.Ioc r b, density (fun (t : ℝ) => U (t, eta)) (fun (t : ℝ) => E (t, eta)) x i - density (fun (t : ℝ) => V (t, eta)) (fun (t : ℝ) => G (t, eta)) x i

noncomputable def NavierStokes.NominalProfile.manuscriptIdealRows (F : OutgoingProfile.Profile) (r eta : ℝ) : Debt

Manuscript ideal rows as an element of Debt.

Equations

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

theorem NavierStokes.NominalProfile.ideal_rows_moments (F : OutgoingProfile.Profile) {r : ℝ} (hr : 0 ≤ r) (eta : ℝ) : moments (fun (p : Point) => idealU p.2) (idealE F) r eta = manuscriptIdealRows F r eta

theorem NavierStokes.NominalProfile.outgoing_manuscript_rows (F : OutgoingProfile.Profile) {r : ℝ} (hr : 0 ≤ r) (hr1 : r ≤ 1) (eta : ℝ) : moments F.U F.E r eta = manuscriptIdealRows F r eta

noncomputable def NavierStokes.NominalProfile.Controls.separation {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ℝ

Separation, given by ShapeTransition.separation c.shapeTime A.normalization F.data.core.P.

Equations

• c.separation = NavierStokes.ShapeTransition.separation c.shapeTime A.normalization F.data.core.P

noncomputable def NavierStokes.NominalProfile.Controls.rawU {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : Field

Raw U, given by ShapeTransition.scaledFamily c.radius c.seedU.

Equations

• c.rawU = NavierStokes.ShapeTransition.scaledFamily c.radius c.seedU

noncomputable def NavierStokes.NominalProfile.Controls.rawF {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : Field

Raw F, given by ShapeTransition.scaledFamily c.radius c.shapedF.

Equations

• c.rawF = NavierStokes.ShapeTransition.scaledFamily c.radius c.shapedF

noncomputable def NavierStokes.NominalProfile.Controls.rawRows {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (r eta : ℝ) : Debt

Raw rows as an element of Debt.

Equations

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

noncomputable def NavierStokes.NominalProfile.Controls.restoreRows {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (r b eta : ℝ) : Debt

Restore rows as an element of Debt.

Equations

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

noncomputable def NavierStokes.NominalProfile.Controls.manuscriptDebt {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (eta : ℝ) : Debt

Manuscript debt as an element of Debt.

Equations

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

theorem NavierStokes.NominalProfile.Controls.separation_pos {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : 0 < c.separation

theorem NavierStokes.NominalProfile.Controls.rawE_eq {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (p : Point) : ShapeTransition.scaledE c.radius c.rawF p = preparedE F A.normalization c.shapeTime c.initialShape c.seedF p

theorem NavierStokes.NominalProfile.Controls.rawRows_eq_moments {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {r : ℝ} (hr : 0 ≤ r) (eta : ℝ) : c.rawRows r eta = moments c.rawU (ShapeTransition.scaledE c.radius c.rawF) r eta

theorem NavierStokes.NominalProfile.Controls.base_prefix_before_restore {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {r : ℝ} (hr : 0 ≤ r) (hr8 : r ≤ Real.exp (-8)) (eta : ℝ) : moments (baseU F A.normalization c.seedU) (baseE F A.normalization c.shapeTime c.initialShape c.seedF) r eta = c.rawRows r eta

theorem NavierStokes.NominalProfile.Controls.base_restore_segment {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {x eta : ℝ} (hx : c.separation ≤ x) (hxb : x ≤ matchFraction) (hη : eta ∈ ReferencePath.parameterInterval) : baseU F A.normalization c.seedU (x, eta) = ShapeTransition.restore c.initialAxial (Real.log x, eta) ∧ baseE F A.normalization c.shapeTime c.initialShape c.seedF (x, eta) = idealE F (x, eta)

theorem NavierStokes.NominalProfile.Controls.base_restore_difference {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {x eta : ℝ} (hx : c.separation ≤ x) (hxb : x ≤ matchFraction) (hη : eta ∈ ReferencePath.parameterInterval) : density (fun (t : ℝ) => baseU F A.normalization c.seedU (t, eta)) (fun (t : ℝ) => baseE F A.normalization c.shapeTime c.initialShape c.seedF (t, eta)) x - density (fun (t : ℝ) => F.U (t, eta)) (fun (t : ℝ) => F.E (t, eta)) x = ![ShapeTransition.restoreDefect c.initialAxial (x, eta), 0, ShapeTransition.restoreDensityJ c.initialAxial (idealAmplitude F) (x, eta), ShapeTransition.restoreDensityS c.initialAxial (x, eta), 0]

theorem NavierStokes.NominalProfile.Controls.restoreRows_eq_integral {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {eta : ℝ} (hη : eta ∈ ReferencePath.parameterInterval) (hsep : c.separation ≤ Real.exp (-8)) : c.restoreRows c.separation matchFraction eta = fun (i : Fin 5) => ∫ (x : ℝ) in Set.Ioc c.separation matchFraction, density (fun (t : ℝ) => baseU F A.normalization c.seedU (t, eta)) (fun (t : ℝ) => baseE F A.normalization c.shapeTime c.initialShape c.seedF (t, eta)) x i - density (fun (t : ℝ) => F.U (t, eta)) (fun (t : ℝ) => F.E (t, eta)) x i

theorem NavierStokes.NominalProfile.Controls.debt_eq_negative_manuscriptDebt {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : c.separation ≤ Real.exp (-8)) {eta : ℝ} (hη : eta ∈ ReferencePath.parameterInterval) : c.debt eta = -c.manuscriptDebt eta

The actual smooth profiles and their canonical pressure

theorem NavierStokes.NominalProfile.Controls.normalizedDebt_smooth {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ContDiffOn ℝ (↑⊤) (normalizedDebt F c.debt) ReferencePath.parameterInterval

noncomputable def NavierStokes.NominalProfile.Controls.admissibleDomain {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ProfileHistories.RadialDomain

Smallness is a transparent test on the already constructed debt. Its strict sublevel set is open, so successful repair gives ordinary smoothness.

Equations

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

theorem NavierStokes.NominalProfile.Controls.admissible_nonnegative {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {p : Point} (hX : 0 ≤ p.1) (hη : p.2 ∈ ReferencePath.parameterInterval) (hs : SmallDebt F c.debt p.2) : p ∈ c.admissibleDomain.carrier

noncomputable def NavierStokes.NominalProfile.Controls.profiles {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : c.separation ≤ Real.exp (-8)) : ProfileHistories.Profiles c.admissibleDomain

Profiles, bundling f, U, f_smooth, U_smooth and the required compatibility proofs.

Equations

• c.profiles hsep = { f := c.f, U := c.U, f_smooth := ⋯, U_smooth := ⋯, pressure0 := F.axisDatum, pressure0_smooth := ⋯ }

theorem NavierStokes.NominalProfile.Controls.profiles_E {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hX : 0 < p.1) : (c.profiles hsep).E p = c.E p

theorem NavierStokes.NominalProfile.Controls.physical_density_eq {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : c.separation ≤ Real.exp (-8)) {x : ℝ} (hx : 0 < x) (eta : ℝ) : density (fun (t : ℝ) => c.U (t, eta)) (fun (t : ℝ) => c.E (t, eta)) x = regularDensity (c.profiles hsep) (x, eta)

theorem NavierStokes.NominalProfile.Controls.physical_density_integrable {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : c.separation ≤ Real.exp (-8)) {r eta : ℝ} (hr : 0 ≤ r) (hη : eta ∈ ReferencePath.parameterInterval) (hs : SmallDebt F c.debt eta) (i : Fin 5) : MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => c.U (t, eta)) (fun (t : ℝ) => c.E (t, eta)) x i) (Set.Ioc 0 r) MeasureTheory.volume

theorem NavierStokes.NominalProfile.Controls.profiles_pressure {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hX : 0 ≤ p.1) : (c.profiles hsep).pressure p = c.Pi p

theorem NavierStokes.NominalProfile.global_integral_replace {f g : ℝ → ℝ} {a : ℝ} (ha : 0 ≤ a) (hf : MeasureTheory.IntegrableOn f (Set.Ioc 0 a) MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g (Set.Ioi 0) MeasureTheory.volume) (head : ∫ (x : ℝ) in Set.Ioc 0 a, f x = ∫ (x : ℝ) in Set.Ioc 0 a, g x) (tail : ∀ (x : ℝ), a < x → f x = g x) : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Ioi 0, g x

theorem NavierStokes.NominalProfile.canonical_past_identity {k : ℝ → ℝ} (hk : MeasureTheory.IntegrableOn k (Set.Ioi 0) MeasureTheory.volume) {X : ℝ} (hX : 0 ≤ X) : (-∫ (x : ℝ) in Set.Ioi 0, k x) + ∫ (x : ℝ) in Set.Ioc 0 X, k x = -∫ (x : ℝ) in Set.Ioi X, k x

noncomputable def NavierStokes.NominalProfile.halfKernel (E : Field) (eta x : ℝ) : ℝ

Half kernel, given by E (x, eta) ^ 2 / (2 * x).

Equations

• NavierStokes.NominalProfile.halfKernel E eta x = E (x, eta) ^ 2 / (2 * x)

theorem NavierStokes.NominalProfile.halfKernel_eq (E : Field) (eta x : ℝ) : halfKernel E eta x = E (x, eta) ^ 2 / x / 2

theorem NavierStokes.NominalProfile.outgoing_halfKernel_integrable (F : OutgoingProfile.Profile) (R eta : ℝ) (hR : 0 < R) : MeasureTheory.IntegrableOn (halfKernel (OutgoingDilation.E F R) eta) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.NominalProfile.outgoing_axis_halfKernel (F : OutgoingProfile.Profile) (R eta : ℝ) (hR : 0 < R) : F.axisDatum eta = -∫ (x : ℝ) in Set.Ioi 0, halfKernel (OutgoingDilation.E F R) eta x

theorem NavierStokes.NominalProfile.outgoing_pressure_halfKernel (F : OutgoingProfile.Profile) (R eta : ℝ) (hR : 0 < R) {X : ℝ} (hX : 0 < X) : OutgoingDilation.Pi F R (X, eta) = -∫ (x : ℝ) in Set.Ioi X, halfKernel (OutgoingDilation.E F R) eta x

theorem NavierStokes.NominalProfile.outgoing_pressure_prefix (F : OutgoingProfile.Profile) (R eta : ℝ) (hR : 0 < R) {X : ℝ} (hX : 0 < X) : F.axisDatum eta + moments (OutgoingDilation.U F R) (OutgoingDilation.E F R) X eta 4 = OutgoingDilation.Pi F R (X, eta)

theorem NavierStokes.NominalProfile.Controls.pressure_after_match {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : c.separation ≤ Real.exp (-8)) {X eta : ℝ} (hX : c.radius * matchFraction ≤ X) (hη : eta ∈ ReferencePath.parameterInterval) (hs : SmallDebt F c.debt eta) : c.Pi (X, eta) = OutgoingDilation.Pi F c.radius (X, eta)

theorem NavierStokes.NominalProfile.Controls.kernel_integral {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : c.separation ≤ Real.exp (-8)) {eta : ℝ} (hη : eta ∈ ReferencePath.parameterInterval) (hs : SmallDebt F c.debt eta) : MeasureTheory.IntegrableOn (halfKernel c.E eta) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (x : ℝ) in Set.Ioi 0, halfKernel c.E eta x = ∫ (x : ℝ) in Set.Ioi 0, halfKernel (OutgoingDilation.E F c.radius) eta x

theorem NavierStokes.NominalProfile.Controls.pressure_canonical {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : c.separation ≤ Real.exp (-8)) {X eta : ℝ} (hX : 0 < X) (hη : eta ∈ ReferencePath.parameterInterval) (hs : SmallDebt F c.debt eta) : c.Pi (X, eta) = -(1 / 2) * ∫ (x : ℝ) in Set.Ioi X, c.E (x, eta) ^ 2 / x

Keeping the actual continuation witness

noncomputable def NavierStokes.NominalProfile.AxisStage.ofEntrance {F : OutgoingProfile.Profile} {j : ℝ} (hj : NaturalAxisData.SmallParameters F.data.h j) (prep : AxisPreparation F j) (Λ C : ℝ) (hΛ : prep.scaleBound ≤ Λ) (hC : NaturalEntrance.entranceNormalization prep.inputs Λ prep.delta ≤ C) (E : NaturalEntrance.EntranceProfile prep.inputs Λ C) : AxisStage F

Of entrance, given by ⟨j, hj, prep, Λ, C, hΛ, hC, E⟩.

Equations

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

noncomputable def NavierStokes.NominalProfile.Controls.ofContinuation {F : OutgoingProfile.Profile} (A : AxisStage F) {N : ℕ} {eps : ℝ} (w : ActivationContinuation.ContinuationWitness A.natural ⋯ ⋯ ⋯ N eps) (T : ℝ) (hT : 0 < T) : Controls A

Of continuation, bundling referenceWidth, referenceWidth_pos, referenceWidth_small, activationTime and the required compatibility proofs.

Equations

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

theorem NavierStokes.NominalProfile.Controls.ofContinuation_seed {F : OutgoingProfile.Profile} (A : AxisStage F) {N : ℕ} {eps : ℝ} (w : ActivationContinuation.ContinuationWitness A.natural ⋯ ⋯ ⋯ N eps) (T : ℝ) (hT : 0 < T) : (ofContinuation A w T hT).seedF = w.parameters.profiles.f ∧ (ofContinuation A w T hT).seedU = w.parameters.profiles.U

theorem NavierStokes.NominalProfile.Controls.ofContinuation_log_control {F : OutgoingProfile.Profile} (A : AxisStage F) {N : ℕ} {eps : ℝ} (w : ActivationContinuation.ContinuationWitness A.natural ⋯ ⋯ ⋯ N eps) (T : ℝ) (hT : 0 < T) : have c := ofContinuation A w T hT; c.reference.SmallLogControl (Set.Icc (-1) 1) N eps c.activationTime c.kappa c.axialWidth c.angularWidth

Joining the heat completion of the same outgoing profile

theorem NavierStokes.NominalProfile.physical_band_in_parameterInterval {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : eta ∈ ReferencePath.parameterInterval

noncomputable def NavierStokes.NominalProfile.Controls.heatJoin {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ℝ

Heat join, given by c.radius * matchFraction.

Equations

• c.heatJoin = c.radius * NavierStokes.NominalProfile.matchFraction

noncomputable def NavierStokes.NominalProfile.Controls.heatBlend {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (X : ℝ) : ℝ

Heat blend, given by ShapeTransition.radialSwitch c.heatJoin 1 X.

Equations

• c.heatBlend X = NavierStokes.ShapeTransition.radialSwitch c.heatJoin 1 X

noncomputable def NavierStokes.NominalProfile.Controls.heatedE {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → HeatedOutgoing.Coeff) (p : Point) : ℝ

Heated E, given by c.E p + c.heatBlend p.1 * (HeatedOutgoing.E F c.radius coef p - c.E p).

Equations

• c.heatedE coef p = c.E p + c.heatBlend p.1 * (NavierStokes.HeatedOutgoing.E F c.radius coef p - c.E p)

noncomputable def NavierStokes.NominalProfile.Controls.heatedH {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → HeatedOutgoing.Coeff) (p : Point) : ℝ

Heated H, given by Real.sqrt (2 * p.1) * c.heatedE coef p.

Equations

• c.heatedH coef p = √(2 * p.1) * c.heatedE coef p

noncomputable def NavierStokes.NominalProfile.Controls.heatedPi {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → HeatedOutgoing.Coeff) (p : Point) : ℝ

Heated pi, given by F.axisDatum p.2 + moments c.U (c.heatedE coef) p.1 p.2 4.

Equations

• c.heatedPi coef p = F.axisDatum p.2 + NavierStokes.NominalProfile.moments c.U (c.heatedE coef) p.1 p.2 4

noncomputable def NavierStokes.NominalProfile.Controls.heatedf {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → HeatedOutgoing.Coeff) (p : Point) : ℝ

Heatedf, with branches according to p.1 ≤ Xi.

Equations

• c.heatedf coef p = if p.1 ≤ NavierStokes.NominalProfile.Xi then c.f p else c.heatedE coef p / √(2 * p.1)

theorem NavierStokes.NominalProfile.Controls.heatJoin_pos {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : 0 < c.heatJoin

theorem NavierStokes.NominalProfile.Controls.heatJoin_lt_radius {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : c.heatJoin < c.radius

theorem NavierStokes.NominalProfile.Controls.heatBlend_smooth {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ContDiff ℝ (↑⊤) c.heatBlend

theorem NavierStokes.NominalProfile.Controls.heatBlend_before {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {X : ℝ} (hX : X ≤ c.heatJoin) : c.heatBlend X = 0

theorem NavierStokes.NominalProfile.Controls.heatBlend_after {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {X : ℝ} (hX : c.radius ≤ X) : c.heatBlend X = 1

theorem NavierStokes.NominalProfile.Controls.heatedE_before {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → HeatedOutgoing.Coeff) {p : Point} (hp : p.1 ≤ c.heatJoin) : c.heatedE coef p = c.E p

theorem NavierStokes.NominalProfile.Controls.heatedE_after {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → HeatedOutgoing.Coeff) {p : Point} (hp : c.heatJoin < p.1) : c.heatedE coef p = HeatedOutgoing.E F c.radius coef p

theorem NavierStokes.NominalProfile.Controls.heated_fields_after {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → HeatedOutgoing.Coeff) {p : Point} (hp : c.heatJoin < p.1) : c.U p = HeatedOutgoing.U F c.radius p ∧ c.heatedE coef p = HeatedOutgoing.E F c.radius coef p

theorem NavierStokes.NominalProfile.Controls.heated_natural_prefix {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → HeatedOutgoing.Coeff) (hsep : c.separation ≤ Real.exp (-8)) (hscale : 1 ≤ A.scale) {p : Point} (hp : p.1 ≤ 4 / A.scale) : c.heatedf coef p = A.natural.profile.family.f p ∧ c.U p = A.natural.profile.family.U p

theorem NavierStokes.NominalProfile.Controls.heatedE_smooth {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B : ℝ} (w : HeatedOutgoing.CompensationWitness F c.radius B) (hsep : c.separation ≤ Real.exp (-8)) : ContDiffOn ℝ (↑⊤) (c.heatedE w.coefficients) {p : Point | p ∈ HeatedOutgoing.domain ∧ SmallDebt F c.debt p.2}

theorem NavierStokes.NominalProfile.density_dilate_integrable (R : ℝ) (hR : 0 < R) (U E : Field) (r eta : ℝ) (i : Fin 5) (hf : MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => U (t, eta)) (fun (t : ℝ) => E (t, eta)) x i) (Set.Ioc 0 (r / R)) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => dilateField R U (t, eta)) (fun (t : ℝ) => dilateField R E (t, eta)) x i) (Set.Ioc 0 r) MeasureTheory.volume

theorem NavierStokes.NominalProfile.heated_outgoing_density_integrable {F : OutgoingProfile.Profile} {R B : ℝ} (w : HeatedOutgoing.CompensationWitness F R B) {eta : ℝ} (hη : eta ∈ HeatedOutgoing.parameterDomain) (r : ℝ) (i : Fin 5) : MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => HeatedOutgoing.U F R (t, eta)) (fun (t : ℝ) => HeatedOutgoing.E F R w.coefficients (t, eta)) x i) (Set.Ioc 0 r) MeasureTheory.volume

theorem NavierStokes.NominalProfile.prefix_integrable_replace {f g : ℝ → ℝ} {a r : ℝ} (ha : 0 ≤ a) (har : a ≤ r) (hf : MeasureTheory.IntegrableOn f (Set.Ioc 0 a) MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g (Set.Ioc 0 r) MeasureTheory.volume) (tail : ∀ (x : ℝ), a < x → f x = g x) : MeasureTheory.IntegrableOn f (Set.Ioc 0 r) MeasureTheory.volume

theorem NavierStokes.NominalProfile.global_integral_replace_renormalized {f g b : ℝ → ℝ} {a : ℝ} (ha : 0 ≤ a) (hf : MeasureTheory.IntegrableOn f (Set.Ioc 0 a) MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g (Set.Ioc 0 a) MeasureTheory.volume) (hgb : MeasureTheory.IntegrableOn (fun (x : ℝ) => g x - b x) (Set.Ioi 0) MeasureTheory.volume) (head : ∫ (x : ℝ) in Set.Ioc 0 a, f x = ∫ (x : ℝ) in Set.Ioc 0 a, g x) (tail : ∀ (x : ℝ), a < x → f x = g x) : MeasureTheory.IntegrableOn (fun (x : ℝ) => f x - b x) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (x : ℝ) in Set.Ioi 0, f x - b x = ∫ (x : ℝ) in Set.Ioi 0, g x - b x

theorem NavierStokes.NominalProfile.Controls.heated_moments_at_match {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B : ℝ} (w : HeatedOutgoing.CompensationWitness F c.radius B) (hsep : c.separation ≤ Real.exp (-8)) {eta : ℝ} (hη : eta ∈ HeatedOutgoing.parameterDomain) (hs : SmallDebt F c.debt eta) : moments c.U (c.heatedE w.coefficients) c.heatJoin eta = moments (HeatedOutgoing.U F c.radius) (HeatedOutgoing.E F c.radius w.coefficients) c.heatJoin eta

theorem NavierStokes.NominalProfile.Controls.heated_density_integrable_at_match {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B : ℝ} (w : HeatedOutgoing.CompensationWitness F c.radius B) (hsep : c.separation ≤ Real.exp (-8)) {eta : ℝ} (hη : eta ∈ HeatedOutgoing.parameterDomain) (hs : SmallDebt F c.debt eta) (i : Fin 5) : MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => c.U (t, eta)) (fun (t : ℝ) => c.heatedE w.coefficients (t, eta)) x i) (Set.Ioc 0 c.heatJoin) MeasureTheory.volume

theorem NavierStokes.NominalProfile.Controls.heated_density_integrable {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B : ℝ} (w : HeatedOutgoing.CompensationWitness F c.radius B) (hsep : c.separation ≤ Real.exp (-8)) {eta r : ℝ} (hη : eta ∈ HeatedOutgoing.parameterDomain) (hs : SmallDebt F c.debt eta) (hr : c.heatJoin ≤ r) (i : Fin 5) : MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => c.U (t, eta)) (fun (t : ℝ) => c.heatedE w.coefficients (t, eta)) x i) (Set.Ioc 0 r) MeasureTheory.volume

theorem NavierStokes.NominalProfile.Controls.heated_moments {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B : ℝ} (w : HeatedOutgoing.CompensationWitness F c.radius B) (hsep : c.separation ≤ Real.exp (-8)) {eta r : ℝ} (hη : eta ∈ HeatedOutgoing.parameterDomain) (hs : SmallDebt F c.debt eta) (hr : c.heatJoin ≤ r) : moments c.U (c.heatedE w.coefficients) r eta = moments (HeatedOutgoing.U F c.radius) (HeatedOutgoing.E F c.radius w.coefficients) r eta

theorem NavierStokes.NominalProfile.Controls.heated_row_transfer {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B : ℝ} (w : HeatedOutgoing.CompensationWitness F c.radius B) (hsep : c.separation ≤ Real.exp (-8)) {eta : ℝ} (hη : eta ∈ HeatedOutgoing.parameterDomain) (hs : SmallDebt F c.debt eta) (i : Fin 5) (background : ℝ → ℝ) (hg : MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => HeatedOutgoing.U F c.radius (t, eta)) (fun (t : ℝ) => HeatedOutgoing.E F c.radius w.coefficients (t, eta)) x i - background x) (Set.Ioi 0) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => c.U (t, eta)) (fun (t : ℝ) => c.heatedE w.coefficients (t, eta)) x i - background x) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (x : ℝ) in Set.Ioi 0, density (fun (t : ℝ) => c.U (t, eta)) (fun (t : ℝ) => c.heatedE w.coefficients (t, eta)) x i - background x = ∫ (x : ℝ) in Set.Ioi 0, density (fun (t : ℝ) => HeatedOutgoing.U F c.radius (t, eta)) (fun (t : ℝ) => HeatedOutgoing.E F c.radius w.coefficients (t, eta)) x i - background x

theorem NavierStokes.NominalProfile.heated_outgoing_halfKernel_integrable {F : OutgoingProfile.Profile} {R B : ℝ} (w : HeatedOutgoing.CompensationWitness F R B) {eta : ℝ} (hη : eta ∈ HeatedOutgoing.parameterDomain) : MeasureTheory.IntegrableOn (halfKernel (HeatedOutgoing.E F R w.coefficients) eta) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.NominalProfile.heated_outgoing_axis_halfKernel {F : OutgoingProfile.Profile} {R B : ℝ} (w : HeatedOutgoing.CompensationWitness F R B) {eta : ℝ} (hη : eta ∈ HeatedOutgoing.parameterDomain) : F.axisDatum eta = -∫ (x : ℝ) in Set.Ioi 0, halfKernel (HeatedOutgoing.E F R w.coefficients) eta x

theorem NavierStokes.NominalProfile.heated_outgoing_pressure_prefix {F : OutgoingProfile.Profile} {R B : ℝ} (w : HeatedOutgoing.CompensationWitness F R B) {eta X : ℝ} (hη : eta ∈ HeatedOutgoing.parameterDomain) (hX : 0 ≤ X) : F.axisDatum eta + moments (HeatedOutgoing.U F R) (HeatedOutgoing.E F R w.coefficients) X eta 4 = HeatedOutgoing.Pi F R w.coefficients (X, eta)

structure NavierStokes.NominalProfile.FiveMomentCertificate (U E : Field) (powerH : ℝ → ℝ) (P0 eta : ℝ) : Prop

The five global conditions are stated for the literal final fields.

• mass_integrable : MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => U (t, eta)) (fun (t : ℝ) => E (t, eta)) x 0) (Set.Ioi 0) MeasureTheory.volume
• transport_integrable : MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => U (t, eta)) (fun (t : ℝ) => E (t, eta)) x 2) (Set.Ioi 0) MeasureTheory.volume
• energy_integrable : MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => U (t, eta)) (fun (t : ℝ) => E (t, eta)) x 3) (Set.Ioi 0) MeasureTheory.volume
• angular_integrable : MeasureTheory.IntegrableOn (fun (x : ℝ) => density (fun (t : ℝ) => U (t, eta)) (fun (t : ℝ) => E (t, eta)) x 1 - powerH x) (Set.Ioi 0) MeasureTheory.volume
• pressure_integrable : MeasureTheory.IntegrableOn (halfKernel E eta) (Set.Ioi 0) MeasureTheory.volume
• mass_zero : ∫ (x : ℝ) in Set.Ioi 0, U (x, eta) = 0
• transport_zero : ∫ (x : ℝ) in Set.Ioi 0, U (x, eta) * √(2 * x) * E (x, eta) = 0
• energy_zero : ∫ (x : ℝ) in Set.Ioi 0, U (x, eta) ^ 2 - E (x, eta) ^ 2 / 2 = 0
• angular_zero : ∫ (x : ℝ) in Set.Ioi 0, √(2 * x) * E (x, eta) - powerH x = 0
• pressure_datum : P0 = -∫ (x : ℝ) in Set.Ioi 0, halfKernel E eta x

theorem NavierStokes.NominalProfile.Controls.heated_pressure_data {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B : ℝ} (w : HeatedOutgoing.CompensationWitness F c.radius B) (hsep : c.separation ≤ Real.exp (-8)) {eta : ℝ} (hη : eta ∈ HeatedOutgoing.parameterDomain) (hs : SmallDebt F c.debt eta) : MeasureTheory.IntegrableOn (halfKernel (c.heatedE w.coefficients) eta) (Set.Ioi 0) MeasureTheory.volume ∧ F.axisDatum eta = -∫ (x : ℝ) in Set.Ioi 0, halfKernel (c.heatedE w.coefficients) eta x

theorem NavierStokes.NominalProfile.Controls.heated_five_moments {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B D : ℝ} (w : HeatedOutgoing.CompensationWitness F c.radius B) (hF : OutgoingProfile.Specification F D) (hsep : c.separation ≤ Real.exp (-8)) {eta : ℝ} (hη : eta ∈ HeatedOutgoing.parameterDomain) (hs : SmallDebt F c.debt eta) : FiveMomentCertificate c.U (c.heatedE w.coefficients) (OutgoingDilation.powerH F c.radius) (F.axisDatum eta) eta

theorem NavierStokes.NominalProfile.Controls.heated_pressure_canonical {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B : ℝ} (w : HeatedOutgoing.CompensationWitness F c.radius B) (hsep : c.separation ≤ Real.exp (-8)) {X eta : ℝ} (hX : 0 ≤ X) (hη : eta ∈ HeatedOutgoing.parameterDomain) (hs : SmallDebt F c.debt eta) : c.heatedPi w.coefficients (X, eta) = -(1 / 2) * ∫ (x : ℝ) in Set.Ioi X, c.heatedE w.coefficients (x, eta) ^ 2 / x

theorem NavierStokes.NominalProfile.Controls.heated_pressure_after {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B : ℝ} (w : HeatedOutgoing.CompensationWitness F c.radius B) (hsep : c.separation ≤ Real.exp (-8)) {X eta : ℝ} (hX : c.heatJoin ≤ X) (hη : eta ∈ HeatedOutgoing.parameterDomain) (hs : SmallDebt F c.debt eta) : c.heatedPi w.coefficients (X, eta) = HeatedOutgoing.Pi F c.radius w.coefficients (X, eta)

theorem NavierStokes.NominalProfile.Controls.heated_pressure_before {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → HeatedOutgoing.Coeff) {p : Point} (hp : p.1 ≤ c.heatJoin) : c.heatedPi coef p = c.Pi p

theorem NavierStokes.NominalProfile.Controls.ofContinuation_reference {F : OutgoingProfile.Profile} (A : AxisStage F) {N : ℕ} {eps : ℝ} (w : ActivationContinuation.ContinuationWitness A.natural ⋯ ⋯ ⋯ N eps) (T : ℝ) (hT : 0 < T) : (ofContinuation A w T hT).reference = w.parameters.reference

theorem NavierStokes.NominalProfile.Controls.ofContinuation_endpoints {F : OutgoingProfile.Profile} (A : AxisStage F) {N : ℕ} {eps : ℝ} (w : ActivationContinuation.ContinuationWitness A.natural ⋯ ⋯ ⋯ N eps) (T : ℝ) (hT : 0 < T) : (ofContinuation A w T hT).initialAxial = w.parameters.endpointAxial ∧ (ofContinuation A w T hT).initialShape = w.parameters.endpointLogarithm

noncomputable def NavierStokes.NominalProfile.Controls.seedProfiles {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ProfileHistories.Profiles A.referenceInput.radialDomain

Seed profiles, constructed using TransitionRamp.physicalProfiles.

Equations

• c.seedProfiles = NavierStokes.TransitionRamp.physicalProfiles A.natural.profile.family ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem NavierStokes.NominalProfile.Controls.Xi_lt_heatJoin {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : c.separation ≤ Real.exp (-8)) : Xi < c.heatJoin

theorem NavierStokes.NominalProfile.Controls.activation_collar_le_Xi {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : 4 / A.scale * Real.exp c.referenceWidth ≤ Xi

theorem NavierStokes.NominalProfile.Controls.heated_seed_fields {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → HeatedOutgoing.Coeff) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hp : p.1 ≤ Xi) : c.heatedf coef p = c.seedProfiles.f p ∧ c.U p = c.seedProfiles.U p ∧ c.heatedE coef p = c.seedProfiles.E p

theorem NavierStokes.NominalProfile.Controls.heated_seed_moments {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → HeatedOutgoing.Coeff) (hsep : c.separation ≤ Real.exp (-8)) {X : ℝ} (hX : X ≤ Xi) (eta : ℝ) : moments c.U (c.heatedE coef) X eta = moments c.seedProfiles.U c.seedProfiles.E X eta

theorem NavierStokes.NominalProfile.Controls.heated_seed_pressure {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → HeatedOutgoing.Coeff) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hX : 0 ≤ p.1) (hp : p.1 ≤ Xi) : c.heatedPi coef p = c.seedProfiles.pressure p

theorem NavierStokes.NominalProfile.Controls.Pi_smoothAt {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hX : 0 < p.1) (hη : p.2 ∈ ReferencePath.parameterInterval) (hs : SmallDebt F c.debt p.2) : ContDiffAt ℝ (↑⊤) c.Pi p

theorem NavierStokes.NominalProfile.Controls.heated_pressure_blend {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B : ℝ} (w : HeatedOutgoing.CompensationWitness F c.radius B) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hX : 0 < p.1) (hη : p.2 ∈ HeatedOutgoing.parameterDomain) (hs : SmallDebt F c.debt p.2) : c.heatedPi w.coefficients p = c.Pi p + c.heatBlend p.1 * (HeatedOutgoing.Pi F c.radius w.coefficients p - c.Pi p)

theorem NavierStokes.NominalProfile.Controls.heatedPi_smooth {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B : ℝ} (w : HeatedOutgoing.CompensationWitness F c.radius B) (hsep : c.separation ≤ Real.exp (-8)) : ContDiffOn ℝ (↑⊤) (c.heatedPi w.coefficients) {p : Point | p ∈ HeatedOutgoing.domain ∧ SmallDebt F c.debt p.2}

theorem NavierStokes.NominalProfile.Controls.heatedE_positive {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B : ℝ} (w : HeatedOutgoing.CompensationWitness F c.radius B) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hX : 0 < p.1) (hη : p.2 ∈ HeatedOutgoing.parameterDomain) (hs : SmallDebt F c.debt p.2) : 0 < c.heatedE w.coefficients p

One ordinary smooth extension of the same physical nominal profile

noncomputable def NavierStokes.NominalProfile.Controls.extendedE {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → ExtendedHeatedOutgoing.Coeff) (p : Point) : ℝ

Extended E, given by `c.E p + c.heatBlend p.1 * (ExtendedHeatedOutgoing.E F c.radius coef p

• c.E p)`.

Equations

• c.extendedE coef p = c.E p + c.heatBlend p.1 * (NavierStokes.ExtendedHeatedOutgoing.E F c.radius coef p - c.E p)

noncomputable def NavierStokes.NominalProfile.Controls.extendedf {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → ExtendedHeatedOutgoing.Coeff) (p : Point) : ℝ

Extendedf, with branches according to p.1 ≤ Xi.

Equations

• c.extendedf coef p = if p.1 ≤ NavierStokes.NominalProfile.Xi then c.f p else c.extendedE coef p / √(2 * p.1)

noncomputable def NavierStokes.NominalProfile.Controls.extendedPi {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → ExtendedHeatedOutgoing.Coeff) (p : Point) : ℝ

Extended pi, given by F.axisDatum p.2 + ProfileHistories.primitive (fun q => c.extendedf coef q ^ 2) p.

Equations

• c.extendedPi coef p = F.axisDatum p.2 + NavierStokes.ProfileHistories.primitive (fun (q : NavierStokes.ProfileHistories.Point) => c.extendedf coef q ^ 2) p

noncomputable def NavierStokes.NominalProfile.Controls.extendedDomain {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) : ProfileHistories.RadialDomain

Extended domain, bundling carrier, isOpen, scale_mem.

Equations

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

theorem NavierStokes.NominalProfile.Controls.extendedDomain_nonnegative {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {p : Point} (hX : 0 ≤ p.1) (hη : p.2 ∈ ReferencePath.parameterInterval) (he : p.2 ∈ ExtendedHeatedOutgoing.parameterDomain) (hs : SmallDebt F c.debt p.2) : p ∈ c.extendedDomain.carrier

theorem NavierStokes.NominalProfile.Controls.extendedE_before {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → ExtendedHeatedOutgoing.Coeff) {p : Point} (hp : p.1 ≤ c.heatJoin) : c.extendedE coef p = c.E p

theorem NavierStokes.NominalProfile.Controls.extendedE_eq_sqrt_f {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → ExtendedHeatedOutgoing.Coeff) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hX : 0 < p.1) : c.extendedE coef p = √(2 * p.1) * c.extendedf coef p

theorem NavierStokes.NominalProfile.Controls.extendedE_smoothAt {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B : ℝ} (w : ExtendedHeatedOutgoing.Witness F c.radius B) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hX : 0 < p.1) (hp : p ∈ c.extendedDomain.carrier) : ContDiffAt ℝ (↑⊤) (c.extendedE w.coefficients) p

theorem NavierStokes.NominalProfile.Controls.extendedf_smoothAt {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B : ℝ} (w : ExtendedHeatedOutgoing.Witness F c.radius B) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hp : p ∈ c.extendedDomain.carrier) : ContDiffAt ℝ (↑⊤) (c.extendedf w.coefficients) p

noncomputable def NavierStokes.NominalProfile.Controls.extendedProfiles {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B : ℝ} (w : ExtendedHeatedOutgoing.Witness F c.radius B) (hsep : c.separation ≤ Real.exp (-8)) : ProfileHistories.Profiles c.extendedDomain

Extended profiles, bundling f, U, f_smooth, U_smooth and the required compatibility proofs.

Equations

• c.extendedProfiles w hsep = { f := c.extendedf w.coefficients, U := c.U, f_smooth := ⋯, U_smooth := ⋯, pressure0 := F.axisDatum, pressure0_smooth := ⋯ }

theorem NavierStokes.NominalProfile.Controls.extended_fields_smoothAt {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) {B : ℝ} (w : ExtendedHeatedOutgoing.Witness F c.radius B) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hp : p ∈ c.extendedDomain.carrier) : ContDiffAt ℝ (↑⊤) (c.extendedf w.coefficients) p ∧ ContDiffAt ℝ (↑⊤) c.U p ∧ ContDiffAt ℝ (↑⊤) (c.extendedPi w.coefficients) p

theorem NavierStokes.NominalProfile.Controls.extendedE_physical {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → ExtendedHeatedOutgoing.Coeff) {p : Point} (hX : 0 < p.1) (hη : p.2 ∈ HeatedOutgoing.parameterDomain) : c.extendedE coef p = c.heatedE coef p

theorem NavierStokes.NominalProfile.Controls.extendedf_physical {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → ExtendedHeatedOutgoing.Coeff) {p : Point} (hX : 0 < p.1) (hη : p.2 ∈ HeatedOutgoing.parameterDomain) : c.extendedf coef p = c.heatedf coef p

theorem NavierStokes.NominalProfile.Controls.extendedPi_physical {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → ExtendedHeatedOutgoing.Coeff) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hX : 0 ≤ p.1) (hη : p.2 ∈ HeatedOutgoing.parameterDomain) : c.extendedPi coef p = c.heatedPi coef p

theorem NavierStokes.NominalProfile.Controls.extended_seed_fields {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → ExtendedHeatedOutgoing.Coeff) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hp : p.1 ≤ Xi) : c.extendedf coef p = c.seedProfiles.f p ∧ c.U p = c.seedProfiles.U p

theorem NavierStokes.NominalProfile.Controls.extended_seed_pressure {F : OutgoingProfile.Profile} {A : AxisStage F} (c : Controls A) (coef : ℝ → ExtendedHeatedOutgoing.Coeff) (hsep : c.separation ≤ Real.exp (-8)) {p : Point} (hX : 0 ≤ p.1) (hp : p.1 ≤ Xi) : c.extendedPi coef p = c.seedProfiles.pressure p

theorem NavierStokes.NominalProfile.FiveMomentCertificate.congr {U E V G : Field} {powerH : ℝ → ℝ} {P0 eta : ℝ} (h : FiveMomentCertificate U E powerH P0 eta) (he : ∀ (x : ℝ), 0 < x → V (x, eta) = U (x, eta) ∧ G (x, eta) = E (x, eta)) : FiveMomentCertificate V G powerH P0 eta

structure NavierStokes.NominalProfile.Witness (F : OutgoingProfile.Profile) : Type

One common nominal profile. All functions below are computed from these retained witnesses; the debt condition is the explicit normalized IFT test.

• axis : AxisStage F

  Axis of Witness, of type AxisStage F.

• controls : Controls self.axis

  Controls of Witness, of type Controls axis.

• outgoingBound : ℝ

  Outgoing bound of Witness, of type ℝ.

• outgoing_specification : OutgoingProfile.Specification F self.outgoingBound
• heatBound : ℝ

  Heat bound of Witness, of type ℝ.

• heat : ExtendedHeatedOutgoing.Witness F self.controls.radius self.heatBound

  Heat of Witness, of type ExtendedHeatedOutgoing.Witness F controls.radius heatBound.

• separated : self.controls.separation ≤ Real.exp (-8)
• debt_small (eta : ℝ) : eta ∈ HeatedOutgoing.parameterDomain → SmallDebt F self.controls.debt eta

noncomputable def NavierStokes.NominalProfile.Witness.f {F : OutgoingProfile.Profile} (W : Witness F) : Field

F, given by W.controls.extendedf W.heat.coefficients.

Equations

• W.f = W.controls.extendedf W.heat.coefficients

noncomputable def NavierStokes.NominalProfile.Witness.U {F : OutgoingProfile.Profile} (W : Witness F) : Field

U, given by W.controls.U.

Equations

• W.U = W.controls.U

noncomputable def NavierStokes.NominalProfile.Witness.E {F : OutgoingProfile.Profile} (W : Witness F) : Field

E, given by W.controls.extendedE W.heat.coefficients.

Equations

• W.E = W.controls.extendedE W.heat.coefficients

noncomputable def NavierStokes.NominalProfile.Witness.H {F : OutgoingProfile.Profile} (W : Witness F) (p : Point) : ℝ

H, given by Real.sqrt (2 * p.1) * W.E p.

Equations

• W.H p = √(2 * p.1) * W.E p

noncomputable def NavierStokes.NominalProfile.Witness.Pi {F : OutgoingProfile.Profile} (W : Witness F) : Field

Pi, given by W.controls.extendedPi W.heat.coefficients.

Equations

• W.Pi = W.controls.extendedPi W.heat.coefficients

noncomputable def NavierStokes.NominalProfile.Witness.domain {F : OutgoingProfile.Profile} (W : Witness F) : ProfileHistories.RadialDomain

Domain, given by W.controls.extendedDomain.

Equations

• W.domain = W.controls.extendedDomain

noncomputable def NavierStokes.NominalProfile.Witness.profiles {F : OutgoingProfile.Profile} (W : Witness F) : ProfileHistories.Profiles W.domain

Profiles, given by W.controls.extendedProfiles W.heat W.separated.

Equations

• W.profiles = W.controls.extendedProfiles W.heat ⋯

theorem NavierStokes.NominalProfile.Witness.domain_contains {F : OutgoingProfile.Profile} (W : Witness F) {p : Point} (hX : 0 ≤ p.1) (hη : p.2 ∈ HeatedOutgoing.parameterDomain) : p ∈ W.domain.carrier

theorem NavierStokes.NominalProfile.Witness.exists_parameter_interval {F : OutgoingProfile.Profile} (W : Witness F) : ∃ (a : ℝ), 1 < a ∧ a < 3 / 2 ∧ ∀ (X : ℝ), 0 ≤ X → ∀ eta ∈ Set.Ioo (-a) a, (X, eta) ∈ W.domain.carrier

Compactness of the physical band gives one common open parameter interval for all nonnegative radii, with the same fields and repair coefficients.

theorem NavierStokes.NominalProfile.Witness.fields_smooth {F : OutgoingProfile.Profile} (W : Witness F) {p : Point} (hp : p ∈ W.domain.carrier) : ContDiffAt ℝ (↑⊤) W.f p ∧ ContDiffAt ℝ (↑⊤) W.U p ∧ ContDiffAt ℝ (↑⊤) W.Pi p

theorem NavierStokes.NominalProfile.Witness.E_eq_sqrt_f {F : OutgoingProfile.Profile} (W : Witness F) {p : Point} (hX : 0 < p.1) : W.E p = √(2 * p.1) * W.f p

theorem NavierStokes.NominalProfile.Witness.E_positive {F : OutgoingProfile.Profile} (W : Witness F) {p : Point} (hX : 0 < p.1) (hη : p.2 ∈ HeatedOutgoing.parameterDomain) : 0 < W.E p

theorem NavierStokes.NominalProfile.Witness.five_moments {F : OutgoingProfile.Profile} (W : Witness F) {eta : ℝ} (hη : eta ∈ HeatedOutgoing.parameterDomain) : FiveMomentCertificate W.U W.E (OutgoingDilation.powerH F W.controls.radius) (F.axisDatum eta) eta

theorem NavierStokes.NominalProfile.Witness.pressure_canonical {F : OutgoingProfile.Profile} (W : Witness F) {X eta : ℝ} (hX : 0 ≤ X) (hη : eta ∈ HeatedOutgoing.parameterDomain) : W.Pi (X, eta) = -(1 / 2) * ∫ (x : ℝ) in Set.Ioi X, W.E (x, eta) ^ 2 / x

theorem NavierStokes.NominalProfile.Witness.seed_agreement {F : OutgoingProfile.Profile} (W : Witness F) {p : Point} (hX : 0 ≤ p.1) (hp : p.1 ≤ Xi) : W.f p = W.controls.seedProfiles.f p ∧ W.U p = W.controls.seedProfiles.U p ∧ W.Pi p = W.controls.seedProfiles.pressure p

theorem NavierStokes.NominalProfile.Witness.heat_agreement {F : OutgoingProfile.Profile} (W : Witness F) {p : Point} (hX : W.controls.heatJoin < p.1) (hη : p.2 ∈ HeatedOutgoing.parameterDomain) : W.U p = HeatedOutgoing.U F W.controls.radius p ∧ W.E p = HeatedOutgoing.E F W.controls.radius W.heat.physical.coefficients p ∧ W.Pi p = HeatedOutgoing.Pi F W.controls.radius W.heat.physical.coefficients p

theorem NavierStokes.NominalProfile.Witness.moments_after {F : OutgoingProfile.Profile} (W : Witness F) {r eta : ℝ} (hr : W.controls.heatJoin ≤ r) (hη : eta ∈ HeatedOutgoing.parameterDomain) : moments W.U W.E r eta = moments (HeatedOutgoing.U F W.controls.radius) (HeatedOutgoing.E F W.controls.radius W.heat.physical.coefficients) r eta

theorem NavierStokes.NominalProfile.Witness.U_outgoing {F : OutgoingProfile.Profile} (W : Witness F) {p : Point} (hp : W.controls.heatJoin < p.1) : W.U p = OutgoingDilation.U F W.controls.radius p

The axial field is unchanged after the matching patch, at every parameter.

theorem NavierStokes.NominalProfile.Witness.mass_outgoing {F : OutgoingProfile.Profile} (W : Witness F) {r eta : ℝ} (hr : W.controls.heatJoin ≤ r) (hp : (r, eta) ∈ W.domain.carrier) : ∫ (x : ℝ) in Set.Ioc 0 r, W.U (x, eta) = OutgoingDilation.M F W.controls.radius eta r

The true mass history agrees on the ordinary open parameter domain.

theorem NavierStokes.NominalProfile.Witness.after_pulse_open {F : OutgoingProfile.Profile} (W : Witness F) {r eta : ℝ} (hr : W.controls.heatJoin < r) (hp : (r, eta) ∈ W.domain.carrier) (hfar : OutgoingDilation.pulseEndRadius F W.controls.radius ≤ r) : W.U (r, eta) = 0 ∧ ∫ (x : ℝ) in Set.Ioc 0 r, W.U (x, eta) = 0

theorem NavierStokes.NominalProfile.Witness.E_extended_after_radius {F : OutgoingProfile.Profile} (W : Witness F) {p : Point} (hp : W.controls.radius ≤ p.1) : W.E p = ExtendedHeatedOutgoing.E F W.controls.radius W.heat.coefficients p

Past the matching radius the extension is the same extended heat field; this equality has no restriction to the closed physical parameter band.

theorem NavierStokes.NominalProfile.Witness.E_outgoing_before_patch {F : OutgoingProfile.Profile} (W : Witness F) {X eta : ℝ} (hR : W.controls.radius ≤ X) (hp : X ≤ OutgoingDilation.patchRadius F W.controls.radius) : W.E (X, eta) = OutgoingDilation.E F W.controls.radius (X, eta)

theorem NavierStokes.NominalProfile.Witness.E_outgoing_between_patch_and_switch {F : OutgoingProfile.Profile} (W : Witness F) {X eta : ℝ} (hR : W.controls.radius ≤ X) (hp : OutgoingDilation.patchRadius F W.controls.radius * OutgoingDilation.compensationPatch.right ≤ X) (hK : X ≤ OutgoingDilation.switchRadius F W.controls.radius) : W.E (X, eta) = OutgoingDilation.E F W.controls.radius (X, eta)

theorem NavierStokes.NominalProfile.exists_assembly_threshold {F : OutgoingProfile.Profile} {D : ℝ} (hF : OutgoingProfile.Specification F D) : ∃ (R0 : ℝ), 0 < R0 ∧ ∀ (A : AxisStage F) (c : Controls A), R0 ≤ c.radius → c.separation ≤ Real.exp (-8) → (∀ eta ∈ HeatedOutgoing.parameterDomain, SmallDebt F c.debt eta) → Nonempty (Witness F)

Heat completion imposes a late radius bound on the already selected outgoing profile. Any matched continuation beyond that bound gives one actual nominal witness, retaining its entrance and ramp parameters.

theorem NavierStokes.NominalProfile.exists_assembly_threshold_preserving {F : OutgoingProfile.Profile} {D : ℝ} (hF : OutgoingProfile.Specification F D) : ∃ (R0 : ℝ), 0 < R0 ∧ ∀ (A : AxisStage F) (c : Controls A), R0 ≤ c.radius → c.separation ≤ Real.exp (-8) → (∀ eta ∈ HeatedOutgoing.parameterDomain, SmallDebt F c.debt eta) → ∃ (W : Witness F), W.axis = A ∧ W.controls ≍ c

theorem NavierStokes.NominalProfile.prepare_axis_with_cutoff (F : OutgoingProfile.Profile) (hP : 2 ≤ F.data.core.P) {j : ℝ} (hj : NaturalAxisData.SmallParameters F.data.h j) : ∃ (prep : AxisPreparation F j), ∀ eta ∈ Set.Icc (-1) 1, |NaturalAxisData.Z F.data.h j F.axisDatum eta| ≤ prep.delta → 99 / 100 < NaturalAxisData.chi F.data.h j prep.sigma eta

Retain the cutoff margin from the same analytic input construction; later ACT existence uses this margin without rechoosing the axis data.