{"id":"palomar/PALOMAR-2026-10-28-000028","url":"https://github.com/jtraverso/erdos81-fractional-split-profiles/tree/f8690bcba57bddc5deefd8626f5b07e0d63e6086","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-28-000028-v2.json","repo":"https://github.com/jtraverso/erdos81-fractional-split-profiles","tags":["math.CO","msc:05C70","msc:05C72","msc:90C05"],"score":0,"title":"Affine profile reduction for fractional triangle packings in split graphs","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-29","reactions":{},"formalized":true,"formalizes":[{"title":"Affine Profile Reduction for Fractional Triangle Packings in Split Graphs","identifier":"doi:10.5281/zenodo.23478825","relationship":"formalizes"},{"title":"Colorability and Realizability (Erdős #81 series, Paper V)","identifier":"doi:10.5281/zenodo.23479507","relationship":"adapts"}]}