Quadratic Extensions in ACL2

Ruben Gamboa
(University of Wyoming)
John Cowles
(University of Wyoming)
Woodrow Gamboa
(woodrowg@stanford.edu)

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.

In Grant Passmore and Ruben Gamboa: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2020), Worldwide, Planet Earth, May 28-29, 2020, Electronic Proceedings in Theoretical Computer Science 327, pp. 75–86.
Published: 29th September 2020.

ArXived at: http://dx.doi.org/10.4204/EPTCS.327.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org