Papers With

← All papers
First page of Class numbers and finiteness of norm Euclidean quadratic lattices over algebraic number fields

Class numbers and finiteness of norm Euclidean quadratic lattices over algebraic number fields

Zilong He

math.NT Oct 27, 2026 · v1
formalization number-theory
Read PDF arXiv abstract Code
TL;DR
Selected main results on norm Euclidean lattices were formalized in Lean 4, with AI assistance, in a cited formalization artifact.
Abstract
Let $F$ be an algebraic number field and $\mathcal{O}_{F}$ the ring of integers of $F$. Let $L$ be an integral $\mathcal{O}_{F}$-lattice of rank $n\ge1$ on an anisotropic quadratic space $V$. We prove that if $L$ is norm Euclidean, then $L$ is $\mathcal{O}_{F}$-maximal of class number one, and the class number of $F$ equals the class number of $L\perp\mathbf{H}$, where $\mathbf{H}$ is the hyperbolic lattice with quadratic form $xy$. Under the same assumption, $F$ has class number one if $n\ge3$ and at most two if $n=1,2$. We also prove finiteness up to isometry for totally definite norm Euclidean lattices over totally real number fields in ranks at least three as the field varies, in rank two for fixed field degree, and in rank one over a fixed field. This confirms Clark's finiteness conjecture in ranks at least three.
Problem

Clark conjectured that totally definite integral norm Euclidean quadratic lattices have class number one, and that there are finitely many of them up to isometry as the totally real base field varies. Earlier finiteness results needed the stronger trace Euclidean hypothesis.

Approach

Following Clark and Jagy, the author develops a Lorentzian lattice method by studying M = L ⊥ H, where H is the hyperbolic plane. The method relies on F-linear maps, norm descent, cancellation of H, and spinor-norm genus theory. Finiteness follows from a bound on the norm ideal combined with Pfeuffer's finiteness theorems. Selected main results were formalized in Lean 4 with assistance from ChatGPT.

Results

Norm Euclidean lattices on anisotropic spaces are O_F-maximal of class number one, and h(F) equals the class number of L ⊥ H. This forces h(F) = 1 for rank at least 3 and h(F) ≤ 2 for ranks 1 and 2. Finiteness up to isometry holds in rank at least 3 as the field varies, which confirms Clark's finiteness conjecture in those ranks.