Remark: Arithmetic proof versus execution claim

Lemma lem:arithmetic specifies the finite arithmetic certificate explicitly. The appendix is an independent way to check its integer comparisons. Inclusion of that code does not assert that the code, a proof assistant, or pdfLaTeX has been executed in preparing this response.