The literal raw curl-corrector equals the genuine periodic Piola corrector.

theorem EulerPacketCylinderField.rawMean_pointField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {raw : EulerPacketProfileRecursion.VectorField} (G : Field P D.T raw) (t : ↑(Set.Icc 0 D.T)) (hm : ∀ (x : EulerSmoothLimit.Space), ∫ (θ : ℝ) in 0..P, raw (↑t, x, θ) = 0) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, EulerCylinderSmoothOrbit.pointField P G.path ⋯ t (x, ↑θ) = 0

theorem EulerPacketCylinderField.rawCorrector_eq_lifted {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {raw : EulerPacketProfileRecursion.VectorField} (G : Field P D.T raw) (t : ↑(Set.Icc 0 D.T)) (hm : ∀ (x : EulerSmoothLimit.Space), ∫ (θ : ℝ) in 0..P, raw (↑t, x, θ) = 0) (x : EulerSmoothLimit.Space) (θ : ℝ) : D.curlCorrector P raw (↑t, x, θ) = EulerPacketConstructedPiola.corrector P (D.deformationEquiv t) D.m₀ (EulerCylinderSmoothOrbit.pointField P G.path ⋯ t) (x, ↑θ)