Code · Zenodo · September 21, 2026

Code and Lean 4 proofs for: Fast Spectral Simulation of One-Dimensional Nonlinear Fractional Waves in Attenuating Media

Nauryzbay Adil, Yertay Kazez, Abdumauvlen Berdyshev, Zh. A. Abdiramanov

Abstract

Supplementary software for the article "Fast Spectral Simulation of One-Dimensional Nonlinear Fractional Waves in Attenuating Media" by N. Adil, Y. Kazez, A. Berdyshev and Z. Abdiramanov (submitted to Computation, MDPI). JuliaSim.zip: Julia code (tested with Julia 1.12.4) of the Legendre-Gauss-Lobatto (LGL) collocation scheme with the L1 and fast L1 sum-of-exponentials (SOE) approximations of the Caputo derivative, for a wave equation with fractional damping, a cubic nonlinearity and an optional constitutive (Caputo model) term. The script run_all.jl reproduces all tables and figures of the article (convergence tests, CPU timings, energy behaviour, seismic Ricker-wavelet experiments, comparison with finite differences, validation of the quality factor Q(f)). Lean4_Verification.zip: Lean 4 / Mathlib project with machine-checked proofs (no sorry) of the discrete energy identity, the bound on the L1 memory operator, a discrete Gronwall-type lemma and the stability and error-energy estimates of the scheme. Checked with Lean v4.35.0-rc2 and Mathlib commit b0df0c4b5cd02a4d247c8ab29ff3cd75ff2db747. Parts of the code and of the Lean formalisation were developed with the assistance of the generative AI tool Claude (Anthropic); all material was checked by the authors. Funding: Science Committee of the Ministry of Science and Higher Education of the Republic of Kazakhstan, grant AP22683307.

Fractional Differential Equations SolutionsNumerical methods for differential equationsDifferential Equations and Boundary Problemsattenuating mediaCaputo fractional derivativesum-of-exponentials approximation

Code and Lean 4 proofs for: Fast Spectral Simulation of One-Dimensional Nonlinear Fractional Waves in Attenuating Media

Abstract

More by Zhanars Abdiramanov