{"id":"palomar/PALOMAR-2026-10-01-000015","url":"https://github.com/Arthur742Ramos/top-trading-cycles-lean/tree/9fc2a2130983b494831f95b831b9cf28620cf556","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-01-000015-v1.json","repo":"https://github.com/Arthur742Ramos/top-trading-cycles-lean","tags":["cs.GT","econ.TH","msc:91B68","mechanism-design","housing-markets","matching","lean"],"score":0,"title":"Gale's Top Trading Cycles (Shapley-Scarf Housing Market)","trust":"high","domain":"cs.GT","source":"palomar","authors":["Arthur Freitas Ramos","David Barros Hulak","Ruy Jose Guerra Barretto de Queiroz"],"reviews":0,"subject":"cs.GT","summary":"A Lean formalization of Gale's top trading cycles algorithm (1974) for the Shapley-Scarf housing market. Finitely many agents (Fin n) each own exactly one house (the endowment is a bijection endow : Fin n ≃ Fin n) and have strict preferences over houses, given most-preferred-first as per-agent permutations rank i : Fin n ≃ Fin n; agent i strictly prefers house a over house b iff (rank i).symm a < (rank i).symm b. The comparator-checked results are TTC.Palomar.ttcTerminates: the TTC procedure (each remaining agent points to the owner of their favourite remaining house, each house points to…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-01","reactions":{},"formalized":true,"formalizes":[{"title":"On cores and indivisibility","identifier":"","relationship":"formalizes"},{"title":"The top trading cycles algorithm","identifier":"","relationship":"formalizes"},{"title":"Weak versus strong domination in a market with indivisible goods","identifier":"","relationship":"formalizes"},{"title":"Incentive compatibility in a market with indivisible goods","identifier":"","relationship":"formalizes"}]}