Fractional clique decompositions of dense partite graphs
Source: github.com/jtraverso/montgomery-fractional-clique-decomposi…
A Lean 4 / Mathlib formalization of the main theorem of R. Montgomery, "Fractional clique decompositions of dense partite graphs" (arXiv:1603.01039; Combin. Probab. Comput. 26 (2017)): for r ≥ 3, every balanced K_r-divisible r-partite graph with parts of size n in which every vertex has at least (1 − 1/(10⁶r³))n neighbours in every other part has a fractional K_r-decomposition (Theorem 1.1); and its non-partite consequence: every graph on n vertices with minimum degree at least (1 − 1/(10⁶r³))n has a fractional K_r-decomposition. The whole proof is formalized: clique counts (Proposition 3.2,…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-03-000019
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-03-000019/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-11-03-000019/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'