A nonzero Hurwitz integer has positive squared norm

Proved

HurwitzQ.normSq_nat_pos

by jawneeboy · Sep 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebrahurwitz-integersnumber-theoryquaternions

Let $\mathcal{H}$ be the Hurwitz subring of the rational quaternions: the four coordinates of an element are either all in $\mathbb{Z}$ or all in $\mathbb{Z}+\frac12$ . Write $N(a+bi+cj+dk)=a^2+b^2+c^2+d^2$ for the squared norm. Let $q$ be a rational quaternion.

q\in\mathcal{H},\ q\ne0\implies\exists n\in\mathbb{N},\quad n\ne0\ \land\ N(q)=n.

In particular, the squared norm of a nonzero Hurwitz integer is at least one.

Preamble

import Definitions.Def_HurwitzQ_hurwitzIntegersQ
import Mathlib.Algebra.Quaternion
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring

open Quaternion QuaternionAlgebra HurwitzQ

Formal statement

theorem HurwitzQ.normSq_nat_pos (q : ℍ[ℚ]) (hq : q ∈ hurwitzIntegersQ) (h0 : q ≠ 0) :
    ∃ n : ℕ, n ≠ 0 ∧ normSq q = n := by sorry

Source

Standard definition: John H. Conway and Derek A. Smith, On Quaternions and Octonions: Their Geometry, Arithmetic, and Symmetry, A K Peters, 2003, §5.1, The Hurwitz Integral Quaternions. https://www.routledge.com/On-Quaternions-and-Octonions/Conway-Smith/p/book/9781568811345 The displayed assertion is an elementary consequence of this definition; no numbered theorem attribution is claimed.

View graph