{"id":"palomar/PALOMAR-2026-09-02-000002","url":"https://github.com/lennrt/palomar-formalizations/tree/a7cc03716e7683cfc0c66cfc0d3b30e00a7a2923/zenodo-21892997/palomar","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-02-000002-v1.json","repo":"https://github.com/lennrt/palomar-formalizations","tags":["math.CO","math.AT","msc:05C35","msc:05C69","msc:55U10","combinatorics","graph-homology","lean","flag-complexes"],"score":0,"title":"Actual F₂ flag homology and the dense extremal counterexample family","trust":"high","domain":"math.CO","source":"palomar","authors":["Lennart Rudolph"],"reviews":0,"subject":"math.CO","summary":"A finite-chain formalization of the F₂ content of Theorem 1.1 and Proposition 3.1 in the source paper. Lean defines the literal flag-chain groups of a finite graph using unordered edges and three-vertex clique faces, their d1 and d2 maps, and actual H1 as ker(d1)/range(d2). It proves that the paper's family G_n has F₂ first Betti number exactly two for every n at least seven, proves the universal F₂ upper bound beta1 <= 2 for every n-vertex graph with choose(n,2)-n edges, and bundles these facts with the exact density and no-complete-bipartite-spanning obstruction. The literal d1-d2 identity…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-02","reactions":{},"formalized":true,"formalizes":[{"title":"An Infinite Dense Counterexample Family for Extremal First Betti Numbers of Flag Complexes","identifier":"10.5281/zenodo.21892997","relationship":"formalizes"}]}