The full fully-switched terminal cone

The release estimate is uniform on the whole remaining logarithmic interval. The closed profile band is treated with the actual smooth heat extension, not with a compact subset of a physical chart. The compensation witness is arbitrary throughout.

noncomputable def NavierStokes.TerminalCone.terminalStart (d : OutgoingTail.TailData) : ℝ

The clock at which the heat switch is complete.

Equations

• NavierStokes.TerminalCone.terminalStart d = NavierStokes.OutgoingTail.tailStart d + 1 / 2

noncomputable def NavierStokes.TerminalCone.normalization (F : OutgoingProfile.Profile) (XR : ℝ) : ℝ

Normalization, given by TerminalPressure.releasedNormalization F.data (OutgoingDilation.switchRadius F XR).

Equations

• NavierStokes.TerminalCone.normalization F XR = NavierStokes.TerminalPressure.releasedNormalization F.data (NavierStokes.OutgoingDilation.switchRadius F XR)

noncomputable def NavierStokes.TerminalCone.shift (F : OutgoingProfile.Profile) (XR : ℝ) : ℝ

Shift, given by Real.log (OutgoingDilation.switchRadius F XR) - 1 / 5.

Equations

• NavierStokes.TerminalCone.shift F XR = Real.log (NavierStokes.OutgoingDilation.switchRadius F XR) - 1 / 5

noncomputable def NavierStokes.TerminalCone.edgeDistance (F : OutgoingProfile.Profile) (y : ℝ) : ℝ

Edge distance, given by OutgoingTail.tailEnd F.data - y.

Equations

• NavierStokes.TerminalCone.edgeDistance F y = NavierStokes.OutgoingTail.tailEnd F.data - y

noncomputable def NavierStokes.TerminalCone.profilePoint (F : OutgoingProfile.Profile) (y eta : ℝ) : ℝ × ℝ

Profile point, given by (eta, edgeDistance F y).

Equations

• NavierStokes.TerminalCone.profilePoint F y eta = (eta, NavierStokes.TerminalCone.edgeDistance F y)

noncomputable def NavierStokes.TerminalCone.releaseTime (c : OutgoingSchedule.Parameters) : ℝ

The release time and release amplitude depend on the core schedule before the terminal exponent is chosen.

Equations

• NavierStokes.TerminalCone.releaseTime c = c.endpoint + NavierStokes.OutgoingTail.flattenLength + 30 * Real.log (1 / c.lam)

noncomputable def NavierStokes.TerminalCone.releaseAmplitude (c : OutgoingSchedule.Parameters) : ℝ

Release amplitude, given by OutgoingSchedule.radialAmplitude c.P c.dropLength c.lam (releaseTime c) / 2.

Equations

• NavierStokes.TerminalCone.releaseAmplitude c = NavierStokes.OutgoingSchedule.radialAmplitude c.P c.dropLength c.lam (NavierStokes.TerminalCone.releaseTime c) / 2

noncomputable def NavierStokes.TerminalCone.annulusRatio : ℝ

Annulus ratio, given by Real.exp 3.

Equations

• NavierStokes.TerminalCone.annulusRatio = Real.exp 3

noncomputable def NavierStokes.TerminalCone.releaseBudget (c : OutgoingSchedule.Parameters) : ℝ

Release budget, given by 16 * annulusRatio * (annulusRatio - 1) * releaseAmplitude c.

Equations

• NavierStokes.TerminalCone.releaseBudget c = 16 * NavierStokes.TerminalCone.annulusRatio * (NavierStokes.TerminalCone.annulusRatio - 1) * NavierStokes.TerminalCone.releaseAmplitude c

def NavierStokes.TerminalCone.SmallTail (d : OutgoingTail.TailData) : Prop

The order is explicit: these bounds use only the already fixed core schedule, then constrain h; the entrance radius is chosen afterwards.

Equations

• NavierStokes.TerminalCone.SmallTail d = (d.h ≤ 1 / 4 ∧ d.h ≤ 1 / (1 + NavierStokes.TerminalCone.releaseBudget d.core))

theorem NavierStokes.TerminalCone.releaseAmplitude_eq (d : OutgoingTail.TailData) : releaseAmplitude d.core = OutgoingTail.finalAngular d (d.releaseStart, 0)

theorem NavierStokes.TerminalCone.normalization_pos (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) : 0 < normalization F XR

theorem NavierStokes.TerminalCone.edgeDistance_bounds (F : OutgoingProfile.Profile) {y : ℝ} (hy : terminalStart F.data ≤ y) (hy' : y < OutgoingTail.tailEnd F.data) : 0 < edgeDistance F y ∧ edgeDistance F y ≤ 5 / 2

theorem NavierStokes.TerminalCone.shift_log (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) : shift F XR = Real.log XR + OutgoingTail.tailStart F.data

theorem NavierStokes.TerminalCone.profileS_clock (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (y : ℝ) : TerminalEdgeFactor.profileS (shift F XR) (edgeDistance F y) = XR * Real.exp y

theorem NavierStokes.TerminalCone.profileS_ge_switch {K δ : ℝ} (hK : 0 < K) (hδ : δ ≤ 5 / 2) : K ≤ TerminalEdgeFactor.profileS (Real.log K - 1 / 5) δ

theorem NavierStokes.TerminalCone.profileRadius_le_outer (y0 : ℝ) {δ : ℝ} (hδ : 0 ≤ δ) : TerminalEdgeFactor.profileRadius y0 δ ≤ TerminalEdgeFactor.profileRadius y0 0

theorem NavierStokes.TerminalCone.profileRadius_annulus (y0 : ℝ) {δ : ℝ} (hδ : δ ≤ 5 / 2) : TerminalEdgeFactor.profileRadius y0 0 ^ 2 ≤ annulusRatio * TerminalEdgeFactor.profileRadius y0 δ ^ 2

theorem NavierStokes.TerminalCone.le_on_closed_band {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) (h : ∀ eta ∈ Set.Ioo (-1) 1, f eta ≤ g eta) {eta : ℝ} (heta : eta ∈ Set.Icc (-1) 1) : f eta ≤ g eta

theorem NavierStokes.TerminalCone.eta_sq_lt_one {eta : ℝ} (heta : eta ∈ Set.Ioo (-1) 1) : eta ^ 2 < 1

Uniform small-argument heat slope, including zero diffusion

noncomputable def NavierStokes.TerminalCone.heatSlope (d : OutgoingTail.TailData) (z : ℝ) : ℝ

Heat slope, given by -z * deriv (HeatProfileExtension.extension (1 + d.h)) z / HeatProfileExtension.extension (1 + d.h) z.

Equations

• NavierStokes.TerminalCone.heatSlope d z = -z * deriv (NavierStokes.HeatProfileExtension.extension (1 + d.h)) z / NavierStokes.HeatProfileExtension.extension (1 + d.h) z

theorem NavierStokes.TerminalCone.extension_deriv_eq (d : OutgoingTail.TailData) {z : ℝ} (hz : 0 ≤ z) : deriv (HeatProfileExtension.extension (1 + d.h)) z = derivWithin (RadialHeatProfile.profile (1 + d.h)) (Set.Ici 0) z

theorem NavierStokes.TerminalCone.heatSlope_bounds (d : OutgoingTail.TailData) (hh : d.h ≤ 1 / 4) {z : ℝ} (hz : 0 ≤ z) (hz1 : z ≤ 1 / 16) : 0 ≤ heatSlope d z ∧ heatSlope d z ≤ d.h / 4

theorem NavierStokes.TerminalCone.profileZ_small (_d : OutgoingTail.TailData) {K δ eta : ℝ} (hK : 32 ≤ K) (hδ : δ ≤ 5 / 2) (heta : eta ^ 2 ≤ 1) : 0 ≤ TerminalEdgeFactor.profileZ (Real.log K - 1 / 5) (eta, δ) ∧ TerminalEdgeFactor.profileZ (Real.log K - 1 / 5) (eta, δ) ≤ 1 / 16

theorem NavierStokes.TerminalCone.profileSpeed_eq {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) {eta δ : ℝ} (heta : eta ^ 2 ≤ 1) : TerminalEdgeFactor.profileSpeed C d y0 (eta, δ) = 2 + 2 * d.h - 2 * heatSlope d (TerminalEdgeFactor.profileZ y0 (eta, δ)) - 2 * OutgoingTail.tailShapeDeriv d (3 - δ) / OutgoingTail.tailShape d (3 - δ)

theorem NavierStokes.TerminalCone.profileSpeed_bounds {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (hh : d.h ≤ 1 / 4) {K δ eta : ℝ} (hK : 32 ≤ K) (hδ : δ ≤ 5 / 2) (heta : eta ^ 2 ≤ 1) : 2 + d.h < TerminalEdgeFactor.profileSpeed C d (Real.log K - 1 / 5) (eta, δ) ∧ TerminalEdgeFactor.profileSpeed C d (Real.log K - 1 / 5) (eta, δ) ≤ 2 + 2 * d.h

Physical-section identities and extension to the closed band

theorem NavierStokes.TerminalCone.normalized_X (d : OutgoingTail.TailData) (y0 δ : ℝ) {eta : ℝ} (heta : eta ^ 2 < 1) : SimilarityProfile.X d.h (TerminalStress.radiusPoint (eta ^ 2) (TerminalEdgeFactor.profileRadius y0 δ) eta) = TerminalEdgeFactor.profileS y0 δ

theorem NavierStokes.TerminalCone.normalized_logX (d : OutgoingTail.TailData) (y0 δ : ℝ) {eta : ℝ} (heta : eta ^ 2 < 1) : Real.log (SimilarityProfile.X d.h (TerminalStress.radiusPoint (eta ^ 2) (TerminalEdgeFactor.profileRadius y0 δ) eta)) = y0 + 3 - δ

theorem NavierStokes.TerminalCone.normalized_denominator (d : OutgoingTail.TailData) {eta : ℝ} (heta : eta ^ 2 < 1) : TerminalStress.timeDenominator d.h (eta ^ 2) eta = TerminalEdgeFactor.profileL d eta

theorem NavierStokes.TerminalCone.normalized_carrier (C : ℝ) (d : OutgoingTail.TailData) (y0 δ : ℝ) {eta : ℝ} (heta : eta ^ 2 < 1) : TerminalStress.heatAmplitude C (1 + d.h) (eta ^ 2) (TerminalEdgeFactor.profileRadius y0 δ) = TerminalEdgeFactor.profileCarrier C d y0 (eta, δ)

theorem NavierStokes.TerminalCone.normalized_angularStress (C : ℝ) (d : OutgoingTail.TailData) (y0 δ : ℝ) {eta : ℝ} (heta : eta ^ 2 < 1) : TerminalStress.terminalStress C d.h (TerminalPressure.outgoingTaper d y0) (eta ^ 2) eta (TerminalEdgeFactor.profileRadius y0 δ) = TerminalEdgeFactor.profileAngularStress C d y0 (eta, δ)

theorem NavierStokes.TerminalCone.normalized_axialStress (C : ℝ) (d : OutgoingTail.TailData) (y0 δ : ℝ) {eta : ℝ} (heta : eta ^ 2 < 1) : TerminalPressure.axialBackwardStress C d.h (TerminalPressure.outgoingTaper d y0) (eta ^ 2) eta (TerminalEdgeFactor.profileRadius y0 δ) = TerminalEdgeFactor.profileAxialStress C d y0 (eta, δ)

noncomputable def NavierStokes.TerminalCone.profileMass (C : ℝ) (d : OutgoingTail.TailData) (y0 δ eta : ℝ) : ℝ

Profile mass as an element of ℝ.

Equations

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

theorem NavierStokes.TerminalCone.profileMass_continuous (C : ℝ) (d : OutgoingTail.TailData) (y0 δ : ℝ) : Continuous (profileMass C d y0 δ)

theorem NavierStokes.TerminalCone.profileMass_le_stress {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) {δ eta : ℝ} (hδ : 0 < δ) (heta : eta ∈ Set.Icc (-1) 1) : profileMass C d y0 δ eta ≤ TerminalEdgeFactor.profileAngularStress C d y0 (eta, δ)

theorem NavierStokes.TerminalCone.profileAngularStress_pos {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) {δ eta : ℝ} (hδ : 0 < δ) (heta : eta ∈ Set.Icc (-1) 1) : 0 < TerminalEdgeFactor.profileAngularStress C d y0 (eta, δ)

theorem NavierStokes.TerminalCone.releaseAmplitude_pos (c : OutgoingSchedule.Parameters) : 0 < releaseAmplitude c

theorem NavierStokes.TerminalCone.annulusRatio_gt_one : 1 < annulusRatio

theorem NavierStokes.TerminalCone.releaseBudget_nonneg (c : OutgoingSchedule.Parameters) : 0 ≤ releaseBudget c

theorem NavierStokes.TerminalCone.release_small (d : OutgoingTail.TailData) (hsmall : SmallTail d) : releaseBudget d.core * d.h ^ 4 ≤ 1

theorem NavierStokes.TerminalCone.profileAxialStress_le_angular (d : OutgoingTail.TailData) (hsmall : SmallTail d) {K δ eta : ℝ} (hK : 0 < K) (hδ : 0 < δ) (hδ' : δ ≤ 5 / 2) (heta : eta ∈ Set.Icc (-1) 1) : |TerminalEdgeFactor.profileAxialStress (TerminalPressure.releasedNormalization d K) d (Real.log K - 1 / 5) (eta, δ)| ≤ TerminalEdgeFactor.profileAngularStress (TerminalPressure.releasedNormalization d K) d (Real.log K - 1 / 5) (eta, δ)

Uniform cone margin through the actual terminal edge

theorem NavierStokes.TerminalCone.profileAngularFactor_pos {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) {δ eta : ℝ} (hδ : 0 ≤ δ) (heta : eta ∈ Set.Icc (-1) 1) : 0 < TerminalEdgeFactor.profileAngularFactor C d y0 (eta, δ)

theorem NavierStokes.TerminalCone.profileTilt_contDiffAt {C : ℝ} (hC : 0 < C) (d : OutgoingTail.TailData) (y0 : ℝ) {δ eta : ℝ} (hδ : 0 ≤ δ) (heta : eta ∈ Set.Icc (-1) 1) : ContDiffAt ℝ (↑⊤) (TerminalEdgeFactor.profileTilt C d y0) (eta, δ)

theorem NavierStokes.TerminalCone.profileTilt_abs_le_one (d : OutgoingTail.TailData) (hsmall : SmallTail d) {K δ eta : ℝ} (hK : 0 < K) (hδ : 0 ≤ δ) (hδ' : δ ≤ 5 / 2) (heta : eta ∈ Set.Icc (-1) 1) : |TerminalEdgeFactor.profileTilt (TerminalPressure.releasedNormalization d K) d (Real.log K - 1 / 5) (eta, δ)| ≤ 1

theorem NavierStokes.TerminalCone.profile_cone_margin (d : OutgoingTail.TailData) (hsmall : SmallTail d) {K δ eta : ℝ} (hK : 32 ≤ K) (hδ : 0 ≤ δ) (hδ' : δ ≤ 5 / 2) (heta : eta ∈ Set.Icc (-1) 1) : 2 + d.h < TerminalEdgeFactor.profileSpeed (TerminalPressure.releasedNormalization d K) d (Real.log K - 1 / 5) (eta, δ) ∧ TerminalEdgeFactor.profileSpeed (TerminalPressure.releasedNormalization d K) d (Real.log K - 1 / 5) (eta, δ) ≤ 2 + 2 * d.h ∧ 3 / 2 ≤ TerminalEdgeFactor.profileConeGap (TerminalPressure.releasedNormalization d K) d (Real.log K - 1 / 5) (eta, δ)

A numerical direction margin on the entire remaining interval, including both closed parameter endpoints and the stress-free terminal edge.

theorem NavierStokes.TerminalCone.profile_relative_cone (d : OutgoingTail.TailData) (hsmall : SmallTail d) {K δ eta : ℝ} (hK : 32 ≤ K) (hδ : 0 < δ) (hδ' : δ ≤ 5 / 2) (heta : eta ∈ Set.Icc (-1) 1) : have C := TerminalPressure.releasedNormalization d K; have y0 := Real.log K - 1 / 5; 0 < TerminalEdgeFactor.profileAngularStress C d y0 (eta, δ) ∧ 2 < TerminalEdgeFactor.profileSpeed C d y0 (eta, δ) ∧ (TerminalEdgeFactor.profileSpeed C d y0 (eta, δ) - 2) * TerminalEdgeFactor.profileAxialStress C d y0 (eta, δ) ^ 2 < 2 * TerminalEdgeFactor.profileAngularStress C d y0 (eta, δ) ^ 2

theorem NavierStokes.TerminalCone.profile_full_true_cone (d : OutgoingTail.TailData) (hsmall : SmallTail d) {K δ eta : ℝ} (hK : 32 ≤ K) (hδ : 0 < δ) (hδ' : δ ≤ 5 / 2) (heta : eta ∈ Set.Icc (-1) 1) : have C := TerminalPressure.releasedNormalization d K; have y0 := Real.log K - 1 / 5; 2 < TerminalEdgeFactor.profileP C d y0 (eta, δ) ∧ TerminalEdgeFactor.profileSpeed C d y0 (eta, δ) < ConeAlgebra.coneBound (TerminalEdgeFactor.profileP C d y0 (eta, δ)) (TerminalEdgeFactor.profileJ C d y0 (eta, δ))

The root-form true cone for the actual heat/taper backward stress, with P-a=Tθ/F and J=Tz/F, on the full switched interval.

The identical compensated outgoing field and the ordered radius choice

theorem NavierStokes.TerminalCone.tailTime_clock (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) (y : ℝ) : Real.log (XR * Real.exp y / OutgoingDilation.switchRadius F XR) + 1 / 5 = y - OutgoingTail.tailStart F.data

theorem NavierStokes.TerminalCone.E_eq_profileAngularVelocity (F : OutgoingProfile.Profile) {XR : ℝ} (c : ℝ → TerminalCompensation.Coeff) (hXR : 0 < XR) {y eta : ℝ} (hy : terminalStart F.data ≤ y) (heta : eta ∈ Set.Icc (-1) 1) : HeatedOutgoing.E F XR c (XR * Real.exp y, eta) = TerminalEdgeFactor.profileAngularVelocity (normalization F XR) F.data (shift F XR) (profilePoint F y eta)

theorem NavierStokes.TerminalCone.U_eq_zero (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) {y eta : ℝ} (hy : terminalStart F.data ≤ y) : HeatedOutgoing.U F XR (XR * Real.exp y, eta) = 0

noncomputable def NavierStokes.TerminalCone.radiusThreshold (F : OutgoingProfile.Profile) : ℝ

Chosen only after the core schedule and h. This bound contains no compensation coefficient or data-dependent edge-collar width.

Equations

• NavierStokes.TerminalCone.radiusThreshold F = 32 / Real.exp (NavierStokes.HeatTailEdit.switchStart F.data)

theorem NavierStokes.TerminalCone.radiusThreshold_pos (F : OutgoingProfile.Profile) : 0 < radiusThreshold F

theorem NavierStokes.TerminalCone.switchRadius_ge_32 (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : radiusThreshold F ≤ XR) : 32 ≤ OutgoingDilation.switchRadius F XR

theorem NavierStokes.TerminalCone.full_interval_true_cone (F : OutgoingProfile.Profile) {XR y eta : ℝ} (hsmall : SmallTail F.data) (hXR : radiusThreshold F ≤ XR) (hy : terminalStart F.data ≤ y) (hy' : y < OutgoingTail.tailEnd F.data) (heta : eta ∈ Set.Icc (-1) 1) : 2 < TerminalEdgeFactor.profileP (normalization F XR) F.data (shift F XR) (profilePoint F y eta) ∧ TerminalEdgeFactor.profileSpeed (normalization F XR) F.data (shift F XR) (profilePoint F y eta) < ConeAlgebra.coneBound (TerminalEdgeFactor.profileP (normalization F XR) F.data (shift F XR) (profilePoint F y eta)) (TerminalEdgeFactor.profileJ (normalization F XR) F.data (shift F XR) (profilePoint F y eta))

theorem NavierStokes.TerminalCone.full_interval_direction_margin (F : OutgoingProfile.Profile) {XR y eta : ℝ} (hsmall : SmallTail F.data) (hXR : radiusThreshold F ≤ XR) (hy : terminalStart F.data ≤ y) (hy' : y ≤ OutgoingTail.tailEnd F.data) (heta : eta ∈ Set.Icc (-1) 1) : 2 + F.data.h < TerminalEdgeFactor.profileSpeed (normalization F XR) F.data (shift F XR) (profilePoint F y eta) ∧ TerminalEdgeFactor.profileSpeed (normalization F XR) F.data (shift F XR) (profilePoint F y eta) ≤ 2 + 2 * F.data.h ∧ 3 / 2 ≤ TerminalEdgeFactor.profileConeGap (normalization F XR) F.data (shift F XR) (profilePoint F y eta)

theorem NavierStokes.TerminalCone.same_witness_full_cone (F : OutgoingProfile.Profile) {XR C y eta : ℝ} (w : HeatedOutgoing.CompensationWitness F XR C) (hsmall : SmallTail F.data) (hXR : radiusThreshold F ≤ XR) (hy : terminalStart F.data ≤ y) (hy' : y < OutgoingTail.tailEnd F.data) (heta : eta ∈ Set.Icc (-1) 1) : HeatedOutgoing.E F XR w.coefficients (XR * Real.exp y, eta) = TerminalEdgeFactor.profileAngularVelocity (normalization F XR) F.data (shift F XR) (profilePoint F y eta) ∧ HeatedOutgoing.U F XR (XR * Real.exp y, eta) = 0 ∧ 2 < TerminalEdgeFactor.profileP (normalization F XR) F.data (shift F XR) (profilePoint F y eta) ∧ TerminalEdgeFactor.profileSpeed (normalization F XR) F.data (shift F XR) (profilePoint F y eta) < ConeAlgebra.coneBound (TerminalEdgeFactor.profileP (normalization F XR) F.data (shift F XR) (profilePoint F y eta)) (TerminalEdgeFactor.profileJ (normalization F XR) F.data (shift F XR) (profilePoint F y eta))

The actual compensated velocity uses precisely the terminal field whose true cone was proved above. The existing witness, its coefficients, and the base outgoing profile are retained.