The spectral cone of the actual aligned modulated base

This module binds the generic profile and physical-shear identities to the same finite modulation, aligned coefficient family, and covariance target.

The same finite modulated profile and aligned slow coefficients

theorem NavierStokes.AlignedProfileSpectralCone.modulated_fields_radial_germ {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {p : ProfileHistories.Point} (hX : 0 < p.1) (heta : |p.2| ≤ 1) : ((fun (X : ℝ) => (EntranceAlignedBase.modulatedCoefficients H v).phi 0 (X, p.2)) =ᶠ[nhds p.1] fun (X : ℝ) => W.axis.normalization * v.profiles.f (X, p.2)) ∧ (fun (X : ℝ) => (EntranceAlignedBase.modulatedCoefficients H v).axial 0 (X, p.2)) =ᶠ[nhds p.1] fun (X : ℝ) => v.profiles.U (X, p.2)

theorem NavierStokes.AlignedProfileSpectralCone.modulated_frequency_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {p : ProfileSpectralCone.Slow} (hT : 0 < p.2.2) (hR : 0 < p.1) : BaseChartJets.leadingFrequency F.data.h W.axis.normalization (EntranceAlignedBase.modulatedCoefficients H v) p = (BaseChartJets.normalizedCoordinates F.data.h p).1 ^ (-CoordinateAlgebra.A F.data.h - 1 / 2) * v.profiles.f (BaseChartJets.normalizedCoordinates F.data.h p).2

theorem NavierStokes.AlignedProfileSpectralCone.modulated_frequency_pos {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {p : ProfileSpectralCone.Slow} (hT : 0 < p.2.2) (hR : 0 < p.1) : 0 < BaseChartJets.leadingFrequency F.data.h W.axis.normalization (EntranceAlignedBase.modulatedCoefficients H v) p

theorem NavierStokes.AlignedProfileSpectralCone.modulated_shear_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {p : ProfileSpectralCone.Slow} (hT : 0 < p.2.2) (hR : 0 < p.1) : PhaseEstimates.shearVector (BaseChartJets.leadingFrequency F.data.h W.axis.normalization (EntranceAlignedBase.modulatedCoefficients H v)) (BaseChartJets.leadingAxial F.data.h (EntranceAlignedBase.modulatedCoefficients H v)) p = BaseChartJets.leadingFrequency F.data.h W.axis.normalization (EntranceAlignedBase.modulatedCoefficients H v) p • !₂[-ModulatedCone.angularShear v.profiles.E (BaseChartJets.normalizedCoordinates F.data.h p).2, -ModulatedCone.signedAxialShear v.profiles.E v.profiles.U (BaseChartJets.normalizedCoordinates F.data.h p).2]

theorem NavierStokes.AlignedProfileSpectralCone.modulated_spectral_cones {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (hcone : ∀ (w : ProfileHistories.Point), NominalConeAssembly.activeLeft W < w.1 → w.1 < NominalConeAssembly.activeRight W → w.2 ∈ Set.Icc (-1) 1 → TrueConeLoop.InTrueCone (ActivationStocks.profileStockOne v.profiles F.data.h w) (ActivationStocks.profileStockTwo v.profiles F.data.h w) (ModulatedCone.angularShear v.profiles.E w) (ModulatedCone.signedAxialShear v.profiles.E v.profiles.U w)) {p : ProfileSpectralCone.Slow} (hT : 0 < p.2.2) (hR : 0 < p.1) (hl : NominalConeAssembly.activeLeft W < (BaseChartJets.normalizedCoordinates F.data.h p).2.1) (hr : (BaseChartJets.normalizedCoordinates F.data.h p).2.1 < NominalConeAssembly.activeRight W) : have F₀ := BaseChartJets.leadingFrequency F.data.h W.axis.normalization (EntranceAlignedBase.modulatedCoefficients H v); have G₀ := BaseChartJets.leadingAxial F.data.h (EntranceAlignedBase.modulatedCoefficients H v); PrimaryRepresentatives.ReferenceCone (F₀ p) (PhaseEstimates.shearVector F₀ G₀ p) ∧ PrimaryRepresentatives.TargetCone (F₀ p) (PhaseEstimates.shearVector F₀ G₀ p) (ProfileSpectralCone.stressVector v.profiles F.data.h (BaseChartJets.normalizedCoordinates F.data.h p).2)

The primitive true-cone conclusion of the actual finite modulation is converted into the two spectral cones for its own leading fields.

theorem NavierStokes.AlignedProfileSpectralCone.modulated_chartTarget_cones {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (hcone : ∀ (w : ProfileHistories.Point), NominalConeAssembly.activeLeft W < w.1 → w.1 < NominalConeAssembly.activeRight W → w.2 ∈ Set.Icc (-1) 1 → TrueConeLoop.InTrueCone (ActivationStocks.profileStockOne v.profiles F.data.h w) (ActivationStocks.profileStockTwo v.profiles F.data.h w) (ModulatedCone.angularShear v.profiles.E w) (ModulatedCone.signedAxialShear v.profiles.E v.profiles.U w)) {p : ProfileSpectralCone.Slow} (hT : 0 < p.2.2) (hR : 0 < p.1) (hl : NominalConeAssembly.activeLeft W < (BaseChartJets.normalizedCoordinates F.data.h p).2.1) (hr : (BaseChartJets.normalizedCoordinates F.data.h p).2.1 < NominalConeAssembly.activeRight W) {q : ℝ} (hq : 0 < q) (N : ℕ) (U : PartitionedCovariance.UnsignedLabel) : have coeff := EntranceAlignedBase.modulatedCoefficients H v; have w := (BaseChartJets.normalizedCoordinates F.data.h p).2; have F₀ := BaseChartJets.leadingFrequency F.data.h W.axis.normalization coeff; have G₀ := BaseChartJets.leadingAxial F.data.h coeff; have T := PartitionedCovariance.chartTarget F.data.h q N ![coeff.stressTheta 0 w, coeff.stressAxial 0 w] U; PrimaryRepresentatives.ReferenceCone (F₀ p) (PhaseEstimates.shearVector F₀ G₀ p) ∧ PrimaryRepresentatives.TargetCone (F₀ p) (PhaseEstimates.shearVector F₀ G₀ p) !₂[T 0, T 1]

The literal covariance target is a positive chart rescaling of the same actual zeroth stress coefficients.

theorem NavierStokes.AlignedProfileSpectralCone.modulated_continuousOn {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {K : Set ProfileSpectralCone.Slow} (hpos : ∀ p ∈ K, 0 < p.2.2 ∧ 0 < p.1) : have F₀ := BaseChartJets.leadingFrequency F.data.h W.axis.normalization (EntranceAlignedBase.modulatedCoefficients H v); have G₀ := BaseChartJets.leadingAxial F.data.h (EntranceAlignedBase.modulatedCoefficients H v); ContinuousOn F₀ K ∧ ContinuousOn (PhaseEstimates.shearVector F₀ G₀) K ∧ ContinuousOn (fun (p : BaseChartJets.Slow) => ProfileSpectralCone.stressVector v.profiles F.data.h (BaseChartJets.normalizedCoordinates F.data.h p).2) K

Continuity of the actual leading frequency, actual radial shear, and actual leading stress follows from the constructed smooth profile.

theorem NavierStokes.AlignedProfileSpectralCone.modulated_compact_bounds {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (hcone : LeadingStressWeights.FullTrueCone v) {K : Set ProfileSpectralCone.Slow} (hK : IsCompact K) (hpos : ∀ p ∈ K, 0 < p.2.2 ∧ 0 < p.1) (hactive : ∀ p ∈ K, NominalConeAssembly.activeLeft W < (BaseChartJets.normalizedCoordinates F.data.h p).2.1 ∧ (BaseChartJets.normalizedCoordinates F.data.h p).2.1 < NominalConeAssembly.activeRight W) : have F₀ := BaseChartJets.leadingFrequency F.data.h W.axis.normalization (EntranceAlignedBase.modulatedCoefficients H v); have G₀ := BaseChartJets.leadingAxial F.data.h (EntranceAlignedBase.modulatedCoefficients H v); have g₀ := PhaseEstimates.shearVector F₀ G₀; have T₀ := fun (p : BaseChartJets.Slow) => ProfileSpectralCone.stressVector v.profiles F.data.h (BaseChartJets.normalizedCoordinates F.data.h p).2; ∃ (M : ℝ) (u : ℝ) (eta : ℝ) (delta : ℝ), 1 ≤ M ∧ 0 < u ∧ 0 < eta ∧ 0 < delta ∧ (∀ p ∈ K, PrimaryRepresentatives.ParameterBounds M p.1 (F₀ p) (g₀ p)) ∧ ∀ p₀ ∈ K, ∀ p ∈ K, dist p p₀ < delta → inner ℝ (T₀ p) (PrimaryRepresentatives.normalDirection (g₀ p₀)) ≤ -eta ∧ |PrimaryRepresentatives.c0 (F₀ p₀) (g₀ p₀) * inner ℝ (T₀ p) (PrimaryRepresentatives.transverseDirection (g₀ p₀)) / inner ℝ (T₀ p) (PrimaryRepresentatives.normalDirection (g₀ p₀))| + eta ≤ PrimaryRepresentatives.slopeRatio u

Uniform reference bounds and one mixed target margin for any compact positive-time subset of the actual active annulus.

A single Euclidean direction through both zero-amplitude edges

noncomputable def NavierStokes.AlignedProfileSpectralCone.planeOfPair : ℝ × ℝ →L[ℝ] ProfileSpectralCone.Plane

Plane of pair, constructed using LinearMap.toContinuousLinearMap.

Equations

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

theorem NavierStokes.AlignedProfileSpectralCone.planeOfPair_injective : Function.Injective ⇑planeOfPair

noncomputable def NavierStokes.AlignedProfileSpectralCone.planeEdgeFactor {J : Set ℝ} {c : ℝ} {S : ℝ × ℝ → ℝ × ℝ} (F : ActiveAnnulusWeight.EdgeFactor J c S) : ActiveAnnulusWeight.EdgeFactor J c fun (p : ℝ × ℝ) => planeOfPair (S p)

Plane edge factor, bundling coefficient, order, width, width_pos and the required compatibility proofs.

Equations

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

theorem NavierStokes.AlignedProfileSpectralCone.normalDirection_pos_smul (T : ProfileSpectralCone.Plane) {c : ℝ} (hc : 0 < c) : PrimaryRepresentatives.normalDirection (c • T) = PrimaryRepresentatives.normalDirection T

noncomputable def NavierStokes.AlignedProfileSpectralCone.gluedDirection (a b : ℝ) (S BL BR : ℝ × ℝ → ProfileSpectralCone.Plane) (p : ℝ × ℝ) : ProfileSpectralCone.Plane

In the interior this is the actual stress normalized in the Euclidean norm. At the two endpoints it uses the corresponding genuine flat factor.

Equations

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

theorem NavierStokes.AlignedProfileSpectralCone.gluedDirection_interior {a b : ℝ} (S BL BR : ℝ × ℝ → ProfileSpectralCone.Plane) {p : ℝ × ℝ} (hp : p.2 ∈ Set.Ioo a b) : gluedDirection a b S BL BR p = PrimaryRepresentatives.normalDirection (S p)

theorem NavierStokes.AlignedProfileSpectralCone.gluedDirection_continuousOn {J : Set ℝ} {a b cL cR : ℝ} {S : ℝ × ℝ → ProfileSpectralCone.Plane} (hab : a < b) (FL : ActiveAnnulusWeight.EdgeFactor J cL (ActiveAnnulusWeight.leftChart a S)) (FR : ActiveAnnulusWeight.EdgeFactor J cR (ActiveAnnulusWeight.rightChart b S)) (hS : ∀ p ∈ J ×ˢ Set.Ioo a b, ContinuousAt S p) (hne : ∀ p ∈ J ×ˢ Set.Ioo a b, S p ≠ 0) : ContinuousOn (gluedDirection a b S FL.coefficient FR.coefficient) (J ×ˢ Set.Icc a b)

theorem NavierStokes.AlignedProfileSpectralCone.gluedDirection_norm {J : Set ℝ} {a b cL cR : ℝ} {S : ℝ × ℝ → ProfileSpectralCone.Plane} (_hab : a < b) (FL : ActiveAnnulusWeight.EdgeFactor J cL (ActiveAnnulusWeight.leftChart a S)) (FR : ActiveAnnulusWeight.EdgeFactor J cR (ActiveAnnulusWeight.rightChart b S)) (hne : ∀ p ∈ J ×ˢ Set.Ioo a b, S p ≠ 0) {p : ℝ × ℝ} (hp : p ∈ J ×ˢ Set.Icc a b) : ‖gluedDirection a b S FL.coefficient FR.coefficient p‖ = 1

noncomputable def NavierStokes.AlignedProfileSpectralCone.logShear {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (omega : ℝ) (p : ℝ × ℝ) : ProfileSpectralCone.Plane

Log shear, given by omega • !₂[-LeadingStressWeights.logShearA v.profiles p, -LeadingStressWeights.logShearB v.profiles p].

Equations

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

theorem NavierStokes.AlignedProfileSpectralCone.exists_closed_direction {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (hcone : LeadingStressWeights.FullTrueCone v) : ∃ (D : ℝ × ℝ → ProfileSpectralCone.Plane), ContinuousOn D (Set.Icc (-1) 1 ×ˢ Set.Icc (LeadingStressWeights.leftEdge W) (LeadingStressWeights.rightEdge W)) ∧ (∀ p ∈ Set.Icc (-1) 1 ×ˢ Set.Icc (LeadingStressWeights.leftEdge W) (LeadingStressWeights.rightEdge W), ‖D p‖ = 1) ∧ (∀ p ∈ Set.Icc (-1) 1 ×ˢ Set.Ioo (LeadingStressWeights.leftEdge W) (LeadingStressWeights.rightEdge W), D p = PrimaryRepresentatives.normalDirection (planeOfPair (LeadingStressWeights.logStress v.profiles F.data.h p))) ∧ ∀ p ∈ Set.Icc (-1) 1 ×ˢ Set.Icc (LeadingStressWeights.leftEdge W) (LeadingStressWeights.rightEdge W), ∀ (omega : ℝ), 0 < omega → PrimaryRepresentatives.ReferenceCone omega (logShear v omega p) ∧ PrimaryRepresentatives.TargetCone omega (logShear v omega p) (D p)

A single actual unit direction, continuous through both flat edges, with the strict spectral target cone on the entire closed annulus.

noncomputable def NavierStokes.AlignedProfileSpectralCone.referenceSet {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : Set ProfileSpectralCone.Slow

Reference set, given by PrimaryRepresentatives.referenceCompact F.data.h (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W).

Equations

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

noncomputable def NavierStokes.AlignedProfileSpectralCone.referenceLogPoint {F : OutgoingProfile.Profile} (_W : NominalProfile.Witness F) (p : ProfileSpectralCone.Slow) : ℝ × ℝ

Reference log point, given by ((PositiveRepresentatives.stableInner F.data.h p).2, Real.log (PositiveRepresentatives.stableInner F.data.h p).1).

Equations

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

structure NavierStokes.AlignedProfileSpectralCone.ReferencePointData {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) (p : ProfileSpectralCone.Slow) : Prop

Reference point data, collecting stable, radius, scalar, inner_pos, parameter, log_mem.

• stable : p ∈ PositiveRepresentatives.stableDomain F.data.h
• radius : 0 < p.1
• scalar : 0 < PositiveRepresentatives.stableQ F.data.h p
• inner_pos : 0 < (PositiveRepresentatives.stableInner F.data.h p).1
• parameter : (PositiveRepresentatives.stableInner F.data.h p).2 ∈ Set.Icc (-1) 1
• log_mem : referenceLogPoint W p ∈ Set.Icc (-1) 1 ×ˢ Set.Icc (LeadingStressWeights.leftEdge W) (LeadingStressWeights.rightEdge W)

theorem NavierStokes.AlignedProfileSpectralCone.referenceSet_compact {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) : IsCompact (referenceSet W)

theorem NavierStokes.AlignedProfileSpectralCone.reference_point {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileSpectralCone.Slow} (hp : p ∈ referenceSet W) : ReferencePointData W p

noncomputable def NavierStokes.AlignedProfileSpectralCone.referenceFrequency {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) : ProfileSpectralCone.Slow → ℝ

Reference frequency, given by PositiveRepresentatives.stablePullback F.data.h (-CoordinateAlgebra.A F.data.h - 1 / 2) v.profiles.f.

Equations

• NavierStokes.AlignedProfileSpectralCone.referenceFrequency v = NavierStokes.PositiveRepresentatives.stablePullback F.data.h (-NavierStokes.CoordinateAlgebra.A F.data.h - 1 / 2) v.profiles.f

noncomputable def NavierStokes.AlignedProfileSpectralCone.referenceShear {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (p : ProfileSpectralCone.Slow) : ProfileSpectralCone.Plane

Reference shear, constructed using referenceFrequency.

Equations

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

theorem NavierStokes.AlignedProfileSpectralCone.referenceFrequency_pos {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) {p : ProfileSpectralCone.Slow} (hp : p ∈ referenceSet W) : 0 < referenceFrequency v p

theorem NavierStokes.AlignedProfileSpectralCone.reference_continuous {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) : ContinuousOn (referenceFrequency v) (referenceSet W) ∧ ContinuousOn (referenceShear v) (referenceSet W) ∧ ContinuousOn (referenceLogPoint W) (referenceSet W)

theorem NavierStokes.AlignedProfileSpectralCone.stableInner_eq_normalized {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {p : ProfileSpectralCone.Slow} (hT : 0 < p.2.2) : PositiveRepresentatives.stableInner F.data.h p = (BaseChartJets.normalizedCoordinates F.data.h p).2

theorem NavierStokes.AlignedProfileSpectralCone.referenceFrequency_eq_actual {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (H : NominalConeAssembly.Certificate W) {p : ProfileSpectralCone.Slow} (hT : 0 < p.2.2) (hR : 0 < p.1) : referenceFrequency v p = BaseChartJets.leadingFrequency F.data.h W.axis.normalization (EntranceAlignedBase.modulatedCoefficients H v) p

theorem NavierStokes.AlignedProfileSpectralCone.referenceShear_eq_actual {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (H : NominalConeAssembly.Certificate W) {p : ProfileSpectralCone.Slow} (hT : 0 < p.2.2) (hR : 0 < p.1) : referenceShear v p = PhaseEstimates.shearVector (BaseChartJets.leadingFrequency F.data.h W.axis.normalization (EntranceAlignedBase.modulatedCoefficients H v)) (BaseChartJets.leadingAxial F.data.h (EntranceAlignedBase.modulatedCoefficients H v)) p

theorem NavierStokes.AlignedProfileSpectralCone.referenceLogPoint_profile {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {p : ProfileSpectralCone.Slow} (hp : p ∈ referenceSet W) : LeadingStressWeights.logPoint (referenceLogPoint W p) = PositiveRepresentatives.stableInner F.data.h p

theorem NavierStokes.AlignedProfileSpectralCone.reference_cone {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (hcone : LeadingStressWeights.FullTrueCone v) {p : ProfileSpectralCone.Slow} (hp : p ∈ referenceSet W) : PrimaryRepresentatives.ReferenceCone (referenceFrequency v p) (referenceShear v p)

theorem NavierStokes.AlignedProfileSpectralCone.modulated_positive_reference_cone {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (H : NominalConeAssembly.Certificate W) (hcone : LeadingStressWeights.FullTrueCone v) {p : ProfileSpectralCone.Slow} (hp : p ∈ PositiveRepresentatives.positivePart (referenceSet W)) : PrimaryRepresentatives.ReferenceCone (BaseChartJets.leadingFrequency F.data.h W.axis.normalization (EntranceAlignedBase.modulatedCoefficients H v) p) (PhaseEstimates.shearVector (BaseChartJets.leadingFrequency F.data.h W.axis.normalization (EntranceAlignedBase.modulatedCoefficients H v)) (BaseChartJets.leadingAxial F.data.h (EntranceAlignedBase.modulatedCoefficients H v)) p)

theorem NavierStokes.AlignedProfileSpectralCone.exists_reference_direction {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (hcone : LeadingStressWeights.FullTrueCone v) : ∃ (T : ProfileSpectralCone.Slow → ProfileSpectralCone.Plane), ContinuousOn T (referenceSet W) ∧ ∀ p ∈ referenceSet W, ‖T p‖ = 1 ∧ PrimaryRepresentatives.ReferenceCone (referenceFrequency v p) (referenceShear v p) ∧ PrimaryRepresentatives.TargetCone (referenceFrequency v p) (referenceShear v p) (T p) ∧ ((PositiveRepresentatives.stableInner F.data.h p).1 ∈ Set.Ioo (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W) → T p = PrimaryRepresentatives.normalDirection (ProfileSpectralCone.stressVector v.profiles F.data.h (PositiveRepresentatives.stableInner F.data.h p)))

The global normalized direction is pulled back by the genuine stable similarity branch. This includes the regular zero-time boundary.

theorem NavierStokes.AlignedProfileSpectralCone.modulated_representative_bounds {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {d : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness d) (H : NominalConeAssembly.Certificate W) (hcone : LeadingStressWeights.FullTrueCone v) : have K := referenceSet W; have F₀ := BaseChartJets.leadingFrequency F.data.h W.axis.normalization (EntranceAlignedBase.modulatedCoefficients H v); have G₀ := BaseChartJets.leadingAxial F.data.h (EntranceAlignedBase.modulatedCoefficients H v); have g₀ := PhaseEstimates.shearVector F₀ G₀; ∃ (T : ProfileSpectralCone.Slow → ProfileSpectralCone.Plane) (M : ℝ) (u : ℝ) (eta : ℝ), 1 ≤ M ∧ 0 < u ∧ 0 < eta ∧ ContinuousOn T K ∧ (∀ p ∈ K, ‖T p‖ = 1) ∧ (∀ p ∈ K, (PositiveRepresentatives.stableInner F.data.h p).1 ∈ Set.Ioo (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W) → T p = PrimaryRepresentatives.normalDirection (ProfileSpectralCone.stressVector v.profiles F.data.h (PositiveRepresentatives.stableInner F.data.h p))) ∧ (∀ (L : PositiveRepresentatives.ActiveLabel K), PrimaryRepresentatives.ParameterBounds M (PositiveRepresentatives.representative K L).1 (F₀ (PositiveRepresentatives.representative K L)) (g₀ (PositiveRepresentatives.representative K L))) ∧ ∃ (N : ℕ), ∀ (L : PositiveRepresentatives.ActiveLabel K), N ≤ (↑L).1 → ∀ p ∈ PositiveRepresentatives.positivePart K, p ∈ PrimaryRepresentatives.gridBox (↑L).1 (↑L).2 2 → inner ℝ (T p) (PrimaryRepresentatives.normalDirection (g₀ (PositiveRepresentatives.representative K L))) ≤ -eta ∧ |PrimaryRepresentatives.c0 (F₀ (PositiveRepresentatives.representative K L)) (g₀ (PositiveRepresentatives.representative K L)) * inner ℝ (T p) (PrimaryRepresentatives.transverseDirection (g₀ (PositiveRepresentatives.representative K L))) / inner ℝ (T p) (PrimaryRepresentatives.normalDirection (g₀ (PositiveRepresentatives.representative K L)))| + eta ≤ PrimaryRepresentatives.slopeRatio u

All reference parameters and the mixed target margin are now derived for the actual positive-time representatives of the same aligned base. The constants and one threshold precede every active band and label.