Quadratic Extensions in ACL2

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 = K0 C K1 C K2 C & BULL; & BULL; & BULL;, where each Ki+1 is a quadratic extension field of Ki. Moreover, we show that some specific numbers, such as 3 & RADIC;2 and cos 9 & pi;, cannot belong to any of the Ki, simply because of the structure of quadratic extension fields. In particular, this is used to show that 3 & RADIC;2 and cos 9 & pi; are not rational.