The actual scalar L² primitive represents the classical pressure integral

The fixed scalar embedding has a norm-one left inverse. Applying the already proved vector H3 evaluation theorem to this embedding identifies the actual scalar L² primitive with the literal normalized periodic integral.

theorem EulerCylinderScalarPrimitive.embed_smooth (P : ℝ) [Fact (0 < P)] (u : ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ)) (hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) u) : EulerCylinderSmoothOrbit.SmoothOrbit P ((embed P) u)

theorem EulerCylinderScalarPrimitive.primitive_ae_classical (P : ℝ) [Fact (0 < P)] (u : ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ)) (hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) u) (f q : EulerLiftedGradientSpace.LiftDomain P → ℝ) (hf : Continuous f) (hrep : ↑↑u =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, f (y, ↑s) = 0) (hq : ∀ (y : EulerSmoothLimit.Space) (θ : ℝ), q (y, ↑θ) = EulerAngleMeanZeroPrimitive.primitive P (fun (s : ℝ) => f (y, ↑s)) θ) : ↑↑((primitive P) u) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] q

The vector H3 reconstruction theorem transfers to the actual scalar primitive.

theorem EulerCylinderScalarPrimitive.primitive_ae_constructed (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) (hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, f (y, ↑s) = 0) : ↑↑((primitive P) u) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] classicalPrimitive P f hf hmean

The actual scalar primitive is exactly the descended normalized integral.