Signed quotient waves from one physical primary reference

The signed numerator is the actual current-state stress request. All band views use the same absolute-lift primary pulse and covariance matrix. Compatibility is proved before restriction to a physical graph.

@[reducible, inline]

abbrev NavierStokes.PhysicalSignedWave.Mat2 : Type

Mat2: an abbreviation for SmoothCovariance.Mat2.

Equations

• NavierStokes.PhysicalSignedWave.Mat2 = NavierStokes.SmoothCovariance.Mat2

@[reducible, inline]

abbrev NavierStokes.PhysicalSignedWave.Vec2 : Type

Vec2: an abbreviation for SmoothCovariance.Vec2.

Equations

• NavierStokes.PhysicalSignedWave.Vec2 = NavierStokes.SmoothCovariance.Vec2

@[reducible, inline]

abbrev NavierStokes.PhysicalSignedWave.Point : Type

Point: an abbreviation for LocalSignedRequest.Point.

Equations

• NavierStokes.PhysicalSignedWave.Point = NavierStokes.LocalSignedRequest.Point

@[reducible, inline]

abbrev NavierStokes.PhysicalSignedWave.Cylinder : Type

Cylinder: an abbreviation for PhysicalResidualBridge.Cylinder.

Equations

• NavierStokes.PhysicalSignedWave.Cylinder = NavierStokes.PhysicalResidualBridge.Cylinder

noncomputable def NavierStokes.PhysicalSignedWave.fastTranslate (x : Cylinder) (k : TorusInverse.Frequency) : Cylinder

Fast translate, given by ((x.1.1, (x.1.2.1, x.1.2.2 + TorusAverages.latticePoint k)), x.2).

Equations

• NavierStokes.PhysicalSignedWave.fastTranslate x k = ((x.1.1, x.1.2.1, x.1.2.2 + NavierStokes.TorusAverages.latticePoint k), x.2)

theorem NavierStokes.PhysicalSignedWave.weights_smul_target (H : Mat2) (T : Vec2) (a : ℝ) : SmoothCovariance.weights H (a • T) = a • SmoothCovariance.weights H T

theorem NavierStokes.PhysicalSignedWave.inverse_smul_target (H : Mat2) (T : Vec2) (a : ℝ) : Matrix.mulVec H⁻¹ (a • T) = a • Matrix.mulVec H⁻¹ T

theorem NavierStokes.PhysicalSignedWave.amplitudes_square_scale (H : Mat2) (T : Vec2) {a : ℝ} (ha : 0 ≤ a) : SmoothCovariance.amplitudes H (a ^ 2 • T) = a • SmoothCovariance.amplitudes H T

theorem NavierStokes.PhysicalSignedWave.increment_square_scale (H : Mat2) (T R : Vec2) {a : ℝ} (ha : 0 < a) (j : Fin 2) : SignedCovariance.increment H (a ^ 2 • T) (a ^ 2 • R) j = a * SignedCovariance.increment H T R j

Both the signed numerator and the original primary target acquire the same squared scale. The quotient is therefore multiplied by the positive scale, including points where its totalized denominator is zero.

noncomputable def NavierStokes.PhysicalSignedWave.coefficientScale (epsilon referenceEpsilon velocityScale : ℝ) : ℝ

Coefficient scale, given by velocityScale * Real.sqrt referenceEpsilon / Real.sqrt epsilon.

Equations

• NavierStokes.PhysicalSignedWave.coefficientScale epsilon referenceEpsilon velocityScale = velocityScale * √referenceEpsilon / √epsilon

theorem NavierStokes.PhysicalSignedWave.coefficientScale_pos {epsilon referenceEpsilon velocityScale : ℝ} (he : 0 < epsilon) (hr : 0 < referenceEpsilon) (hv : 0 < velocityScale) : 0 < coefficientScale epsilon referenceEpsilon velocityScale

theorem NavierStokes.PhysicalSignedWave.coefficientScale_square {epsilon referenceEpsilon velocityScale : ℝ} (he : 0 < epsilon) (hr : 0 ≤ referenceEpsilon) : coefficientScale epsilon referenceEpsilon velocityScale ^ 2 = velocityScale ^ 2 * referenceEpsilon / epsilon

theorem NavierStokes.PhysicalSignedWave.sqrt_mul_coefficientScale {epsilon referenceEpsilon velocityScale : ℝ} (he : 0 < epsilon) : √epsilon * coefficientScale epsilon referenceEpsilon velocityScale = velocityScale * √referenceEpsilon

theorem NavierStokes.PhysicalSignedWave.primary_scalar_scale (H : Mat2) (T : Vec2) (mask : ℝ) {epsilon referenceEpsilon velocityScale : ℝ} (he : 0 < epsilon) (hr : 0 < referenceEpsilon) (hv : 0 < velocityScale) (j : Fin 2) : PartitionedCovariance.amplitude epsilon mask H (coefficientScale epsilon referenceEpsilon velocityScale ^ 2 • T) j = velocityScale * PartitionedCovariance.amplitude referenceEpsilon mask H T j

The primary square root and the signed inverse quotient have exactly the same velocity scaling. The matrix and column are unchanged.

theorem NavierStokes.PhysicalSignedWave.signed_scalar_scale (H : Mat2) (T R : Vec2) (mask : ℝ) {epsilon referenceEpsilon velocityScale : ℝ} (he : 0 < epsilon) (hr : 0 < referenceEpsilon) (hv : 0 < velocityScale) (j : Fin 2) : √epsilon * SignedCovariance.increment H (coefficientScale epsilon referenceEpsilon velocityScale ^ 2 • T) (coefficientScale epsilon referenceEpsilon velocityScale ^ 2 • R) j * mask = velocityScale * (√referenceEpsilon * SignedCovariance.increment H T R j * mask)

theorem NavierStokes.PhysicalSignedWave.increment_twice_target (H : Mat2) (T : Vec2) (j : Fin 2) : SignedCovariance.increment H T (2 • T) j = SmoothCovariance.amplitudes H T j

With request twice the target, the literal signed quotient is exactly the primary square root. This also holds at totalized zero denominators.

A concrete periodic reference phase with native clock germs

structure NavierStokes.PhysicalSignedWave.ReferencePhase : Type

Reference phase data, collecting geometry, window, epsilon, axialFrequency, radialFrequency, angularMode and their compatibility conditions.

• geometry : CommonCoverSolve.Geometry

  Geometry of ReferencePhase, of type CommonCoverSolve.Geometry.

• window : PeriodicPhaseAssembly.ClockWindow

  Window of ReferencePhase, of type PeriodicPhaseAssembly.ClockWindow.

• epsilon : ℝ

  Epsilon of ReferencePhase, of type ℝ.

• axialFrequency : ℝ

  Axial frequency of ReferencePhase, of type ℝ.

• radialFrequency : ℝ

  Radial frequency of ReferencePhase, of type ℝ.

• angularMode : ℤ

  Angular mode of ReferencePhase, of type ℤ.

• F : PeriodicPhaseAssembly.Parameter → ℝ

  F of ReferencePhase, of type PeriodicPhaseAssembly.Parameter → ℝ.

• G : PeriodicPhaseAssembly.Parameter → ℝ

  Geometric data of ReferencePhase, of type PeriodicPhaseAssembly.Parameter → ℝ.

noncomputable def NavierStokes.PhysicalSignedWave.ReferencePhase.phase (C : ReferencePhase) (K : ℝ) (x : Cylinder) : ℝ

Phase, constructed using PeriodicPhaseAssembly.angularLift.

Equations

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

noncomputable def NavierStokes.PhysicalSignedWave.ReferencePhase.nativePhase (C : ReferencePhase) (K : ℝ) (copy : TorusInverse.Frequency) (x : Cylinder) : ℝ

Native phase, constructed using PhaseCalculus.phase.

Equations

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

theorem NavierStokes.PhysicalSignedWave.ReferencePhase.phase_affine (C : ReferencePhase) (K : ℝ) : CopyAngularInvariance.AffinePhase (0, 1) (↑C.angularMode / K) (C.phase K)

theorem NavierStokes.PhysicalSignedWave.ReferencePhase.phase_periodic (C : ReferencePhase) (K : ℝ) (x : Cylinder) (k : TorusInverse.Frequency) : C.phase K (fastTranslate x k) = C.phase K x

theorem NavierStokes.PhysicalSignedWave.ReferencePhase.phase_native_germ (C : ReferencePhase) (K : ℝ) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => C.geometry.center + C.geometry.basis z) '' C.window.outer)) (copy : TorusInverse.Frequency) {x : Cylinder} (hx : C.geometry.coordinates copy x.1.2.2 ∈ C.window.core) : C.phase K =ᶠ[nhds x] C.nativePhase K copy

theorem NavierStokes.PhysicalSignedWave.ReferencePhase.phase_native_jets (C : ReferencePhase) (K : ℝ) (hinj : Set.InjOn TorusAverages.quotientPoint ((fun (z : TorusInverse.Plane) => C.geometry.center + C.geometry.basis z) '' C.window.outer)) (copy : TorusInverse.Frequency) {x : Cylinder} (hx : C.geometry.coordinates copy x.1.2.2 ∈ C.window.core) (m : ℕ) : iteratedFDeriv ℝ m (C.phase K) x = iteratedFDeriv ℝ m (C.nativePhase K copy) x

theorem NavierStokes.PhysicalSignedWave.ReferencePhase.phase_smooth (C : ReferencePhase) (K : ℝ) (hF : ContDiff ℝ (↑⊤) C.F) (hG : ContDiff ℝ (↑⊤) C.G) : ContDiff ℝ (↑⊤) (C.phase K)

noncomputable def NavierStokes.PhysicalSignedWave.ReferencePhase.base (C : ReferencePhase) (a : LinearWaveBounds.WaveCoefficients Cylinder) : LinearWaveBounds.WaveCoefficients Cylinder

Base, given by { a with phase := fun n => C.phase (a.frequency n) }.

Equations

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

theorem NavierStokes.PhysicalSignedWave.fullRequest_chart (s sr : WeightedClasses.StripData Point) (P : SignedStressPrimitive.Patch) (coord coordr : ℝ) (c cr : CorrectionState.Context Point) (u ur : CorrectionState.State Point) (n nr : ℕ) {l : ℝ} (hl : 0 < l) (C : LocalSignedRequest.Plane →L[ℝ] LocalSignedRequest.Plane) (gap : ℕ) (sourceScale : ℝ) (t : LocalSignedRequest.Plane) (hq : 0 < SimilarityCoordinates.coordinateQ coord t) {V : Set LocalSignedRequest.Plane} (hV : IsOpen V) (ht : C t ∈ V) (hθ : ContDiffOn ℝ (↑⊤) (ur.thetaResidual cr nr) (PhysicalMeanDomain.slowDomain V)) (hz : ContDiffOn ℝ (↑⊤) (ur.axialResidual cr nr) (PhysicalMeanDomain.slowDomain V)) (hpθ : PhysicalMeanDomain.PeriodicOn V (ur.thetaResidual cr nr)) (hpz : PhysicalMeanDomain.PeriodicOn V (ur.axialResidual cr nr)) (hlength : √(SimilarityCoordinates.coordinateQ coordr (C t)) = l * √(SimilarityCoordinates.coordinateQ coord t)) (heθ : ∀ (r : ℝ) (Y : PressureStream.Plane), u.thetaResidual c n (r, t, Y) = sourceScale * ur.thetaResidual cr nr (l * r, C t, (TemporalMeanUpdate.coverMap gap) Y)) (hez : ∀ (r : ℝ) (Y : PressureStream.Plane), u.axialResidual c n (r, t, Y) = sourceScale * ur.axialResidual cr nr (l * r, C t, (TemporalMeanUpdate.coverMap gap) Y)) (r : ℝ) (Y : LocalSignedRequest.Plane) (angle : ℝ) : LocalSignedRequest.fullRequest s P coord c u n ((r, t, Y), angle) = (sourceScale / l * sr.epsilon nr / s.epsilon n) • LocalSignedRequest.fullRequest sr P coordr cr ur nr ((l * r, C t, (TemporalMeanUpdate.coverMap gap) Y), angle)

The primitive is taken from the actual current-state residual on every radius and fast coordinate of the stated slow fiber. Graph-only agreement is not used in this theorem.

theorem NavierStokes.PhysicalSignedWave.source_over_radial {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (h : ℝ) : PhysicalParticularWave.sourceWeight h Q Qr / PhysicalParticularWave.ratioPower Q Qr (1 / 2) = PhysicalParticularWave.velocityWeight h Q Qr ^ 2

theorem NavierStokes.PhysicalSignedWave.physical_request_factor {Q Qr epsilon referenceEpsilon : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (he : 0 < epsilon) (hr : 0 ≤ referenceEpsilon) (h : ℝ) : PhysicalParticularWave.sourceWeight h Q Qr / PhysicalParticularWave.ratioPower Q Qr (1 / 2) * referenceEpsilon / epsilon = coefficientScale epsilon referenceEpsilon (PhysicalParticularWave.velocityWeight h Q Qr) ^ 2

The actual current-state request on the full free lift

noncomputable def NavierStokes.PhysicalSignedWave.slowChange (h Q Qr : ℝ) : LocalSignedRequest.Plane →L[ℝ] LocalSignedRequest.Plane

Slow change as an element of LocalSignedRequest.Plane →L[ℝ] LocalSignedRequest.Plane.

Equations

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

noncomputable def NavierStokes.PhysicalSignedWave.requestChart (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) : Point ≃L[ℝ] Point

Request chart as an element of Point ≃L[ℝ] Point.

Equations

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

theorem NavierStokes.PhysicalSignedWave.requestChart_apply (h : ℝ) {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (gap : ℕ) (x : Point) : (requestChart h hQ hQr gap) x = (PhysicalParticularWave.ratioPower Q Qr (1 / 2) * x.1, (slowChange h Q Qr) x.2.1, (TemporalMeanUpdate.coverMap gap) x.2.2)

theorem NavierStokes.PhysicalSignedWave.ratioPower_eq_div_rpow {Q Qr : ℝ} (hQ : 0 < Q) (hQr : 0 < Qr) (p : ℝ) : PhysicalParticularWave.ratioPower Q Qr p = (Q / Qr) ^ p

theorem NavierStokes.PhysicalSignedWave.slowChange_coordinateQ {h Q Qr : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (hQr : 0 < Qr) {t : LocalSignedRequest.Plane} (ht : 0 < t.1) : SimilarityCoordinates.coordinateQ (2 * h) ((slowChange h Q Qr) t) = Q / Qr * SimilarityCoordinates.coordinateQ (2 * h) t

theorem NavierStokes.PhysicalSignedWave.slowChange_length {h Q Qr : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (hQr : 0 < Qr) {t : LocalSignedRequest.Plane} (ht : 0 < t.1) : √(SimilarityCoordinates.coordinateQ (2 * h) ((slowChange h Q Qr) t)) = PhysicalParticularWave.ratioPower Q Qr (1 / 2) * √(SimilarityCoordinates.coordinateQ (2 * h) t)

noncomputable def NavierStokes.PhysicalSignedWave.stateStrip (s : WeightedClasses.StripData Cylinder) : WeightedClasses.StripData Point

The strip and input coordinates are moved together. Its epsilon is definitionally the epsilon of the same full-angle wave strip.

Equations

• NavierStokes.PhysicalSignedWave.stateStrip s = NavierStokes.SignedWaveUpdate.sectionStrip (NavierStokes.ParticularWaveBounds.reindexStrip NavierStokes.PhysicalResidualTZ.swapCylinder s)

noncomputable def NavierStokes.PhysicalSignedWave.stateRequest (s : WeightedClasses.StripData Cylinder) (P : SignedStressPrimitive.Patch) (h : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) : ℕ → Cylinder → Vec2

State request, defined pointwise by LocalSignedRequest.fullRequest (stateStrip s) P (2 * h) c u n (PhysicalResidualTZ.swapCylinder x).

Equations

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

theorem NavierStokes.PhysicalSignedWave.stateRequest_invariant (s : WeightedClasses.StripData Cylinder) (P : SignedStressPrimitive.Patch) (h : ℝ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (n : ℕ) : CopyAngularInvariance.Invariant (0, 1) (stateRequest s P h c u n)

theorem NavierStokes.PhysicalSignedWave.fullRequest_of_state (s sr : WeightedClasses.StripData Point) (P : SignedStressPrimitive.Patch) {h Q Qr : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (hQr : 0 < Qr) (c cr : CorrectionState.Context Point) (u ur : CorrectionState.State Point) (n nr gap : ℕ) {W : Set Point} (hW : IsOpen W) (H : PhysicalResidualNaturality.StateOn W (requestChart h hQ hQr gap) (PhysicalParticularWave.velocityWeight h Q Qr) (PhysicalParticularWave.ratioPower Q Qr (1 / 2)) u ur n nr) (G : PhysicalResidualNaturality.ContextOn W (requestChart h hQ hQr gap) (PhysicalParticularWave.velocityWeight h Q Qr) (PhysicalParticularWave.ratioPower Q Qr (1 / 2)) c cr n nr) (t : LocalSignedRequest.Plane) (ht : 0 < t.1) (hfiber : ∀ (r : ℝ) (Y : PressureStream.Plane), (r, t, Y) ∈ W) {V : Set LocalSignedRequest.Plane} (hV : IsOpen V) (htV : (slowChange h Q Qr) t ∈ V) (hθ : ContDiffOn ℝ (↑⊤) (ur.thetaResidual cr nr) (PhysicalMeanDomain.slowDomain V)) (hz : ContDiffOn ℝ (↑⊤) (ur.axialResidual cr nr) (PhysicalMeanDomain.slowDomain V)) (hpθ : PhysicalMeanDomain.PeriodicOn V (ur.thetaResidual cr nr)) (hpz : PhysicalMeanDomain.PeriodicOn V (ur.axialResidual cr nr)) (r : ℝ) (Y : LocalSignedRequest.Plane) (angle : ℝ) : LocalSignedRequest.fullRequest s P (2 * h) c u n ((r, t, Y), angle) = coefficientScale (s.epsilon n) (sr.epsilon nr) (PhysicalParticularWave.velocityWeight h Q Qr) ^ 2 • LocalSignedRequest.fullRequest sr P (2 * h) cr ur nr ((requestChart h hQ hQr gap) (r, t, Y), angle)

Naturality of the actual request is a consequence of primitive current-state and background coherence on an open free-lift neighborhood containing the whole integration fiber. No residual or quotient compatibility is a hypothesis.

theorem NavierStokes.PhysicalSignedWave.stateRequest_of_state (s sr : WeightedClasses.StripData Cylinder) (P : SignedStressPrimitive.Patch) {h Q Qr : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (hQr : 0 < Qr) (c cr : CorrectionState.Context Point) (u ur : CorrectionState.State Point) (n nr gap : ℕ) {W : Set Point} (hW : IsOpen W) (H : PhysicalResidualNaturality.StateOn W (requestChart h hQ hQr gap) (PhysicalParticularWave.velocityWeight h Q Qr) (PhysicalParticularWave.ratioPower Q Qr (1 / 2)) u ur n nr) (G : PhysicalResidualNaturality.ContextOn W (requestChart h hQ hQr gap) (PhysicalParticularWave.velocityWeight h Q Qr) (PhysicalParticularWave.ratioPower Q Qr (1 / 2)) c cr n nr) (x : Cylinder) (ht : 0 < x.1.2.1.2) (hfiber : ∀ (r : ℝ) (Y : PressureStream.Plane), (r, (x.1.2.1.2, x.1.2.1.1), Y) ∈ W) {V : Set LocalSignedRequest.Plane} (hV : IsOpen V) (htV : (slowChange h Q Qr) (x.1.2.1.2, x.1.2.1.1) ∈ V) (hθ : ContDiffOn ℝ (↑⊤) (ur.thetaResidual cr nr) (PhysicalMeanDomain.slowDomain V)) (hz : ContDiffOn ℝ (↑⊤) (ur.axialResidual cr nr) (PhysicalMeanDomain.slowDomain V)) (hpθ : PhysicalMeanDomain.PeriodicOn V (ur.thetaResidual cr nr)) (hpz : PhysicalMeanDomain.PeriodicOn V (ur.axialResidual cr nr)) : stateRequest s P h c u n x = coefficientScale (s.epsilon n) (sr.epsilon nr) (PhysicalParticularWave.velocityWeight h Q Qr) ^ 2 • stateRequest sr P h cr ur nr ((PhysicalParticularWave.cylinderChange h Q Qr gap) x)

theorem NavierStokes.PhysicalSignedWave.signedVector_transport {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData D) (sr : WeightedClasses.StripData E) (H : ℕ → D → Mat2) (Hr : ℕ → E → Mat2) (T R : ℕ → D → Vec2) (Tr Rr : ℕ → E → Vec2) (mask : ℕ → D → ℝ) (maskr : ℕ → E → ℝ) (v : ℕ → D → ProblemStatement.Space) (vr : ℕ → E → ProblemStatement.Space) (n nr : ℕ) (x : D) (xr : E) {c : ℝ} (hc : 0 < c) (hH : H n x = Hr nr xr) (hT : T n x = coefficientScale (s.epsilon n) (sr.epsilon nr) c ^ 2 • Tr nr xr) (hR : R n x = coefficientScale (s.epsilon n) (sr.epsilon nr) c ^ 2 • Rr nr xr) (hm : mask n x = maskr nr xr) (hv : v n x = vr nr xr) (j : Fin 2) : SignedWaveUpdate.signedVector s H T R mask v j n x = c • SignedWaveUpdate.signedVector sr Hr Tr Rr maskr vr j nr xr

Exact pointwise transport of the literal signed quotient coefficient from primitive matrix, targets, mask and primary fundamental identities.

theorem NavierStokes.PhysicalSignedWave.homogeneousPressure_scale (K Kr rate c normalScale : ℝ) (hK : K ≠ 0) (hKr : Kr ≠ 0) (hs : normalScale ≠ 0) (N Ndot v Av : ProblemStatement.Space) : Complex.I * ↑(TangentProjection.pressureCoefficient (normalScale • N) ((normalScale * rate) • Ndot) (c • v) ((rate * c) • Av) 0) / ↑K = (rate * c / normalScale * (Kr / K)) • (Complex.I * ↑(TangentProjection.pressureCoefficient N Ndot v Av 0) / ↑Kr)

One actual primary pulse family, reused in every view

structure NavierStokes.PhysicalSignedWave.PrimaryData (U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow) : Type

Only primary construction data and background fields are stored. The pulse, covariance matrix, square roots and signed quotients are all computed by the existing constructors.

• strip : WeightedClasses.StripData Cylinder

  Strip of PrimaryData, of type StripData Cylinder.

• base : LinearWaveBounds.WaveCoefficients Cylinder

  Base of PrimaryData, of type LinearWaveBounds.WaveCoefficients Cylinder.

• directions : LinearWaveBounds.GraphDirections Cylinder

  Directions of PrimaryData, of type LinearWaveBounds.GraphDirections Cylinder.

• pulse : Fin 2 → PrimaryPulseBounds.PhaseConstruction U

  Pulse of PrimaryData, of type Fin 2 → PrimaryPulseBounds.PhaseConstruction U.

• prefactor : Fin 2 → ℕ → ℝ

  Prefactor of PrimaryData, of type Fin 2 → ℕ → ℝ.

• coordinate : ℕ → Cylinder → PhaseCalculus.Slow × ℝ

  Coordinate of PrimaryData, of type ℕ → Cylinder → PhaseCalculus.Slow × ℝ.

• target : ℕ → Cylinder → Vec2

  Target of PrimaryData, of type ℕ → Cylinder → Vec2.

• mask : ℕ → Cylinder → ℝ

  Mask of PrimaryData, of type ℕ → Cylinder → ℝ.

• normalMotion : ℕ → Cylinder → ProblemStatement.Space

  Normal motion of PrimaryData, of type ℕ → Cylinder → Space.

• action : ℕ → Cylinder → ProblemStatement.Space →L[ℝ] ProblemStatement.Space

  Action of PrimaryData, of type ℕ → Cylinder → Space →L[ℝ] Space.

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.withReferencePhase {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (C : ReferencePhase) : PrimaryData U

With reference phase, given by { B with base := C.base B.base }.

Equations

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

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.matrix {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) : ℕ → Cylinder → Mat2

Matrix, given by SignedWaveUpdate.phaseMatrix B.pulse B.prefactor B.coordinate.

Equations

• B.matrix = NavierStokes.SignedWaveUpdate.phaseMatrix B.pulse B.prefactor B.coordinate

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.fundamental {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (j : Fin 2) : ℕ → Cylinder → ProblemStatement.Space

Fundamental, given by SignedWaveUpdate.phaseFundamental B.pulse B.coordinate j.

Equations

• B.fundamental j = NavierStokes.SignedWaveUpdate.phaseFundamental B.pulse B.coordinate j

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.cutoff {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (n : ℕ) (x : Cylinder) : ℝ

The single Gaussian slot cutoff of this primary pulse.

Equations

• B.cutoff n x = NavierStokes.GaussianTailFlat.profile (B.coordinate n x).2

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.coefficients {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (request : ℕ → Cylinder → Vec2) (j : Fin 2) : LinearWaveBounds.WaveCoefficients Cylinder

Coefficients, constructed using SignedWaveUpdate.coefficients.

Equations

• B.coefficients request j = NavierStokes.SignedWaveUpdate.coefficients B.base B.strip B.directions B.matrix B.target request B.mask (B.fundamental j) B.normalMotion B.action j

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.primaryVector {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (j : Fin 2) (n : ℕ) (x : Cylinder) : ProblemStatement.Space

Primary vector, given by PartitionedCovariance.amplitude (B.strip.epsilon n) (B.mask n x) (B.matrix n x) (B.target n x) j • B.fundamental j n x.

Equations

• B.primaryVector j n x = NavierStokes.PartitionedCovariance.amplitude (B.strip.epsilon n) (B.mask n x) (B.matrix n x) (B.target n x) j • B.fundamental j n x

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.primaryCoefficients {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (j : Fin 2) : LinearWaveBounds.WaveCoefficients Cylinder

Primary coefficients, given by SignedWaveUpdate.homogeneousCoefficients B.base B.strip B.directions (B.primaryVector j) B.normalMotion B.action.

Equations

• B.primaryCoefficients j = NavierStokes.SignedWaveUpdate.homogeneousCoefficients B.base B.strip B.directions (B.primaryVector j) B.normalMotion B.action

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.primaryRequest {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) : ℕ → Cylinder → Vec2

Primary request, defined pointwise by (2 : ℝ) • B.target n x.

Equations

• B.primaryRequest n x = 2 • B.target n x

theorem NavierStokes.PhysicalSignedWave.PrimaryData.primaryVector_eq_signed {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (j : Fin 2) : B.primaryVector j = SignedWaveUpdate.signedVector B.strip B.matrix B.target B.primaryRequest B.mask (B.fundamental j) j

theorem NavierStokes.PhysicalSignedWave.PrimaryData.primaryCoefficients_eq_signed {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (j : Fin 2) : B.primaryCoefficients j = B.coefficients B.primaryRequest j

theorem NavierStokes.PhysicalSignedWave.PrimaryData.primary_cutoff_amplitude {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (j : Fin 2) (n : ℕ) (x : Cylinder) : ((B.primaryCoefficients j).withCutoff B.cutoff).amplitude n x = PartitionedCovariance.amplitude (B.strip.epsilon n) (B.mask n x) (B.matrix n x) (B.target n x) j • CurlClassBounds.complexify (PrimaryPulseBounds.cutoffPulse ((B.pulse j).frame n) ((B.pulse j).lam n) ((B.pulse j).u n) ((B.pulse j).L n) (B.coordinate n x))

The primary uses the actual normalized Volterra pulse. Its Gaussian factor is inserted exactly once, after the primary square root.

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.viewBase {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (background : LinearWaveBounds.WaveCoefficients Cylinder) (frequency : ℕ → ℝ) (view : ℕ → Cylinder → Cylinder) (reference : ℕ) : LinearWaveBounds.WaveCoefficients Cylinder

The same reference carrier is pulled back before multiplication by the target band's frequency. All other background fields remain inputs.

Equations

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

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.viewTarget {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (s : WeightedClasses.StripData Cylinder) (velocity : ℕ → ℝ) (view : ℕ → Cylinder → Cylinder) (reference : ℕ) : ℕ → Cylinder → Vec2

View target, defined pointwise by coefficientScale (s.epsilon n) (B.strip.epsilon reference) (velocity n) ^ 2 • B.target reference (view n x).

Equations

• B.viewTarget s velocity view reference n x = NavierStokes.PhysicalSignedWave.coefficientScale (s.epsilon n) (B.strip.epsilon reference) (velocity n) ^ 2 • B.target reference (view n x)

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.viewCutoff {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (view : ℕ → Cylinder → Cylinder) (reference : ℕ) : ℕ → Cylinder → ℝ

View cutoff, defined pointwise by B.cutoff reference (view n x).

Equations

• B.viewCutoff view reference n x = B.cutoff reference (view n x)

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.viewCoefficients {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (s : WeightedClasses.StripData Cylinder) (d : LinearWaveBounds.GraphDirections Cylinder) (background : LinearWaveBounds.WaveCoefficients Cylinder) (frequency velocity clock normal : ℕ → ℝ) (view : ℕ → Cylinder → Cylinder) (reference : ℕ) (request : ℕ → Cylinder → Vec2) (j : Fin 2) : LinearWaveBounds.WaveCoefficients Cylinder

Each view calls the actual signed quotient constructor, with the same reference pulse and matrix. Its request may be the literal current-state request and is not replaced by an independently chosen signed wave.

Equations

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

theorem NavierStokes.PhysicalSignedWave.PrimaryData.view_carrier {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (background : LinearWaveBounds.WaveCoefficients Cylinder) (frequency : ℕ → ℝ) (view : ℕ → Cylinder → Cylinder) (reference n : ℕ) (hf : frequency n ≠ 0) (x : Cylinder) : (B.viewBase background frequency view reference).frequency n * (B.viewBase background frequency view reference).phase n x = B.base.frequency reference * B.base.phase reference (view n x)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.view_signedVector {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (s : WeightedClasses.StripData Cylinder) (velocity : ℕ → ℝ) (view : ℕ → Cylinder → Cylinder) (reference n : ℕ) (request referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) (x : Cylinder) (hc : 0 < velocity n) (hrequest : request n x = coefficientScale (s.epsilon n) (B.strip.epsilon reference) (velocity n) ^ 2 • referenceRequest reference (view n x)) : SignedWaveUpdate.signedVector s (fun (n : ℕ) (x : Cylinder) => B.matrix reference (view n x)) (B.viewTarget s velocity view reference) request (fun (n : ℕ) (x : Cylinder) => B.mask reference (view n x)) (fun (n : ℕ) (x : Cylinder) => B.fundamental j reference (view n x)) j n x = velocity n • SignedWaveUpdate.signedVector B.strip B.matrix B.target referenceRequest B.mask (B.fundamental j) j reference (view n x)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.view_amplitude {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (s : WeightedClasses.StripData Cylinder) (d : LinearWaveBounds.GraphDirections Cylinder) (background : LinearWaveBounds.WaveCoefficients Cylinder) (frequency velocity clock normal : ℕ → ℝ) (view : ℕ → Cylinder → Cylinder) (reference n : ℕ) (request referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) (x : Cylinder) (hc : 0 < velocity n) (hrequest : request n x = coefficientScale (s.epsilon n) (B.strip.epsilon reference) (velocity n) ^ 2 • referenceRequest reference (view n x)) : (B.viewCoefficients s d background frequency velocity clock normal view reference request j).amplitude n x = velocity n • (B.coefficients referenceRequest j).amplitude reference (view n x)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.view_cutoff_amplitude {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (s : WeightedClasses.StripData Cylinder) (d : LinearWaveBounds.GraphDirections Cylinder) (background : LinearWaveBounds.WaveCoefficients Cylinder) (frequency velocity clock normal : ℕ → ℝ) (view : ℕ → Cylinder → Cylinder) (reference n : ℕ) (request referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) (x : Cylinder) (hc : 0 < velocity n) (hrequest : request n x = coefficientScale (s.epsilon n) (B.strip.epsilon reference) (velocity n) ^ 2 • referenceRequest reference (view n x)) : ((B.viewCoefficients s d background frequency velocity clock normal view reference request j).withCutoff (B.viewCutoff view reference)).amplitude n x = velocity n • ((B.coefficients referenceRequest j).withCutoff B.cutoff).amplitude reference (view n x)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.view_pressure {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (s : WeightedClasses.StripData Cylinder) (d : LinearWaveBounds.GraphDirections Cylinder) (background : LinearWaveBounds.WaveCoefficients Cylinder) (frequency velocity clock normal : ℕ → ℝ) (view : ℕ → Cylinder → Cylinder) (reference n : ℕ) (request referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) (x : Cylinder) (hc : 0 < velocity n) (hK : frequency n ≠ 0) (hKr : B.base.frequency reference ≠ 0) (hs : normal n ≠ 0) (hrequest : request n x = coefficientScale (s.epsilon n) (B.strip.epsilon reference) (velocity n) ^ 2 • referenceRequest reference (view n x)) (hN : (B.viewBase background frequency view reference).normal s d n x = normal n • B.base.normal B.strip B.directions reference (view n x)) : (B.viewCoefficients s d background frequency velocity clock normal view reference request j).pressure n x = (clock n * velocity n / normal n * (B.base.frequency reference / frequency n)) • (B.coefficients referenceRequest j).pressure reference (view n x)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.view_cutoff_pressure {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (s : WeightedClasses.StripData Cylinder) (d : LinearWaveBounds.GraphDirections Cylinder) (background : LinearWaveBounds.WaveCoefficients Cylinder) (frequency velocity clock normal : ℕ → ℝ) (view : ℕ → Cylinder → Cylinder) (reference n : ℕ) (request referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) (x : Cylinder) (hc : 0 < velocity n) (hK : frequency n ≠ 0) (hKr : B.base.frequency reference ≠ 0) (hs : normal n ≠ 0) (hrequest : request n x = coefficientScale (s.epsilon n) (B.strip.epsilon reference) (velocity n) ^ 2 • referenceRequest reference (view n x)) (hN : (B.viewBase background frequency view reference).normal s d n x = normal n • B.base.normal B.strip B.directions reference (view n x)) : ((B.viewCoefficients s d background frequency velocity clock normal view reference request j).withCutoff (B.viewCutoff view reference)).pressure n x = (clock n * velocity n / normal n * (B.base.frequency reference / frequency n)) • ((B.coefficients referenceRequest j).withCutoff B.cutoff).pressure reference (view n x)

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.viewPrimaryVector {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (s : WeightedClasses.StripData Cylinder) (velocity : ℕ → ℝ) (view : ℕ → Cylinder → Cylinder) (reference : ℕ) (j : Fin 2) (n : ℕ) (x : Cylinder) : ProblemStatement.Space

View primary vector, constructed using PartitionedCovariance.amplitude.

Equations

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

theorem NavierStokes.PhysicalSignedWave.PrimaryData.view_primaryVector {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (s : WeightedClasses.StripData Cylinder) (velocity : ℕ → ℝ) (view : ℕ → Cylinder → Cylinder) (reference : ℕ) (j : Fin 2) (n : ℕ) (x : Cylinder) (hc : 0 < velocity n) : B.viewPrimaryVector s velocity view reference j n x = velocity n • B.primaryVector j reference (view n x)

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.viewPrimaryCoefficients {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (s : WeightedClasses.StripData Cylinder) (d : LinearWaveBounds.GraphDirections Cylinder) (background : LinearWaveBounds.WaveCoefficients Cylinder) (frequency velocity clock normal : ℕ → ℝ) (view : ℕ → Cylinder → Cylinder) (reference : ℕ) (j : Fin 2) : LinearWaveBounds.WaveCoefficients Cylinder

View primary coefficients, constructed using SignedWaveUpdate.homogeneousCoefficients.

Equations

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

theorem NavierStokes.PhysicalSignedWave.PrimaryData.view_primary_amplitude {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (s : WeightedClasses.StripData Cylinder) (d : LinearWaveBounds.GraphDirections Cylinder) (background : LinearWaveBounds.WaveCoefficients Cylinder) (frequency velocity clock normal : ℕ → ℝ) (view : ℕ → Cylinder → Cylinder) (reference n : ℕ) (j : Fin 2) (x : Cylinder) (hc : 0 < velocity n) : ((B.viewPrimaryCoefficients s d background frequency velocity clock normal view reference j).withCutoff (B.viewCutoff view reference)).amplitude n x = velocity n • ((B.primaryCoefficients j).withCutoff B.cutoff).amplitude reference (view n x)

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

Regularity on one reference native cell. Every entry concerns the original coordinate, target, current request, mask or phase/frame input; there is no regularity assumption on a solved wave.

• coordinate : ContDiffOn ℝ (↑⊤) (B.coordinate reference) B.strip.domain
• coordinate_mem (x : Cylinder) : x ∈ B.strip.domain → B.coordinate reference x ∈ U.carrier reference ×ˢ 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 : 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 : 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 : Cylinder) : x ∈ B.strip.domain → B.base.normal B.strip B.directions reference x ≠ 0
• normal_frame (x : Cylinder) : x ∈ B.strip.domain → 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 * (B.coordinate reference x).2)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Regular.forPrimary {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {request : ℕ → Cylinder → Vec2} {reference : ℕ} {column : Fin 2} (H : B.Regular request reference column) : B.Regular B.primaryRequest reference column

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

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Regular.fundamental_smooth {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {request : ℕ → Cylinder → Vec2} {reference : ℕ} {column : Fin 2} (H : B.Regular request reference column) (j : Fin 2) : ContDiffOn ℝ (↑⊤) (B.fundamental j reference) B.strip.domain

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Regular.cutoff_smooth {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {request : ℕ → Cylinder → Vec2} {reference : ℕ} {column : Fin 2} (H : B.Regular request reference column) : ContDiffOn ℝ (↑⊤) (B.cutoff reference) B.strip.domain

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Regular.signedScalar_smooth {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {request : ℕ → Cylinder → Vec2} {reference : ℕ} {column : Fin 2} (H : B.Regular request reference column) (j : Fin 2) : ContDiffOn ℝ (↑⊤) (SignedWaveUpdate.signedScalar B.strip B.matrix B.target request B.mask j reference) B.strip.domain

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Regular.amplitude_smooth {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {request : ℕ → Cylinder → Vec2} {reference : ℕ} {column : Fin 2} (H : B.Regular request reference column) (j : Fin 2) : ContDiffOn ℝ (↑⊤) ((B.coefficients request j).amplitude reference) B.strip.domain

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Regular.cutoff_amplitude_smooth {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {request : ℕ → Cylinder → Vec2} {reference : ℕ} {column : Fin 2} (H : B.Regular request reference column) (j : Fin 2) : ContDiffOn ℝ (↑⊤) (((B.coefficients request j).withCutoff B.cutoff).amplitude reference) B.strip.domain

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Regular.fundamental_tangent {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {request : ℕ → Cylinder → Vec2} {reference : ℕ} {column : Fin 2} (H : B.Regular request reference column) {x : Cylinder} (hx : x ∈ B.strip.domain) : inner ℝ (B.base.normal B.strip B.directions reference x) (B.fundamental column reference x) = 0

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Regular.amplitude_tangent {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {request : ℕ → Cylinder → Vec2} {reference : ℕ} {column : Fin 2} (H : B.Regular request reference column) {x : Cylinder} (hx : x ∈ B.strip.domain) : HarmonicCalculus.normalDot (B.base.normal B.strip B.directions reference x) ((B.coefficients request column).amplitude reference x) = 0

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Regular.cutoff_amplitude_tangent {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {request : ℕ → Cylinder → Vec2} {reference : ℕ} {column : Fin 2} (H : B.Regular request reference column) {x : Cylinder} (hx : x ∈ B.strip.domain) : HarmonicCalculus.normalDot (B.base.normal B.strip B.directions reference x) (((B.coefficients request column).withCutoff B.cutoff).amplitude reference x) = 0

structure NavierStokes.PhysicalSignedWave.PrimaryData.Angular {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (request : ℕ → Cylinder → Vec2) (reference : ℕ) : Type

Angular conditions concern the original phase, coordinate and scalar inputs. In particular the signed coefficient's invariance is a theorem.

• mode : ℤ

  Mode of Angular, of type ℤ.

• phase : CopyAngularInvariance.AffinePhase (0, 1) (↑self.mode / B.base.frequency reference) (B.base.phase reference)
• coordinate : CopyAngularInvariance.Invariant (0, 1) (B.coordinate reference)
• target : CopyAngularInvariance.Invariant (0, 1) (B.target reference)
• request : CopyAngularInvariance.Invariant (0, 1) (request reference)
• mask : CopyAngularInvariance.Invariant (0, 1) (B.mask reference)
• normalMotion : CopyAngularInvariance.Invariant (0, 1) (B.normalMotion reference)
• action : CopyAngularInvariance.Invariant (0, 1) (B.action reference)

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.Angular.forPrimary {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) {request : ℕ → Cylinder → Vec2} {reference : ℕ} (H : B.Angular request reference) : B.Angular B.primaryRequest reference

For primary, given by { H with request := H.target.map (fun t => (2 : ℝ) • t) }.

Equations

• NavierStokes.PhysicalSignedWave.PrimaryData.Angular.forPrimary B H = { mode := H.mode, phase := ⋯, coordinate := ⋯, target := ⋯, request := ⋯, mask := ⋯, normalMotion := ⋯, action := ⋯ }

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.periodicAngular {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (C : ReferencePhase) (request : ℕ → Cylinder → Vec2) (reference : ℕ) (hc : CopyAngularInvariance.Invariant (0, 1) (B.coordinate reference)) (hT : CopyAngularInvariance.Invariant (0, 1) (B.target reference)) (hR : CopyAngularInvariance.Invariant (0, 1) (request reference)) (hm : CopyAngularInvariance.Invariant (0, 1) (B.mask reference)) (hn : CopyAngularInvariance.Invariant (0, 1) (B.normalMotion reference)) (ha : CopyAngularInvariance.Invariant (0, 1) (B.action reference)) : (B.withReferencePhase C).Angular request reference

The angular phase and full auxiliary periodicity can be supplied by the explicit compact-clock construction, before any signed solve.

Equations

• B.periodicAngular C request reference hc hT hR hm hn ha = { mode := C.angularMode, phase := ⋯, coordinate := hc, target := hT, request := hR, mask := hm, normalMotion := hn, action := ha }

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.periodicStateAngular {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (C : ReferencePhase) (P : SignedStressPrimitive.Patch) (h : ℝ) (context : CorrectionState.Context Point) (current : CorrectionState.State Point) (reference : ℕ) (hc : CopyAngularInvariance.Invariant (0, 1) (B.coordinate reference)) (hT : CopyAngularInvariance.Invariant (0, 1) (B.target reference)) (hm : CopyAngularInvariance.Invariant (0, 1) (B.mask reference)) (hn : CopyAngularInvariance.Invariant (0, 1) (B.normalMotion reference)) (ha : CopyAngularInvariance.Invariant (0, 1) (B.action reference)) : (B.withReferencePhase C).Angular (stateRequest B.strip P h context current) reference

Periodic state angular, given by B.periodicAngular C _ reference hc hT (stateRequest_invariant B.strip P h context current reference) hm hn ha.

Equations

• B.periodicStateAngular C P h context current reference hc hT hm hn ha = B.periodicAngular C (NavierStokes.PhysicalSignedWave.stateRequest B.strip P h context current) reference hc hT ⋯ hm hn ha

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.raw {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (reference : ℕ) : Cylinder → HarmonicCalculus.ComplexVector

Raw, given by ((B.coefficients request j).withCutoff B.cutoff).amplitude reference.

Equations

• B.raw request j reference = ((B.coefficients request j).withCutoff B.cutoff).amplitude reference

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.rawPressure {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (reference : ℕ) : Cylinder → ℂ

Raw pressure, given by ((B.coefficients request j).withCutoff B.cutoff).pressure reference.

Equations

• B.rawPressure request j reference = ((B.coefficients request j).withCutoff B.cutoff).pressure reference

theorem NavierStokes.PhysicalSignedWave.PrimaryData.raw_invariant {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) {request : ℕ → Cylinder → Vec2} {reference : ℕ} (H : B.Angular request reference) (j : Fin 2) : CopyAngularInvariance.Invariant (0, 1) (B.raw request j reference)

structure NavierStokes.PhysicalSignedWave.ChartGeometry (a : LinearWaveBounds.WaveCoefficients Cylinder) (s : WeightedClasses.StripData Cylinder) (d : LinearWaveBounds.GraphDirections Cylinder) (n : ℕ) (h Q : ℝ) (cover : ℕ) : Prop

Literal background chart operators, before any wave is formed.

• radius : a.radius n = PhysicalResidualBridge.ScaledGraph.radius
• radial : d.radialField n = (PhysicalResidualBridge.commonGraph Q h cover).radial
• angular : (fun (x : PhysicalResidualBridge.Cylinder) => d.angular) = PhysicalResidualBridge.ScaledGraph.angular
• axial : d.axialField s n = (PhysicalResidualBridge.commonGraph Q h cover).axial

theorem NavierStokes.PhysicalSignedWave.ChartGeometry.normal {a : LinearWaveBounds.WaveCoefficients Cylinder} {s : WeightedClasses.StripData Cylinder} {d : LinearWaveBounds.GraphDirections Cylinder} {n cover : ℕ} {h Q : ℝ} (G : ChartGeometry a s d n h Q cover) : a.normal s d n = HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h cover).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h cover).axial (a.phase n)

theorem NavierStokes.PhysicalSignedWave.ChartGeometry.corrected_wave {a : LinearWaveBounds.WaveCoefficients Cylinder} {s : WeightedClasses.StripData Cylinder} {d : LinearWaveBounds.GraphDirections Cylinder} {n cover : ℕ} {h Q : ℝ} (G : ChartGeometry a s d n h Q cover) (cutoff : ℕ → Cylinder → ℝ) : HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((a.corrected s d cutoff).amplitude n) = HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) (CurlClassBounds.realizedCoefficient (a.frequency n) PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h cover).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h cover).axial (a.phase n) ((a.withCutoff cutoff).amplitude n))

theorem NavierStokes.PhysicalSignedWave.ChartGeometry.normal_invariant {a : LinearWaveBounds.WaveCoefficients Cylinder} {s : WeightedClasses.StripData Cylinder} {d : LinearWaveBounds.GraphDirections Cylinder} {n cover : ℕ} {h Q slope : ℝ} (G : ChartGeometry a s d n h Q cover) (hphi : CopyAngularInvariance.AffinePhase (0, 1) slope (a.phase n)) : CopyAngularInvariance.Invariant (0, 1) (a.normal s d n)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.rawPressure_invariant {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (reference : ℕ) {request : ℕ → Cylinder → Vec2} (H : B.Angular request reference) {h Q : ℝ} {cover : ℕ} (G : ChartGeometry B.base B.strip B.directions reference h Q cover) (j : Fin 2) : CopyAngularInvariance.Invariant (0, 1) (B.rawPressure request j reference)

structure NavierStokes.PhysicalSignedWave.PrimaryData.Views {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} (B : PrimaryData U) (reference : ℕ) : Type

One physical reference scale and cover for this primary column. Band backgrounds are primitive data; frequency, phase, target, pulse, cutoff, normal motion and action of each view are constructed below.

• exponent : ℝ

  Exponent of Views, of type ℝ.

• referenceScale : ℝ

  Reference scale of Views, of type ℝ.

• referenceScale_pos : 0 < self.referenceScale
• referenceCover : ℕ

  Reference cover of Views, of type ℕ.

• scale : ℕ → ℝ

  Scale of Views, of type ℕ → ℝ.

• scale_pos (n : ℕ) : 0 < self.scale n
• cover : ℕ → ℕ

  Cover of Views, of type ℕ → ℕ.

• cover_le (n : ℕ) : self.cover n ≤ self.referenceCover
• frequency : ℕ → ℝ

  Frequency of Views, of type ℕ → ℝ.

• frequency_ne (n : ℕ) : self.frequency n ≠ 0
• strip : WeightedClasses.StripData Cylinder

  Strip of Views, of type StripData Cylinder.

• directions : LinearWaveBounds.GraphDirections Cylinder

  Directions of Views, of type LinearWaveBounds.GraphDirections Cylinder.

• background : LinearWaveBounds.WaveCoefficients Cylinder

  Background of Views, of type LinearWaveBounds.WaveCoefficients Cylinder.

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.Views.map {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (n : ℕ) : Cylinder →L[ℝ] Cylinder

Map, given by PhysicalParticularWave.cylinderChange V.exponent (V.scale n) V.referenceScale (V.referenceCover - V.cover n).

Equations

• V.map n = NavierStokes.PhysicalParticularWave.cylinderChange V.exponent (V.scale n) V.referenceScale (V.referenceCover - V.cover n)

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

Velocity, given by PhysicalParticularWave.velocityWeight V.exponent (V.scale n) V.referenceScale.

Equations

• V.velocity n = NavierStokes.PhysicalParticularWave.velocityWeight V.exponent (V.scale n) V.referenceScale

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

Clock, given by PhysicalParticularWave.clockWeight V.exponent (V.scale n) V.referenceScale.

Equations

• V.clock n = NavierStokes.PhysicalParticularWave.clockWeight V.exponent (V.scale n) V.referenceScale

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

Normal, given by PhysicalParticularWave.normalWeight (V.scale n) V.referenceScale (V.frequency n) (B.base.frequency reference).

Equations

• V.normal n = NavierStokes.PhysicalParticularWave.normalWeight (V.scale n) V.referenceScale (V.frequency n) (B.base.frequency reference)

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

Coefficients, constructed using B.viewCoefficients.

Equations

• V.coefficients request j = B.viewCoefficients V.strip V.directions V.background V.frequency V.velocity V.clock V.normal (fun (n : ℕ) => ⇑(V.map n)) reference request j

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.Views.cutoff {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) : ℕ → Cylinder → ℝ

Cutoff, given by B.viewCutoff (fun n => V.map n) reference.

Equations

• V.cutoff = B.viewCutoff (fun (n : ℕ) => ⇑(V.map n)) reference

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

Exact coefficients, given by (V.coefficients request j).corrected V.strip V.directions V.cutoff.

Equations

• V.exactCoefficients request j = (V.coefficients request j).corrected V.strip V.directions V.cutoff

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.map_graph {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (n : ℕ) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) : (V.map n) ((PhysicalResidualBridge.commonGraph (V.scale n) V.exponent (V.cover n)).map z) = (PhysicalResidualBridge.commonGraph V.referenceScale V.exponent V.referenceCover).map z

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.map_fastTranslate {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (n : ℕ) (x : Cylinder) (k : TorusInverse.Frequency) : (V.map n) (fastTranslate x k) = fastTranslate ((V.map n) x) (CommonCoverSolve.coverIndex (V.referenceCover - V.cover n) k)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.phase_periodic {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (hp : ∀ (x : Cylinder) (k : TorusInverse.Frequency), B.base.phase reference (fastTranslate x k) = B.base.phase reference x) (n : ℕ) (x : Cylinder) (k : TorusInverse.Frequency) : (V.coefficients request j).phase n (fastTranslate x k) = (V.coefficients request j).phase n x

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.carrier_periodic {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (hp : ∀ (x : Cylinder) (k : TorusInverse.Frequency), B.base.phase reference (fastTranslate x k) = B.base.phase reference x) (n : ℕ) (x : Cylinder) (k : TorusInverse.Frequency) : HarmonicCalculus.carrier (V.frequency n) ((V.coefficients request j).phase n) (fastTranslate x k) = HarmonicCalculus.carrier (V.frequency n) ((V.coefficients request j).phase n) x

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.normal_transport {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (G : ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (n : ℕ) (H : 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 : 0 < x.1.1) (hΦ : DifferentiableAt ℝ (B.base.phase reference) ((V.map n) x)) : (B.viewBase V.background V.frequency (fun (n : ℕ) => ⇑(V.map n)) reference).normal V.strip V.directions n x = V.normal n • B.base.normal B.strip B.directions reference ((V.map n) x)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.amplitude_transport {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (request referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) (n : ℕ) (x : Cylinder) (hrequest : request n x = coefficientScale (V.strip.epsilon n) (B.strip.epsilon reference) (V.velocity n) ^ 2 • referenceRequest reference ((V.map n) x)) : ((V.coefficients request j).withCutoff V.cutoff).amplitude n x = V.velocity n • ((B.coefficients referenceRequest j).withCutoff B.cutoff).amplitude reference ((V.map n) x)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.pressure_transport {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (request referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) (n : ℕ) {x : Cylinder} (hx : 0 < x.1.1) (hKr : B.base.frequency reference ≠ 0) (G : ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (H : 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)) (hΦ : DifferentiableAt ℝ (B.base.phase reference) ((V.map n) x)) (hrequest : request n x = coefficientScale (V.strip.epsilon n) (B.strip.epsilon reference) (V.velocity n) ^ 2 • referenceRequest reference ((V.map n) x)) : ((V.coefficients request j).withCutoff V.cutoff).pressure n x = PhysicalParticularWave.pressureWeight V.exponent (V.scale n) V.referenceScale • ((B.coefficients referenceRequest j).withCutoff B.cutoff).pressure reference ((V.map n) x)

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.Views.physicalPhase {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) : ProblemStatement.SpaceTime → ℝ

Physical phase, defined pointwise by B.base.phase reference ((PhysicalResidualBridge.commonGraph V.referenceScale V.exponent V.referenceCover).map z).

Equations

• V.physicalPhase z = B.base.phase reference ((NavierStokes.PhysicalResidualBridge.commonGraph V.referenceScale V.exponent V.referenceCover).map z)

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.Views.physicalRaw {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector

Physical raw as an element of SpaceTime → ComplexVector.

Equations

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

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.Views.referencePotential {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector

Reference potential, given by PhysicalCurlCovariance.referencePotential (B.base.frequency reference) V.physicalPhase (V.physicalRaw referenceRequest j).

Equations

• V.referencePotential referenceRequest j = NavierStokes.PhysicalCurlCovariance.referencePotential (B.base.frequency reference) V.physicalPhase (V.physicalRaw referenceRequest j)

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.Views.physicalPotential {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) (delta : ℝ) : ProblemStatement.VelocityField

One Cartesian potential is chosen from the reference band and cover, and each actual band wave will be identified with its curl.

Equations

• V.physicalPotential referenceRequest j delta = NavierStokes.PhysicalCurlCovariance.globalCartesianPotential delta (V.referencePotential referenceRequest j)

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.Views.physicalVelocity {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) (delta : ℝ) : ProblemStatement.VelocityField

Physical velocity, given by SpatialCurl.spatialCurl (V.physicalPotential referenceRequest j delta).

Equations

• V.physicalVelocity referenceRequest j delta = NavierStokes.SpatialCurl.spatialCurl (V.physicalPotential referenceRequest j delta)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.physicalGraph_add_angle {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (z : ProblemStatement.SpaceTime) (t : ℝ) : (PhysicalResidualBridge.commonGraph V.referenceScale V.exponent V.referenceCover).map (z + t • (0, ProblemStatement.coordinateVector 1)) = (PhysicalResidualBridge.commonGraph V.referenceScale V.exponent V.referenceCover).map z + t • (0, 1)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.referencePotential_periodic {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) {referenceRequest : ℕ → Cylinder → Vec2} (H : B.Angular referenceRequest reference) (hK : B.base.frequency reference ≠ 0) (j : Fin 2) (t r z : ℝ) : Function.Periodic (fun (angle : ℝ) => V.referencePotential referenceRequest j (t, AxisymmetricResidual.pack r angle z)) (2 * Real.pi)

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

Wave, constructed using vectorMode.

Equations

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

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.wave_eq_exact {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (n : ℕ) (H : 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)) : V.wave request j n = HarmonicCalculus.vectorMode ((V.exactCoefficients request j).frequency n) ((V.exactCoefficients request j).phase n) ((V.exactCoefficients request j).amplitude n)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.wave_physical {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (request referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) (n : ℕ) (R : B.Regular referenceRequest reference j) (A : B.Angular referenceRequest reference) (hK : B.base.frequency reference ≠ 0) (G : ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (H : 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) (hrequest : ∀ x ∈ V.strip.domain, request n x = coefficientScale (V.strip.epsilon n) (B.strip.epsilon reference) (V.velocity n) ^ 2 • referenceRequest reference ((V.map n) x)) {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) : (V.wave request j 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)) (V.physicalVelocity referenceRequest j delta (z.1, CylindricalResidual.chart z.2))).ofLp component

The output is one literal Cartesian curl. All phase and amplitude identities used by the curl theorem are derived from the constructors.

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.referencePotential_smoothAt {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) (R : B.Regular referenceRequest reference j) (hK : B.base.frequency reference ≠ 0) (G : ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (hradius : ∀ x ∈ B.strip.domain, 0 < x.1.1) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hx : (PhysicalResidualBridge.commonGraph V.referenceScale V.exponent V.referenceCover).map z ∈ B.strip.domain) : ContDiffAt ℝ (↑⊤) (V.referencePotential referenceRequest j) z

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.physicalPotential_smoothAt {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) (R : B.Regular referenceRequest reference j) (A : B.Angular referenceRequest reference) (hK : B.base.frequency reference ≠ 0) (G : ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (hradius : ∀ x ∈ B.strip.domain, 0 < x.1.1) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hx : (PhysicalResidualBridge.commonGraph V.referenceScale V.exponent V.referenceCover).map z ∈ B.strip.domain) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : ContDiffAt ℝ (↑⊤) (V.physicalPotential referenceRequest j delta) (z.1, CylindricalResidual.chart z.2)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.physicalVelocity_divergence {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) (R : B.Regular referenceRequest reference j) (A : B.Angular referenceRequest reference) (hK : B.base.frequency reference ≠ 0) (G : ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (hradius : ∀ x ∈ B.strip.domain, 0 < x.1.1) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hx : (PhysicalResidualBridge.commonGraph V.referenceScale V.exponent V.referenceCover).map z ∈ B.strip.domain) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : ProblemStatement.spatialDivergence (V.physicalVelocity referenceRequest j delta) z.1 (CylindricalResidual.chart z.2) = 0

Pressure is transported from the same reference coefficient

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.Views.physicalPressureCoefficient {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) : ProblemStatement.SpaceTime → ℂ

Physical pressure coefficient as an element of SpaceTime → ℂ.

Equations

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

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.Views.complexPhysicalPressure {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) : ProblemStatement.SpaceTime → ℂ

Complex physical pressure, given by mode (B.base.frequency reference) V.physicalPhase (V.physicalPressureCoefficient referenceRequest j).

Equations

• V.complexPhysicalPressure referenceRequest j = NavierStokes.HarmonicCalculus.mode (B.base.frequency reference) V.physicalPhase (V.physicalPressureCoefficient referenceRequest j)

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.Views.physicalPressure {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) (delta : ℝ) : ProblemStatement.PressureField

Physical pressure as an element of PressureField.

Equations

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

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

Pressure mode, given by mode (V.frequency n) ((V.coefficients request j).phase n) (((V.coefficients request j).withCutoff V.cutoff).pressure n).

Equations

• V.pressureMode request j n = NavierStokes.HarmonicCalculus.mode (V.frequency n) ((V.coefficients request j).phase n) (((V.coefficients request j).withCutoff V.cutoff).pressure n)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.complexPhysicalPressure_periodic {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) {referenceRequest : ℕ → Cylinder → Vec2} (A : B.Angular referenceRequest reference) (hK : B.base.frequency reference ≠ 0) (G : ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (j : Fin 2) (t r z : ℝ) : Function.Periodic (fun (angle : ℝ) => V.complexPhysicalPressure referenceRequest j (t, AxisymmetricResidual.pack r angle z)) (2 * Real.pi)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.physicalPressure_forward {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) {referenceRequest : ℕ → Cylinder → Vec2} (A : B.Angular referenceRequest reference) (hK : B.base.frequency reference ≠ 0) (G : ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (j : Fin 2) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hz : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : V.physicalPressure referenceRequest j delta (z.1, CylindricalResidual.chart z.2) = (V.complexPhysicalPressure referenceRequest j z).re

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.pressureMode_physical {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (request referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) (n : ℕ) (hK : B.base.frequency reference ≠ 0) (G : ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (H : 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)) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hPhi : DifferentiableAt ℝ (B.base.phase reference) ((PhysicalResidualBridge.commonGraph V.referenceScale V.exponent V.referenceCover).map z)) (hrequest : request n ((PhysicalResidualBridge.commonGraph (V.scale n) V.exponent (V.cover n)).map z) = coefficientScale (V.strip.epsilon n) (B.strip.epsilon reference) (V.velocity n) ^ 2 • referenceRequest reference ((PhysicalResidualBridge.commonGraph V.referenceScale V.exponent V.referenceCover).map z)) : V.pressureMode request j n ((PhysicalResidualBridge.commonGraph (V.scale n) V.exponent (V.cover n)).map z) = V.scale n ^ (2 * CoordinateAlgebra.A V.exponent) • V.complexPhysicalPressure referenceRequest j z

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.pressure_physical {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (request referenceRequest : ℕ → Cylinder → Vec2) (j : Fin 2) (n : ℕ) (A : B.Angular referenceRequest reference) (hK : B.base.frequency reference ≠ 0) (G : ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (H : 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)) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hPhi : DifferentiableAt ℝ (B.base.phase reference) ((PhysicalResidualBridge.commonGraph V.referenceScale V.exponent V.referenceCover).map z)) (hrequest : request n ((PhysicalResidualBridge.commonGraph (V.scale n) V.exponent (V.cover n)).map z) = coefficientScale (V.strip.epsilon n) (B.strip.epsilon reference) (V.velocity n) ^ 2 • referenceRequest reference ((PhysicalResidualBridge.commonGraph V.referenceScale V.exponent V.referenceCover).map z)) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : (V.pressureMode request j n ((PhysicalResidualBridge.commonGraph (V.scale n) V.exponent (V.cover n)).map z)).re = V.scale n ^ (2 * CoordinateAlgebra.A V.exponent) * V.physicalPressure referenceRequest j delta (z.1, CylindricalResidual.chart z.2)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.pressureMode_eq_exact {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (request : ℕ → Cylinder → Vec2) (j : Fin 2) (n : ℕ) : V.pressureMode request j n = HarmonicCalculus.mode ((V.exactCoefficients request j).frequency n) ((V.exactCoefficients request j).phase n) ((V.exactCoefficients request j).pressure n)

The primary coefficient is an exact specialization

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.Views.primaryRequest {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) : ℕ → Cylinder → Vec2

Primary request, defined pointwise by (2 : ℝ) • B.viewTarget V.strip V.velocity (fun n => V.map n) reference n x.

Equations

• V.primaryRequest n x = 2 • B.viewTarget V.strip V.velocity (fun (n : ℕ) => ⇑(V.map n)) reference n x

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.Views.primaryCoefficients {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (j : Fin 2) : LinearWaveBounds.WaveCoefficients Cylinder

Primary coefficients, given by B.viewPrimaryCoefficients V.strip V.directions V.background V.frequency V.velocity V.clock V.normal (fun n => V.map n) reference j.

Equations

• V.primaryCoefficients j = B.viewPrimaryCoefficients V.strip V.directions V.background V.frequency V.velocity V.clock V.normal (fun (n : ℕ) => ⇑(V.map n)) reference j

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.Views.primaryExactCoefficients {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (j : Fin 2) : LinearWaveBounds.WaveCoefficients Cylinder

Primary exact coefficients, given by (V.primaryCoefficients j).corrected V.strip V.directions V.cutoff.

Equations

• V.primaryExactCoefficients j = (V.primaryCoefficients j).corrected V.strip V.directions V.cutoff

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.primaryCoefficients_eq_signed {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (j : Fin 2) : V.primaryCoefficients j = V.coefficients V.primaryRequest j

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.primaryRequest_transport {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) (n : ℕ) (x : Cylinder) : V.primaryRequest n x = coefficientScale (V.strip.epsilon n) (B.strip.epsilon reference) (V.velocity n) ^ 2 • B.primaryRequest reference ((V.map n) x)

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

Primary physical potential, given by V.physicalPotential B.primaryRequest j delta.

Equations

• V.primaryPhysicalPotential delta j = V.physicalPotential B.primaryRequest j delta

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

Primary physical velocity, given by SpatialCurl.spatialCurl (V.primaryPhysicalPotential delta j).

Equations

• V.primaryPhysicalVelocity delta j = NavierStokes.SpatialCurl.spatialCurl (V.primaryPhysicalPotential delta j)

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

Primary physical pressure, given by V.physicalPressure B.primaryRequest j delta.

Equations

• V.primaryPhysicalPressure delta j = V.physicalPressure B.primaryRequest j delta

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.primary_wave_physical {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) {request : ℕ → Cylinder → Vec2} (j : Fin 2) (n : ℕ) (R : B.Regular request reference j) (A : B.Angular request reference) (hK : B.base.frequency reference ≠ 0) (G : ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (H : 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 ((V.primaryExactCoefficients j).frequency n) ((V.primaryExactCoefficients j).phase n) ((V.primaryExactCoefficients j).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)) (V.primaryPhysicalVelocity delta j (z.1, CylindricalResidual.chart z.2))).ofLp component

The primary statement uses its actual square-root coefficient and the same once-cutoff curl correction as the signed update.

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.primary_pressure_physical {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) {request : ℕ → Cylinder → Vec2} (j : Fin 2) (n : ℕ) (R : B.Regular request reference j) (A : B.Angular request reference) (hK : B.base.frequency reference ≠ 0) (G : ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (H : 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)) {z : ProblemStatement.SpaceTime} (hz : 0 < z.2.ofLp 0) (hx : (PhysicalResidualBridge.commonGraph V.referenceScale V.exponent V.referenceCover).map z ∈ B.strip.domain) {delta : ℝ} (hdelta : 0 < delta) (chart : PolarCharts.Index) (hchart : z ∈ PhysicalCurlCovariance.validCylindrical delta chart) : (HarmonicCalculus.mode ((V.primaryExactCoefficients j).frequency n) ((V.primaryExactCoefficients j).phase n) ((V.primaryExactCoefficients j).pressure n) ((PhysicalResidualBridge.commonGraph (V.scale n) V.exponent (V.cover n)).map z)).re = V.scale n ^ (2 * CoordinateAlgebra.A V.exponent) * V.primaryPhysicalPressure delta j (z.1, CylindricalResidual.chart z.2)

Bind the constructor to the literal current-state request

structure NavierStokes.PhysicalSignedWave.PrimaryData.Views.StateData {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} (V : B.Views reference) : Type

All coherence fields concern the current state, background and integration domain before the signed wave is constructed.

• patch : SignedStressPrimitive.Patch

  Patch of StateData, of type SignedStressPrimitive.Patch.

• context : CorrectionState.Context Point

  Context of StateData, of type CorrectionState.Context Point.

• referenceContext : CorrectionState.Context Point

  Reference context of StateData, of type CorrectionState.Context Point.

• current : CorrectionState.State Point

  Current of StateData, of type CorrectionState.State Point.

• referenceState : CorrectionState.State Point

  Reference state of StateData, of type CorrectionState.State Point.

• exponent_pos : 0 < V.exponent
• exponent_lt_half : V.exponent < 1 / 2
• domain : ℕ → Set Point

  Domain of StateData, of type ℕ → Set Point.

• domain_open (n : ℕ) : IsOpen (self.domain n)
• state_coherent (n : ℕ) : PhysicalResidualNaturality.StateOn (self.domain n) (requestChart V.exponent ⋯ ⋯ (V.referenceCover - V.cover n)) (V.velocity n) (PhysicalParticularWave.ratioPower (V.scale n) V.referenceScale (1 / 2)) self.current self.referenceState n reference
• context_coherent (n : ℕ) : PhysicalResidualNaturality.ContextOn (self.domain n) (requestChart V.exponent ⋯ ⋯ (V.referenceCover - V.cover n)) (V.velocity n) (PhysicalParticularWave.ratioPower (V.scale n) V.referenceScale (1 / 2)) self.context self.referenceContext n reference
• time_pos (x : Cylinder) : x ∈ V.strip.domain → 0 < x.1.2.1.2
• fibers (n : ℕ) (x : Cylinder) : x ∈ V.strip.domain → ∀ (r : ℝ) (Y : PressureStream.Plane), (r, (x.1.2.1.2, x.1.2.1.1), Y) ∈ self.domain n
• referenceSlow : ℕ → Set LocalSignedRequest.Plane

  Reference slow of StateData, of type ℕ → Set LocalSignedRequest.Plane.

• referenceSlow_open (n : ℕ) : IsOpen (self.referenceSlow n)
• referenceSlow_mem (n : ℕ) (x : Cylinder) : x ∈ V.strip.domain → (slowChange V.exponent (V.scale n) V.referenceScale) (x.1.2.1.2, x.1.2.1.1) ∈ self.referenceSlow n
• reference_theta_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (self.referenceState.thetaResidual self.referenceContext reference) (PhysicalMeanDomain.slowDomain (self.referenceSlow n))
• reference_axial_smooth (n : ℕ) : ContDiffOn ℝ (↑⊤) (self.referenceState.axialResidual self.referenceContext reference) (PhysicalMeanDomain.slowDomain (self.referenceSlow n))
• reference_theta_periodic (n : ℕ) : PhysicalMeanDomain.PeriodicOn (self.referenceSlow n) (self.referenceState.thetaResidual self.referenceContext reference)
• reference_axial_periodic (n : ℕ) : PhysicalMeanDomain.PeriodicOn (self.referenceSlow n) (self.referenceState.axialResidual self.referenceContext reference)

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.Views.StateData.request {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} {V : B.Views reference} (D : V.StateData) : ℕ → Cylinder → Vec2

Request, given by stateRequest V.strip D.patch V.exponent D.context D.current.

Equations

• D.request = NavierStokes.PhysicalSignedWave.stateRequest V.strip D.patch V.exponent D.context D.current

noncomputable def NavierStokes.PhysicalSignedWave.PrimaryData.Views.StateData.referenceRequest {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} {V : B.Views reference} (D : V.StateData) : ℕ → Cylinder → Vec2

Reference request, given by stateRequest B.strip D.patch V.exponent D.referenceContext D.referenceState.

Equations

• D.referenceRequest = NavierStokes.PhysicalSignedWave.stateRequest B.strip D.patch V.exponent D.referenceContext D.referenceState

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.StateData.request_transport {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} {V : B.Views reference} (D : V.StateData) (n : ℕ) (x : Cylinder) (hx : x ∈ V.strip.domain) : D.request n x = coefficientScale (V.strip.epsilon n) (B.strip.epsilon reference) (V.velocity n) ^ 2 • D.referenceRequest reference ((V.map n) x)

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.StateData.actual_wave_physical {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} {V : B.Views reference} (D : V.StateData) (j : Fin 2) (n : ℕ) (R : B.Regular D.referenceRequest reference j) (A : B.Angular D.referenceRequest reference) (hK : B.base.frequency reference ≠ 0) (G : ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (H : 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 ((V.exactCoefficients D.request j).frequency n) ((V.exactCoefficients D.request j).phase n) ((V.exactCoefficients D.request j).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)) (V.physicalVelocity D.referenceRequest j delta (z.1, CylindricalResidual.chart z.2))).ofLp component

theorem NavierStokes.PhysicalSignedWave.PrimaryData.Views.StateData.actual_pressure_physical {U : PhaseJetBounds.Domain ℕ PhaseCalculus.Slow} {B : PrimaryData U} {reference : ℕ} {V : B.Views reference} (D : V.StateData) (j : Fin 2) (n : ℕ) (R : B.Regular D.referenceRequest reference j) (A : B.Angular D.referenceRequest reference) (hK : B.base.frequency reference ≠ 0) (G : ChartGeometry B.base B.strip B.directions reference V.exponent V.referenceScale V.referenceCover) (H : 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 ((V.exactCoefficients D.request j).frequency n) ((V.exactCoefficients D.request j).phase n) ((V.exactCoefficients D.request j).pressure n) ((PhysicalResidualBridge.commonGraph (V.scale n) V.exponent (V.cover n)).map z)).re = V.scale n ^ (2 * CoordinateAlgebra.A V.exponent) * V.physicalPressure D.referenceRequest j delta (z.1, CylindricalResidual.chart z.2)