A periodic phase with the actual native clock germs

An explicit compact smooth cutoff has a plateau around the entire native core. Its clock-weighted copies are summed on the common cover. The phase is therefore periodic on the full auxiliary lift and retains the original clock, with every derivative, on each padded wave core.

noncomputable def NavierStokes.PeriodicPhaseAssembly.intervalCutoff (a b d x : ℝ) : ℝ

A concrete smooth interval cutoff. Its plateau includes an extra padding interval on each side of [a,b].

Equations

• NavierStokes.PeriodicPhaseAssembly.intervalCutoff a b d x = ((x - (a - 2 * d)) / d).smoothTransition * ((b + 2 * d - x) / d).smoothTransition

theorem NavierStokes.PeriodicPhaseAssembly.intervalCutoff_contDiff (a b d : ℝ) : ContDiff ℝ (↑⊤) (intervalCutoff a b d)

theorem NavierStokes.PeriodicPhaseAssembly.intervalCutoff_one {a b d x : ℝ} (hd : 0 < d) (ha : a - d ≤ x) (hb : x ≤ b + d) : intervalCutoff a b d x = 1

theorem NavierStokes.PeriodicPhaseAssembly.intervalCutoff_support {a b d : ℝ} (hd : 0 < d) : Function.support (intervalCutoff a b d) ⊆ Set.Icc (a - 2 * d) (b + 2 * d)

structure NavierStokes.PeriodicPhaseAssembly.ClockWindow : Type

Input geometry for the compact clock cutoff. The full sampled native path and all wave cutoff supports are placed inside core.

• lower : TorusInverse.Plane

  Lower of ClockWindow, of type Plane.

• upper : TorusInverse.Plane

  Upper of ClockWindow, of type Plane.

• padding : ℝ

  Padding of ClockWindow, of type ℝ.

• padding_pos : 0 < self.padding

noncomputable def NavierStokes.PeriodicPhaseAssembly.ClockWindow.core (w : ClockWindow) : Set TorusInverse.Plane

Core, given by Icc w.lower.1 w.upper.1 ×ˢ Icc w.lower.2 w.upper.2.

Equations

• w.core = Set.Icc w.lower.1 w.upper.1 ×ˢ Set.Icc w.lower.2 w.upper.2

noncomputable def NavierStokes.PeriodicPhaseAssembly.ClockWindow.plateau (w : ClockWindow) : Set TorusInverse.Plane

Plateau, given by Ioo (w.lower.1 - w.padding) (w.upper.1 + w.padding) ×ˢ Ioo (w.lower.2 - w.padding) (w.upper.2 + w.padding).

Equations

• w.plateau = Set.Ioo (w.lower.1 - w.padding) (w.upper.1 + w.padding) ×ˢ Set.Ioo (w.lower.2 - w.padding) (w.upper.2 + w.padding)

noncomputable def NavierStokes.PeriodicPhaseAssembly.ClockWindow.outer (w : ClockWindow) : Set TorusInverse.Plane

Outer, given by Icc (w.lower.1 - 2 * w.padding) (w.upper.1 + 2 * w.padding) ×ˢ Icc (w.lower.2 - 2 * w.padding) (w.upper.2 + 2 * w.padding).

Equations

• w.outer = Set.Icc (w.lower.1 - 2 * w.padding) (w.upper.1 + 2 * w.padding) ×ˢ Set.Icc (w.lower.2 - 2 * w.padding) (w.upper.2 + 2 * w.padding)

noncomputable def NavierStokes.PeriodicPhaseAssembly.ClockWindow.cutoff (w : ClockWindow) (z : TorusInverse.Plane) : ℝ

Cutoff, given by intervalCutoff w.lower.1 w.upper.1 w.padding z.1 * intervalCutoff w.lower.2 w.upper.2 w.padding z.2.

Equations

• w.cutoff z = NavierStokes.PeriodicPhaseAssembly.intervalCutoff w.lower.1 w.upper.1 w.padding z.1 * NavierStokes.PeriodicPhaseAssembly.intervalCutoff w.lower.2 w.upper.2 w.padding z.2

theorem NavierStokes.PeriodicPhaseAssembly.ClockWindow.core_compact (w : ClockWindow) : IsCompact w.core

theorem NavierStokes.PeriodicPhaseAssembly.ClockWindow.outer_compact (w : ClockWindow) : IsCompact w.outer

theorem NavierStokes.PeriodicPhaseAssembly.ClockWindow.plateau_open (w : ClockWindow) : IsOpen w.plateau

theorem NavierStokes.PeriodicPhaseAssembly.ClockWindow.core_subset_plateau (w : ClockWindow) : w.core ⊆ w.plateau

theorem NavierStokes.PeriodicPhaseAssembly.ClockWindow.plateau_subset_outer (w : ClockWindow) : w.plateau ⊆ w.outer

theorem NavierStokes.PeriodicPhaseAssembly.ClockWindow.core_subset_outer (w : ClockWindow) : w.core ⊆ w.outer

theorem NavierStokes.PeriodicPhaseAssembly.ClockWindow.cutoff_contDiff (w : ClockWindow) : ContDiff ℝ (↑⊤) w.cutoff

theorem NavierStokes.PeriodicPhaseAssembly.ClockWindow.cutoff_support (w : ClockWindow) : Function.support w.cutoff ⊆ w.outer

theorem NavierStokes.PeriodicPhaseAssembly.ClockWindow.cutoff_compact (w : ClockWindow) : HasCompactSupport w.cutoff

theorem NavierStokes.PeriodicPhaseAssembly.ClockWindow.cutoff_one (w : ClockWindow) {z : TorusInverse.Plane} (hz : z ∈ w.plateau) : w.cutoff z = 1

theorem NavierStokes.PeriodicPhaseAssembly.ClockWindow.cutoff_germ (w : ClockWindow) {z : TorusInverse.Plane} (hz : z ∈ w.core) : w.cutoff =ᶠ[nhds z] fun (x : TorusInverse.Plane) => 1

theorem NavierStokes.PeriodicPhaseAssembly.ClockWindow.cutoff_germ_on_support (w : ClockWindow) {E : Type} [Zero E] {κ : TorusInverse.Plane → E} (hκ : tsupport κ ⊆ w.core) {z : TorusInverse.Plane} (hz : z ∈ tsupport κ) : w.cutoff =ᶠ[nhds z] fun (x : TorusInverse.Plane) => 1

noncomputable def NavierStokes.PeriodicPhaseAssembly.periodizeScalar (g : CommonCoverSolve.Geometry) (f : TorusInverse.Plane → ℝ) (Y : TorusInverse.Plane) : ℝ

The literal lattice sum of a native scalar.

Equations

• NavierStokes.PeriodicPhaseAssembly.periodizeScalar g f Y = ∑' (k : NavierStokes.TorusInverse.Frequency), f (g.coordinates k Y)

theorem NavierStokes.PeriodicPhaseAssembly.periodizeScalar_eventually_finite (g : CommonCoverSolve.Geometry) {f : TorusInverse.Plane → ℝ} (hf : HasCompactSupport f) (Y : TorusInverse.Plane) : ∃ (J : Finset TorusInverse.Frequency), periodizeScalar g f =ᶠ[nhds Y] fun (Z : TorusInverse.Plane) => ∑ k ∈ J, f (g.coordinates k Z)

theorem NavierStokes.PeriodicPhaseAssembly.periodizeScalar_contDiff (g : CommonCoverSolve.Geometry) {f : TorusInverse.Plane → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) : ContDiff ℝ (↑⊤) (periodizeScalar g f)

theorem NavierStokes.PeriodicPhaseAssembly.periodizeScalar_periodic (g : CommonCoverSolve.Geometry) (f : TorusInverse.Plane → ℝ) (Y : TorusInverse.Plane) (n : TorusInverse.Frequency) : periodizeScalar g f (Y + TorusAverages.latticePoint n) = periodizeScalar g f Y

theorem NavierStokes.PeriodicPhaseAssembly.periodizeScalar_refine (g : CommonCoverSolve.Geometry) (f : TorusInverse.Plane → ℝ) (d : ℕ) (Y : TorusInverse.Plane) : periodizeScalar (CopySolveCompatibility.refineGeometry g d) f Y = periodizeScalar g f ((CommonCoverSolve.coverPower d) Y)

theorem NavierStokes.PeriodicPhaseAssembly.periodizeScalar_transport (g : CommonCoverSolve.Geometry) (f : TorusInverse.Plane → ℝ) (d : ℕ) (shift rate : ℝ) (hrate : rate ≠ 0) (Y : TorusInverse.Plane) : periodizeScalar (CopySolveCompatibility.transportGeometry g d shift rate hrate) (f ∘ CopySolveCompatibility.nativeTimeMap shift rate) Y = periodizeScalar g f ((CommonCoverSolve.coverPower d) Y)

noncomputable def NavierStokes.PeriodicPhaseAssembly.periodicClock (g : CommonCoverSolve.Geometry) (χ : TorusInverse.Plane → ℝ) : TorusInverse.Plane → ℝ

The clock itself is periodicized together with its cutoff.

Equations

• NavierStokes.PeriodicPhaseAssembly.periodicClock g χ = NavierStokes.PeriodicPhaseAssembly.periodizeScalar g fun (z : NavierStokes.TorusInverse.Plane) => χ z * z.2

theorem NavierStokes.PeriodicPhaseAssembly.periodicClock_contDiff (g : CommonCoverSolve.Geometry) (w : ClockWindow) : ContDiff ℝ (↑⊤) (periodicClock g w.cutoff)

theorem NavierStokes.PeriodicPhaseAssembly.periodicClock_periodic (g : CommonCoverSolve.Geometry) (χ : TorusInverse.Plane → ℝ) (Y : TorusInverse.Plane) (n : TorusInverse.Frequency) : periodicClock g χ (Y + TorusAverages.latticePoint n) = periodicClock g χ Y

theorem NavierStokes.PeriodicPhaseAssembly.periodicClock_refine (g : CommonCoverSolve.Geometry) (χ : TorusInverse.Plane → ℝ) (d : ℕ) (Y : TorusInverse.Plane) : periodicClock (CopySolveCompatibility.refineGeometry g d) χ Y = periodicClock g χ ((CommonCoverSolve.coverPower d) Y)

theorem NavierStokes.PeriodicPhaseAssembly.periodicClock_transport (g : CommonCoverSolve.Geometry) (χ : TorusInverse.Plane → ℝ) (d : ℕ) (shift rate : ℝ) (hrate : rate ≠ 0) (Y : TorusInverse.Plane) : periodizeScalar (CopySolveCompatibility.transportGeometry g d shift rate hrate) (fun (z : TorusInverse.Plane) => χ (CopySolveCompatibility.nativeTimeMap shift rate z) * (shift + rate * z.2)) Y = periodicClock g χ ((CommonCoverSolve.coverPower d) Y)

Clock reparametrization transports the compact native scalar as a whole. The shift is multiplied by the cutoff as well.

theorem NavierStokes.PeriodicPhaseAssembly.periodicClock_germ {P : Type} [NormedAddCommGroup P] (g : CommonCoverSolve.Geometry) (w : ClockWindow) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' w.outer)) (k : TorusInverse.Frequency) {z : P × TorusInverse.Plane} (hz : g.coordinates k z.2 ∈ w.core) : (fun (x : P × TorusInverse.Plane) => periodicClock g w.cutoff x.2) =ᶠ[nhds z] fun (x : P × TorusInverse.Plane) => (g.coordinates k x.2).2

Exact clock agreement on a neighborhood of every closed native core. The geometric input is injectivity of the larger padded support cell.

theorem NavierStokes.PeriodicPhaseAssembly.periodicClock_jets {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CommonCoverSolve.Geometry) (w : ClockWindow) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' w.outer)) (k : TorusInverse.Frequency) {z : P × TorusInverse.Plane} (hz : g.coordinates k z.2 ∈ w.core) (m : ℕ) : iteratedFDeriv ℝ m (fun (x : P × TorusInverse.Plane) => periodicClock g w.cutoff x.2) z = iteratedFDeriv ℝ m (fun (x : P × TorusInverse.Plane) => (g.coordinates k x.2).2) z

theorem NavierStokes.PeriodicPhaseAssembly.periodicClock_path (g : CommonCoverSolve.Geometry) (w : ClockWindow) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' w.outer)) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) (t : ℝ) (htransverse : (g.coordinates k Y).1 ∈ Set.Icc w.lower.1 w.upper.1) (ht : t ∈ Set.Icc w.lower.2 w.upper.2) : periodicClock g w.cutoff (g.path k Y t) = t

The complete earlier-time Volterra path can be kept in the clock plateau. This uses the full sampled interval, including points where the wave cutoff itself vanishes.

Actual phases and complete carriers

noncomputable def NavierStokes.PeriodicPhaseAssembly.phase {P : Type} (g : CommonCoverSolve.Geometry) (χ : TorusInverse.Plane → ℝ) (A B : P → ℝ) (z : P × TorusInverse.Plane) : ℝ

Phase, given by A z.1 - periodicClock g χ z.2 * B z.1.

Equations

• NavierStokes.PeriodicPhaseAssembly.phase g χ A B z = A z.1 - NavierStokes.PeriodicPhaseAssembly.periodicClock g χ z.2 * B z.1

noncomputable def NavierStokes.PeriodicPhaseAssembly.nativePhase {P : Type} (g : CommonCoverSolve.Geometry) (A B : P → ℝ) (k : TorusInverse.Frequency) (z : P × TorusInverse.Plane) : ℝ

Native phase, given by A z.1 - (g.coordinates k z.2).2 * B z.1.

Equations

• NavierStokes.PeriodicPhaseAssembly.nativePhase g A B k z = A z.1 - (g.coordinates k z.2).2 * B z.1

theorem NavierStokes.PeriodicPhaseAssembly.phase_contDiff {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CommonCoverSolve.Geometry) (w : ClockWindow) {A B : P → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hB : ContDiff ℝ (↑⊤) B) : ContDiff ℝ (↑⊤) (phase g w.cutoff A B)

theorem NavierStokes.PeriodicPhaseAssembly.phase_contDiffOn {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CommonCoverSolve.Geometry) (w : ClockWindow) {A B : P → ℝ} {U : Set P} (hA : ContDiffOn ℝ (↑⊤) A U) (hB : ContDiffOn ℝ (↑⊤) B U) : ContDiffOn ℝ (↑⊤) (phase g w.cutoff A B) (U ×ˢ Set.univ)

theorem NavierStokes.PeriodicPhaseAssembly.phase_periodic {P : Type} (g : CommonCoverSolve.Geometry) (χ : TorusInverse.Plane → ℝ) (A B : P → ℝ) (p : P) (Y : TorusInverse.Plane) (n : TorusInverse.Frequency) : phase g χ A B (p, Y + TorusAverages.latticePoint n) = phase g χ A B (p, Y)

theorem NavierStokes.PeriodicPhaseAssembly.phase_germ {P : Type} [NormedAddCommGroup P] (g : CommonCoverSolve.Geometry) (w : ClockWindow) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' w.outer)) (A B : P → ℝ) (k : TorusInverse.Frequency) {z : P × TorusInverse.Plane} (hz : g.coordinates k z.2 ∈ w.core) : phase g w.cutoff A B =ᶠ[nhds z] nativePhase g A B k

theorem NavierStokes.PeriodicPhaseAssembly.phase_jets {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CommonCoverSolve.Geometry) (w : ClockWindow) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' w.outer)) (A B : P → ℝ) (k : TorusInverse.Frequency) {z : P × TorusInverse.Plane} (hz : g.coordinates k z.2 ∈ w.core) (m : ℕ) : iteratedFDeriv ℝ m (phase g w.cutoff A B) z = iteratedFDeriv ℝ m (nativePhase g A B k) z

theorem NavierStokes.PeriodicPhaseAssembly.phase_path {P : Type} (g : CommonCoverSolve.Geometry) (w : ClockWindow) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' w.outer)) (A B : P → ℝ) (k : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (t : ℝ) (htransverse : (g.coordinates k Y).1 ∈ Set.Icc w.lower.1 w.upper.1) (ht : t ∈ Set.Icc w.lower.2 w.upper.2) : phase g w.cutoff A B (p, g.path k Y t) = A p - t * B p

noncomputable def NavierStokes.PeriodicPhaseAssembly.angularLift {P : Type} (Φ : P × TorusInverse.Plane → ℝ) (angular : ℝ) (x : (P × ℝ) × TorusInverse.Plane) : ℝ

The angular coordinate is distinct from the auxiliary torus.

Equations

• NavierStokes.PeriodicPhaseAssembly.angularLift Φ angular x = Φ (x.1.1, x.2) + angular * x.1.2

theorem NavierStokes.PeriodicPhaseAssembly.angularLift_contDiff {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {Φ : P × TorusInverse.Plane → ℝ} (hΦ : ContDiff ℝ (↑⊤) Φ) (angular : ℝ) : ContDiff ℝ (↑⊤) (angularLift Φ angular)

theorem NavierStokes.PeriodicPhaseAssembly.angularLift_affine {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (Φ : P × TorusInverse.Plane → ℝ) (angular : ℝ) : CopyAngularInvariance.AffinePhase ((0, 1), 0) angular (angularLift Φ angular)

theorem NavierStokes.PeriodicPhaseAssembly.angularLift_germ {P : Type} [NormedAddCommGroup P] {Φ Ψ : P × TorusInverse.Plane → ℝ} (angular : ℝ) {x : (P × ℝ) × TorusInverse.Plane} (hΦ : Φ =ᶠ[nhds (x.1.1, x.2)] Ψ) : angularLift Φ angular =ᶠ[nhds x] angularLift Ψ angular

theorem NavierStokes.PeriodicPhaseAssembly.fullPhase_germ {P : Type} [NormedAddCommGroup P] (g : CommonCoverSolve.Geometry) (w : ClockWindow) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' w.outer)) (A B : P → ℝ) (angular : ℝ) (k : TorusInverse.Frequency) {x : (P × ℝ) × TorusInverse.Plane} (hx : g.coordinates k x.2 ∈ w.core) : angularLift (phase g w.cutoff A B) angular =ᶠ[nhds x] angularLift (nativePhase g A B k) angular

theorem NavierStokes.PeriodicPhaseAssembly.fullPhase_jets {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CommonCoverSolve.Geometry) (w : ClockWindow) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' w.outer)) (A B : P → ℝ) (angular : ℝ) (k : TorusInverse.Frequency) {x : (P × ℝ) × TorusInverse.Plane} (hx : g.coordinates k x.2 ∈ w.core) (m : ℕ) : iteratedFDeriv ℝ m (angularLift (phase g w.cutoff A B) angular) x = iteratedFDeriv ℝ m (angularLift (nativePhase g A B k) angular) x

theorem NavierStokes.PeriodicPhaseAssembly.fullPhase_periodic {P : Type} (g : CommonCoverSolve.Geometry) (χ : TorusInverse.Plane → ℝ) (A B : P → ℝ) (angular : ℝ) (p : P) (θ : ℝ) (Y : TorusInverse.Plane) (n : TorusInverse.Frequency) : angularLift (phase g χ A B) angular ((p, θ), Y + TorusAverages.latticePoint n) = angularLift (phase g χ A B) angular ((p, θ), Y)

theorem NavierStokes.PeriodicPhaseAssembly.carrier_periodic {P : Type} (g : CommonCoverSolve.Geometry) (χ : TorusInverse.Plane → ℝ) (A B : P → ℝ) (angular K : ℝ) (p : P) (θ : ℝ) (Y : TorusInverse.Plane) (n : TorusInverse.Frequency) : HarmonicCalculus.carrier K (angularLift (phase g χ A B) angular) ((p, θ), Y + TorusAverages.latticePoint n) = HarmonicCalculus.carrier K (angularLift (phase g χ A B) angular) ((p, θ), Y)

theorem NavierStokes.PeriodicPhaseAssembly.fullMode_periodic {P : Type} (g : CommonCoverSolve.Geometry) (χ : TorusInverse.Plane → ℝ) (A B : P → ℝ) (angular K : ℝ) (a : (P × ℝ) × TorusInverse.Plane → ℂ) (ha : ∀ (p : P) (θ : ℝ) (Y : TorusInverse.Plane) (n : TorusInverse.Frequency), a ((p, θ), Y + TorusAverages.latticePoint n) = a ((p, θ), Y)) (p : P) (θ : ℝ) (Y : TorusInverse.Plane) (n : TorusInverse.Frequency) : HarmonicCalculus.mode K (angularLift (phase g χ A B) angular) a ((p, θ), Y + TorusAverages.latticePoint n) = HarmonicCalculus.mode K (angularLift (phase g χ A B) angular) a ((p, θ), Y)

theorem NavierStokes.PeriodicPhaseAssembly.carrier_angularLift_eq_character {P : Type} (Φ : P × TorusInverse.Plane → ℝ) {K : ℝ} (hK : K ≠ 0) (m j : ℤ) (x : (P × ℝ) × TorusInverse.Plane) : HarmonicCalculus.carrier (↑j * K) (angularLift Φ (↑m / K)) x = HarmonicFields.character j (K * Φ (x.1.1, x.2) + ↑m * x.1.2)

theorem NavierStokes.PeriodicPhaseAssembly.carrier_angular_periodic {P : Type} (Φ : P × TorusInverse.Plane → ℝ) {K : ℝ} (hK : K ≠ 0) (m j : ℤ) (p : P) (Y : TorusInverse.Plane) (θ : ℝ) : HarmonicCalculus.carrier (↑j * K) (angularLift Φ (↑m / K)) ((p, θ + 2 * Real.pi), Y) = HarmonicCalculus.carrier (↑j * K) (angularLift Φ (↑m / K)) ((p, θ), Y)

The integer angular character is retained by the actual global carrier.

The manuscript phase in physical slow-coordinate order (R,(T,Z))

@[reducible, inline]

abbrev NavierStokes.PeriodicPhaseAssembly.Parameter : Type

Parameter: an abbreviation for PhysicalParticularWave.Parameter.

Equations

• NavierStokes.PeriodicPhaseAssembly.Parameter = NavierStokes.PhysicalParticularWave.Parameter

noncomputable def NavierStokes.PeriodicPhaseAssembly.slowSwap (p : Parameter) : PhaseCalculus.Slow

Slow swap, given by (p.1, (p.2.2, p.2.1)).

Equations

• NavierStokes.PeriodicPhaseAssembly.slowSwap p = (p.1, p.2.2, p.2.1)

noncomputable def NavierStokes.PeriodicPhaseAssembly.profileIntercept (ε pz x0 : ℝ) (s : Parameter) : ℝ

Profile intercept, given by (pz / ε) * s.2.2 + x0 * s.1.

Equations

• NavierStokes.PeriodicPhaseAssembly.profileIntercept ε pz x0 s = pz / ε * s.2.2 + x0 * s.1

noncomputable def NavierStokes.PeriodicPhaseAssembly.profileRate (p pz : ℝ) (F G : Parameter → ℝ) (s : Parameter) : ℝ

Profile rate, given by p * F s + pz * G s.

Equations

• NavierStokes.PeriodicPhaseAssembly.profileRate p pz F G s = p * F s + pz * G s

noncomputable def NavierStokes.PeriodicPhaseAssembly.profilePhase (g : CommonCoverSolve.Geometry) (χ : TorusInverse.Plane → ℝ) (ε p pz x0 : ℝ) (F G : Parameter → ℝ) : Parameter × TorusInverse.Plane → ℝ

Profile phase, given by phase g χ (profileIntercept ε pz x0) (profileRate p pz F G).

Equations

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

theorem NavierStokes.PeriodicPhaseAssembly.profilePhase_eq_literal (g : CommonCoverSolve.Geometry) (χ : TorusInverse.Plane → ℝ) (ε p pz x0 : ℝ) (F G : Parameter → ℝ) (x : (Parameter × ℝ) × TorusInverse.Plane) : angularLift (profilePhase g χ ε p pz x0 F G) p x = PhaseCalculus.phase ε p pz x0 (fun (s : PhaseCalculus.Slow) => F (s.1, s.2.2, s.2.1)) (fun (s : PhaseCalculus.Slow) => G (s.1, s.2.2, s.2.1)) (slowSwap x.1.1, x.1.2, periodicClock g χ x.2)

theorem NavierStokes.PeriodicPhaseAssembly.profilePhase_germ (g : CommonCoverSolve.Geometry) (w : ClockWindow) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' w.outer)) (ε p pz x0 : ℝ) (F G : Parameter → ℝ) (k : TorusInverse.Frequency) {x : (Parameter × ℝ) × TorusInverse.Plane} (hx : g.coordinates k x.2 ∈ w.core) : angularLift (profilePhase g w.cutoff ε p pz x0 F G) p =ᶠ[nhds x] fun (y : (Parameter × ℝ) × TorusInverse.Plane) => PhaseCalculus.phase ε p pz x0 (fun (s : PhaseCalculus.Slow) => F (s.1, s.2.2, s.2.1)) (fun (s : PhaseCalculus.Slow) => G (s.1, s.2.2, s.2.1)) (slowSwap y.1.1, y.1.2, (g.coordinates k y.2).2)

theorem NavierStokes.PeriodicPhaseAssembly.profilePhase_jets (g : CommonCoverSolve.Geometry) (w : ClockWindow) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' w.outer)) (ε p pz x0 : ℝ) (F G : Parameter → ℝ) (k : TorusInverse.Frequency) {x : (Parameter × ℝ) × TorusInverse.Plane} (hx : g.coordinates k x.2 ∈ w.core) (m : ℕ) : iteratedFDeriv ℝ m (angularLift (profilePhase g w.cutoff ε p pz x0 F G) p) x = iteratedFDeriv ℝ m (fun (y : (Parameter × ℝ) × TorusInverse.Plane) => PhaseCalculus.phase ε p pz x0 (fun (s : PhaseCalculus.Slow) => F (s.1, s.2.2, s.2.1)) (fun (s : PhaseCalculus.Slow) => G (s.1, s.2.2, s.2.1)) (slowSwap y.1.1, y.1.2, (g.coordinates k y.2).2)) x

One reference phase under actual clock and common-cover changes

theorem NavierStokes.PeriodicPhaseAssembly.periodicClock_scale_transport (g : CommonCoverSolve.Geometry) (χ : TorusInverse.Plane → ℝ) (d : ℕ) (rate : ℝ) (hrate : rate ≠ 0) (Y : TorusInverse.Plane) : rate * periodicClock (CopySolveCompatibility.transportGeometry g d 0 rate hrate) (χ ∘ CopySolveCompatibility.nativeTimeMap 0 rate) Y = periodicClock g χ ((CommonCoverSolve.coverPower d) Y)

noncomputable def NavierStokes.PeriodicPhaseAssembly.transportPhase {P Q : Type} (Φ : P × TorusInverse.Plane → ℝ) (φ : Q → P) (gap : ℕ) (K Kr : ℝ) (z : Q × TorusInverse.Plane) : ℝ

Each target band is a view of one fixed reference phase.

Equations

• NavierStokes.PeriodicPhaseAssembly.transportPhase Φ φ gap K Kr z = Kr / K * Φ (φ z.1, (NavierStokes.CommonCoverSolve.coverPower gap) z.2)

theorem NavierStokes.PeriodicPhaseAssembly.transportPhase_weighted {P Q : Type} (Φ : P × TorusInverse.Plane → ℝ) (φ : Q → P) (gap : ℕ) {K : ℝ} (hK : K ≠ 0) (Kr : ℝ) (z : Q × TorusInverse.Plane) : K * transportPhase Φ φ gap K Kr z = Kr * Φ (φ z.1, (CommonCoverSolve.coverPower gap) z.2)

theorem NavierStokes.PeriodicPhaseAssembly.transportPhase_contDiff {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Q] [NormedSpace ℝ Q] {Φ : P × TorusInverse.Plane → ℝ} {φ : Q → P} (hΦ : ContDiff ℝ (↑⊤) Φ) (hφ : ContDiff ℝ (↑⊤) φ) (gap : ℕ) (K Kr : ℝ) : ContDiff ℝ (↑⊤) (transportPhase Φ φ gap K Kr)

theorem NavierStokes.PeriodicPhaseAssembly.transportPhase_periodic {P Q : Type} {Φ : P × TorusInverse.Plane → ℝ} (hΦ : ∀ (p : P) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency), Φ (p, Y + TorusAverages.latticePoint k) = Φ (p, Y)) (φ : Q → P) (gap : ℕ) (K Kr : ℝ) (p : Q) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency) : transportPhase Φ φ gap K Kr (p, Y + TorusAverages.latticePoint k) = transportPhase Φ φ gap K Kr (p, Y)

theorem NavierStokes.PeriodicPhaseAssembly.transportPhase_eq_refined {P Q : Type} (g : CommonCoverSolve.Geometry) (χ : TorusInverse.Plane → ℝ) (A B : P → ℝ) (φ : Q → P) (gap : ℕ) (K Kr : ℝ) : transportPhase (phase g χ A B) φ gap K Kr = phase (CopySolveCompatibility.refineGeometry g gap) χ (fun (p : Q) => Kr / K * A (φ p)) fun (p : Q) => Kr / K * B (φ p)

Equality of the constructed fields, including off the native support.

theorem NavierStokes.PeriodicPhaseAssembly.transportPhase_eq_scaled_clock {P Q : Type} (g : CommonCoverSolve.Geometry) (χ : TorusInverse.Plane → ℝ) (A B : P → ℝ) (φ : Q → P) (gap : ℕ) (K Kr rate : ℝ) (hrate : rate ≠ 0) : transportPhase (phase g χ A B) φ gap K Kr = phase (CopySolveCompatibility.transportGeometry g gap 0 rate hrate) (χ ∘ CopySolveCompatibility.nativeTimeMap 0 rate) (fun (p : Q) => Kr / K * A (φ p)) fun (p : Q) => Kr / K * rate * B (φ p)

The actual physical clock rate and its rescaled cutoff give the same global target phase as the weighted reference pullback.

theorem NavierStokes.PeriodicPhaseAssembly.transportPhase_native_germ {P Q : Type} [NormedAddCommGroup P] [NormedAddCommGroup Q] (g : CommonCoverSolve.Geometry) (w : ClockWindow) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' w.outer)) (A B : P → ℝ) (φ : Q → P) (gap : ℕ) (K Kr shift rate : ℝ) (hrate : rate ≠ 0) (copy : TorusInverse.Frequency) {z : Q × TorusInverse.Plane} (hφ : ContinuousAt φ z.1) (hz : CopySolveCompatibility.nativeTimeMap shift rate ((CopySolveCompatibility.transportGeometry g gap shift rate hrate).coordinates copy z.2) ∈ w.core) : transportPhase (phase g w.cutoff A B) φ gap K Kr =ᶠ[nhds z] nativePhase (CopySolveCompatibility.transportGeometry g gap shift rate hrate) (fun (p : Q) => Kr / K * (A (φ p) - shift * B (φ p))) (fun (p : Q) => Kr / K * rate * B (φ p)) copy

The full native phase, with its original anchor, agrees as a germ on every transformed cell. Only continuity of the parameter change is needed to transport the germ.

theorem NavierStokes.PeriodicPhaseAssembly.transportPhase_native_jets {P Q : Type} [NormedAddCommGroup P] [NormedAddCommGroup Q] [NormedSpace ℝ Q] (g : CommonCoverSolve.Geometry) (w : ClockWindow) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' w.outer)) (A B : P → ℝ) (φ : Q → P) (gap : ℕ) (K Kr shift rate : ℝ) (hrate : rate ≠ 0) (copy : TorusInverse.Frequency) {z : Q × TorusInverse.Plane} (hφ : ContinuousAt φ z.1) (hz : CopySolveCompatibility.nativeTimeMap shift rate ((CopySolveCompatibility.transportGeometry g gap shift rate hrate).coordinates copy z.2) ∈ w.core) (m : ℕ) : iteratedFDeriv ℝ m (transportPhase (phase g w.cutoff A B) φ gap K Kr) z = iteratedFDeriv ℝ m (nativePhase (CopySolveCompatibility.transportGeometry g gap shift rate hrate) (fun (p : Q) => Kr / K * (A (φ p) - shift * B (φ p))) (fun (p : Q) => Kr / K * rate * B (φ p)) copy) z

theorem NavierStokes.PeriodicPhaseAssembly.transportPhase_angular_weighted {P Q : Type} (Φ : P × TorusInverse.Plane → ℝ) (φ : Q → P) (gap : ℕ) {K Kr : ℝ} (hK : K ≠ 0) (hKr : Kr ≠ 0) (m : ℤ) (x : (Q × ℝ) × TorusInverse.Plane) : K * angularLift (transportPhase Φ φ gap K Kr) (↑m / K) x = Kr * angularLift Φ (↑m / Kr) ((φ x.1.1, x.1.2), (CommonCoverSolve.coverPower gap) x.2)

theorem NavierStokes.PeriodicPhaseAssembly.parameterChange_self {Q : ℝ} (hQ : 0 < Q) (h : ℝ) : PhysicalParticularWave.parameterChange h Q Q = id

noncomputable def NavierStokes.PeriodicPhaseAssembly.physicalBlock (b : CorrectionState.HarmonicBlock (Parameter × TorusInverse.Plane)) (h : ℝ) (Q : ℕ → ℝ) (gap : ℕ → ℕ) (reference : ℕ) (angular : ℤ) (g : CommonCoverSolve.Geometry) (w : ClockWindow) (A B : Parameter → ℝ) : CorrectionState.HarmonicBlock (Parameter × TorusInverse.Plane)

A literal harmonic block with one reference phase and one angular integer. Its amplitudes and pressure coefficients are supplied by the existing block; its phase is the constructed common-cover view.

Equations

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

theorem NavierStokes.PeriodicPhaseAssembly.physicalBlock_reference (b : CorrectionState.HarmonicBlock (Parameter × TorusInverse.Plane)) (h : ℝ) (Q : ℕ → ℝ) (gap : ℕ → ℕ) (reference : ℕ) (angular : ℤ) (g : CommonCoverSolve.Geometry) (w : ClockWindow) (A B : Parameter → ℝ) (hQ : 0 < Q reference) (hgap : gap reference = 0) (hK : b.frequency reference ≠ 0) : (physicalBlock b h Q gap reference angular g w A B).phase reference = phase g w.cutoff A B

theorem NavierStokes.PeriodicPhaseAssembly.physicalBlock_weighted (b : CorrectionState.HarmonicBlock (Parameter × TorusInverse.Plane)) (h : ℝ) (Q : ℕ → ℝ) (gap : ℕ → ℕ) (reference : ℕ) (angular : ℤ) (g : CommonCoverSolve.Geometry) (w : ClockWindow) (A B : Parameter → ℝ) (hQ : 0 < Q reference) (hgap : gap reference = 0) (hK : ∀ (n : ℕ), b.frequency n ≠ 0) (n : ℕ) (p : Parameter) (Y : TorusInverse.Plane) : (physicalBlock b h Q gap reference angular g w A B).frequency n * (physicalBlock b h Q gap reference angular g w A B).phase n (p, Y) = (physicalBlock b h Q gap reference angular g w A B).frequency reference * (physicalBlock b h Q gap reference angular g w A B).phase reference (PhysicalParticularWave.parameterChange h (Q n) (Q reference) p, (CommonCoverSolve.coverPower (gap n)) Y)

theorem NavierStokes.PeriodicPhaseAssembly.physicalBlock_periodic (b : CorrectionState.HarmonicBlock (Parameter × TorusInverse.Plane)) (h : ℝ) (Q : ℕ → ℝ) (gap : ℕ → ℕ) (reference : ℕ) (angular : ℤ) (g : CommonCoverSolve.Geometry) (w : ClockWindow) (A B : Parameter → ℝ) (n : ℕ) (p : Parameter) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency) : (physicalBlock b h Q gap reference angular g w A B).phase n (p, Y + TorusAverages.latticePoint k) = (physicalBlock b h Q gap reference angular g w A B).phase n (p, Y)

theorem NavierStokes.PeriodicPhaseAssembly.physicalBlock_contDiff (b : CorrectionState.HarmonicBlock (Parameter × TorusInverse.Plane)) (h : ℝ) (Q : ℕ → ℝ) (gap : ℕ → ℕ) (reference : ℕ) (angular : ℤ) (g : CommonCoverSolve.Geometry) (w : ClockWindow) {A B : Parameter → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hB : ContDiff ℝ (↑⊤) B) (n : ℕ) : ContDiff ℝ (↑⊤) ((physicalBlock b h Q gap reference angular g w A B).phase n)

theorem NavierStokes.PeriodicPhaseAssembly.physicalBlock_eq_scaled_clock (b : CorrectionState.HarmonicBlock (Parameter × TorusInverse.Plane)) (h : ℝ) (Q : ℕ → ℝ) (gap : ℕ → ℕ) (reference : ℕ) (angular : ℤ) (g : CommonCoverSolve.Geometry) (w : ClockWindow) (A B : Parameter → ℝ) (n : ℕ) (hQn : 0 < Q n) (hQr : 0 < Q reference) : (physicalBlock b h Q gap reference angular g w A B).phase n = phase (CopySolveCompatibility.transportGeometry g (gap n) 0 (PhysicalParticularWave.clockWeight h (Q n) (Q reference)) ⋯) (w.cutoff ∘ CopySolveCompatibility.nativeTimeMap 0 (PhysicalParticularWave.clockWeight h (Q n) (Q reference))) (fun (p : PhysicalParticularWave.Parameter) => b.frequency reference / b.frequency n * A (PhysicalParticularWave.parameterChange h (Q n) (Q reference) p)) fun (p : PhysicalParticularWave.Parameter) => b.frequency reference / b.frequency n * PhysicalParticularWave.clockWeight h (Q n) (Q reference) * B (PhysicalParticularWave.parameterChange h (Q n) (Q reference) p)

The exact PPW clock, with its cutoff transformed by the same rate.

noncomputable def NavierStokes.PeriodicPhaseAssembly.periodicAssembly (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) (Q : ℕ → ℝ) (gap : ℕ → ℕ) (angular : ℤ) (w : ClockWindow) (A B : Parameter → ℝ) : ParticularWaveAssembly.AssemblyData Parameter

Assign the constructed phase family to the literal assembly record.

Equations

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

theorem NavierStokes.PeriodicPhaseAssembly.bandPhase_eq_actualCarrier (D : ParticularWaveAssembly.AssemblyData Parameter) (h : ℝ) (Q : ℕ → ℝ) (gap : ℕ → ℕ) (angular : ℤ) (w : ClockWindow) (A B : Parameter → ℝ) (hQ : 0 < Q D.reference.band) (hgap : gap D.reference.band = 0) (hK : ∀ (n : ℕ), D.carrierBlock.frequency n ≠ 0) (n : ℕ) (j : ℤ) (hj : j ≠ 0) : PhysicalParticularWave.bandPhase (periodicAssembly D h Q gap angular w A B) h (Q n) (Q D.reference.band) (gap n) (↑j * D.carrierBlock.frequency n) j = fun (x : PhysicalParticularWave.Cylinder) => (ParticularWaveAssembly.actualCarrier D.background (periodicAssembly D h Q gap angular w A B).carrierBlock j).phase n (PhysicalParticularWave.waveEquiv x)

Native support geometry and direct carrier adapters

theorem NavierStokes.PeriodicPhaseAssembly.transportGeometry_affine (g : CommonCoverSolve.Geometry) (gap : ℕ) (shift rate : ℝ) (hrate : rate ≠ 0) (z : TorusInverse.Plane) : (CopySolveCompatibility.transportGeometry g gap shift rate hrate).center + (CopySolveCompatibility.transportGeometry g gap shift rate hrate).basis z = g.center + g.basis (CopySolveCompatibility.nativeTimeMap shift rate z)

theorem NavierStokes.PeriodicPhaseAssembly.transportGeometry_injective (g : CommonCoverSolve.Geometry) (gap : ℕ) (shift rate : ℝ) (hrate : rate ≠ 0) {K : Set TorusInverse.Plane} (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' K)) : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (CopySolveCompatibility.transportGeometry g gap shift rate hrate).center + (CopySolveCompatibility.transportGeometry g gap shift rate hrate).basis z) '' CopySolveCompatibility.nativeTimeMap shift rate ⁻¹' K)

theorem NavierStokes.PeriodicPhaseAssembly.transportPhase_contDiffOn {P Q : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Q] [NormedSpace ℝ Q] {Φ : P × TorusInverse.Plane → ℝ} {φ : Q → P} {U : Set P} {V : Set Q} (hΦ : ContDiffOn ℝ (↑⊤) Φ (U ×ˢ Set.univ)) (hφ : ContDiffOn ℝ (↑⊤) φ V) (hmap : Set.MapsTo φ V U) (gap : ℕ) (K Kr : ℝ) : ContDiffOn ℝ (↑⊤) (transportPhase Φ φ gap K Kr) (V ×ˢ Set.univ)

theorem NavierStokes.PeriodicPhaseAssembly.transportPhase_path {P Q : Type} [NormedAddCommGroup P] [NormedAddCommGroup Q] (g : CommonCoverSolve.Geometry) (w : ClockWindow) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' w.outer)) (A B : P → ℝ) (φ : Q → P) (gap : ℕ) (K Kr shift rate : ℝ) (hrate : rate ≠ 0) (copy : TorusInverse.Frequency) (p : Q) (hφ : ContinuousAt φ p) (Y : TorusInverse.Plane) (t : ℝ) (htransverse : ((CopySolveCompatibility.transportGeometry g gap shift rate hrate).coordinates copy Y).1 ∈ Set.Icc w.lower.1 w.upper.1) (ht : shift + rate * t ∈ Set.Icc w.lower.2 w.upper.2) : transportPhase (phase g w.cutoff A B) φ gap K Kr (p, (CopySolveCompatibility.transportGeometry g gap shift rate hrate).path copy Y t) = Kr / K * (A (φ p) - (shift + rate * t) * B (φ p))

Exact values on the entire transformed sampling interval, with the original reference anchor shift + rate*t.

theorem NavierStokes.PeriodicPhaseAssembly.latticePeriodic_jets {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : P × TorusInverse.Plane → E} (hf : ∀ (p : P) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency), f (p, Y + TorusAverages.latticePoint k) = f (p, Y)) (m : ℕ) (p : P) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency) : iteratedFDeriv ℝ m f (p, Y + TorusAverages.latticePoint k) = iteratedFDeriv ℝ m f (p, Y)

Periodicity of all joint derivative tensors follows from the proved function identity under the constant lattice translation.

theorem NavierStokes.PeriodicPhaseAssembly.carrier_germ {P : Type} [NormedAddCommGroup P] {Φ Ψ : P → ℝ} {x : P} (hΦ : Φ =ᶠ[nhds x] Ψ) (K : ℝ) : HarmonicCalculus.carrier K Φ =ᶠ[nhds x] HarmonicCalculus.carrier K Ψ

theorem NavierStokes.PeriodicPhaseAssembly.fullMode_germ {P : Type} [NormedAddCommGroup P] {Φ Ψ : P → ℝ} {x : P} (hΦ : Φ =ᶠ[nhds x] Ψ) (K : ℝ) (a : P → ℂ) : HarmonicCalculus.mode K Φ a =ᶠ[nhds x] HarmonicCalculus.mode K Ψ a

theorem NavierStokes.PeriodicPhaseAssembly.carrier_jets_of_phase_germ {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {Φ Ψ : P → ℝ} {x : P} (hΦ : Φ =ᶠ[nhds x] Ψ) (K : ℝ) (m : ℕ) : iteratedFDeriv ℝ m (HarmonicCalculus.carrier K Φ) x = iteratedFDeriv ℝ m (HarmonicCalculus.carrier K Ψ) x

theorem NavierStokes.PeriodicPhaseAssembly.fullMode_jets_of_phase_germ {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {Φ Ψ : P → ℝ} {x : P} (hΦ : Φ =ᶠ[nhds x] Ψ) (K : ℝ) (a : P → ℂ) (m : ℕ) : iteratedFDeriv ℝ m (HarmonicCalculus.mode K Φ a) x = iteratedFDeriv ℝ m (HarmonicCalculus.mode K Ψ a) x

theorem NavierStokes.PeriodicPhaseAssembly.actualCarrier_phase_germ {P : Type} [NormedAddCommGroup P] (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (j : ℤ) (n : ℕ) {Φ : P × TorusInverse.Plane → ℝ} {x : (P × ℝ) × TorusInverse.Plane} (hΦ : b.phase n =ᶠ[nhds (x.1.1, x.2)] Φ) : (ParticularWaveAssembly.actualCarrier base b j).phase n =ᶠ[nhds x] angularLift Φ (↑(b.angularFrequency n) / b.frequency n)

theorem NavierStokes.PeriodicPhaseAssembly.actualCarrier_periodic {P : Type} (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (j : ℤ) (n : ℕ) (hΦ : ∀ (p : P) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency), b.phase n (p, Y + TorusAverages.latticePoint k) = b.phase n (p, Y)) (p : P) (θ : ℝ) (Y : TorusInverse.Plane) (k : TorusInverse.Frequency) : (ParticularWaveAssembly.actualCarrier base b j).phase n ((p, θ), Y + TorusAverages.latticePoint k) = (ParticularWaveAssembly.actualCarrier base b j).phase n ((p, θ), Y) ∧ HarmonicCalculus.carrier ((ParticularWaveAssembly.actualCarrier base b j).frequency n) ((ParticularWaveAssembly.actualCarrier base b j).phase n) ((p, θ), Y + TorusAverages.latticePoint k) = HarmonicCalculus.carrier ((ParticularWaveAssembly.actualCarrier base b j).frequency n) ((ParticularWaveAssembly.actualCarrier base b j).phase n) ((p, θ), Y)

theorem NavierStokes.PeriodicPhaseAssembly.actualCarrier_angular_periodic {P : Type} (base : LinearWaveBounds.WaveCoefficients ((P × ℝ) × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (j : ℤ) (n : ℕ) (hK : b.frequency n ≠ 0) (p : P) (θ : ℝ) (Y : TorusInverse.Plane) : HarmonicCalculus.carrier ((ParticularWaveAssembly.actualCarrier base b j).frequency n) ((ParticularWaveAssembly.actualCarrier base b j).phase n) ((p, θ + 2 * Real.pi), Y) = HarmonicCalculus.carrier ((ParticularWaveAssembly.actualCarrier base b j).frequency n) ((ParticularWaveAssembly.actualCarrier base b j).phase n) ((p, θ), Y)

theorem NavierStokes.PeriodicPhaseAssembly.physicalBlock_native_germ (b : CorrectionState.HarmonicBlock (Parameter × TorusInverse.Plane)) (h : ℝ) (Q : ℕ → ℝ) (gap : ℕ → ℕ) (reference : ℕ) (angular : ℤ) (g : CommonCoverSolve.Geometry) (w : ClockWindow) (A B : Parameter → ℝ) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => g.center + g.basis z) '' w.outer)) (n : ℕ) (shift rate : ℝ) (hrate : rate ≠ 0) (copy : TorusInverse.Frequency) {z : Parameter × TorusInverse.Plane} (hz : CopySolveCompatibility.nativeTimeMap shift rate ((CopySolveCompatibility.transportGeometry g (gap n) shift rate hrate).coordinates copy z.2) ∈ w.core) : (physicalBlock b h Q gap reference angular g w A B).phase n =ᶠ[nhds z] nativePhase (CopySolveCompatibility.transportGeometry g (gap n) shift rate hrate) (fun (p : Parameter) => b.frequency reference / b.frequency n * (A (PhysicalParticularWave.parameterChange h (Q n) (Q reference) p) - shift * B (PhysicalParticularWave.parameterChange h (Q n) (Q reference) p))) (fun (p : Parameter) => b.frequency reference / b.frequency n * rate * B (PhysicalParticularWave.parameterChange h (Q n) (Q reference) p)) copy

theorem NavierStokes.PeriodicPhaseAssembly.physicalBlock_carrier_natural (base : LinearWaveBounds.WaveCoefficients ((Parameter × ℝ) × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (Parameter × TorusInverse.Plane)) (h : ℝ) (Q : ℕ → ℝ) (gap : ℕ → ℕ) (reference : ℕ) (angular : ℤ) (g : CommonCoverSolve.Geometry) (w : ClockWindow) (A B : Parameter → ℝ) (hQ : 0 < Q reference) (hgap : gap reference = 0) (hK : ∀ (n : ℕ), b.frequency n ≠ 0) (j : ℤ) (n : ℕ) (p : Parameter) (θ : ℝ) (Y : TorusInverse.Plane) : HarmonicCalculus.carrier (↑j * b.frequency n) ((ParticularWaveAssembly.actualCarrier base (physicalBlock b h Q gap reference angular g w A B) j).phase n) ((p, θ), Y) = HarmonicCalculus.carrier (↑j * b.frequency reference) ((ParticularWaveAssembly.actualCarrier base (physicalBlock b h Q gap reference angular g w A B) j).phase reference) ((PhysicalParticularWave.parameterChange h (Q n) (Q reference) p, θ), (CommonCoverSolve.coverPower (gap n)) Y)

Exact naturality of the complete carrier, including its unchanged integer angular character, on the free lift.