Leading digit $d$ $\iff$ $\{\log_b x\} \in [\log_b d, \log_b(d+1))$

Proved

BenfordLaw.leadingDigit_eq_iff_fract_logb

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

benford-lawequidistributionleading-digits

Let $b \ge 2$ , let $x > 0$ be real and let $d \in \{1,\dots,b-1\}$ . Then $x$ has leading digit $d$ in base $b$ if and only if the fractional part of $\log_b x$ lies in $[\log_b d, \log_b(d+1))$ :

D_b(x) = d \iff \log_b d \le \{\log_b x\} < \log_b(d+1).

This is the observation behind the logarithmic form of the law: the probability of leading digit $d$ is the length of the interval $[\log_b d,\log_b(d+1))$ whenever $\{\log_b x\}$ is uniformly distributed.

Preamble

import Mathlib
import Definitions.Def_BenfordLaw_Defs

Formal statement

namespace BenfordLaw

theorem leadingDigit_eq_iff_fract_logb (b : ℕ) (hb : 2 ≤ b) (x : ℝ) (hx : 0 < x)
    (d : ℕ) (hd1 : 1 ≤ d) (hdb : d < b) :
    leadingDigit b x = d ↔
      Real.logb b d ≤ Int.fract (Real.logb b x) ∧
        Int.fract (Real.logb b x) < Real.logb b (d + 1) := by sorry

end BenfordLaw

Source

Wikipedia, "Benford's law" (https://en.wikipedia.org/wiki/Benford%27s_law), snapshot uploaded by the proposer, section "Definition" ("x starts with the digit 1 if log 1 ≤ log x < log 2 ...").

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 natural $b$ with $b \ge 2$ , all real $x$ with $x > 0$ , and all natural $d$ with $1 \le d$ and $d < b$ :

\lfloor b^{\{\log_b x\}}\rfloor = d \quad\Longleftrightarrow\quad \log_b d \le \{\log_b x\} \ \text{ and }\ \{\log_b x\} < \log_b(d+1),

where the left side is $\mathrm{leadingDigit}(b,x)$ (floor into $\mathbb N$ ), $\{t\}$ is the fractional part $t-\lfloor t\rfloor$ , and $\log_b y = \ln y/\ln b$ with $d$ and $d+1$ read as reals.

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

Leading digit ddd ⟺ \iff⟺{log⁡bx}∈[log⁡bd,log⁡b(d+1))\{\log_b x\} \in [\log_b d, \log_b(d+1)){logb​x}∈[logb​d,logb​(d+1))

Leading digit $d$ $\iff$ $\{\log_b x\} \in [\log_b d, \log_b(d+1))$