{"id":"palomar/PALOMAR-2026-09-26-000002","url":"https://github.com/Arthur742Ramos/myerson-satterthwaite-lean/tree/f4dae9744e26a499679e4b8a7aeb9d82dd3f11ee","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-26-000002-v1.json","repo":"https://github.com/Arthur742Ramos/myerson-satterthwaite-lean","tags":["econ.TH","cs.GT","msc:91B26","mechanism-design","bilateral-trade","lean-formalization","game-theory"],"score":0,"title":"Myerson-Satterthwaite impossibility theorem (continuous bilateral-trade version)","trust":"high","domain":"econ.TH","source":"palomar","authors":["Arthur Freitas Ramos"],"reviews":0,"subject":"econ.TH","summary":"Formalizes the continuous-type bilateral-trade impossibility result: no mechanism can satisfy ex post efficiency (almost surely), Bayesian incentive compatibility, interim individual rationality, and weak ex ante budget balance when buyer and seller supports overlap. The proof uses payoff equivalence and envelope identities, together with the strict rent-gap identity B + C > S.","category":"research","comments":0,"disputed":false,"division":"econ","mentions":0,"verified":true,"discussed":0,"published":"2026-09-26","reactions":{},"formalized":true,"formalizes":[{"title":"Efficient Mechanisms for Bilateral Trading","identifier":"https://doi.org/10.1016/0022-0531(83)90048-0","relationship":"formalizes"}]}