The literal residual of the generated finite packet contains only the uncancelled tail.

theorem EulerPacketProfileRecursion.recursive_residual_tail (O : Operators) (A : VectorField) (π : ScalarField) (N : ℕ) (hN : 1 ≤ N) (κ : ℝ) (hκ : κ ≠ 0) (z : EulerPacketPointJets.Domain) (hs : UniqueDiffWithinAt ℝ O.interval z.1) (hA : ∀ (i : ℕ), EulerPacketPointJets.SliceDifferentiable O.interval (profiles O (primaryProfile O A π) i).high z) (hB : ∀ (i : ℕ), EulerPacketPointJets.SliceDifferentiable O.interval (profiles O (primaryProfile O A π) i).mean z) (hC : ∀ (i : ℕ), EulerPacketPointJets.SliceDifferentiable O.interval (profiles O (primaryProfile O A π) i).corrector z) (hq : ∀ (i : ℕ), DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => (profiles O (primaryProfile O A π) i).meanPressure (z.1, y)) z.2) (hπ : ∀ (i : ℕ), DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => (profiles O (primaryProfile O A π) i).highPressure (z.1, y)) z.2) (hqθ : ∀ i ≤ N, (EulerPacketPointJets.fastPressure (O.normal z)) (EulerPacketPointJets.pressureJet (profiles O (primaryProfile O A π) i).meanPressure z) = 0) (htan : inner ℝ (O.normal z) (A z) = 0) (hprimary : (EulerPacketPointJets.linearPart (O.strain z)) (EulerPacketPointJets.slicedJet O.interval A z) + (EulerPacketPointJets.fastPressure (O.normal z)) (EulerPacketPointJets.pressureJet π z) = 0) (hhigh : ∀ (p : ℕ), 2 ≤ p → p ≤ N → inner ℝ (O.normal z) ((profiles O (primaryProfile O A π) p).high z) = 0) (hmeanEquation : ∀ (p : ℕ), 2 ≤ p → p ≤ N → (EulerPacketPointJets.linearPart (O.strain z)) (EulerPacketPointJets.slicedJet O.interval (profiles O (primaryProfile O A π) p).mean z) + (EulerPacketPointJets.slowPressure (O.inverseFrame z)) (EulerPacketPointJets.pressureJet (profiles O (primaryProfile O A π) p).meanPressure z) = meanForce O p (profiles O (primaryProfile O A π)) z) (hhighEquation : ∀ (p : ℕ), 2 ≤ p → p ≤ N → (EulerPacketPointJets.linearPart (O.strain z)) (EulerPacketPointJets.slicedJet O.interval (profiles O (primaryProfile O A π) p).high z) + (EulerPacketPointJets.fastPressure (O.normal z)) (EulerPacketPointJets.pressureJet (profiles O (primaryProfile O A π) p).highPressure z) = highForce O p (profiles O (primaryProfile O A π)) z) : EulerPacketPointJets.slicedMomentumResidual O.interval κ (O.inverseFrame z) (O.strain z) (O.normal z) (EulerPacketPointJets.fieldSum (N + 1) κ (assembledVelocity N (profiles O (primaryProfile O A π)))) (EulerPacketPointJets.fieldSum (N + 1) κ (assembledPressure N (profiles O (primaryProfile O A π)))) z = ∑ n ∈ Finset.Ico (N + 1) (2 * N + 3), κ ^ n • recursiveGrade O N (profiles O (primaryProfile O A π)) z n

The generated profiles satisfy the actual closed-interval residual identity when their two concrete linear solves satisfy their defining equations.