{"id":"palomar/PALOMAR-2026-09-14-000004","url":"https://github.com/BochaoKong/permutohedron/tree/886b7364faa7ab6db7d9eb36cf5a0c26e37d388a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-14-000004-v1.json","repo":"https://github.com/BochaoKong/permutohedron","tags":["math.CO","msc:52B05","discrete-geometry","lean","permutohedron"],"score":0,"title":"To cover a permutohedron","trust":"high","domain":"math.CO","source":"palomar","authors":["Bochao Kong"],"reviews":0,"subject":"math.CO","summary":"This Lean 4 formalization of Kong and Zeng's To cover a permutohedron (arXiv:2509.13877v3, 9 April 2026) determines the minimum number of affine hyperplanes needed to cover the permutation vertices of (1,...,n), excluding the hyperplane containing every vertex. The exact answer is n for odd n at least 3, and n-1 for even n at least 4. It also proves that an arbitrary injective real tuple of length n at least 2 has the sharp hyperplane intersection bound (n-1)! when its n-1 signed critical values are distinct. Genuine polynomial-root path lifting establishes local transpositions and the cycle…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-14","reactions":{},"formalized":true,"formalizes":[{"title":"To cover a permutohedron","identifier":"https://arxiv.org/abs/2509.13877v3","relationship":"adapts"},{"title":"Covering the permutohedron by affine hyperplanes","identifier":"https://arxiv.org/abs/2305.06202v3","relationship":"adapts"}]}