A quartic entropy deficit for random rankings

Dev D. Goyal

A quartic entropy deficit for random rankings

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

Problem and result

Problem: Leighton–Moitra entropy conjecture for rankings: an explicit quartic ε⁴ entropy deficit
Posed in: Leighton and Moitra (qualitative conjecture, proved by Acan, Devlin and Kahn); a Cε⁴ deficit is proposed in Devlin's research statement
Status: Sharpened
Result: Every probability distribution on rankings of n labels in which each pairwise comparison has probability at distance at least ε > 0 from 1/2 has entropy at most (1 − ε⁴/144) log(n!), for every n.

Abstract

A distribution on rankings of n labels has entropy at most (1 − ε⁴/144) log(n!) if every pairwise comparison has probability at distance at least ε > 0 from 1/2.

The proof includes all finite sizes and actual position-valued permutations. It assumes neither independent comparisons nor transitive preferred directions.

Details

Year: 2026
Discipline: Mathematics
Area: Probability and combinatorics
Subject: Discrete analysis, tilings, probability and entropy
Result type: Entropy deficit from pairwise comparison bias
Formal proof: Standalone Lean package
Family: quartic-rankings
Keywords: random rankings, permutation entropy, pairwise comparisons, entropy bounds, ranking distributions

Statement and scope

Formal scope. The proof includes all finite sizes and actual position-valued permutations. It assumes neither independent comparisons nor transitive preferred directions.

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 337 KB
PDF on GitHub: papers/mathematics/quartic-rankings/manuscript.pdf
LaTeX source: papers/mathematics/quartic-rankings/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/quartic-rankings/ 21 Lean files

Lakefile

papers/mathematics/quartic-rankings/lakefile.lean

Toolchain

leanprover/lean4:v4.19.0

Library roots

Reproduce

The commands below are quoted from papers/mathematics/quartic-rankings/README.md, which gives their context and working directory.

Reproduce the proof

lake exe cache get
lake build
lake env lean -DwarningAsError=true PermEntropy/Verification.lean

README: papers/mathematics/quartic-rankings/README.md
Verification record: papers/mathematics/quartic-rankings/VERIFICATION.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Source. Acan, Devlin, and Kahn, 2019; the manuscript identifies the established entropy arguments.

Questions and answers

What does this paper prove about the Leighton–Moitra entropy conjecture?

It gives an explicit quantitative version: if every pairwise comparison of a random ranking of n labels has probability at least ε away from 1/2, the entropy is at most (1 − ε⁴/144) log(n!), for every n ≥ 0 and without independence or transitivity assumptions. The constant and the exponent 4 are not claimed to be optimal, and no matching lower construction is given.

Was the conjecture already proved?

Yes, qualitatively. Acan, Devlin and Kahn proved the general theorem (J. Combin. Theory Ser. A, 2019) with a coefficient of order exp[−ε^(−O(1))], Leighton and Moitra had proved a quartic bound when the preferred comparisons are consistent with a total order, and Devlin's research statement proposed a deficit of the form Cε⁴. The contribution here is the explicit general quartic bound and its proof.

Is the proof formally verified?

Yes. The main theorem is formalized in Lean 4 for finite probability distributions on actual rankings of every finite size, with the literal pairwise comparison events; the axiom audit permits only propext, Classical.choice and Quot.sound.

Cite

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

@misc{goyal2026quarticrankings,
  author = {Goyal, Dev D.},
  title = {A quartic entropy deficit for random rankings},
  year = {2026},
  howpublished = {Preprint},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/quartic-rankings},
  note = {Fully autonomous agentic research generated by AI systems.}
}