Support of the actual harmonic residual supplied to a copy solve

The support conclusions below are derived from the literal harmonic derivatives, convolutions, real projection, and removal of the zero mode. Only nonzero input harmonics need be localized: a spatially global zero mode, such as an axisymmetric pressure alias, does not create a new slot.

def NavierStokes.HarmonicSourceSupport.NonzeroSupported {D : Type} (K : Set D) (c : HarmonicFields.Coefficients D) : Prop

Every nonzero harmonic vanishes outside the specified spatial set. The zero coefficient is unrestricted.

Equations

• NavierStokes.HarmonicSourceSupport.NonzeroSupported K c = ∀ (j : ℤ), j ≠ 0 → ∀ x ∉ K, c.coeff j x = 0

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupported.zero {D : Type} {K : Set D} : NonzeroSupported K 0

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupported.mono {D : Type} {K : Set D} {c : HarmonicFields.Coefficients D} (hc : NonzeroSupported K c) {L : Set D} (hKL : K ⊆ L) : NonzeroSupported L c

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupported.add {D : Type} {K : Set D} {c d : HarmonicFields.Coefficients D} (hc : NonzeroSupported K c) (hd : NonzeroSupported K d) : NonzeroSupported K (c + d)

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupported.neg {D : Type} {K : Set D} {c : HarmonicFields.Coefficients D} (hc : NonzeroSupported K c) : NonzeroSupported K (-c)

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupported.sub {D : Type} {K : Set D} {c d : HarmonicFields.Coefficients D} (hc : NonzeroSupported K c) (hd : NonzeroSupported K d) : NonzeroSupported K (c - d)

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupported.mul {D : Type} {K : Set D} {c d : HarmonicFields.Coefficients D} (hc : NonzeroSupported K c) (hd : NonzeroSupported K d) : NonzeroSupported K (c * d)

In a nonzero convolution mode, at least one input index is nonzero.

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupported.boundConstant {D : Type} {K : Set D} (f : D → ℂ) : NonzeroSupported K (HarmonicFields.constantCoefficient f)

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupported.coefficient_germ {D : Type} [NormedAddCommGroup D] {K : Set D} {c : HarmonicFields.Coefficients D} (hc : NonzeroSupported K c) (hK : IsClosed K) {j : ℤ} (hj : j ≠ 0) {x : D} (hx : x ∉ K) : c.coeff j =ᶠ[nhds x] fun (x : D) => 0

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupported.differentiate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {K : Set D} {c : HarmonicFields.Coefficients D} (hc : NonzeroSupported K c) (hK : IsClosed K) (V : D → D) (k : ℝ) (Φ : D → ℝ) : NonzeroSupported K (HarmonicFields.differentiate V k Φ c)

Actual Fréchet differentiation is local, including when no regularity of the coefficient is assumed on the other side of the support.

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupported.angular {D : Type} {K : Set D} {c : HarmonicFields.Coefficients D} (hc : NonzeroSupported K c) (kp : ℤ) : NonzeroSupported K (HarmonicFields.angularDifferentiate kp c)

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupported.realProjection {D : Type} {K : Set D} {c : HarmonicFields.Coefficients D} (hc : NonzeroSupported K c) : NonzeroSupported K (HarmonicResidual.realCoefficients c)

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupported.nonconstant {D : Type} {K : Set D} {c : HarmonicFields.Coefficients D} (hc : NonzeroSupported K c) : NonzeroSupported K (HarmonicResidual.nonconstant c)

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupported.tsupport {D : Type} [NormedAddCommGroup D] {K : Set D} {c : HarmonicFields.Coefficients D} (hc : NonzeroSupported K c) (hK : IsClosed K) {j : ℤ} (hj : j ≠ 0) : _root_.tsupport (c.coeff j) ⊆ K

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupported.of_tsupport {D : Type} [NormedAddCommGroup D] {K : Set D} {c : HarmonicFields.Coefficients D} (hc : ∀ (j : ℤ), j ≠ 0 → _root_.tsupport (c.coeff j) ⊆ K) : NonzeroSupported K c

theorem NavierStokes.HarmonicSourceSupport.rotate_supported {D : Type} {K : Set D} {a : HarmonicResidual.VectorCoefficients D} (ha : ∀ (i : Fin 3), NonzeroSupported K (a i)) (i : Fin 3) : NonzeroSupported K (HarmonicResidual.rotate a i)

theorem NavierStokes.HarmonicSourceSupport.scalarLaplacian_supported {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {K : Set D} (hK : IsClosed K) (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) {c : HarmonicFields.Coefficients D} (hc : NonzeroSupported K c) : NonzeroSupported K (HarmonicResidual.scalarLaplacian g k Φ kp c)

theorem NavierStokes.HarmonicSourceSupport.vectorLaplacian_supported {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {K : Set D} (hK : IsClosed K) (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) {a : HarmonicResidual.VectorCoefficients D} (ha : ∀ (i : Fin 3), NonzeroSupported K (a i)) (i : Fin 3) : NonzeroSupported K (HarmonicResidual.vectorLaplacian g k Φ kp a i)

theorem NavierStokes.HarmonicSourceSupport.transport_supported {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {K : Set D} (hK : IsClosed K) (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) {a b : HarmonicResidual.VectorCoefficients D} (ha : ∀ (i : Fin 3), NonzeroSupported K (a i)) (hb : ∀ (i : Fin 3), NonzeroSupported K (b i)) (i : Fin 3) : NonzeroSupported K (HarmonicResidual.transport g k Φ kp a b i)

theorem NavierStokes.HarmonicSourceSupport.gradient_supported {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {K : Set D} (hK : IsClosed K) (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) {p : HarmonicFields.Coefficients D} (hp : NonzeroSupported K p) (i : Fin 3) : NonzeroSupported K (HarmonicResidual.gradient g k Φ kp p i)

theorem NavierStokes.HarmonicSourceSupport.nonlinearResidual_supported {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {K : Set D} (hK : IsClosed K) (g : HarmonicResidual.Frame D) (k : ℝ) (Φ : D → ℝ) (kp : ℤ) {B a : HarmonicResidual.VectorCoefficients D} {p : HarmonicFields.Coefficients D} (hB : ∀ (i : Fin 3), NonzeroSupported K (B i)) (ha : ∀ (i : Fin 3), NonzeroSupported K (a i)) (hp : NonzeroSupported K p) (i : Fin 3) : NonzeroSupported K (HarmonicResidual.nonlinearResidual g k Φ kp B a p i)

theorem NavierStokes.HarmonicSourceSupport.realCoefficients_sub {D : Type} (c d : HarmonicFields.Coefficients D) : HarmonicResidual.realCoefficients (c - d) = HarmonicResidual.realCoefficients c - HarmonicResidual.realCoefficients d

theorem NavierStokes.HarmonicSourceSupport.nonlinear_ofBlock_supported {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {K : Set D} (hK : IsClosed K) (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) (n : ℕ) (hv : ∀ (i : Fin 3), NonzeroSupported K (b.velocity n i)) (hp : NonzeroSupported K (b.pressure n)) (i : Fin 3) : NonzeroSupported K (HarmonicResidual.nonlinearResidual (HarmonicResidual.contextFrame c n) (b.frequency n) (b.phase n) (b.angularFrequency n) (HarmonicResidual.constantVector (HarmonicResidual.contextBase c n + HarmonicResidual.stateMean u n)) (HarmonicResidual.ofBlock b G A n).velocity (HarmonicResidual.ofBlock b G A n).pressure i)

noncomputable def NavierStokes.HarmonicSourceSupport.excludedSource {D : Type} (G A : HarmonicResidual.BlockCoefficients D) (j : ℤ) (n : ℕ) (x : D) : HarmonicCalculus.ComplexVector

The exact excluded nonzero coefficient. Its mean part is removed even when that part is not localized in a native slot.

Equations

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

theorem NavierStokes.HarmonicSourceSupport.residualSource_apply_ne_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) {j : ℤ} (hj : j ≠ 0) (n : ℕ) (x : D) (i : Fin 3) : ParticularWaveAssembly.residualSource c u b G A j n x i = (HarmonicResidual.realCoefficients (HarmonicResidual.nonlinearResidual (HarmonicResidual.contextFrame c n) (b.frequency n) (b.phase n) (b.angularFrequency n) (HarmonicResidual.constantVector (HarmonicResidual.contextBase c n + HarmonicResidual.stateMean u n)) (HarmonicResidual.ofBlock b G A n).velocity (HarmonicResidual.ofBlock b G A n).pressure i)).coeff j x - (HarmonicResidual.realCoefficients (G n i)).coeff j x - (HarmonicResidual.realCoefficients (A n i)).coeff j x

theorem NavierStokes.HarmonicSourceSupport.residualSource_outside {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) {K : Set D} (hK : IsClosed K) (n : ℕ) (hv : ∀ (i : Fin 3), NonzeroSupported K (b.velocity n i)) (hp : NonzeroSupported K (b.pressure n)) (j : ℤ) {x : D} (hx : x ∉ K) : ParticularWaveAssembly.residualSource c u b G A j n x = excludedSource G A j n x

Outside the wave and pressure cells, the literal residual source is exactly the negative excluded nonzero coefficient. No error is discarded.

theorem NavierStokes.HarmonicSourceSupport.residualSource_complement_germ {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) {K : Set D} (hK : IsClosed K) (n : ℕ) (hv : ∀ (i : Fin 3), NonzeroSupported K (b.velocity n i)) (hp : NonzeroSupported K (b.pressure n)) (j : ℤ) {x : D} (hx : x ∉ K) : ParticularWaveAssembly.residualSource c u b G A j n =ᶠ[nhds x] excludedSource G A j n

theorem NavierStokes.HarmonicSourceSupport.residualSource_support {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) {K : Set D} (hK : IsClosed K) (n : ℕ) (hv : ∀ (i : Fin 3), NonzeroSupported K (b.velocity n i)) (hp : NonzeroSupported K (b.pressure n)) (hG : ∀ (i : Fin 3), NonzeroSupported K (G n i)) (hA : ∀ (i : Fin 3), NonzeroSupported K (A n i)) (j : ℤ) : Function.support (ParticularWaveAssembly.residualSource c u b G A j n) ⊆ K

theorem NavierStokes.HarmonicSourceSupport.residualSource_tsupport {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) {K : Set D} (hK : IsClosed K) (n : ℕ) (hv : ∀ (i : Fin 3), NonzeroSupported K (b.velocity n i)) (hp : NonzeroSupported K (b.pressure n)) (hG : ∀ (i : Fin 3), NonzeroSupported K (G n i)) (hA : ∀ (i : Fin 3), NonzeroSupported K (A n i)) (j : ℤ) : tsupport (ParticularWaveAssembly.residualSource c u b G A j n) ⊆ K

Support of the actual real fields suffices

theorem NavierStokes.HarmonicSourceSupport.nonlinear_ofBlock_supported_of_real {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {K : Set D} (hK : IsClosed K) (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) (n : ℕ) (hv : ∀ (i : Fin 3), NonzeroSupported K (HarmonicResidual.realCoefficients (b.velocity n i))) (hp : NonzeroSupported K (HarmonicResidual.realCoefficients (b.pressure n))) (i : Fin 3) : NonzeroSupported K (HarmonicResidual.nonlinearResidual (HarmonicResidual.contextFrame c n) (b.frequency n) (b.phase n) (b.angularFrequency n) (HarmonicResidual.constantVector (HarmonicResidual.contextBase c n + HarmonicResidual.stateMean u n)) (HarmonicResidual.ofBlock b G A n).velocity (HarmonicResidual.ofBlock b G A n).pressure i)

theorem NavierStokes.HarmonicSourceSupport.residualSource_outside_of_real {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) {K : Set D} (hK : IsClosed K) (n : ℕ) (hv : ∀ (i : Fin 3), NonzeroSupported K (HarmonicResidual.realCoefficients (b.velocity n i))) (hp : NonzeroSupported K (HarmonicResidual.realCoefficients (b.pressure n))) (j : ℤ) {x : D} (hx : x ∉ K) : ParticularWaveAssembly.residualSource c u b G A j n x = excludedSource G A j n x

theorem NavierStokes.HarmonicSourceSupport.residualSource_complement_germ_of_real {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) {K : Set D} (hK : IsClosed K) (n : ℕ) (hv : ∀ (i : Fin 3), NonzeroSupported K (HarmonicResidual.realCoefficients (b.velocity n i))) (hp : NonzeroSupported K (HarmonicResidual.realCoefficients (b.pressure n))) (j : ℤ) {x : D} (hx : x ∉ K) : ParticularWaveAssembly.residualSource c u b G A j n =ᶠ[nhds x] excludedSource G A j n

theorem NavierStokes.HarmonicSourceSupport.residualSource_support_of_real {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) {K : Set D} (hK : IsClosed K) (n : ℕ) (hv : ∀ (i : Fin 3), NonzeroSupported K (HarmonicResidual.realCoefficients (b.velocity n i))) (hp : NonzeroSupported K (HarmonicResidual.realCoefficients (b.pressure n))) (hG : ∀ (i : Fin 3), NonzeroSupported K (HarmonicResidual.realCoefficients (G n i))) (hA : ∀ (i : Fin 3), NonzeroSupported K (HarmonicResidual.realCoefficients (A n i))) (j : ℤ) : Function.support (ParticularWaveAssembly.residualSource c u b G A j n) ⊆ K

theorem NavierStokes.HarmonicSourceSupport.realCoefficient_eq_zero_of_field {D : Type} (c : HarmonicFields.Coefficients D) (k : ℝ) (Φ : D → ℝ) {kp : ℤ} (hkp : kp ≠ 0) (j : ℤ) (x : D) (hf : ∀ (θ : ℝ), (HarmonicFields.field c k Φ kp (x, θ)).re = 0) : (HarmonicResidual.realCoefficients c).coeff j x = 0

theorem NavierStokes.HarmonicSourceSupport.realCoefficients_supported_of_field {D : Type} (c : HarmonicFields.Coefficients D) (k : ℝ) (Φ : D → ℝ) {kp : ℤ} (hkp : kp ≠ 0) {K : Set D} (hf : ∀ x ∉ K, ∀ (θ : ℝ), (HarmonicFields.field c k Φ kp (x, θ)).re = 0) : NonzeroSupported K (HarmonicResidual.realCoefficients c)

Fourier uniqueness transfers support of the evaluated real field to its actual real-projected coefficients; no coefficient support is assumed.

theorem NavierStokes.HarmonicSourceSupport.realCoefficients_tsupport_of_field {D : Type} [NormedAddCommGroup D] (c : HarmonicFields.Coefficients D) (k : ℝ) (Φ : D → ℝ) {kp : ℤ} (hkp : kp ≠ 0) {K : Set D} (hK : IsClosed K) (hf : ∀ x ∉ K, ∀ (θ : ℝ), (HarmonicFields.field c k Φ kp (x, θ)).re = 0) (j : ℤ) : tsupport ((HarmonicResidual.realCoefficients c).coeff j) ⊆ K

theorem NavierStokes.HarmonicSourceSupport.residualSource_support_of_fields {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) {K : Set D} (hK : IsClosed K) (n : ℕ) (hkp : b.angularFrequency n ≠ 0) (hv : ∀ x ∉ K, ∀ (θ : ℝ) (i : Fin 3), b.oscillation n (x, θ) i = 0) (hp : ∀ x ∉ K, ∀ (θ : ℝ), b.oscillatoryPressure n (x, θ) = 0) (hG : ∀ x ∉ K, ∀ (θ : ℝ) (i : Fin 3), (HarmonicResidual.vectorField (G n) (b.frequency n) (b.phase n) (b.angularFrequency n) (x, θ) i).re = 0) (hA : ∀ x ∉ K, ∀ (θ : ℝ) (i : Fin 3), (HarmonicResidual.vectorField (A n) (b.frequency n) (b.phase n) (b.angularFrequency n) (x, θ) i).re = 0) (j : ℤ) : Function.support (ParticularWaveAssembly.residualSource c u b G A j n) ⊆ K

The uncovered source is estimated from its explicit excluded errors

theorem NavierStokes.HarmonicSourceSupport.residualSource_complementJets {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) {I : Type u_1} (K : PeriodizedWaveBounds.Cells D I) (hv : ∀ (n : ℕ) (i : Fin 3), NonzeroSupported (⋃ (a : I), K.carrier n a) (HarmonicResidual.realCoefficients (b.velocity n i))) (hp : ∀ (n : ℕ), NonzeroSupported (⋃ (a : I), K.carrier n a) (HarmonicResidual.realCoefficients (b.pressure n))) (j : ℤ) {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} (he : WeightedClasses.MemClass s w α (excludedSource G A j)) : PeriodizedWaveBounds.ComplementJets s w α K.carrier (ParticularWaveAssembly.residualSource c u b G A j)

Coverage by all actual native copies

noncomputable def NavierStokes.HarmonicSourceSupport.nativeUnion {P : Type} (g : CommonCoverSolve.Geometry) (K : Set TorusInverse.Plane) : Set (P × TorusInverse.Plane)

Native union, given by ⋃ k : Frequency, PeriodizedWaveBounds.nativeCell g K k.

Equations

• NavierStokes.HarmonicSourceSupport.nativeUnion g K = ⋃ (k : NavierStokes.TorusInverse.Frequency), NavierStokes.PeriodizedWaveBounds.nativeCell g K k

theorem NavierStokes.HarmonicSourceSupport.nativeUnion_closed {P : Type} [NormedAddCommGroup P] (g : CommonCoverSolve.Geometry) {K : Set TorusInverse.Plane} (hK : IsCompact K) : IsClosed (nativeUnion g K)

theorem NavierStokes.HarmonicSourceSupport.mem_nativeUnion_iff {P : Type} (g : CommonCoverSolve.Geometry) (K : Set TorusInverse.Plane) (z : P × TorusInverse.Plane) : z ∈ nativeUnion g K ↔ z.2 ∈ SlotGeometry.liftedSupport g.gap ((fun (w : TorusInverse.Plane) => g.center + g.basis w) '' K)

The union of copy-coordinate cells is precisely the periodic lift of the native cell's actual geometric image.

theorem NavierStokes.HarmonicSourceSupport.sourceFamily_covered {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (g : ℕ → CommonCoverSolve.Geometry) (K : ℕ → Set TorusInverse.Plane) (hK : ∀ (n : ℕ), IsCompact (K n)) (hv : ∀ (n : ℕ) (i : Fin 3), NonzeroSupported (nativeUnion (g n) (K n)) (HarmonicResidual.realCoefficients (b.velocity n i))) (hp : ∀ (n : ℕ), NonzeroSupported (nativeUnion (g n) (K n)) (HarmonicResidual.realCoefficients (b.pressure n))) (hG : ∀ (n : ℕ) (i : Fin 3), NonzeroSupported (nativeUnion (g n) (K n)) (HarmonicResidual.realCoefficients (G n i))) (hA : ∀ (n : ℕ) (i : Fin 3), NonzeroSupported (nativeUnion (g n) (K n)) (HarmonicResidual.realCoefficients (A n i))) (j : ℤ) (n : ℕ) : Function.support (ParticularWaveAssembly.sourceFamily c u b G A j n) ⊆ ⋃ (k : TorusInverse.Frequency), PeriodizedWaveBounds.nativeCell (g n) (K n) k

Different labels: genuine derivative products vanish on separated slots

theorem NavierStokes.HarmonicSourceSupport.transport_zero_of_product_germ {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) {u v : D → HarmonicCalculus.ComplexVector} {x : D} (hc : ∀ (i : Fin 3), ContinuousAt (fun (y : D) => u y i) x) (hp : ∀ᶠ (y : D) in nhds x, ∀ (i j : Fin 3), u y i * v y j = 0) : LinearWaveResidual.transport R Vr Vθ Vz u v x = 0

Pointwise disjoint products on a neighborhood give the zero germ of the right factor whenever a component of the left factor is nonzero. This handles boundary points without imposing globally disjoint supports.

theorem NavierStokes.HarmonicSourceSupport.transport_sum_self_of_product_germs {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} (s : Finset ι) (R : D → ℝ) (Vr Vθ Vz : D → D) (u : ι → D → HarmonicCalculus.ComplexVector) {x : D} (hu : ∀ l ∈ s, ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => u l y i) x) (hp : ∀ l ∈ s, ∀ k ∈ s, l ≠ k → ∀ᶠ (y : D) in nhds x, ∀ (i j : Fin 3), u l y i * u k y j = 0) : LinearWaveResidual.transport R Vr Vθ Vz (∑ l ∈ s, u l) (∑ l ∈ s, u l) x = ∑ l ∈ s, LinearWaveResidual.transport R Vr Vθ Vz (u l) (u l) x

theorem NavierStokes.HarmonicSourceSupport.supported_product_germ {D : Type} [NormedAddCommGroup D] {ι : Type u_1} {d h : ℝ} {vr vt : TorusInverse.Plane} {sys : PartitionedCovariance.SlotSystem d h vr vt} {label : ℕ → ι → SlotColoring.Label} {χ : ℕ → D → LabelSumBounds.WindowPoint} {Y : ℕ → D → TorusInverse.Plane} {U : Set D} {u v : ι → CorrectionState.Oscillation D} (hU : IsOpen U) (hu : LabelSumBounds.SupportedOscillations sys label χ Y U u) (hv : LabelSumBounds.SupportedOscillations sys label χ Y U v) {l k : ι} {n : ℕ} (hl : 1 ≤ (label n l).1) (hk : 1 ≤ (label n k).1) (hne : label n l ≠ label n k) {x : D × ℝ} (hx : x.1 ∈ U) : ∀ᶠ (y : D × ℝ) in nhds x, ∀ (i j : Fin 3), LinearWaveResidual.realLift (u l n) y i * LinearWaveResidual.realLift (v k n) y j = 0

theorem NavierStokes.HarmonicSourceSupport.supported_transport_zero {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} {d h : ℝ} {vr vt : TorusInverse.Plane} {sys : PartitionedCovariance.SlotSystem d h vr vt} {label : ℕ → ι → SlotColoring.Label} {χ : ℕ → D → LabelSumBounds.WindowPoint} {Y : ℕ → D → TorusInverse.Plane} {U : Set D} {u v : ι → CorrectionState.Oscillation D} (hU : IsOpen U) (hu : LabelSumBounds.SupportedOscillations sys label χ Y U u) (hv : LabelSumBounds.SupportedOscillations sys label χ Y U v) {l k : ι} {n : ℕ} (hl : 1 ≤ (label n l).1) (hk : 1 ≤ (label n k).1) (hne : label n l ≠ label n k) {x : D × ℝ} (hx : x.1 ∈ U) (hc : ∀ (i : Fin 3), ContinuousAt (fun (y : D × ℝ) => u l n y i) x) (R : D × ℝ → ℝ) (Vr Vθ Vz : D × ℝ → D × ℝ) : LinearWaveResidual.transport R Vr Vθ Vz (LinearWaveResidual.realLift (u l n)) (LinearWaveResidual.realLift (v k n)) x = 0

The actual colored-slot geometry eliminates cross-label advection, including every derivative of the right factor in the cylindrical operator.

theorem NavierStokes.HarmonicSourceSupport.supported_nonlinearResidual_sum {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {ι : Type u_1} {d h : ℝ} {vr vt : TorusInverse.Plane} {sys : PartitionedCovariance.SlotSystem d h vr vt} {label : ℕ → ι → SlotColoring.Label} {χ : ℕ → D → LabelSumBounds.WindowPoint} {Y : ℕ → D → TorusInverse.Plane} {U : Set D} {u : ι → CorrectionState.Oscillation D} (hU : IsOpen U) (hs : LabelSumBounds.SupportedOscillations sys label χ Y U u) (labels : Finset ι) (n : ℕ) (hlevel : ∀ l ∈ labels, 1 ≤ (label n l).1) (hinj : Set.InjOn (label n) ↑labels) (ε : ℝ) (R : D × ℝ → ℝ) {Vr Vθ Vz : D × ℝ → D × ℝ} (Vt : D × ℝ → D × ℝ) (hr : ContDiffOn ℝ (↑⊤) Vr (HarmonicResidual.liftDomain U)) (hθ : ContDiffOn ℝ (↑⊤) Vθ (HarmonicResidual.liftDomain U)) (hz : ContDiffOn ℝ (↑⊤) Vz (HarmonicResidual.liftDomain U)) (B : D × ℝ → HarmonicCalculus.ComplexVector) (p : ι → D × ℝ → ℂ) (hu : ∀ l ∈ labels, ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : D × ℝ) => u l n y i) (HarmonicResidual.liftDomain U)) (hp : ∀ l ∈ labels, ContDiffOn ℝ (↑⊤) (p l) (HarmonicResidual.liftDomain U)) {x : D × ℝ} (hx : x.1 ∈ U) : HarmonicResidual.Actual.nonlinearResidual ε R Vr Vθ Vz Vt B (∑ l ∈ labels, LinearWaveResidual.realLift (u l n)) (∑ l ∈ labels, p l) x = ∑ l ∈ labels, HarmonicResidual.Actual.nonlinearResidual ε R Vr Vθ Vz Vt B (LinearWaveResidual.realLift (u l n)) (p l) x

The nonlinear residual of the actual finite sum is the sum of its same-label residuals. Cross-label cancellation comes from the geometric support predicate, not from an assumed PDE cancellation.

Relative support on the actual open strip

def NavierStokes.HarmonicSourceSupport.NonzeroSupportedOn {D : Type} (U K : Set D) (c : HarmonicFields.Coefficients D) : Prop

Nonzero coefficients are supported in K relative to U. Values outside U are not constrained.

Equations

• NavierStokes.HarmonicSourceSupport.NonzeroSupportedOn U K c = ∀ (j : ℤ), j ≠ 0 → ∀ x ∈ U, x ∉ K → c.coeff j x = 0

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupportedOn.enlarge {D : Type} {U K : Set D} {c : HarmonicFields.Coefficients D} (hc : NonzeroSupportedOn U K c) : NonzeroSupported (Uᶜ ∪ K) c

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupportedOn.of_global {D : Type} {U K : Set D} {c : HarmonicFields.Coefficients D} (hc : NonzeroSupported K c) : NonzeroSupportedOn U K c

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupportedOn.of_enlarge {D : Type} {U K : Set D} {c : HarmonicFields.Coefficients D} (hc : NonzeroSupported (Uᶜ ∪ K) c) : NonzeroSupportedOn U K c

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupportedOn.add {D : Type} {U K : Set D} {c : HarmonicFields.Coefficients D} (hc : NonzeroSupportedOn U K c) {d : HarmonicFields.Coefficients D} (hd : NonzeroSupportedOn U K d) : NonzeroSupportedOn U K (c + d)

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupportedOn.sub {D : Type} {U K : Set D} {c : HarmonicFields.Coefficients D} (hc : NonzeroSupportedOn U K c) {d : HarmonicFields.Coefficients D} (hd : NonzeroSupportedOn U K d) : NonzeroSupportedOn U K (c - d)

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupportedOn.mul {D : Type} {U K : Set D} {c : HarmonicFields.Coefficients D} (hc : NonzeroSupportedOn U K c) {d : HarmonicFields.Coefficients D} (hd : NonzeroSupportedOn U K d) : NonzeroSupportedOn U K (c * d)

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupportedOn.boundConstant {D : Type} {U K : Set D} (f : D → ℂ) : NonzeroSupportedOn U K (HarmonicFields.constantCoefficient f)

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupportedOn.differentiate {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U K : Set D} {c : HarmonicFields.Coefficients D} (hc : NonzeroSupportedOn U K c) (hU : IsOpen U) (hK : IsClosed K) (V : D → D) (k : ℝ) (Φ : D → ℝ) : NonzeroSupportedOn U K (HarmonicFields.differentiate V k Φ c)

theorem NavierStokes.HarmonicSourceSupport.NonzeroSupportedOn.realProjection {D : Type} {U K : Set D} {c : HarmonicFields.Coefficients D} (hc : NonzeroSupportedOn U K c) : NonzeroSupportedOn U K (HarmonicResidual.realCoefficients c)

structure NavierStokes.HarmonicSourceSupport.InputSupportOn {D : Type} (U : Set D) (K : ℕ → Set D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) : Prop

Primitive support data for the incoming block and its two excluded error families. There is no assumption about its residual or derivatives.

• velocity (n : ℕ) (i : Fin 3) : NonzeroSupportedOn U (K n) (HarmonicResidual.realCoefficients (b.velocity n i))
• pressure (n : ℕ) : NonzeroSupportedOn U (K n) (HarmonicResidual.realCoefficients (b.pressure n))
• gaussian (n : ℕ) (i : Fin 3) : NonzeroSupportedOn U (K n) (HarmonicResidual.realCoefficients (G n i))
• aliasError (n : ℕ) (i : Fin 3) : NonzeroSupportedOn U (K n) (HarmonicResidual.realCoefficients (A n i))

theorem NavierStokes.HarmonicSourceSupport.realCoefficients_supportedOn_of_field {D : Type} (c : HarmonicFields.Coefficients D) (k : ℝ) (Φ : D → ℝ) {kp : ℤ} (hkp : kp ≠ 0) {U K : Set D} (hf : ∀ x ∈ U, x ∉ K → ∀ (θ : ℝ), (HarmonicFields.field c k Φ kp (x, θ)).re = 0) : NonzeroSupportedOn U K (HarmonicResidual.realCoefficients c)

theorem NavierStokes.HarmonicSourceSupport.InputSupportOn.of_fields {D : Type} (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) {U : Set D} {K : ℕ → Set D} (hkp : ∀ (n : ℕ), b.angularFrequency n ≠ 0) (hv : ∀ (n : ℕ), ∀ x ∈ U, x ∉ K n → ∀ (θ : ℝ) (i : Fin 3), b.oscillation n (x, θ) i = 0) (hp : ∀ (n : ℕ), ∀ x ∈ U, x ∉ K n → ∀ (θ : ℝ), b.oscillatoryPressure n (x, θ) = 0) (hG : ∀ (n : ℕ), ∀ x ∈ U, x ∉ K n → ∀ (θ : ℝ) (i : Fin 3), (HarmonicResidual.vectorField (G n) (b.frequency n) (b.phase n) (b.angularFrequency n) (x, θ) i).re = 0) (hA : ∀ (n : ℕ), ∀ x ∈ U, x ∉ K n → ∀ (θ : ℝ) (i : Fin 3), (HarmonicResidual.vectorField (A n) (b.frequency n) (b.phase n) (b.angularFrequency n) (x, θ) i).re = 0) : InputSupportOn U K b G A

theorem NavierStokes.HarmonicSourceSupport.residualSource_complement_germ_on {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) {U K : Set D} (hU : IsOpen U) (hK : IsClosed K) (n : ℕ) (hv : ∀ (i : Fin 3), NonzeroSupportedOn U K (HarmonicResidual.realCoefficients (b.velocity n i))) (hp : NonzeroSupportedOn U K (HarmonicResidual.realCoefficients (b.pressure n))) (j : ℤ) {x : D} (hx : x ∈ U) (hn : x ∉ K) : ParticularWaveAssembly.residualSource c u b G A j n =ᶠ[nhds x] excludedSource G A j n

theorem NavierStokes.HarmonicSourceSupport.residualSource_zero_germ_on {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) {U : Set D} {K : ℕ → Set D} (hU : IsOpen U) (hK : ∀ (n : ℕ), IsClosed (K n)) (hs : InputSupportOn U K b G A) (j : ℤ) (n : ℕ) {x : D} (hx : x ∈ U) (hn : x ∉ K n) : ParticularWaveAssembly.residualSource c u b G A j n =ᶠ[nhds x] fun (x : D) => 0

The source has a genuine zero neighborhood at every uncovered point of the open strip. Only incoming coefficient support on that strip is used.

theorem NavierStokes.HarmonicSourceSupport.zero_complementJets_of_germs {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_1} {I : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData D) (w : ℕ → D → ℝ) (α : ℝ) (K : ℕ → I → Set D) (f : ℕ → D → E) (hg : ∀ (n : ℕ), ∀ x ∈ s.domain, (∀ (i : I), x ∉ K n i) → f n =ᶠ[nhds x] fun (x : D) => 0) : PeriodizedWaveBounds.ComplementJets s w α K f

theorem NavierStokes.HarmonicSourceSupport.residualSource_zero_complementJets {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) {I : Type u_1} (K : PeriodizedWaveBounds.Cells D I) (s : WeightedClasses.StripData D) (hs : InputSupportOn s.domain (fun (n : ℕ) => ⋃ (i : I), K.carrier n i) b G A) (j : ℤ) (w : ℕ → D → ℝ) (α : ℝ) : PeriodizedWaveBounds.ComplementJets s w α K.carrier (ParticularWaveAssembly.residualSource c u b G A j)

theorem NavierStokes.HarmonicSourceSupport.residualSource_complementJets_on {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (G A : HarmonicResidual.BlockCoefficients D) {I : Type u_1} (K : PeriodizedWaveBounds.Cells D I) (s : WeightedClasses.StripData D) (hv : ∀ (n : ℕ) (i : Fin 3), NonzeroSupportedOn s.domain (⋃ (a : I), K.carrier n a) (HarmonicResidual.realCoefficients (b.velocity n i))) (hp : ∀ (n : ℕ), NonzeroSupportedOn s.domain (⋃ (a : I), K.carrier n a) (HarmonicResidual.realCoefficients (b.pressure n))) (j : ℤ) {w : ℕ → D → ℝ} {α : ℝ} (he : WeightedClasses.MemClass s w α (excludedSource G A j)) : PeriodizedWaveBounds.ComplementJets s w α K.carrier (ParticularWaveAssembly.residualSource c u b G A j)

If an excluded nonzero tail is present outside the native cells, its actual class supplies the complement estimate. The source is not replaced by zero there.

theorem NavierStokes.HarmonicSourceSupport.coefficient_nativeSupport_of_field {P : Type} (c : HarmonicFields.Coefficients (P × TorusInverse.Plane)) (k : ℝ) (Φ : P × TorusInverse.Plane → ℝ) {kp : ℤ} (hkp : kp ≠ 0) (g : CommonCoverSolve.Geometry) (K : Set TorusInverse.Plane) {U : Set (P × TorusInverse.Plane)} (level : ℕ) (slot : Set TorusInverse.Plane) (Y : P × TorusInverse.Plane → TorusInverse.Plane) (hcoord : ∀ x ∈ U, (CommonCoverSolve.coverPower g.gap) x.2 = (SlotGeometry.cover ^ level) (Y x)) (hslot : slot ⊆ (fun (v : TorusInverse.Plane) => g.center + g.basis v) '' K) (hf : ∀ x ∈ U, ∀ (θ : ℝ), (HarmonicFields.field c k Φ kp (x, θ)).re ≠ 0 → Y x ∈ SlotGeometry.liftedSupport level slot) : NonzeroSupportedOn U (nativeUnion g K) (HarmonicResidual.realCoefficients c)

Angular extraction and the actual coordinate identity transfer support in a geometric native slot to support in the union of all copy cells.

theorem NavierStokes.HarmonicSourceSupport.block_velocity_nativeSupport {P : Type} {ι : Type u_1} {d h : ℝ} {vr vt : TorusInverse.Plane} (sys : PartitionedCovariance.SlotSystem d h vr vt) (label : ℕ → ι → SlotColoring.Label) (χ : ℕ → P × TorusInverse.Plane → LabelSumBounds.WindowPoint) (Y : ℕ → P × TorusInverse.Plane → TorusInverse.Plane) {U : Set (P × TorusInverse.Plane)} (b : ι → CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (hb : LabelSumBounds.SupportedOscillations sys label χ Y U fun (l : ι) => (b l).oscillation) (l : ι) (n : ℕ) (hkp : (b l).angularFrequency n ≠ 0) (g : CommonCoverSolve.Geometry) (K : Set TorusInverse.Plane) (hcoord : ∀ x ∈ U, (CommonCoverSolve.coverPower g.gap) x.2 = (SlotGeometry.cover ^ SlotColoring.nativeIndex h (label n l).1) (Y n x)) (hslot : PartitionedCovariance.slotSet h sys.radius vr vt (label n l) ⊆ (fun (v : TorusInverse.Plane) => g.center + g.basis v) '' K) (i : Fin 3) : NonzeroSupportedOn U (nativeUnion g K) (HarmonicResidual.realCoefficients ((b l).velocity n i))

theorem NavierStokes.HarmonicSourceSupport.InputSupportOn.of_native_fields {P : Type} (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (g : ℕ → CommonCoverSolve.Geometry) (K : ℕ → Set TorusInverse.Plane) {U : Set (P × TorusInverse.Plane)} (level : ℕ → ℕ) (slot : ℕ → Set TorusInverse.Plane) (Y : ℕ → P × TorusInverse.Plane → TorusInverse.Plane) (hkp : ∀ (n : ℕ), b.angularFrequency n ≠ 0) (hcoord : ∀ (n : ℕ), ∀ x ∈ U, (CommonCoverSolve.coverPower (g n).gap) x.2 = (SlotGeometry.cover ^ level n) (Y n x)) (hslot : ∀ (n : ℕ), slot n ⊆ (fun (v : TorusInverse.Plane) => (g n).center + (g n).basis v) '' K n) (hv : ∀ (n : ℕ), ∀ x ∈ U, ∀ (θ : ℝ) (i : Fin 3), b.oscillation n (x, θ) i ≠ 0 → Y n x ∈ SlotGeometry.liftedSupport (level n) (slot n)) (hp : ∀ (n : ℕ), ∀ x ∈ U, ∀ (θ : ℝ), b.oscillatoryPressure n (x, θ) ≠ 0 → Y n x ∈ SlotGeometry.liftedSupport (level n) (slot n)) (hG : ∀ (n : ℕ), ∀ x ∈ U, ∀ (θ : ℝ) (i : Fin 3), (HarmonicResidual.vectorField (G n) (b.frequency n) (b.phase n) (b.angularFrequency n) (x, θ) i).re ≠ 0 → Y n x ∈ SlotGeometry.liftedSupport (level n) (slot n)) (hA : ∀ (n : ℕ), ∀ x ∈ U, ∀ (θ : ℝ) (i : Fin 3), (HarmonicResidual.vectorField (A n) (b.frequency n) (b.phase n) (b.angularFrequency n) (x, θ) i).re ≠ 0 → Y n x ∈ SlotGeometry.liftedSupport (level n) (slot n)) : InputSupportOn U (fun (n : ℕ) => nativeUnion (g n) (K n)) b G A

theorem NavierStokes.HarmonicSourceSupport.sourceFamily_zero_germ_on {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (g : ℕ → CommonCoverSolve.Geometry) (K : ℕ → Set TorusInverse.Plane) (hK : ∀ (n : ℕ), IsCompact (K n)) {U : Set (P × TorusInverse.Plane)} (hU : IsOpen U) (hs : InputSupportOn U (fun (n : ℕ) => nativeUnion (g n) (K n)) b G A) (j : ℤ) (n : ℕ) {x : (P × ℝ) × TorusInverse.Plane} (hx : (x.1.1, x.2) ∈ U) (hn : ∀ (k : TorusInverse.Frequency), x ∉ PeriodizedWaveBounds.nativeCell (g n) (K n) k) : ParticularWaveAssembly.sourceFamily c u b G A j n =ᶠ[nhds x] fun (x : (P × ℝ) × TorusInverse.Plane) => 0

theorem NavierStokes.HarmonicSourceSupport.sourceFamily_zero_complementJets {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (c : CorrectionState.Context (P × TorusInverse.Plane)) (u : CorrectionState.State (P × TorusInverse.Plane)) (b : CorrectionState.HarmonicBlock (P × TorusInverse.Plane)) (G A : HarmonicResidual.BlockCoefficients (P × TorusInverse.Plane)) (g : ℕ → CommonCoverSolve.Geometry) (K : ℕ → Set TorusInverse.Plane) (hK : ∀ (n : ℕ), IsCompact (K n)) {U : Set (P × TorusInverse.Plane)} (hU : IsOpen U) (hs : InputSupportOn U (fun (n : ℕ) => nativeUnion (g n) (K n)) b G A) (s : WeightedClasses.StripData ((P × ℝ) × TorusInverse.Plane)) (hdom : ∀ x ∈ s.domain, (x.1.1, x.2) ∈ U) (j : ℤ) (w : ℕ → (P × ℝ) × TorusInverse.Plane → ℝ) (α : ℝ) : PeriodizedWaveBounds.ComplementJets s w α (fun (n : ℕ) => PeriodizedWaveBounds.nativeCell (g n) (K n)) (ParticularWaveAssembly.sourceFamily c u b G A j)

This is the source-complement input for the global Gaussian estimate on the full angular lift. It has every exponent with constant zero, and does not assert support or regularity outside the incoming open strip.

Unrestricted zero modes and the exact excluded-tail obstruction

theorem NavierStokes.HarmonicSourceSupport.realCoefficient_eq_zero_of_field_constant {D : Type} (c : HarmonicFields.Coefficients D) (k : ℝ) (Φ : D → ℝ) {kp : ℤ} (hkp : kp ≠ 0) {j : ℤ} (hj : j ≠ 0) (x : D) (m : ℝ) (hf : ∀ (θ : ℝ), (HarmonicFields.field c k Φ kp (x, θ)).re = m) : (HarmonicResidual.realCoefficients c).coeff j x = 0

theorem NavierStokes.HarmonicSourceSupport.realCoefficients_supportedOn_of_field_constant {D : Type} (c : HarmonicFields.Coefficients D) (k : ℝ) (Φ : D → ℝ) {kp : ℤ} (hkp : kp ≠ 0) {U K : Set D} (hf : ∀ x ∈ U, x ∉ K → ∃ (m : ℝ), ∀ (θ : ℝ), (HarmonicFields.field c k Φ kp (x, θ)).re = m) : NonzeroSupportedOn U K (HarmonicResidual.realCoefficients c)

Outside the slot, the real field may have any angularly constant part. Only its nonzero Fourier modes are constrained.

theorem NavierStokes.HarmonicSourceSupport.zero_wave_unlocalized_error {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (b : CorrectionState.HarmonicBlock D) (n : ℕ) (hv : ∀ (i : Fin 3), b.velocity n i = 0) (hp : b.pressure n = 0) (x : D) : ParticularWaveAssembly.residualSource c u b (fun (x : ℕ) (x_1 : Fin 3) => AddMonoidAlgebra.single 1 fun (x : D) => 1) 0 1 n x = fun (x : Fin 3) => -2⁻¹

An explicit obstruction to dropping the excluded-source condition: even a zero wave and zero pressure leave a nonzero residual if the stored Gaussian family contains an unlocalized first harmonic.