Dross's theorem on fractional triangle decompositions
A Lean 4 / Mathlib formalization of Dross's theorem: every finite graph on n vertices with minimum degree at least 9n/10 has a fractional triangle decomposition, i.e. nonnegative real weights on its triangles such that every edge lies in triangles of total weight exactly one. The threshold 9/10 is the exact one of the paper. The proof follows the max-flow/min-cut approach: the existence of the weights is reduced to a flow problem, a finite max-flow/min-cut theorem (included) is applied, and every cut is bounded below by counting triangles and K4s, with a peeling reduction for heavy triangles.
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-15-000008
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-15-000008/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-10-15-000008/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'