The actual scalar average-zero condition gives literal pointwise zero angular mean.

theorem EulerCylinderScalarPrimitive.scalar_mean_zero (P : ℝ) [Fact (0 < P)] (u : ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ)) (hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) u) (f : EulerLiftedGradientSpace.LiftDomain P → ℝ) (hf : Continuous f) (hrep : ↑↑u =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) (hz : (EulerCylinderAngleAverage.average P) u = 0) (y : EulerSmoothLimit.Space) : ∫ (s : ℝ) in 0..P, f (y, ↑s) = 0

No pointwise mean-zero condition is assumed for the representative: it follows from the zero average of the actual scalar L² class.