Exact dynamics of the selected signed unit

The unit is the actual normalized primary pulse in the selected copy chart. Its scalar signed amplitude is deliberately absent here. The time equation, base action, and tangency germ therefore apply to either signed column before the separate scalar multiplication and compact cutoff.

@[reducible, inline]

abbrev NavierStokes.ActualSignedDynamics.Native : Type

Native: an abbreviation for ActualSignedGeometry.Native.

Equations

• NavierStokes.ActualSignedDynamics.Native = NavierStokes.ActualSignedGeometry.Native

@[reducible, inline]

abbrev NavierStokes.ActualSignedDynamics.Space : Type

Space: an abbreviation for ProblemStatement.Space.

Equations

• NavierStokes.ActualSignedDynamics.Space = NavierStokes.ProblemStatement.Space

noncomputable def NavierStokes.ActualSignedDynamics.nativeUnit {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (x : Native) : Space

The actual unweighted unit, before choosing a periodic copy.

Equations

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

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

The selected native unit transported to the full free lift.

Equations

• NavierStokes.ActualSignedDynamics.unitPulse j L n k x = NavierStokes.ActualSignedDynamics.nativeUnit j L (NavierStokes.ActualPrimaryDynamics.copyPoint j L n k x)

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

Unit 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.ActualSignedDynamics.unitAction {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (x : CorrectionInitialization.ActualPrimary.FullPoint) : Space →L[ℝ] Space

Unit action, constructed using clockScale.

Equations

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

theorem NavierStokes.ActualSignedDynamics.pulseCoordinates_contDiff {B N0 : ℕ} (L : CorrectionInitialization.ActualPrimary.Label B N0) : ContDiff ℝ (↑⊤) (CorrectionInitialization.ActualPrimary.pulseCoordinates L)

theorem NavierStokes.ActualSignedDynamics.nativeUnit_contDiffAt {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 / (CorrectionInitialization.ActualPrimary.phases B N0 j).L L ∈ Set.Ioo 0 1) : ContDiffAt ℝ (↑⊤) (nativeUnit j L) x

theorem NavierStokes.ActualSignedDynamics.unitPulse_contDiffAt {B N0 : ℕ} (j : Fin 2) (L : CorrectionInitialization.ActualPrimary.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {x : CorrectionInitialization.ActualPrimary.FullPoint} (hp : (ActualPrimaryDynamics.copyPoint j L n k x).1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier L) (ht : (ActualPrimaryDynamics.copyPoint j L n k x).2.2 / (CorrectionInitialization.ActualPrimary.phases B N0 j).L L ∈ Set.Ioo 0 1) : ContDiffAt ℝ (↑⊤) (unitPulse j L n k) x

theorem NavierStokes.ActualSignedDynamics.nativeUnit_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 / (CorrectionInitialization.ActualPrimary.phases B N0 j).L L ∈ Set.Ioo 0 1) : HasDerivAt (fun (t : ℝ) => nativeUnit 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)) (nativeUnit 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))) (nativeUnit j L x)) 0 (((CorrectionInitialization.ActualPrimary.phases B N0 j).frame L).viscosity (CorrectionInitialization.ActualPrimary.phasePoint L x))) x.2.2

Unnormalizing the slot time gives the actual homogeneous projected ODE.

theorem NavierStokes.ActualSignedDynamics.unitPulse_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) (hp : (ActualPrimaryDynamics.copyPoint j L n k x).1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier L) (ht : (ActualPrimaryDynamics.copyPoint j L n k x).2.2 / (CorrectionInitialization.ActualPrimary.phases B N0 j).L L ∈ Set.Ioo 0 1) (hc : (ActualPrimaryDynamics.copyPoint j L n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow L).core) : HarmonicCalculus.along ((PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)).fastField n) (unitPulse 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) (unitMotion j L n k x) (unitPulse j L n k x) ((unitAction j L n k x) (unitPulse 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)

The copied unit satisfies the exact equation used by the signed principal.

theorem NavierStokes.ActualSignedDynamics.unitPulse_action {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) : CurlClassBounds.complexify ((unitAction j L n k x) (unitPulse j L n k x)) = 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) => CurlClassBounds.complexify (unitPulse j L n k y)) x

The action in the unit ODE is exactly the chart's real base shear.

theorem NavierStokes.ActualSignedDynamics.nativeUnit_tangent {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 / (CorrectionInitialization.ActualPrimary.phases B N0 j).L L ∈ Set.Icc 0 1) : inner ℝ ((CorrectionInitialization.ActualPrimary.phases B N0 j).phase.normal L (CorrectionInitialization.ActualPrimary.phasePoint L x)) (nativeUnit j L x) = 0

The native unit is tangent even at the endpoints of its closed time interval.

theorem NavierStokes.ActualSignedDynamics.normal_eq_copy_germ {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 : (ActualPrimaryDynamics.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 =ᶠ[nhds x] fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => ActualPrimaryDynamics.normalScale L n • (CorrectionInitialization.ActualPrimary.phases B N0 j).phase.normal L (CorrectionInitialization.ActualPrimary.phasePoint L (ActualPrimaryDynamics.copyPoint j L n k y))

The actual chart normal agrees with its copied native expression on a neighborhood of every point in the closed clock core. The proof differentiates the padded plateau's phase germ, so the core itself need not be open.

theorem NavierStokes.ActualSignedDynamics.unitPulse_tangent_germ {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) (hp : (ActualPrimaryDynamics.copyPoint j L n k x).1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier L) (ht : (ActualPrimaryDynamics.copyPoint j L n k x).2.2 / (CorrectionInitialization.ActualPrimary.phases B N0 j).L L ∈ Set.Ioo 0 1) (hc : (ActualPrimaryDynamics.copyPoint j L n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow L).core) : (fun (y : CorrectionInitialization.ActualPrimary.FullPoint) => inner ℝ ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).normal (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)) (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)) n y) (unitPulse j L n k y)) =ᶠ[nhds x] fun (x : CorrectionInitialization.ActualPrimary.FullPoint) => 0

True ambient tangency near every admissible closed-core point.

theorem NavierStokes.ActualSignedDynamics.unitPulse_tangent {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) (hp : (ActualPrimaryDynamics.copyPoint j L n k x).1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier L) (ht : (ActualPrimaryDynamics.copyPoint j L n k x).2.2 / (CorrectionInitialization.ActualPrimary.phases B N0 j).L L ∈ Set.Ioo 0 1) (hc : (ActualPrimaryDynamics.copyPoint j L n k x).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow L).core) : inner ℝ ((CorrectionInitialization.ActualPrimary.chartCoefficients j L).normal (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal U)) (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)) n x) (unitPulse j L n k x) = 0