{"id":"palomar/PALOMAR-2026-10-02-000003","url":"https://github.com/Arthur742Ramos/cremer-mclean-lean/tree/e0578ad905149bb579a2b4fe7930720055497c50","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-02-000003-v1.json","repo":"https://github.com/Arthur742Ramos/cremer-mclean-lean","tags":["econ.TH","cs.GT","msc:91B26","mechanism-design","auction-theory","game-theory","lean-formalization"],"score":0,"title":"Cremer-McLean Full Surplus Extraction Theorem","trust":"high","domain":"econ.TH","source":"palomar","authors":["Arthur Freitas Ramos","David Barros Hulak","Ruy Jose Guerra Barretto de Queiroz"],"reviews":0,"subject":"econ.TH","summary":"A Lean 4 formalization of the Cremer-McLean full surplus extraction theorem (Econometrica, 1988): for a single indivisible object with finitely many bidders, finite type spaces, and a correlated joint prior with full support, if every bidder's family of conditional distributions over the others' types is convex independent (no conditional lies in the convex hull of the rest), then there exists a Bayesian incentive compatible, interim individually rational direct mechanism that allocates ex post efficiently and extracts the full surplus: every bidder's interim expected utility is zero, so…","category":"research","comments":0,"disputed":false,"division":"econ","mentions":0,"verified":true,"discussed":0,"published":"2026-10-02","reactions":{},"formalized":true,"formalizes":[{"title":"Full Extraction of the Surplus in Bayesian and Dominant Strategy Auctions","identifier":"","relationship":"formalizes"}]}