Exact dynamics of the selected primary pulses

The native equation uses the same selected frame, covariance amplitude and pressure as CorrectionInitialization.ActualPrimary. Its homogeneous equation is localized to the Gaussian support: the outer attachment cutoff is deliberately differentiated outside that support.

@[reducible, inline]

abbrev NavierStokes.ActualPrimaryDynamics.Native : Type

Native: an abbreviation for ActualSignedGeometry.Native.

Equations

• NavierStokes.ActualPrimaryDynamics.Native = NavierStokes.ActualSignedGeometry.Native

@[reducible, inline]

abbrev NavierStokes.ActualPrimaryDynamics.Space : Type

Space: an abbreviation for ProblemStatement.Space.

Equations

• NavierStokes.ActualPrimaryDynamics.Space = NavierStokes.ProblemStatement.Space

theorem NavierStokes.ActualPrimaryDynamics.frame_tail_ne {I : Type u_1} {U : PhaseJetBounds.Domain I PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction U) (i : I) {z : PhaseCalculus.Slow × ℝ} (hz : z ∈ (U.slot P.V ⋯).carrier i) : MovingFrameODE.tail (P.phase.normal i z) ≠ 0

theorem NavierStokes.ActualPrimaryDynamics.frame_normal {I : Type u_1} {U : PhaseJetBounds.Domain I PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction U) (i : I) {z : PhaseCalculus.Slow × ℝ} (hz : z ∈ (U.slot P.V ⋯).carrier i) : (P.frame i).normal z = P.phase.normal i z

theorem NavierStokes.ActualPrimaryDynamics.frame_motion {I : Type u_1} {U : PhaseJetBounds.Domain I PhaseCalculus.Slow} (P : PrimaryPulseBounds.PhaseConstruction U) (i : I) {z : PhaseCalculus.Slow × ℝ} (hz : z ∈ (U.slot P.V ⋯).carrier i) : (P.frame i).normalMotion z = P.phase.velocity i z

theorem NavierStokes.ActualPrimaryDynamics.rawVelocity_hasDerivAt {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : Native} (hp : x.1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier L) (ht : x.2.2 ∈ Set.Ioo 0 ((CorrectionInitialization.ActualPrimary.phases B N0 j).L L)) : HasDerivAt (fun (t : ℝ) => CorrectionInitialization.ActualPrimary.rawVelocity j L (x.1, x.2.1, t)) (TangentProjection.projectedRhs ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.normal L (CorrectionInitialization.ActualPrimary.phasePoint L x)) ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.velocity L (CorrectionInitialization.ActualPrimary.phasePoint L x)) (CorrectionInitialization.ActualPrimary.rawVelocity j L x) ((PrimaryCopyBridge.baseOperator ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.F L x.1) ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.shear L (CorrectionInitialization.ActualPrimary.phasePoint L x))) (CorrectionInitialization.ActualPrimary.rawVelocity j L x)) 0 (((CorrectionInitialization.ActualPrimary.phases B N0 j).frame L).viscosity (CorrectionInitialization.ActualPrimary.phasePoint L x))) x.2.2

theorem NavierStokes.ActualPrimaryDynamics.frame_viscosity {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (x : Native) : ((CorrectionInitialization.ActualPrimary.phases B N0 j).frame L).viscosity (CorrectionInitialization.ActualPrimary.phasePoint L x) = ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L) * ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) ^ 2 * ‖(CorrectionInitialization.ActualPrimary.phases B N0 j).phase.normal L (CorrectionInitialization.ActualPrimary.phasePoint L x)‖ ^ 2

theorem NavierStokes.ActualPrimaryDynamics.rawVelocity_hasDerivAt_on_slot {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : Native} (hT : 0 < x.1.2.2) (ht : x.2.2 ∈ Set.Ioo 0 ((CorrectionInitialization.ActualPrimary.phases B N0 j).L L)) : HasDerivAt (fun (t : ℝ) => CorrectionInitialization.ActualPrimary.rawVelocity j L (x.1, x.2.1, t)) (TangentProjection.projectedRhs ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.normal L (CorrectionInitialization.ActualPrimary.phasePoint L x)) ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.velocity L (CorrectionInitialization.ActualPrimary.phasePoint L x)) (CorrectionInitialization.ActualPrimary.rawVelocity j L x) ((PrimaryCopyBridge.baseOperator ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.F L x.1) ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.shear L (CorrectionInitialization.ActualPrimary.phasePoint L x))) (CorrectionInitialization.ActualPrimary.rawVelocity j L x)) 0 (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L) * ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) ^ 2 * ‖(CorrectionInitialization.ActualPrimary.phases B N0 j).phase.normal L (CorrectionInitialization.ActualPrimary.phasePoint L x)‖ ^ 2)) x.2.2

theorem NavierStokes.ActualPrimaryDynamics.gaussian_slot {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : Native} (hg : CorrectionInitialization.ActualPrimary.gaussian L x ≠ 0) : x.2.2 ∈ Set.Ioo 0 ((CorrectionInitialization.ActualPrimary.phases B N0 0).L L)

theorem NavierStokes.ActualPrimaryDynamics.outerCutoff_one_germ {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : Native} (hg : CorrectionInitialization.ActualPrimary.gaussian L x ≠ 0) : (fun (t : ℝ) => PrimaryCopyBounds.outerCutoff (t / (CorrectionInitialization.ActualPrimary.phases B N0 0).L L)) =ᶠ[nhds x.2.2] fun (x : ℝ) => 1

theorem NavierStokes.ActualPrimaryDynamics.attachedVelocity_hasDerivAt {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : Native} (hT : 0 < x.1.2.2) (hg : CorrectionInitialization.ActualPrimary.gaussian L x ≠ 0) : HasDerivAt (fun (t : ℝ) => CorrectionInitialization.ActualPrimary.attachedRawVelocity j L (x.1, x.2.1, t)) (TangentProjection.projectedRhs ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.normal L (CorrectionInitialization.ActualPrimary.phasePoint L x)) ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.velocity L (CorrectionInitialization.ActualPrimary.phasePoint L x)) (CorrectionInitialization.ActualPrimary.attachedRawVelocity j L x) ((PrimaryCopyBridge.baseOperator ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.F L x.1) ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.shear L (CorrectionInitialization.ActualPrimary.phasePoint L x))) (CorrectionInitialization.ActualPrimary.attachedRawVelocity j L x)) 0 (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L) * ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) ^ 2 * ‖(CorrectionInitialization.ActualPrimary.phases B N0 j).phase.normal L (CorrectionInitialization.ActualPrimary.phasePoint L x)‖ ^ 2)) x.2.2

theorem NavierStokes.ActualPrimaryDynamics.attachedPressure_eq {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) {x : Native} (hg : CorrectionInitialization.ActualPrimary.gaussian L x ≠ 0) : CorrectionInitialization.ActualPrimary.attachedRawPressure j L x = Complex.I * ↑(TangentProjection.pressureCoefficient ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.normal L (CorrectionInitialization.ActualPrimary.phasePoint L x)) ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.velocity L (CorrectionInitialization.ActualPrimary.phasePoint L x)) (CorrectionInitialization.ActualPrimary.attachedRawVelocity j L x) ((PrimaryCopyBridge.baseOperator ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.F L x.1) ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.shear L (CorrectionInitialization.ActualPrimary.phasePoint L x))) (CorrectionInitialization.ActualPrimary.attachedRawVelocity j L x)) 0) / ↑↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L))

theorem NavierStokes.ActualPrimaryDynamics.geometry_radial {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : (CorrectionInitialization.ActualPrimary.geometry j L).coordinateLinear CorrectionInitialization.ActualPrimary.radialVector = (ChartScales.Lambda ^ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L), 0)

theorem NavierStokes.ActualPrimaryDynamics.geometry_temporal {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : (CorrectionInitialization.ActualPrimary.geometry j L).coordinateLinear CorrectionInitialization.ActualPrimary.temporalVector = (0, (ChartScales.Q (BaseChartJets.cellBand L) ^ (1 + CorrectionInitialization.ActualPrimary.h))⁻¹)

noncomputable def NavierStokes.ActualPrimaryDynamics.absoluteNativeLinear {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : ActualPrimaryCoherence.Absolute →L[ℝ] Native

Absolute native linear, bundling toFun, map_add, map_smul, cont.

Equations

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

noncomputable def NavierStokes.ActualPrimaryDynamics.copyLinear {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : CorrectionInitialization.ActualPrimary.FullPoint →L[ℝ] Native

Copy linear, given by (absoluteNativeLinear j L).comp (ActualPrimaryCoherence.absoluteChart n).toContinuousLinearMap.

Equations

• NavierStokes.ActualPrimaryDynamics.copyLinear j L n = NavierStokes.ActualPrimaryDynamics.absoluteNativeLinear j L ∘SL ↑(NavierStokes.ActualPrimaryCoherence.absoluteChart n)

noncomputable def NavierStokes.ActualPrimaryDynamics.copyPoint {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : Native

Copy point, given by (nativeSlow L (toAbsolute n x.1), (geometry j L).coordinates k (toAbsolute n x.1).2).

Equations

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

theorem NavierStokes.ActualPrimaryDynamics.copyPoint_affine {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : copyPoint j L n k x = (copyLinear j L n) x + (0, (CorrectionInitialization.ActualPrimary.geometry j L).coordinates k 0)

theorem NavierStokes.ActualPrimaryDynamics.copyPoint_hasFDerivAt {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : HasFDerivAt (copyPoint j L n k) (copyLinear j L n) x

theorem NavierStokes.ActualPrimaryDynamics.copyPoint_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) : ContDiff ℝ (↑⊤) (copyPoint j L n k)

noncomputable def NavierStokes.ActualPrimaryDynamics.clockScale {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ℝ

Clock scale, given by ChartScales.Q n ^ (1+h) / ChartScales.Q (BaseChartJets.cellBand L) ^ (1+h).

Equations

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

noncomputable def NavierStokes.ActualPrimaryDynamics.radialScale {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ℝ

Radial scale, given by Real.sqrt (ChartScales.Q n) / Real.sqrt (ChartScales.Q (BaseChartJets.cellBand L)).

Equations

• NavierStokes.ActualPrimaryDynamics.radialScale L n = √(NavierStokes.ChartScales.Q n) / √(NavierStokes.ChartScales.Q (NavierStokes.BaseChartJets.cellBand L))

noncomputable def NavierStokes.ActualPrimaryDynamics.velocityScale {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ℝ

Velocity scale, given by ChartScales.Q n ^ CoordinateAlgebra.A h / ChartScales.Q (BaseChartJets.cellBand L) ^ CoordinateAlgebra.A h.

Equations

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

theorem NavierStokes.ActualPrimaryDynamics.copyLinear_fast {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) : (copyLinear j L n) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).fastField n x) = (0, 0, clockScale L n)

theorem NavierStokes.ActualPrimaryDynamics.copyPoint_fast_line {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) (t : ℝ) : copyPoint j L n k (x + t • (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).fastField n x) = ((copyPoint j L n k x).1, (copyPoint j L n k x).2.1, (copyPoint j L n k x).2.2 + t * clockScale L n)

noncomputable def NavierStokes.ActualPrimaryDynamics.slotLinear {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : CorrectionInitialization.ActualPrimary.FullPoint →L[ℝ] PhaseCalculus.Slot

Slot linear as an element of FullPoint →L[ℝ] PhaseCalculus.Slot.

Equations

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

noncomputable def NavierStokes.ActualPrimaryDynamics.slotPoint {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : PhaseCalculus.Slot

Slot point, given by ((copyPoint j L n k x).1,(x.2,(copyPoint j L n k x).2.2)).

Equations

• NavierStokes.ActualPrimaryDynamics.slotPoint j L n k x = ((NavierStokes.ActualPrimaryDynamics.copyPoint j L n k x).1, x.2, (NavierStokes.ActualPrimaryDynamics.copyPoint j L n k x).2.2)

theorem NavierStokes.ActualPrimaryDynamics.slotLinear_apply {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) : (slotLinear j L n) x = (((copyLinear j L n) x).1, x.2, ((copyLinear j L n) x).2.2)

theorem NavierStokes.ActualPrimaryDynamics.slotPoint_hasFDerivAt {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : HasFDerivAt (slotPoint j L n k) (slotLinear j L n) x

theorem NavierStokes.ActualPrimaryDynamics.slotLinear_radial {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) : (slotLinear j L n) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).radialField n x) = radialScale L n • PhaseCalculus.eR

theorem NavierStokes.ActualPrimaryDynamics.slotLinear_angular {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) : (slotLinear j L n) (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).angular = PhaseCalculus.eTheta

theorem NavierStokes.ActualPrimaryDynamics.radialScale_epsilon {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : radialScale L n * ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L) = √(ChartScales.Q n) / ChartScales.Q (BaseChartJets.cellBand L) ^ CoordinateAlgebra.D CorrectionInitialization.ActualPrimary.h

theorem NavierStokes.ActualPrimaryDynamics.slotLinear_axial {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (x : CorrectionInitialization.ActualPrimary.FullPoint) : (slotLinear j L n) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).axialField (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)) n x) = (radialScale L n * ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) • PhaseCalculus.eZ

theorem NavierStokes.ActualPrimaryDynamics.slotPoint_radius {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : (slotPoint j L n k x).1.1 = radialScale L n * x.1.1

theorem NavierStokes.ActualPrimaryDynamics.copyPoint_time_pos {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hT : 0 < x.1.2.1.1) : 0 < (copyPoint j L n k x).1.2.2

theorem NavierStokes.ActualPrimaryDynamics.along_copy {B N0 : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (f : Native → E) {x : CorrectionInitialization.ActualPrimary.FullPoint} {v : E} (hd : HasDerivAt (fun (t : ℝ) => f ((copyPoint j L n k x).1, (copyPoint j L n k x).2.1, t)) v (copyPoint j L n k x).2.2) (hf : DifferentiableAt ℝ (fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => f (copyPoint j L n k y)) x) : HarmonicCalculus.along ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).fastField n) (fun (y : LocalSignedRequest.Point × ℝ) => f (copyPoint j L n k y)) x = clockScale L n • v

Transport of an actual native time derivative. This also applies to the unweighted fundamental and to later signed amplitudes.

noncomputable def NavierStokes.ActualPrimaryDynamics.coefficientPoint {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (x : CorrectionInitialization.ActualPrimary.FullPoint) : Native

Coefficient point, given by (nativeSlow L (toAbsolute n x.1), (toAbsolute n x.1).2).

Equations

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

theorem NavierStokes.ActualPrimaryDynamics.coefficientPoint_smooth {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiff ℝ (↑⊤) (coefficientPoint L n)

noncomputable def NavierStokes.ActualPrimaryDynamics.nativePhase {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) : PhaseCalculus.Slot → ℝ

Native phase, constructed using PhaseCalculus.phase.

Equations

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

theorem NavierStokes.ActualPrimaryDynamics.phase_germ {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hc : (copyPoint j L n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow L).core) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).phase n =ᶠ[nhds x] fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) / ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n) * nativePhase j L (slotPoint j L n k y)

theorem NavierStokes.ActualPrimaryDynamics.cutoff_eq_copy {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hc : (copyPoint j L n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow L).core) : CorrectionInitialization.ActualPrimary.chartCutoff j L n x = CorrectionInitialization.ActualPrimary.gaussian L (copyPoint j L n k x)

theorem NavierStokes.ActualPrimaryDynamics.velocityScale_eq {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : velocityScale L n = ChartScales.Q n ^ CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h * ChartScales.Q (BaseChartJets.cellBand L) ^ (-CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)

theorem NavierStokes.ActualPrimaryDynamics.pressureScale_eq {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : velocityScale L n ^ 2 = ChartScales.Q n ^ (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) * ChartScales.Q (BaseChartJets.cellBand L) ^ (-(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h))

noncomputable def NavierStokes.ActualPrimaryDynamics.copyAmplitude {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : HarmonicCalculus.ComplexVector

Copy amplitude, given by velocityScale L n • CurlClassBounds.complexify (attachedRawVelocity j L (copyPoint j L n k x)).

Equations

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

noncomputable def NavierStokes.ActualPrimaryDynamics.copyPressure {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : ℂ

Copy pressure, given by velocityScale L n ^ 2 • attachedRawPressure j L (copyPoint j L n k x).

Equations

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

theorem NavierStokes.ActualPrimaryDynamics.amplitude_germ {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hc : (copyPoint j L n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow L).core) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).amplitude n =ᶠ[nhds x] copyAmplitude j L n k

theorem NavierStokes.ActualPrimaryDynamics.pressure_germ {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hc : (copyPoint j L n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow L).core) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).pressure n =ᶠ[nhds x] copyPressure j L n k

theorem NavierStokes.ActualPrimaryDynamics.coefficient_zero_germs {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hc : ∀ (k : TorusInverse.Frequency), (copyPoint j L n k x).2 ∉ (CorrectionInitialization.ActualPrimary.clockWindow L).core) : ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).amplitude n =ᶠ[nhds x] fun (x : CorrectionInitialization.ActualPrimary.FullPoint) => 0) ∧ (CorrectionInitialization.ActualPrimary.chartCoefficients j L).pressure n =ᶠ[nhds x] fun (x : CorrectionInitialization.ActualPrimary.FullPoint) => 0

theorem NavierStokes.ActualPrimaryDynamics.radialScale_pos {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : 0 < radialScale L n

theorem NavierStokes.ActualPrimaryDynamics.velocityScale_pos {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : 0 < velocityScale L n

theorem NavierStokes.ActualPrimaryDynamics.clockScale_eq {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : clockScale L n = PhysicalParticularWave.clockWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand L))

theorem NavierStokes.ActualPrimaryDynamics.radialScale_eq {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : radialScale L n = PhysicalParticularWave.ratioPower (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand L)) (1 / 2)

theorem NavierStokes.ActualPrimaryDynamics.clockScale_factor {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : clockScale L n = velocityScale L n * radialScale L n

theorem NavierStokes.ActualPrimaryDynamics.copyPoint_radius_pos {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hR : 0 < x.1.1) : 0 < (copyPoint j L n k x).1.1

theorem NavierStokes.ActualPrimaryDynamics.native_base_differentiable {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hR : 0 < x.1.1) (hT : 0 < x.1.2.1.1) : DifferentiableAt ℝ ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.F L) (copyPoint j L n k x).1 ∧ DifferentiableAt ℝ ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.G L) (copyPoint j L n k x).1

noncomputable def NavierStokes.ActualPrimaryDynamics.normalScale {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ℝ

Normal scale, given by ((ChartScales.carrier h (BaseChartJets.cellBand L) : ℝ) / (ChartScales.carrier h n : ℝ)) * radialScale L n.

Equations

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

theorem NavierStokes.ActualPrimaryDynamics.normalScale_pos {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : 0 < normalScale L n

theorem NavierStokes.ActualPrimaryDynamics.normal_eq_copy {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hR : 0 < x.1.1) (hT : 0 < x.1.2.1.1) (hc : (copyPoint j L n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow L).core) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).normal (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)) (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)) n x = normalScale L n • (CorrectionInitialization.ActualPrimary.phases B N0 j).phase.normal L (CorrectionInitialization.ActualPrimary.phasePoint L (copyPoint j L n k x))

theorem NavierStokes.ActualPrimaryDynamics.frequency_germ {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hR : 0 < x.1.1) (hT : 0 < x.1.2.1.1) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).frequencyBase n =ᶠ[nhds x] fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => clockScale L n * (CorrectionInitialization.ActualPrimary.phases B N0 j).phase.F L (copyPoint j L n k y).1

theorem NavierStokes.ActualPrimaryDynamics.axial_germ {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hT : 0 < x.1.2.1.1) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).axialBase n =ᶠ[nhds x] fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => velocityScale L n * (CorrectionInitialization.ActualPrimary.phases B N0 j).phase.G L (copyPoint j L n k y).1

theorem NavierStokes.ActualPrimaryDynamics.slow_radial_derivative {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (a : ℝ) (f : PhaseCalculus.Slow → ℝ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hf : DifferentiableAt ℝ f (copyPoint j L n k x).1) : HarmonicCalculus.along ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).radialField n) (fun (y : LocalSignedRequest.Point × ℝ) => a * f (copyPoint j L n k y).1) x = a * radialScale L n * PhaseCalculus.slowR f (copyPoint j L n k x).1

theorem NavierStokes.ActualPrimaryDynamics.copy_shear_function {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (v : Native → Space) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hR : 0 < x.1.1) (hT : 0 < x.1.2.1.1) : LinearWaveResidual.shear ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).radius n) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).frequencyBase n) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).axialBase n) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).radialField n) (fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => velocityScale L n • CurlClassBounds.complexify (v (copyPoint j L n k y))) x = (clockScale L n * velocityScale L n) • CurlClassBounds.complexify ((PrimaryCopyBridge.baseOperator ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.F L (copyPoint j L n k x).1) ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.shear L (CorrectionInitialization.ActualPrimary.phasePoint L (copyPoint j L n k x)))) (v (copyPoint j L n k x)))

theorem NavierStokes.ActualPrimaryDynamics.copy_shear {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hR : 0 < x.1.1) (hT : 0 < x.1.2.1.1) : LinearWaveResidual.shear ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).radius n) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).frequencyBase n) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).axialBase n) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).radialField n) (copyAmplitude j L n k) x = (clockScale L n * velocityScale L n) • CurlClassBounds.complexify ((PrimaryCopyBridge.baseOperator ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.F L (copyPoint j L n k x).1) ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.shear L (CorrectionInitialization.ActualPrimary.phasePoint L (copyPoint j L n k x)))) (CorrectionInitialization.ActualPrimary.attachedRawVelocity j L (copyPoint j L n k x)))

theorem NavierStokes.ActualPrimaryDynamics.epsilon_scale {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n * radialScale L n ^ 2 = clockScale L n * ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)

theorem NavierStokes.ActualPrimaryDynamics.damping_scale {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (N : Space) : ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n * ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n) ^ 2 * ‖normalScale L n • N‖ ^ 2 = clockScale L n * (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L) * ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand L)) ^ 2 * ‖N‖ ^ 2)

noncomputable def NavierStokes.ActualPrimaryDynamics.copyVelocity {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : Space

Copy velocity, given by velocityScale L n • attachedRawVelocity j L (copyPoint j L n k x).

Equations

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

noncomputable def NavierStokes.ActualPrimaryDynamics.copyMotion {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : Space

Copy motion, given by (normalScale L n * clockScale L n) • (phases B N0 j).phase.velocity L (phasePoint L (copyPoint j L n k x)).

Equations

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

noncomputable def NavierStokes.ActualPrimaryDynamics.copyAction {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : Space

Copy action as an element of Space.

Equations

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

theorem NavierStokes.ActualPrimaryDynamics.copyVelocity_differentiable {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hT : 0 < x.1.2.1.1) : DifferentiableAt ℝ (copyVelocity j L n k) x

theorem NavierStokes.ActualPrimaryDynamics.copyVelocity_ode {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hR : 0 < x.1.1) (hT : 0 < x.1.2.1.1) (hc : (copyPoint j L n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow L).core) (hg : CorrectionInitialization.ActualPrimary.chartCutoff j L n x ≠ 0) : HarmonicCalculus.along ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).fastField n) (copyVelocity j L n k) x = TangentProjection.projectedRhs ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).normal (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)) (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)) n x) (copyMotion j L n k x) (copyVelocity j L n k x) (copyAction j L n k x) 0 (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n * ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n) ^ 2 * ‖(CorrectionInitialization.ActualPrimary.chartCoefficients j L).normal (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)) (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)) n x‖ ^ 2)

theorem NavierStokes.ActualPrimaryDynamics.pressure_scale_algebra {K Kr r : ℝ} (hK : K ≠ 0) (hKr : Kr ≠ 0) (hr : r ≠ 0) (b c : ℝ) : b ^ 2 • (Complex.I * ↑c / ↑Kr) = Complex.I * ↑(b * r * b / (Kr / K * r) * c) / ↑K

theorem NavierStokes.ActualPrimaryDynamics.copyPressure_projected {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hR : 0 < x.1.1) (hT : 0 < x.1.2.1.1) (hc : (copyPoint j L n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow L).core) (hg : CorrectionInitialization.ActualPrimary.chartCutoff j L n x ≠ 0) : copyPressure j L n k x = ParticularWaveBounds.projectedPressure (↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).normal (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)) (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)) n) (copyMotion j L n k) (copyVelocity j L n k) (copyAction j L n k) (fun (x : CorrectionInitialization.ActualPrimary.FullPoint) => 0) x

theorem NavierStokes.ActualPrimaryDynamics.copy_principal_zero {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hR : 0 < x.1.1) (hT : 0 < x.1.2.1.1) (hc : (copyPoint j L n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow L).core) (hg : CorrectionInitialization.ActualPrimary.chartCutoff j L n x ≠ 0) : LinearWaveResidual.principal (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h n) (↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).radius n) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).frequencyBase n) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).axialBase n) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).radialField n) (fun (x : CorrectionInitialization.ActualPrimary.FullPoint) => (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).angular) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).axialField (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)) n) ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).fastField n) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).phase n) (copyAmplitude j L n k) (copyPressure j L n k) x = 0

theorem NavierStokes.ActualPrimaryDynamics.principal_zero_on_cutoff {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hR : 0 < x.1.1) (hT : 0 < x.1.2.1.1) (hg : CorrectionInitialization.ActualPrimary.chartCutoff j L n x ≠ 0) : (CorrectionInitialization.ActualPrimary.chartCoefficients j L).principal (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)) (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)) n x = 0

The global attachment only satisfies the homogeneous equation on the actual Gaussian support. No band-nearness or global slot premise occurs.

theorem NavierStokes.ActualPrimaryDynamics.localLinearIdentity {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : LinearWaveBounds.WaveCoefficients E) (s : WeightedClasses.StripData E) (d : LinearWaveBounds.GraphDirections E) (ψ : ℕ → E → ℝ) (f : ℕ → E → HarmonicCalculus.ComplexVector) (n : ℕ) {Ω : Set E} (hg : LocalizedWaveBounds.ExactOn ((a.withCutoff ψ).addAmplitude f) s d n Ω) {x : E} (hx : x ∈ Ω) (hA : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => a.amplitude n y i) x) (hψ : DifferentiableAt ℝ (ψ n) x) (hf : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => f n y i) x) (hz : ψ n x • a.principal s d n x = 0) (i : Fin 3) : (((a.withCutoff ψ).addAmplitude f).harmonicResidual s d n x i).re = (HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) (a.goodCoefficient s d ψ f n) x i).re + (HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) (LinearWaveBounds.excludedSlotError d ψ a.amplitude 0 n) x i).re

The exact cutoff and curl algebra only needs the localized principal equation. The actual primary application below supplies every hypothesis.

theorem NavierStokes.ActualPrimaryDynamics.absoluteChart_positive (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ ActualPrimaryCoherence.positiveRadialChart) : (ActualPrimaryCoherence.absoluteChart n) x ∈ ActualPrimaryCoherence.positiveRadialAbsolute

theorem NavierStokes.ActualPrimaryDynamics.amplitude_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).amplitude n) ActualPrimaryCoherence.positiveRadialChart

theorem NavierStokes.ActualPrimaryDynamics.pressure_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).pressure n) ActualPrimaryCoherence.positiveRadialChart

theorem NavierStokes.ActualPrimaryDynamics.cutoff_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiff ℝ (↑⊤) (CorrectionInitialization.ActualPrimary.chartCutoff j L n)

theorem NavierStokes.ActualPrimaryDynamics.phase_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).phase n) ActualPrimaryCoherence.positiveRadialChart

theorem NavierStokes.ActualPrimaryDynamics.exactAmplitude_smooth {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((CorrectionInitialization.ActualPrimary.piece U j L).exactCoefficients.amplitude n) ActualPrimaryCoherence.positiveRadialChart

theorem NavierStokes.ActualPrimaryDynamics.curl_smooth {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) (((CorrectionInitialization.ActualPrimary.chartCoefficients j L).withCutoff (CorrectionInitialization.ActualPrimary.chartCutoff j L)).curlCorrection (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)) (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)) n) ActualPrimaryCoherence.positiveRadialChart

theorem NavierStokes.ActualPrimaryDynamics.base_smooth {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ ActualPrimaryCoherence.positiveRadialChart) : ContDiffAt ℝ (↑⊤) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).radialBase n) x ∧ ContDiffAt ℝ (↑⊤) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).frequencyBase n) x ∧ ContDiffAt ℝ (↑⊤) ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).axialBase n) x

theorem NavierStokes.ActualPrimaryDynamics.exactOn {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) : LocalizedWaveBounds.ExactOn (CorrectionInitialization.ActualPrimary.piece U j L).exactCoefficients (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)) (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)) n ActualPrimaryCoherence.positiveRadialChart

theorem NavierStokes.ActualPrimaryDynamics.linearResidual_eq {B N0 : ℕ} (U : LocalSignedRequest.SlowRegion (2 * CorrectionInitialization.ActualPrimary.h)) (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x ∈ ActualPrimaryCoherence.positiveRadialChart) (i : Fin 3) : (CorrectionInitialization.ActualPrimary.piece U j L).linearResidual n x i = (CorrectionInitialization.ActualPrimary.piece U j L).linearGoodField n x i + (CorrectionInitialization.ActualPrimary.piece U j L).excluded n x i

Exact decomposition of the same selected, attached, periodized and curl-corrected primary piece. The Gaussian derivative is retained.

theorem NavierStokes.ActualPrimaryDynamics.linearResidual_eq_on_strip {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hx : x.1 ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) (i : Fin 3) : (CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion j L).linearResidual n x i = (CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion j L).linearGoodField n x i + (CorrectionInitialization.ActualPrimary.piece CorrectionInitialization.ActualPrimary.standardRegion j L).excluded n x i