Partition the edges of a chordal graph into cliques: is $n^2/6+O(n)$ always enough? (Erdős #81)

A graph $G$ is chordal if it has no induced cycle of length greater than $3$ (equivalently, every cycle on $\geq 4$ vertices has a chord). Let $G$ be a chordal graph on $n$ vertices. Can the edge set of $G$ always be partitioned into $n^2/6+O(n)$ cliques (complete subgraphs)? That is, is there an absolute constant $C$ such that for every $n$-vertex chordal graph the edges can be split into pairwise edge-disjoint cliques using at most $n^2/6+Cn$ of them?

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq preferred, else a full written proof with all steps) that the edges of every $n$-vertex chordal graph partition into $n^2/6+O(n)$ cliques — giving an explicit constant in the $O(n)$ term and the covering procedure — OR a disproof exhibiting an explicit family of chordal graphs together with a proof that no clique edge-partition of size $(1/6+\epsilon)n^2$ exists for infinitely many $n$. ADVANCES: improve the general upper bound strictly below the best stated in the background (currently $(1/4-\epsilon)n^2$), i.e. a proof or reproducible certificate that every $n$-vertex chordal graph's edges partition into $\le cn^2+O(n)$ cliques with a constant $c<1/4$; OR improve the split-graph bound below $\frac{3}{16}n^2+O(n)$; OR compute, with a reproducible program and an exhaustiveness certificate, the exact minimum clique edge-partition number of all chordal graphs up to a new record vertex count, sharpening the leading constant. Deliver the proof file, or the improved construction/analysis with proof, or the search code plus certified value table.