Uniform estimates for finite coefficient assembly, including zero and terminal grades.

theorem EulerPacketCylinderField.Field.wordBound_truncateFamily {P T : ℝ} [Fact (0 < P)] (M : ℕ) (f : ℕ → EulerPacketProfileRecursion.VectorField) (G : (i : ℕ) → i ≤ M → Field P T (f i)) (q : ℕ) (R : ℝ) (A : ℕ → ℝ) (d : ℕ → ℕ) (hR : 0 ≤ R) (hA : ∀ (i : ℕ), 0 ≤ A i) (hG : ∀ (i : ℕ) (hi : i ≤ M), (G i hi).WordBound q R (A i) (d i)) (n : ℕ) : (truncateFamily M f G n).WordBound q R (A n) (d n)

theorem EulerPacketCylinderField.Field.wordBound_assembleFamily {P T : ℝ} [Fact (0 < P)] (M : ℕ) (f c : ℕ → EulerPacketProfileRecursion.VectorField) (G : (i : ℕ) → i ≤ M → Field P T (f i)) (H : (i : ℕ) → i ≤ M → Field P T (c i)) (R A : ℝ) (hR : 1 ≤ R) (hA : 1 ≤ A) (hG : ∀ (i : ℕ) (hi : i ≤ M), (G i hi).WordBound 6 R (2 * A ^ (2 * i)) (EulerPacketShiftArithmetic.highShift i)) (hH : ∀ (i : ℕ) (hi : i ≤ M), (H i hi).WordBound 6 R (A ^ (2 * i)) (EulerPacketShiftArithmetic.highShift i)) (n : ℕ) : (assembleFamily M f c G H n).WordBound 6 R (3 * A ^ (2 * n)) (EulerPacketShiftArithmetic.highShift n)