Structure preserved by actual harmonic block addition

The carrier-retaining sum is the actual HarmonicWaveInteraction.addBlock. Smoothness of its input coefficient functions justifies linearity of the Fréchet derivatives in the cylindrical divergence. No output divergence condition, nonzero frequency, or nonzero angular frequency is assumed.

theorem NavierStokes.HarmonicStructurePreservation.amplitude_addBlock {D : Type} (a b : CorrectionState.HarmonicBlock D) (j : ℤ) (n : ℕ) : HarmonicWaveInteraction.amplitude (HarmonicWaveInteraction.addBlock a b) j n = HarmonicWaveInteraction.amplitude a j n + HarmonicWaveInteraction.amplitude b j n

theorem NavierStokes.HarmonicStructurePreservation.amplitude_withCarrier {D : Type} (a b : CorrectionState.HarmonicBlock D) (j : ℤ) (n : ℕ) : HarmonicWaveInteraction.amplitude (HarmonicWaveInteraction.withCarrier a b) j n = HarmonicWaveInteraction.amplitude b j n

theorem NavierStokes.HarmonicStructurePreservation.singleMode_addBlock {D : Type} (a b : CorrectionState.HarmonicBlock D) (j : ℤ) (n : ℕ) : HarmonicWaveInteraction.singleMode (HarmonicWaveInteraction.addBlock a b) j n = HarmonicWaveInteraction.singleMode a j n + HarmonicWaveInteraction.singleMode (HarmonicWaveInteraction.withCarrier a b) j n

The complex single Fourier fields add before any real projection or differentiation. This identity also holds at harmonic zero.

theorem NavierStokes.HarmonicStructurePreservation.withCarrier_eq {D : Type} {a b : CorrectionState.HarmonicBlock D} (hfrequency : b.frequency = a.frequency) (hphase : b.phase = a.phase) (hangular : b.angularFrequency = a.angularFrequency) : HarmonicWaveInteraction.withCarrier a b = b

theorem NavierStokes.HarmonicStructurePreservation.singleMode_addBlock_of_sameCarrier {D : Type} {a b : CorrectionState.HarmonicBlock D} (hfrequency : b.frequency = a.frequency) (hphase : b.phase = a.phase) (hangular : b.angularFrequency = a.angularFrequency) (j : ℤ) (n : ℕ) : HarmonicWaveInteraction.singleMode (HarmonicWaveInteraction.addBlock a b) j n = HarmonicWaveInteraction.singleMode a j n + HarmonicWaveInteraction.singleMode b j n

theorem NavierStokes.HarmonicStructurePreservation.amplitude_contDiffOn {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {b : CorrectionState.HarmonicBlock D} (hb : ∀ (n : ℕ) (i : Fin 3), HarmonicResidual.SmoothCoefficients U (b.velocity n i)) (j : ℤ) (n : ℕ) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (x : D) => HarmonicWaveInteraction.amplitude b j n x i) U

theorem NavierStokes.HarmonicStructurePreservation.singleMode_contDiffOn {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {b : CorrectionState.HarmonicBlock D} (hb : ∀ (n : ℕ) (i : Fin 3), HarmonicResidual.SmoothCoefficients U (b.velocity n i)) (hphase : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (b.phase n) U) (j : ℤ) (n : ℕ) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (p : D × ℝ) => HarmonicWaveInteraction.singleMode b j n p i) (HarmonicResidual.liftDomain U)

theorem NavierStokes.HarmonicStructurePreservation.cylindricalDivergence_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) {a b : E → HarmonicCalculus.ComplexVector} {x : E} (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => a y i) x) (hb : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => b y i) x) : HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz (a + b) x = HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz a x + HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz b x

Additivity uses actual differentiability of all components at the evaluation point. The geometric direction fields need no derivatives.

theorem NavierStokes.HarmonicStructurePreservation.velocity_smooth_addBlock {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {a b : CorrectionState.HarmonicBlock D} (ha : ∀ (n : ℕ) (i : Fin 3), HarmonicResidual.SmoothCoefficients U (a.velocity n i)) (hb : ∀ (n : ℕ) (i : Fin 3), HarmonicResidual.SmoothCoefficients U (b.velocity n i)) (n : ℕ) (i : Fin 3) : HarmonicResidual.SmoothCoefficients U ((HarmonicWaveInteraction.addBlock a b).velocity n i)

theorem NavierStokes.HarmonicStructurePreservation.pressure_smooth_addBlock {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {a b : CorrectionState.HarmonicBlock D} (ha : ∀ (n : ℕ), HarmonicResidual.SmoothCoefficients U (a.pressure n)) (hb : ∀ (n : ℕ), HarmonicResidual.SmoothCoefficients U (b.pressure n)) (n : ℕ) : HarmonicResidual.SmoothCoefficients U ((HarmonicWaveInteraction.addBlock a b).pressure n)

theorem NavierStokes.HarmonicStructurePreservation.phase_smooth_addBlock {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {a b : CorrectionState.HarmonicBlock D} (ha : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) U) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((HarmonicWaveInteraction.addBlock a b).phase n) U

theorem NavierStokes.HarmonicStructurePreservation.modeSolenoidal_addBlock_withCarrier {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {c : CorrectionState.Context D} {a b : CorrectionState.HarmonicBlock D} (ha : ∀ (n : ℕ) (i : Fin 3), HarmonicResidual.SmoothCoefficients s.domain (a.velocity n i)) (hb : ∀ (n : ℕ) (i : Fin 3), HarmonicResidual.SmoothCoefficients s.domain (b.velocity n i)) (hphase : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hda : HarmonicWaveInteraction.ModeSolenoidal s c a) (hdb : HarmonicWaveInteraction.ModeSolenoidal s c (HarmonicWaveInteraction.withCarrier a b)) : HarmonicWaveInteraction.ModeSolenoidal s c (HarmonicWaveInteraction.addBlock a b)

The carrier-retaining sum preserves modewise solenoidality when the second input is interpreted on the retained carrier.

theorem NavierStokes.HarmonicStructurePreservation.modeSolenoidal_addBlock {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {c : CorrectionState.Context D} {a b : CorrectionState.HarmonicBlock D} (hfrequency : b.frequency = a.frequency) (hphase_eq : b.phase = a.phase) (hangular : b.angularFrequency = a.angularFrequency) (ha : ∀ (n : ℕ) (i : Fin 3), HarmonicResidual.SmoothCoefficients s.domain (a.velocity n i)) (hb : ∀ (n : ℕ) (i : Fin 3), HarmonicResidual.SmoothCoefficients s.domain (b.velocity n i)) (hphase : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (a.phase n) s.domain) (hda : HarmonicWaveInteraction.ModeSolenoidal s c a) (hdb : HarmonicWaveInteraction.ModeSolenoidal s c b) : HarmonicWaveInteraction.ModeSolenoidal s c (HarmonicWaveInteraction.addBlock a b)

Actual addition of two smooth solenoidal blocks on a common carrier preserves the same primitive solenoidality condition on the same strip.

theorem NavierStokes.HarmonicStructurePreservation.zeroMode_addBlock {D : Type} {a b : CorrectionState.HarmonicBlock D} (ha : HarmonicWaveInteraction.ZeroMode a) (hb : HarmonicWaveInteraction.ZeroMode b) : HarmonicWaveInteraction.ZeroMode (HarmonicWaveInteraction.addBlock a b)

The velocity zero-mode condition is preserved coefficientwise, as an identity of actual coefficient functions.

theorem NavierStokes.HarmonicStructurePreservation.zeroPressure_addBlock {D : Type} {a b : CorrectionState.HarmonicBlock D} (ha : ∀ (n : ℕ), (a.pressure n).coeff 0 = 0) (hb : ∀ (n : ℕ), (b.pressure n).coeff 0 = 0) (n : ℕ) : ((HarmonicWaveInteraction.addBlock a b).pressure n).coeff 0 = 0

Pressure has the same algebraic preservation without any derivative or regularity assumptions.

theorem NavierStokes.HarmonicStructurePreservation.zeroMode_withCarrier {D : Type} {a b : CorrectionState.HarmonicBlock D} (hb : HarmonicWaveInteraction.ZeroMode b) : HarmonicWaveInteraction.ZeroMode (HarmonicWaveInteraction.withCarrier a b)

theorem NavierStokes.HarmonicStructurePreservation.zeroPressure_withCarrier {D : Type} {a b : CorrectionState.HarmonicBlock D} (hb : ∀ (n : ℕ), (b.pressure n).coeff 0 = 0) (n : ℕ) : ((HarmonicWaveInteraction.withCarrier a b).pressure n).coeff 0 = 0