Torus-packet equidistribution in prime, quartic, and sextic degrees

3 papersLean

Proves Haar equidistribution without escape of mass for complete volume-weighted torus packets from totally real fields: arbitrary lattices and prescribed local types in fixed prime degree at least five, arbitrary-order Picard packets in primitive quartic fields, and maximal-order ideal-class packets in primitive sextic fields. Here primitive means having no proper intermediate field; the relevant order or field discriminant tends to infinity.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 3

Equidistribution of Prime-Degree Torus Packets with Arbitrary Local Type

OpenAI · September 24, 2026

We prove the packet form of the higher-dimensional Duke equidistribution problem for totally real fields of any fixed prime degree at least five, allowing arbitrary local homothety types of full lattices. As the multiplier-order discriminant tends to infinity, the volume-weighted packet measures converge to Haar probability measure, with no escape of mass.

Read PDF Download Source

Cite

@misc{OAI:Equidistribution-of-Prime-Degree-Torus-Packets-with-Arbitrary-Local-Type-September-24-2026,
  author = {{OpenAI}},
  title = {{Equidistribution of Prime-Degree Torus Packets with Arbitrary Local Type}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Equidistribution-of-Prime-Degree-Torus-Packets-with-Arbitrary-Local-Type-September-24-2026/paper.pdf}{OAI:Equidistribution-of-Prime-Degree-Torus-Packets-with-Arbitrary-Local-Type-September-24-2026}},
  year = {2026}
}

Equidistribution of primitive quartic torus packets for arbitrary orders

OpenAI · October 5, 2026

Let K range over totally real quartic fields with no proper intermediate field, and let \(\mathcal O\) be any order in K. We prove that the packets of periodic diagonal orbits attached to invertible \(\mathcal O\)-ideal classes, weighted by orbit volume, equidistribute with no escape of mass as \(|\mathop{\mathrm{Disc}}\nolimits (\mathcal O)|\) tends to infinity. The proof combines measure rigidity with a cubic-resolvent estimate that remains uniform at primes dividing the order index.

Read PDF Download Source

Cite

@misc{OAI:Equidistribution-of-Primitive-Quartic-Torus-Packets-for-Arbitrary-Orders-October-5-2026,
  author = {{OpenAI}},
  title = {{Equidistribution of primitive quartic torus packets for arbitrary orders}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Equidistribution-of-Primitive-Quartic-Torus-Packets-for-Arbitrary-Orders-October-5-2026/quartic-torus-packets.pdf}{OAI:Equidistribution-of-Primitive-Quartic-Torus-Packets-for-Arbitrary-Orders-October-5-2026}},
  year = {2026}
}

Equidistribution of Primitive Sextic Torus Packets

OpenAI · October 5, 2026

We prove that the complete ideal-class packets of maximal orders in totally real sextic fields with no proper intermediate fields become equidistributed, with no escape of mass, in the space of unimodular lattices as their field discriminants tend to infinity. The limit is Haar probability measure. Each packet includes all coordinate-sign translates and is weighted by diagonal-orbit volume.

Read PDF Download Source

Cite

@misc{OAI:Equidistribution-of-Primitive-Sextic-Torus-Packets-October-5-2026,
  author = {{OpenAI}},
  title = {{Equidistribution of Primitive Sextic Torus Packets}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Equidistribution-of-Primitive-Sextic-Torus-Packets-October-5-2026/primitive-sextic-torus-packets.pdf}{OAI:Equidistribution-of-Primitive-Sextic-Torus-Packets-October-5-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Equidistribution of Prime-Degree Torus Packets with Arbitrary Local Type

Scope

The formalization proves equidistribution of volume-weighted torus packets for totally real number fields of every fixed prime degree at least five. For any sequence of full lattices whose multiplier-order discriminants tend to infinity, the packet measures converge weakly to Haar probability measure and form a tight family, so no mass escapes. Arbitrary local homothety types are allowed, and the fields may vary along the sequence.

Comparator links

Result	Comparator statement
Equidistribution of prime-degree torus packets	DukePrimeDegree.lean

Scope note on GitHub →