Uniform estimates for the actual harmonic interaction

The finite-jet constants are chosen before the spatial label and band. The nonlinear estimate uses exact mode solenoidality to remove the phase normal. Only the fixed signed harmonic ratio remains in that cancellation.

noncomputable def NavierStokes.UniformHarmonicInteraction.UniformVelocity {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (P : ι → ℕ → D → ℝ) (α : ℝ) (a : ι → CorrectionState.HarmonicBlock D) : Prop

Uniform input classes for each fixed signed Fourier mode and physical component. The label and band are inside the uniform estimate.

Equations

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

theorem NavierStokes.UniformHarmonicInteraction.waveBounds_each {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {α : ℝ} {a : ι → CorrectionState.HarmonicBlock D} (ha : UniformVelocity s P α a) (l : ι) : CorrectionState.HarmonicBlock.WaveBounds s (P l) α (a l)

theorem NavierStokes.UniformHarmonicInteraction.cmul {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w v : ι → ℕ → D → ℝ} {α β : ℝ} {f g : ι → ℕ → D → ℂ} (hf : LabelSumBounds.UniformClass s w α f) (hg : LabelSumBounds.UniformClass s v β g) : LabelSumBounds.UniformClass s (fun (l : ι) (n : ℕ) (x : D) => w l n x * v l n x) (α + β) fun (l : ι) (n : ℕ) (x : D) => f l n x * g l n x

theorem NavierStokes.UniformHarmonicInteraction.div_radius {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α κ : ℝ} (G : WaveInteractionBounds.Geometry s κ) {f : ι → ℕ → D → ℂ} (hf : LabelSumBounds.UniformClass s w α f) : LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => f l n x / ↑(G.radius n x)

theorem NavierStokes.UniformHarmonicInteraction.generator {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α : ℝ} {a : ι → WaveInteractionBounds.Family D} (ha : ∀ (i : Fin 3), LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => a l n x i) (i : Fin 3) : LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => HarmonicCalculus.angularGenerator (a l n x) i

theorem NavierStokes.UniformHarmonicInteraction.strippedTransport_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w v : ι → ℕ → D → ℝ} {α β κ : ℝ} (G : WaveInteractionBounds.Geometry s κ) (hκ : 0 ≤ κ) {a b : ι → WaveInteractionBounds.Family D} (ha : ∀ (i : Fin 3), LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => a l n x i) (hb : ∀ (i : Fin 3), LabelSumBounds.UniformClass s v β fun (l : ι) (n : ℕ) (x : D) => b l n x i) (i : Fin 3) : LabelSumBounds.UniformClass s (fun (l : ι) (n : ℕ) (x : D) => w l n x * v l n x) (α + β - κ) fun (l : ι) (n : ℕ) (x : D) => WaveInteractionBounds.strippedTransport G (a l) (b l) n x i

theorem NavierStokes.UniformHarmonicInteraction.strippedDivergence_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ι → ℕ → D → ℝ} {α κ : ℝ} (G : WaveInteractionBounds.Geometry s κ) (hκ : 0 ≤ κ) {a : ι → WaveInteractionBounds.Family D} (ha : ∀ (i : Fin 3), LabelSumBounds.UniformClass s w α fun (l : ι) (n : ℕ) (x : D) => a l n x i) : LabelSumBounds.UniformClass s w (α - κ) fun (l : ι) (n : ℕ) => HarmonicCalculus.strippedDivergence (G.radius n) (G.radial n) (G.axial n) (a l n)

theorem NavierStokes.UniformHarmonicInteraction.orderedKernel_eq_cancelled {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β : ℝ} {P : ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {a b : CorrectionState.HarmonicBlock D} (ha : CorrectionState.HarmonicBlock.WaveBounds s P α a) (hb : CorrectionState.HarmonicBlock.WaveBounds s P β b) (hΦ : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hk : ∀ (n : ℕ), a.frequency n ≠ 0) (hdiv : HarmonicWaveInteraction.ModeSolenoidal s c a) {j m : ℤ} (hj : j ≠ 0) (hm : m ≠ 0) (n : ℕ) {x : D} (hx : x ∈ s.domain) (i : Fin 3) : HarmonicWaveInteraction.orderedKernel (HarmonicResidual.contextFrame c n) (a.frequency n) (a.phase n) (a.angularFrequency n) m (HarmonicWaveInteraction.amplitude a j n) (HarmonicWaveInteraction.amplitude b m n) x i = WaveInteractionBounds.strippedTransport (HarmonicMeanInteraction.slowGeometry c ho hR) (HarmonicWaveInteraction.amplitude a j) (HarmonicWaveInteraction.amplitude b m) n x i + (↑m / ↑j) • -HarmonicCalculus.strippedDivergence ((HarmonicMeanInteraction.slowGeometry c ho hR).radius n) ((HarmonicMeanInteraction.slowGeometry c ho hR).radial n) ((HarmonicMeanInteraction.slowGeometry c ho hR).axial n) (HarmonicWaveInteraction.amplitude a j n) x * HarmonicWaveInteraction.amplitude b m n x i

Exact cancellation for the literal ordered harmonic coefficient. The output contains no phase normal and no carrier magnitude.

theorem NavierStokes.UniformHarmonicInteraction.blockAmplitude_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {α : ℝ} {P : ι → ℕ → D → ℝ} {a : ι → CorrectionState.HarmonicBlock D} (ha : UniformVelocity s P α a) {j : ℤ} (hj : j ≠ 0) (i : Fin 3) : LabelSumBounds.UniformWaveClass s P α fun (l : ι) (n : ℕ) (x : D) => HarmonicWaveInteraction.amplitude (a l) j n x i

theorem NavierStokes.UniformHarmonicInteraction.orderedKernel_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β : ℝ} {P : ι → ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {a b : ι → CorrectionState.HarmonicBlock D} (ha : UniformVelocity s P α a) (hb : UniformVelocity s P β b) (hΦ : ∀ (l : ι) (n : ℕ), ContDiffOn ℝ (↑⊤) ((a l).phase n) s.domain) (hk : ∀ (l : ι) (n : ℕ), (a l).frequency n ≠ 0) (hdiv : ∀ (l : ι), HarmonicWaveInteraction.ModeSolenoidal s c (a l)) {j m : ℤ} (hj : j ≠ 0) (hm : m ≠ 0) (i : Fin 3) : LabelSumBounds.UniformClass s (fun (l : ι) (n : ℕ) (x : D) => √(s.zeta x) * P l n x * (√(s.zeta x) * P l n x)) (α + β - κ) fun (l : ι) (n : ℕ) (x : D) => HarmonicWaveInteraction.orderedKernel (HarmonicResidual.contextFrame c n) ((a l).frequency n) ((a l).phase n) ((a l).angularFrequency n) m (HarmonicWaveInteraction.amplitude (a l) j n) (HarmonicWaveInteraction.amplitude (b l) m n) x i

The genuine ordered coefficient has a uniform class before summing harmonics. No quantitative assumption on the phase normal is used.

theorem NavierStokes.UniformHarmonicInteraction.orderedKernel_uniform_all {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β : ℝ} {P : ι → ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {a b : ι → CorrectionState.HarmonicBlock D} (ha : UniformVelocity s P α a) (hb : UniformVelocity s P β b) (ha0 : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (a l)) (hb0 : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (b l)) (hΦ : ∀ (l : ι) (n : ℕ), ContDiffOn ℝ (↑⊤) ((a l).phase n) s.domain) (hk : ∀ (l : ι) (n : ℕ), (a l).frequency n ≠ 0) (hdiv : ∀ (l : ι), HarmonicWaveInteraction.ModeSolenoidal s c (a l)) (j m : ℤ) (i : Fin 3) : LabelSumBounds.UniformClass s (fun (l : ι) (n : ℕ) (x : D) => √(s.zeta x) * P l n x * (√(s.zeta x) * P l n x)) (α + β - κ) fun (l : ι) (n : ℕ) (x : D) => HarmonicWaveInteraction.orderedKernel (HarmonicResidual.contextFrame c n) ((a l).frequency n) ((a l).phase n) ((a l).angularFrequency n) m (HarmonicWaveInteraction.amplitude (a l) j n) (HarmonicWaveInteraction.amplitude (b l) m n) x i

Zero input modes contribute exactly zero, so the uniform ordered estimate applies to every signed pair of Fourier indices.

theorem NavierStokes.UniformHarmonicInteraction.transport_uniform_raw {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β : ℝ} {P : ι → ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {a b : ι → CorrectionState.HarmonicBlock D} {M : ℕ} (ha : UniformVelocity s P α a) (hb : UniformVelocity s P β b) (ha0 : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (a l)) (hb0 : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (b l)) (hM : ∀ (l : ι), (a l).BandLimited M) (hΦ : ∀ (l : ι) (n : ℕ), ContDiffOn ℝ (↑⊤) ((a l).phase n) s.domain) (hk : ∀ (l : ι) (n : ℕ), (a l).frequency n ≠ 0) (hdiv : ∀ (l : ι), HarmonicWaveInteraction.ModeSolenoidal s c (a l)) (m : ℤ) (i : Fin 3) : LabelSumBounds.UniformClass s (fun (l : ι) (n : ℕ) (x : D) => √(s.zeta x) * P l n x * (√(s.zeta x) * P l n x)) (α + β - κ) fun (l : ι) (n : ℕ) (x : D) => (HarmonicResidual.transport (HarmonicResidual.contextFrame c n) ((a l).frequency n) ((a l).phase n) ((a l).angularFrequency n) (HarmonicMeanInteraction.blockAmplitude (a l) n) (HarmonicMeanInteraction.blockAmplitude (b l) n) i).coeff m x

Only the common harmonic band is summed. The number of spatial labels does not enter the constants.

theorem NavierStokes.UniformHarmonicInteraction.square_weight_wave {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ι → ℕ → D → ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ} {f : ι → ℕ → D → E} (hf : LabelSumBounds.UniformClass s (fun (l : ι) (n : ℕ) (x : D) => √(s.zeta x) * P l n x * (√(s.zeta x) * P l n x)) γ f) (hζ : ∀ x ∈ s.domain, s.zeta x ≤ 1) (hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x) (hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1) : LabelSumBounds.UniformWaveClass s P γ f

theorem NavierStokes.UniformHarmonicInteraction.transport_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β : ℝ} {P : ι → ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {a b : ι → CorrectionState.HarmonicBlock D} {M : ℕ} (ha : UniformVelocity s P α a) (hb : UniformVelocity s P β b) (ha0 : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (a l)) (hb0 : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (b l)) (hM : ∀ (l : ι), (a l).BandLimited M) (hΦ : ∀ (l : ι) (n : ℕ), ContDiffOn ℝ (↑⊤) ((a l).phase n) s.domain) (hk : ∀ (l : ι) (n : ℕ), (a l).frequency n ≠ 0) (hdiv : ∀ (l : ι), HarmonicWaveInteraction.ModeSolenoidal s c (a l)) (hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x) (hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1) (m : ℤ) (i : Fin 3) : LabelSumBounds.UniformWaveClass s P (α + β - κ) fun (l : ι) (n : ℕ) (x : D) => (HarmonicResidual.transport (HarmonicResidual.contextFrame c n) ((a l).frequency n) ((a l).phase n) ((a l).angularFrequency n) (HarmonicMeanInteraction.blockAmplitude (a l) n) (HarmonicMeanInteraction.blockAmplitude (b l) n) i).coeff m x

theorem NavierStokes.UniformHarmonicInteraction.mixed_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β : ℝ} {P : ι → ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {a b : ι → CorrectionState.HarmonicBlock D} {M N : ℕ} (ha : UniformVelocity s P α a) (hb : UniformVelocity s P β b) (ha0 : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (a l)) (hb0 : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (b l)) (hM : ∀ (l : ι), (a l).BandLimited M) (hN : ∀ (l : ι), (b l).BandLimited N) (hΦ : ∀ (l : ι) (n : ℕ), ContDiffOn ℝ (↑⊤) ((a l).phase n) s.domain) (hk : ∀ (l : ι) (n : ℕ), (a l).frequency n ≠ 0) (hda : ∀ (l : ι), HarmonicWaveInteraction.ModeSolenoidal s c (a l)) (hdb : ∀ (l : ι), HarmonicWaveInteraction.ModeSolenoidal s c (HarmonicWaveInteraction.withCarrier (a l) (b l))) (hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x) (hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1) (m : ℤ) (i : Fin 3) : LabelSumBounds.UniformWaveClass s P (α + β - κ) fun (l : ι) (n : ℕ) (x : D) => (HarmonicWaveInteraction.blockTransport c (a l) (a l) (b l) n i).coeff m x + (HarmonicWaveInteraction.blockTransport c (a l) (b l) (a l) n i).coeff m x

theorem NavierStokes.UniformHarmonicInteraction.square_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ β : ℝ} {P : ι → ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) (a : ι → CorrectionState.HarmonicBlock D) {b : ι → CorrectionState.HarmonicBlock D} {N : ℕ} (hb : UniformVelocity s P β b) (hb0 : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (b l)) (hN : ∀ (l : ι), (b l).BandLimited N) (hΦ : ∀ (l : ι) (n : ℕ), ContDiffOn ℝ (↑⊤) ((a l).phase n) s.domain) (hk : ∀ (l : ι) (n : ℕ), (a l).frequency n ≠ 0) (hdb : ∀ (l : ι), HarmonicWaveInteraction.ModeSolenoidal s c (HarmonicWaveInteraction.withCarrier (a l) (b l))) (hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x) (hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1) (m : ℤ) (i : Fin 3) : LabelSumBounds.UniformWaveClass s P (2 * β - κ) fun (l : ι) (n : ℕ) (x : D) => (HarmonicWaveInteraction.blockTransport c (a l) (b l) (b l) n i).coeff m x

theorem NavierStokes.UniformHarmonicInteraction.nonlinearCoefficients_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β : ℝ} {P : ι → ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {a b : ι → CorrectionState.HarmonicBlock D} {M N : ℕ} (ha : UniformVelocity s P α a) (hb : UniformVelocity s P β b) (ha0 : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (a l)) (hb0 : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (b l)) (hM : ∀ (l : ι), (a l).BandLimited M) (hN : ∀ (l : ι), (b l).BandLimited N) (hΦ : ∀ (l : ι) (n : ℕ), ContDiffOn ℝ (↑⊤) ((a l).phase n) s.domain) (hk : ∀ (l : ι) (n : ℕ), (a l).frequency n ≠ 0) (hda : ∀ (l : ι), HarmonicWaveInteraction.ModeSolenoidal s c (a l)) (hdb : ∀ (l : ι), HarmonicWaveInteraction.ModeSolenoidal s c (HarmonicWaveInteraction.withCarrier (a l) (b l))) (hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x) (hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1) (m : ℤ) (i : Fin 3) : LabelSumBounds.UniformWaveClass s P (min (α + β - κ) (2 * β - κ)) fun (l : ι) (n : ℕ) (x : D) => (HarmonicWaveInteraction.nonlinearCoefficients c (a l) (b l) n i).coeff m x

The literal three-term nonlinear update has a uniform class over all labels, with the mixed and self-interaction exponents both retained.

theorem NavierStokes.UniformHarmonicInteraction.interactionBlock_uniform {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ α β μ : ℝ} {P : ι → ℕ → D → ℝ} (c : CorrectionState.Context D) (ho : MeanIncrementBounds.OperatorBounds s c.operators κ) (hκ : κ ≤ 1 / 2) (hR : ∀ x ∈ s.domain, 0 < c.operators.radius x) {u : CorrectionState.State D} (hmean : MeanIncrementBounds.IncrementBounds s μ u.mean) {a b : ι → CorrectionState.HarmonicBlock D} {M N : ℕ} (ha : UniformVelocity s P α a) (hb : UniformVelocity s P β b) (ha0 : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (a l)) (hb0 : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (b l)) (hM : ∀ (l : ι), (a l).BandLimited M) (hN : ∀ (l : ι), (b l).BandLimited N) (hΦ : ∀ (l : ι) (n : ℕ), ContDiffOn ℝ (↑⊤) ((a l).phase n) s.domain) (hk : ∀ (l : ι) (n : ℕ), (a l).frequency n ≠ 0) (hda : ∀ (l : ι), HarmonicWaveInteraction.ModeSolenoidal s c (a l)) (hdb : ∀ (l : ι), HarmonicWaveInteraction.ModeSolenoidal s c (HarmonicWaveInteraction.withCarrier (a l) (b l))) {C : ℕ → ι → Set D} (hNormal : ∀ (i : Fin 3), LocalizedWaveBounds.LocalUnweighted s C 0 fun (n : ℕ) (l : ι) (x : D) => (HarmonicMeanInteraction.slowNormal c ho hR (a l).phase n x).ofLp i) (hFreq : LocalizedWaveBounds.LocalUnweighted s C (-(1 / 2)) fun (n : ℕ) (l : ι) (x : D) => (a l).frequency n) (hAng : LocalizedWaveBounds.LocalUnweighted s C (-(1 / 2)) fun (n : ℕ) (l : ι) (x : D) => ↑((a l).angularFrequency n)) (hz : ∀ (n : ℕ) (l : ι), ∀ x ∈ s.domain, x ∉ C n l → ∀ (i : Fin 3) (j : ℤ), j ≠ 0 → ((b l).velocity n i).coeff j =ᶠ[nhds x] fun (x : D) => 0) (hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, 0 ≤ P l n x) (hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ s.domain, P l n x ≤ 1) {j : ℤ} (hj : j ≠ 0) (i : Fin 3) : LabelSumBounds.UniformClass s (fun (l : ι) (n : ℕ) (x : D) => √(s.zeta x) * P l n x) (min (β + μ - 1 / 2) (min (α + β - κ) (2 * β - κ))) fun (l : ι) (n : ℕ) (x : D) => ((HarmonicWaveInteraction.interactionBlock c u (a l) (b l)).velocity n i).coeff j x

The actual interaction block, including the unchanged state's mean, has one finite-jet bound uniform over labels and bands. Phase normals and frequencies are required only on the genuine support patch of each wave.

theorem NavierStokes.UniformHarmonicInteraction.interactionBlock_structure {D : Type} {ι : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (c : CorrectionState.Context D) (u : CorrectionState.State D) (a b : ι → CorrectionState.HarmonicBlock D) {M N : ℕ} (hM : ∀ (l : ι), (a l).BandLimited M) (hN : ∀ (l : ι), (b l).BandLimited N) (l : ι) : (HarmonicWaveInteraction.interactionBlock c u (a l) (b l)).BandLimited (max (M + N) (N + N)) ∧ HarmonicWaveInteraction.ZeroMode (HarmonicWaveInteraction.interactionBlock c u (a l) (b l)) ∧ (HarmonicWaveInteraction.interactionBlock c u (a l) (b l)).frequency = (a l).frequency ∧ (HarmonicWaveInteraction.interactionBlock c u (a l) (b l)).phase = (a l).phase ∧ (HarmonicWaveInteraction.interactionBlock c u (a l) (b l)).angularFrequency = (a l).angularFrequency

The same expression is still a genuine finite harmonic block, with zero constant mode and the original carrier. This is independent of the estimates and uses the exact coefficient constructors.