Every genuine derivative word preserves the ordinary Helmholtz constraint, and consequently the pressure pairing vanishes at every order.

theorem EulerOrdinarySobolev.word_toLp_eq_orbit (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {n : ℕ} (w : Fin n → Fin 3) : (wordField A w).toLp = EulerParameterWordGevrey.wordDerivative axis (fun (a : EulerSmoothLimit.Space) => (EulerLpTranslation.translation a) A.toLp) w 0

theorem EulerOrdinarySobolev.projection_word (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {n : ℕ} (w : Fin n → Fin 3) : EulerMeanSolenoidal.solenoidalProjection (wordField A w).toLp = EulerParameterWordGevrey.wordDerivative axis (fun (a : EulerSmoothLimit.Space) => (EulerLpTranslation.translation a) (EulerMeanSolenoidal.solenoidalProjection A.toLp)) w 0

theorem EulerOrdinarySobolev.word_solenoidal (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) {n : ℕ} (w : Fin n → Fin 3) : (wordField A w).toLp ∈ EulerMeanSolenoidal.solenoidalSpace

theorem EulerOrdinarySobolev.word_gradient (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : A.toLp ∈ EulerMeanSolenoidal.gradientSpace) {n : ℕ} (w : Fin n → Fin 3) : (wordField A w).toLp ∈ EulerMeanSolenoidal.gradientSpace

theorem EulerOrdinarySobolev.word_pressure_pairing_zero (P U : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hP : P.toLp ∈ EulerMeanSolenoidal.gradientSpace) (hU : U.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) {n : ℕ} (w : Fin n → Fin 3) : inner ℝ (wordField P w).toLp (wordField U w).toLp = 0