The source's next-frame scalar formulas represent the actual normalized physical ray and velocity. Orientation, physical norms, and pressure numerators are identified exactly before any quantitative estimate is used.

Exact scaled cross and pressure algebra used by physical frame renewal.

theorem EulerPacketMovingFrame.velocityNumerator_homogeneous (A : Fin 3 → Fin 3 → ℝ) (P Q N U V W : ℝ) (hV : V ≠ 0) : EulerPacketRay.velocityNumerator A P Q N U V W = V * EulerPacketRay.velocityNumerator A P Q N (U / V) 1 (W / V)

theorem EulerPacketMovingFrame.scaling_cross_flux {a : ℝ} (ha : a ≠ 0) (s₀ ε : ℝ) (M : Fin 3 → Fin 3 → ℝ) (R V : Fin 3 → ℝ) (hV : V 1 ≠ 0) : ∑ i : Fin 3, (crossProduct fun (j : Fin 3) => s₀ * EulerPacketRay.rayScale ε j * R j) (fun (j : Fin 3) => velocityScale ε j * V j) i * ∑ j : Fin 3, M i j * (velocityScale ε j * V j) = s₀ * a * V 1 ^ 2 * EulerPacketFrameStability.frameCrossNumerator ε (R 0) (R 1) (R 2) (V 0 / V 1) (V 2 / V 1) (EulerPacketFrameStability.rowAction (EulerPacketRay.scaledVelocityEntry a ε M) 0 (V 0 / V 1) (V 2 / V 1)) (EulerPacketFrameStability.rowAction (EulerPacketRay.scaledVelocityEntry a ε M) 1 (V 0 / V 1) (V 2 / V 1)) (EulerPacketFrameStability.rowAction (EulerPacketRay.scaledVelocityEntry a ε M) 2 (V 0 / V 1) (V 2 / V 1))

theorem EulerPacketMovingFrame.scaling_pressure_ratio {a : ℝ} (ha : a ≠ 0) (s₀ ε : ℝ) (M : Fin 3 → Fin 3 → ℝ) (R V : Fin 3 → ℝ) (hV : V 1 ≠ 0) : ∑ i : Fin 3, s₀ * EulerPacketRay.rayScale ε i * R i * ∑ j : Fin 3, M i j * (velocityScale ε j * V j) = s₀ * a * V 1 * EulerPacketRay.velocityNumerator (EulerPacketRay.scaledVelocityEntry a ε M) (R 0) (R 1) (R 2) (V 0 / V 1) 1 (V 2 / V 1)

theorem EulerPacketMovingFrame.physical_pressure_ratio (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m v r w : ℝ → EulerSmoothLimit.Space) {s₀ t₀ a ε τ : ℝ} (ha : a ≠ 0) (hs₀ : s₀ ≠ 0) (hε : ε ≠ 0) (hm : m (physicalTime t₀ a ε τ) ≠ 0) (hv : v (physicalTime t₀ a ε τ) ≠ 0) (hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0) (hV : scaledVelocity m v w t₀ a ε τ 1 ≠ 0) : have R := scaledRay m v r s₀ t₀ a ε τ; have V := scaledVelocity m v w t₀ a ε τ; have A := scaledAction M m v a ε (physicalTime t₀ a ε τ); inner ℝ (r (physicalTime t₀ a ε τ)) (M (w (physicalTime t₀ a ε τ))) = s₀ * a * V 1 * EulerPacketRay.velocityNumerator A (R 0) (R 1) (R 2) (V 0 / V 1) 1 (V 2 / V 1)

theorem EulerPacketMovingFrame.physical_cross_ratio (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m v r w : ℝ → EulerSmoothLimit.Space) {s₀ t₀ a ε τ : ℝ} (ha : a ≠ 0) (hs₀ : s₀ ≠ 0) (hε : ε ≠ 0) (hm : m (physicalTime t₀ a ε τ) ≠ 0) (hv : v (physicalTime t₀ a ε τ) ≠ 0) (hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0) (hV : scaledVelocity m v w t₀ a ε τ 1 ≠ 0) : have R := scaledRay m v r s₀ t₀ a ε τ; have V := scaledVelocity m v w t₀ a ε τ; have A := scaledAction M m v a ε (physicalTime t₀ a ε τ); inner ℝ (EulerPacketCrossProduct.cross (r (physicalTime t₀ a ε τ)) (w (physicalTime t₀ a ε τ))) (M (w (physicalTime t₀ a ε τ))) = s₀ * a * V 1 ^ 2 * EulerPacketFrameStability.frameCrossNumerator ε (R 0) (R 1) (R 2) (V 0 / V 1) (V 2 / V 1) (EulerPacketFrameStability.rowAction A 0 (V 0 / V 1) (V 2 / V 1)) (EulerPacketFrameStability.rowAction A 1 (V 0 / V 1) (V 2 / V 1)) (EulerPacketFrameStability.rowAction A 2 (V 0 / V 1) (V 2 / V 1))

theorem EulerPacketMovingFrame.physical_frame_formulas (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m v r w : ℝ → EulerSmoothLimit.Space) {s₀ t₀ a ε τ : ℝ} (ha : a ≠ 0) (hs₀ : 0 < s₀) (hε : ε ≠ 0) (hm : m (physicalTime t₀ a ε τ) ≠ 0) (hv : v (physicalTime t₀ a ε τ) ≠ 0) (hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0) (hr : r (physicalTime t₀ a ε τ) ≠ 0) (hV : 0 < scaledVelocity m v w t₀ a ε τ 1) : have R := scaledRay m v r s₀ t₀ a ε τ; have V := scaledVelocity m v w t₀ a ε τ; have A := scaledAction M m v a ε (physicalTime t₀ a ε τ); have D := EulerPacketRay.rayDenominator ε (R 0) (R 1) (R 2); have E := EulerPacketFrameStability.velocityDirectionNormSq ε (V 0 / V 1) (V 2 / V 1); have J := EulerPacketRay.velocityNumerator A (R 0) (R 1) (R 2) (V 0 / V 1) 1 (V 2 / V 1); have C := EulerPacketFrameStability.frameCrossNumerator ε (R 0) (R 1) (R 2) (V 0 / V 1) (V 2 / V 1) (EulerPacketFrameStability.rowAction A 0 (V 0 / V 1) (V 2 / V 1)) (EulerPacketFrameStability.rowAction A 1 (V 0 / V 1) (V 2 / V 1)) (EulerPacketFrameStability.rowAction A 2 (V 0 / V 1) (V 2 / V 1)); normalizedCoupling M (r (physicalTime t₀ a ε τ)) (w (physicalTime t₀ a ε τ)) / a = J / (√D * √E) ∧ normalizedTilt M (r (physicalTime t₀ a ε τ)) (w (physicalTime t₀ a ε τ)) = C / (J * √E)

Exact source (34) quantities for the actual next normalized frame.