A rank bound for represented totally positive unit squareclasses

Dev D. Goyal

A rank bound for represented totally positive unit squareclasses

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Daans–Kala–Man–Widmer–Yatsyna Question 3.4 on represented unit square classes
Posed in: Daans, Kala, Man, Widmer and Yatsyna, PNAS 122(20), e2419414122 (2025), Question 3.4
Status: Answered negatively
Result: A totally positive definite quadratic lattice of rank n over any totally real algebraic field, with integral norms but not necessarily classical, represents at most n totally positive unit square classes, so n + 1 cannot occur.

Abstract

Let K be a totally real algebraic field, possibly of infinite degree, and L a totally positive definite quadratic lattice over its ring of integers with Q(L) ⊆ O_K, not necessarily classical. Then every family of pairwise distinct classes of totally positive units modulo squares of units represented by L has at most rank L members, and the bound is attained when the field has enough classes. This answers negatively Question 3.4 of Daans, Kala, Man, Widmer and Yatsyna, who proved the bound 2n − 2 and asked whether n + 1 classes can occur. The bound is a short consequence of standard facts on finite reflection groups: unit-valued vectors give integral reflections, and conjugate reflections carry the same unit class. As a corollary, a universal lattice has rank at least the number of totally positive unit classes.

Details

Year: 2026
Discipline: Mathematics
Area: Quadratic forms and number theory
Subject: Quadratic forms and number theory
Result type: Theorem answering a published question and reproducible proof package
Formal proof: Standalone Lean package
Family: unit-squareclasses
Keywords: quadratic lattices, totally real fields, unit square classes, universal quadratic forms, nonclassical lattices, reflection groups, Daans–Kala–Man–Widmer–Yatsyna

Statement and scope

Formal scope. The bound for every algebraic totally real field, including infinite extensions, every O_K-submodule with integral norms in a finite-dimensional totally positive definite space, and actual units of the ring of integers is formalized in 11 Lean modules. The derivation from finite reflection groups, sharpness and the universality corollary are conventional.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 289 KB
PDF on GitHub: papers/mathematics/unit-squareclasses/manuscript.pdf
LaTeX source: papers/mathematics/unit-squareclasses/manuscript.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/mathematics/unit-squareclasses/

Lean project

papers/mathematics/unit-squareclasses/lean/ 11 Lean files

Lakefile

papers/mathematics/unit-squareclasses/lean/lakefile.toml

Toolchain

leanprover/lean4:v4.19.0

Library roots

Reproduce

The commands below are quoted from papers/mathematics/unit-squareclasses/VERIFICATION.md, which gives their context and working directory.

lake exe cache get
python3 scripts/verify_cached.py --mathlib-cache .lake/packages/mathlib \
  --lean-bin "$(lean --print-prefix)/bin/lean" --packages-root .lake/packages --output /tmp/unit-squareclasses-verification

README: papers/mathematics/unit-squareclasses/README.md
Verification guide: papers/mathematics/unit-squareclasses/verification/README.md
Verification record: papers/mathematics/unit-squareclasses/VERIFICATION.md
Authorship: papers/mathematics/unit-squareclasses/AUTHORSHIP.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Source. Daans, Kala, Man, Widmer and Yatsyna (PNAS 2025) proved the bound 2n − 2 and asked whether n + 1 classes can occur (Question 3.4); Daans, Kala and Man had treated classical lattices. The reflection mechanism is classical (Scharlau–Blaschke). Historical priority is not certified.

Questions and answers

Can a rank-n lattice represent n + 1 totally positive unit square classes?

No. The preprint proves that a totally positive definite lattice of rank n with integral norms, classical or not, over any totally real algebraic field represents at most n classes of totally positive units modulo squares of units, improving the bound 2n − 2 of Daans, Kala, Man, Widmer and Yatsyna. The bound is attained when the field has enough classes.

Was part of this already known?

Yes. For classical lattices the bound n was already known from Daans, Kala and Man, and the reflection mechanism is classical (Scharlau–Blaschke). The bound is a short consequence of standard facts on finite reflection groups; historical priority is not certified.

Is the proof formally verified?

The bound for every algebraic totally real field, including infinite extensions, is formalized in 11 Lean 4 modules. The finite-reflection-group derivation, sharpness and the universality corollary have conventional proofs.

Cite

Citation file papers/mathematics/unit-squareclasses/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026unitsquareclasses,
  author = {Goyal, Dev D.},
  title = {A Rank Bound for Represented Totally Positive Unit Squareclasses},
  year = {2026},
  month = oct,
  note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/unit-squareclasses}
}