Browse › Number theory › 015 Torus-packet equidistribution in prime, quartic, and sextic degrees
Equidistribution of Prime-Degree Torus Packets with Arbitrary Local Type
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
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.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI math release, Lean scope note 015: Torus-packet equidistribution in prime, quartic, and sextic degrees (lean/docs/015.md, release of 2026-10-06). Describes the release's Lean formalization of this paper's main theorem (weak convergence to Haar measure and tightness for every fixed prime degree at least five, arbitrary local homothety type) and links the comparator statement. [family-level]
- OpenAI math release, DukePrimeDegree.lean (comparator challenge) (lean/ComparatorChallenges, 2026-10-06). Comparator statement
prime_degree_packet_measure_equidistribution_unconditional, left assorry, against which the formal proof is checked. - OpenAI math release, MainUnconditional.lean (lean/OAI/NumberTheory/DukePrimeDegree, 2026-10-06). Solution module stating
prime_degree_packet_equidistribution_unconditional, closed using lemmas imported from other modules of the development.
Related prior literature mentioned by others
- Manfred Einsiedler, Elon Lindenstrauss, Philippe Michel and Akshay Venkatesh, Distribution of periodic torus orbits and Duke’s theorem for cubic fields (Annals of Mathematics 173, 2011). The VibeMathed family entry identifies this cubic equidistribution theorem and its higher-degree discussion as background to the family’s packet-equidistribution claims. [family-level]
Possibly relevant literature (found by the agent, not checked)
- Ilya Khayutin, Non-vanishing of Class Group L-functions for Number Fields with a Small Regulator (arXiv:1901.06710, 2019). Uses almost-equidistribution of Eisenstein periods on maximal-order toral packets in degree n together with escape of mass for the trivial-class orbit, which bears on the paper's remark that it makes no assertion about individual orbits.
Digests and expositions
- Latent Seminar, Arithmetic torus packets and equidistribution (2026-10-06). This exposition distinguishes the three packet theorems and outlines tightness, entropy, and the additional quartic and sextic arguments, explicitly without independently verifying the complete proofs. [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 015
Independent sites; their content is not reviewed here.
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}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/015.md. The Lean statements have not been checked by people against the paper's claims.
Family 015: Torus-packet equidistribution in prime, quartic, and sextic degrees
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.
Other papers in this family:
- Equidistribution of primitive quartic torus packets for arbitrary orders · October 5, 2026
- Equidistribution of Primitive Sextic Torus Packets · October 5, 2026