Quadratic Extensions in ACL2

TL;DR

This paper demonstrates how ACL2(r) can be used to reason about chains of quadratic extension fields, proving that certain algebraic numbers like cube root of 2 and cos(pi/9) are not rational.

Contribution

It introduces a method to formalize reasoning about quadratic extension fields within ACL2(r), including proofs of non-membership for specific algebraic numbers.

Findings

Proves cube root of 2 is not rational.

Shows cosine of pi/9 is not rational.

Demonstrates ACL2(r) can reason about algebraic field extensions.

Abstract

Given a field K, a quadratic extension field L is an extension of K that can be generated from K by adding a root of a quadratic polynomial with coefficients in K. This paper shows how ACL2(r) can be used to reason about chains of quadratic extension fields Q = K_0, K_1, K_2, ..., where each K_i+1 is a quadratic extension field of K_i. Moreover, we show that some specific numbers, such as the cube root of 2 and the cosine of pi/9, cannot belong to any of the K_i, simply because of the structure of quadratic extension fields. In particular, this is used to show that the cube root of 2 and cosine of pi/9 are not rational.