Actual smooth representatives of the closed divergence-free space have pointwise lifted divergence zero.

theorem EulerClassicalDivergence.divergenceFree_classical_divergence_zero (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : u ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hrep : ↑↑u =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ∑ i : Fin 3, (EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection κ m i) g x).ofLp i = 0

A genuine smooth representative of a weakly lifted-divergence-free L² field has zero pointwise lifted divergence.