{"id":"palomar/PALOMAR-2026-10-29-000005","url":"https://github.com/jtraverso/refined-absorption-lean/tree/5bfe5c7346a7b245581152dccebe363e22f072b6","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-29-000005-v1.json","repo":"https://github.com/jtraverso/refined-absorption-lean","tags":["math.CO","msc:05B05","msc:05B07","msc:05C15","msc:05C70"],"score":0,"title":"Formalizing Delcourt–Postle’s refined absorption in Lean","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"One assembled Lean formalization of principal refined absorption results and their consequences. The selected results include refined omni-absorbers and refiners, labelled reserve matchings, dense compatible decompositions, an additive compatible-absorber interface retaining independence of the entire old ambient vertex set, and existence of simple designs for every fixed q > r ≥ 2 and index λ ≥ 1 at all sufficiently large admissible orders. The literal global embedding conclusion of the survey is refuted separately from a proved piecewise replacement. The research-note endpoints give…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-29","reactions":{},"formalized":true,"formalizes":[{"title":"Refined Absorption: A New Proof of the Existence Conjecture","identifier":"doi:10.48550/arXiv.2402.17855","relationship":"formalizes"},{"title":"Refined Absorption: A New Proof of the Existence Conjecture and Its Applications to Extremal and Probabilistic Design Theory","identifier":"doi:10.1137/25M1805977","relationship":"adapts"},{"title":"Formalizing Delcourt–Postle’s refined absorption in Lean","identifier":"doi:10.5281/zenodo.23715622","relationship":"formalizes"},{"title":"Pseudorandom hypergraph matchings","identifier":"doi:10.1017/S0963548320000280","relationship":"adapts"},{"title":"A Proof of Nash-Williams' Conjecture","identifier":"doi:10.48550/arXiv.2606.11178","relationship":"adapts"}]}