The coefficient equations of the literal assembled packet give the force in (14).

theorem EulerPacketResidual.assembled_fast_pressure {Q : Type u_2} {W : Type u_3} [AddCommGroup Q] [Module ℝ Q] [AddCommGroup W] [Module ℝ W] (N p : ℕ) (hp : p ≤ N) (H : Q →ₗ[ℝ] W) (q π : ℕ → Q) (hq : ∀ i ≤ N, H (q i) = 0) : H (EulerFiniteGrades.assemble N q π (p + 1)) = H (π p)

theorem EulerPacketResidual.coefficient_assembled {V : Type u_1} {Q : Type u_2} {W : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup Q] [Module ℝ Q] [AddCommGroup W] [Module ℝ W] (N p : ℕ) (hp : 1 ≤ p) (hpN : p ≤ N) (L : V →ₗ[ℝ] W) (G H : Q →ₗ[ℝ] W) (B C : V →ₗ[ℝ] V →ₗ[ℝ] W) (a b c : ℕ → V) (q π : ℕ → Q) (hq : ∀ i ≤ N, H (q i) = 0) : coefficient (N + 1) L G H B C (EulerFiniteGrades.assemble N (fun (i : ℕ) => a i + b i) c) (EulerFiniteGrades.assemble N q π) p = L (a p) + H (π p) + (L (b p) + G (q p)) + (L (c (p - 1)) + G (π (p - 1))) + EulerFiniteGrades.convolution (N + 1) B (EulerFiniteGrades.assemble N (fun (i : ℕ) => a i + b i) c) (EulerFiniteGrades.assemble N (fun (i : ℕ) => a i + b i) c) p + EulerFiniteGrades.convolution (N + 1) C (EulerFiniteGrades.assemble N (fun (i : ℕ) => a i + b i) c) (EulerFiniteGrades.assemble N (fun (i : ℕ) => a i + b i) c) (p + 1)

Both pressure contributions and the final corrector are retained in this identity.

theorem EulerPacketResidual.coefficient_assembled_eq_zero {V : Type u_1} {Q : Type u_2} {W : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup Q] [Module ℝ Q] [AddCommGroup W] [Module ℝ W] (N p : ℕ) (hp : 1 ≤ p) (hpN : p ≤ N) (L : V →ₗ[ℝ] W) (G H : Q →ₗ[ℝ] W) (B C : V →ₗ[ℝ] V →ₗ[ℝ] W) (a b c : ℕ → V) (q π : ℕ → Q) (hq : ∀ i ≤ N, H (q i) = 0) (fmean : W) (hmean : L (b p) + G (q p) = fmean) (hhigh : L (a p) + H (π p) = -(L (c (p - 1)) + G (π (p - 1)) + EulerFiniteGrades.convolution (N + 1) B (EulerFiniteGrades.assemble N (fun (i : ℕ) => a i + b i) c) (EulerFiniteGrades.assemble N (fun (i : ℕ) => a i + b i) c) p + EulerFiniteGrades.convolution (N + 1) C (EulerFiniteGrades.assemble N (fun (i : ℕ) => a i + b i) c) (EulerFiniteGrades.assemble N (fun (i : ℕ) => a i + b i) c) (p + 1)) - fmean) : coefficient (N + 1) L G H B C (EulerFiniteGrades.assemble N (fun (i : ℕ) => a i + b i) c) (EulerFiniteGrades.assemble N q π) p = 0

The two actual linear equations imply cancellation; no residual equation is assumed.

theorem EulerPacketResidual.coefficient_zero_grade {V : Type u_1} {Q : Type u_2} {W : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup Q] [Module ℝ Q] [AddCommGroup W] [Module ℝ W] (N : ℕ) (L : V →ₗ[ℝ] W) (G H : Q →ₗ[ℝ] W) (B C : V →ₗ[ℝ] V →ₗ[ℝ] W) (u : ℕ → V) (q : ℕ → Q) (hu0 : u 0 = 0) (hq0 : G (q 0) = 0) (hq1 : H (q 1) = 0) : coefficient (N + 1) L G H B C u q 0 = 0