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

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](../../preprints/Equidistribution-of-Prime-Degree-Torus-Packets-with-Arbitrary-Local-Type-September-24-2026/paper.pdf)

## 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](../ComparatorChallenges/DukePrimeDegree.lean) |