{"id":"palomar/PALOMAR-2026-08-20-000004","url":"https://github.com/guanyangwang/ktv-swap-lean-comparator/tree/fd4dc985900b1fba59791067dcf3bf9341a94bda","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-20-000004-v1.json","repo":"https://github.com/guanyangwang/ktv-swap-lean-comparator","tags":["math.PR","cs.DS","math.CO","stat.CO","msc:60J10","markov-chains","contingency-tables","mixing-times","lean-formalization"],"score":0,"title":"guanyangwang/ktv-swap-lean-comparator","trust":"high","domain":"math.PR","source":"palomar","authors":["Guanyang Wang"],"reviews":0,"subject":"math.PR","summary":"Lean 4 formalization and Comparator verification of the spectral-gap theorem for the lazy swap chain on binary contingency tables with fixed margins.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-20","reactions":{},"formalized":true,"formalizes":[{"title":"Spectral Gap for the Binary Fixed-Margin Swap Chain","identifier":"arXiv:2606.22636","relationship":"formalizes"}]}