Modulation of one actual nominal profile

The regular fields f,U are extended from the closed positive half-plane without changing them there. Consequently their actual histories from the axis, including the pressure constant, are preserved. The separate angular field used by the periodic-loop construction is clamped only away from the modulation annulus. Finally only the supported edits are transplanted back to the original nominal profile.

+# Smooth auxiliary fields for an annulus

The maps constructed here agree with the physical fields on an open positive annulus and are globally smooth. Absolute histories from the axis are not preserved by clamping. The final section proves the correct transfer statement: supported edit differences, including their nonlinear density integrals, are unchanged when transplanted back to the original field.

noncomputable def NavierStokes.AnnularAuxiliary.positiveMap (a X : ℝ) : ℝ

Positive map, given by a + TransportPrimitive.cutoff (a / 2) a X * (X - a).

Equations

• NavierStokes.AnnularAuxiliary.positiveMap a X = a + NavierStokes.TransportPrimitive.cutoff (a / 2) a X * (X - a)

theorem NavierStokes.AnnularAuxiliary.positiveMap_contDiff (a : ℝ) : ContDiff ℝ (↑⊤) (positiveMap a)

theorem NavierStokes.AnnularAuxiliary.positiveMap_eq {a X : ℝ} (ha : 0 < a) (hX : a ≤ X) : positiveMap a X = X

theorem NavierStokes.AnnularAuxiliary.positiveMap_pos {a : ℝ} (ha : 0 < a) (X : ℝ) : 0 < positiveMap a X

noncomputable def NavierStokes.AnnularAuxiliary.auxiliary {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) (a : ℝ) (F : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

Auxiliary, given by F (positiveMap a p.1, w.parameterMap p.2).

Equations

• NavierStokes.AnnularAuxiliary.auxiliary w a F p = F (NavierStokes.AnnularAuxiliary.positiveMap a p.1, w.parameterMap p.2)

theorem NavierStokes.AnnularAuxiliary.auxiliary_contDiff {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) {a : ℝ} (ha : 0 < a) {F : ℝ × ℝ → ℝ} (hF : ContDiffOn ℝ (↑⊤) F (Set.Ioi 0 ×ˢ S)) : ContDiff ℝ (↑⊤) (auxiliary w a F)

theorem NavierStokes.AnnularAuxiliary.auxiliary_eq {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) {a : ℝ} (ha : 0 < a) (F : ℝ × ℝ → ℝ) {p : ℝ × ℝ} (hX : a ≤ p.1) (heta : |p.2| ≤ w.inner) : auxiliary w a F p = F p

theorem NavierStokes.AnnularAuxiliary.auxiliary_germ {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) {a : ℝ} (ha : 0 < a) (F : ℝ × ℝ → ℝ) {p : ℝ × ℝ} (hX : a < p.1) (heta : |p.2| < w.inner) : auxiliary w a F =ᶠ[nhds p] F

theorem NavierStokes.AnnularAuxiliary.auxiliary_jets {S : Set ℝ} (w : ParametricRadialExtension.ParameterWindow S) {a : ℝ} (ha : 0 < a) (F : ℝ × ℝ → ℝ) (m : ℕ) {p : ℝ × ℝ} (hX : a < p.1) (heta : |p.2| < w.inner) : iteratedFDeriv ℝ m (auxiliary w a F) p = iteratedFDeriv ℝ m F p

noncomputable def NavierStokes.AnnularAuxiliary.transplant {α : Type u_1} {E : Type u_2} [AddCommGroup E] (base aux replacement : α → E) (x : α) : E

Transplant only the edit. The original field carries the unchanged history between the axis and the edit window.

Equations

• NavierStokes.AnnularAuxiliary.transplant base aux replacement x = base x + (replacement x - aux x)

theorem NavierStokes.AnnularAuxiliary.transplant_outside {α : Type u_1} {E : Type u_2} [AddCommGroup E] {base aux replacement : α → E} {x : α} (hx : replacement x = aux x) : transplant base aux replacement x = base x

theorem NavierStokes.AnnularAuxiliary.transplant_inside {α : Type u_1} {E : Type u_2} [AddCommGroup E] {base aux replacement : α → E} {x : α} (hx : base x = aux x) : transplant base aux replacement x = replacement x

theorem NavierStokes.AnnularAuxiliary.transplant_density_difference {α : Type u_1} {E : Type u_2} {V : Type u_3} [AddCommGroup E] [AddCommGroup V] (H : α → E → V) {base aux replacement : α → E} {K : Set α} (hbase : Set.EqOn base aux K) (hedit : ∀ x ∉ K, replacement x = aux x) (x : α) : H x (transplant base aux replacement x) - H x (base x) = H x (replacement x) - H x (aux x)

Arbitrary nonlinear density changes transfer pointwise. This includes quadratic energy, transport, and pressure densities.

theorem NavierStokes.AnnularAuxiliary.transplant_contDiffOn {D : Set (ℝ × ℝ)} {base aux replacement : ℝ × ℝ → ℝ} (hb : ContDiffOn ℝ (↑⊤) base D) (ha : ContDiff ℝ (↑⊤) aux) (hr : ContDiff ℝ (↑⊤) replacement) : ContDiffOn ℝ (↑⊤) (transplant base aux replacement) D

theorem NavierStokes.AnnularAuxiliary.transplanted_density_integral {E : Type u_1} {V : Type u_2} [AddCommGroup E] [NormedAddCommGroup V] [NormedSpace ℝ V] (H : ℝ × ℝ → E → V) {base aux replacement : ℝ × ℝ → E} {K : Set (ℝ × ℝ)} (hbase : Set.EqOn base aux K) (hedit : ∀ x ∉ K, replacement x = aux x) (X eta : ℝ) : ∫ (r : ℝ) in 0..X, H (r, eta) (transplant base aux replacement (r, eta)) - H (r, eta) (base (r, eta)) = ∫ (r : ℝ) in 0..X, H (r, eta) (replacement (r, eta)) - H (r, eta) (aux (r, eta))

noncomputable def NavierStokes.ModulatedProfileAssembly.restrictDomain (D : ProfileHistories.RadialDomain) (S : Set ℝ) (hS : IsOpen S) : ProfileHistories.RadialDomain

Restrict parameters without changing any radial segment or any field.

Equations

• NavierStokes.ModulatedProfileAssembly.restrictDomain D S hS = { carrier := D.carrier ∩ Set.univ ×ˢ S, isOpen := ⋯, scale_mem := ⋯ }

theorem NavierStokes.ModulatedProfileAssembly.rows_eq_of_nonnegative {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (h0 : P.pressure0 = Q.pressure0) {X eta : ℝ} (hX : 0 ≤ X) (hf : ∀ x ∈ Set.Icc 0 X, P.f (x, eta) = Q.f (x, eta)) (hu : ∀ x ∈ Set.Icc 0 X, P.U (x, eta) = Q.U (x, eta)) : ModulatedHistories.profileRows P (X, eta) = ModulatedHistories.profileRows Q (X, eta)

theorem NavierStokes.ModulatedProfileAssembly.histories_eq_of_nonnegative {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (h0 : P.pressure0 = Q.pressure0) {X eta : ℝ} (hX : 0 ≤ X) (hf : ∀ x ∈ Set.Icc 0 X, P.f (x, eta) = Q.f (x, eta)) (hu : ∀ x ∈ Set.Icc 0 X, P.U (x, eta) = Q.U (x, eta)) (r : StressActivation.HistoryRow) : StressActivation.profileHistory P r (X, eta) = StressActivation.profileHistory Q r (X, eta)

structure NavierStokes.ModulatedProfileAssembly.ParameterData {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : Type

This is genuine available domain data of a fixed nominal witness.

• parameters : Set ℝ

  Parameters of ParameterData, of type Set ℝ.

• isOpen : IsOpen self.parameters
• contains : Set.Icc (-1) 1 ⊆ self.parameters
• nonnegative (X : ℝ) : 0 ≤ X → ∀ eta ∈ self.parameters, (X, eta) ∈ W.domain.carrier

theorem NavierStokes.ModulatedProfileAssembly.exists_parameterData {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : Nonempty (ParameterData W)

noncomputable def NavierStokes.ModulatedProfileAssembly.ParameterData.window {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) : ParametricRadialExtension.ParameterWindow d.parameters

Window, given by ParametricRadialExtension.parameterWindow d.isOpen d.contains.

Equations

• d.window = NavierStokes.ParametricRadialExtension.parameterWindow ⋯ ⋯

noncomputable def NavierStokes.ModulatedProfileAssembly.ParameterData.target {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) : Set ℝ

Target, given by Ioo (-d.window.inner) d.window.inner.

Equations

• d.target = Set.Ioo (-d.window.inner) d.window.inner

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.target_open {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) : IsOpen d.target

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.target_contains {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) : Set.Icc (-1) 1 ⊆ d.target

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.target_subset {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) : d.target ⊆ d.parameters

noncomputable def NavierStokes.ModulatedProfileAssembly.ParameterData.parameterized {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) (f : ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

Parameterized, given by f (p.1, d.window.parameterMap p.2).

Equations

• d.parameterized f p = f (p.1, d.window.parameterMap p.2)

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.parameterized_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) {f : ProfileHistories.Field} (hf : ContDiffOn ℝ (↑⊤) f W.domain.carrier) : ContDiffOn ℝ (↑⊤) (d.parameterized f) (Set.Ici 0 ×ˢ Set.univ)

noncomputable def NavierStokes.ModulatedProfileAssembly.ParameterData.extended {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) (f : ProfileHistories.Field) (hf : ContDiffOn ℝ (↑⊤) f W.domain.carrier) : ProfileHistories.Field

Extended, given by ParametricRadialExtension.halfPlaneExtension (d.parameterized f) (d.parameterized_smooth hf).

Equations

• d.extended f hf = NavierStokes.ParametricRadialExtension.halfPlaneExtension (d.parameterized f) ⋯

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.extended_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) (f : ProfileHistories.Field) (hf : ContDiffOn ℝ (↑⊤) f W.domain.carrier) : ContDiff ℝ (↑⊤) (d.extended f hf)

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.extended_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) (f : ProfileHistories.Field) (hf : ContDiffOn ℝ (↑⊤) f W.domain.carrier) {p : ProfileHistories.Point} (hX : 0 ≤ p.1) (heta : |p.2| ≤ d.window.inner) : d.extended f hf p = f p

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.extended_germ {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) (f : ProfileHistories.Field) (hf : ContDiffOn ℝ (↑⊤) f W.domain.carrier) {p : ProfileHistories.Point} (hX : 0 < p.1) (heta : p.2 ∈ d.target) : d.extended f hf =ᶠ[nhds p] f

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

F, given by d.extended W.profiles.f W.profiles.f_smooth.

Equations

• d.f = d.extended W.profiles.f ⋯

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

U, given by d.extended W.profiles.U W.profiles.U_smooth.

Equations

• d.U = d.extended W.profiles.U ⋯

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.f_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) : ContDiff ℝ (↑⊤) d.f

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.U_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) : ContDiff ℝ (↑⊤) d.U

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.fields_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) {p : ProfileHistories.Point} (hX : 0 ≤ p.1) (heta : p.2 ∈ d.target) : d.f p = W.profiles.f p ∧ d.U p = W.profiles.U p

noncomputable def NavierStokes.ModulatedProfileAssembly.ParameterData.profiles {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) : ProfileHistories.Profiles (ModulatedHistories.stripDomain Set.univ ⋯)

Profiles, constructed using ModulatedHistories.profiles.

Equations

• d.profiles = NavierStokes.ModulatedHistories.profiles Set.univ NavierStokes.ModulatedProfileAssembly.ParameterData.profiles._proof_1 d.f d.U F.axisDatum ⋯ ⋯ ⋯

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.pressure0_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) : d.profiles.pressure0 = W.profiles.pressure0

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.rows_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) {X eta : ℝ} (hX : 0 ≤ X) (heta : eta ∈ d.target) : ModulatedHistories.profileRows d.profiles (X, eta) = ModulatedHistories.profileRows W.profiles (X, eta)

These are absolute histories, not the histories of a radially clamped field.

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.histories_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) {X eta : ℝ} (hX : 0 ≤ X) (heta : eta ∈ d.target) (r : StressActivation.HistoryRow) : StressActivation.profileHistory d.profiles r (X, eta) = StressActivation.profileHistory W.profiles r (X, eta)

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.stocks_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) {p : ProfileHistories.Point} (hX : 0 < p.1) (heta : p.2 ∈ d.target) (hf : W.profiles.f p ≠ 0) : ActivationStocks.profileStockOne d.profiles F.data.h p = ActivationStocks.profileStockOne W.profiles F.data.h p ∧ ActivationStocks.profileStockTwo d.profiles F.data.h p = ActivationStocks.profileStockTwo W.profiles F.data.h p

noncomputable def NavierStokes.ModulatedProfileAssembly.ParameterData.E {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) (a : ℝ) (p : ProfileHistories.Point) : ℝ

Clamp only the auxiliary angular field. The history-bearing f,U above are unchanged on the entire positive half-plane.

Equations

• d.E a p = √(2 * NavierStokes.AnnularAuxiliary.positiveMap a p.1) * d.f (NavierStokes.AnnularAuxiliary.positiveMap a p.1, p.2)

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.E_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) {a : ℝ} (ha : 0 < a) : ContDiff ℝ (↑⊤) (d.E a)

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.E_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) {a : ℝ} (ha : 0 < a) {p : ProfileHistories.Point} (hX : a ≤ p.1) : d.E a p = d.profiles.E p

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.E_germ {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) {a : ℝ} (ha : 0 < a) {p : ProfileHistories.Point} (hX : a < p.1) : d.E a =ᶠ[nhds p] d.profiles.E

theorem NavierStokes.ModulatedProfileAssembly.ParameterData.E_nominal_germ {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : ParameterData W) {a : ℝ} (ha : 0 < a) {p : ProfileHistories.Point} (hX : a < p.1) (heta : p.2 ∈ d.target) : d.E a =ᶠ[nhds p] W.profiles.E

noncomputable def NavierStokes.ModulatedProfileAssembly.repairPatch {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : FiveProfileMoments.Patch

The first reserved five-row patch, belonging to the very same outgoing schedule and physical dilation as the nominal witness.

Equations

• NavierStokes.ModulatedProfileAssembly.repairPatch W = NavierStokes.ReservedPatches.momentPatch F W.controls.radius ⋯ NavierStokes.ReservedPatches.Slot.modulation

theorem NavierStokes.ModulatedProfileAssembly.repairPatch_before_positive {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : (repairPatch W).right < ReservedPatches.left F W.controls.radius ReservedPatches.Slot.positive

theorem NavierStokes.ModulatedProfileAssembly.nominal_patch_fields {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (eta : ℝ) {X : ℝ} (hX : X ∈ Set.Ioo (repairPatch W).left (repairPatch W).right) : W.profiles.U (X, eta) = 0 ∧ W.profiles.E (X, eta) = ReservedPatches.xAmplitude F W.controls.radius eta * X ^ (-1 / 2 - F.data.core.lam)

noncomputable def NavierStokes.ModulatedProfileAssembly.transplantProfiles {D D' : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) (R : ProfileHistories.Profiles D') (f U : ProfileHistories.Field) (hf : ContDiff ℝ (↑⊤) f) (hU : ContDiff ℝ (↑⊤) U) (S : Set ℝ) (hS : IsOpen S) (hD : (restrictDomain D S hS).carrier ⊆ D'.carrier) : ProfileHistories.Profiles (restrictDomain D S hS)

The original nominal profile plus a supported difference. Its axis pressure is retained literally.

Equations

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

theorem NavierStokes.ModulatedProfileAssembly.transplantProfiles_fields {D D' : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) (R : ProfileHistories.Profiles D') (f U : ProfileHistories.Field) (hf : ContDiff ℝ (↑⊤) f) (hU : ContDiff ℝ (↑⊤) U) (S : Set ℝ) (hS : IsOpen S) (hD : (restrictDomain D S hS).carrier ⊆ D'.carrier) {p : ProfileHistories.Point} (hfp : f p = Q.f p) (hUp : U p = Q.U p) : (transplantProfiles Q R f U hf hU S hS hD).f p = R.f p ∧ (transplantProfiles Q R f U hf hU S hS hD).U p = R.U p

noncomputable def NavierStokes.ModulatedProfileAssembly.band (a : ℝ) : Set ℝ

Band, given by Icc (-a) a.

Equations

• NavierStokes.ModulatedProfileAssembly.band a = Set.Icc (-a) a

noncomputable def NavierStokes.ModulatedProfileAssembly.modulationRegion (v : ModulatedHistories.Window) (a : ℝ) : Set ProfileHistories.Point

Modulation region, given by Icc v.left v.right ×ˢ band a.

Equations

• NavierStokes.ModulatedProfileAssembly.modulationRegion v a = Set.Icc v.left v.right ×ˢ NavierStokes.ModulatedProfileAssembly.band a

noncomputable def NavierStokes.ModulatedProfileAssembly.followingRegion {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (v : ModulatedHistories.Window) (a : ℝ) : Set ProfileHistories.Point

Following region, given by Icc v.right (repairPatch W).right ×ˢ band a.

Equations

• NavierStokes.ModulatedProfileAssembly.followingRegion W v a = Set.Icc v.right (NavierStokes.ModulatedProfileAssembly.repairPatch W).right ×ˢ NavierStokes.ModulatedProfileAssembly.band a

noncomputable def NavierStokes.ModulatedProfileAssembly.fullRegion {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (v : ModulatedHistories.Window) (a : ℝ) : Set ProfileHistories.Point

Full region, given by Icc v.left (repairPatch W).right ×ˢ band a.

Equations

• NavierStokes.ModulatedProfileAssembly.fullRegion W v a = Set.Icc v.left (NavierStokes.ModulatedProfileAssembly.repairPatch W).right ×ˢ NavierStokes.ModulatedProfileAssembly.band a

noncomputable def NavierStokes.ModulatedProfileAssembly.boundaryRegion (v : ModulatedHistories.Window) (a : ℝ) : Set ProfileHistories.Point

Boundary region, given by ({v.left, v.right} : Set ℝ) ×ˢ band a.

Equations

• NavierStokes.ModulatedProfileAssembly.boundaryRegion v a = {v.left, v.right} ×ˢ NavierStokes.ModulatedProfileAssembly.band a

structure NavierStokes.ModulatedProfileAssembly.LoopData {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : Type

Only nominal data are premises. The loop, modulation frequency and nonlinear repair are constructed later. Each supplied smooth coordinate is identified with an actual stock or shear of this particular W.

• parameter : ParameterData W

  Parameter of LoopData, of type ParameterData W.

• etaRadius : ℝ

  Eta radius of LoopData, of type ℝ.

• one_lt_etaRadius : 1 < self.etaRadius
• etaRadius_lt_target : self.etaRadius < self.parameter.window.inner
• modulation : ModulatedHistories.Window

  Modulation of LoopData, of type ModulatedHistories.Window.

• after_initial : 4 / W.axis.scale < self.modulation.left
• before_repair : self.modulation.right < (repairPatch W).left
• a : ProfileHistories.Field

  A of LoopData, of type Field.

• m : ProfileHistories.Field

  M of LoopData, of type Field.

• p₁ : ProfileHistories.Field

  P₁ of LoopData, of type Field.

• p₂ : ProfileHistories.Field

  P₂ of LoopData, of type Field.

• a_smooth : ContDiff ℝ (↑⊤) self.a
• m_smooth : ContDiff ℝ (↑⊤) self.m
• p₁_smooth : ContDiff ℝ (↑⊤) self.p₁
• p₂_smooth : ContDiff ℝ (↑⊤) self.p₂
• angular_eq (p : ProfileHistories.Point) : p ∈ fullRegion W self.modulation self.etaRadius → self.a p = ModulatedCone.angularShear W.profiles.E p
• axial_eq (p : ProfileHistories.Point) : p ∈ fullRegion W self.modulation self.etaRadius → self.a p * self.m p = ModulatedCone.signedAxialShear W.profiles.E W.profiles.U p
• stock₁_eq (p : ProfileHistories.Point) : p ∈ fullRegion W self.modulation self.etaRadius → self.p₁ p = ActivationStocks.profileStockOne W.profiles F.data.h p
• stock₂_eq (p : ProfileHistories.Point) : p ∈ fullRegion W self.modulation self.etaRadius → self.p₂ p = ActivationStocks.profileStockTwo W.profiles F.data.h p
• positive_f (p : ProfileHistories.Point) : p ∈ fullRegion W self.modulation self.etaRadius → 0 < W.profiles.f p
• positive_a (p : ProfileHistories.Point) : p ∈ fullRegion W self.modulation self.etaRadius → 0 < self.a p
• nonzero_L (p : ProfileHistories.Point) : p ∈ fullRegion W self.modulation self.etaRadius → NaturalAxisData.L F.data.h p.2 ≠ 0
• projection (p : ProfileHistories.Point) : p ∈ modulationRegion self.modulation self.etaRadius → 2 < self.p₁ p + self.p₂ p * self.m p
• relaxed (p : ProfileHistories.Point) : p ∈ modulationRegion self.modulation self.etaRadius → TrueConeLoop.nominalSpeed (self.a p) (self.m p) < ConeAlgebra.coneBound (self.p₁ p + self.p₂ p * self.m p) (self.p₂ p - self.p₁ p * self.m p)
• true_boundary (p : ProfileHistories.Point) : p ∈ boundaryRegion self.modulation self.etaRadius → 2 < TrueConeLoop.nominalSpeed (self.a p) (self.m p)
• true_following (p : ProfileHistories.Point) : p ∈ followingRegion W self.modulation self.etaRadius → TrueConeLoop.InTrueCone (self.p₁ p) (self.p₂ p) (self.a p) (self.a p * self.m p)

noncomputable def NavierStokes.ModulatedProfileAssembly.LoopData.parameters {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) : Set ℝ

Parameters, given by Ioo (-d.etaRadius) d.etaRadius.

Equations

• d.parameters = Set.Ioo (-d.etaRadius) d.etaRadius

theorem NavierStokes.ModulatedProfileAssembly.LoopData.parameters_open {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) : IsOpen d.parameters

theorem NavierStokes.ModulatedProfileAssembly.LoopData.parameters_contains {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) : Set.Icc (-1) 1 ⊆ d.parameters

theorem NavierStokes.ModulatedProfileAssembly.LoopData.band_target {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) : band d.etaRadius ⊆ d.parameter.target

theorem NavierStokes.ModulatedProfileAssembly.LoopData.parameters_target {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) : d.parameters ⊆ d.parameter.target

theorem NavierStokes.ModulatedProfileAssembly.LoopData.union_full {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) : modulationRegion d.modulation d.etaRadius ∪ followingRegion W d.modulation d.etaRadius ⊆ fullRegion W d.modulation d.etaRadius

theorem NavierStokes.ModulatedProfileAssembly.LoopData.full_positive {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) {p : ProfileHistories.Point} (hp : p ∈ fullRegion W d.modulation d.etaRadius) : 0 < p.1

theorem NavierStokes.ModulatedProfileAssembly.LoopData.boundary_subset {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) : boundaryRegion d.modulation d.etaRadius ⊆ modulationRegion d.modulation d.etaRadius

theorem NavierStokes.ModulatedProfileAssembly.LoopData.exists_realization {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) : Nonempty (ParametricModulation.TrueConeRealization d.a d.m d.p₁ d.p₂ (modulationRegion d.modulation d.etaRadius) (boundaryRegion d.modulation d.etaRadius))

@[reducible, inline]

abbrev NavierStokes.ModulatedProfileAssembly.LoopData.Realization {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) : Type

Realization: an abbreviation for ParametricModulation.TrueConeRealization d.a d.m d.p₁ d.p₂ (modulationRegion d.modulation d.etaRadius) (boundaryRegion d.modulation d.etaRadius).

Equations

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

noncomputable def NavierStokes.ModulatedProfileAssembly.LoopData.angularAux {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) : ProfileHistories.Field

Angular auxiliary, given by d.parameter.E (d.modulation.left / 2).

Equations

• d.angularAux = d.parameter.E (d.modulation.left / 2)

theorem NavierStokes.ModulatedProfileAssembly.LoopData.angularAux_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) : ContDiff ℝ (↑⊤) d.angularAux

theorem NavierStokes.ModulatedProfileAssembly.LoopData.auxiliary_shears {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) {p : ProfileHistories.Point} (hp : p ∈ fullRegion W d.modulation d.etaRadius) : ModulatedCone.angularShear d.angularAux p = ModulatedCone.angularShear W.profiles.E p ∧ ModulatedCone.signedAxialShear d.angularAux d.parameter.U p = ModulatedCone.signedAxialShear W.profiles.E W.profiles.U p

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

Domain, given by restrictDomain W.domain d.parameters d.parameters_open.

Equations

• d.domain = NavierStokes.ModulatedProfileAssembly.restrictDomain W.domain d.parameters ⋯

theorem NavierStokes.ModulatedProfileAssembly.LoopData.domain_nonnegative {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) {p : ProfileHistories.Point} (hX : 0 ≤ p.1) (heta : p.2 ∈ d.parameters) : p ∈ d.domain.carrier

noncomputable def NavierStokes.ModulatedProfileAssembly.LoopData.outputF {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) (r : d.Realization) (N : ℕ) (c : ℝ → ModulatedHistories.Coeff) : ProfileHistories.Field

Output F, constructed using AnnularAuxiliary.transplant.

Equations

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

noncomputable def NavierStokes.ModulatedProfileAssembly.LoopData.outputU {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) (r : d.Realization) (N : ℕ) (c : ℝ → ModulatedHistories.Coeff) : ProfileHistories.Field

Output U, constructed using AnnularAuxiliary.transplant.

Equations

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

theorem NavierStokes.ModulatedProfileAssembly.LoopData.output_outside {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) (r : d.Realization) (N : ℕ) (c : ℝ → ModulatedHistories.Coeff) {p : ProfileHistories.Point} (hp : p.1 ∉ Set.Ioo d.modulation.left (repairPatch W).right) : d.outputF r N c p = W.profiles.f p ∧ d.outputU r N c p = W.profiles.U p

structure NavierStokes.ModulatedProfileAssembly.Witness {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) : Type

A finite, actually solved modulation of W, on an open parameter neighborhood of the complete physical band.

• realization : d.Realization

  Realization of Witness, of type d.Realization.

• frequency : ℕ

  Frequency of Witness, of type ℕ.

• frequency_pos : 0 < self.frequency
• coefficients : ℝ → ModulatedHistories.Coeff

  Coefficients of Witness, of type ℝ → ModulatedHistories.Coeff.

• coefficients_smooth : ContDiff ℝ (↑⊤) self.coefficients
• profiles : ProfileHistories.Profiles d.domain

  Profiles of Witness, of type Profiles d.domain.

• f_formula : self.profiles.f = d.outputF self.realization self.frequency self.coefficients
• U_formula : self.profiles.U = d.outputU self.realization self.frequency self.coefficients
• pressure0 : self.profiles.pressure0 = W.profiles.pressure0
• restored (eta : ℝ) : eta ∈ d.parameters → ∀ (X : ℝ), (repairPatch W).right ≤ X → ModulatedHistories.profileRows self.profiles (X, eta) = ModulatedHistories.profileRows W.profiles (X, eta)
• true_cone (p : ℝ × ℝ) : p ∈ Set.Icc d.modulation.left (repairPatch W).right ×ˢ d.parameters → 0 < self.profiles.f p ∧ TrueConeLoop.InTrueCone (ActivationStocks.profileStockOne self.profiles F.data.h p) (ActivationStocks.profileStockTwo self.profiles F.data.h p) (ModulatedCone.angularShear self.profiles.E p) (ModulatedCone.signedAxialShear self.profiles.E self.profiles.U p)

theorem NavierStokes.ModulatedProfileAssembly.exists_witness {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (d : LoopData W) : Nonempty (Witness d)

theorem NavierStokes.ModulatedProfileAssembly.Witness.same_axis_pressure {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (v : Witness d) : v.profiles.pressure0 = F.axisDatum

theorem NavierStokes.ModulatedProfileAssembly.Witness.fields_outside {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (v : Witness d) {p : ProfileHistories.Point} (hp : p.1 ∉ Set.Ioo d.modulation.left (repairPatch W).right) : v.profiles.f p = W.profiles.f p ∧ v.profiles.U p = W.profiles.U p

theorem NavierStokes.ModulatedProfileAssembly.Witness.rows_before {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (v : Witness d) {X eta : ℝ} (hX : 0 ≤ X) (hbefore : X ≤ d.modulation.left) : ModulatedHistories.profileRows v.profiles (X, eta) = ModulatedHistories.profileRows W.profiles (X, eta)

theorem NavierStokes.ModulatedProfileAssembly.Witness.exterior_pressure {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (v : Witness d) {X eta : ℝ} (heta : eta ∈ d.parameters) (hX : (repairPatch W).right ≤ X) : v.profiles.pressure (X, eta) = W.profiles.pressure (X, eta)

theorem NavierStokes.ModulatedProfileAssembly.Witness.exterior_mass {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (v : Witness d) {X eta : ℝ} (heta : eta ∈ d.parameters) (hX : (repairPatch W).right ≤ X) : v.profiles.M (X, eta) = W.profiles.M (X, eta)

theorem NavierStokes.ModulatedProfileAssembly.Witness.exterior_angular {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (v : Witness d) {X eta : ℝ} (heta : eta ∈ d.parameters) (hX : (repairPatch W).right ≤ X) : v.profiles.I (X, eta) = W.profiles.I (X, eta)

theorem NavierStokes.ModulatedProfileAssembly.Witness.exterior_transport {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (v : Witness d) {X eta : ℝ} (heta : eta ∈ d.parameters) (hX : (repairPatch W).right ≤ X) : v.profiles.J (X, eta) = W.profiles.J (X, eta)

theorem NavierStokes.ModulatedProfileAssembly.Witness.exterior_energy {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (v : Witness d) {X eta : ℝ} (heta : eta ∈ d.parameters) (hX : (repairPatch W).right ≤ X) : v.profiles.S (X, eta) = W.profiles.S (X, eta)

theorem NavierStokes.ModulatedProfileAssembly.Witness.rows_outside {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (v : Witness d) {X eta : ℝ} (hX : 0 ≤ X) (heta : eta ∈ d.parameters) (hout : X ∉ Set.Ioo d.modulation.left (repairPatch W).right) : ModulatedHistories.profileRows v.profiles (X, eta) = ModulatedHistories.profileRows W.profiles (X, eta)

theorem NavierStokes.ModulatedProfileAssembly.Witness.stocks_outside {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (v : Witness d) {p : ProfileHistories.Point} (hX : 0 < p.1) (heta : p.2 ∈ d.parameters) (hout : p.1 ∉ Set.Ioo d.modulation.left (repairPatch W).right) (hf : W.profiles.f p ≠ 0) : ActivationStocks.profileStockOne v.profiles F.data.h p = ActivationStocks.profileStockOne W.profiles F.data.h p ∧ ActivationStocks.profileStockTwo v.profiles F.data.h p = ActivationStocks.profileStockTwo W.profiles F.data.h p

theorem NavierStokes.ModulatedProfileAssembly.Witness.shears_outside {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (v : Witness d) {p : ProfileHistories.Point} (hout : p.1 < d.modulation.left ∨ (repairPatch W).right < p.1) : ModulatedCone.angularShear v.profiles.E p = ModulatedCone.angularShear W.profiles.E p ∧ ModulatedCone.signedAxialShear v.profiles.E v.profiles.U p = ModulatedCone.signedAxialShear W.profiles.E W.profiles.U p

theorem NavierStokes.ModulatedProfileAssembly.Witness.true_cone_from_nominal {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (v : Witness d) {p : ProfileHistories.Point} (hX : 0 < p.1) (heta : p.2 ∈ d.parameters) (hf : W.profiles.f p ≠ 0) (houtside : p.1 < d.modulation.left ∨ (repairPatch W).right < p.1 → TrueConeLoop.InTrueCone (ActivationStocks.profileStockOne W.profiles F.data.h p) (ActivationStocks.profileStockTwo W.profiles F.data.h p) (ModulatedCone.angularShear W.profiles.E p) (ModulatedCone.signedAxialShear W.profiles.E W.profiles.U p)) : TrueConeLoop.InTrueCone (ActivationStocks.profileStockOne v.profiles F.data.h p) (ActivationStocks.profileStockTwo v.profiles F.data.h p) (ModulatedCone.angularShear v.profiles.E p) (ModulatedCone.signedAxialShear v.profiles.E v.profiles.U p)

Outside the finite modulation interval the original true cone is preserved with its actual stocks; inside it the constructed loop supplies the true cone. This can be applied on the entire nominal annulus.

Construction of the loop inputs from actual nominal cone bounds

theorem NavierStokes.ModulatedProfileAssembly.exists_smooth_extension {K O : Set ProfileHistories.Point} (hK : IsCompact K) (hO : IsOpen O) (hKO : K ⊆ O) (f : ProfileHistories.Field) (hf : ContDiffOn ℝ (↑⊤) f O) : ∃ (g : ProfileHistories.Field), ContDiff ℝ (↑⊤) g ∧ Set.EqOn g f K

noncomputable def NavierStokes.ModulatedProfileAssembly.regularDomain {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) : Set ProfileHistories.Point

Regular domain, given by {p | p ∈ D.carrier ∧ 0 < p.1 ∧ 0 < P.f p ∧ 0 < ActivationContinuation.shearA P p ∧ NaturalAxisData.L h p.2 ≠ 0}.

Equations

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

theorem NavierStokes.ModulatedProfileAssembly.regularDomain_open {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) : IsOpen (regularDomain P h)

theorem NavierStokes.ModulatedProfileAssembly.coordinates_smooth {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) : ContDiffOn ℝ (↑⊤) (ActivationContinuation.shearA P) (regularDomain P h) ∧ ContDiffOn ℝ (↑⊤) (NominalConeAssembly.tilt P) (regularDomain P h) ∧ ContDiffOn ℝ (↑⊤) (ReferenceBounds.p1 P h) (regularDomain P h) ∧ ContDiffOn ℝ (↑⊤) (ReferenceBounds.p2 P h) (regularDomain P h)

noncomputable def NavierStokes.ModulatedProfileAssembly.relaxedDomain {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) : Set ProfileHistories.Point

Relaxed domain, given by {p | p ∈ regularDomain P h ∧ ActivationContinuation.IsRelaxed P h p}.

Equations

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

theorem NavierStokes.ModulatedProfileAssembly.relaxedDomain_open {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) : IsOpen (relaxedDomain P h)

noncomputable def NavierStokes.ModulatedProfileAssembly.trueDomain {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) : Set ProfileHistories.Point

True domain, given by {p | p ∈ relaxedDomain P h ∧ NominalConeAssembly.IsTrue P h p}.

Equations

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

theorem NavierStokes.ModulatedProfileAssembly.trueDomain_open {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) : IsOpen (trueDomain P h)

structure NavierStokes.ModulatedProfileAssembly.NominalBounds {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : Type

The remaining analytic input is stated entirely for the given nominal profile and the physical band. No loop, repair, extension or modified profile is assumed.

• modulation : ModulatedHistories.Window

  Modulation of NominalBounds, of type ModulatedHistories.Window.

• after_initial : 4 / W.axis.scale < self.modulation.left
• before_repair : self.modulation.right < (repairPatch W).left
• relaxed (p : ProfileHistories.Point) : p ∈ fullRegion W self.modulation 1 → ActivationContinuation.IsRelaxed W.profiles F.data.h p
• true_boundary (p : ProfileHistories.Point) : p ∈ boundaryRegion self.modulation 1 → NominalConeAssembly.IsTrue W.profiles F.data.h p
• true_following (p : ProfileHistories.Point) : p ∈ followingRegion W self.modulation 1 → NominalConeAssembly.IsTrue W.profiles F.data.h p

theorem NavierStokes.ModulatedProfileAssembly.NominalBounds.regular_of_relaxed {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {p : ProfileHistories.Point} (hX : 0 < p.1) (heta : p.2 ∈ band 1) (hc : ActivationContinuation.IsRelaxed W.profiles F.data.h p) : p ∈ regularDomain W.profiles F.data.h

theorem NavierStokes.ModulatedProfileAssembly.NominalBounds.exists_loopData {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (b : NominalBounds W) : ∃ (d : LoopData W), d.modulation = b.modulation

theorem NavierStokes.ModulatedProfileAssembly.NominalBounds.exists_modulated {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (b : NominalBounds W) : ∃ (d : LoopData W), d.modulation = b.modulation ∧ Nonempty (Witness d)

noncomputable def NavierStokes.ModulatedProfileAssembly.Witness.slowParameters {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (_v : Witness d) : Set ℝ

Slow parameters, given by d.parameters ∩ AssembledSlowBase.nominalParameters W.

Equations

• _v.slowParameters = d.parameters ∩ NavierStokes.AssembledSlowBase.nominalParameters W

theorem NavierStokes.ModulatedProfileAssembly.Witness.finiteModification {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (v : Witness d) : AssembledSlowBase.FiniteModification W v.profiles v.slowParameters d.modulation.left (repairPatch W).right

The consumer certificate is proved for this actual finite profile. The slow hierarchy can therefore be reconstructed from the same W.

theorem NavierStokes.ModulatedProfileAssembly.Witness.slow_outer_angular {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (v : Witness d) {eta : ℝ} (heta : eta ∈ v.slowParameters) : v.profiles.I (AssembledSlowBase.nominalOuterX W, eta) = W.profiles.I (AssembledSlowBase.nominalOuterX W, eta)

The additional angular anchor needed by the first-order exterior stress argument is retained alongside the finite-modification certificate.

theorem NavierStokes.ModulatedProfileAssembly.Witness.positive_f {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (v : Witness d) {p : ProfileHistories.Point} (hX : 0 < p.1) (heta : p.2 ∈ Set.Icc (-1) 1) : 0 < v.profiles.f p

theorem NavierStokes.ModulatedProfileAssembly.Witness.positive_E {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : LoopData W} (v : Witness d) {p : ProfileHistories.Point} (hX : 0 < p.1) (heta : p.2 ∈ Set.Icc (-1) 1) : 0 < v.profiles.E p

Bind the constructed profile to the completed nominal cone theorem

noncomputable def NavierStokes.ModulatedProfileAssembly.holdRadius {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : ℝ

Hold radius, given by W.controls.radius * Real.exp F.data.core.holdStart.

Equations

• NavierStokes.ModulatedProfileAssembly.holdRadius W = W.controls.radius * Real.exp F.data.core.holdStart

theorem NavierStokes.ModulatedProfileAssembly.holdRadius_gt_radius {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : W.controls.radius < holdRadius W

theorem NavierStokes.ModulatedProfileAssembly.holdRadius_before_repair {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : holdRadius W < (repairPatch W).left

theorem NavierStokes.ModulatedProfileAssembly.repairPatch_before_activeRight {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : (repairPatch W).right < NominalConeAssembly.activeRight W

theorem NavierStokes.ModulatedProfileAssembly.nominalBounds_of_certificate {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (hW : NominalConeAssembly.Certificate W) : ∃ (b : NominalBounds W), ∀ (p : ProfileHistories.Point), NominalConeAssembly.activeLeft W < p.1 → p.1 < NominalConeAssembly.activeRight W → p.2 ∈ Set.Icc (-1) 1 → p.1 < b.modulation.left ∨ (repairPatch W).right < p.1 → NominalConeAssembly.IsTrue W.profiles F.data.h p

theorem NavierStokes.ModulatedProfileAssembly.exists_of_certificate {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (hW : NominalConeAssembly.Certificate W) : ∃ (d : LoopData W) (v : Witness d), ∀ (p : ProfileHistories.Point), NominalConeAssembly.activeLeft W < p.1 → p.1 < NominalConeAssembly.activeRight W → p.2 ∈ Set.Icc (-1) 1 → TrueConeLoop.InTrueCone (ActivationStocks.profileStockOne v.profiles F.data.h p) (ActivationStocks.profileStockTwo v.profiles F.data.h p) (ModulatedCone.angularShear v.profiles.E p) (ModulatedCone.signedAxialShear v.profiles.E v.profiles.U p)

One actual modulated physical profile of the fixed nominal witness, with the true cone on its whole active annulus. The nominal certificate constructs every input of the finite modulation theorem.

theorem NavierStokes.ModulatedProfileAssembly.exists_modulated_profile : ∃ (F : OutgoingProfile.Profile) (W : NominalProfile.Witness F) (d : LoopData W) (v : Witness d), ∀ (p : ProfileHistories.Point), NominalConeAssembly.activeLeft W < p.1 → p.1 < NominalConeAssembly.activeRight W → p.2 ∈ Set.Icc (-1) 1 → TrueConeLoop.InTrueCone (ActivationStocks.profileStockOne v.profiles F.data.h p) (ActivationStocks.profileStockTwo v.profiles F.data.h p) (ModulatedCone.angularShear v.profiles.E p) (ModulatedCone.signedAxialShear v.profiles.E v.profiles.U p)

The already constructed nominal cone theorem supplies a concrete profile, its actual finite modulation, and the full active true cone.