Abstract
Wave equations with Caputo fractional damping produce power-law attenuation, but their non-local memory term is costly, and stability proofs for nonlinear variants involve long, error-prone algebra. We discretise a one-dimensional wave equation with Caputo damping of order α ∈ (0,1) and a cubic nonlinearity by Legendre–Gauss–Lobatto collocation in space and a linearly implicit three-level L1 scheme in time. A sum-of-exponentials (SOE) approximation with a certified uniform relative accuracy reduces the memory cost from O(Nt2) to O(NeNt), with Ne growing logarithmically. Without relying on a sign of the discrete memory form, we prove, in exact arithmetic, a conditional stability estimate whose step-size restriction is independent of the polynomial degree and the time unit, and, under step-size and smallness conditions, an error bound of order τ2−α + N1−m + εSOE for smooth solutions. The algebraic core of both proofs, but not the approximation theory, is machine-checked in Lean 4. The strongly nonlinear computations violate the step-size condition; their stability is observed, not proved. The experiments confirm spectral accuracy in space and the temporal rate 2 − α for α = 0.5 and 0.7, and the memory evaluation becomes almost 60 times faster. For damping calibrated to a prescribed quality factor, the quality factor measured from synthetic seismograms agrees with the dispersion relation to within 0.5% between 5 and 20 Hz. An extension to Caputo’s constitutive model reproduces a nearly constant quality factor.