{"id":"palomar/PALOMAR-2026-08-27-000014","url":"https://github.com/sneed-and-feed/lean-theorems-1/tree/d14072a07f6c5a4dbca1428c7d013828d7c1a9da","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-27-000014-v1.json","repo":"https://github.com/sneed-and-feed/lean-theorems-1","tags":["math.CO","math.AT","msc:05E45","msc:57Q05","msc:52A35","msc:55M20","combinatorics","lean","sperner-lemma","topology"],"score":0,"title":"sneed-and-feed/lean-theorems-1","trust":"high","domain":"math.CO","source":"palomar","authors":["Sneed & Feed Formalization Team"],"reviews":0,"subject":"math.CO","summary":"A machine-checked Lean 4 formalization of the general n-dimensional combinatorial Sperner parity theorem on abstract n-dimensional pseudomanifolds with boundary for arbitrary dimension n : ℕ. Proves the local door-counting parity invariant on (n+1)-simplices, the global double-counting identity on door-facet incidences, and the master parity congruence modulo 2 relating panchromatic (n+1)-simplices to boundary doors. The theorem is conditional on an odd number of boundary (n-1)-doors; obtaining the classical geometric Sperner lemma for simplicial subdivisions of geometric simplices with…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-27","reactions":{},"formalized":true,"formalizes":[{"title":"Neuer Beweis für die Invarianz der Dimensionszahl und des Gebietes","identifier":"","relationship":"adapts"},{"title":"Simplicial Approximation of Fixed Points","identifier":"","relationship":"adapts"}]}