The actual projected velocity equation after the source scaling, with its pressure numerator and denominator identified exactly. The first two rows therefore feed the existing scalar-amplification estimates.

The actual projected primary-velocity ODE in the normalized moving frame.

theorem EulerPacketMovingFrame.frameSkew_antisymm (B : Fin 3 → Fin 3 → ℝ) (i j : Fin 3) : EulerPacketRay.frameSkew B j i = -EulerPacketRay.frameSkew B i j

theorem EulerPacketMovingFrame.frameMatrix_adjoint (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q : EulerSmoothLimit.Space) (i j : Fin 3) : frameMatrix (ContinuousLinearMap.adjoint B) p q i j = frameMatrix B p q j i

theorem EulerPacketMovingFrame.frame_action (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q x : EulerSmoothLimit.Space) (hp : inner ℝ p p = 1) (hq : inner ℝ q q = 1) (hpq : inner ℝ p q = 0) (i : Fin 3) : ∑ j : Fin 3, frameMatrix M p q i j * inner ℝ (frame p q j) x = inner ℝ (frame p q i) (M x)

theorem EulerPacketMovingFrame.frame_norm_sq (p q x : EulerSmoothLimit.Space) (hp : inner ℝ p p = 1) (hq : inner ℝ q q = 1) (hpq : inner ℝ p q = 0) : ∑ j : Fin 3, inner ℝ (frame p q j) x ^ 2 = ‖x‖ ^ 2

theorem EulerPacketMovingFrame.frame_flux (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q r w : EulerSmoothLimit.Space) (hp : inner ℝ p p = 1) (hq : inner ℝ q q = 1) (hpq : inner ℝ p q = 0) : ∑ i : Fin 3, inner ℝ (frame p q i) r * ∑ j : Fin 3, frameMatrix M p q i j * inner ℝ (frame p q j) w = inner ℝ r (M w)

theorem EulerPacketMovingFrame.movingVelocityRate_identity (B M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q w : EulerSmoothLimit.Space) (hp : inner ℝ p p = 1) (hq : inner ℝ q q = 1) (hpq : inner ℝ p q = 0) (i : Fin 3) : -inner ℝ (frame p q i) (M w) + inner ℝ (frameRate B p q i) w = -∑ j : Fin 3, (frameMatrix M p q i j + EulerPacketRay.frameSkew (frameMatrix B p q) i j) * inner ℝ (frame p q j) w

noncomputable def EulerPacketMovingFrame.movingVelocity (m v w : ℝ → EulerSmoothLimit.Space) (t : ℝ) (i : Fin 3) : ℝ

Moving velocity, given by ⟪normalizedFrame m v t i,w t⟫_ℝ.

Equations

• EulerPacketMovingFrame.movingVelocity m v w t i = inner ℝ (EulerPacketMovingFrame.normalizedFrame m v t i) (w t)

noncomputable def EulerPacketMovingFrame.movingFlux (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m v r w : ℝ → EulerSmoothLimit.Space) (t : ℝ) : ℝ

Moving flux, given by ∑ i : Fin 3, movingRay m v r t i * (∑ j : Fin 3, frameMatrix M (unit (m t)) (unit (v t)) i j * movingVelocity m v w t j).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerPacketMovingFrame.movingDenominator (m v r : ℝ → EulerSmoothLimit.Space) (t : ℝ) : ℝ

Moving denominator, given by ∑ j : Fin 3, (movingRay m v r t j)^2.

Equations

• EulerPacketMovingFrame.movingDenominator m v r t = ∑ j : Fin 3, EulerPacketMovingFrame.movingRay m v r t j ^ 2

theorem EulerPacketMovingFrame.movingFlux_eq (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m v r w : ℝ → EulerSmoothLimit.Space) (t : ℝ) (hm : m t ≠ 0) (hv : v t ≠ 0) (hmv : inner ℝ (m t) (v t) = 0) : movingFlux M m v r w t = inner ℝ (r t) (M (w t))

theorem EulerPacketMovingFrame.movingDenominator_eq (m v r : ℝ → EulerSmoothLimit.Space) (t : ℝ) (hm : m t ≠ 0) (hv : v t ≠ 0) (hmv : inner ℝ (m t) (v t) = 0) : movingDenominator m v r t = ‖r t‖ ^ 2

theorem EulerPacketMovingFrame.moving_pairing (m v r w : ℝ → EulerSmoothLimit.Space) (t : ℝ) (hm : m t ≠ 0) (hv : v t ≠ 0) (hmv : inner ℝ (m t) (v t) = 0) : ∑ j : Fin 3, movingRay m v r t j * movingVelocity m v w t j = inner ℝ (r t) (w t)

theorem EulerPacketMovingFrame.movingVelocity_hasDerivWithinAt (B M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) {m v r w : ℝ → EulerSmoothLimit.Space} {t : ℝ} {S : Set ℝ} (hm : HasDerivWithinAt m (-(ContinuousLinearMap.adjoint B) (m t)) S t) (hv : HasDerivWithinAt v (-B (v t) + (2 * inner ℝ (m t) (B (v t)) / ‖m t‖ ^ 2) • m t) S t) (hw : HasDerivWithinAt w (-M (w t) + (2 * inner ℝ (r t) (M (w t)) / ‖r t‖ ^ 2) • r t) S t) (hm0 : m t ≠ 0) (hv0 : v t ≠ 0) (hmv : inner ℝ (m t) (v t) = 0) (i : Fin 3) : HasDerivWithinAt (fun (s : ℝ) => movingVelocity m v w s i) (-∑ j : Fin 3, (frameMatrix M (EulerPacketNormalizedPrimary.unit (m t)) (EulerPacketNormalizedPrimary.unit (v t)) i j + EulerPacketRay.frameSkew (frameMatrix B (EulerPacketNormalizedPrimary.unit (m t)) (EulerPacketNormalizedPrimary.unit (v t))) i j) * movingVelocity m v w t j + 2 * movingFlux M m v r w t / movingDenominator m v r t * movingRay m v r t i) S t

The physical projected ODE becomes the exact -(M+S) moving-frame equation, with its actual scalar pressure flux and denominator.

noncomputable def EulerPacketMovingFrame.scaledVelocity (m v w : ℝ → EulerSmoothLimit.Space) (t₀ a ε τ : ℝ) (i : Fin 3) : ℝ

Scaled velocity, given by movingVelocity m v w (physicalTime t₀ a ε τ) i / velocityScale ε i.

Equations

• EulerPacketMovingFrame.scaledVelocity m v w t₀ a ε τ i = EulerPacketMovingFrame.movingVelocity m v w (EulerPacketMovingFrame.physicalTime t₀ a ε τ) i / EulerPacketMovingFrame.velocityScale ε i

theorem EulerPacketMovingFrame.scaledRay_restore (m v r : ℝ → EulerSmoothLimit.Space) {s₀ t₀ a ε τ : ℝ} (hs₀ : s₀ ≠ 0) (hε : ε ≠ 0) (i : Fin 3) : s₀ * EulerPacketRay.rayScale ε i * scaledRay m v r s₀ t₀ a ε τ i = movingRay m v r (physicalTime t₀ a ε τ) i

theorem EulerPacketMovingFrame.scaledVelocity_restore (m v w : ℝ → EulerSmoothLimit.Space) {t₀ a ε τ : ℝ} (hε : ε ≠ 0) (i : Fin 3) : velocityScale ε i * scaledVelocity m v w t₀ a ε τ i = movingVelocity m v w (physicalTime t₀ a ε τ) i

noncomputable def EulerPacketMovingFrame.scaledAction (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m v : ℝ → EulerSmoothLimit.Space) (a ε t : ℝ) : Fin 3 → Fin 3 → ℝ

Scaled action, given by scaledVelocityEntry a ε (frameMatrix M (unit (m t)) (unit (v t))).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerPacketMovingFrame.scaledTransport (B M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m v : ℝ → EulerSmoothLimit.Space) (a ε t : ℝ) : Fin 3 → Fin 3 → ℝ

Scaled transport, constructed using scaledVelocityEntry.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerPacketMovingFrame.movingDenominator_scaling (m v r : ℝ → EulerSmoothLimit.Space) {s₀ t₀ a ε τ : ℝ} (hs₀ : s₀ ≠ 0) (hε : ε ≠ 0) : movingDenominator m v r (physicalTime t₀ a ε τ) = s₀ ^ 2 * EulerPacketRay.rayDenominator ε (scaledRay m v r s₀ t₀ a ε τ 0) (scaledRay m v r s₀ t₀ a ε τ 1) (scaledRay m v r s₀ t₀ a ε τ 2)

theorem EulerPacketMovingFrame.movingFlux_scaling (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m v r w : ℝ → EulerSmoothLimit.Space) {s₀ t₀ a ε τ : ℝ} (ha : a ≠ 0) (hs₀ : s₀ ≠ 0) (hε : ε ≠ 0) : movingFlux M m v r w (physicalTime t₀ a ε τ) = s₀ * a * EulerPacketRay.velocityNumerator (scaledAction M m v a ε (physicalTime t₀ a ε τ)) (scaledRay m v r s₀ t₀ a ε τ 0) (scaledRay m v r s₀ t₀ a ε τ 1) (scaledRay m v r s₀ t₀ a ε τ 2) (scaledVelocity m v w t₀ a ε τ 0) (scaledVelocity m v w t₀ a ε τ 1) (scaledVelocity m v w t₀ a ε τ 2)

theorem EulerPacketMovingFrame.scaled_pairing_zero (m v r w : ℝ → EulerSmoothLimit.Space) {s₀ t₀ a ε τ : ℝ} (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) (hrw : inner ℝ (r (physicalTime t₀ a ε τ)) (w (physicalTime t₀ a ε τ)) = 0) : scaledRay m v r s₀ t₀ a ε τ 0 * scaledVelocity m v w t₀ a ε τ 0 + scaledRay m v r s₀ t₀ a ε τ 1 * scaledVelocity m v w t₀ a ε τ 1 + scaledRay m v r s₀ t₀ a ε τ 2 * scaledVelocity m v w t₀ a ε τ 2 = 0

theorem EulerPacketMovingFrame.scaled_denominator_ne_zero (m v r : ℝ → EulerSmoothLimit.Space) {s₀ t₀ a ε τ : ℝ} (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) (hr : r (physicalTime t₀ a ε τ) ≠ 0) : EulerPacketRay.rayDenominator ε (scaledRay m v r s₀ t₀ a ε τ 0) (scaledRay m v r s₀ t₀ a ε τ 1) (scaledRay m v r s₀ t₀ a ε τ 2) ≠ 0

theorem EulerPacketMovingFrame.scaledVelocity_hasDerivWithinAt (B M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) {m v r w : ℝ → EulerSmoothLimit.Space} {s₀ t₀ a ε τ : ℝ} {S U : Set ℝ} (ha : a ≠ 0) (hε : ε ≠ 0) (hs₀ : s₀ ≠ 0) (hmap : Set.MapsTo (physicalTime t₀ a ε) U S) (hm : HasDerivWithinAt m (-(ContinuousLinearMap.adjoint B) (m (physicalTime t₀ a ε τ))) S (physicalTime t₀ a ε τ)) (hv : HasDerivWithinAt v (-B (v (physicalTime t₀ a ε τ)) + (2 * inner ℝ (m (physicalTime t₀ a ε τ)) (B (v (physicalTime t₀ a ε τ))) / ‖m (physicalTime t₀ a ε τ)‖ ^ 2) • m (physicalTime t₀ a ε τ)) S (physicalTime t₀ a ε τ)) (hw : HasDerivWithinAt w (-M (w (physicalTime t₀ a ε τ)) + (2 * inner ℝ (r (physicalTime t₀ a ε τ)) (M (w (physicalTime t₀ a ε τ))) / ‖r (physicalTime t₀ a ε τ)‖ ^ 2) • r (physicalTime t₀ a ε τ)) S (physicalTime t₀ a ε τ)) (hm0 : m (physicalTime t₀ a ε τ) ≠ 0) (hv0 : v (physicalTime t₀ a ε τ) ≠ 0) (hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0) (hr0 : r (physicalTime t₀ a ε τ) ≠ 0) (i : Fin 3) : HasDerivWithinAt (fun (σ : ℝ) => scaledVelocity m v w t₀ a ε σ i) (scaledVelocityRhs (scaledAction M m v a ε (physicalTime t₀ a ε τ)) (scaledTransport B M m v a ε (physicalTime t₀ a ε τ)) ε (scaledRay m v r s₀ t₀ a ε τ) (scaledVelocity m v w t₀ a ε τ) i) U τ

The actual three scaled velocity coordinates satisfy the exact projected system, including the small middle-row pressure factor ε².