Uniform n²/6 + o(n²) bound for chordal clique partitions
OpenErdos81.asymptotic_leading_boundFor every fixed , all sufficiently large finite chordal graphs on vertices have an exact edge partition into at most
cliques. The cutoff may depend on but is uniform over all chordal graphs of that order. This is a leading-coefficient statement; it does not supply the linear remainder required by the root theorem.
import Definitions.Def_erdos81_clique_partitions
namespace Erdos81
/-- Uniform asymptotic leading coefficient `1/6` for clique partitions of
finite chordal graphs. -/
theorem asymptotic_leading_bound :
∀ ε : ℝ, 0 < ε → ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n →
∀ G : SimpleGraph (Fin n), IsChordal G →
HasCliquePartitionAtMost G ((1 / 6 + ε) * (n : ℝ) ^ 2) := by sorry
end Erdos81Read-back
What the Lean code literally says, in plain math · gpt-5.6-luna
For every real number ε with ε greater than 0, there exists a natural number n₀ such that for every natural number n with n₀ ≤ n, and for every simple graph G whose vertex set is Fin n, if there exists an injective assignment of a natural-number rank to the vertices such that any two distinct later neighbors of the same vertex are adjacent, then there exists a finite collection P of finite vertex sets such that every member of P is a clique, every edge of G belongs to exactly one member of P, and the real-valued number of members of P is at most (1⁄6 + ε) times the square of n regarded as a real number. Here Fin n is the n-element vertex type, and all natural numbers n satisfying the stated inequality are included.
Confirmed by the mission captain (proposal self-audit).