Acknowledgments and citation

Authors and AI disclosure

Le Chen, Associate Professor, Department of Mathematics and Statistics, Auburn University. The Lean code was developed with AI assistance under the author’s direction. Lean compilation and an independent kernel comparison check the stated theorems only; AI assistance is not human mathematical review. Mathlib retains its own notices (see NOTICE).

lean-pkg

Developed and verified with lean-pkg (doi:10.5281/zenodo.23272098). The receipts under .lean-receipts/ bind the checks to a source commit, and the verification section below is rendered by lean-pkg page from coverage.yaml, claims.yaml and those receipts; lean-pkg page neumann-cosine-lean --check confirms it is current.

Auburn University Easley Cluster

This work was completed in part with resources provided by the Auburn University Easley Cluster.

The release build gates ran there as Slurm jobs; their receipts are committed under .lean-receipts/ and listed on the verification page.

Built on

Mathlib: The mathlib Community, The Lean Mathematical Library, CPP 2020, doi:10.1145/3372885.3373824. Through Mathlib: Batteries, Aesop, Qq, Plausible, ProofWidgets4, LeanSearchClient, import-graph and lean4-cli.
Lean 4, including leanchecker (replay of the compiled proofs) and the con-ron kernel checker shipped in the toolchain.
comparator with lean4export and the nanoda kernel, for the statement comparison.

These projects formalize nearby results. No code from them is used here.

xiangyazi24/Shen_work (Xiang Huang): a continuum Neumann cosine layer on $[0,1]$ for $C^2$ functions, with coefficient decay and pointwise inversion at interior points. The repository has no license.
The one-dimensional weak-derivative file of the Escauriaza–Seregin–Šverák formalization, scottnarmstrong/EscauriazaSereginSverak, also collected in LeanPool. It proves independently that a weak derivative gives an absolutely continuous primitive.
TauCeti: Fourier coefficients of absolutely continuous functions on the circle, by integration by parts.
jinshanmu/Hatano-Nelson: the sine eigenbasis and spectrum of tridiagonal Toeplitz matrices, the Dirichlet analogue of item 10.

How to cite

Cite the software with CITATION.cff (doi:10.5281/zenodo.23488175).