The literal difference equation of two actual inviscid corrections.

theorem EulerInviscidDifferencePDE.inviscid_difference_hasDerivAt (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (T : ℝ) (hT : 0 ≤ T) (D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T)) (u v : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hu : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT u r)) (EulerCylinderSobolevSpace.value period ((EulerCorrectionOperators.CorrectionData.coefficients period D hq).apply ⟨t, ⋯⟩ (u ⟨t, ⋯⟩))) t) (hv : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT v r)) (EulerCylinderSobolevSpace.value period ((EulerCorrectionOperators.CorrectionData.coefficients period D hq).apply ⟨t, ⋯⟩ (v ⟨t, ⋯⟩))) t) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT u r) - EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT v r)) (EulerCorrectionDifferencePDE.differenceRhs period D hq 0 0 ⟨t, ⋯⟩ (u ⟨t, ⋯⟩) (v ⟨t, ⋯⟩)) t

Subtracting the actual inviscid correction equations gives the zero-viscosity difference equation.