Top

Journal of Automated Reasoning

Published in:

25-10-2018

Classification of Finite Fields with Applications

Authors: Hing-Lun Chan, Michael Norrish

Published in: Journal of Automated Reasoning | Issue 3/2019

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

We present a formalisation of the theory of finite fields, from basic axioms to their classification, both existence and uniqueness, in HOL4 using the notion of subfields. The tools developed are applied to the characterisation of subfields of finite fields, and to the cyclotomic factorisation of polynomials of the form

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9485-1/MediaObjects/10817_2018_9485_IEq1_HTML.gif

, with coefficients over a finite fields.

previous article Mechanized Metatheory Revisited

next article Formally Verifying the Solution to the Boolean Pythagorean Triples Problem

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

In this Coq script, at https://github.com/math-comp/math-comp/blob/master/mathcomp/field/finfield.v, Section FinFieldExists.

Typical examples of algebra textbooks treating finite fields are Gallian [21], Herstein [24], and Judson [29].

Typical examples of coding textbooks treating finite fields are McEliece [37], Garrett [22] and Pretzel [39]

Here we refer to an element of the multiplicative monoid, for the multiplicative order. Every nonzero field element has the same additive order, as will be discussed in Sect. 3.

For example, in

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9485-1/MediaObjects/10817_2018_9485_Figed_HTML.gif

, \(2 * 3 = 0\). Hence in

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9485-1/MediaObjects/10817_2018_9485_Figee_HTML.gif

, \((X - 2)(X - 3) = X^2 - 5X = X(X - 5)\), which is an example of a degree 2 polynomial with more than 2 roots.

For example, the integers \(\mathbb {Z}\) form a ring. In

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9485-1/MediaObjects/10817_2018_9485_Figeg_HTML.gif

, 2X has a leading coefficient not invertible in \(\mathbb {Z}\), hence cannot be taken as a modulus for polynomial division.

Viewing polynomials as functions, this is their function composition.

This proof, based on counting field order elements, is adapted from McEliece [37], Corollary of Theorem 5.7.

Such a proof is given in Justesen and Høholdt [30], Theorem 2.1.2.

This proof works because polynomial rings over a field is a unique factorisation domain, in which irreducibles are primes.

This proof, based on degree and divisibility of special polynomials, is adapted from Belk [12], Theorem 9.

See, e.g., Lidl and Niederreiter [34], Ireland and Rosen [28], and McEliece [37].

This proof, based on quotient fields by minimal polynomials of primitives, is adapted from Belk [12], Theorem 3. Similar ideas are given in Herstein [25], Theorem 6.4.2.

When

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9485-1/MediaObjects/10817_2018_9485_Figmc_HTML.gif

is not required to be irreducible,

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9485-1/MediaObjects/10817_2018_9485_Figmd_HTML.gif

is a quotient ring, which becomes a quotient field when

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9485-1/MediaObjects/10817_2018_9485_Figme_HTML.gif

is irreducible.

Such proofs can be found in, e.g., Herstein [25] Theorem 6.3.3, Judson [29] Theorem 20.5, or Robinson [40] Theorem 10.3.1.

Our proof of this identity follows that given in McEliece [37], Theorem 2.3.

This proof, based on divisibility and pairwise coprime factors, is adapted from Ireland and Rosen [28], Proposition 13.3.2.

See, e.g., Bastida and Lyndon [11] Proposition 3.5.6, or Newman [38] Theorem 5.3.

Such a proof is given in McEliece [37] Theorem 6.6, or Ireland and Rosen [28] Proposition 7.1.5.

Our proof followed the approach given in Herstein [25], Theorem 4.5.11.

Skew fields are fields without the commutative requirement for multiplication, and Wedderburn Theorem asserts that every finite skew field must be commutative, i.e., a field.

Aczel, P.: Galois: a theory development project. Department of Computer Science and Mathematics, Manchester University, U.K. http://www.cs.man.ac.uk/~petera/galois.ps.gz (1995)

Affeldt, R., Garrigue, J., Saikawa, T.: Formalization of Reed–Solomon codes and progress report on formalization of LDPC codes. In: The 2016 International Symposium on Information Theory and its Applications (ISITA 2016), pp. 532–536 (2016)

Arneson, B., Baaz, M., Rudnicki, P.: Witt’s proof of the Wedderburn theorem. J. Formaliz. Math. 12, 69–75 (2003)

Arneson, B., Rudnicki, P.: Primitive roots of unity and cyclotomic polynomials. J. Formaliz. Math 12, 59–67 (2003)

Asperti, A., Armentano, C.: A page in number theory. J. Formaliz. Reason. 1(1), 1–23 (2008)MathSciNetMATH

Assia, M., Tassi, E.: The Mathematical Components library: principles and design choices. http://ssr.msr-inria.inria.fr/doc/tutorial-itp13/slides.pdf (2013)

Axler, S.: Linear Algebra Done Right. Undergraduate texts in mathematics. Springer, Berlin (2015). ISBN: 9783319307657MATH

Bailey, A.: The machine-checked literate formalisation of algebra in type theory. PhD thesis, Department of Computer Science, University of Manchester (1998)

Barthe, G.: A formal proof of the unsolvability of the symmetric group over a set with five or more elements. Department of Computer Science, University of Nijmegen, the Netherlands. ftp://ftp.cs.ru.nl/pub/CompMath.Found/sn.ps.Z (1994)

10.

Bartzia, E.-I., Strub, P.-Y.: A formal library for elliptic curves in the Coq proof assistant. In: Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings, ITP 2014, pp. 77–92. Springer, Cham (2014)

11.

Bastida, J.R., Lyndon, R.: Field Extensions and Galois Theory. Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge (1984). ISBN: 9781107340749CrossRef

12.

Belk, J.: Classification of finite fields. Number Theory Course: Math 318, Bard College. http://faculty.bard.edu/belk/math318/ClassificationFiniteFieldsRevised.pdf (2016)

13.

Chan, H.L., Norrish, M.: A string of pearls: proofs of Fermat’s little theorem. J. Formaliz. Reason. 6(1), 63–87 (2013)MathSciNetMATH

14.

Chan, H.L., Norrish, M.: Mechanisation of AKS Algorithm: Part 1—The Main Theorem. In: Urban, C., Zhang, X. (eds), Interactive Theorem Proving, ITP 2015, number 9236 in LNCS, pp. 117–136. Springer (2015)

15.

Cohen, C.: Construction of Real Algebraic Numbers in Coq. In: Beringer, L., Felty, A. (eds) Interactive Theorem Proving, ITP 2012, number 7406 in LNCS, pp. 67–82. Springer (2012)

16.

Curiel, N.: Formalizing Galois Theory: I automorphism groups of fields. Master’s thesis, California State University San Marcos. http://csusm-dspace.calstate.edu/handle/10211.8/107 (2011)

17.

Divasón, J., Joosten, S., Thiemann, R., Yamada, A.: A Formalization of the Berlekamp–Zassenhaus Factorization Algorithm. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp. 17–29, New York, NY, USA. ACM (2017)

18.

Ballarin, C., et al.: The Isabelle/HOL Algebra Library http://isabelle.in.tum.de/library/HOL/HOL-Algebra/index.html (2016)

19.

Fujisawa, Y., Fuwa, Y., Shimizu, H.: Public-key cryptography and Pepin’s test for the primality of fermat numbers. J. Formaliz. Math. http://mizar.org/JFM/Vol10/pepin.html (1998)

20.

Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari: Formalization of definitions and theorems related to an elliptic curve over a finite prime field by using Mizar. J. Automat. Reason. 50(2), 161–172 (2013)MathSciNetCrossRefMATH

21.

Gallian, J.A.: Contemporary Abstract Algebra. Brooks Cole, Boston (2006). ISBN: 9780618514717MATH

22.

Garrett, P.B.: The Mathematics of Coding Theory: Information, Compression, Error Correction, and Finite Fields. Pearson Prentice Hall, Upper Saddle River (2004). ISBN: 9780131019676MATH

23.

Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O’Connor, R., Biha, S., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Théry, L.: A Machine-Checked Proof of the Odd Order Theorem, pp. 163–179. Springer, Berlin (2013)MATH

24.

Herstein, I.N.: Topics in Algebra. Wiley, New York (1975). ISBN: 9780471010906MATH

25.

Herstein, I.N.: Abstract Algebra. Wiley, New York (1996). ISBN: 9780471368793MATH

26.

Hurd, J.: Verification of the Miller–Rabin Probabilistic Primality Test. Elsevier Science Inc., New York. https://doi.org/10.1016/S1567-8326(02)00065-6 (2003)

27.

Hurd, J., Gordon, M., Fox, A.: Formalized elliptic curve cryptography. High Confid. Softw. Syst. https://cps-vo.org/node/1542 (2006)

28.

Ireland, K., Rosen, M.: A Classical Introduction to Modern Number Theory. Graduate Texts in Mathematics, vol. 84. Springer, New York (1990). ISBN: 9781441930941CrossRefMATH

29.

Judson, T.W.: Abstract Algebra: Theory and Applications. The Prindle, Weber & Schmidt Series in Advanced Mathematics. PWS Publishing Company, Boston (1994)MATH

30.

Justesen, J., Høholdt, T.: A Course in Error-Correcting Codes. EMS Textbooks in Mathematics, 2nd edn. European Mathematical Society, New York (2004)CrossRefMATH

31.

Kusak, E., Leonczuk, W., Muzalewski, M.: Abelian groups, fields and vector spaces. J. Formaliz. Math. http://www.mizar.org/JFM/Vol1/vectsp_1.html (1989)

32.

Laurent, T., Hanrot, G.: Primality proving with elliptic curves. In: Schneider, K., Brandt, J. (eds), TPHOL 2007, volume 4732 of LNCS, pp. 319–333. Kaiserslautern, Germany: Springer (2007)

33.

Laurent, T.: Proving the group law for elliptic curves formally. Technical Report RT-0330, INRIA https://hal.inria.fr/inria-00129237/en/ (2007)

34.

Lidl, R., Niederreiter, H.: Introduction to Finite Fields and Their Applications, 2nd edn. Cambridge University Press, New York (1986)MATH

35.

Mizar Mathematical Library: http://www.mizar.org/library/ (2014)

36.

Mathematical Components Team: Script finfield.v in field folder of The Mathematical Components library for Coq, March. https://github.com/math-comp/math-comp/blob/master/mathcomp/field/finfield.v (2015)

37.

McEliece, R.J.: Finite Fields for Computer Scientists and Engineers. The Kluwer International Series in Engineering and Computer Science. Springer, New York (1987). ISBN: 9781461291855CrossRefMATH

38.

Newman, S.C.: A Classical Introduction to Galois Theory. Wiley, New York (2012). ISBN: 9781118091395CrossRefMATH

39.

Pretzel, O.: Error-Correcting Codes and Finite Fields. Applied Mathematics and Computing Science Series. Clarendon Press, Oxford (1996). ISBN 9780192690678MATH

40.

Robinson, D.J.S.: An Introduction to Abstract Algebra. De Gruyter Textbook. De Gruyter, Berlin (2008). ISBN: 9783110198164

41.

Rotman, J.J.: Advanced Modern Algebra: Second Edition. Graduate Studies in Mathematics. American Mathematical Society, Providence (2010). ISBN: 9781470411763MATH

42.

Wimmer, L.N.S.: A Formalisation of Lehmer’s primality criterion. Arch. Formal Proofs, Isabelle (2013)

43.

Thiemann, R., Yamada, A.: Algebraic Numbers in Isabelle/HOL. In: Blanchette, J.C., Merz, S. (eds), Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22–25, 2016, Proceedings, pp. 391–408. Cham: Springer (2016)

Title: Classification of Finite Fields with Applications
Authors: Hing-Lun Chan
Michael Norrish
Publication date: 25-10-2018
Publisher: Springer Netherlands
Published in: Journal of Automated Reasoning / Issue 3/2019
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-018-9485-1

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 3/2019

Formalization of Geometric Algebra in HOL Light

A PSpace Algorithm for Acyclic Epistemic DL

Wombit: A Portfolio Bit-Vector Solver Using Word-Level Propagation

Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF

An Isabelle/HOL Formalisation of Green’s Theorem

Semantics of Mizar as an Isabelle Object Logic

Premium Partner