Machine-Checked Finite Differential Privacy in Lean

Differential privacy proofs often rely on finite-sum arguments that are routine on paper but sensitive to side conditions: events must be represented explicitly, stochastic validity is separate from the privacy inequality, and post-processing and composition rely on nonnegativity. We present a compact Lean 4 formalization of finite pure differential privacy that exposes these proof obligations theorem-by-theorem. The artifact models mechanisms as real-valued kernels, proves equivalence between pointwise and finite-event privacy, verifies post-processing and deterministic post-processing, proves two-stage adaptive and disjoint-product parallel composition theorems, and checks randomized response and a generic finite exponential mechanism. It also includes bundled stochasticity-plus-privacy preservation lemmas and a checked signed-kernel counterexample with a negative entry showing why post-processing nonnegativity cannot be dropped. The contribution is proof-engineering clarity rather than an automated theorem-proving system or a deployable privacy library. The development is intentionally limited to finite events and real-valued kernels; it does not cover approximate differential privacy, continuous distributions, verified samplers, floating-point semantics, or arbitrary interactive protocols.