Uniform Rényi Privacy Amplification by Shuffling

We study independent one-message shuffling through a common channel with replacement adjacency and arbitrary deterministic backgrounds. Under one local Rényi budget, without a pointwise likelihood-ratio cap, the optimal uniform same-order rate is $n^{-\min\{1,\alpha-1\}}$ for fixed $\alpha>1$; a local KL budget alone gives no uniform amplification. We determine the exact asymptotic worst-case approximate-DP envelope at each fixed positive privacy parameter and the leading inverse calibration at failure probability $d/n$ for all fixed $\alpha>1$. Matching upper bounds are uniform over channels and alphabets varying with $n$. At and above order three, the calibration coefficient is the square root of an attained local triple-variance frontier, realizable on at most nine output symbols. At order three we evaluate this frontier on a certified budget interval and identify the unique extremal ratio law. The same frontier determines the limiting central-window profile for $\alpha>2$ and the logarithmic moderate-window exponent. Under local $\chi^2$ diameter $C$, the exact asymptotic neighboring coefficient is $2C(C+5)/(C+4)$; we also give explicit finite amplification bounds and a fixed-channel background reduction. Formal verification. All statements of the paper have been formalized in Lean 4 (version 4.35.0) with Mathlib (release v4.35.0), including the computer-assisted order-three theorem, for which all certificate computations are checked by the Lean kernel. The formal proofs contain no sorry and use only the standard axioms propext, Classical.choice and Quot.sound. The project builds from scratch, every module passes a replay by the Lean kernel (leanchecker), and all theorems of the interface file Statements.lean, together with everything they depend on (69 078 declarations in total), were rechecked by the independent type checker nanoda. ChatGPT was used to write the Lean code and Claude to audit it; the author takes full responsibility for all results. Files. The PDF is the paper (24 pages). The ZIP archive Uniform_Renyi_arXiv_source_2026-11-09.zip is the LaTeX source. Its folder anc/ contains the exact rational polynomial certificate for the computer-assisted order-three theorem (verify_order_three_frontier.py, needs only the Python standard library) and further exact checks. The ZIP archive UniformRenyiShuffle-Lean-1.0.0-2026-11-09.zip is the Lean project UniformRenyiShuffle 1.0.0; its file MAP.md gives the Lean name of every statement of the paper. Changes from version 1. The Lean formalization is added. The paper and its LaTeX source are unchanged.