Papers With

← All papers
First page of Finiteness theorems for trace Euclidean quadratic lattices over totally real number fields

Finiteness theorems for trace Euclidean quadratic lattices over totally real number fields

Zilong He

math.NT Oct 25, 2026 · v1
formalization number-theory
Read PDF arXiv abstract Code
TL;DR
Selected main results are formalized in Lean 4, developed with AI assistance, with documented scope and external assumptions in an accompanying repository.
Abstract
Motivated by Clark's work on Euclidean quadratic forms, we introduce trace Euclidean and house Euclidean quadratic lattices over totally real number fields, and relate these concepts through the $p$-norm Euclidean property. We prove that, as $F$ varies over all totally real number fields of arbitrary degree, there are only finitely many positive definite trace Euclidean $\mathcal{O}_{F}$-lattices of arbitrary rank $n\ge1$, up to isometry. For every $p\in[1,\infty]$, the same finiteness holds for positive definite $p$-norm Euclidean lattices. We also classify all positive definite trace Euclidean lattices of rank one over real quadratic fields: there are exactly six isometry classes, and every such lattice is free. As a corollary, the trace Euclidean real quadratic fields are precisely $\mathbb{Q}(\sqrt{2})$, $\mathbb{Q}(\sqrt{5})$, and $\mathbb{Q}(\sqrt{13})$.
Problem

Clark defined Euclidean quadratic forms over the integers. This work extends the notion to lattices over rings of integers of totally real number fields, defining trace Euclidean and house Euclidean lattices. It then asks whether only finitely many such lattices exist.

Approach

The trace Euclidean condition is related to covolumes and the trace covering radius of the associated real lattice. This yields bounds on the root discriminant of the field and on the norm of the lattice's volume ideal. Odlyzko-type discriminant bounds then restrict the field degree and the lattice rank, and classical finiteness results for lattices finish the argument. Selected main results were formalized in Lean 4, and Mathematica checked the numerical computations.

Results

Over all totally real fields there are only finitely many positive definite trace Euclidean lattices of any rank, up to isometry, and the same holds for p-norm Euclidean lattices. Over real quadratic fields there are exactly six isometry classes of rank-one trace Euclidean lattices, all of them free. The trace Euclidean real quadratic fields are Q(√2), Q(√5) and Q(√13).