Actual native-copy realization of the signed reference wave

The primary pulse and signed quotient are fixed. A periodic reference coordinate and mask are constructed from the native layout. The native copies are summed before curl, and equality with the same reference output is proved from the periodic-clock identity on their compact supports.

@[reducible, inline]

abbrev NavierStokes.ActualPeriodizedSignedRealization.Cylinder : Type

Cylinder: an abbreviation for PhysicalResidualBridge.Cylinder.

Equations

• NavierStokes.ActualPeriodizedSignedRealization.Cylinder = NavierStokes.PhysicalResidualBridge.Cylinder

@[reducible, inline]

abbrev NavierStokes.ActualPeriodizedSignedRealization.Plane : Type

Plane: an abbreviation for TorusInverse.Plane.

Equations

• NavierStokes.ActualPeriodizedSignedRealization.Plane = NavierStokes.TorusInverse.Plane

@[reducible, inline]

abbrev NavierStokes.ActualPeriodizedSignedRealization.Frequency : Type

Frequency: an abbreviation for TorusInverse.Frequency.

Equations

• NavierStokes.ActualPeriodizedSignedRealization.Frequency = NavierStokes.TorusInverse.Frequency

@[reducible, inline]

abbrev NavierStokes.ActualPeriodizedSignedRealization.Space : Type

Space: an abbreviation for ProblemStatement.Space.

Equations

• NavierStokes.ActualPeriodizedSignedRealization.Space = NavierStokes.ProblemStatement.Space

@[reducible, inline]

abbrev NavierStokes.ActualPeriodizedSignedRealization.Mat2 : Type

Mat2: an abbreviation for SmoothCovariance.Mat2.

Equations

• NavierStokes.ActualPeriodizedSignedRealization.Mat2 = NavierStokes.SmoothCovariance.Mat2

@[reducible, inline]

abbrev NavierStokes.ActualPeriodizedSignedRealization.Vec2 : Type

Vec2: an abbreviation for SmoothCovariance.Vec2.

Equations

• NavierStokes.ActualPeriodizedSignedRealization.Vec2 = NavierStokes.SmoothCovariance.Vec2

structure NavierStokes.ActualPeriodizedSignedRealization.Layout : Type

Primitive native geometry and its actual compact mask. No summed coefficient or solved-wave identity is a field of this record.

• geometry : ℕ → CommonCoverSolve.Geometry

  Geometry of Layout, of type ℕ → CommonCoverSolve.Geometry.

• window : ℕ → PeriodicPhaseAssembly.ClockWindow

  Window of Layout, of type ℕ → PeriodicPhaseAssembly.ClockWindow.

• length : ℕ → ℝ

  Length of Layout, of type ℕ → ℝ.

• length_pos (n : ℕ) : 0 < self.length n
• cutoff : ℕ → Plane → ℝ

  Cutoff of Layout, of type ℕ → Plane → ℝ.

• cutoff_smooth (n : ℕ) : ContDiff ℝ (↑⊤) (self.cutoff n)
• cutoff_support (n : ℕ) : Function.support (self.cutoff n) ⊆ (self.window n).core
• injective (n : ℕ) : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => (self.geometry n).center + (self.geometry n).basis z) '' (self.window n).outer)

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.Layout.nativeMask (l : Layout) (n : ℕ) (k : Frequency) (Y : Plane) : ℝ

Native mask, given by l.cutoff n ((l.geometry n).coordinates k Y).

Equations

• l.nativeMask n k Y = l.cutoff n ((l.geometry n).coordinates k Y)

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.Layout.mask (l : Layout) (n : ℕ) (Y : Plane) : ℝ

Mask, given by ∑' k, l.nativeMask n k Y.

Equations

• l.mask n Y = ∑' (k : NavierStokes.ActualPeriodizedSignedRealization.Frequency), l.nativeMask n k Y

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.Layout.clock (l : Layout) (n : ℕ) (Y : Plane) : ℝ

Clock, given by PeriodicPhaseAssembly.periodicClock (l.geometry n) (l.window n).cutoff Y / l.length n.

Equations

• l.clock n Y = NavierStokes.PeriodicPhaseAssembly.periodicClock (l.geometry n) (l.window n).cutoff Y / l.length n

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.Layout.nativeClock (l : Layout) (n : ℕ) (k : Frequency) (Y : Plane) : ℝ

Native clock, given by ((l.geometry n).coordinates k Y).2 / l.length n.

Equations

• l.nativeClock n k Y = ((l.geometry n).coordinates k Y).2 / l.length n

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.Layout.gaussian (l : Layout) (n : ℕ) (Y : Plane) : ℝ

Gaussian, given by GaussianTailFlat.profile (l.clock n Y).

Equations

• l.gaussian n Y = NavierStokes.GaussianTailFlat.profile (l.clock n Y)

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.Layout.nativeGaussian (l : Layout) (n : ℕ) (k : Frequency) (Y : Plane) : ℝ

Native gaussian, given by GaussianTailFlat.profile (l.nativeClock n k Y).

Equations

• l.nativeGaussian n k Y = NavierStokes.GaussianTailFlat.profile (l.nativeClock n k Y)

theorem NavierStokes.ActualPeriodizedSignedRealization.Layout.cutoff_compact (l : Layout) (n : ℕ) : HasCompactSupport (l.cutoff n)

theorem NavierStokes.ActualPeriodizedSignedRealization.Layout.mask_summable (l : Layout) (n : ℕ) (Y : Plane) : Summable fun (k : Frequency) => l.nativeMask n k Y

theorem NavierStokes.ActualPeriodizedSignedRealization.Layout.clock_eq_native (l : Layout) (n : ℕ) (k : Frequency) (Y : Plane) (hk : l.nativeMask n k Y ≠ 0) : l.clock n Y = l.nativeClock n k Y

theorem NavierStokes.ActualPeriodizedSignedRealization.Layout.gaussian_eq_native (l : Layout) (n : ℕ) (k : Frequency) (Y : Plane) (hk : l.nativeMask n k Y ≠ 0) : l.gaussian n Y = l.nativeGaussian n k Y

theorem NavierStokes.ActualPeriodizedSignedRealization.Layout.mask_smooth (l : Layout) (n : ℕ) : ContDiff ℝ (↑⊤) (l.mask n)

theorem NavierStokes.ActualPeriodizedSignedRealization.Layout.clock_smooth (l : Layout) (n : ℕ) : ContDiff ℝ (↑⊤) (l.clock n)

theorem NavierStokes.ActualPeriodizedSignedRealization.Layout.mask_periodic (l : Layout) (n : ℕ) (Y : Plane) (k : Frequency) : l.mask n (Y + TorusAverages.latticePoint k) = l.mask n Y

theorem NavierStokes.ActualPeriodizedSignedRealization.Layout.gaussian_periodic (l : Layout) (n : ℕ) (Y : Plane) (k : Frequency) : l.gaussian n (Y + TorusAverages.latticePoint k) = l.gaussian n Y

theorem NavierStokes.ActualPeriodizedSignedRealization.Layout.gaussian_mask_sum (l : Layout) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (Y : Plane) (a : E) : ∑' (k : Frequency), l.nativeGaussian n k Y • l.nativeMask n k Y • a = l.gaussian n Y • l.mask n Y • a

Actual finite native support justifies the scalar/vector infinite sum. The Gaussian is inserted once, on each native copy.

theorem NavierStokes.ActualPeriodizedSignedRealization.Layout.maskedSum_contDiffOn (l : Layout) {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (projection : D → Plane) (hprojection : ContDiff ℝ (↑⊤) projection) {O : Set D} (hO : IsOpen O) (f : Frequency → D → E) (hf : ∀ (k : TorusInverse.Frequency), ∀ x ∈ O, (l.geometry n).coordinates k (projection x) ∈ tsupport (l.cutoff n) → ContDiffAt ℝ (↑⊤) (f k) x) : ContDiffOn ℝ (↑⊤) (fun (x : D) => ∑' (k : Frequency), l.nativeMask n k (projection x) • f k x) O

Local finiteness of the actual native cutoffs permits arbitrary smooth slow factors; only their germs on the native support are needed.

The primitive homogeneous pressure is linear in its velocity

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.homogeneousPressure (K : ℝ) (N Ndot : Space) (A : Space →L[ℝ] Space) (u : Space) : ℂ

Homogeneous pressure, given by Complex.I * (TangentProjection.pressureCoefficient N Ndot u (A u) 0 : ℂ) / (K : ℂ).

Equations

• NavierStokes.ActualPeriodizedSignedRealization.homogeneousPressure K N Ndot A u = Complex.I * ↑(NavierStokes.TangentProjection.pressureCoefficient N Ndot u (A u) 0) / ↑K

theorem NavierStokes.ActualPeriodizedSignedRealization.homogeneousPressure_smul (K c : ℝ) (N Ndot : Space) (A : Space →L[ℝ] Space) (u : Space) : homogeneousPressure K N Ndot A (c • u) = c • homogeneousPressure K N Ndot A u

theorem NavierStokes.ActualPeriodizedSignedRealization.homogeneousPressure_zero (K : ℝ) (N Ndot : Space) (A : Space →L[ℝ] Space) : homogeneousPressure K N Ndot A 0 = 0

theorem NavierStokes.ActualPeriodizedSignedRealization.coefficients_amplitude_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (H : ℕ → D → Mat2) (T R : ℕ → D → Vec2) (mask : ℕ → D → ℝ) (unit Ndot : ℕ → D → Space) (A : ℕ → D → Space →L[ℝ] Space) (j : Fin 2) (n : ℕ) (x : D) : (SignedWaveUpdate.coefficients a s d H T R mask unit Ndot A j).amplitude n x = SignedWaveUpdate.signedScalar s H T R mask j n x • CurlClassBounds.complexify (unit n x)

theorem NavierStokes.ActualPeriodizedSignedRealization.coefficients_pressure_at {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : LinearWaveBounds.WaveCoefficients D) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) (H : ℕ → D → Mat2) (T R : ℕ → D → Vec2) (mask : ℕ → D → ℝ) (unit Ndot : ℕ → D → Space) (A : ℕ → D → Space →L[ℝ] Space) (j : Fin 2) (n : ℕ) (x : D) : (SignedWaveUpdate.coefficients a s d H T R mask unit Ndot A j).pressure n x = SignedWaveUpdate.signedScalar s H T R mask j n x • homogeneousPressure (a.frequency n) (a.normal s d n x) (Ndot n x) (A n x) (unit n x)

theorem NavierStokes.ActualPeriodizedSignedRealization.signedScalar_mul_mask {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (H : ℕ → D → Mat2) (T R : ℕ → D → Vec2) (mask factor : ℕ → D → ℝ) (j : Fin 2) (n : ℕ) (x : D) : SignedWaveUpdate.signedScalar s H T R (fun (n : ℕ) (x : D) => mask n x * factor n x) j n x = factor n x * SignedWaveUpdate.signedScalar s H T R mask j n x

Periodic reference constructed from the same primary data

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.periodizedPrimary {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) : PhysicalSignedWave.PrimaryData U

Periodized primary, given by {B with coordinate := fun n x => ((B.coordinate n x).1, l.clock n x.1.2.2) mask := fun n x => B.mask n x * l.mask n x.1.2.2}.

Equations

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

@[simp]

theorem NavierStokes.ActualPeriodizedSignedRealization.periodizedPrimary_pulse {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) : (periodizedPrimary B l).pulse = B.pulse

@[simp]

theorem NavierStokes.ActualPeriodizedSignedRealization.periodizedPrimary_target {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) : (periodizedPrimary B l).target = B.target

@[simp]

theorem NavierStokes.ActualPeriodizedSignedRealization.periodizedPrimary_matrix {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) : (periodizedPrimary B l).matrix = B.matrix

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.views {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) : (periodizedPrimary B l).Views reference

All view scales, integer covers, backgrounds, and operators are retained.

Equations

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

@[simp]

theorem NavierStokes.ActualPeriodizedSignedRealization.views_map {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) : (views B l V).map = V.map

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.stateData {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} {V : B.Views reference} (D : V.StateData) : (views B l V).StateData

Reuse the actual current state, reference state, and their full-fiber coherence. There is no second signed choice or request.

Equations

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

@[simp]

theorem NavierStokes.ActualPeriodizedSignedRealization.stateData_request {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} {V : B.Views reference} (D : V.StateData) : (stateData B l D).request = D.request

@[simp]

theorem NavierStokes.ActualPeriodizedSignedRealization.stateData_referenceRequest {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} {V : B.Views reference} (D : V.StateData) : (stateData B l D).referenceRequest = D.referenceRequest

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.sharedMask {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) {reference : ℕ} (V : B.Views reference) (n : ℕ) (x : Cylinder) : ℝ

Shared mask, given by B.mask reference (V.map n x).

Equations

• NavierStokes.ActualPeriodizedSignedRealization.sharedMask B V n x = B.mask reference ((V.map n) x)

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.totalMask {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (n : ℕ) (x : Cylinder) : ℝ

Total mask, given by sharedMask B V n x * l.mask reference (V.map n x).1.2.2.

Equations

• NavierStokes.ActualPeriodizedSignedRealization.totalMask B l V n x = NavierStokes.ActualPeriodizedSignedRealization.sharedMask B V n x * l.mask reference ((V.map n) x).1.2.2

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.copyMask {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (k : Frequency) (n : ℕ) (x : Cylinder) : ℝ

Copy mask, given by sharedMask B V n x * l.nativeMask reference k (V.map n x).1.2.2.

Equations

• NavierStokes.ActualPeriodizedSignedRealization.copyMask B l V k n x = NavierStokes.ActualPeriodizedSignedRealization.sharedMask B V n x * l.nativeMask reference k ((V.map n) x).1.2.2

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.commonUnit {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (j : Fin 2) (n : ℕ) (x : Cylinder) : Space

Common unit, given by (periodizedPrimary B l).fundamental j reference (V.map n x).

Equations

• NavierStokes.ActualPeriodizedSignedRealization.commonUnit B l V j n x = (NavierStokes.ActualPeriodizedSignedRealization.periodizedPrimary B l).fundamental j reference ((V.map n) x)

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.nativeUnit {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (j : Fin 2) (k : Frequency) (n : ℕ) (x : Cylinder) : Space

Native unit, constructed using PrimaryPulseBounds.normalizedPulse.

Equations

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

theorem NavierStokes.ActualPeriodizedSignedRealization.commonUnit_eq_native {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (j : Fin 2) (k : Frequency) (n : ℕ) (x : Cylinder) (hk : l.nativeMask reference k ((V.map n) x).1.2.2 ≠ 0) : commonUnit B l V j n x = nativeUnit B l V j k n x

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.coefficientsWith {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (mask : ℕ → Cylinder → ℝ) (unit : ℕ → Cylinder → Space) : LinearWaveBounds.WaveCoefficients Cylinder

One call to the original homogeneous signed quotient constructor.

Equations

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

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.commonCoefficients {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) : LinearWaveBounds.WaveCoefficients Cylinder

Common coefficients, given by coefficientsWith B l V request j (sharedMask B V) (commonUnit B l V j).

Equations

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

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.nativeCoefficients {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (k : Frequency) : LinearWaveBounds.WaveCoefficients Cylinder

Native coefficients, given by coefficientsWith B l V request j (copyMask B l V k) (nativeUnit B l V j k).

Equations

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

theorem NavierStokes.ActualPeriodizedSignedRealization.views_coefficients {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) : (views B l V).coefficients request j = coefficientsWith B l V request j (totalMask B l V) (commonUnit B l V j)

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.commonScalar {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (n : ℕ) (x : Cylinder) : ℝ

Common scalar, constructed using SignedWaveUpdate.signedScalar.

Equations

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

theorem NavierStokes.ActualPeriodizedSignedRealization.coefficientsWith_amplitude {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (mask : ℕ → Cylinder → ℝ) (unit : ℕ → Cylinder → Space) (n : ℕ) (x : Cylinder) : (coefficientsWith B l V request j mask unit).amplitude n x = SignedWaveUpdate.signedScalar V.strip (fun (n : ℕ) (x : PhysicalSignedWave.Cylinder) => B.matrix reference ((V.map n) x)) (B.viewTarget V.strip V.velocity (fun (n : ℕ) => ⇑(V.map n)) reference) request mask j n x • CurlClassBounds.complexify (unit n x)

theorem NavierStokes.ActualPeriodizedSignedRealization.coefficientsWith_pressure {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (mask : ℕ → Cylinder → ℝ) (unit : ℕ → Cylinder → Space) (n : ℕ) (x : Cylinder) : (coefficientsWith B l V request j mask unit).pressure n x = SignedWaveUpdate.signedScalar V.strip (fun (n : ℕ) (x : PhysicalSignedWave.Cylinder) => B.matrix reference ((V.map n) x)) (B.viewTarget V.strip V.velocity (fun (n : ℕ) => ⇑(V.map n)) reference) request mask j n x • homogeneousPressure (V.frequency n) (((periodizedPrimary B l).viewBase V.background V.frequency (fun (n : ℕ) => ⇑(V.map n)) reference).normal V.strip V.directions n x) ((V.normal n * V.clock n) • B.normalMotion reference ((V.map n) x)) (V.clock n • B.action reference ((V.map n) x)) (unit n x)

theorem NavierStokes.ActualPeriodizedSignedRealization.copy_scalar {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (k : Frequency) (n : ℕ) (x : Cylinder) : SignedWaveUpdate.signedScalar V.strip (fun (n : ℕ) (x : PhysicalSignedWave.Cylinder) => B.matrix reference ((V.map n) x)) (B.viewTarget V.strip V.velocity (fun (n : ℕ) => ⇑(V.map n)) reference) request (copyMask B l V k) j n x = l.nativeMask reference k ((V.map n) x).1.2.2 * SignedWaveUpdate.signedScalar V.strip (fun (n : ℕ) (x : PhysicalSignedWave.Cylinder) => B.matrix reference ((V.map n) x)) (B.viewTarget V.strip V.velocity (fun (n : ℕ) => ⇑(V.map n)) reference) request (sharedMask B V) j n x

theorem NavierStokes.ActualPeriodizedSignedRealization.total_scalar {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (n : ℕ) (x : Cylinder) : SignedWaveUpdate.signedScalar V.strip (fun (n : ℕ) (x : PhysicalSignedWave.Cylinder) => B.matrix reference ((V.map n) x)) (B.viewTarget V.strip V.velocity (fun (n : ℕ) => ⇑(V.map n)) reference) request (totalMask B l V) j n x = l.mask reference ((V.map n) x).1.2.2 * SignedWaveUpdate.signedScalar V.strip (fun (n : ℕ) (x : PhysicalSignedWave.Cylinder) => B.matrix reference ((V.map n) x)) (B.viewTarget V.strip V.velocity (fun (n : ℕ) => ⇑(V.map n)) reference) request (sharedMask B V) j n x

theorem NavierStokes.ActualPeriodizedSignedRealization.native_amplitude {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (k : Frequency) (n : ℕ) (x : Cylinder) : (nativeCoefficients B l V request j k).amplitude n x = l.nativeMask reference k ((V.map n) x).1.2.2 • (commonCoefficients B l V request j).amplitude n x

theorem NavierStokes.ActualPeriodizedSignedRealization.native_pressure {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (k : Frequency) (n : ℕ) (x : Cylinder) : (nativeCoefficients B l V request j k).pressure n x = l.nativeMask reference k ((V.map n) x).1.2.2 • (commonCoefficients B l V request j).pressure n x

theorem NavierStokes.ActualPeriodizedSignedRealization.view_amplitude {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (n : ℕ) (x : Cylinder) : ((views B l V).coefficients request j).amplitude n x = l.mask reference ((V.map n) x).1.2.2 • (commonCoefficients B l V request j).amplitude n x

theorem NavierStokes.ActualPeriodizedSignedRealization.view_pressure {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (n : ℕ) (x : Cylinder) : ((views B l V).coefficients request j).pressure n x = l.mask reference ((V.map n) x).1.2.2 • (commonCoefficients B l V request j).pressure n x

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.copyData {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) : PeriodizedWaveBounds.CopyData Cylinder Frequency

Every lattice copy is built by the actual native signed quotient and projected homogeneous pressure; the cutoff is applied before summation.

Equations

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

theorem NavierStokes.ActualPeriodizedSignedRealization.copyData_raw {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (k : Frequency) : (copyData B l V request j).raw k = nativeCoefficients B l V request j k

theorem NavierStokes.ActualPeriodizedSignedRealization.common_amplitude {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (n : ℕ) (x : Cylinder) : (copyData B l V request j).common.amplitude n x = (((views B l V).coefficients request j).withCutoff (views B l V).cutoff).amplitude n x

theorem NavierStokes.ActualPeriodizedSignedRealization.common_pressure {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (n : ℕ) (x : Cylinder) : (copyData B l V request j).common.pressure n x = (((views B l V).coefficients request j).withCutoff (views B l V).cutoff).pressure n x

theorem NavierStokes.ActualPeriodizedSignedRealization.common_eq {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) : (copyData B l V request j).common = ((views B l V).coefficients request j).withCutoff (views B l V).cutoff

theorem NavierStokes.ActualPeriodizedSignedRealization.commonCorrected_eq {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) : (copyData B l V request j).commonCorrected V.strip V.directions = (views B l V).exactCoefficients request j

Exact coefficient equality precedes all differentiation. In particular every derivative of the native cutoffs remains in the curl.

The literal current-state request and one physical reference

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.actualCopyData {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (D : V.StateData) (j : Fin 2) : PeriodizedWaveBounds.CopyData Cylinder Frequency

The native copies use the current state's actual signed request.

Equations

• NavierStokes.ActualPeriodizedSignedRealization.actualCopyData B l V D j = NavierStokes.ActualPeriodizedSignedRealization.copyData B l V D.request j

theorem NavierStokes.ActualPeriodizedSignedRealization.actual_commonCorrected_eq {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (D : V.StateData) (j : Fin 2) : (actualCopyData B l V D j).commonCorrected V.strip V.directions = (views B l V).exactCoefficients (stateData B l D).request j

theorem NavierStokes.ActualPeriodizedSignedRealization.actual_amplitude_transport {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (D : V.StateData) (j : Fin 2) (n : ℕ) (x : Cylinder) (hx : x ∈ V.strip.domain) : (actualCopyData B l V D j).common.amplitude n x = V.velocity n • (periodizedPrimary B l).raw D.referenceRequest j reference ((V.map n) x)

This equality holds before restriction to a physical graph, at every point of the full slow/angle/fast strip.

theorem NavierStokes.ActualPeriodizedSignedRealization.actual_amplitude_transport_germ {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (D : V.StateData) (j : Fin 2) (n : ℕ) {x : Cylinder} (hx : x ∈ V.strip.domain) : (actualCopyData B l V D j).common.amplitude n =ᶠ[nhds x] fun (y : Cylinder) => V.velocity n • (periodizedPrimary B l).raw D.referenceRequest j reference ((V.map n) y)

theorem NavierStokes.ActualPeriodizedSignedRealization.actual_pressure_transport {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (D : V.StateData) (j : Fin 2) (n : ℕ) (hK : B.base.frequency reference ≠ 0) (G : PhysicalSignedWave.ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (H : PhysicalSignedWave.ChartGeometry (B.viewBase V.background V.frequency (fun (n : ℕ) => ⇑(V.map n)) reference) V.strip V.directions n V.exponent (V.scale n) (V.cover n)) {x : Cylinder} (hx : x ∈ V.strip.domain) (hr : 0 < x.1.1) (hPhi : DifferentiableAt ℝ (B.base.phase reference) ((V.map n) x)) : (actualCopyData B l V D j).common.pressure n x = PhysicalParticularWave.pressureWeight V.exponent (V.scale n) V.referenceScale • (periodizedPrimary B l).rawPressure D.referenceRequest j reference ((V.map n) x)

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.physicalPotential {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (D : V.StateData) (j : Fin 2) (delta : ℝ) : ProblemStatement.VelocityField

One genuine periodized Cartesian potential, retaining the same pulse, reference state, scales, and integer covers as the native copies.

Equations

• NavierStokes.ActualPeriodizedSignedRealization.physicalPotential B l V D j delta = (NavierStokes.ActualPeriodizedSignedRealization.views B l V).physicalPotential D.referenceRequest j delta

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.physicalVelocity {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (D : V.StateData) (j : Fin 2) (delta : ℝ) : ProblemStatement.VelocityField

Physical velocity, given by SpatialCurl.spatialCurl (physicalPotential B l V D j delta).

Equations

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

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.physicalPressure {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (D : V.StateData) (j : Fin 2) (delta : ℝ) : ProblemStatement.PressureField

Physical pressure, given by (views B l V).physicalPressure D.referenceRequest j delta.

Equations

• NavierStokes.ActualPeriodizedSignedRealization.physicalPressure B l V D j delta = (NavierStokes.ActualPeriodizedSignedRealization.views B l V).physicalPressure D.referenceRequest j delta

theorem NavierStokes.ActualPeriodizedSignedRealization.physicalVelocity_eq_curl {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (D : V.StateData) (j : Fin 2) (delta : ℝ) : physicalVelocity B l V D j delta = SpatialCurl.spatialCurl (physicalPotential B l V D j delta)

theorem NavierStokes.ActualPeriodizedSignedRealization.actual_wave_physical {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (D : V.StateData) (j : Fin 2) (n : ℕ) (R : (periodizedPrimary B l).Regular D.referenceRequest reference j) (A : (periodizedPrimary B l).Angular D.referenceRequest reference) (hK : B.base.frequency reference ≠ 0) (G : PhysicalSignedWave.ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (H : PhysicalSignedWave.ChartGeometry (B.viewBase V.background V.frequency (fun (n : ℕ) => ⇑(V.map n)) reference) V.strip V.directions n V.exponent (V.scale n) (V.cover n)) (hmap : Set.MapsTo (⇑(V.map n)) V.strip.domain B.strip.domain) (hradius : ∀ x ∈ V.strip.domain, 0 < x.1.1) {z : ProblemStatement.SpaceTime} (hz : z ∈ (PhysicalResidualBridge.commonGraph (V.scale n) V.exponent (V.cover n)).source V.strip.domain) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) (component : Fin 3) : (HarmonicCalculus.vectorMode (((actualCopyData B l V D j).commonCorrected V.strip V.directions).frequency n) (((actualCopyData B l V D j).commonCorrected V.strip V.directions).phase n) (((actualCopyData B l V D j).commonCorrected V.strip V.directions).amplitude n) ((PhysicalResidualBridge.commonGraph (V.scale n) V.exponent (V.cover n)).map z) component).re = V.scale n ^ CoordinateAlgebra.A V.exponent * ((CylindricalResidual.frame (-z.2.ofLp 1)) (physicalVelocity B l V D j delta (z.1, CylindricalResidual.chart z.2))).ofLp component

The actual native-copy sum, corrected after cutoff and summation, is the band view of the single constructed Cartesian curl. Analytic inputs concern the primitive reference data and coordinate charts.

theorem NavierStokes.ActualPeriodizedSignedRealization.actual_pressure_physical {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (D : V.StateData) (j : Fin 2) (n : ℕ) (R : (periodizedPrimary B l).Regular D.referenceRequest reference j) (A : (periodizedPrimary B l).Angular D.referenceRequest reference) (hK : B.base.frequency reference ≠ 0) (G : PhysicalSignedWave.ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (H : PhysicalSignedWave.ChartGeometry (B.viewBase V.background V.frequency (fun (n : ℕ) => ⇑(V.map n)) reference) V.strip V.directions n V.exponent (V.scale n) (V.cover n)) (hmap : Set.MapsTo (⇑(V.map n)) V.strip.domain B.strip.domain) {z : ProblemStatement.SpaceTime} (hz : z ∈ (PhysicalResidualBridge.commonGraph (V.scale n) V.exponent (V.cover n)).source V.strip.domain) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : (HarmonicCalculus.mode (((actualCopyData B l V D j).commonCorrected V.strip V.directions).frequency n) (((actualCopyData B l V D j).commonCorrected V.strip V.directions).phase n) (((actualCopyData B l V D j).commonCorrected V.strip V.directions).pressure n) ((PhysicalResidualBridge.commonGraph (V.scale n) V.exponent (V.cover n)).map z)).re = V.scale n ^ (2 * CoordinateAlgebra.A V.exponent) * physicalPressure B l V D j delta (z.1, CylindricalResidual.chart z.2)

Support-local primitive regularity on the complete reference strip

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.referenceNativeUnit {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) (j : Fin 2) (n : ℕ) (k : Frequency) (x : Cylinder) : Space

Reference native unit, constructed using PrimaryPulseBounds.normalizedPulse.

Equations

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

theorem NavierStokes.ActualPeriodizedSignedRealization.referenceUnit_eq_native {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) (j : Fin 2) (n : ℕ) (k : Frequency) (x : Cylinder) (hk : l.nativeMask n k x.1.2.2 ≠ 0) : (periodizedPrimary B l).fundamental j n x = referenceNativeUnit B l j n k x

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.referenceScalar {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (n : ℕ) (x : Cylinder) : ℝ

Reference scalar, given by SignedWaveUpdate.signedScalar B.strip B.matrix B.target request B.mask j n x.

Equations

• NavierStokes.ActualPeriodizedSignedRealization.referenceScalar B request j n x = NavierStokes.SignedWaveUpdate.signedScalar B.strip B.matrix B.target request B.mask j n x

theorem NavierStokes.ActualPeriodizedSignedRealization.reference_raw_formula {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (n : ℕ) (x : Cylinder) : (periodizedPrimary B l).raw request j n x = l.gaussian n x.1.2.2 • l.mask n x.1.2.2 • referenceScalar B request j n x • CurlClassBounds.complexify ((periodizedPrimary B l).fundamental j n x)

theorem NavierStokes.ActualPeriodizedSignedRealization.reference_raw_eq_sum {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (n : ℕ) : (periodizedPrimary B l).raw request j n = fun (x : Cylinder) => ∑' (k : Frequency), l.nativeMask n k x.1.2.2 • l.nativeGaussian n k x.1.2.2 • referenceScalar B request j n x • CurlClassBounds.complexify (referenceNativeUnit B l j n k x)

structure NavierStokes.ActualPeriodizedSignedRealization.SupportedRegular {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) (request : ℕ → Cylinder → Vec2) (reference : ℕ) (column : Fin 2) : Prop

Every condition is on the original slow data, native pulse, or native support. Inactive gaps need no uncut pulse-time hypothesis.

• coordinate : ContDiffOn ℝ (↑⊤) (fun (x : PhysicalSignedWave.Cylinder) => (B.coordinate reference x).1) B.strip.domain
• coordinate_mem (x : PhysicalSignedWave.Cylinder) : x ∈ B.strip.domain → (B.coordinate reference x).1 ∈ U.carrier reference
• native_time (k : TorusInverse.Frequency) (x : PhysicalSignedWave.Cylinder) : x ∈ B.strip.domain → (l.geometry reference).coordinates k x.1.2.2 ∈ tsupport (l.cutoff reference) → l.nativeClock reference k x.1.2.2 ∈ Set.Ioo 0 1
• prefactor (j : Fin 2) : PhaseJetBounds.PolynomialJets U fun (n : ℕ) (x : PhaseCalculus.Slow) => B.prefactor j n
• target (j : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (x : PhysicalSignedWave.Cylinder) => B.target reference x j) B.strip.domain
• request (j : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (x : Cylinder) => request reference x j) B.strip.domain
• mask : ContDiffOn ℝ (↑⊤) (B.mask reference) B.strip.domain
• cone (x : PhysicalSignedWave.Cylinder) : x ∈ B.strip.domain → SmoothCovariance.StrictCone (B.matrix reference x) (B.target reference x)
• phase : ContDiffOn ℝ (↑⊤) (B.base.phase reference) B.strip.domain
• normal_ne (x : PhysicalSignedWave.Cylinder) : x ∈ B.strip.domain → B.base.normal B.strip B.directions reference x ≠ 0
• normal_frame (k : Frequency) (x : PhysicalSignedWave.Cylinder) : x ∈ B.strip.domain → l.nativeMask reference k x.1.2.2 ≠ 0 → B.base.normal B.strip B.directions reference x = ((B.pulse column).frame reference).normal ((B.coordinate reference x).1, (B.pulse column).L reference * l.nativeClock reference k x.1.2.2)

theorem NavierStokes.ActualPeriodizedSignedRealization.SupportedRegular.matrix_smooth {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PhysicalSignedWave.PrimaryData U} {l : Layout} {request : ℕ → Cylinder → Vec2} {reference : ℕ} {column : Fin 2} (R : SupportedRegular B l request reference column) (i j : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (x : PhysicalSignedWave.Cylinder) => B.matrix reference x i j) B.strip.domain

theorem NavierStokes.ActualPeriodizedSignedRealization.SupportedRegular.scalar_smooth {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PhysicalSignedWave.PrimaryData U} {l : Layout} {request : ℕ → Cylinder → Vec2} {reference : ℕ} {column : Fin 2} (R : SupportedRegular B l request reference column) (j : Fin 2) : ContDiffOn ℝ (↑⊤) (referenceScalar B request j reference) B.strip.domain

theorem NavierStokes.ActualPeriodizedSignedRealization.SupportedRegular.unit_smoothAt {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PhysicalSignedWave.PrimaryData U} {l : Layout} {request : ℕ → Cylinder → Vec2} {reference : ℕ} {column : Fin 2} (R : SupportedRegular B l request reference column) (j : Fin 2) (k : Frequency) {x : Cylinder} (hx : x ∈ B.strip.domain) (hs : (l.geometry reference).coordinates k x.1.2.2 ∈ tsupport (l.cutoff reference)) : ContDiffAt ℝ (↑⊤) (referenceNativeUnit B l j reference k) x

theorem NavierStokes.ActualPeriodizedSignedRealization.SupportedRegular.raw_smooth {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PhysicalSignedWave.PrimaryData U} {l : Layout} {request : ℕ → Cylinder → Vec2} {reference : ℕ} {column : Fin 2} (R : SupportedRegular B l request reference column) (j : Fin 2) : ContDiffOn ℝ (↑⊤) ((periodizedPrimary B l).raw request j reference) B.strip.domain

Smoothness is derived from the actual native sum, including its zero germs between support cells.

theorem NavierStokes.ActualPeriodizedSignedRealization.SupportedRegular.raw_tangent {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PhysicalSignedWave.PrimaryData U} {l : Layout} {request : ℕ → Cylinder → Vec2} {reference : ℕ} {column : Fin 2} (R : SupportedRegular B l request reference column) {x : Cylinder} (hx : x ∈ B.strip.domain) : HarmonicCalculus.normalDot (B.base.normal B.strip B.directions reference x) ((periodizedPrimary B l).raw request column reference x) = 0

theorem NavierStokes.ActualPeriodizedSignedRealization.fast_invariant : CopyAngularInvariance.Invariant (0, 1) fun (x : Cylinder) => x.1.2.2

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.periodizedAngular {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {request : ℕ → Cylinder → Vec2} {reference : ℕ} (A : B.Angular request reference) : (periodizedPrimary B l).Angular request reference

Angular invariance is inherited from the same primary inputs. The new clock and native mask depend only on the auxiliary torus coordinate.

Equations

• NavierStokes.ActualPeriodizedSignedRealization.periodizedAngular B l A = { mode := A.mode, phase := ⋯, coordinate := ⋯, target := ⋯, request := ⋯, mask := ⋯, normalMotion := ⋯, action := ⋯ }

noncomputable def NavierStokes.ActualPeriodizedSignedRealization.actualBlock {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (D : V.StateData) (j : Fin 2) (angularFrequency : ℕ → ℤ) : CorrectionState.HarmonicBlock PhysicalResidualBridge.Lift

The integer harmonic block is built from the same corrected native sum. No independent wave is substituted into the iteration.

Equations

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

theorem NavierStokes.ActualPeriodizedSignedRealization.actualBlock_eq {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (D : V.StateData) (j : Fin 2) (angularFrequency : ℕ → ℤ) : actualBlock B l V D j angularFrequency = SignedWaveUpdate.blockOfCoefficients ((views B l V).exactCoefficients D.request j) angularFrequency

theorem NavierStokes.ActualPeriodizedSignedRealization.supported_wave_physical {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (D : V.StateData) (j : Fin 2) (n : ℕ) (R : SupportedRegular B l D.referenceRequest reference j) (A : B.Angular D.referenceRequest reference) (hK : B.base.frequency reference ≠ 0) (G : PhysicalSignedWave.ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (H : PhysicalSignedWave.ChartGeometry (B.viewBase V.background V.frequency (fun (n : ℕ) => ⇑(V.map n)) reference) V.strip V.directions n V.exponent (V.scale n) (V.cover n)) (hmap : Set.MapsTo (⇑(V.map n)) V.strip.domain B.strip.domain) (hradius : ∀ x ∈ V.strip.domain, 0 < x.1.1) {z : ProblemStatement.SpaceTime} (hz : z ∈ (PhysicalResidualBridge.commonGraph (V.scale n) V.exponent (V.cover n)).source V.strip.domain) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) (component : Fin 3) : (HarmonicCalculus.vectorMode (((actualCopyData B l V D j).commonCorrected V.strip V.directions).frequency n) (((actualCopyData B l V D j).commonCorrected V.strip V.directions).phase n) (((actualCopyData B l V D j).commonCorrected V.strip V.directions).amplitude n) ((PhysicalResidualBridge.commonGraph (V.scale n) V.exponent (V.cover n)).map z) component).re = V.scale n ^ CoordinateAlgebra.A V.exponent * ((CylindricalResidual.frame (-z.2.ofLp 1)) (physicalVelocity B l V D j delta (z.1, CylindricalResidual.chart z.2))).ofLp component

Full-strip realization from support-local native input regularity. There is no condition on the uncut pulse in inactive periodic gaps.

theorem NavierStokes.ActualPeriodizedSignedRealization.supported_pressure_physical {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PhysicalSignedWave.PrimaryData U) (l : Layout) {reference : ℕ} (V : B.Views reference) (D : V.StateData) (j : Fin 2) (n : ℕ) (R : SupportedRegular B l D.referenceRequest reference j) (A : B.Angular D.referenceRequest reference) (hK : B.base.frequency reference ≠ 0) (G : PhysicalSignedWave.ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (H : PhysicalSignedWave.ChartGeometry (B.viewBase V.background V.frequency (fun (n : ℕ) => ⇑(V.map n)) reference) V.strip V.directions n V.exponent (V.scale n) (V.cover n)) (hmap : Set.MapsTo (⇑(V.map n)) V.strip.domain B.strip.domain) {z : ProblemStatement.SpaceTime} (hz : z ∈ (PhysicalResidualBridge.commonGraph (V.scale n) V.exponent (V.cover n)).source V.strip.domain) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : (HarmonicCalculus.mode (((actualCopyData B l V D j).commonCorrected V.strip V.directions).frequency n) (((actualCopyData B l V D j).commonCorrected V.strip V.directions).phase n) (((actualCopyData B l V D j).commonCorrected V.strip V.directions).pressure n) ((PhysicalResidualBridge.commonGraph (V.scale n) V.exponent (V.cover n)).map z)).re = V.scale n ^ (2 * CoordinateAlgebra.A V.exponent) * physicalPressure B l V D j delta (z.1, CylindricalResidual.chart z.2)

Pressure uses the same native quotient, normal motion, action and single Gaussian, with its physical squared-velocity scaling.