Exact identification of the limiting actual metric forcing with the seven spatial correction terms.

theorem EulerEnergyForcingIdentity.transportOperator_of_value_eq (period : ℝ) [Fact (0 < period)] {p q : ℕ} (hp : 3 ≤ p) (hq : 3 ≤ q) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period p)) (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (huv : EulerCylinderSobolevSpace.value period u = EulerCylinderSobolevSpace.value period v) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) : (EulerSobolevMetricTransport.transportOperator period hp κ m u) e = (EulerSobolevMetricTransport.transportOperator period hq κ m v) e

The actual H¹→L² transport depends only on the underlying velocity field, independently of its Sobolev order.

theorem EulerEnergyForcingIdentity.metric_topTransport (period : ℝ) [Fact (0 < period)] {s N : ℕ} (hs : 6 ≤ s) (hN : N + 6 ≤ s) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (z : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (hzu : EulerCylinderSobolevSpace.value period z = EulerCylinderSobolevSpace.value period u) (I : EulerGevreyMetricComparison.ExternalWord N) (a : EulerBaseWordMetric.BaseWord 6) : (EulerSobolevMetricTransport.transportOperator period ⋯ κ m z) ((EulerMildTopWord.boundedWordBlock period 1 (EulerEnergyWordCoordinates.energyLength I a) ⋯ (EulerEnergyWordCoordinates.energyWord I a)) v) = EulerGevreyDifferentiatedEquation.topTransport period N hN (EulerSobolevTransport.velocityComponents κ m) u v I a

The literal metric transport of a concatenated energy word is exactly the top transport in the spatial telescope.

theorem EulerEnergyForcingIdentity.energyValues_neg (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (I : EulerGevreyMetricComparison.ExternalWord N) (a : EulerBaseWordMetric.BaseWord q) : EulerGevreyMetricComparison.energyValues period q N hN (-u) I a = -EulerGevreyMetricComparison.energyValues period q N hN u I a

Negating a genuine Sobolev field negates every exact external/base energy word.

theorem EulerEnergyForcingIdentity.forcing_word_telescope (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (K0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (N : ℕ) (hN : N + 6 ≤ s) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (hL : ∀ (i : Fin 4), ‖EulerSobolevTransport.velocityComponents κ m i‖ ≤ 1) (z : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (hzu : EulerCylinderSobolevSpace.value period z = EulerCylinderSobolevSpace.value period u) (f p0 p1 : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (I : EulerGevreyMetricComparison.ExternalWord N) (a : EulerBaseWordMetric.BaseWord 6) : EulerCylinderSobolevSpace.word period (-(((EulerSobolevTransport.transportBilinear period hs (EulerSobolevTransport.velocityComponents κ m) hL) u) v + f - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period K) p0 - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period K) p1)) ⋯ (EulerEnergyWordCoordinates.energyWord I a) + (EulerSobolevMetricTransport.transportOperator period ⋯ κ m z) ((EulerMildTopWord.boundedWordBlock period 1 (EulerEnergyWordCoordinates.energyLength I a) ⋯ (EulerEnergyWordCoordinates.energyWord I a)) v) + A.operator (EulerCylinderSobolevSpace.word period (-(p0 + p1)) ⋯ (EulerEnergyWordCoordinates.energyWord I a)) = EulerGevreyCorrectionForcing.correctionForcing period hs K K0 N hN (EulerSobolevTransport.velocityComponents κ m) hL u v f p0 p1 I a

The actual source-plus-transport-plus-signed-pressure forcing equals precisely the seven correction terms.