Actual packet word bounds give the finite weighted Sobolev budgets used by the nonlinear correction, with no change to the spatial radius.

theorem EulerPacketCylinderField.Field.WordBound.toFieldTower_weightedNorm_le {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) (s N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (t : ↑(Set.Icc 0 T)) : EulerSobolevGevreyOperators.weightedNorm P q N ρ ((G.toFieldTower.realization s) t) ≤ A * ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerGevrey.majorant R d n

theorem EulerPacketCylinderField.Field.WordBound.toFieldTower_weightedDerivativeNorm_le {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) (s N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (t : ↑(Set.Icc 0 T)) : ∑ i : Fin 4, EulerSobolevGevreyOperators.weightedNorm P q N ρ ((EulerCylinderSobolevSpace.derivativeOperator P s i) ((G.toFieldTower.realization (s + 1)) t)) ≤ A * ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerGevrey.majorant R (d + 1) n

theorem EulerPacketCylinderField.Field.weight_majorant_zero (ρ R : ℝ) (n : ℕ) : EulerPacketWeights.weight ρ n * EulerGevrey.majorant R 0 n = (ρ * R) ^ n

theorem EulerPacketCylinderField.Field.weight_majorant_one (ρ R : ℝ) (n : ℕ) : EulerPacketWeights.weight ρ n * EulerGevrey.majorant R 1 n = R * ((ρ * R) ^ n * ↑(n + 1) ^ 2)

theorem EulerPacketCylinderField.Field.square_geometric_le_twelve (r : ℝ) (hr : 0 ≤ r) (hrhalf : r ≤ 1 / 2) (N : ℕ) : ∑ n ∈ Finset.range N, r ^ n * ↑(n + 1) ^ 2 ≤ 12

theorem EulerPacketCylinderField.Field.WordBound.toFieldTower_weightedNorm_le_two {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q : ℕ} {R A : ℝ} (hG : G.WordBound q R A 0) (hR : 0 ≤ R) (hA : 0 ≤ A) (s N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (hsmall : ρ * R ≤ 1 / 2) (t : ↑(Set.Icc 0 T)) : EulerSobolevGevreyOperators.weightedNorm P q N ρ ((G.toFieldTower.realization s) t) ≤ 2 * A

The unshifted all-order packet estimate yields a cutoff-independent background or residual budget, with the original word radius R.

theorem EulerPacketCylinderField.Field.WordBound.toFieldTower_weightedDerivativeNorm_le_twelve {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q : ℕ} {R A : ℝ} (hG : G.WordBound q R A 0) (hR : 0 ≤ R) (hA : 0 ≤ A) (s N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (hsmall : ρ * R ≤ 1 / 2) (t : ↑(Set.Icc 0 T)) : ∑ i : Fin 4, EulerSobolevGevreyOperators.weightedNorm P q N ρ ((EulerCylinderSobolevSpace.derivativeOperator P s i) ((G.toFieldTower.realization (s + 1)) t)) ≤ 12 * A * R

All four actual derivative budgets together cost 12AR, independent of the cutoff and with no extra alphabet factor.