The constructed exact lifted packet gives the actual momentum equation after the genuine parent-flow change of coordinates. The scalar pressure is the normalized radial potential of the constructed pressure tower.

The frame evolution is derived by differentiating the actual parent flow. Symmetry of the genuine second derivative supplies the mixed-derivative identity; no independent strain evolution is assumed.

theorem EulerPacketPhysicalTransform.flow_time_derivative_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (X u : ℝ × E → E) (q : ℝ × E) (hX : DifferentiableAt ℝ X q) (hflow : HasDerivAt (fun (s : ℝ) => X (s, q.2)) (u (q.1, X q)) q.1) : (fderiv ℝ X q) (1, 0) = u (q.1, X q)

theorem EulerPacketPhysicalTransform.parent_frame_time {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (X u : ℝ × E → E) (F : ℝ × E → E →L[ℝ] E) (q : ℝ × E) (DF : ℝ × E →L[ℝ] E →L[ℝ] E) (Du : ℝ × E →L[ℝ] E) (hX : ContDiffAt ℝ 2 X q) (hF : HasFDerivAt F DF q) (hu : HasFDerivAt u Du (q.1, X q)) (hframe : F =ᶠ[nhds q] fun (r : ℝ × E) => fderiv ℝ X r ∘SL ContinuousLinearMap.inr ℝ ℝ E) (hflow : (fun (r : ℝ × E) => (fderiv ℝ X r) (1, 0)) =ᶠ[nhds q] fun (r : ℝ × E) => u (r.1, X r)) (v : E) : (DF (1, 0)) v = Du (0, (F q) v)

theorem EulerPacketPhysicalTransform.physical_euler_momentum_of_flow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (κ k : ℝ) (hκ : k * κ = 1) (m : E) (F : ℝ × E → E →L[ℝ] E) (z : ℝ × E × ℝ → E) (u : ℝ × E → E) (p Q : ℝ × E → ℝ) (X Y : ℝ × E → E) (t : ℝ) (x : E) (A : E ≃L[ℝ] E) (DF : ℝ × E →L[ℝ] E →L[ℝ] E) (Dz : ℝ × E × ℝ →L[ℝ] E) (Du : ℝ × E →L[ℝ] E) (P : E) (hleft : ∀ (s : ℝ) (y : E), Y (s, X (s, y)) = y) (hY : DifferentiableAt ℝ (inverseCoordinates Y) (t, X (t, x))) (hX : ContDiffAt ℝ 2 X (t, x)) (hframe : F =ᶠ[nhds (t, x)] fun (r : ℝ × E) => fderiv ℝ X r ∘SL ContinuousLinearMap.inr ℝ ℝ E) (hflow : (fun (r : ℝ × E) => (fderiv ℝ X r) (1, 0)) =ᶠ[nhds (t, x)] fun (r : ℝ × E) => u (r.1, X r)) (hF : HasFDerivAt F DF (t, x)) (hz : HasFDerivAt z Dz ((spaceTimeGraph k m) (t, x))) (hA : F (t, x) = ↑A) (hu : HasFDerivAt u Du (t, X (t, x))) (hp : DifferentiableAt ℝ (fun (y : E) => p (t, y)) (X (t, x))) (hQ : DifferentiableAt ℝ (fun (y : E) => Q (t, y)) x) (hQgradient : gradient (fun (y : E) => Q (t, y)) x = κ • P) (hparent : EulerLagrangian.momentumResidual u p (t, X (t, x)) = 0) (hlift : Dz (1, 0, 0) + 2 • A.symm ((DF (1, 0)) (z ((spaceTimeGraph k m) (t, x)))) + Dz (0, κ • z ((spaceTimeGraph k m) (t, x)), inner ℝ m (z ((spaceTimeGraph k m) (t, x)))) + κ • A.symm ((DF (0, z ((spaceTimeGraph k m) (t, x)))) (z ((spaceTimeGraph k m) (t, x)))) + A.symm ((ContinuousLinearMap.adjoint ↑A.symm) P) = 0) : EulerLagrangian.momentumResidual (fun (q : ℝ × E) => u q + physicalVelocity κ k m F z Y q) (fun (q : ℝ × E) => p q + physicalPressure Q Y q) (t, X (t, x)) = 0

The usual flow ODE and Jacobian identity suffice to supply the frame evolution used by the physical Euler transformation. The identities need only hold in a neighborhood of the current interior spacetime point.

theorem EulerPacketPhysicalTransform.exact_source_momentum {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P D.T} {B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData D P κ hκ Z R)} (S : EulerAllOrderDriftCorrection.ExactLiftedPacket P ⋯ (EulerPacketCorrectionCoefficients.correctionData D P κ hκ Z R) B) (k : ℝ) (hk : k * κ = 1) (F : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (p : ℝ × EulerSmoothLimit.Space → ℝ) (X Y : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hmatch : ∀ (s : ↑(Set.Icc 0 D.T)) (y : EulerSmoothLimit.Space), F (↑s, y) = (D.F.field s) y) (t : ℝ) (ht : t ∈ Set.Ioo 0 D.T) (x : EulerSmoothLimit.Space) (hleft : ∀ (s : ℝ) (y : EulerSmoothLimit.Space), Y (s, X (s, y)) = y) (hY : DifferentiableAt ℝ (inverseCoordinates Y) (t, X (t, x))) (hX : ContDiffAt ℝ 2 X (t, x)) (hframe : F =ᶠ[nhds (t, x)] fun (r : ℝ × EulerSmoothLimit.Space) => fderiv ℝ X r ∘SL ContinuousLinearMap.inr ℝ ℝ EulerSmoothLimit.Space) (hflow : (fun (r : ℝ × EulerSmoothLimit.Space) => (fderiv ℝ X r) (1, 0)) =ᶠ[nhds (t, x)] fun (r : ℝ × EulerSmoothLimit.Space) => u (r.1, X r)) (hu : DifferentiableAt ℝ u (t, X (t, x))) (hp : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => p (t, y)) (X (t, x))) (hparent : EulerLagrangian.momentumResidual u p (t, X (t, x)) = 0) : EulerLagrangian.momentumResidual (fun (q : ℝ × EulerSmoothLimit.Space) => u q + physicalVelocity κ k D.m₀ F S.rawVelocity Y q) (fun (q : ℝ × EulerSmoothLimit.Space) => p q + physicalPressure (S.rawGraphPotential k) Y q) (t, X (t, x)) = 0

All derivatives and the pressure of the perturbation are constructed from the exact lifted solution. Only the actual parent flow and its inverse enter as geometric data.