{"id":"palomar/PALOMAR-2026-08-21-000007","url":"https://github.com/lennrt/palomar-formalizations/tree/d259d35ad32d0e7c8c60ddd5a574aa987956e1d2/zenodo-21986230/palomar","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-21-000007-v2.json","repo":"https://github.com/lennrt/palomar-formalizations","tags":["math.CO","msc:05C62","msc:05C75","msc:06A07","msc:68R15","graph-theory","combinatorics","lean-formalization","bit-incidence"],"score":0,"title":"lennrt/palomar-formalizations","trust":"high","domain":"math.CO","source":"palomar","authors":["Lennart Rudolph"],"reviews":0,"subject":"math.CO","summary":"A Lean formalization of the paper's standard finite-word semantics for k-uniform two-word π-representability, its neighbourhood-trace bound binomial(k(|A|+1),k)^2, the explicit 20-by-741322 bit-incidence graph B20, and the theorem that B20 is not representable by two 2-uniform words. It also retains the companion's token-order bridge and exact arithmetic endpoints.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-03","reactions":{},"formalized":true,"formalizes":[{"title":"An Explicit Obstruction to Uniform Two-Word π-Representability","identifier":"10.5281/zenodo.21986230","relationship":"formalizes"}]}