<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In this article, we formalize in Mizar [<xref ref-type="bibr" rid="j_forma-2017-0015_ref_005_w2aab3b7b7b1b6b1ab1ab5Aa">5</xref>] the definition of dual lattice and their properties. We formally prove that a set of all dual vectors in a rational lattice has the construction of a lattice. We show that a dual basis can be calculated by elements of an inverse of the Gram Matrix. We also formalize a summation of inner products and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL(Lenstra, Lenstra and Lovász) base reduction algorithm and cryptographic systems with lattice [<xref ref-type="bibr" rid="j_forma-2017-0015_ref_020_w2aab3b7b7b1b6b1ab1ac20Aa">20</xref>], [<xref ref-type="bibr" rid="j_forma-2017-0015_ref_010_w2aab3b7b7b1b6b1ab1ac10Aa">10</xref>] and [<xref ref-type="bibr" rid="j_forma-2017-0015_ref_019_w2aab3b7b7b1b6b1ab1ac19Aa">19</xref>].</p></abstract>

In this article, we formalize in Mizar [5] the definition of dual lattice and their properties. We formally prove that a set of all dual vectors in a rational lattice has the construction of a lattice. We show that a dual basis can be calculated by elements of an inverse of the Gram Matrix. We also formalize a summation of inner products and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL(Lenstra, Lenstra and Lovász) base reduction algorithm and cryptographic systems with lattice [20], [10] and [19].

Dual Lattice of ℤ-module Lattice

Formalized Mathematics

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

{"article-title":"Dual Lattice of ℤ-module Lattice"}

In this article, we formalize in Mizar [5] the definition of dual lattice and their properties. We formally prove that a set of all dual vectors in a rational...

Dual Lattice of ℤ-module Lattice

Publié en ligne: 23 sept. 2017

Pages: 157 - 169

Reçu: 27 juin 2017

DOI: https://doi.org/10.1515/forma-2017-0015

Mots clés
ℤ-lattice, dual lattice of ℤ-lattice, dual basis of ℤ-lattice

© 2017 Yuichi Futa et al., published by De Gruyter Open

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Dual Lattice of ℤ-module Lattice

Publié en ligne: 23 sept. 2017

Pages: 157 - 169

Reçu: 27 juin 2017

DOI: https://doi.org/10.1515/forma-2017-0015

Mots clésℤ-lattice, dual lattice of ℤ-lattice, dual basis of ℤ-lattice

© 2017 Yuichi Futa et al., published by De Gruyter Open

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Mots clés
ℤ-lattice, dual lattice of ℤ-lattice, dual basis of ℤ-lattice