Prove2Me

Log–log plot of the Zipf distribution is affine with slope −s-s

Proved
ZipfLaw.log_zipfPMF_affine

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

harmonic-numberspower-lawzipf-law

For 1≤k≤N1\le k\le N and real ss,

ln⁡f(k;N,s)=−sln⁡k−ln⁡HN,s,\ln f(k;N,s)=-s\ln k-\ln H_{N,s},

so on a log–log plot (log rank against log frequency) the Zipf distribution lies on a straight line of slope −s-s.

Preamble
import Mathlib
import Definitions.Def_ZipfLaw_Defs
Formal statement
namespace ZipfLaw

theorem log_zipfPMF_affine (N : ℕ) (s : ℝ) (k : ℕ) (hk1 : 1 ≤ k) (hkN : k ≤ N) :
    Real.log (zipfPMF N s k) = -s * Real.log k - Real.log (genHarmonic N s) := by sorry

end ZipfLaw
Source
Wikipedia, "Zipf's law" (https://en.wikipedia.org/wiki/Zipf%27s_law), snapshot uploaded by the proposer, section "Empirical testing" ("The data conform to Zipf's law with exponent s to the extent that the plot approximates a linear (more precisely, affine) function with slope −s").
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 NN, kk with 1≤k≤N1\le k\le N and every real ss: ln⁡(zipfPMF(N,s,k))=−sln⁡k−ln⁡(genHarmonic(N,s))\ln\big(\mathrm{zipfPMF}(N,s,k)\big)=-s\ln k-\ln\big(\mathrm{genHarmonic}(N,s)\big).

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