Weighted bounds for the actual leading stress

The stress consists of the two genuine coefficients in LeadingStress. Its edge factors are transported through the literal finite modulation and the five restored profile histories.

noncomputable def NavierStokes.LeadingStressWeights.stress {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) (p : ProfileHistories.Point) : ℝ × ℝ

Stress, given by (LeadingStress.theta P h p, LeadingStress.axial P h p).

Equations

• NavierStokes.LeadingStressWeights.stress P h p = (NavierStokes.LeadingStress.theta P h p, NavierStokes.LeadingStress.axial P h p)

theorem NavierStokes.LeadingStressWeights.stress_eq {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) {p : ProfileHistories.Point} (hX : 0 < p.1) (hf : P.f p ≠ 0) : stress P h p = P.f p • (ReferenceBounds.p1 P h p - ActivationContinuation.shearA P p, ReferenceBounds.p2 P h p - ActivationContinuation.shearB P p)

theorem NavierStokes.LeadingStressWeights.stress_contDiffAt {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 ℝ (↑⊤) (stress P h) p

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

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

Equations

• NavierStokes.LeadingStressWeights.stressDomain P h = {p : NavierStokes.ProfileHistories.Point | p ∈ D.carrier ∧ 0 < p.1 ∧ P.f p ≠ 0 ∧ NavierStokes.NaturalAxisData.L h p.2 ≠ 0}

theorem NavierStokes.LeadingStressWeights.stressDomain_open {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) : IsOpen (stressDomain P h)

theorem NavierStokes.LeadingStressWeights.stress_smooth {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) : ContDiffOn ℝ (↑⊤) (stress P h) (stressDomain P h)

noncomputable def NavierStokes.LeadingStressWeights.logPoint (p : ℝ × ℝ) : ProfileHistories.Point

Log point, given by (Real.exp p.2, p.1).

Equations

• NavierStokes.LeadingStressWeights.logPoint p = (Real.exp p.2, p.1)

theorem NavierStokes.LeadingStressWeights.logPoint_smooth : ContDiff ℝ (↑⊤) logPoint

noncomputable def NavierStokes.LeadingStressWeights.logStress {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) : ℝ × ℝ → ℝ × ℝ

Log stress, given by stress P h ∘ logPoint.

Equations

• NavierStokes.LeadingStressWeights.logStress P h = NavierStokes.LeadingStressWeights.stress P h ∘ NavierStokes.LeadingStressWeights.logPoint

noncomputable def NavierStokes.LeadingStressWeights.logStressDomain {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) : Set (ℝ × ℝ)

Log stress domain, given by logPoint ⁻¹' stressDomain P h.

Equations

• NavierStokes.LeadingStressWeights.logStressDomain P h = NavierStokes.LeadingStressWeights.logPoint ⁻¹' NavierStokes.LeadingStressWeights.stressDomain P h

theorem NavierStokes.LeadingStressWeights.logStressDomain_open {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) : IsOpen (logStressDomain P h)

theorem NavierStokes.LeadingStressWeights.logStress_smooth {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) : ContDiffOn ℝ (↑⊤) (logStress P h) (logStressDomain P h)

theorem NavierStokes.LeadingStressWeights.stress_eq_of_coordinates {D D' : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (Q : ProfileHistories.Profiles D') (h : ℝ) {p : ProfileHistories.Point} (hX : 0 < p.1) (hQ : Q.f p ≠ 0) (hf : P.f p = Q.f p) (ha : ActivationContinuation.shearA P p = ActivationContinuation.shearA Q p) (hb : ActivationContinuation.shearB P p = ActivationContinuation.shearB Q p) (hp1 : ReferenceBounds.p1 P h p = ReferenceBounds.p1 Q h p) (hp2 : ReferenceBounds.p2 P h p = ReferenceBounds.p2 Q h p) : stress P h p = stress Q h p

theorem NavierStokes.LeadingStressWeights.stress_outside {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {p : ProfileHistories.Point} (hX : 0 < p.1) (hη : p.2 ∈ Set.Icc (-1) 1) (hout : p.1 < d.modulation.left ∨ (ModulatedProfileAssembly.repairPatch W).right < p.1) : stress v.profiles F.data.h p = stress W.profiles F.data.h p

theorem NavierStokes.LeadingStressWeights.logStress_mem {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {p : ℝ × ℝ} (hη : p.1 ∈ Set.Icc (-1) 1) : p ∈ logStressDomain v.profiles F.data.h

theorem NavierStokes.LeadingStressWeights.activation_shears (N : ReferencePath.Input) {T delta : ℝ} (hT : 0 < T) (hd : 0 < delta) (hdlim : 2 * delta < ReferencePath.rampLimit) (kappa : ℝ) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (y : ℝ) {eta : ℝ} (hη : eta ∈ ReferencePath.parameterInterval) : have P := StressActivation.FromReference.histories N hT hd hdlim kappa P0 hP0; ActivationContinuation.shearA P (StressActivation.radius N.endpoint y, eta) = StressActivation.actualP1 T kappa (StressActivation.FromReference.refLog N delta) (y, eta) ∧ ActivationContinuation.shearB P (StressActivation.radius N.endpoint y, eta) = StressActivation.actualP2 T kappa N.endpoint (StressActivation.FromReference.refLog N delta) (StressActivation.FromReference.refAxial N delta) (y, eta)

theorem NavierStokes.LeadingStressWeights.activation_stress (N : ReferencePath.Input) {T delta : ℝ} (hT : 0 < T) (hd : 0 < delta) (hdlim : 2 * delta < ReferencePath.rampLimit) (kappa h : ℝ) (P0 : ℝ → ℝ) (hP0 : ContDiff ℝ (↑⊤) P0) (y : ℝ) {eta : ℝ} (hη : eta ∈ ReferencePath.parameterInterval) : have P := StressActivation.FromReference.histories N hT hd hdlim kappa P0 hP0; stress P h (StressActivation.radius N.endpoint y, eta) = ActivationCone.activatedStress h N.endpoint (ActivationStocks.FromReference.initial N hd hdlim P0 hP0) (StressActivation.FromReference.refLog N delta) (StressActivation.FromReference.refAxial N delta) T kappa (y, eta)

noncomputable def NavierStokes.LeadingStressWeights.activationProfiles {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : ProfileHistories.Profiles W.axis.referenceInput.radialDomain

Activation profiles, constructed using FromReference.histories.

Equations

• NavierStokes.LeadingStressWeights.activationProfiles W = NavierStokes.StressActivation.FromReference.histories W.axis.referenceInput ⋯ ⋯ ⋯ W.controls.kappa F.axisDatum ⋯

noncomputable def NavierStokes.LeadingStressWeights.activationStress {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : ProfileHistories.Point → ℝ × ℝ

Activation stress, constructed using ActivationCone.activatedStress.

Equations

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

theorem NavierStokes.LeadingStressWeights.nominal_activation_stress {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {y eta : ℝ} (hy : y ≤ W.controls.referenceWidth) (hη : eta ∈ Set.Icc (-1) 1) : stress W.profiles F.data.h (NominalConeAssembly.chart (NominalConeAssembly.activeLeft W) (y, eta)) = activationStress W (y, eta)

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

Inner width, given by min W.controls.referenceWidth (Real.log (d.modulation.left / NominalConeAssembly.activeLeft W)).

Equations

• NavierStokes.LeadingStressWeights.innerWidth _v = min W.controls.referenceWidth (Real.log (d.modulation.left / NavierStokes.NominalConeAssembly.activeLeft W))

theorem NavierStokes.LeadingStressWeights.innerWidth_pos {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) : 0 < innerWidth v

theorem NavierStokes.LeadingStressWeights.inner_chart_before {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {x : ℝ} (hx : x < innerWidth v) : NominalConeAssembly.activeLeft W * Real.exp x < d.modulation.left

theorem NavierStokes.LeadingStressWeights.modulated_activation_stress {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {x eta : ℝ} (hx : x < innerWidth v) (hη : eta ∈ Set.Icc (-1) 1) : ActiveAnnulusWeight.leftChart (Real.log (NominalConeAssembly.activeLeft W)) (logStress v.profiles F.data.h) (eta, x) = activationStress W (x, eta)

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

Left edge, given by Real.log (NominalConeAssembly.activeLeft W).

Equations

• NavierStokes.LeadingStressWeights.leftEdge W = Real.log (NavierStokes.NominalConeAssembly.activeLeft W)

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

Right edge, given by Real.log (NominalConeAssembly.activeRight W).

Equations

• NavierStokes.LeadingStressWeights.rightEdge W = Real.log (NavierStokes.NominalConeAssembly.activeRight W)

theorem NavierStokes.LeadingStressWeights.rightEdge_eq {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : rightEdge W = Real.log W.controls.radius + OutgoingTail.tailEnd F.data

theorem NavierStokes.LeadingStressWeights.rightEdge_shift {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : rightEdge W = TerminalHistoryBridge.shift F W.controls.radius + 3

theorem NavierStokes.LeadingStressWeights.edges_ordered {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : leftEdge W < rightEdge W

theorem NavierStokes.LeadingStressWeights.nominal_terminal_stress {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {y eta : ℝ} (hy : TerminalCone.terminalStart F.data ≤ y) (hη : eta ∈ Set.Icc (-1) 1) : stress W.profiles F.data.h (NominalConeAssembly.chart W.controls.radius (y, eta)) = TerminalEdgeFactor.profileStress (TerminalHistoryBridge.normalization F W.controls.radius) F.data (TerminalHistoryBridge.shift F W.controls.radius) (eta, OutgoingTail.tailEnd F.data - y)

theorem NavierStokes.LeadingStressWeights.activeRight_pos {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : 0 < NominalConeAssembly.activeRight W

theorem NavierStokes.LeadingStressWeights.right_chart_eq {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (x : ℝ) : Real.exp (rightEdge W - x) = W.controls.radius * Real.exp (OutgoingTail.tailEnd F.data - x)

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

Outer width, given by min 1 (Real.log (NominalConeAssembly.activeRight W / (ModulatedProfileAssembly.repairPatch W).right)).

Equations

• NavierStokes.LeadingStressWeights.outerWidth _v = min 1 (Real.log (NavierStokes.NominalConeAssembly.activeRight W / (NavierStokes.ModulatedProfileAssembly.repairPatch W).right))

theorem NavierStokes.LeadingStressWeights.outerWidth_pos {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) : 0 < outerWidth v

theorem NavierStokes.LeadingStressWeights.outer_chart_after {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {x : ℝ} (hx : x < outerWidth v) : (ModulatedProfileAssembly.repairPatch W).right < Real.exp (rightEdge W - x)

theorem NavierStokes.LeadingStressWeights.modulated_terminal_stress {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {x eta : ℝ} (hx : x < outerWidth v) (hη : eta ∈ Set.Icc (-1) 1) : ActiveAnnulusWeight.rightChart (rightEdge W) (logStress v.profiles F.data.h) (eta, x) = TerminalEdgeFactor.profileStress (TerminalHistoryBridge.normalization F W.controls.radius) F.data (TerminalHistoryBridge.shift F W.controls.radius) (eta, x)

theorem NavierStokes.LeadingStressWeights.stress_zero_after {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {p : ProfileHistories.Point} (hX : NominalConeAssembly.activeRight W ≤ p.1) (hη : p.2 ∈ Set.Icc (-1) 1) : stress v.profiles F.data.h p = 0

The actual two leading stresses vanish on the whole terminal exterior, including the edge. All five histories, not just the velocity, are retained.

noncomputable def NavierStokes.LeadingStressWeights.FullTrueCone {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) : Prop

The actual full-annulus cone delivered by the finite modulation theorem.

Equations

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

theorem NavierStokes.LeadingStressWeights.stress_ne_zero {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (hcone : FullTrueCone v) {p : ProfileHistories.Point} (hl : NominalConeAssembly.activeLeft W < p.1) (hr : p.1 < NominalConeAssembly.activeRight W) (hη : p.2 ∈ Set.Icc (-1) 1) : stress v.profiles F.data.h p ≠ 0

theorem NavierStokes.LeadingStressWeights.logStress_ne_zero {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (hcone : FullTrueCone v) {eta y : ℝ} (hη : eta ∈ Set.Icc (-1) 1) (hy : y ∈ Set.Ioo (leftEdge W) (rightEdge W)) : logStress v.profiles F.data.h (eta, y) ≠ 0

theorem NavierStokes.LeadingStressWeights.kappa_lt_one {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (hcone : FullTrueCone v) : W.controls.kappa < 1

A full true cone rules out the inactive value kappa = 1. This is derived for the supplied final witness, without choosing new controls.

theorem NavierStokes.LeadingStressWeights.weighted_bounds {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (hcone : FullTrueCone v) : ActiveAnnulusWeight.WeightedBounds (Set.Icc (-1) 1) (W.controls.activationTime ^ 2) (leftEdge W) (rightEdge W) (logStress v.profiles F.data.h)

Equation (20) for the same final finite-modulation witness. The tensor bounds contain every mixed profile derivative, in both logarithmic and physical radial charts.

noncomputable def NavierStokes.LeadingStressWeights.logShearA {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ℝ × ℝ) : ℝ

Log shear A, given by ActivationContinuation.shearA P (logPoint p).

Equations

• NavierStokes.LeadingStressWeights.logShearA P p = NavierStokes.ActivationContinuation.shearA P (NavierStokes.LeadingStressWeights.logPoint p)

noncomputable def NavierStokes.LeadingStressWeights.logShearB {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ℝ × ℝ) : ℝ

Log shear B, given by ActivationContinuation.shearB P (logPoint p).

Equations

• NavierStokes.LeadingStressWeights.logShearB P p = NavierStokes.ActivationContinuation.shearB P (NavierStokes.LeadingStressWeights.logPoint p)

noncomputable def NavierStokes.LeadingStressWeights.logSpeed {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ℝ × ℝ) : ℝ

Log speed, given by ActivationContinuation.shearSize (logShearA P p) (logShearB P p).

Equations

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

noncomputable def NavierStokes.LeadingStressWeights.logSlope {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (p : ℝ × ℝ) : ℝ

Log slope, given by logShearB P p / logShearA P p.

Equations

• NavierStokes.LeadingStressWeights.logSlope P p = NavierStokes.LeadingStressWeights.logShearB P p / NavierStokes.LeadingStressWeights.logShearA P p

theorem NavierStokes.LeadingStressWeights.shearSize_eq (a b : ℝ) : ActivationContinuation.shearSize a b = a + b ^ 2 / a

theorem NavierStokes.LeadingStressWeights.shears_outside {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {p : ProfileHistories.Point} (hX : 0 < p.1) (hη : p.2 ∈ Set.Icc (-1) 1) (hout : p.1 < d.modulation.left ∨ (ModulatedProfileAssembly.repairPatch W).right < p.1) : ActivationContinuation.shearA v.profiles p = ActivationContinuation.shearA W.profiles p ∧ ActivationContinuation.shearB v.profiles p = ActivationContinuation.shearB W.profiles p

theorem NavierStokes.LeadingStressWeights.nominal_activation_shears {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {y eta : ℝ} (hy : y ≤ W.controls.referenceWidth) (hη : eta ∈ Set.Icc (-1) 1) : have N := W.axis.referenceInput; have L := StressActivation.FromReference.refLog N W.controls.referenceWidth; have U := StressActivation.FromReference.refAxial N W.controls.referenceWidth; have p := NominalConeAssembly.chart (NominalConeAssembly.activeLeft W) (y, eta); ActivationContinuation.shearA W.profiles p = StressActivation.actualP1 W.controls.activationTime W.controls.kappa L (y, eta) ∧ ActivationContinuation.shearB W.profiles p = StressActivation.actualP2 W.controls.activationTime W.controls.kappa N.endpoint L U (y, eta)

theorem NavierStokes.LeadingStressWeights.modulated_activation_shears {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {x eta : ℝ} (hx : x < innerWidth v) (hη : eta ∈ Set.Icc (-1) 1) : have N := W.axis.referenceInput; have L := StressActivation.FromReference.refLog N W.controls.referenceWidth; have U := StressActivation.FromReference.refAxial N W.controls.referenceWidth; logShearA v.profiles (eta, leftEdge W + x) = StressActivation.actualP1 W.controls.activationTime W.controls.kappa L (x, eta) ∧ logShearB v.profiles (eta, leftEdge W + x) = StressActivation.actualP2 W.controls.activationTime W.controls.kappa N.endpoint L U (x, eta)

theorem NavierStokes.LeadingStressWeights.modulated_activation_speed_slope {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {x eta : ℝ} (hx : x < innerWidth v) (hη : eta ∈ Set.Icc (-1) 1) : have N := W.axis.referenceInput; have L := StressActivation.FromReference.refLog N W.controls.referenceWidth; have U := StressActivation.FromReference.refAxial N W.controls.referenceWidth; ActiveAnnulusWeight.leftChart (leftEdge W) (logSpeed v.profiles) (eta, x) = StressActivation.shearSize W.controls.activationTime W.controls.kappa N.endpoint L U (x, eta) ∧ ActiveAnnulusWeight.leftChart (leftEdge W) (logSlope v.profiles) (eta, x) = StressActivation.shearSlope W.controls.activationTime W.controls.kappa N.endpoint L U (x, eta)

theorem NavierStokes.LeadingStressWeights.nominal_terminal_shears {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {y eta : ℝ} (hy : TerminalCone.terminalStart F.data ≤ y) (hη : eta ∈ Set.Icc (-1) 1) : have p := NominalConeAssembly.chart W.controls.radius (y, eta); ActivationContinuation.shearA W.profiles p = TerminalEdgeFactor.profileSpeed (TerminalHistoryBridge.normalization F W.controls.radius) F.data (TerminalHistoryBridge.shift F W.controls.radius) (eta, OutgoingTail.tailEnd F.data - y) ∧ ActivationContinuation.shearB W.profiles p = 0

theorem NavierStokes.LeadingStressWeights.modulated_terminal_shears {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {x eta : ℝ} (hx : x < outerWidth v) (hη : eta ∈ Set.Icc (-1) 1) : logShearA v.profiles (eta, rightEdge W - x) = TerminalEdgeFactor.profileSpeed (TerminalHistoryBridge.normalization F W.controls.radius) F.data (TerminalHistoryBridge.shift F W.controls.radius) (eta, x) ∧ logShearB v.profiles (eta, rightEdge W - x) = 0

theorem NavierStokes.LeadingStressWeights.modulated_terminal_speed_slope {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {x eta : ℝ} (hx : x < outerWidth v) (hη : eta ∈ Set.Icc (-1) 1) : ActiveAnnulusWeight.rightChart (rightEdge W) (logSpeed v.profiles) (eta, x) = TerminalEdgeFactor.profileSpeed (TerminalHistoryBridge.normalization F W.controls.radius) F.data (TerminalHistoryBridge.shift F W.controls.radius) (eta, x) ∧ ActiveAnnulusWeight.rightChart (rightEdge W) (logSlope v.profiles) (eta, x) = 0

theorem NavierStokes.LeadingStressWeights.trueDirection_transfer {K : Set ℝ} {T S B : ℝ × ℝ → ℝ × ℝ} {u s u' s' : ℝ × ℝ → ℝ} {w w' : ℝ} (hdir : ActiveAnnulusWeight.HasTrueDirectionCollar K T B u s w) (hw' : 0 < w') (hT : ∀ eta ∈ K, ∀ (x : ℝ), 0 < x → x < w' → S (eta, x) = T (eta, x)) (hu : ∀ eta ∈ K, ∀ (x : ℝ), 0 ≤ x → x < w' → u' (eta, x) = u (eta, x)) (hs : ∀ eta ∈ K, ∀ (x : ℝ), 0 ≤ x → x < w' → s' (eta, x) = s (eta, x)) : ActiveAnnulusWeight.HasTrueDirectionCollar K S B u' s' w'

Transfer a genuine smooth directional extension through exact local stress and shear identities. Shrinking keeps all closed collar endpoints.

theorem NavierStokes.LeadingStressWeights.inner_direction {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (hcone : FullTrueCone v) : ∃ (G : ActiveAnnulusWeight.EdgeFactor (Set.Icc (-1) 1) (W.controls.activationTime ^ 2) (ActiveAnnulusWeight.leftChart (leftEdge W) (logStress v.profiles F.data.h))), ActiveAnnulusWeight.HasTrueDirectionCollar (Set.Icc (-1) 1) (ActiveAnnulusWeight.leftChart (leftEdge W) (logStress v.profiles F.data.h)) G.coefficient (ActiveAnnulusWeight.leftChart (leftEdge W) (logSpeed v.profiles)) (ActiveAnnulusWeight.leftChart (leftEdge W) (logSlope v.profiles)) G.width

The actual stress has the inner flat factor and a smooth unit direction with strict margins for the actual modulated shear.

theorem NavierStokes.LeadingStressWeights.outer_direction {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) : ∃ (G : ActiveAnnulusWeight.EdgeFactor (Set.Icc (-1) 1) 4 (ActiveAnnulusWeight.rightChart (rightEdge W) (logStress v.profiles F.data.h))), ActiveAnnulusWeight.HasTrueDirectionCollar (Set.Icc (-1) 1) (ActiveAnnulusWeight.rightChart (rightEdge W) (logStress v.profiles F.data.h)) G.coefficient (ActiveAnnulusWeight.rightChart (rightEdge W) (logSpeed v.profiles)) (ActiveAnnulusWeight.rightChart (rightEdge W) (logSlope v.profiles)) G.width

The inverse-cubic terminal factor has a smooth nonzero direction, with strict cone margin through the true terminal edge.

theorem NavierStokes.LeadingStressWeights.inner_shear_edge {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : 0 < logShearA v.profiles (eta, leftEdge W) ∧ 2 < logSpeed v.profiles (eta, leftEdge W)

theorem NavierStokes.LeadingStressWeights.outer_shear_edge {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {eta : ℝ} (hη : eta ∈ Set.Icc (-1) 1) : 0 < logShearA v.profiles (eta, rightEdge W) ∧ 2 < logSpeed v.profiles (eta, rightEdge W)

theorem NavierStokes.LeadingStressWeights.closed_shear_positive {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (hcone : FullTrueCone v) {eta y : ℝ} (hη : eta ∈ Set.Icc (-1) 1) (hy : y ∈ Set.Icc (leftEdge W) (rightEdge W)) : 0 < logShearA v.profiles (eta, y) ∧ 2 < logSpeed v.profiles (eta, y)

The reference shear remains strictly admissible also at the two closed annulus endpoints; the strict interior is the actual modulation theorem.

theorem NavierStokes.LeadingStressWeights.inner_angular_positive {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (hcone : FullTrueCone v) : ∃ (r : ℝ), 0 < r ∧ r < innerWidth v ∧ ∀ eta ∈ Set.Icc (-1) 1, ∀ (x : ℝ), 0 < x → x ≤ r → 0 < (ActiveAnnulusWeight.leftChart (leftEdge W) (logStress v.profiles F.data.h) (eta, x)).1

theorem NavierStokes.LeadingStressWeights.outer_angular_positive {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) : ∃ (r : ℝ), 0 < r ∧ r < outerWidth v ∧ ∀ eta ∈ Set.Icc (-1) 1, ∀ (x : ℝ), 0 < x → x ≤ r → 0 < (ActiveAnnulusWeight.rightChart (rightEdge W) (logStress v.profiles F.data.h) (eta, x)).1

noncomputable def NavierStokes.LeadingStressWeights.activationSpeed {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (q : ℝ × ℝ) : ℝ

Activation speed, constructed using shearSize.

Equations

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

noncomputable def NavierStokes.LeadingStressWeights.activationSlope {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (q : ℝ × ℝ) : ℝ

Activation slope, constructed using shearSlope.

Equations

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

theorem NavierStokes.LeadingStressWeights.activation_direction_positive {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (hκ : W.controls.kappa < 1) : ∃ (G : ActiveAnnulusWeight.EdgeFactor (Set.Icc (-1) 1) (W.controls.activationTime ^ 2) fun (q : ℝ × ℝ) => activationStress W (q.2, q.1)), (∀ eta ∈ Set.Icc (-1) 1, 0 < (G.coefficient (eta, 0)).1) ∧ ActiveAnnulusWeight.HasTrueDirectionCollar (Set.Icc (-1) 1) (fun (q : ℝ × ℝ) => activationStress W (q.2, q.1)) G.coefficient (activationSpeed W) (activationSlope W) G.width

theorem NavierStokes.LeadingStressWeights.inner_direction_positive {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (hcone : FullTrueCone v) : ∃ (G : ActiveAnnulusWeight.EdgeFactor (Set.Icc (-1) 1) (W.controls.activationTime ^ 2) (ActiveAnnulusWeight.leftChart (leftEdge W) (logStress v.profiles F.data.h))), (∀ eta ∈ Set.Icc (-1) 1, 0 < (G.coefficient (eta, 0)).1) ∧ ActiveAnnulusWeight.HasTrueDirectionCollar (Set.Icc (-1) 1) (ActiveAnnulusWeight.leftChart (leftEdge W) (logStress v.profiles F.data.h)) G.coefficient (ActiveAnnulusWeight.leftChart (leftEdge W) (logSpeed v.profiles)) (ActiveAnnulusWeight.leftChart (leftEdge W) (logSlope v.profiles)) G.width

A single actual inner factor carries both the positive angular orientation and the strict directional certificate.

theorem NavierStokes.LeadingStressWeights.outer_direction_positive {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) : ∃ (G : ActiveAnnulusWeight.EdgeFactor (Set.Icc (-1) 1) 4 (ActiveAnnulusWeight.rightChart (rightEdge W) (logStress v.profiles F.data.h))), (∀ eta ∈ Set.Icc (-1) 1, 0 < (G.coefficient (eta, 0)).1) ∧ ActiveAnnulusWeight.HasTrueDirectionCollar (Set.Icc (-1) 1) (ActiveAnnulusWeight.rightChart (rightEdge W) (logStress v.profiles F.data.h)) G.coefficient (ActiveAnnulusWeight.rightChart (rightEdge W) (logSpeed v.profiles)) (ActiveAnnulusWeight.rightChart (rightEdge W) (logSlope v.profiles)) G.width

The actual terminal inverse-cubic factor, with its positive angular orientation and strict directional certificate on the same factor.

theorem NavierStokes.LeadingStressWeights.activationStress_zero_of_nonpos {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {x eta : ℝ} (hx : x ≤ 0) (hη : eta ∈ Set.Icc (-1) 1) : activationStress W (x, eta) = 0

theorem NavierStokes.LeadingStressWeights.logStress_zero_before {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {eta y : ℝ} (hy : y ≤ leftEdge W) (hη : eta ∈ Set.Icc (-1) 1) : logStress v.profiles F.data.h (eta, y) = 0

theorem NavierStokes.LeadingStressWeights.stress_zero_before {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {p : ProfileHistories.Point} (hX : 0 ≤ p.1) (hbefore : p.1 ≤ NominalConeAssembly.activeLeft W) (hη : p.2 ∈ Set.Icc (-1) 1) : stress v.profiles F.data.h p = 0

Both actual leading stress components are zero on the entire inner physical region, with the axis included by their literal formulas.

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

The actual product weight, with the two fixed physical attachment points and the same activation time used to construct the profile.

Equations

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

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

Distance, given by edgeDistance (leftEdge W) (rightEdge W) (Real.log X).

Equations

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

theorem NavierStokes.LeadingStressWeights.zeta_positive {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {X : ℝ} (hX : X ∈ Set.Ioo (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W)) : 0 < zeta v X

theorem NavierStokes.LeadingStressWeights.radialPullback_eq {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) {q : ℝ × ℝ} (hX : 0 < q.2) : ActiveAnnulusWeight.radialPullback (logStress P h) q = stress P h (q.2, q.1)

theorem NavierStokes.LeadingStressWeights.radialPullback_jet_eq {D : ProfileHistories.RadialDomain} (P : ProfileHistories.Profiles D) (h : ℝ) {q : ℝ × ℝ} (hX : 0 < q.2) (n : ℕ) : iteratedFDeriv ℝ n (ActiveAnnulusWeight.radialPullback (logStress P h)) q = iteratedFDeriv ℝ n (fun (p : ℝ × ℝ) => stress P h (p.2, p.1)) q

theorem NavierStokes.LeadingStressWeights.stress_lower_bound {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (hcone : FullTrueCone v) : ∃ (c : ℝ), 0 < c ∧ ∀ (p : ProfileHistories.Point), p.1 ∈ Set.Ioo (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W) → p.2 ∈ Set.Icc (-1) 1 → c * zeta v p.1 ≤ ‖stress v.profiles F.data.h p‖

A positive multiple of the actual radial product weight is below the norm of the literal two leading stress components.

theorem NavierStokes.LeadingStressWeights.physical_jet_bound {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (hcone : FullTrueCone v) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ eta ∈ Set.Icc (-1) 1, ∀ X ∈ Set.Ioo (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W), ‖iteratedFDeriv ℝ n (fun (p : ℝ × ℝ) => stress v.profiles F.data.h (p.2, p.1)) (eta, X)‖ ≤ C * zeta v X / distance v X ^ N

Every actual mixed physical profile tensor has the same flat product weight, with a finite derivative-dependent inverse-distance loss.

theorem NavierStokes.LeadingStressWeights.exists_weighted_profile : ∃ (F : OutgoingProfile.Profile) (W : NominalProfile.Witness F) (d : ModulatedProfileAssembly.LoopData W) (v : ModulatedProfileAssembly.Witness d), FullTrueCone v ∧ ActiveAnnulusWeight.WeightedBounds (Set.Icc (-1) 1) (W.controls.activationTime ^ 2) (leftEdge W) (rightEdge W) (logStress v.profiles F.data.h) ∧ (∃ (G : ActiveAnnulusWeight.EdgeFactor (Set.Icc (-1) 1) (W.controls.activationTime ^ 2) (ActiveAnnulusWeight.leftChart (leftEdge W) (logStress v.profiles F.data.h))), (∀ eta ∈ Set.Icc (-1) 1, 0 < (G.coefficient (eta, 0)).1) ∧ ActiveAnnulusWeight.HasTrueDirectionCollar (Set.Icc (-1) 1) (ActiveAnnulusWeight.leftChart (leftEdge W) (logStress v.profiles F.data.h)) G.coefficient (ActiveAnnulusWeight.leftChart (leftEdge W) (logSpeed v.profiles)) (ActiveAnnulusWeight.leftChart (leftEdge W) (logSlope v.profiles)) G.width) ∧ ∃ (G : ActiveAnnulusWeight.EdgeFactor (Set.Icc (-1) 1) 4 (ActiveAnnulusWeight.rightChart (rightEdge W) (logStress v.profiles F.data.h))), (∀ eta ∈ Set.Icc (-1) 1, 0 < (G.coefficient (eta, 0)).1) ∧ ActiveAnnulusWeight.HasTrueDirectionCollar (Set.Icc (-1) 1) (ActiveAnnulusWeight.rightChart (rightEdge W) (logStress v.profiles F.data.h)) G.coefficient (ActiveAnnulusWeight.rightChart (rightEdge W) (logSpeed v.profiles)) (ActiveAnnulusWeight.rightChart (rightEdge W) (logSlope v.profiles)) G.width

One no-input instance of the complete actual weighted profile and its two oriented strict edge-direction certificates.