Asymptotic fractional triangle packing bound for chordal graphs

Open

Erdos81.chordal_fractional_triangle_packing_leading_bound

by Yuning · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

chordal-graphscombinatoricsfractional-packingtriangle-packing

Let $m(G)$ denote the number of edges of an $n$ -vertex chordal graph $G$ , and let $\nu_3^*(G)$ be the maximum total weight of a fractional packing of triangles. For every $\eta>0$ , there is $n_0$ such that every $n\ge n_0$ and every chordal $G$ on $n$ vertices admit a fractional triangle packing of weight at least

\frac{m(G)}2-\left(\frac1{12}+\eta\right)n^2.

This is the chordal structural input needed for the sharp $1/6$ leading coefficient in an exact clique partition.

Formalization Note The theorem gives a witness packing rather than introducing an optimization operator.

Preamble

import Definitions.Def_Erdos81_triangle_packings

Formal statement

namespace Erdos81

/-- The chordal-graph structural input: asymptotically, every chordal graph has
enough fractional edge-disjoint triangles to leave the `n²/6` leading term. -/
theorem chordal_fractional_triangle_packing_leading_bound :
    ∀ η : ℝ, 0 < η → ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n →
      ∀ G : SimpleGraph (Fin n), IsChordal G →
        ∃ w : Finset (Fin n) → ℝ,
          IsFractionalTrianglePacking G w ∧
          (edgeCount G : ℝ) / 2 - (1 / 12 + η) * (n : ℝ) ^ 2 ≤
            fractionalTrianglePackingWeight w := by
  sorry

end Erdos81

Source

Prove2Me candidate derivation for Erdos81.asymptotic_leading_bound, commit 09c2b6f3e277eb20fc34d0add65ee8d027c5bb37, research/artifacts/candidates/erdos81-a01-c22-c20-audit.md; target record https://prove2.me/theorems/e19444a7-f040-43e0-80b8-6a211856a8d7

View graph