A Lean formalization of the finite-support empirical DRO reduction

This technical note and standalone Lean packet formalize the finite-support empirical distributionally robust optimization reduction in Henry Lam's Recovering Best Statistical Guarantees via the Empirical Divergence-based Distributionally Robust Optimization, arXiv:1605.09349v1 (2016), Proposition 1 and its proof. For a sample of positive finite size classified among finitely many support points, the observation-weight Burg uncertainty set and support-weight Burg ball attain exactly the same objective values. Their lower and upper robust values therefore agree at the stated radius scaling. Aggregation preserves the objective and decreases Burg divergence by logarithm concavity within nonempty classes. Conversely, equal splitting of each support mass among its observations preserves both divergence and objective. The formal model explicitly imposes zero mass on unobserved classes and positive mass on observed classes; the extended-real generator excludes zero observation weights at finite radius. The feasibility directions work for arbitrary real radius. The final proposition has nonnegative kappa and radius kappa/(2n), arbitrary support and real-valued cost maps, and no additional attainment assumption. Statistical coverage and the rest of the source paper are outside scope. Three exact accepted proofs, all five platform definition dependencies, complete independent target/axiom audits with autoImplicit=false, immutable Lean 4.33.1 and Mathlib pins, the established archive verifier and fresh reproduction evidence are included. Three invalid controls test rejection of changed proof bytes, a weaker statement and an extra local axiom. Only propext, Classical.choice and Quot.sound occur as proof axioms; compiled third-party caches remain trusted inputs. Original mathematics is credited to Henry Lam. mikedeng1 supplied the formal interfaces and explicit support conditions; Shuze Chen reviewed statements. Shared divergence and robust-mean interfaces credit Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen, and Duchi, Glynn and Namkoong. Relevant Lean/Mathlib authors retain specific credit. Alexander Richard Towell directed; substantial OpenAI Codex assistance in formalization, verification, submission and documentation is disclosed. No mathematical novelty, independent human review or source-author endorsement is claimed. All three accepted proofs were publicly submitted on October 20, 2026. Their original disclosures and earlier central metadata record are separate from this first DOI archive, version 1.1.0. This is one coherent archival contribution and does not increase the count of accepted targets. The owning development repository remains private.