Division algorithms for norm-Euclidean real quadratic fields -- part I

TL;DR

This paper develops Euclidean division algorithms for specific real quadratic fields, utilizing geometric coverings and mechanized proofs to analyze their Euclidean properties based on the first Euclidean minimum.

Contribution

It introduces explicit Euclidean division algorithms for select real quadratic fields, linking the remainders to the Euclidean minimum and employing computational methods for proof verification.

Findings

Algorithms for fields Q(√2), Q(√3), Q(√6), Q(√7), Q(√11), Q(√19)

Coverage of the fundamental square with hyperbolas for division regions

Mechanized, exact proof methods for Euclidean properties

Abstract

We give a Euclidean division algorithm for the real quadratic fields $\mathbb{Q}(\sqrt{m})$ for $m \in \{2, 3, 6, 7, 11, 19\}$, with the property that the norm of the remainder depends on the first Euclidean minimum of the field. In each case, we cover the square $[-1/2, 1/2] \times [-1/2, 1/2]$ with hyperbolas and give a list of these, together with regions covered. We mechanize the proofs as much as we can, using exact computations, in order to be able to reproduce them.