Erdős Problem #81 — Chordal Clique Partitions: Papers I–IV

This record contains four official author preprints from a research program on Erdős Problem #81, concerning edge partitions into cliques and the structure of chordal graphs. The series progresses from fractional extremal bounds and constructions for split graphs to integral bounds for all chordal graphs, quantitative stability, and extensions to rooted simplicial defect. Each paper is accompanied in the linked GitHub repository by Lean 4 formalizations, frozen sources, reproducibility material, integrity manifests, and documented audit evidence. Paper I — Affine Profile Reduction for Fractional Triangle Packings in Split Graphs (v1.3). For every split graph G on n vertices, it proves |E(G)| − 2ν₃*(G) ≤ n²/6 + n, where ν₃*(G) is the fractional triangle-packing number. This is a finite fractional result and does not itself give an integral clique-partition theorem. Paper II — Complete-Split Extremizers for a Fractional Triangle-Cover Functional on Chordal Graphs (v1.2). For every integer n ≥ 1, it determines the exact maximum of |E(G)| − 2τ₃*(G) over n-vertex chordal graphs as ⌊(2n+1)²/24⌋, attained by a complete-split graph. This is an exact fractional-cover extremal theorem and does not itself give an integral clique-partition theorem. Paper III — Linear-Error Clique Partitions of Split Graphs via Structured Triangle Packing (v1.5). It proves cp(G) ≤ n²/6 + O(n) for every split graph G, with sharp quadratic coefficient 1/6. It resolves the split-graph case of Erdős Problem #81 at the conjectured quadratic scale and supplies packing and rounding infrastructure used in Paper IV. It does not determine the least uniform linear coefficient. Paper IV — Clique partitions with rooted simplicial defect: quantitative stability and sharp eventual bounds (v1.23). For every chordal graph G on n vertices, it proves c₄(G) ≤ M(n) + b for an absolute constant b, where M(n) = ⌊n(n+1)/6⌋ and c₄ restricts partition pieces to cliques of order at most four. This implies the bound cp(G) ≤ n²/6 + O(n) asked in Erdős Problem #81. For sufficiently large n, the exact maximum is M(n), attained by complete-split graphs even against unrestricted clique partitions. The structural results control both graphs and their near-optimal partitions. For sufficiently large chordal graphs with c₄(G) ≥ M(n) − δ, in the stated deficit range, at most 16δ edge edits produce a complete-split graph. The same clique root controls every unrestricted partition with at most M(n) + τ pieces: at most τ + 48δ pieces are noncanonical, containing at most 10τ + 480δ edges in total. Paper IV extends quantitative stability and the order-four eventual bound to every fixed rooted simplicial defect, and proves approximation and stability results for sublinear defect. Its thresholds are explicit but impractical. Scope and attribution. Other proofs of the extremal bounds and related stability results are credited and compared in Paper IV; no priority for the extremal values is claimed. The Lean proofs use only the standard foundational axioms, with software dependencies explicitly recorded. The universal strengthening b = 0 is not proved. These manuscripts have not undergone human peer review, and documented AI audits do not constitute a specialist priority determination. The eight deposited PDFs are the English and Spanish editions of Papers I–IV. The complete public packages and verification evidence are preserved at the immutable GitHub commit linked below.