The physical activation data give the scaled initial conditions.

theorem EulerPacketMovingFrame.scaledRay_initial {m v r : ℝ → EulerSmoothLimit.Space} {s₀ t₀ a ε : ℝ} (hs₀ : s₀ ≠ 0) (hm0 : m t₀ ≠ 0) (hv0 : v t₀ ≠ 0) (hmv : inner ℝ (m t₀) (v t₀) = 0) (hr : r t₀ = s₀ • EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit (m t₀)) (EulerPacketNormalizedPrimary.unit (v t₀))) : scaledRay m v r s₀ t₀ a ε 0 = ![0, 0, 1]

theorem EulerPacketMovingFrame.activation_scaled_velocity {m v w : ℝ → EulerSmoothLimit.Space} {t₀ a ε C γ : ℝ} (hε : 0 < ε) (hγlo : -C ≤ γ) (hγhi : γ ≤ 0) (hp : inner ℝ (EulerPacketNormalizedPrimary.unit (m t₀)) (w t₀) = γ) (hq : inner ℝ (EulerPacketNormalizedPrimary.unit (v t₀)) (w t₀) = 1) : 0 ≤ -γ / ε ∧ -γ / ε ≤ C / ε ∧ scaledVelocity m v w t₀ a ε 0 0 = -(-γ / ε) ∧ scaledVelocity m v w t₀ a ε 0 1 = 1

The signed physical p component in (26) becomes a nonnegative scalar initial slope, with the expected factor ε⁻¹.

theorem EulerPacketMovingFrame.activation_tangent_pairing {m v r w : ℝ → EulerSmoothLimit.Space} {s₀ t₀ : ℝ} (hr : r t₀ = s₀ • EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit (m t₀)) (EulerPacketNormalizedPrimary.unit (v t₀))) (hw : inner ℝ (EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit (m t₀)) (EulerPacketNormalizedPrimary.unit (v t₀))) (w t₀) = 0) : inner ℝ (r t₀) (w t₀) = 0