Random deposition: $(N_t-t)/\sqrt t\Rightarrow\mathcal N(0,1)$

Proved

KPZBallistic.random_deposition_clt

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

ballistic-depositionkpzprobability

Let $N_t(0)$ be the random deposition height of column $0$ at time $t$ , i.e. the number of rings of a rate-one Poisson clock in $[0,t]$ . For every $x\in\mathbb R$ ,

\lim_{t\to\infty}P\Big(\frac{N_t(0)-t}{\sqrt t}\le x\Big)=\Phi(x),

where $\Phi$ is the standard Gaussian distribution function. Random deposition has no spatial interaction and is in the Gaussian universality class (fluctuation exponent $1/2$ ); it is the baseline against which KPZ behaviour is contrasted.

Preamble

import Mathlib
import Definitions.Def_KPZBallistic_Defs

open MeasureTheory ProbabilityTheory Filter Topology

Formal statement

namespace KPZBallistic

theorem random_deposition_clt {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    [IsProbabilityMeasure P] (τ : ℤ → ℕ → Ω → ℝ) (hτ : IsPoissonClocks P τ) (x : ℝ) :
    Tendsto (fun t : ℝ => P.real {ω | ((rdHeight τ t 0 ω : ℝ) - t) / Real.sqrt t ≤ x})
      atTop (𝓝 ((gaussianReal 0 1).real (Set.Iic x))) := by sorry

end KPZBallistic

Source

I. Corwin, The Kardar-Parisi-Zhang equation and universality class, Random Matrices Theory Appl. 1 (2012), https://arxiv.org/abs/1106.1596, Section 1.1.1, p. 3 (random deposition: 'the height at time t fluctuates like t^{1/2} and is governed by the Gaussian distribution (due to the classical central limit theorem)'); Open Problem Garden, 'KPZ Universality Conjecture' (posted by T. Kojar, 2020), http://www.openproblemgarden.org/op/kpz_universality_conjecture

Human review

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

View graph

Random deposition: (Nt−t)/t⇒N(0,1)(N_t-t)/\sqrt t\Rightarrow\mathcal N(0,1)(Nt​−t)/t​⇒N(0,1)

Random deposition: $(N_t-t)/\sqrt t\Rightarrow\mathcal N(0,1)$