Affine profile reduction for fractional triangle packings in split graphs
A Lean 4 / Mathlib formalization of the main result of the author's preprint "Affine Profile Reduction for Fractional Triangle Packings in Split Graphs" (Erdős #81 series, Paper I): for every finite split graph G on n vertices, |E(G)| − 2ν₃*(G) ≤ n²/6 + n/2, where ν₃* is the fractional triangle packing number (the maximum total weight of a nonnegative weighting of the triangles with load at most one on every edge). It is stated both for the paper's finite split model (clique Fin p, independent vertices, neighbourhoods) and for every split graph in Mathlib's SimpleGraph, with the definitions…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-28-000028
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-28-000028/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-28-000028/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'