## My research and investigations

### Theorem-Proving in Finite Fields

This is my PhD project proposal.

## Introduction

Finite fields are also known as Galois fields, in honor of the French mathematical genius Évariste Galois (1811 – 1832). The theory is developed from a small list of axioms, with subject matter intimately related to the arithmetic of remainders under division. Division by prime numbers give base fields, while division by primitive polynomials give nice extensions of base fields. Such is the power of a simple theory, unifying ideas from diverse topics.

There are many theorems, big and small, in the theory of Finite Fields. Since axioms are very low-level, but theorems can be high-level, the chain of reasoning from axioms to theorems is often very long. It is not uncommon to find in textbooks proof sketches of high-level theorems, leaving tedious details as exercises. Such tasks are better suited to a theorem-prover, working tirelessly and attending to logical details.

## Applications

Although a topic in abstract algebra, Finite Fields have found applications in digital computers and digital communication. Two areas of interest to this project are:

• Linear Feedback Shift Register (LFSR) – this is a simple logical circuit to deliver a sequence of binary bits. The bits look random: but since the number of circuit states is finite, the bits will repeat after a period. For cryptography, where long pseudo-random sequences can provide security for encryption, the problem is how to design LFSRs with long periods. Such work is pioneered by Solomon Golomb in 1955, showing the best LFSR designs are related to primitive polynomials in finite fields. Nowadays, LFSR have extensive military, industrial and consumer applications. For example, A5/1, a stream cipher used to encrypt mobile phone conversations in GSM standard, is LFSR-based (see here). Global Positioning System (GPS) uses an LFSR to rapidly transmit a sequence that indicates high-precision relative time offsets.
• Error-Correcting Codes (ECC) – these are coding schemes for reliable communication through a noisy channel. Examples are Bose-Chaudhuri-Hocquenghem (BCH) codes, which are based on primitive polynomials over a finite field. Because BCH codes can detect and correct multiple error bits, they are crucial for digital data storage and retrieval, and make NASA space missions possible. Reed-Solomon codes, a special type of BCH code, was used in Voyager 2 probe to send back color pictures of inner and outer planets. Today (see here) Reed-Solomon codes can be found in devices using CDs, DVDs, Blu-ray Discs; in hard-drives and flash-drives; as well as in communication protocols over networks, both cable and wireless.

The BCH codes and Reed-Solomon codes were conceived around 1960. Initially there is one drawback: while the codes can encode messages fast, the decoding process is complex and slow. In 1967, Elwyn Berlekamp invented an efficient algorithm for decoding BCH codes. Later in 1969, James Massey developed an algorithm for a different problem: how to find the shortest LFSR for given a binary sequence. Massey soon realized that his algorithm was essentially an improved version of Berlekamp’s algorithm. This Berlekamp-Massey algorithm, based on the theory of finite fields, turns using Reed-Solomon codes in error-detection and error-recovery a practical reality.

## Proposal

I intend to work on the formalization of Finite Fields, with the goal of proving Berlekamp-Massey algorithm. Major milestones are:

1. Formalize elementary field theory from its axioms, based upon a finite set.
2. Extend this formalization to include primitive polynomials of finite fields.
3. Prove properties of LFSR within this finite fields formalization.
4. Prove properties of BCH codes within this finite fields formalization.
5. Show that the problems of BCH decoding and shortest LFSR are equivalent.
6. Show that Berlekamp-Massey algorithm is correct.

### Notes

• The theorem-prover to be used is HOL4, a system with some packages for group theory and number theory.
• This formalization only covers the fundamental parts of the theory of Finite Fields.

### Finite Fields 2

The applications of the theory of finite fields (see here) depend on finding primitive polynomial of the field. This is due to the fact that a root of the primitive polynomial can act as a generator of the whole finite field.

My own presentation of this topic can be found here (click Primes for Random, then Simple Machines), showing how primitive polynomials underlie the construction of LFSRs for pseudo-random number generation.

In 1967, Elwyn Berlekamp invented an algorithm for decoding BCH codes, which is a type of polynomial code based on primitive polynomials of finite fields. Later James Massey simplified the algorithm, and recognized its application to LFSR which is also based on primitive polynomials of finite fields. Their algorithm is now known as Berlekamp-Massey algorithm.

My plan for the project work on this topic is to do the following:

1. Formalize elementary field theory from its axioms, based upon a finite set.
2. Extend this formalization to include the primitive polynomials of finite fields.

With these tools, I can try to prove the Berlekamp-Massey algorithm. I am now studying a Java applet that demonstrates this algorithm.

### Finite Fields

In abstract algebra, a field is a system within which add, subtract, multiply and divide are possible. An example of such a system is all the fractions (called rationals Q in math), but the number of fractions is infinite. Finite systems with suitably-defined +-*/ do exist, and they are known as finite fields. It was a remarkable discovery by Évariste Galois, a math genius, that finite fields are characterized only by its number of elements, which must be either a prime or power of a prime. Due to this, finite fields are also known as Galois fields.

Finite fields have many practical applications, including cryptography, error-correcting codes and LFSRs (Linear feedback shift register) for pseudo-random number generation. There is a large collection of algorithms based on theory of finite fields.

Search on Net shows the Google project: coq-galois-theory. Its timeline suggests that some progress have been made, but still a lot of work to be done. Maybe I can do a project on proving/verifying finite field algorithms in error codes and LFSRs.