\section*{Declarations}

\subsection*{Funding} No funding was received for this work.

\subsection*{Conflict of interest} The author declares no conflict of interest.

\subsection*{Data availability} The program that computes the Fourier coefficients of Appendix~\ref{app:computation} and every table of this paper, the Lean~4 certificates of its finite statements, the scripts that check the explicit constants of Appendices~\ref{app:infraredlimit} and~\ref{app:softremainder}, and the source of the paper are in release \texttt{v2.0.1} of the repository named in the note under the abstract, archived on Zenodo as \href{https://doi.org/\zenodoCodeID}{\zenodoCodeID} \cite{Bha26}. The catalogue of Section~\ref{sec:catalogue} is kept in the ledger format of the engine Anaxia \cite{BLLM26}. The source register in Appendix~\ref{app:scopechecks} records the primary passages used for the scope corrections.