$f(1)/f(n)=n^s$ : the top item is $n^s$ times as frequent as the $n$ -th

Proved

ZipfLaw.zipfPMF_ratio

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

harmonic-numberspower-lawzipf-law

For $1\le n\le N$ and real $s$ , the most probable item is exactly $n^s$ times as probable as the item of rank $n$ :

\frac{f(1;N,s)}{f(n;N,s)}=n^{s}.

For $s=1$ : the most common word occurs $n$ times as often as the $n$ -th most common one.

Preamble

import Mathlib
import Definitions.Def_ZipfLaw_Defs

Formal statement

namespace ZipfLaw

theorem zipfPMF_ratio (N : ℕ) (s : ℝ) (n : ℕ) (hn1 : 1 ≤ n) (hnN : n ≤ N) :
    zipfPMF N s 1 / zipfPMF N s n = (n : ℝ) ^ s := by sorry

end ZipfLaw

Source

Wikipedia, "Zipf's law" (https://en.wikipedia.org/wiki/Zipf%27s_law), snapshot uploaded by the proposer, lead section and "Word frequencies in human languages" ("the most common word occurs about n times the n-th most common one").

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - non-blind, same agent as the drafter

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source article and of the intended meaning. It is not a blind audit by an independent reader, and no reviewer should treat it as one. Please compare it against the Lean code yourself.

For all naturals $N$ , $n$ with $1\le n\le N$ and every real $s$ : $\mathrm{zipfPMF}(N,s,1)/\mathrm{zipfPMF}(N,s,n)=n^s$ (real power of the real $n$ ).

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

f(1)/f(n)=nsf(1)/f(n)=n^sf(1)/f(n)=ns: the top item is nsn^sns times as frequent as the nnn-th

$f(1)/f(n)=n^s$ : the top item is $n^s$ times as frequent as the $n$ -th