Actual F₂ flag homology and the dense extremal counterexample family
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-02-000002
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-02-000002/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-02-000002/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'