# Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation

 Title: Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation Authors: Ralph Bottesch, Jose Divasón and René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at) Submission date: 2021-03-12 Abstract: We verify two algorithms for which modular arithmetic plays an essential role: Storjohann's variant of the LLL lattice basis reduction algorithm and Kopparty's algorithm for computing the Hermite normal form of a matrix. To do this, we also formalize some facts about the modulo operation with symmetric range. Our implementations are based on the original papers, but are otherwise efficient. For basis reduction we formalize two versions: one that includes all of the optimizations/heuristics from Storjohann's paper, and one excluding a heuristic that we observed to often decrease efficiency. We also provide a fast, self-contained certifier for basis reduction, based on the efficient Hermite normal form algorithm. BibTeX: @article{Modular_arithmetic_LLL_and_HNF_algorithms-AFP, author = {Ralph Bottesch and Jose Divasón and René Thiemann}, title = {Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation}, journal = {Archive of Formal Proofs}, month = mar, year = 2021, note = {\url{https://isa-afp.org/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Hermite, Jordan_Normal_Form, LLL_Basis_Reduction, Show, Smith_Normal_Form