The transported primary has zero normal component, so the actual normal drift is small.
theorem
EulerPacketCylinderField.ProfileRegularity.normalizedNormal_bound
{P T : ℝ}
[Fact (0 < P)]
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{support : Set EulerSmoothLimit.Space}
(hT : 0 < T)
(G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ support (a i))
{S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)}
{R : ℝ}
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → ProfileBudget (G i hi) S R i)
(hR : 1 ≤ R)
(ha : a 0 = 0)
(hb : (a 1).mean = 0)
(hN : 1 ≤ N)
{O : EulerPacketProfileRecursion.Operators}
{C : CoefficientData P T O}
(BC : CoefficientBudget C)
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R)
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ ≤ 1)
(htan :
∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ),
inner ℝ m ((O.inverseFrame (↑t, x, θ)) ((a 1).high (↑t, x, θ))) = 0)
(k : ℝ)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase R S.H0 BC.termCost N ≤ k ^ (1 / 100))
:
(((C.inverse.multiply (velocityField hT G k⁻¹)).smul k).map (normalComponentMap m)).WordBound 6 (4 * R)
(BC.multiplierCost * (fixedVelocityGradeCost R S.H0 2 + 2) / k) 0