Cone coordinates of one actual nominal profile

The physical coordinates below are computed from the genuine smooth profile and its axis-integrated histories. The outgoing convention for axial shear has the opposite sign to the signed shear used by the modulation theorem.

Cone bounds through the shape transition and moment repair

The source estimates use the actual fields and their radial averages. The large natural logarithmic gradient is retained in the growing term rather than estimated by an absolute constant.

theorem NavierStokes.MatchingConeBounds.logShape_hasDerivAt (eta : ℝ) : HasDerivAt ShapeTransition.logShape (-OutgoingEntranceCone.shapeGradient eta) eta

theorem NavierStokes.MatchingConeBounds.shape_axis_lower {h j eta ell theta : ℝ} (hs : NaturalAxisData.SmallParameters h j) (hη : eta ∈ Set.Icc (-1) 1) (hl : 11 / 20 ≤ ell) (ht : theta ∈ Set.Icc 0 1) : 8 / 5 < -NaturalAxisData.W h j eta * ell - h * (1 - 2 * eta * NaturalAxisData.U j eta) + theta * NaturalAxisData.H h j eta * OutgoingEntranceCone.shapeGradient eta

noncomputable def NavierStokes.MatchingConeBounds.shapeRemainder (h j sigma eta theta ell : ℝ) (v : Fin 5 → ℝ) (t : ℝ) : ℝ

Shape remainder as an element of ℝ.

Equations

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

@[reducible, inline]

abbrev NavierStokes.MatchingConeBounds.ShapeParameter (B : ℝ) : Type

Shape parameter: an abbreviation for Icc (-1 : ℝ) 1 × (Icc (0 : ℝ) 1 × (Icc (11 / 20 : ℝ) (13 / 20) × ReferenceBounds.BoundedJets B)).

Equations

• NavierStokes.MatchingConeBounds.ShapeParameter B = (↑(Set.Icc (-1) 1) × ↑(Set.Icc 0 1) × ↑(Set.Icc (11 / 20) (13 / 20)) × ↑(NavierStokes.ReferenceBounds.BoundedJets B))

noncomputable def NavierStokes.MatchingConeBounds.shapeModel (h j sigma B : ℝ) (p : ShapeParameter B) (t : ℝ) : ℝ

Shape model, given by shapeRemainder h j sigma p.1.val p.2.1.val p.2.2.1.val p.2.2.2.val t.

Equations

• NavierStokes.MatchingConeBounds.shapeModel h j sigma B p t = NavierStokes.MatchingConeBounds.shapeRemainder h j sigma (↑p.1) (↑p.2.1) (↑p.2.2.1) (↑p.2.2.2) t

theorem NavierStokes.MatchingConeBounds.shapeModel_continuous (h j B : ℝ) {sigma : ℝ} (hsigma : 0 < sigma) : Continuous fun (p : ShapeParameter B × ℝ) => shapeModel h j sigma B p.1 p.2

theorem NavierStokes.MatchingConeBounds.shapeModel_zero_lower {h j sigma B : ℝ} (hs : NaturalAxisData.SmallParameters h j) (hsigma : 0 < sigma) (p : ShapeParameter B) (hz : (1 - ↑p.2.1) * NaturalAxisData.L h ↑p.1 * NaturalAxisData.chi h j sigma ↑p.1 = 0) : 3 / 2 < shapeModel h j sigma B p 0

theorem NavierStokes.MatchingConeBounds.shapeModel_uniform_lower {h j sigma : ℝ} (hs : NaturalAxisData.SmallParameters h j) (hsigma : 0 < sigma) (B : ℝ) : ∃ (M : ℝ), 0 < M ∧ ∀ (Λ : ℝ), M ≤ Λ → ∀ (p : ShapeParameter B), 5 / 4 < Λ * ((1 - ↑p.2.1) * NaturalAxisData.L h ↑p.1 * NaturalAxisData.chi h j sigma ↑p.1) + shapeModel h j sigma B p (1 / Λ)

noncomputable def NavierStokes.MatchingConeBounds.shapeJet {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (_h j Λ g : ℝ) (p : ProfileHistories.Point) : Fin 5 → ℝ

Shape jet, given by ![1, Λ * (P.U p - U j p.2), Λ * (P.Ubar p - U j p.2), Λ * (average (parameterPartial P.U) p - 4), g].

Equations

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

theorem NavierStokes.MatchingConeBounds.shapeSource_identity {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h j sigma Λ theta ell g : ℝ) (hΛ : Λ ≠ 0) (p : ProfileHistories.Point) (hl : ReferenceBounds.logSlope P p = ell) (hg : ProfileHistories.parameterPartial P.f p / P.f p = (1 - theta) * (Λ * NaturalAxisCoefficients.realGradient h j sigma p.2 + g) - theta * OutgoingEntranceCone.shapeGradient p.2) : ReferenceBounds.sourceQ P h p = Λ * ((1 - theta) * NaturalAxisData.L h p.2 * NaturalAxisData.chi h j sigma p.2) + shapeRemainder h j sigma p.2 theta ell (shapeJet P h j Λ g p) (1 / Λ)

theorem NavierStokes.MatchingConeBounds.actual_shape_source_threshold {h j sigma B : ℝ} (hs : NaturalAxisData.SmallParameters h j) (hsigma : 0 < sigma) (hB : 1 ≤ B) : ∃ (M : ℝ), 0 < M ∧ ∀ (Λ : ℝ), M ≤ Λ → ∀ {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ProfileHistories.Point) (theta ell g : ℝ), p.2 ∈ Set.Icc (-1) 1 → theta ∈ Set.Icc 0 1 → ell ∈ Set.Icc (11 / 20) (13 / 20) → ReferenceBounds.logSlope P p = ell → ProfileHistories.parameterPartial P.f p / P.f p = (1 - theta) * (Λ * NaturalAxisCoefficients.realGradient h j sigma p.2 + g) - theta * OutgoingEntranceCone.shapeGradient p.2 → |Λ * (P.U p - NaturalAxisData.U j p.2)| ≤ B → |Λ * (P.Ubar p - NaturalAxisData.U j p.2)| ≤ B → |Λ * (ProfileHistories.average (ProfileHistories.parameterPartial P.U) p - 4)| ≤ B → |g| ≤ B → 5 / 4 < ReferenceBounds.sourceQ P h p

Uniform positivity for the literal convex interpolation of the old and target parameter gradients. The hypotheses concern only low-order actual field jets; no angular-stock or cone estimate is assumed.

noncomputable def NavierStokes.MatchingConeBounds.angularGap {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h eta X : ℝ) : ℝ

Angular gap, given by primitive (P.angularSource h) (X, eta) - 2 * L h eta * P.H (X, eta).

Equations

• NavierStokes.MatchingConeBounds.angularGap P h eta X = NavierStokes.ProfileHistories.primitive (P.angularSource h) (X, eta) - 2 * NavierStokes.NaturalAxisData.L h eta * P.H (X, eta)

theorem NavierStokes.MatchingConeBounds.angularGap_hasDerivAt {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) {eta X : ℝ} (hp : (X, eta) ∈ D.carrier) : HasDerivAt (angularGap P h eta) (P.angularSource h (X, eta) - 2 * NaturalAxisData.L h eta * ProfileHistories.radialPartial P.H (X, eta)) X

theorem NavierStokes.MatchingConeBounds.angular_barrier {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {h eta a X : ℝ} (ha : 2 ≤ a) (haX : a ≤ X) (hL : 0 < NaturalAxisData.L h eta) (hL1 : NaturalAxisData.L h eta ≤ 1) (hmem : ∀ s ∈ Set.Icc a X, (s, eta) ∈ D.carrier) (hf : ∀ s ∈ Set.Icc a X, 0 < P.f (s, eta)) (hl : ∀ s ∈ Set.Icc a X, ReferenceBounds.logSlope P (s, eta) ≤ 1) (hq : ∀ s ∈ Set.Icc a X, 1 < ReferenceBounds.sourceQ P h (s, eta)) (hinit : 2 < ReferenceBounds.p1 P h (a, eta)) : 2 < ReferenceBounds.p1 P h (X, eta)

A barrier with a variable logarithmic slope. It uses the actual source primitive and the actual integrating factor H.

theorem NavierStokes.MatchingConeBounds.shape_relaxed_from_source {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {h eta a X : ℝ} (ha : 2 ≤ a) (haX : a ≤ X) (hL : 0 < NaturalAxisData.L h eta) (hL1 : NaturalAxisData.L h eta ≤ 1) (hmem : ∀ s ∈ Set.Icc a X, (s, eta) ∈ D.carrier) (hf : ∀ s ∈ Set.Icc a X, 0 < P.f (s, eta)) (hl : ∀ s ∈ Set.Icc a X, ReferenceBounds.logSlope P (s, eta) ∈ Set.Icc (11 / 20) (13 / 20)) (hq : ∀ s ∈ Set.Icc a X, 1 < ReferenceBounds.sourceQ P h (s, eta)) (hinit : 2 < ReferenceBounds.p1 P h (a, eta)) (hu : ProfileHistories.radialPartial P.U (X, eta) = 0) : ActivationContinuation.IsRelaxed P h (X, eta)

theorem NavierStokes.MatchingConeBounds.axial_error_jet {J K : Set ℝ} (R : TransitionRamp.StockReference J) (hJ : IsOpen J) (hKJ : K ⊆ J) {N : ℕ} {eps T kappa wU wE y eta : ℝ} (hb : 0 ≤ R.bigTime) (hwU : 0 < wU) (hwE : 0 < wE) (hc : R.SmallLogControl K N eps T kappa wU wE) (hy : 0 ≤ y) (hη : eta ∈ K) {n : ℕ} (hn : n ≤ N) : |iteratedDeriv n (fun (e : ℝ) => R.axialVelocity T kappa wU (y, e) - R.initialU e) eta| ≤ eps

theorem NavierStokes.MatchingConeBounds.seedU_error_jets {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {N : ℕ} {eps X eta : ℝ} (hc : MatchingDebtBounds.SmallControl c N eps) (heps : 0 ≤ eps) (hX : 0 ≤ X) (hη : eta ∈ Set.Icc (-1) 1) {n : ℕ} (hn : n ≤ N) : |iteratedDeriv n (fun (e : ℝ) => c.seedU (X, e) - NaturalAxisData.U A.j e) eta| ≤ ReferenceJetBounds.jetConstant A.preparation.inputs.coefficients 0 n / A.scale + eps

theorem NavierStokes.MatchingConeBounds.seedU_scaled_error_jets {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {N : ℕ} {eps X eta : ℝ} (hc : MatchingDebtBounds.SmallControl c N eps) (heps : 0 ≤ eps) (hX : 0 ≤ X) (hη : eta ∈ Set.Icc (-1) 1) {n : ℕ} (hn : n ≤ N) : |A.scale * iteratedDeriv n (fun (e : ℝ) => c.seedU (X, e) - NaturalAxisData.U A.j e) eta| ≤ ReferenceJetBounds.jetConstant A.preparation.inputs.coefficients 0 n + A.scale * eps

theorem NavierStokes.MatchingConeBounds.initialShape_gradient_bound {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {N : ℕ} {eps eta : ℝ} (hc : MatchingDebtBounds.SmallControl c N eps) (hN : 1 ≤ N) (hscale : AxisReference.stabilityScale A.preparation.inputs.coefficients.epsilon (NaturalProfile.profileErrorConstant A.preparation.inputs) ≤ A.scale) (hη : eta ∈ Set.Icc (-1) 1) : |deriv c.initialShape eta - A.scale * NaturalAxisCoefficients.realGradient F.data.h A.j A.preparation.sigma eta| ≤ 8 * ReferenceJetBounds.jetConstant A.preparation.inputs.coefficients 0 1 + eps

theorem NavierStokes.MatchingConeBounds.seedU_source_jets {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {N : ℕ} {eps X eta : ℝ} (hc : MatchingDebtBounds.SmallControl c N eps) (heps : 0 ≤ eps) (hN : 1 ≤ N) (hX : 0 ≤ X) (hη : eta ∈ Set.Icc (-1) 1) : |A.scale * (c.seedU (X, eta) - NaturalAxisData.U A.j eta)| ≤ ReferenceJetBounds.jetConstant A.preparation.inputs.coefficients 0 0 + A.scale * eps ∧ |A.scale * (ProfileHistories.parameterPartial c.seedU (X, eta) - 4)| ≤ ReferenceJetBounds.jetConstant A.preparation.inputs.coefficients 0 1 + A.scale * eps

theorem NavierStokes.MatchingConeBounds.profiles_before_restore {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : ProfileHistories.Point} (hX : p.1 ≤ c.radius * Real.exp (-8)) : (c.profiles hsep).U p = c.seedU p ∧ (c.profiles hsep).f p = c.shapedF p

theorem NavierStokes.MatchingConeBounds.profiles_source_jets {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {N : ℕ} {eps X eta : ℝ} (hc : MatchingDebtBounds.SmallControl c N eps) (heps : 0 ≤ eps) (hN : 1 ≤ N) (hX : 0 ≤ X) (hR : X ≤ c.radius * Real.exp (-8)) (hη : eta ∈ Set.Icc (-1) 1) (hsmall : NominalProfile.SmallDebt F c.debt eta) : |A.scale * ((c.profiles hsep).U (X, eta) - NaturalAxisData.U A.j eta)| ≤ ReferenceJetBounds.jetConstant A.preparation.inputs.coefficients 0 0 + A.scale * eps ∧ |A.scale * ((c.profiles hsep).Ubar (X, eta) - NaturalAxisData.U A.j eta)| ≤ ReferenceJetBounds.jetConstant A.preparation.inputs.coefficients 0 0 + A.scale * eps ∧ |A.scale * (ProfileHistories.average (ProfileHistories.parameterPartial (c.profiles hsep).U) (X, eta) - 4)| ≤ ReferenceJetBounds.jetConstant A.preparation.inputs.coefficients 0 1 + A.scale * eps

theorem NavierStokes.MatchingConeBounds.deriv_eqOn_Ici {f g : ℝ → ℝ} {a x : ℝ} (hx : a ≤ x) (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (he : Set.EqOn f g (Set.Ici a)) : deriv f x = deriv g x

theorem NavierStokes.MatchingConeBounds.deriv_eqOn_Iic {f g : ℝ → ℝ} {a x : ℝ} (hx : x ≤ a) (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (he : Set.EqOn f g (Set.Iic a)) : deriv f x = deriv g x

noncomputable def NavierStokes.MatchingConeBounds.shapeValue (C T : ℝ) (li : ℝ → ℝ) (X eta : ℝ) : ℝ

Shape value, given by ShapeTransition.angular C T li (Real.log (X / NominalProfile.Xi), eta) / Real.sqrt (2 * X).

Equations

• NavierStokes.MatchingConeBounds.shapeValue C T li X eta = NavierStokes.ShapeTransition.angular C T li (Real.log (X / NavierStokes.NominalProfile.Xi), eta) / √(2 * X)

theorem NavierStokes.MatchingConeBounds.shapeValue_hasDerivAt_x (C T : ℝ) (li : ℝ → ℝ) {X : ℝ} (hX : 0 < X) (eta : ℝ) : HasDerivAt (fun (s : ℝ) => shapeValue C T li s eta) (shapeValue C T li X eta * (ShapeTransition.logarithmicSlope T li (Real.log (X / NominalProfile.Xi), eta) - 1) / X) X

theorem NavierStokes.MatchingConeBounds.shapeValue_hasDerivAt_eta (C T : ℝ) {li : ℝ → ℝ} {X eta : ℝ} (hli : DifferentiableAt ℝ li eta) : HasDerivAt (shapeValue C T li X) (shapeValue C T li X eta * ((1 - OutgoingSchedule.sigma (Real.log (X / NominalProfile.Xi) / T)) * deriv li eta - OutgoingSchedule.sigma (Real.log (X / NominalProfile.Xi) / T) * OutgoingEntranceCone.shapeGradient eta)) eta

theorem NavierStokes.MatchingConeBounds.shapedF_value {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) {X eta : ℝ} (hX : NominalProfile.Xi ≤ X) (hη : eta ∈ ReferencePath.parameterInterval) : c.shapedF (X, eta) = shapeValue A.normalization c.shapeTime c.initialShape X eta

theorem NavierStokes.MatchingConeBounds.profiles_shape_value {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {X eta : ℝ} (hX : NominalProfile.Xi ≤ X) (hR : X ≤ c.radius * Real.exp (-8)) (hη : eta ∈ ReferencePath.parameterInterval) : (c.profiles hsep).f (X, eta) = shapeValue A.normalization c.shapeTime c.initialShape X eta

theorem NavierStokes.MatchingConeBounds.profiles_shape_positive {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {X eta : ℝ} (hX : 0 ≤ X) (hR : X ≤ c.radius * Real.exp (-8)) (hη : eta ∈ ReferencePath.parameterInterval) : 0 < (c.profiles hsep).f (X, eta)

theorem NavierStokes.MatchingConeBounds.profiles_shape_radialU {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {X eta : ℝ} (hX : NominalProfile.Xi ≤ X) (hR : X ≤ c.radius * Real.exp (-8)) (hη : eta ∈ ReferencePath.parameterInterval) (hsmall : NominalProfile.SmallDebt F c.debt eta) : ProfileHistories.radialPartial (c.profiles hsep).U (X, eta) = 0

theorem NavierStokes.MatchingConeBounds.profiles_shape_radialF {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {X eta : ℝ} (hX : NominalProfile.Xi ≤ X) (hR : X ≤ c.radius * Real.exp (-8)) (hη : eta ∈ ReferencePath.parameterInterval) (hsmall : NominalProfile.SmallDebt F c.debt eta) : ProfileHistories.radialPartial (c.profiles hsep).f (X, eta) = (c.profiles hsep).f (X, eta) * (ShapeTransition.logarithmicSlope c.shapeTime c.initialShape (Real.log (X / NominalProfile.Xi), eta) - 1) / X

theorem NavierStokes.MatchingConeBounds.profiles_shape_logSlope {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {X eta : ℝ} (hX : NominalProfile.Xi ≤ X) (hR : X ≤ c.radius * Real.exp (-8)) (hη : eta ∈ ReferencePath.parameterInterval) (hsmall : NominalProfile.SmallDebt F c.debt eta) : ReferenceBounds.logSlope (c.profiles hsep) (X, eta) = ShapeTransition.logarithmicSlope c.shapeTime c.initialShape (Real.log (X / NominalProfile.Xi), eta)

theorem NavierStokes.MatchingConeBounds.profiles_shape_gradient {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {X eta : ℝ} (hX : NominalProfile.Xi ≤ X) (hR : X ≤ c.radius * Real.exp (-8)) (hη : eta ∈ ReferencePath.parameterInterval) (hsmall : NominalProfile.SmallDebt F c.debt eta) : ProfileHistories.parameterPartial (c.profiles hsep).f (X, eta) / (c.profiles hsep).f (X, eta) = (1 - OutgoingSchedule.sigma (Real.log (X / NominalProfile.Xi) / c.shapeTime)) * deriv c.initialShape eta - OutgoingSchedule.sigma (Real.log (X / NominalProfile.Xi) / c.shapeTime) * OutgoingEntranceCone.shapeGradient eta

noncomputable def NavierStokes.MatchingConeBounds.shapeConstant {F : OutgoingProfile.Profile} {j : ℝ} (prep : NominalProfile.AxisPreparation F j) : ℝ

Shape constant, given by 1 + ReferenceJetBounds.jetConstant prep.inputs.coefficients 0 0 + 9 * ReferenceJetBounds.jetConstant prep.inputs.coefficients 0 1.

Equations

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

theorem NavierStokes.MatchingConeBounds.shapeConstant_one {F : OutgoingProfile.Profile} {j : ℝ} (prep : NominalProfile.AxisPreparation F j) : 1 ≤ shapeConstant prep

noncomputable def NavierStokes.MatchingConeBounds.shapeScale {F : OutgoingProfile.Profile} {j : ℝ} (hj : NaturalAxisData.SmallParameters F.data.h j) (prep : NominalProfile.AxisPreparation F j) : ℝ

The shape-source scale depends on the fixed natural-axis data, before the normalization or continuation controls are chosen.

Equations

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

theorem NavierStokes.MatchingConeBounds.shapeScale_one {F : OutgoingProfile.Profile} {j : ℝ} (hj : NaturalAxisData.SmallParameters F.data.h j) (prep : NominalProfile.AxisPreparation F j) : 1 ≤ shapeScale hj prep

theorem NavierStokes.MatchingConeBounds.actual_shape_source {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {eps X eta : ℝ} (hscale : shapeScale ⋯ A.preparation ≤ A.scale) (hc : MatchingDebtBounds.SmallControl c 1 eps) (heps : 0 ≤ eps) (heps1 : eps ≤ min 1 (1 / A.scale)) (hX : NominalProfile.Xi ≤ X) (hR : X ≤ c.radius * Real.exp (-8)) (hη : eta ∈ Set.Icc (-1) 1) (hsmall : NominalProfile.SmallDebt F c.debt eta) (hl : ReferenceBounds.logSlope (c.profiles hsep) (X, eta) ∈ Set.Icc (11 / 20) (13 / 20)) : 5 / 4 < ReferenceBounds.sourceQ (c.profiles hsep) F.data.h (X, eta)

theorem NavierStokes.MatchingConeBounds.actual_shape_relaxed {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {N : ℕ} {rho eps X eta : ℝ} (hm : MatchingDebtBounds.MatchingBounds c N rho) (hrho : rho ≤ NominalProfile.resetSolver.radius) (hscale : shapeScale ⋯ A.preparation ≤ A.scale) (hc : MatchingDebtBounds.SmallControl c 1 eps) (heps : 0 ≤ eps) (heps1 : eps ≤ min 1 (1 / A.scale)) (hX : NominalProfile.Xi ≤ X) (hR : X ≤ c.radius * Real.exp (-8)) (hη : eta ∈ Set.Icc (-1) 1) (hinit : 2 < ReferenceBounds.p1 (c.profiles hsep) F.data.h (NominalProfile.Xi, eta)) : 2 < ReferenceBounds.p1 (c.profiles hsep) F.data.h (X, eta) ∧ ActivationContinuation.IsRelaxed (c.profiles hsep) F.data.h (X, eta)

The actual shape interval satisfies the relaxed cone. The sole stock input is the incoming value at Xi, supplied by the same continuation witness; the angular source and its propagation are proved here.

structure NavierStokes.MatchingConeBounds.PreparedBounds {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (N : ℕ) (rho delta radiusFloor : ℝ) : Prop

Quantitative inputs for the shape and repair regions, obtained together from one continuation. The endpoint drift is controlled separately from the vanishing prefix debt.

• matching : MatchingDebtBounds.MatchingBounds c N rho
• debt_radius : rho ≤ NominalProfile.resetSolver.radius
• scale_large : shapeScale ⋯ A.preparation ≤ A.scale
• control : MatchingDebtBounds.SmallControl c 1 (min 1 (1 / A.scale))
• radius_large : radiusFloor ≤ c.radius
• coefficients : JetBounds.FiniteJetBound N (NominalProfile.resetCoefficients F c.debt) (Set.Icc (-1) 1) delta
• endpoint (eta : ℝ) : eta ∈ Set.Icc (-1) 1 → ∀ n ≤ N, |iteratedDeriv n (fun (e : ℝ) => c.initialAxial e - 4 * e) eta| ≤ delta

theorem NavierStokes.MatchingConeBounds.PreparedBounds.shape_relaxed {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} {c : NominalProfile.Controls A} {N : ℕ} {rho delta radiusFloor : ℝ} (hb : PreparedBounds c N rho delta radiusFloor) {X eta : ℝ} (hX : NominalProfile.Xi ≤ X) (hR : X ≤ c.radius * Real.exp (-8)) (hη : eta ∈ Set.Icc (-1) 1) (hinit : 2 < ReferenceBounds.p1 (c.profiles ⋯) F.data.h (NominalProfile.Xi, eta)) : ActivationContinuation.IsRelaxed (c.profiles ⋯) F.data.h (X, eta)

theorem NavierStokes.MatchingConeBounds.exists_ordered_prepared_continuation (F : OutgoingProfile.Profile) (N : ℕ) (hN : 1 ≤ N) {delta : ℝ} (hdelta : 0 < delta) (radiusFloor : ℝ) : ∃ (rho : ℝ), 0 < rho ∧ ∃ (jcap : ℝ), 0 < jcap ∧ jcap ≤ 1 ∧ ∀ (j : ℝ), |j| ≤ jcap → ∀ (hj : NaturalAxisData.SmallParameters F.data.h j) (prep : NominalProfile.AxisPreparation F j) (nu : ℝ), 0 < nu → (∀ eta ∈ Set.Icc (-1) 1, |NaturalAxisData.Z F.data.h j F.axisDatum eta| ≤ nu → 99 / 100 < NaturalAxisData.chi F.data.h j prep.sigma eta) → ∃ (Λ0 : ℝ), 1 ≤ Λ0 ∧ ∀ (Λ : ℝ) (hΛ : 0 < Λ), Λ0 ≤ Λ → ∃ (T : ℝ) (hT : 0 < T) (C0 : ℝ), 1 ≤ C0 ∧ ∀ (C : ℝ), C0 ≤ C → ∃ (hΛlarge : prep.scaleBound ≤ Λ) (hClarge : NaturalEntrance.entranceNormalization prep.inputs Λ prep.delta ≤ C) (E : NaturalEntrance.EntranceProfile prep.inputs Λ C), ∀ (J : ℕ) (epsilon : ℝ), 0 < epsilon → ∃ (tolerance : ℝ), 0 < tolerance ∧ tolerance ≤ epsilon ∧ ∃ (w : ActivationContinuation.ContinuationWitness E hΛ hj ⋯ (max N J) tolerance), let A := NominalProfile.AxisStage.ofEntrance hj prep Λ C hΛlarge hClarge E; have c := NominalProfile.Controls.ofContinuation A w T hT; PreparedBounds c N rho delta radiusFloor

Ordered common-witness selection. The repair tolerance and requested finite jet order are fixed before j; the source and endpoint scales are fixed before C. Every sufficiently large C works. The same entrance profile then supports every later finite control order and tolerance.

structure NavierStokes.MatchingConeBounds.PreparedWitness (F : OutgoingProfile.Profile) (N : ℕ) (delta radiusFloor : ℝ) : Type

The actual entrance profile and continuation are stored, so subsequent cone gluing uses the same controls that produced the small repair debt.

• axis : NominalProfile.AxisStage F

  Axis of PreparedWitness, of type NominalProfile.AxisStage F.

• order : ℕ

  Order of PreparedWitness, of type ℕ.

• order_ge : N ≤ self.order
• tolerance : ℝ

  Tolerance of PreparedWitness, of type ℝ.

• tolerance_pos : 0 < self.tolerance
• continuation : ActivationContinuation.ContinuationWitness self.axis.natural ⋯ ⋯ ⋯ self.order self.tolerance

  Continuation supplied by PreparedWitness.

• shapeTime : ℝ

  Shape time of PreparedWitness, of type ℝ.

• shapeTime_pos : 0 < self.shapeTime
• rho : ℝ

  Rho of PreparedWitness, of type ℝ.

• rho_pos : 0 < self.rho
• bounds : PreparedBounds (NominalProfile.Controls.ofContinuation self.axis self.continuation self.shapeTime ⋯) N self.rho delta radiusFloor

noncomputable def NavierStokes.MatchingConeBounds.PreparedWitness.controls {F : OutgoingProfile.Profile} {N : ℕ} {delta radiusFloor : ℝ} (W : PreparedWitness F N delta radiusFloor) : NominalProfile.Controls W.axis

Controls, given by NominalProfile.Controls.ofContinuation W.axis W.continuation W.shapeTime W.shapeTime_pos.

Equations

• W.controls = NavierStokes.NominalProfile.Controls.ofContinuation W.axis W.continuation W.shapeTime ⋯

theorem NavierStokes.MatchingConeBounds.preparedWitness_exists (F : OutgoingProfile.Profile) (hP : 2 ≤ F.data.core.P) (hh : F.data.h ≤ 1 / 1000) (N : ℕ) (hN : 1 ≤ N) {delta : ℝ} (hdelta : 0 < delta) (radiusFloor : ℝ) : Nonempty (PreparedWitness F N delta radiusFloor)

The final j, axis preparation, scale, normalization and continuation are chosen in their required order. The incoming cone witness remains part of the output, rather than being replaced by unrelated fields.

A common scheduled profile below caller-supplied parameter bounds

The reset coefficient bound is selected before lambda. The caller's lambda cap is intersected with the existing reset and energy thresholds before any profile is constructed. The actual core is then fixed before choosing h.

theorem NavierStokes.ScheduledProfileChoice.exists_scheduled_core_below (P m : ℝ) (hP : 0 < P) (hm : 0 < m) (cap : ℝ → ℝ) (hcap : ∀ (K : ℝ), 0 < K → 0 < cap K) : ∃ (K : ℝ) (B : ℝ) (core : OutgoingSchedule.Parameters), 0 < K ∧ 0 < B ∧ core.P = P ∧ core.m = m ∧ core.wait = 60 * Real.log (1 / core.lam) ∧ core.lam < cap K ∧ core.lam < 1 / 120 ∧ ∀ (h : ℝ), 0 < h → 2 * h < core.lam → ∃ (F : OutgoingProfile.Profile), F.data.core = core ∧ F.data.h = h ∧ F.coefficientBound = K ∧ ExtendedHeatedOutgoing.ScheduleBounds F ∧ OutgoingProfile.Specification F B

The actual core and reset bound precede every subsequent height choice.

theorem NavierStokes.ScheduledProfileChoice.exists_scheduled_profile_below (P m : ℝ) (hP : 0 < P) (hm : 0 < m) (cap : ℝ → ℝ) (hcap : ∀ (K : ℝ), 0 < K → 0 < cap K) : ∃ (K : ℝ) (lam : ℝ) (B : ℝ), 0 < K ∧ 0 < lam ∧ lam < cap K ∧ lam < 1 / 120 ∧ 0 < B ∧ ∀ (h : ℝ), 0 < h → 2 * h < lam → ∃ (F : OutgoingProfile.Profile), F.data.core.P = P ∧ F.data.core.m = m ∧ F.data.core.lam = lam ∧ F.data.h = h ∧ F.coefficientBound = K ∧ ExtendedHeatedOutgoing.ScheduleBounds F ∧ OutgoingProfile.Specification F B

A scalar-parameter form of the same construction, with the reset bound retained as an explicit preceding existential.

noncomputable def NavierStokes.ScheduledProfileChoice.heightCap (core : OutgoingSchedule.Parameters) (extra : ℝ) : ℝ

This number depends on the already fixed core and an additional caller height bound. It is chosen before the terminal exponent h.

Equations

• NavierStokes.ScheduledProfileChoice.heightCap core extra = min (core.lam / 4) (min extra (min (1 / 1000) (min (1 / 4) (1 / (1 + NavierStokes.TerminalCone.releaseBudget core)))))

theorem NavierStokes.ScheduledProfileChoice.heightCap_pos (core : OutgoingSchedule.Parameters) {extra : ℝ} (he : 0 < extra) : 0 < heightCap core extra

theorem NavierStokes.ScheduledProfileChoice.heightCap_bounds (core : OutgoingSchedule.Parameters) (extra : ℝ) : 2 * heightCap core extra < core.lam ∧ heightCap core extra ≤ extra ∧ heightCap core extra ≤ 1 / 1000 ∧ heightCap core extra ≤ 1 / 4 ∧ heightCap core extra ≤ 1 / (1 + TerminalCone.releaseBudget core)

theorem NavierStokes.ScheduledProfileChoice.exists_scheduled_family_below (P m : ℝ) (hP : 0 < P) (hm : 0 < m) (cap : ℝ → ℝ) (hcap : ∀ (K : ℝ), 0 < K → 0 < cap K) (extraHeight : OutgoingSchedule.Parameters → ℝ) (hextra : ∀ (core : OutgoingSchedule.Parameters), 0 < extraHeight core) : ∃ (K : ℝ) (B : ℝ) (H : ℝ) (core : OutgoingSchedule.Parameters), 0 < K ∧ 0 < B ∧ 0 < H ∧ core.P = P ∧ core.m = m ∧ core.wait = 60 * Real.log (1 / core.lam) ∧ core.lam < cap K ∧ core.lam < 1 / 120 ∧ 2 * H < core.lam ∧ H ≤ extraHeight core ∧ H ≤ 1 / 1000 ∧ ∀ (h : ℝ), 0 < h → h ≤ H → ∃ (F : OutgoingProfile.Profile), F.data.core = core ∧ F.data.h = h ∧ F.coefficientBound = K ∧ ExtendedHeatedOutgoing.ScheduleBounds F ∧ OutgoingProfile.Specification F B ∧ TerminalCone.SmallTail F.data

The common lambda and all height caps are fixed before h and before the actual reset/Profile. The additional cap may impose the outgoing-cone height bound; the built-in caps also give the axis and terminal requirements.

One prepared outgoing profile and arbitrarily late nominal matching

The reset bound precedes the outgoing exponent, the height bounds precede the actual height, and the natural-axis choices use this same profile. The clean cone below belongs to the unedited outgoing profile. Identification with the complete edited nominal stress is a separate construction.

structure NavierStokes.PreparedOutgoing.PreparedProfile : Type

Data obtained from the actual schedule construction, with a clean cone available at all sufficiently late matching radii.

• profile : OutgoingProfile.Profile

  Profile of PreparedProfile, of type Profile.

• bound : ℝ

  Bound of PreparedProfile, of type ℝ.

• bound_pos : 0 < self.bound
• specification : OutgoingProfile.Specification self.profile self.bound
• schedule : ExtendedHeatedOutgoing.ScheduleBounds self.profile
• terminal : TerminalCone.SmallTail self.profile.data
• amplitude_lower : 2 ≤ self.profile.data.core.P
• height_upper : self.profile.data.h ≤ 1 / 1000
• clean (left : ℝ) : left ≤ 0 → ∃ (R0 : ℝ), 0 < R0 ∧ ∀ (R : ℝ), R0 < R → OutgoingCone.ProfileCleanCone self.profile R left

theorem NavierStokes.PreparedOutgoing.exists_prepared : Nonempty PreparedProfile

Select the reset bound and exponent together, respecting the clean-cone cap before constructing the profile. No existing exponent is changed later.

theorem NavierStokes.PreparedOutgoing.PreparedProfile.large_nominal (d : PreparedProfile) (floor left : ℝ) (hleft : left ≤ 0) : ∃ (W : NominalProfile.Witness d.profile), floor < W.controls.radius ∧ OutgoingCone.ProfileCleanCone d.profile W.controls.radius left

The actual nominal matching radius can exceed any prescribed bound while the outgoing profile and all its schedule choices remain fixed.

noncomputable def NavierStokes.PreparedOutgoing.prepared : PreparedProfile

An actual fixed prepared profile, obtained from the proved existence.

Equations

• NavierStokes.PreparedOutgoing.prepared = Classical.choice NavierStokes.PreparedOutgoing.exists_prepared

theorem NavierStokes.PreparedOutgoing.exists_matched_nominal (floor left : ℝ) (hleft : left ≤ 0) : ∃ (d : PreparedProfile) (W : NominalProfile.Witness d.profile), floor < W.controls.radius ∧ OutgoingCone.ProfileCleanCone d.profile W.controls.radius left

noncomputable def NavierStokes.NominalConeAssembly.IsTrue {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) (p : ProfileHistories.Point) : Prop

Is true, constructed using ActivationContinuation.IsRelaxed.

Equations

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

theorem NavierStokes.NominalConeAssembly.isTrue_iff_loop {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) (p : ProfileHistories.Point) : IsTrue P h p ↔ TrueConeLoop.InTrueCone (ReferenceBounds.p1 P h p) (ReferenceBounds.p2 P h p) (ActivationContinuation.shearA P p) (ActivationContinuation.shearB P p)

theorem NavierStokes.NominalConeAssembly.p1_eq_stock {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) (p : ProfileHistories.Point) : ReferenceBounds.p1 P h p = ActivationStocks.profileStockOne P h p

theorem NavierStokes.NominalConeAssembly.p2_eq_stock {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) (p : ProfileHistories.Point) : ReferenceBounds.p2 P h p = ActivationStocks.profileStockTwo P h p

Local smooth coordinates for the modulation annulus

noncomputable def NavierStokes.NominalConeAssembly.tilt {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ProfileHistories.Point) : ℝ

Tilt, given by ActivationContinuation.shearB P p / ActivationContinuation.shearA P p.

Equations

• NavierStokes.NominalConeAssembly.tilt P p = NavierStokes.ActivationContinuation.shearB P p / NavierStokes.ActivationContinuation.shearA P p

theorem NavierStokes.NominalConeAssembly.physicalE_smoothAt {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) : ContDiffAt ℝ (↑⊤) P.E p

theorem NavierStokes.NominalConeAssembly.shears_smoothAt {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) (hf : P.f p ≠ 0) : ContDiffAt ℝ (↑⊤) (ActivationContinuation.shearA P) p ∧ ContDiffAt ℝ (↑⊤) (ActivationContinuation.shearB P) p

theorem NavierStokes.NominalConeAssembly.stocks_smoothAt {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) (hf : P.f p ≠ 0) (hL : NaturalAxisData.L h p.2 ≠ 0) : ContDiffAt ℝ (↑⊤) (ReferenceBounds.p1 P h) p ∧ ContDiffAt ℝ (↑⊤) (ReferenceBounds.p2 P h) p

theorem NavierStokes.NominalConeAssembly.cone_coordinates_smoothAt {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) (hf : P.f p ≠ 0) (ha : ActivationContinuation.shearA P p ≠ 0) (hL : NaturalAxisData.L h p.2 ≠ 0) : ContDiffAt ℝ (↑⊤) (ActivationContinuation.shearA P) p ∧ ContDiffAt ℝ (↑⊤) (tilt P) p ∧ ContDiffAt ℝ (↑⊤) (ReferenceBounds.p1 P h) p ∧ ContDiffAt ℝ (↑⊤) (ReferenceBounds.p2 P h) p

theorem NavierStokes.NominalConeAssembly.history_of_prefix {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') {J : Set ℝ} {R : ℝ} (h0 : P.pressure0 = Q.pressure0) (hf : ∀ (p : ProfileHistories.Point), p.2 ∈ J → p.1 ≤ R → P.f p = Q.f p) (hu : ∀ (p : ProfileHistories.Point), p.2 ∈ J → p.1 ≤ R → P.U p = Q.U p) (r : StressActivation.HistoryRow) {X eta : ℝ} (hX : 0 ≤ X) (hR : X ≤ R) (heta : eta ∈ J) : StressActivation.profileHistory P r (X, eta) = StressActivation.profileHistory Q r (X, eta)

Equality of an actual prefix propagates to every history, before any derivative or stock comparison is made.

theorem NavierStokes.NominalConeAssembly.radialPartial_of_left {D D' : ProfileHistories.RadialDomain} {F G : ProfileHistories.Field} (hF : ContDiffOn ℝ (↑⊤) F D.carrier) (hG : ContDiffOn ℝ (↑⊤) G D'.carrier) {R : ℝ} {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hq : p ∈ D'.carrier) (hR : p.1 ≤ R) (he : ∀ x ≤ R, F (x, p.2) = G (x, p.2)) : ProfileHistories.radialPartial F p = ProfileHistories.radialPartial G p

The endpoint is included: equality on the left determines the radial derivative because both fields are genuinely differentiable there.

theorem NavierStokes.NominalConeAssembly.coordinates_of_prefix {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (h : ℝ) {J : Set ℝ} (hJ : IsOpen J) {R : ℝ} (h0 : P.pressure0 = Q.pressure0) (hf : ∀ (p : ProfileHistories.Point), p.2 ∈ J → p.1 ≤ R → P.f p = Q.f p) (hu : ∀ (p : ProfileHistories.Point), p.2 ∈ J → p.1 ≤ R → P.U p = Q.U p) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hq : p ∈ D'.carrier) (hX : 0 < p.1) (hR : p.1 ≤ R) (heta : p.2 ∈ J) (hfne : Q.f p ≠ 0) : ActivationContinuation.shearA P p = ActivationContinuation.shearA Q p ∧ ActivationContinuation.shearB P p = ActivationContinuation.shearB Q p ∧ ReferenceBounds.p1 P h p = ReferenceBounds.p1 Q h p ∧ ReferenceBounds.p2 P h p = ReferenceBounds.p2 Q h p

theorem NavierStokes.NominalConeAssembly.relaxed_of_coordinates {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') {h : ℝ} {p : ProfileHistories.Point} (he : ActivationContinuation.shearA P p = ActivationContinuation.shearA Q p ∧ ActivationContinuation.shearB P p = ActivationContinuation.shearB Q p ∧ ReferenceBounds.p1 P h p = ReferenceBounds.p1 Q h p ∧ ReferenceBounds.p2 P h p = ReferenceBounds.p2 Q h p) (hc : ActivationContinuation.IsRelaxed Q h p) : ActivationContinuation.IsRelaxed P h p

theorem NavierStokes.NominalConeAssembly.controls_seed_coordinates {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} (c : NominalProfile.Controls A) (hsep : c.separation ≤ Real.exp (-8)) {p : ProfileHistories.Point} (hsmall : NominalProfile.SmallDebt F c.debt p.2) (hX : 0 < p.1) (hXi : p.1 ≤ NominalProfile.Xi) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : ActivationContinuation.shearA (c.profiles hsep) p = ActivationContinuation.shearA c.seedProfiles p ∧ ActivationContinuation.shearB (c.profiles hsep) p = ActivationContinuation.shearB c.seedProfiles p ∧ ReferenceBounds.p1 (c.profiles hsep) F.data.h p = ReferenceBounds.p1 c.seedProfiles F.data.h p ∧ ReferenceBounds.p2 (c.profiles hsep) F.data.h p = ReferenceBounds.p2 c.seedProfiles F.data.h p

theorem NavierStokes.NominalConeAssembly.continuation_first_at_Xi {F : OutgoingProfile.Profile} {A : NominalProfile.AxisStage F} {N : ℕ} {eps T : ℝ} (w : ActivationContinuation.ContinuationWitness A.natural ⋯ ⋯ ⋯ N eps) (hT : 0 < T) (hsep : (NominalProfile.Controls.ofContinuation A w T hT).separation ≤ Real.exp (-8)) {eta : ℝ} (hsmall : NominalProfile.SmallDebt F (NominalProfile.Controls.ofContinuation A w T hT).debt eta) (heta : eta ∈ HeatedOutgoing.parameterDomain) : 2 < ReferenceBounds.p1 ((NominalProfile.Controls.ofContinuation A w T hT).profiles hsep) F.data.h (NominalProfile.Xi, eta)

noncomputable def NavierStokes.NominalConeAssembly.historyIndex (r : StressActivation.HistoryRow) : Fin 5

History index as an element of Fin 5.

Equations

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

@[simp]

theorem NavierStokes.NominalConeAssembly.historyIndex_mass : historyIndex StressActivation.HistoryRow.mass = 0

@[simp]

theorem NavierStokes.NominalConeAssembly.historyIndex_angular : historyIndex StressActivation.HistoryRow.angular = 1

@[simp]

theorem NavierStokes.NominalConeAssembly.historyIndex_transport : historyIndex StressActivation.HistoryRow.transport = 2

@[simp]

theorem NavierStokes.NominalConeAssembly.historyIndex_energy : historyIndex StressActivation.HistoryRow.energy = 3

@[simp]

theorem NavierStokes.NominalConeAssembly.historyIndex_pressure : historyIndex StressActivation.HistoryRow.pressure = 4

theorem NavierStokes.NominalConeAssembly.profileDensity_eq_regular {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (r : StressActivation.HistoryRow) (p : ProfileHistories.Point) : StressActivation.profileDensity P r p = NominalProfile.regularDensity P p (historyIndex r)

theorem NavierStokes.NominalConeAssembly.history_eq_moment {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (r : StressActivation.HistoryRow) {X eta : ℝ} (hX : 0 ≤ X) : StressActivation.profileHistory P r (X, eta) = StressActivation.profileInitial P r eta + NominalProfile.moments P.U P.E X eta (historyIndex r)

theorem NavierStokes.NominalConeAssembly.Witness.f_positive {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hX : 0 < p.1) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : 0 < W.profiles.f p

theorem NavierStokes.NominalConeAssembly.Witness.prefix_f {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hp : p.1 ≤ W.controls.heatJoin) : W.profiles.f p = (W.controls.profiles ⋯).f p

theorem NavierStokes.NominalConeAssembly.Witness.prefix_histories {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (r : StressActivation.HistoryRow) {X eta : ℝ} (hX : 0 ≤ X) (hR : X ≤ W.controls.heatJoin) : StressActivation.profileHistory W.profiles r (X, eta) = StressActivation.profileHistory (W.controls.profiles ⋯) r (X, eta)

theorem NavierStokes.NominalConeAssembly.Witness.prefix_coordinates {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hp : p ∈ W.domain.carrier) (hX : 0 < p.1) (hR : p.1 ≤ W.controls.heatJoin) (hf : W.controls.f p ≠ 0) : ActivationContinuation.shearA W.profiles p = ActivationContinuation.shearA (W.controls.profiles ⋯) p ∧ ActivationContinuation.shearB W.profiles p = ActivationContinuation.shearB (W.controls.profiles ⋯) p ∧ ReferenceBounds.p1 W.profiles F.data.h p = ReferenceBounds.p1 (W.controls.profiles ⋯) F.data.h p ∧ ReferenceBounds.p2 W.profiles F.data.h p = ReferenceBounds.p2 (W.controls.profiles ⋯) F.data.h p

theorem NavierStokes.NominalConeAssembly.Witness.prefix_relaxed {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hX : 0 < p.1) (hR : p.1 ≤ W.controls.heatJoin) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) (hc : ActivationContinuation.IsRelaxed (W.controls.profiles ⋯) F.data.h p) : ActivationContinuation.IsRelaxed W.profiles F.data.h p

theorem NavierStokes.NominalConeAssembly.Witness.seed_coordinates {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hX : 0 < p.1) (hXi : p.1 ≤ NominalProfile.Xi) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : ActivationContinuation.shearA W.profiles p = ActivationContinuation.shearA W.controls.seedProfiles p ∧ ActivationContinuation.shearB W.profiles p = ActivationContinuation.shearB W.controls.seedProfiles p ∧ ReferenceBounds.p1 W.profiles F.data.h p = ReferenceBounds.p1 W.controls.seedProfiles F.data.h p ∧ ReferenceBounds.p2 W.profiles F.data.h p = ReferenceBounds.p2 W.controls.seedProfiles F.data.h p

theorem NavierStokes.NominalConeAssembly.Witness.seed_relaxed {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hX : 0 < p.1) (hXi : p.1 ≤ NominalProfile.Xi) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) (hc : ActivationContinuation.IsRelaxed W.controls.seedProfiles F.data.h p) : ActivationContinuation.IsRelaxed W.profiles F.data.h p

theorem NavierStokes.NominalConeAssembly.Witness.seed_true {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hX : 0 < p.1) (hXi : p.1 ≤ NominalProfile.Xi) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) (hc : IsTrue W.controls.seedProfiles F.data.h p) : IsTrue W.profiles F.data.h p

theorem NavierStokes.NominalConeAssembly.Witness.continuation_relaxed {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {N : ℕ} {eps T : ℝ} (w : ActivationContinuation.ContinuationWitness W.axis.natural ⋯ ⋯ ⋯ N eps) (hT : 0 < T) (hc : W.controls = NominalProfile.Controls.ofContinuation W.axis w T hT) {p : ProfileHistories.Point} (heta : p.2 ∈ HeatedOutgoing.parameterDomain) (hX : p.1 ∈ Set.Icc w.parameters.startRadius 110) : ActivationContinuation.IsRelaxed W.profiles F.data.h p

theorem NavierStokes.NominalConeAssembly.Witness.moments_eq_profile_moments {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (X eta : ℝ) : NominalProfile.moments W.profiles.U W.profiles.E X eta = NominalProfile.moments W.U W.E X eta

theorem NavierStokes.NominalConeAssembly.Witness.history_after {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (r : StressActivation.HistoryRow) {X eta : ℝ} (hX : W.controls.heatJoin ≤ X) (heta : eta ∈ HeatedOutgoing.parameterDomain) : StressActivation.profileHistory W.profiles r (X, eta) = StressActivation.profileInitial W.profiles r eta + NominalProfile.moments (HeatedOutgoing.U F W.controls.radius) (HeatedOutgoing.E F W.controls.radius W.heat.physical.coefficients) X eta (historyIndex r)

Literal physical moments in the logarithmic chart

noncomputable def NavierStokes.NominalConeAssembly.chart (XR : ℝ) (p : ProfileHistories.Point) : ProfileHistories.Point

Chart, given by (XR * Real.exp p.1, p.2).

Equations

• NavierStokes.NominalConeAssembly.chart XR p = (XR * Real.exp p.1, p.2)

theorem NavierStokes.NominalConeAssembly.chart_positive {XR : ℝ} (hXR : 0 < XR) (p : ProfileHistories.Point) : 0 < (chart XR p).1

theorem NavierStokes.NominalConeAssembly.integral_log_chart (f : ℝ → ℝ) {XR : ℝ} (hXR : 0 < XR) (y : ℝ) : ∫ (x : ℝ) in Set.Ioc 0 (XR * Real.exp y), f x = XR * ∫ (t : ℝ) in Set.Iic y, Real.exp t * f (XR * Real.exp t)

theorem NavierStokes.NominalConeAssembly.sqrt_chart {XR : ℝ} (hXR : 0 < XR) (y : ℝ) : √(2 * (XR * Real.exp y)) = √(2 * XR) * Real.exp (y / 2)

theorem NavierStokes.NominalConeAssembly.outgoing_U_chart (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (p : ProfileHistories.Point) : OutgoingDilation.U F XR (chart XR p) = F.logU p

theorem NavierStokes.NominalConeAssembly.outgoing_E_chart (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (p : ProfileHistories.Point) : OutgoingDilation.E F XR (chart XR p) = F.logE p

theorem NavierStokes.NominalConeAssembly.outgoing_M_chart (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (y eta : ℝ) : OutgoingDilation.M F XR eta (XR * Real.exp y) = XR * OutgoingHistories.M F.data F.amp (y, eta)

theorem NavierStokes.NominalConeAssembly.outgoing_J_chart (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (y eta : ℝ) : OutgoingDilation.J F XR eta (XR * Real.exp y) = XR * √(2 * XR) * OutgoingHistories.J F.reset F.amp (y, eta)

theorem NavierStokes.NominalConeAssembly.heated_I_chart (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (coef : ℝ → HeatedOutgoing.Coeff) {eta : ℝ} (heta : eta ∈ HeatedOutgoing.parameterDomain) (y : ℝ) : NominalProfile.moments (HeatedOutgoing.U F XR) (HeatedOutgoing.E F XR coef) (XR * Real.exp y) eta 1 = XR * √(2 * XR) * HeatSwitchCone.logI F XR coef (y, eta)

theorem NavierStokes.NominalConeAssembly.heated_S_chart (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (coef : ℝ → HeatedOutgoing.Coeff) {eta : ℝ} (heta : eta ∈ HeatedOutgoing.parameterDomain) (y : ℝ) : NominalProfile.moments (HeatedOutgoing.U F XR) (HeatedOutgoing.E F XR coef) (XR * Real.exp y) eta 3 = XR * HeatSwitchCone.logS F XR coef (y, eta)

theorem NavierStokes.NominalConeAssembly.heated_J_chart (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (coef : ℝ → HeatedOutgoing.Coeff) (y eta : ℝ) : NominalProfile.moments (HeatedOutgoing.U F XR) (HeatedOutgoing.E F XR coef) (XR * Real.exp y) eta 2 = XR * √(2 * XR) * OutgoingHistories.J F.reset F.amp (y, eta)

theorem NavierStokes.NominalConeAssembly.Witness.log_histories {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hp : W.controls.heatJoin ≤ (chart W.controls.radius p).1) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : W.profiles.M (chart W.controls.radius p) = W.controls.radius * OutgoingHistories.M F.data F.amp p ∧ W.profiles.I (chart W.controls.radius p) = W.controls.radius * √(2 * W.controls.radius) * HeatSwitchCone.logI F W.controls.radius W.heat.coefficients p ∧ W.profiles.J (chart W.controls.radius p) = W.controls.radius * √(2 * W.controls.radius) * OutgoingHistories.J F.reset F.amp p ∧ W.profiles.S (chart W.controls.radius p) = W.controls.radius * HeatSwitchCone.logS F W.controls.radius W.heat.coefficients p

theorem NavierStokes.NominalConeAssembly.Witness.log_pressure {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hp : W.controls.heatJoin < (chart W.controls.radius p).1) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : W.profiles.pressure (chart W.controls.radius p) = HeatSwitchCone.logPi F W.controls.radius W.heat.coefficients p

theorem NavierStokes.NominalConeAssembly.parameterPartial_eq_scaled_within {D : ProfileHistories.RadialDomain} {f g : ProfileHistories.Field} (hf : ContDiffOn ℝ (↑⊤) f D.carrier) {X y eta k : ℝ} (hp : (X, eta) ∈ D.carrier) (heta : eta ∈ HeatedOutgoing.parameterDomain) (hk : k ≠ 0) (he : ∀ xi ∈ HeatedOutgoing.parameterDomain, f (X, xi) = k * g (y, xi)) : ProfileHistories.parameterPartial f (X, eta) = k * derivWithin (fun (xi : ℝ) => g (y, xi)) HeatedOutgoing.parameterDomain eta

theorem NavierStokes.NominalConeAssembly.smooth_parameterWithin_eq_dEta {g : ProfileHistories.Field} (hg : ContDiff ℝ (↑⊤) g) {p : ProfileHistories.Point} (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : derivWithin (fun (xi : ℝ) => g (p.1, xi)) HeatedOutgoing.parameterDomain p.2 = OutgoingHistories.dEta g p

theorem NavierStokes.NominalConeAssembly.angular_scaled_quotient {R r : ℝ} (hR : R ≠ 0) (hr : r ≠ 0) (a b c k I Ieta J Jeta x z e : ℝ) : (a * (R * r * I) - b * (R * r * Ieta) - c * (R * r * Jeta) + k * (R * r * J)) / (R * x * (r * z * e)) = (a * I - b * Ieta - c * Jeta + k * J) / (x * z * e)

theorem NavierStokes.NominalConeAssembly.scaled_difference_quotient {R : ℝ} (hR : R ≠ 0) (a eta u v x : ℝ) : a * (R * u - eta * (R * v)) / (R * x) = a * (u - eta * v) / x

theorem NavierStokes.NominalConeAssembly.scaled_affine_quotient {R : ℝ} (hR : R ≠ 0) (a b u v x : ℝ) : (a * (R * u) - b * (R * v)) / (R * x) = (a * u - b * v) / x

theorem NavierStokes.NominalConeAssembly.shear_dilation_cancel {r z f : ℝ} (hr : r ≠ 0) (hz : z ≠ 0) (hf : f ≠ 0) (X df : ℝ) : -2 * X * df / f = 1 - 2 * (r * (z * (1 / 2)) * f + r * z * (df * X)) / (r * z * f)

theorem NavierStokes.NominalConeAssembly.physical_log_shears {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {R : ℝ} (hR : 0 < R) (p : ProfileHistories.Point) (hp : chart R p ∈ D.carrier) (hf : P.f (chart R p) ≠ 0) : ActivationContinuation.shearA P (chart R p) = 1 - 2 * deriv (fun (y : ℝ) => P.E (R * Real.exp y, p.2)) p.1 / P.E (chart R p) ∧ ActivationContinuation.shearB P (chart R p) = -2 * deriv (fun (y : ℝ) => P.U (R * Real.exp y, p.2)) p.1 / P.E (chart R p)

The logarithmic radial chart changes actual derivatives, not independent formal jets. This statement is also valid for the matching profile before the heat splice.

theorem NavierStokes.NominalConeAssembly.physical_shear_cancel {r f X : ℝ} (hr : r ≠ 0) (hf : f ≠ 0) (hsq : r ^ 2 = 2 * X) (df : ℝ) : 1 - 2 * X * (1 / (2 * r) * (2 * 1) * f + r * df) / (r * f) = -2 * X * df / f

theorem NavierStokes.NominalConeAssembly.modulated_shears_eq {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) {p : ProfileHistories.Point} (hp : p ∈ D.carrier) (hX : 0 < p.1) (hf : P.f p ≠ 0) : ModulatedCone.angularShear P.E p = ActivationContinuation.shearA P p ∧ ModulatedCone.signedAxialShear P.E P.U p = ActivationContinuation.shearB P p

theorem NavierStokes.NominalConeAssembly.Witness.log_history_parameters {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hp : W.controls.heatJoin < (chart W.controls.radius p).1) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : ProfileHistories.parameterPartial W.profiles.M (chart W.controls.radius p) = W.controls.radius * OutgoingHistories.dEta (OutgoingHistories.M F.data F.amp) p ∧ ProfileHistories.parameterPartial W.profiles.I (chart W.controls.radius p) = W.controls.radius * √(2 * W.controls.radius) * derivWithin (fun (eta : ℝ) => HeatSwitchCone.logI F W.controls.radius W.heat.coefficients (p.1, eta)) HeatedOutgoing.parameterDomain p.2 ∧ ProfileHistories.parameterPartial W.profiles.J (chart W.controls.radius p) = W.controls.radius * √(2 * W.controls.radius) * OutgoingHistories.dEta (OutgoingHistories.J F.reset F.amp) p ∧ ProfileHistories.parameterPartial W.profiles.S (chart W.controls.radius p) = W.controls.radius * derivWithin (fun (eta : ℝ) => HeatSwitchCone.logS F W.controls.radius W.heat.coefficients (p.1, eta)) HeatedOutgoing.parameterDomain p.2 ∧ ProfileHistories.parameterPartial W.profiles.pressure (chart W.controls.radius p) = derivWithin (fun (eta : ℝ) => HeatSwitchCone.logPi F W.controls.radius W.heat.coefficients (p.1, eta)) HeatedOutgoing.parameterDomain p.2

theorem NavierStokes.NominalConeAssembly.Witness.log_fields {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hp : W.controls.heatJoin < (chart W.controls.radius p).1) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : W.profiles.U (chart W.controls.radius p) = F.logU p ∧ W.profiles.E (chart W.controls.radius p) = HeatSwitchCone.logE F W.controls.radius W.heat.coefficients p ∧ W.profiles.H (chart W.controls.radius p) = √(2 * W.controls.radius) * Real.exp (p.1 / 2) * HeatSwitchCone.logE F W.controls.radius W.heat.coefficients p

theorem NavierStokes.NominalConeAssembly.Witness.log_transport {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hp : W.controls.heatJoin < (chart W.controls.radius p).1) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : W.profiles.W F.data.h (chart W.controls.radius p) = OutgoingHistories.W F.data F.amp p

theorem NavierStokes.NominalConeAssembly.Witness.log_lags {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hp : W.controls.heatJoin < (chart W.controls.radius p).1) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : W.profiles.angularLag F.data.h (chart W.controls.radius p) = HeatSwitchCone.Qs F W.controls.radius W.heat.coefficients p ∧ W.profiles.axialLag F.data.h (chart W.controls.radius p) = HeatSwitchCone.Ns F W.controls.radius W.heat.coefficients p

theorem NavierStokes.NominalConeAssembly.Witness.log_stocks {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hp : W.controls.heatJoin < (chart W.controls.radius p).1) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : ReferenceBounds.p1 W.profiles F.data.h (chart W.controls.radius p) = HeatSwitchCone.stressScale F W.controls.radius W.heat.coefficients p ∧ ReferenceBounds.p2 W.profiles F.data.h (chart W.controls.radius p) = W.controls.radius * Real.exp p.1 * HeatSwitchCone.Ns F W.controls.radius W.heat.coefficients p / (NaturalAxisData.L F.data.h p.2 * HeatSwitchCone.logE F W.controls.radius W.heat.coefficients p)

theorem NavierStokes.NominalConeAssembly.Witness.log_shears {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hp : W.controls.heatJoin < (chart W.controls.radius p).1) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : ActivationContinuation.shearA W.profiles (chart W.controls.radius p) = HeatSwitchCone.radialA F W.controls.radius W.heat.coefficients p ∧ ActivationContinuation.shearB W.profiles (chart W.controls.radius p) = -HeatSwitchCone.radialB F W.controls.radius W.heat.coefficients p

Both radial shears are derivatives of the actual fields. The signed axial convention is explicitly the negative of the outgoing convention.

theorem NavierStokes.NominalConeAssembly.stock_ratio_identity (x q n L e : ℝ) (hq : q ≠ 0) : x * n / (L * e) = x * q / L * (n / (e * q))

theorem NavierStokes.NominalConeAssembly.relaxed_scaled_coordinates {a b s r : ℝ} (ha : 0 < a) (hp : 2 < s * (1 - b * r / a)) (hc : a * (1 + (b / a) ^ 2) < ConeAlgebra.coneBound (s * (1 - b * r / a)) (s * (r + b / a))) : ActivationContinuation.Relaxed a (-b) s (s * r)

noncomputable def NavierStokes.NominalConeAssembly.HeatRelaxedAt (F : OutgoingProfile.Profile) (XR : ℝ) (coef : ℝ → HeatedOutgoing.Coeff) (p : ProfileHistories.Point) : Prop

Heat relaxed at, constructed using 0.

Equations

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

theorem NavierStokes.NominalConeAssembly.heated_histories_before_patch (F : OutgoingProfile.Profile) {R : ℝ} (hR : 0 < R) (coef : ℝ → HeatedOutgoing.Coeff) {p : ProfileHistories.Point} (hp : p.1 ≤ OutgoingDilation.patchClock F) : HeatSwitchCone.logI F R coef p = OutgoingHistories.I F.reset p ∧ HeatSwitchCone.logS F R coef p = OutgoingHistories.S F.reset F.amp p ∧ HeatSwitchCone.logPi F R coef p = OutgoingHistories.Pi F.reset p

The pressure cancellation and all preceding histories are retained before the first compensation patch, for every parameter.

theorem NavierStokes.NominalConeAssembly.heated_lags_before_patch (F : OutgoingProfile.Profile) {R : ℝ} (hR : 0 < R) (coef : ℝ → HeatedOutgoing.Coeff) {p : ProfileHistories.Point} (hp : p.1 ≤ OutgoingDilation.patchClock F) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : HeatSwitchCone.Qs F R coef p = OutgoingHistories.Qs F.reset F.amp p ∧ HeatSwitchCone.Ns F R coef p = OutgoingHistories.Ns F.reset F.amp p

theorem NavierStokes.NominalConeAssembly.heated_shears_before_patch (F : OutgoingProfile.Profile) {R : ℝ} (hR : 0 < R) (coef : ℝ → HeatedOutgoing.Coeff) {p : ProfileHistories.Point} (hp : p.1 < OutgoingDilation.patchClock F) : HeatSwitchCone.radialA F R coef p = OutgoingEntranceCone.coneA F.reset p ∧ HeatSwitchCone.radialB F R coef p = OutgoingEntranceCone.coneB F.reset F.amp p

theorem NavierStokes.NominalConeAssembly.heated_relaxed_before_patch (F : OutgoingProfile.Profile) {R : ℝ} (hR : 0 < R) (coef : ℝ → HeatedOutgoing.Coeff) {p : ProfileHistories.Point} (hp : p.1 < OutgoingDilation.patchClock F) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) (hc : OutgoingCone.RelaxedAt F.reset F.amp R p) : HeatRelaxedAt F R coef p

theorem NavierStokes.NominalConeAssembly.Witness.log_second_stock {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hp : W.controls.heatJoin < (chart W.controls.radius p).1) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) (hq : HeatSwitchCone.Qs F W.controls.radius W.heat.coefficients p ≠ 0) : ReferenceBounds.p2 W.profiles F.data.h (chart W.controls.radius p) = HeatSwitchCone.stressScale F W.controls.radius W.heat.coefficients p * HeatSwitchCone.ratio F W.controls.radius W.heat.coefficients p

theorem NavierStokes.NominalConeAssembly.Witness.heat_relaxed {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hp : W.controls.heatJoin < (chart W.controls.radius p).1) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) (hc : HeatRelaxedAt F W.controls.radius W.heat.coefficients p) : ActivationContinuation.IsRelaxed W.profiles F.data.h (chart W.controls.radius p)

theorem NavierStokes.NominalConeAssembly.Witness.heat_true {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hp : W.controls.heatJoin < (chart W.controls.radius p).1) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) (hc : HeatSwitchCone.TrueAt F W.controls.radius W.heat.coefficients p) : IsTrue W.profiles F.data.h (chart W.controls.radius p)

theorem NavierStokes.NominalConeAssembly.Witness.chart_after_match {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hp : 0 ≤ p.1) : W.controls.heatJoin < (chart W.controls.radius p).1

theorem NavierStokes.NominalConeAssembly.Witness.chart_after_matching {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileHistories.Point} (hp : -5 < p.1) : W.controls.heatJoin < (chart W.controls.radius p).1

theorem NavierStokes.NominalConeAssembly.Witness.clean_relaxed_before_hold {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (hc : OutgoingCone.ProfileCleanCone F W.controls.radius (-5)) {p : ProfileHistories.Point} (hy : -5 < p.1) (hhold : p.1 ≤ F.data.core.holdStart) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : ActivationContinuation.IsRelaxed W.profiles F.data.h (chart W.controls.radius p)

theorem NavierStokes.NominalConeAssembly.Witness.terminal_true {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {y eta : ℝ} (hsmall : TerminalCone.SmallTail F.data) (hXR : TerminalCone.radiusThreshold F ≤ W.controls.radius) (hy : TerminalCone.terminalStart F.data ≤ y) (hy' : y < OutgoingTail.tailEnd F.data) (heta : eta ∈ HeatedOutgoing.parameterDomain) : IsTrue W.profiles F.data.h (chart W.controls.radius (y, eta))

A compensation bound chosen before the entrance radius

structure NavierStokes.NominalConeAssembly.CompensatedFamily (F : OutgoingProfile.Profile) : Type

Compensated family data, collecting bound, bound_pos, radiusFloor, radiusFloor_pos, branches, true_from_hold.

• bound : ℝ

  Bound of CompensatedFamily, of type ℝ.

• bound_pos : 0 < self.bound
• radiusFloor : ℝ

  Radius floor of CompensatedFamily, of type ℝ.

• radiusFloor_pos : 0 < self.radiusFloor
• branches (XR : ℝ) : self.radiusFloor ≤ XR → Nonempty (ExtendedHeatedOutgoing.Witness F XR self.bound)
• true_from_hold (XR : ℝ) : self.radiusFloor ≤ XR → ∀ (w : ExtendedHeatedOutgoing.Witness F XR self.bound), ∀ p ∈ OutgoingCone.trueWindow F.data, HeatSwitchCone.TrueAt F XR w.coefficients p

theorem NavierStokes.NominalConeAssembly.exists_compensatedFamily (F : OutgoingProfile.Profile) {anchor left : ℝ} (hc : OutgoingCone.CleanOutgoingCone F.reset anchor left) (ha : 0 < anchor) : Nonempty (CompensatedFamily F)

noncomputable def NavierStokes.NominalConeAssembly.CompensatedFamily.assemble {F : OutgoingProfile.Profile} (G : CompensatedFamily F) {D : ℝ} (hF : OutgoingProfile.Specification F D) (A : NominalProfile.AxisStage F) (c : NominalProfile.Controls A) (hr : G.radiusFloor ≤ c.radius) (hsep : c.separation ≤ Real.exp (-8)) (hs : ∀ eta ∈ HeatedOutgoing.parameterDomain, NominalProfile.SmallDebt F c.debt eta) : NominalProfile.Witness F

The actual heat witness and the nominal fields are constructed only after the same physical radius has met the previously fixed bound.

Equations

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

theorem NavierStokes.NominalConeAssembly.CompensatedFamily.assemble_axis {F : OutgoingProfile.Profile} (G : CompensatedFamily F) {D : ℝ} (hF : OutgoingProfile.Specification F D) (A : NominalProfile.AxisStage F) (c : NominalProfile.Controls A) (hr : G.radiusFloor ≤ c.radius) (hsep : c.separation ≤ Real.exp (-8)) (hs : ∀ eta ∈ HeatedOutgoing.parameterDomain, NominalProfile.SmallDebt F c.debt eta) : (G.assemble hF A c hr hsep hs).axis = A

theorem NavierStokes.NominalConeAssembly.CompensatedFamily.assemble_controls {F : OutgoingProfile.Profile} (G : CompensatedFamily F) {D : ℝ} (hF : OutgoingProfile.Specification F D) (A : NominalProfile.AxisStage F) (c : NominalProfile.Controls A) (hr : G.radiusFloor ≤ c.radius) (hsep : c.separation ≤ Real.exp (-8)) (hs : ∀ eta ∈ HeatedOutgoing.parameterDomain, NominalProfile.SmallDebt F c.debt eta) : (G.assemble hF A c hr hsep hs).controls = c

theorem NavierStokes.NominalConeAssembly.CompensatedFamily.assemble_bound {F : OutgoingProfile.Profile} (G : CompensatedFamily F) {D : ℝ} (hF : OutgoingProfile.Specification F D) (A : NominalProfile.AxisStage F) (c : NominalProfile.Controls A) (hr : G.radiusFloor ≤ c.radius) (hsep : c.separation ≤ Real.exp (-8)) (hs : ∀ eta ∈ HeatedOutgoing.parameterDomain, NominalProfile.SmallDebt F c.debt eta) : (G.assemble hF A c hr hsep hs).heatBound = G.bound

theorem NavierStokes.NominalConeAssembly.CompensatedFamily.assemble_true_from_hold {F : OutgoingProfile.Profile} (G : CompensatedFamily F) {D : ℝ} (hF : OutgoingProfile.Specification F D) (A : NominalProfile.AxisStage F) (c : NominalProfile.Controls A) (hr : G.radiusFloor ≤ c.radius) (hsep : c.separation ≤ Real.exp (-8)) (hs : ∀ eta ∈ HeatedOutgoing.parameterDomain, NominalProfile.SmallDebt F c.debt eta) (p : ProfileHistories.Point) (hp : p ∈ OutgoingCone.trueWindow F.data) : HeatSwitchCone.TrueAt F c.radius (G.assemble hF A c hr hsep hs).heat.coefficients p

theorem NavierStokes.NominalConeAssembly.CompensatedFamily.assemble_profile_true {F : OutgoingProfile.Profile} (G : CompensatedFamily F) {D : ℝ} (hF : OutgoingProfile.Specification F D) (A : NominalProfile.AxisStage F) (c : NominalProfile.Controls A) (hr : G.radiusFloor ≤ c.radius) (hsep : c.separation ≤ Real.exp (-8)) (hs : ∀ eta ∈ HeatedOutgoing.parameterDomain, NominalProfile.SmallDebt F c.debt eta) (p : ProfileHistories.Point) (hp : p ∈ OutgoingCone.trueWindow F.data) : IsTrue (G.assemble hF A c hr hsep hs).profiles F.data.h (chart c.radius p)

theorem NavierStokes.NominalConeAssembly.CompensatedFamily.assemble_profile_true_late {F : OutgoingProfile.Profile} (G : CompensatedFamily F) {D : ℝ} (hF : OutgoingProfile.Specification F D) (A : NominalProfile.AxisStage F) (c : NominalProfile.Controls A) (hr : G.radiusFloor ≤ c.radius) (hsep : c.separation ≤ Real.exp (-8)) (hs : ∀ eta ∈ HeatedOutgoing.parameterDomain, NominalProfile.SmallDebt F c.debt eta) (hsmall : TerminalCone.SmallTail F.data) (hXR : TerminalCone.radiusThreshold F ≤ c.radius) {p : ProfileHistories.Point} (hp : F.data.core.holdStart ≤ p.1) (hend : p.1 < OutgoingTail.tailEnd F.data) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : IsTrue (G.assemble hF A c hr hsep hs).profiles F.data.h (chart c.radius p)

theorem NavierStokes.NominalConeAssembly.CompensatedFamily.assemble_profile_relaxed_outer {F : OutgoingProfile.Profile} (G : CompensatedFamily F) {D : ℝ} (hF : OutgoingProfile.Specification F D) (A : NominalProfile.AxisStage F) (c : NominalProfile.Controls A) (hr : G.radiusFloor ≤ c.radius) (hsep : c.separation ≤ Real.exp (-8)) (hs : ∀ eta ∈ HeatedOutgoing.parameterDomain, NominalProfile.SmallDebt F c.debt eta) (hsmall : TerminalCone.SmallTail F.data) (hXR : TerminalCone.radiusThreshold F ≤ c.radius) (hclean : OutgoingCone.ProfileCleanCone F c.radius (-5)) {p : ProfileHistories.Point} (hp : -5 < p.1) (hend : p.1 < OutgoingTail.tailEnd F.data) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : ActivationContinuation.IsRelaxed (G.assemble hF A c hr hsep hs).profiles F.data.h (chart c.radius p)

noncomputable def NavierStokes.NominalConeAssembly.CompensatedFamily.assemblePrepared {F : OutgoingProfile.Profile} (G : CompensatedFamily F) {D : ℝ} (hF : OutgoingProfile.Specification F D) {N : ℕ} {delta radiusFloor : ℝ} (M : MatchingConeBounds.PreparedWitness F N delta radiusFloor) (hr : G.radiusFloor ≤ radiusFloor) : NominalProfile.Witness F

The already selected axis stage and continuation are used literally in the final fields; only the compensation branch is selected here.

Equations

• G.assemblePrepared hF M hr = G.assemble hF M.axis M.controls ⋯ ⋯ ⋯

theorem NavierStokes.NominalConeAssembly.CompensatedFamily.prepared_continuation_relaxed {F : OutgoingProfile.Profile} (G : CompensatedFamily F) {D : ℝ} (hF : OutgoingProfile.Specification F D) {N : ℕ} {delta radiusFloor : ℝ} (M : MatchingConeBounds.PreparedWitness F N delta radiusFloor) (hr : G.radiusFloor ≤ radiusFloor) {p : ProfileHistories.Point} (heta : p.2 ∈ HeatedOutgoing.parameterDomain) (hp : p.1 ∈ Set.Icc M.continuation.parameters.startRadius 110) : ActivationContinuation.IsRelaxed (G.assemblePrepared hF M hr).profiles F.data.h p

theorem NavierStokes.NominalConeAssembly.CompensatedFamily.prepared_shape_relaxed {F : OutgoingProfile.Profile} (G : CompensatedFamily F) {D : ℝ} (hF : OutgoingProfile.Specification F D) {N : ℕ} {delta radiusFloor : ℝ} (M : MatchingConeBounds.PreparedWitness F N delta radiusFloor) (hr : G.radiusFloor ≤ radiusFloor) {X eta : ℝ} (hX : NominalProfile.Xi ≤ X) (hR : X ≤ M.controls.radius * Real.exp (-8)) (heta : eta ∈ HeatedOutgoing.parameterDomain) : ActivationContinuation.IsRelaxed (G.assemblePrepared hF M hr).profiles F.data.h (X, eta)

theorem NavierStokes.NominalConeAssembly.Initial.physical_initial_shears {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : ActivationContinuation.RampParameters E.profile.family hΛ hsmall hP0) {y η : ℝ} (hy : y ≤ r.refTime) (hη : η ∈ ReferencePath.parameterInterval) : have N := ReferencePath.Input.ofNatural hΛ E.profile.family; have L := StressActivation.FromReference.refLog N r.refTime; have U := StressActivation.FromReference.refAxial N r.refTime; have z := (StressActivation.radius N.endpoint y, η); ActivationContinuation.shearA r.profiles z = StressActivation.actualP1 r.actTime r.kappa L (y, η) ∧ ActivationContinuation.shearB r.profiles z = StressActivation.actualP2 r.actTime r.kappa N.endpoint L U (y, η)

Exact physical shears on the initial natural collar.

theorem NavierStokes.NominalConeAssembly.Initial.referenceP1_positive_initial {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : ActivationContinuation.RampParameters E.profile.family hΛ hsmall hP0) {y η : ℝ} (hy : y ≤ r.refTime) (hη : η ∈ Set.Icc (-1) 1) : 0 < StressActivation.referenceP1 (StressActivation.FromReference.refLog (ReferencePath.Input.ofNatural hΛ E.profile.family) r.refTime) (y, η)

Positivity from this same constructed entrance profile.

theorem NavierStokes.NominalConeAssembly.Initial.shearSize_eq_initial (a b : ℝ) (ha : a ≠ 0) : ActivationContinuation.shearSize a b = a + b ^ 2 / a

theorem NavierStokes.NominalConeAssembly.Initial.projection_eq_initial (h X0 T κ : ℝ) (I : StressActivation.HistoryRow → ℝ → ℝ) (L U : ProfileHistories.Field) (p : ProfileHistories.Point) : ActivationContinuation.projection (ActivationCone.activatedStockOne h X0 I L U T κ p) (ActivationCone.activatedStockTwo h X0 I L U T κ p) (StressActivation.actualP1 T κ L p) (StressActivation.actualP2 T κ X0 L U p) = ActivationCone.activatedProjection h X0 I L U T κ p

theorem NavierStokes.NominalConeAssembly.Initial.transverse_eq_initial (h X0 T κ : ℝ) (I : StressActivation.HistoryRow → ℝ → ℝ) (L U : ProfileHistories.Field) (p : ProfileHistories.Point) : ActivationContinuation.transverse (ActivationCone.activatedStockOne h X0 I L U T κ p) (ActivationCone.activatedStockTwo h X0 I L U T κ p) (StressActivation.actualP1 T κ L p) (StressActivation.actualP2 T κ X0 L U p) = ActivationCone.activatedCross h X0 I L U T κ p

theorem NavierStokes.NominalConeAssembly.Initial.physical_initial_stocks {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} (r : ActivationContinuation.RampParameters E.profile.family hΛ hsmall hP0) {y η : ℝ} (hy : y ≤ r.refTime) (hη : η ∈ ReferencePath.parameterInterval) : have N := ReferencePath.Input.ofNatural hΛ E.profile.family; have L := StressActivation.FromReference.refLog N r.refTime; have U := StressActivation.FromReference.refAxial N r.refTime; have I := ActivationStocks.FromReference.initial N ⋯ ⋯ P0 hP0; have z := (StressActivation.radius N.endpoint y, η); ReferenceBounds.p1 r.profiles h z = ActivationCone.activatedStockOne h N.endpoint I L U r.actTime r.kappa (y, η) ∧ ReferenceBounds.p2 r.profiles h z = ActivationCone.activatedStockTwo h N.endpoint I L U r.actTime r.kappa (y, η)

The actual ACT histories of the same continuation witness give the logarithmic stock coordinates in its initial activation certificate.

theorem NavierStokes.NominalConeAssembly.Initial.activation_cone {h j σ Λ C : ℝ} {P0 : ℝ → ℝ} {d : NaturalAxisCoefficients.AnalyticInputs h j σ P0} (E : NaturalEntrance.EntranceProfile d Λ C) {hΛ : 0 < Λ} {hsmall : NaturalAxisData.SmallParameters h j} {hP0 : ContDiff ℝ (↑⊤) P0} {order : ℕ} {eps : ℝ} (w : ActivationContinuation.ContinuationWitness E hΛ hsmall hP0 order eps) : have N := ReferencePath.Input.ofNatural hΛ E.profile.family; (∀ (y eta : ℝ), 0 < y → y ≤ w.parameters.actTime → eta ∈ Set.Icc (-1) 1 → ActivationContinuation.IsRelaxed w.parameters.profiles h (StressActivation.radius N.endpoint y, eta)) ∧ ∃ (t : ℝ), 0 < t ∧ t ≤ w.parameters.actTime ∧ ∀ (y eta : ℝ), 0 < y → y ≤ t → eta ∈ Set.Icc (-1) 1 → IsTrue w.parameters.profiles h (StressActivation.radius N.endpoint y, eta)

The active annulus and one common ordered choice

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

Active left, given by 4 / W.axis.scale.

Equations

• NavierStokes.NominalConeAssembly.activeLeft W = 4 / W.axis.scale

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

Active right, given by W.controls.radius * Real.exp (OutgoingTail.tailEnd F.data).

Equations

• NavierStokes.NominalConeAssembly.activeRight W = W.controls.radius * Real.exp (NavierStokes.OutgoingTail.tailEnd F.data)

theorem NavierStokes.NominalConeAssembly.activeLeft_pos {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : 0 < activeLeft W

theorem NavierStokes.NominalConeAssembly.activeLeft_lt_Xi {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : activeLeft W < NominalProfile.Xi

theorem NavierStokes.NominalConeAssembly.chart_log {R : ℝ} (hR : 0 < R) {p : ProfileHistories.Point} (hp : 0 < p.1) : chart R (Real.log (p.1 / R), p.2) = p

theorem NavierStokes.NominalConeAssembly.log_chart_lt {R X y : ℝ} (hR : 0 < R) (hX : 0 < X) (hy : X < R * Real.exp y) : Real.log (X / R) < y

theorem NavierStokes.NominalConeAssembly.lt_log_chart {R X y : ℝ} (hR : 0 < R) (hy : R * Real.exp y < X) : y < Real.log (X / R)

structure NavierStokes.NominalConeAssembly.Certificate {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : Prop

Every assertion concerns the same physical fields and absolute histories. The extra lower speed condition is asserted only on the two regions where the pre-modulation construction proves it.

• relaxed (p : ProfileHistories.Point) : activeLeft W < p.1 → p.1 < activeRight W → p.2 ∈ HeatedOutgoing.parameterDomain → ActivationContinuation.IsRelaxed W.profiles F.data.h p
• initial : ∃ (t : ℝ), 0 < t ∧ t ≤ W.controls.activationTime ∧ ∀ (y eta : ℝ), 0 < y → y ≤ t → eta ∈ HeatedOutgoing.parameterDomain → IsTrue W.profiles F.data.h (chart (activeLeft W) (y, eta))
• outgoing (y eta : ℝ) : F.data.core.holdStart ≤ y → y < OutgoingTail.tailEnd F.data → eta ∈ HeatedOutgoing.parameterDomain → IsTrue W.profiles F.data.h (chart W.controls.radius (y, eta))

theorem NavierStokes.NominalConeAssembly.Certificate.coordinates_smoothAt {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (hW : Certificate W) {p : ProfileHistories.Point} (hl : activeLeft W < p.1) (hr : p.1 < activeRight W) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : ContDiffAt ℝ (↑⊤) (ActivationContinuation.shearA W.profiles) p ∧ ContDiffAt ℝ (↑⊤) (tilt W.profiles) p ∧ ContDiffAt ℝ (↑⊤) (ReferenceBounds.p1 W.profiles F.data.h) p ∧ ContDiffAt ℝ (↑⊤) (ReferenceBounds.p2 W.profiles F.data.h) p

structure NavierStokes.NominalConeAssembly.Assembly (d : PreparedOutgoing.PreparedProfile) : Type

Intermediate data retain the actual continuation and its repair coefficients. The existence theorem below constructs every cone field in this record from the already proved estimates.

• family : CompensatedFamily d.profile

  Family of Assembly, of type CompensatedFamily d.profile.

• delta : ℝ

  Delta of Assembly, of type ℝ.

• radiusFloor : ℝ

  Radius floor of Assembly, of type ℝ.

• matching : MatchingConeBounds.PreparedWitness d.profile 1 self.delta self.radiusFloor

  Matching of Assembly, of type MatchingConeBounds.PreparedWitness d.profile 1 delta radiusFloor.

• family_floor : self.family.radiusFloor ≤ self.radiusFloor
• terminal_floor : TerminalCone.radiusThreshold d.profile ≤ self.matching.controls.radius
• clean : OutgoingCone.ProfileCleanCone d.profile self.matching.controls.radius (-5)
• repair (p : ProfileHistories.Point) : p.1 ∈ Set.Icc (self.matching.controls.radius * Real.exp (-8)) (self.matching.controls.radius * Real.exp (-5)) → p.2 ∈ HeatedOutgoing.parameterDomain → ActivationContinuation.IsRelaxed (self.matching.controls.profiles ⋯) d.profile.data.h p

noncomputable def NavierStokes.NominalConeAssembly.Assembly.witness {d : PreparedOutgoing.PreparedProfile} (A : Assembly d) : NominalProfile.Witness d.profile

Witness, given by A.family.assemblePrepared d.specification A.matching A.family_floor.

Equations

• A.witness = A.family.assemblePrepared ⋯ A.matching ⋯

theorem NavierStokes.NominalConeAssembly.Assembly.outgoing {d : PreparedOutgoing.PreparedProfile} (A : Assembly d) {y eta : ℝ} (hy : d.profile.data.core.holdStart ≤ y) (hend : y < OutgoingTail.tailEnd d.profile.data) (heta : eta ∈ HeatedOutgoing.parameterDomain) : IsTrue A.witness.profiles d.profile.data.h (chart A.witness.controls.radius (y, eta))

theorem NavierStokes.NominalConeAssembly.Assembly.outer_relaxed {d : PreparedOutgoing.PreparedProfile} (A : Assembly d) {p : ProfileHistories.Point} (hXi : NominalProfile.Xi ≤ p.1) (hend : p.1 < activeRight A.witness) (heta : p.2 ∈ HeatedOutgoing.parameterDomain) : ActivationContinuation.IsRelaxed A.witness.profiles d.profile.data.h p

theorem NavierStokes.NominalConeAssembly.Assembly.initial_cones {d : PreparedOutgoing.PreparedProfile} (A : Assembly d) : (∀ (y eta : ℝ), 0 < y → y ≤ A.witness.controls.activationTime → eta ∈ HeatedOutgoing.parameterDomain → ActivationContinuation.IsRelaxed A.witness.profiles d.profile.data.h (chart (activeLeft A.witness) (y, eta))) ∧ ∃ (t : ℝ), 0 < t ∧ t ≤ A.witness.controls.activationTime ∧ ∀ (y eta : ℝ), 0 < y → y ≤ t → eta ∈ HeatedOutgoing.parameterDomain → IsTrue A.witness.profiles d.profile.data.h (chart (activeLeft A.witness) (y, eta))

theorem NavierStokes.NominalConeAssembly.Assembly.certificate {d : PreparedOutgoing.PreparedProfile} (A : Assembly d) : Certificate A.witness

The nominal profile has the relaxed cone throughout its active annulus and the true cone in its initial collar and from the shaped hold through the terminal region. Every component uses the stored witness.

theorem NavierStokes.NominalConeAssembly.assembly_exists (d : PreparedOutgoing.PreparedProfile) : Nonempty (Assembly d)

theorem NavierStokes.NominalConeAssembly.exists_certificate (d : PreparedOutgoing.PreparedProfile) : ∃ (W : NominalProfile.Witness d.profile), Certificate W

Any one prepared outgoing profile has a nominal witness with the complete actual cone certificate. No cone or matching-debt assumption is added to the prepared profile.

theorem NavierStokes.NominalConeAssembly.exists_nominal_cone : ∃ (F : OutgoingProfile.Profile) (W : NominalProfile.Witness F), Certificate W