{"id":"palomar/PALOMAR-2026-09-20-000013","url":"https://github.com/insammael/one-sided-affine-hat-guessing/tree/991721669233b41666e6f56b1471e58eb63d719e","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-20-000013-v1.json","repo":"https://github.com/insammael/one-sided-affine-hat-guessing","tags":["math.CO","msc:05C57","msc:91A43","msc:11T06","combinatorics","hat-guessing","finite-fields","lean"],"score":0,"title":"One-Sided Affine Obstructions in Complete Bipartite Hat Guessing","trust":"high","domain":"math.CO","source":"palomar","authors":["Myunglae Jo"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 formalization of manuscript Theorem 2.4: for every finite field K with |K| at least 4 and every m at least 1, a coordinatewise-affine strategy on the class of size |K|-1 cannot be completed to a winning strategy by arbitrary deterministic rules on the opposite class of size m, with respect to the fixed finite-field labeling.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-20","reactions":{},"formalized":true,"formalizes":[{"title":"One-Sided Affine Obstructions in Complete Bipartite Hat Guessing","identifier":"10.5281/zenodo.22568338","relationship":"formalizes"}]}