Physical covariance of the actual wave curl

The potential is differentiated before any cutoff or carrier is removed. All operators below are actual Frechet derivatives.

@[reducible, inline]

abbrev NavierStokes.PhysicalCurlCovariance.Cylinder : Type

Cylinder: an abbreviation for PhysicalResidualBridge.Cylinder.

Equations

• NavierStokes.PhysicalCurlCovariance.Cylinder = NavierStokes.PhysicalResidualBridge.Cylinder

@[reducible, inline]

abbrev NavierStokes.PhysicalCurlCovariance.ScaledGraph : Type

Scaled graph: an abbreviation for PhysicalResidualBridge.ScaledGraph.

Equations

• NavierStokes.PhysicalCurlCovariance.ScaledGraph = NavierStokes.PhysicalResidualBridge.ScaledGraph

noncomputable def NavierStokes.PhysicalCurlCovariance.realVector (a : HarmonicCalculus.ComplexVector) : ProblemStatement.Space

Real vector, given by AxisymmetricResidual.pack (a 0).re (a 1).re (a 2).re.

Equations

• NavierStokes.PhysicalCurlCovariance.realVector a = NavierStokes.AxisymmetricResidual.pack (a 0).re (a 1).re (a 2).re

@[simp]

theorem NavierStokes.PhysicalCurlCovariance.realVector_apply (a : HarmonicCalculus.ComplexVector) (i : Fin 3) : (realVector a).ofLp i = (a i).re

noncomputable def NavierStokes.PhysicalCurlCovariance.realCurl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (a : E → Fin 3 → ℝ) (x : E) : Fin 3 → ℝ

Real curl as an element of Fin 3 → ℝ.

Equations

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

theorem NavierStokes.PhysicalCurlCovariance.real_cylindricalCurl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) {a : E → HarmonicCalculus.ComplexVector} {x : E} (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => a y i) x) (i : Fin 3) : (CurlClassBounds.cylindricalCurl R Vr Vθ Vz a x i).re = realCurl R Vr Vθ Vz (fun (y : E) (j : Fin 3) => (a y j).re) x i

theorem NavierStokes.PhysicalCurlCovariance.curlLinear_rotation (L : ProblemStatement.Space →L[ℝ] ProblemStatement.Space) (θ : ℝ) : (CylindricalResidual.frame (-θ)) (SpatialCurl.curlLinear L) = SpatialCurl.curlLinear (CylindricalResidual.frame (-θ) ∘SL L ∘SL CylindricalResidual.frame θ)

Curl, like its underlying alternating tensor, rotates with an oriented orthonormal cylindrical frame.

noncomputable def NavierStokes.PhysicalCurlCovariance.cylindricalSpatialCurl (a : ProblemStatement.Space → ProblemStatement.Space) (q : ProblemStatement.Space) : ProblemStatement.Space

Cylindrical spatial curl, constructed using AxisymmetricResidual.pack.

Equations

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

theorem NavierStokes.PhysicalCurlCovariance.cartesianCurl_components {a : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} (ha : DifferentiableAt ℝ a (CylindricalResidual.chart q)) (hr : q.ofLp 0 ≠ 0) : (CylindricalResidual.frame (-q.ofLp 1)) (SpatialCurl.curl a (CylindricalResidual.chart q)) = cylindricalSpatialCurl (CylindricalResidual.components a) q

The moving-frame connection term is part of the genuine Cartesian curl.

theorem NavierStokes.PhysicalCurlCovariance.along_complex_pull {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Γ : E → F} {V : E → E} {W : F → F} {f : F → ℂ} {x : E} (c : ℂ) (k : ℝ) (hΓ : DifferentiableAt ℝ Γ x) (hf : DifferentiableAt ℝ f (Γ x)) (hV : (fderiv ℝ Γ x) (V x) = k • W (Γ x)) : HarmonicCalculus.along V (fun (y : E) => c * f (Γ y)) x = c * ↑k * HarmonicCalculus.along W f (Γ x)

theorem NavierStokes.PhysicalCurlCovariance.cylindricalCurl_pull {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Γ : E → F} {R : F → ℝ} {r : E → ℝ} {Vr Vθ Vz : F → F} {Sr Sθ Sz : E → E} {x : E} {l : ℝ} (hl : l ≠ 0) (hr : r x ≠ 0) (hΓ : DifferentiableAt ℝ Γ x) (hDr : (fderiv ℝ Γ x) (Sr x) = l • Vr (Γ x)) (hDθ : (fderiv ℝ Γ x) (Sθ x) = Vθ (Γ x)) (hDz : (fderiv ℝ Γ x) (Sz x) = l • Vz (Γ x)) (hR : R (Γ x) = l * r x) {a : F → HarmonicCalculus.ComplexVector} (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : F) => a y i) (Γ x)) (c : ℂ) : CurlClassBounds.cylindricalCurl r Sr Sθ Sz (fun (y : E) => c • a (Γ y)) x = (c * ↑l) • CurlClassBounds.cylindricalCurl R Vr Vθ Vz a (Γ x)

theorem NavierStokes.PhysicalCurlCovariance.phaseNormal_pull {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Γ : E → F} {R : F → ℝ} {r : E → ℝ} {Vr Vθ Vz : F → F} {Sr Sθ Sz : E → E} {x : E} {l : ℝ} (hl : l ≠ 0) (hr : r x ≠ 0) (hΓ : DifferentiableAt ℝ Γ x) (hDr : (fderiv ℝ Γ x) (Sr x) = l • Vr (Γ x)) (hDθ : (fderiv ℝ Γ x) (Sθ x) = Vθ (Γ x)) (hDz : (fderiv ℝ Γ x) (Sz x) = l • Vz (Γ x)) (hR : R (Γ x) = l * r x) {Φ : F → ℝ} (hΦ : DifferentiableAt ℝ Φ (Γ x)) (b : ℝ) : HarmonicCalculus.phaseNormal r Sr Sθ Sz (fun (y : E) => b * Φ (Γ y)) x = (b * l) • HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ (Γ x)

theorem NavierStokes.PhysicalCurlCovariance.normalCoefficient_scale (n : ProblemStatement.Space) (a : HarmonicCalculus.ComplexVector) {s : ℝ} (hs : s ≠ 0) (c : ℝ) : CurlClassBounds.normalCoefficient (s • n) (c • a) = (c / s) • CurlClassBounds.normalCoefficient n a

theorem NavierStokes.PhysicalCurlCovariance.carrier_eq_of_products {E : Type u_1} {F : Type u_2} {K L : ℝ} {Φ : E → ℝ} {Ψ : F → ℝ} {x : E} {y : F} (h : K * Φ x = L * Ψ y) : HarmonicCalculus.carrier K Φ x = HarmonicCalculus.carrier L Ψ y

theorem NavierStokes.PhysicalCurlCovariance.vectorPotential_pull {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Γ : E → F} {R : F → ℝ} {r : E → ℝ} {Vr Vθ Vz : F → F} {Sr Sθ Sz : E → E} {x : E} {l b K L : ℝ} (hl : l ≠ 0) (hr : r x ≠ 0) (hK : K ≠ 0) (hb : b ≠ 0) (hKL : K * b = L) (hΓ : DifferentiableAt ℝ Γ x) (hDr : (fderiv ℝ Γ x) (Sr x) = l • Vr (Γ x)) (hDθ : (fderiv ℝ Γ x) (Sθ x) = Vθ (Γ x)) (hDz : (fderiv ℝ Γ x) (Sz x) = l • Vz (Γ x)) (hR : R (Γ x) = l * r x) {Φ : F → ℝ} (hΦ : DifferentiableAt ℝ Φ (Γ x)) (a : F → HarmonicCalculus.ComplexVector) (c : ℝ) : CurlClassBounds.vectorPotential K r Sr Sθ Sz (fun (y : E) => b * Φ (Γ y)) (fun (y : E) => c • a (Γ y)) x = (c / l) • CurlClassBounds.vectorPotential L R Vr Vθ Vz Φ a (Γ x)

The phase rescaling and inverse carrier cancel exactly. This is why the potential has one fewer inverse length than the velocity.

theorem NavierStokes.PhysicalCurlCovariance.realCurl_eq_cylindrical {a : ProblemStatement.VelocityField} {t : ℝ} {q : ProblemStatement.Space} (ha : DifferentiableAt ℝ a (t, q)) (i : Fin 3) : realCurl LinearWaveResidual.coordinateRadius (LinearWaveResidual.spaceDirection 0) (LinearWaveResidual.spaceDirection 1) (LinearWaveResidual.spaceDirection 2) (fun (z : ProblemStatement.SpaceTime) (j : Fin 3) => (a z).ofLp j) (t, q) i = (cylindricalSpatialCurl (fun (y : ProblemStatement.Space) => a (t, y)) q).ofLp i

theorem NavierStokes.PhysicalCurlCovariance.cylindricalSpatialCurl_congr {a b : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} (hab : a =ᶠ[nhds q] b) : cylindricalSpatialCurl a q = cylindricalSpatialCurl b q

theorem NavierStokes.PhysicalCurlCovariance.curl_of_representation {A w : ProblemStatement.VelocityField} {t : ℝ} {q : ProblemStatement.Space} (hA : DifferentiableAt ℝ A (t, CylindricalResidual.chart q)) (hw : DifferentiableAt ℝ w (t, q)) (hr : q.ofLp 0 ≠ 0) (hrep : (fun (z : ProblemStatement.SpaceTime) => A (z.1, CylindricalResidual.chart z.2)) =ᶠ[nhds (t, q)] fun (z : ℝ × ProblemStatement.Space) => (CylindricalResidual.frame (z.2.ofLp 1)) (w z)) (i : Fin 3) : ((CylindricalResidual.frame (-q.ofLp 1)) (SpatialCurl.spatialCurl A (t, CylindricalResidual.chart q))).ofLp i = realCurl LinearWaveResidual.coordinateRadius (LinearWaveResidual.spaceDirection 0) (LinearWaveResidual.spaceDirection 1) (LinearWaveResidual.spaceDirection 2) (fun (z : ProblemStatement.SpaceTime) (j : Fin 3) => (w z).ofLp j) (t, q) i

A potential value identity gives its physical curl identity by the actual chain rule. It is not necessary to assume matching velocity fields.

theorem NavierStokes.PhysicalCurlCovariance.realVector_differentiableAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : E → HarmonicCalculus.ComplexVector} {x : E} (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => a y i) x) : DifferentiableAt ℝ (fun (y : E) => realVector (a y)) x

noncomputable def NavierStokes.PhysicalCurlCovariance.ScaledGraph.complexPotential (G : ScaledGraph) (c : ℝ) (B : Cylinder → HarmonicCalculus.ComplexVector) (z : ProblemStatement.SpaceTime) : HarmonicCalculus.ComplexVector

Complex potential, given by (c : ℂ) • B (G.map z).

Equations

• G.complexPotential c B z = ↑c • B (NavierStokes.PhysicalResidualBridge.ScaledGraph.map G z)

noncomputable def NavierStokes.PhysicalCurlCovariance.ScaledGraph.realPotential (G : ScaledGraph) (c : ℝ) (B : Cylinder → HarmonicCalculus.ComplexVector) : ProblemStatement.VelocityField

Real potential, defined pointwise by realVector (complexPotential G c B z).

Equations

• G.realPotential c B z = NavierStokes.PhysicalCurlCovariance.realVector (G.complexPotential c B z)

theorem NavierStokes.PhysicalCurlCovariance.ScaledGraph.complexPotential_differentiableAt (G : ScaledGraph) {z : ProblemStatement.SpaceTime} (hr : G.radialScale * z.2.ofLp 0 ≠ 0) {B : Cylinder → HarmonicCalculus.ComplexVector} (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : Cylinder) => B y i) (PhysicalResidualBridge.ScaledGraph.map G z)) (c : ℝ) (i : Fin 3) : DifferentiableAt ℝ (fun (y : ProblemStatement.SpaceTime) => G.complexPotential c B y i) z

theorem NavierStokes.PhysicalCurlCovariance.ScaledGraph.physical_curl (G : ScaledGraph) (hl : 0 < G.radialScale) {B : Cylinder → HarmonicCalculus.ComplexVector} {t : ℝ} {q : ProblemStatement.Space} (hr : 0 < q.ofLp 0) (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : Cylinder) => B y i) (PhysicalResidualBridge.ScaledGraph.map G (t, q))) (c : ℝ) {A : ProblemStatement.VelocityField} (hA : DifferentiableAt ℝ A (t, CylindricalResidual.chart q)) (hrep : (fun (z : ProblemStatement.SpaceTime) => A (z.1, CylindricalResidual.chart z.2)) =ᶠ[nhds (t, q)] fun (z : ℝ × ProblemStatement.Space) => (CylindricalResidual.frame (z.2.ofLp 1)) (G.realPotential c B z)) (i : Fin 3) : ((CylindricalResidual.frame (-q.ofLp 1)) (SpatialCurl.spatialCurl A (t, CylindricalResidual.chart q))).ofLp i = c * G.radialScale * (CurlClassBounds.cylindricalCurl PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.ScaledGraph.radial G) PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.ScaledGraph.axial G) B (PhysicalResidualBridge.ScaledGraph.map G (t, q)) i).re

Coordinate reassociation and smooth cutoffs.

noncomputable def NavierStokes.PhysicalCurlCovariance.reindexVector {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃L[ℝ] F) (V : F → F) (x : E) : E

Reindex vector, given by e.symm (V (e x)).

Equations

• NavierStokes.PhysicalCurlCovariance.reindexVector e V x = e.symm (V (e x))

theorem NavierStokes.PhysicalCurlCovariance.along_reindex {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃L[ℝ] F) (V : F → F) {W : Type u_3} [NormedAddCommGroup W] [NormedSpace ℝ W] {f : F → W} {x : E} (hf : DifferentiableAt ℝ f (e x)) : HarmonicCalculus.along (reindexVector e V) (fun (y : E) => f (e y)) x = HarmonicCalculus.along V f (e x)

theorem NavierStokes.PhysicalCurlCovariance.cylindricalCurl_reindex {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃L[ℝ] F) (R : F → ℝ) (Vr Vθ Vz : F → F) {B : F → HarmonicCalculus.ComplexVector} {x : E} (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : F) => B y i) (e x)) : CurlClassBounds.cylindricalCurl (fun (y : E) => R (e y)) (reindexVector e Vr) (reindexVector e Vθ) (reindexVector e Vz) (fun (y : E) => B (e y)) x = CurlClassBounds.cylindricalCurl R Vr Vθ Vz B (e x)

theorem NavierStokes.PhysicalCurlCovariance.phaseNormal_reindex {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃L[ℝ] F) (R : F → ℝ) (Vr Vθ Vz : F → F) {Φ : F → ℝ} {x : E} (hΦ : DifferentiableAt ℝ Φ (e x)) : HarmonicCalculus.phaseNormal (fun (y : E) => R (e y)) (reindexVector e Vr) (reindexVector e Vθ) (reindexVector e Vz) (fun (y : E) => Φ (e y)) x = HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ (e x)

theorem NavierStokes.PhysicalCurlCovariance.vectorPotential_reindex {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃L[ℝ] F) (K : ℝ) (R : F → ℝ) (Vr Vθ Vz : F → F) {Φ : F → ℝ} (a : F → HarmonicCalculus.ComplexVector) {x : E} (hΦ : DifferentiableAt ℝ Φ (e x)) : CurlClassBounds.vectorPotential K (fun (y : E) => R (e y)) (reindexVector e Vr) (reindexVector e Vθ) (reindexVector e Vz) (fun (y : E) => Φ (e y)) (fun (y : E) => a (e y)) x = CurlClassBounds.vectorPotential K R Vr Vθ Vz Φ a (e x)

theorem NavierStokes.PhysicalCurlCovariance.cylindricalCurl_cutoff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) {χ : E → ℝ} {B : E → HarmonicCalculus.ComplexVector} {x : E} (hχ : DifferentiableAt ℝ χ x) (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => B y i) x) : CurlClassBounds.cylindricalCurl R Vr Vθ Vz (fun (y : E) => χ y • B y) x = χ x • CurlClassBounds.cylindricalCurl R Vr Vθ Vz B x + CurlClassBounds.normalCross (HarmonicCalculus.phaseNormal R Vr Vθ Vz χ x) (B x)

Cutoff differentiation produces the full gradient-cross-potential term.

theorem NavierStokes.PhysicalCurlCovariance.vectorPotential_cutoff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ℝ) (R : E → ℝ) (Vr Vθ Vz : E → E) (Φ : E → ℝ) (a : E → HarmonicCalculus.ComplexVector) (χ : E → ℝ) (x : E) : CurlClassBounds.vectorPotential K R Vr Vθ Vz Φ (fun (y : E) => χ y • a y) x = χ x • CurlClassBounds.vectorPotential K R Vr Vθ Vz Φ a x

theorem NavierStokes.PhysicalCurlCovariance.cylindricalCurl_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {R : E → ℝ} {Vr Vθ Vz : E → E} {A B : E → HarmonicCalculus.ComplexVector} {x : E} (hAB : A =ᶠ[nhds x] B) : CurlClassBounds.cylindricalCurl R Vr Vθ Vz A x = CurlClassBounds.cylindricalCurl R Vr Vθ Vz B x

A local equality of the full potentials, including their cutoffs and carriers, automatically propagates to equality of actual curls.

noncomputable def NavierStokes.PhysicalCurlCovariance.radiusCLM : Cylinder →L[ℝ] ℝ

Radius continuous linear map as an element of Cylinder →L[ℝ] ℝ.

Equations

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

noncomputable def NavierStokes.PhysicalCurlCovariance.ScaledGraph.radialCurve (G : ScaledGraph) (r : ℝ) : Cylinder

Radial curve, given by ((1, ((0, 0), (G.frequency * GraphCalculus.radialSpeed G.exponent r) • G.radialVector)), 0).

Equations

• G.radialCurve r = ((1, (0, 0), (G.frequency * NavierStokes.GraphCalculus.radialSpeed G.exponent r) • G.radialVector), 0)

theorem NavierStokes.PhysicalCurlCovariance.ScaledGraph.radialCurve_smoothAt (G : ScaledGraph) {r : ℝ} (hr : r ≠ 0) : ContDiffAt ℝ (↑⊤) G.radialCurve r

theorem NavierStokes.PhysicalCurlCovariance.ScaledGraph.radial_aux_derivative (G : ScaledGraph) {x : Cylinder} (hx : x.1.1 ≠ 0) (v : Cylinder) (hv : v.1.1 = 0) : (fderiv ℝ (PhysicalResidualBridge.ScaledGraph.radial G) x) v = 0

theorem NavierStokes.PhysicalCurlCovariance.ScaledGraph.geometry (G : ScaledGraph) {U : Set Cylinder} (hU : IsOpen U) (hR : ∀ x ∈ U, x.1.1 ≠ 0) : CurlClassBounds.CylindricalGeometry U PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.ScaledGraph.radial G) PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.ScaledGraph.axial G)

theorem NavierStokes.PhysicalCurlCovariance.commonGraph_potentialScale {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (k : ℕ) : (PhysicalResidualBridge.commonGraph Q h k).velocityScale / (PhysicalResidualBridge.commonGraph Q h k).radialScale = Q ^ (-h)

theorem NavierStokes.PhysicalCurlCovariance.commonGraph_curlScale {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (k : ℕ) : Q ^ (-h) * (PhysicalResidualBridge.commonGraph Q h k).radialScale = Q ^ (-CoordinateAlgebra.A h)

theorem NavierStokes.PhysicalCurlCovariance.commonGraph_physical_curl {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (k : ℕ) {B : Cylinder → HarmonicCalculus.ComplexVector} {t : ℝ} {q : ProblemStatement.Space} (hr : 0 < q.ofLp 0) (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : Cylinder) => B y i) ((PhysicalResidualBridge.commonGraph Q h k).map (t, q))) {A : ProblemStatement.VelocityField} (hA : DifferentiableAt ℝ A (t, CylindricalResidual.chart q)) (hrep : (fun (z : ProblemStatement.SpaceTime) => A (z.1, CylindricalResidual.chart z.2)) =ᶠ[nhds (t, q)] fun (z : ℝ × ProblemStatement.Space) => (CylindricalResidual.frame (z.2.ofLp 1)) (ScaledGraph.realPotential (PhysicalResidualBridge.commonGraph Q h k) (Q ^ (-h)) B z)) (i : Fin 3) : (CurlClassBounds.cylindricalCurl PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h k).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h k).axial B ((PhysicalResidualBridge.commonGraph Q h k).map (t, q)) i).re = Q ^ CoordinateAlgebra.A h * ((CylindricalResidual.frame (-q.ofLp 1)) (SpatialCurl.spatialCurl A (t, CylindricalResidual.chart q))).ofLp i

Arbitrary native or common covering index, with the exact potential weight Q^(-h) and velocity weight Q^(-A).

theorem NavierStokes.PhysicalCurlCovariance.commonGraph_vectorPotential_pull {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (k : ℕ) {K L : ℝ} (hK : K ≠ 0) (hL : L ≠ 0) {Φ : Cylinder → ℝ} {x : ProblemStatement.SpaceTime} (hr : 0 < x.2.ofLp 0) (hΦ : DifferentiableAt ℝ Φ ((PhysicalResidualBridge.commonGraph Q h k).map x)) (a : Cylinder → HarmonicCalculus.ComplexVector) : CurlClassBounds.vectorPotential K LinearWaveResidual.coordinateRadius (LinearWaveResidual.spaceDirection 0) (LinearWaveResidual.spaceDirection 1) (LinearWaveResidual.spaceDirection 2) (fun (y : ProblemStatement.SpaceTime) => L / K * Φ ((PhysicalResidualBridge.commonGraph Q h k).map y)) (fun (y : ProblemStatement.SpaceTime) => Q ^ (-CoordinateAlgebra.A h) • a ((PhysicalResidualBridge.commonGraph Q h k).map y)) x = Q ^ (-h) • CurlClassBounds.vectorPotential L PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h k).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h k).axial Φ a ((PhysicalResidualBridge.commonGraph Q h k).map x)

Derivation of the potential pullback from raw amplitude and phase scaling. The real factor b also covers signed harmonics.

theorem NavierStokes.PhysicalCurlCovariance.vectorPotential_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ℝ) (R : E → ℝ) (Vr Vθ Vz : E → E) {Φ Ψ : E → ℝ} {a b : E → HarmonicCalculus.ComplexVector} {x : E} (hΦ : Φ =ᶠ[nhds x] Ψ) (ha : a x = b x) : CurlClassBounds.vectorPotential K R Vr Vθ Vz Φ a x = CurlClassBounds.vectorPotential K R Vr Vθ Vz Ψ b x

noncomputable def NavierStokes.PhysicalCurlCovariance.referencePotential (K : ℝ) (Ψ : ProblemStatement.SpaceTime → ℝ) (a : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector

The single reference potential expressed in physical cylindrical coordinates, before taking its real part and rotating to Cartesian axes.

Equations

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

theorem NavierStokes.PhysicalCurlCovariance.referencePotential_eq_on {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (k : ℕ) {U : Set Cylinder} (hU : IsOpen U) {K L : ℝ} (hK : K ≠ 0) (hL : L ≠ 0) {Φ : Cylinder → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (a : Cylinder → HarmonicCalculus.ComplexVector) (Ψ : ProblemStatement.SpaceTime → ℝ) (v : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) (hphase : ∀ z ∈ (PhysicalResidualBridge.commonGraph Q h k).source U, K * Ψ z = L * Φ ((PhysicalResidualBridge.commonGraph Q h k).map z)) (hamplitude : ∀ z ∈ (PhysicalResidualBridge.commonGraph Q h k).source U, v z = Q ^ (-CoordinateAlgebra.A h) • a ((PhysicalResidualBridge.commonGraph Q h k).map z)) : Set.EqOn (referencePotential K Ψ v) (fun (z : ProblemStatement.SpaceTime) => Q ^ (-h) • CurlClassBounds.vectorPotential L PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h k).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h k).axial Φ a ((PhysicalResidualBridge.commonGraph Q h k).map z)) ((PhysicalResidualBridge.commonGraph Q h k).source U)

Potential covariance is derived from the primitive phase and amplitude identities. No identity between curls or corrected velocities is assumed.

theorem NavierStokes.PhysicalCurlCovariance.reference_correctedWave {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (k : ℕ) {U : Set Cylinder} (hU : IsOpen U) (hR : ∀ x ∈ U, x.1.1 ≠ 0) {K L : ℝ} (hK : K ≠ 0) (hL : L ≠ 0) {Φ : Cylinder → ℝ} {a : Cylinder → HarmonicCalculus.ComplexVector} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) (hn : ∀ x ∈ U, HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h k).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h k).axial Φ x ≠ 0) (ht : ∀ x ∈ U, HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h k).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h k).axial Φ x) (a x) = 0) (Ψ : ProblemStatement.SpaceTime → ℝ) (v : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) (hphase : ∀ z ∈ (PhysicalResidualBridge.commonGraph Q h k).source U, K * Ψ z = L * Φ ((PhysicalResidualBridge.commonGraph Q h k).map z)) (hamplitude : ∀ z ∈ (PhysicalResidualBridge.commonGraph Q h k).source U, v z = Q ^ (-CoordinateAlgebra.A h) • a ((PhysicalResidualBridge.commonGraph Q h k).map z)) {t : ℝ} {q : ProblemStatement.Space} (hz : (t, q) ∈ (PhysicalResidualBridge.commonGraph Q h k).source U) {A : ProblemStatement.VelocityField} (hA : DifferentiableAt ℝ A (t, CylindricalResidual.chart q)) (hAvalue : (fun (z : ProblemStatement.SpaceTime) => A (z.1, CylindricalResidual.chart z.2)) =ᶠ[nhds (t, q)] fun (z : ℝ × ProblemStatement.Space) => (CylindricalResidual.frame (z.2.ofLp 1)) (realVector (referencePotential K Ψ v z))) (i : Fin 3) : (HarmonicCalculus.vectorMode L Φ (CurlClassBounds.realizedCoefficient L PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h k).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h k).axial Φ a) ((PhysicalResidualBridge.commonGraph Q h k).map (t, q)) i).re = Q ^ CoordinateAlgebra.A h * ((CylindricalResidual.frame (-q.ofLp 1)) (SpatialCurl.spatialCurl A (t, CylindricalResidual.chart q))).ofLp i

One Cartesian reference potential supplies every compatible band's actual corrected wave. Amplitude and phase compatibility are primitive field-value identities; the curl and cutoff derivatives are derived.

theorem NavierStokes.PhysicalCurlCovariance.wave_cutoff_potential {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : LinearWaveBounds.WaveCoefficients E) (s : WeightedClasses.StripData E) (d : LinearWaveBounds.GraphDirections E) (ψ : ℕ → E → ℝ) (n : ℕ) (x : E) : (a.withCutoff ψ).curlPotential s d n x = ψ n x • a.curlPotential s d n x

theorem NavierStokes.PhysicalCurlCovariance.corrected_is_curl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a : LinearWaveBounds.WaveCoefficients E) (s : WeightedClasses.StripData E) (d : LinearWaveBounds.GraphDirections E) (ψ : ℕ → E → ℝ) (n : ℕ) (G : CurlClassBounds.CylindricalGeometry s.domain (a.radius n) (d.radialField n) (fun (x : E) => d.angular) (d.axialField s n)) (hK : a.frequency n ≠ 0) (hΦ : ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (ha : ContDiffOn ℝ (↑⊤) (a.amplitude n) s.domain) (hψ : ContDiffOn ℝ (↑⊤) (ψ n) s.domain) (hn : ∀ x ∈ s.domain, a.normal s d n x ≠ 0) (ht : ∀ x ∈ s.domain, HarmonicCalculus.normalDot (a.normal s d n x) (a.amplitude n x) = 0) {x : E} (hx : x ∈ s.domain) : CurlClassBounds.cylindricalCurl (a.radius n) (d.radialField n) (fun (x : E) => d.angular) (d.axialField s n) ((a.withCutoff ψ).curlPotential s d n) x = HarmonicCalculus.vectorMode (a.frequency n) (a.phase n) ((a.corrected s d ψ).amplitude n) x

The coefficient used by the wave pipeline, after the cutoff, is the coefficient of the actual curl. The cutoff is applied exactly once.

theorem NavierStokes.PhysicalCurlCovariance.spatialCurl_zero_of_zero_near {A : ProblemStatement.VelocityField} {z : ProblemStatement.SpaceTime} (hA : A =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0) : SpatialCurl.spatialCurl A z = 0

theorem NavierStokes.PhysicalCurlCovariance.spatialCurl_axis_zero (A : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) (hx₀ : x.ofLp 0 = 0) (hx₁ : x.ofLp 1 = 0) {r : ℝ} (hr : 0 < r) (hA : ∀ (y : ProblemStatement.Space), y.ofLp 0 ^ 2 + y.ofLp 1 ^ 2 < r ^ 2 → A (t, y) = 0) : SpatialCurl.spatialCurl A (t, x) = 0

Annularly localized potentials have zero actual curl on the axis, without assigning a cylindrical angle there.

A concrete Cartesian potential in an actual inverse polar chart

theorem NavierStokes.PhysicalCurlCovariance.realVector_smooth : ContDiff ℝ (↑⊤) realVector

noncomputable def NavierStokes.PhysicalCurlCovariance.polarInput (a : ℝ) (j : PolarCharts.Index) (z : ProblemStatement.SpaceTime) : PhysicalResidualBridge.Plane

Polar input, given by PolarCharts.chart a j (PhysicalGraphBounds.radialProjection z).

Equations

• NavierStokes.PhysicalCurlCovariance.polarInput a j z = NavierStokes.PolarCharts.chart a j (NavierStokes.PhysicalGraphBounds.radialProjection z)

noncomputable def NavierStokes.PhysicalCurlCovariance.polarCoordinates (a : ℝ) (j : PolarCharts.Index) (z : ProblemStatement.SpaceTime) : ProblemStatement.SpaceTime

Polar coordinates, given by (z.1, AxisymmetricResidual.pack (polarInput a j z).1 (polarInput a j z).2 (z.2 2)).

Equations

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

noncomputable def NavierStokes.PhysicalCurlCovariance.cartesianPotential (a : ℝ) (j : PolarCharts.Index) (B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) (z : ProblemStatement.SpaceTime) : ProblemStatement.Space

The actual Cartesian field, not a prescribed derivative or a matching predicate. Its inverse polar chart has a smooth global extension.

Equations

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

theorem NavierStokes.PhysicalCurlCovariance.polarInput_smooth {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) : ContDiff ℝ (↑⊤) (polarInput a j)

theorem NavierStokes.PhysicalCurlCovariance.polarCoordinates_smooth {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) : ContDiff ℝ (↑⊤) (polarCoordinates a j)

theorem NavierStokes.PhysicalCurlCovariance.cartesianPotential_smoothAt {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector} {z : ProblemStatement.SpaceTime} (hB : ContDiffAt ℝ (↑⊤) B (polarCoordinates a j z)) : ContDiffAt ℝ (↑⊤) (cartesianPotential a j B) z

noncomputable def NavierStokes.PhysicalCurlCovariance.validCylindrical (a : ℝ) (j : PolarCharts.Index) : Set ProblemStatement.SpaceTime

Valid cylindrical as an element of Set SpaceTime.

Equations

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

theorem NavierStokes.PhysicalCurlCovariance.validCylindrical_open (a : ℝ) (j : PolarCharts.Index) : IsOpen (validCylindrical a j)

theorem NavierStokes.PhysicalCurlCovariance.polarInput_forward {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hz : z ∈ validCylindrical a j) : polarInput a j (z.1, CylindricalResidual.chart z.2) = (z.2.ofLp 0, z.2.ofLp 1)

theorem NavierStokes.PhysicalCurlCovariance.polarCoordinates_forward {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hz : z ∈ validCylindrical a j) : polarCoordinates a j (z.1, CylindricalResidual.chart z.2) = z

theorem NavierStokes.PhysicalCurlCovariance.cartesianPotential_forward {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) {z : ProblemStatement.SpaceTime} (hz : z ∈ validCylindrical a j) : cartesianPotential a j B (z.1, CylindricalResidual.chart z.2) = (CylindricalResidual.frame (z.2.ofLp 1)) (realVector (B z))

theorem NavierStokes.PhysicalCurlCovariance.cartesianPotential_forward_germ {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) {z : ProblemStatement.SpaceTime} (hz : z ∈ validCylindrical a j) : (fun (w : ProblemStatement.SpaceTime) => cartesianPotential a j B (w.1, CylindricalResidual.chart w.2)) =ᶠ[nhds z] fun (w : ProblemStatement.SpaceTime) => (CylindricalResidual.frame (w.2.ofLp 1)) (realVector (B w))

theorem NavierStokes.PhysicalCurlCovariance.cartesianPotential_curl {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector} {z : ProblemStatement.SpaceTime} (hz : z ∈ validCylindrical a j) (hB : ContDiffAt ℝ (↑⊤) B z) (i : Fin 3) : ((CylindricalResidual.frame (-z.2.ofLp 1)) (SpatialCurl.spatialCurl (cartesianPotential a j B) (z.1, CylindricalResidual.chart z.2))).ofLp i = (CurlClassBounds.cylindricalCurl LinearWaveResidual.coordinateRadius (LinearWaveResidual.spaceDirection 0) (LinearWaveResidual.spaceDirection 1) (LinearWaveResidual.spaceDirection 2) B z i).re

The constructed Cartesian potential has the prescribed actual curl in its polar chart. No potential-representation premise remains.

theorem NavierStokes.PhysicalCurlCovariance.frame_periodic : Function.Periodic CylindricalResidual.frame (2 * Real.pi)

theorem NavierStokes.PhysicalCurlCovariance.cartesianPotential_overlap {a : ℝ} (ha : 0 < a) (i j : PolarCharts.Index) (B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) (hB : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => B (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) {x : ProblemStatement.SpaceTime} (hi : PhysicalGraphBounds.radialProjection x ∈ PolarCharts.chartDomain a i) (hj : PhysicalGraphBounds.radialProjection x ∈ PolarCharts.chartDomain a j) : cartesianPotential a i B x = cartesianPotential a j B x

Periodicity of the full cylindrical potential gives equality of the constructed Cartesian potentials on chart overlaps.

theorem NavierStokes.PhysicalCurlCovariance.spatialCurl_congr {A B : ProblemStatement.VelocityField} {z : ProblemStatement.SpaceTime} (hAB : A =ᶠ[nhds z] B) : SpatialCurl.spatialCurl A z = SpatialCurl.spatialCurl B z

theorem NavierStokes.PhysicalCurlCovariance.cartesianPotential_overlap_germ {a : ℝ} (ha : 0 < a) (i j : PolarCharts.Index) (B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) (hB : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => B (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) {x : ProblemStatement.SpaceTime} (hi : PhysicalGraphBounds.radialProjection x ∈ PolarCharts.chartDomain a i) (hj : PhysicalGraphBounds.radialProjection x ∈ PolarCharts.chartDomain a j) : cartesianPotential a i B =ᶠ[nhds x] cartesianPotential a j B

theorem NavierStokes.PhysicalCurlCovariance.cartesianPotential_curl_overlap {a : ℝ} (ha : 0 < a) (i j : PolarCharts.Index) (B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) (hB : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => B (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) {x : ProblemStatement.SpaceTime} (hi : PhysicalGraphBounds.radialProjection x ∈ PolarCharts.chartDomain a i) (hj : PhysicalGraphBounds.radialProjection x ∈ PolarCharts.chartDomain a j) : SpatialCurl.spatialCurl (cartesianPotential a i B) x = SpatialCurl.spatialCurl (cartesianPotential a j B) x

noncomputable def NavierStokes.PhysicalCurlCovariance.globalCartesianPotential (a : ℝ) (B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) (x : ProblemStatement.SpaceTime) : ProblemStatement.Space

A single actual Cartesian potential is selected from the compatible local inverse charts. Outside their union it is defined to be zero.

Equations

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

theorem NavierStokes.PhysicalCurlCovariance.globalCartesianPotential_eq_local {a : ℝ} (ha : 0 < a) (B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) (hB : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => B (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) {x : ProblemStatement.SpaceTime} (j : PolarCharts.Index) (hj : PhysicalGraphBounds.radialProjection x ∈ PolarCharts.chartDomain a j) : globalCartesianPotential a B x = cartesianPotential a j B x

theorem NavierStokes.PhysicalCurlCovariance.globalCartesianPotential_germ_local {a : ℝ} (ha : 0 < a) (B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) (hB : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => B (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) {x : ProblemStatement.SpaceTime} (j : PolarCharts.Index) (hj : PhysicalGraphBounds.radialProjection x ∈ PolarCharts.chartDomain a j) : globalCartesianPotential a B =ᶠ[nhds x] cartesianPotential a j B

theorem NavierStokes.PhysicalCurlCovariance.polarCoordinates_radius {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {x : ProblemStatement.SpaceTime} (hj : PhysicalGraphBounds.radialProjection x ∈ PolarCharts.chartDomain a j) : (polarCoordinates a j x).2.ofLp 0 = PolarCharts.radius (PhysicalGraphBounds.radialProjection x)

theorem NavierStokes.PhysicalCurlCovariance.globalCartesianPotential_zero {a : ℝ} (ha : 0 < a) {B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector} (hzero : ∀ (z : ProblemStatement.SpaceTime), z.2.ofLp 0 ≤ a → B z = 0) {x : ProblemStatement.SpaceTime} (hx : PolarCharts.radius (PhysicalGraphBounds.radialProjection x) ≤ a) : globalCartesianPotential a B x = 0

theorem NavierStokes.PhysicalCurlCovariance.globalCartesianPotential_smooth {a : ℝ} (ha : 0 < a) {B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector} (hB : ContDiffOn ℝ (↑⊤) B {z : ProblemStatement.SpaceTime | 0 < z.2.ofLp 0}) (hper : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => B (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) (hzero : ∀ (z : ProblemStatement.SpaceTime), z.2.ofLp 0 ≤ a → B z = 0) : ContDiff ℝ (↑⊤) (globalCartesianPotential a B)

Annular vanishing removes the boundary of the selected-chart union; the resulting Cartesian potential is genuinely smooth everywhere.

theorem NavierStokes.PhysicalCurlCovariance.globalCartesianPotential_zero_germ {a : ℝ} (ha : 0 < a) {B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector} (hzero : ∀ (z : ProblemStatement.SpaceTime), z.2.ofLp 0 ≤ a → B z = 0) {x : ProblemStatement.SpaceTime} (hx : PolarCharts.radius (PhysicalGraphBounds.radialProjection x) < a) : globalCartesianPotential a B =ᶠ[nhds x] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.PhysicalCurlCovariance.globalCartesianPotential_smoothOn {a : ℝ} (ha : 0 < a) {times : Set ℝ} (hTimes : IsOpen times) {B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector} (hB : ContDiffOn ℝ (↑⊤) B {z : ProblemStatement.SpaceTime | z.1 ∈ times ∧ 0 < z.2.ofLp 0}) (hper : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => B (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) (hzero : ∀ (z : ProblemStatement.SpaceTime), z.2.ofLp 0 ≤ a → B z = 0) : ContDiffOn ℝ (↑⊤) (globalCartesianPotential a B) (times ×ˢ Set.univ)

The potential need only be smooth on the physical time domain; no extension through a possible singular terminal time is required.

noncomputable def NavierStokes.PhysicalCurlCovariance.cartesianVelocity (a : ℝ) (B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) : ProblemStatement.VelocityField

Cartesian velocity, given by SpatialCurl.spatialCurl (globalCartesianPotential a B).

Equations

• NavierStokes.PhysicalCurlCovariance.cartesianVelocity a B = NavierStokes.SpatialCurl.spatialCurl (NavierStokes.PhysicalCurlCovariance.globalCartesianPotential a B)

theorem NavierStokes.PhysicalCurlCovariance.cartesianVelocity_smoothOn {a : ℝ} (ha : 0 < a) {times : Set ℝ} (hTimes : IsOpen times) {B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector} (hB : ContDiffOn ℝ (↑⊤) B {z : ProblemStatement.SpaceTime | z.1 ∈ times ∧ 0 < z.2.ofLp 0}) (hper : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => B (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) (hzero : ∀ (z : ProblemStatement.SpaceTime), z.2.ofLp 0 ≤ a → B z = 0) : ContDiffOn ℝ (↑⊤) (cartesianVelocity a B) (times ×ˢ Set.univ)

theorem NavierStokes.PhysicalCurlCovariance.cartesianVelocity_divergence {a : ℝ} (ha : 0 < a) {times : Set ℝ} (hTimes : IsOpen times) {B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector} (hB : ContDiffOn ℝ (↑⊤) B {z : ProblemStatement.SpaceTime | z.1 ∈ times ∧ 0 < z.2.ofLp 0}) (hper : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => B (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) (hzero : ∀ (z : ProblemStatement.SpaceTime), z.2.ofLp 0 ≤ a → B z = 0) {t : ℝ} (ht : t ∈ times) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence (cartesianVelocity a B) t x = 0

theorem NavierStokes.PhysicalCurlCovariance.cartesianVelocity_axis_zero {a : ℝ} (ha : 0 < a) {B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector} (hzero : ∀ (z : ProblemStatement.SpaceTime), z.2.ofLp 0 ≤ a → B z = 0) (t : ℝ) (x : ProblemStatement.Space) (hx₀ : x.ofLp 0 = 0) (hx₁ : x.ofLp 1 = 0) : cartesianVelocity a B (t, x) = 0

theorem NavierStokes.PhysicalCurlCovariance.globalCartesianPotential_curl {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector} (hper : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => B (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) {z : ProblemStatement.SpaceTime} (hz : z ∈ validCylindrical a j) (hB : ContDiffAt ℝ (↑⊤) B z) (i : Fin 3) : ((CylindricalResidual.frame (-z.2.ofLp 1)) (SpatialCurl.spatialCurl (globalCartesianPotential a B) (z.1, CylindricalResidual.chart z.2))).ofLp i = (CurlClassBounds.cylindricalCurl LinearWaveResidual.coordinateRadius (LinearWaveResidual.spaceDirection 0) (LinearWaveResidual.spaceDirection 1) (LinearWaveResidual.spaceDirection 2) B z i).re

theorem NavierStokes.PhysicalCurlCovariance.globalCartesianPotential_forward_germ {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) (hper : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => B (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) {z : ProblemStatement.SpaceTime} (hz : z ∈ validCylindrical a j) : (fun (w : ProblemStatement.SpaceTime) => globalCartesianPotential a B (w.1, CylindricalResidual.chart w.2)) =ᶠ[nhds z] fun (w : ProblemStatement.SpaceTime) => (CylindricalResidual.frame (w.2.ofLp 1)) (realVector (B w))

theorem NavierStokes.PhysicalCurlCovariance.globalCartesianPotential_smoothAt_forward {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {B : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector} (hper : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => B (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) {z : ProblemStatement.SpaceTime} (hz : z ∈ validCylindrical a j) (hB : ContDiffAt ℝ (↑⊤) B z) : ContDiffAt ℝ (↑⊤) (globalCartesianPotential a B) (z.1, CylindricalResidual.chart z.2)

theorem NavierStokes.PhysicalCurlCovariance.vectorPotential_fullTurn {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {θ : D} {R : D → ℝ} {Vr Vθ Vz : D → D} {Φ : D → ℝ} {a : D → HarmonicCalculus.ComplexVector} {slope K : ℝ} (m : ℤ) (hR : CopyAngularInvariance.Invariant θ R) (hr : CopyAngularInvariance.Invariant θ Vr) (hθ : CopyAngularInvariance.Invariant θ Vθ) (hz : CopyAngularInvariance.Invariant θ Vz) (hΦ : CopyAngularInvariance.AffinePhase θ slope Φ) (ha : CopyAngularInvariance.Invariant θ a) (hfreq : K * slope = ↑m) (x : D) : CurlClassBounds.vectorPotential K R Vr Vθ Vz Φ a (x + (2 * Real.pi) • θ) = CurlClassBounds.vectorPotential K R Vr Vθ Vz Φ a x

Integer angular frequency makes the complete potential periodic, including its normal coefficient and inverse carrier.

theorem NavierStokes.PhysicalCurlCovariance.reference_correctedWave_constructed {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (k : ℕ) {U : Set Cylinder} (hU : IsOpen U) (hR : ∀ x ∈ U, x.1.1 ≠ 0) {K L : ℝ} (hK : K ≠ 0) (hL : L ≠ 0) {Φ : Cylinder → ℝ} {a : Cylinder → HarmonicCalculus.ComplexVector} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) (hn : ∀ x ∈ U, HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h k).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h k).axial Φ x ≠ 0) (ht : ∀ x ∈ U, HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h k).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h k).axial Φ x) (a x) = 0) (Ψ : ProblemStatement.SpaceTime → ℝ) (v : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) (hphase : ∀ z ∈ (PhysicalResidualBridge.commonGraph Q h k).source U, K * Ψ z = L * Φ ((PhysicalResidualBridge.commonGraph Q h k).map z)) (hamplitude : ∀ z ∈ (PhysicalResidualBridge.commonGraph Q h k).source U, v z = Q ^ (-CoordinateAlgebra.A h) • a ((PhysicalResidualBridge.commonGraph Q h k).map z)) (hper : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => referencePotential K Ψ v (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) {t : ℝ} {q : ProblemStatement.Space} (hz : (t, q) ∈ (PhysicalResidualBridge.commonGraph Q h k).source U) {δ : ℝ} (hδ : 0 < δ) (j : PolarCharts.Index) (hchart : (t, q) ∈ validCylindrical δ j) (i : Fin 3) : (HarmonicCalculus.vectorMode L Φ (CurlClassBounds.realizedCoefficient L PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph Q h k).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph Q h k).axial Φ a) ((PhysicalResidualBridge.commonGraph Q h k).map (t, q)) i).re = Q ^ CoordinateAlgebra.A h * ((CylindricalResidual.frame (-q.ofLp 1)) (SpatialCurl.spatialCurl (globalCartesianPotential δ (referencePotential K Ψ v)) (t, CylindricalResidual.chart q))).ofLp i

The end-to-end band reconstruction uses a single explicitly constructed Cartesian potential. Only primitive phase/amplitude compatibility and periodicity are inputs; potential and curl compatibility are conclusions.