A norm-Euclidean lattice is an integral quadratic lattice 
over the ring of integers 
of a number
field 
such that
 |
for some 
for every 
in its ambient quadratic space. Here 
is an anisotropic quadratic
form, meaning that 
implies 
, and 
is the field norm (Clark
2012, He 2026). Here an integral quadratic lattice is a finitely generated 
-submodule 
spanning the quadratic space, with 
. The inequality measures approximation by lattice
vectors using the field norm of the quadratic value.
He (2026) proved that every such integral lattice is maximal among integral lattices on the same quadratic space and has exactly one isometry class in its genus. The
class number of 
is 1 when the rank is at least three and is at most 2 in ranks
one and two. He (2026) also proved that, up to isometry, only finitely many totally
definite norm-Euclidean integral quadratic lattices of rank at least three occur
as 
varies over all totally real fields. Totally
definite means that the form is positive or negative definite at every real embedding.
He (2026) reports AI assistance with exploring proof strategies
and formalization.
