Three Rings I — Privacy Composition via Mahler, Jensen, and Szegő (Lean 4)

Lean 4 + Mathlib formalization of a complex-analytic framework for privacy composition in protocols whose distinguishing-advantage sequence obeys a self-similar Mahler-type recurrence. Approximately 110 theorems across 26 files, with 0 sorry and exactly 3 axioms encoding classical results from Mahler-function theory (Nishioka), ergodic theory of the doubling map (Walters), and Szegő H² boundary-trace theory (Garnett, Koosis, Simon). Includes the LaTeX source of the companion paper, the compiled PDF, and a Python reproducibility script.