{"id":"palomar/PALOMAR-2026-10-29-000004","url":"https://github.com/jtraverso/erdos81-complete-split-extremizers/tree/7961c3aba6062b03de3df28f42d339c1aec145d8","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-29-000004-v1.json","repo":"https://github.com/jtraverso/erdos81-complete-split-extremizers","tags":["math.CO","msc:05C70","msc:05C75","msc:05C35"],"score":0,"title":"Complete-split extremizers for the fractional triangle-cover deficit on chordal 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 \"Complete-Split Extremizers for a Fractional Triangle-Cover Functional on Chordal Graphs\" (Erdős #81 series, Paper II). For a finite simple graph G let τ₃*(G) be its fractional triangle cover number (the least total weight of a nonnegative weighting of vertex pairs giving every triangle weight at least one on its edges) and Φ_τ(G) = |E(G)| − 2τ₃*(G). For every n ≥ 1, every chordal graph on n vertices satisfies Φ_τ(G) ≤ ⌊(2n + 1)²/24⌋, and equality is attained by a complete-split graph K_p ∨ K̄_q with p + q = n…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-29","reactions":{},"formalized":true,"formalizes":[{"title":"Complete-Split Extremizers for a Fractional Triangle-Cover Functional on Chordal Graphs","identifier":"doi:10.5281/zenodo.23478825","relationship":"formalizes"}]}