Weighted-neighborhood compression certificate for chordal signed duals

Open

Erdos81.chordal_signed_dual_compression

by Zexuan Liu · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

chordal-graphscombinatoricsfractional-packinglinear-programmingtriangle-packing

Let $G$ be a chordal graph on $n$ vertices, and let $y$ be any feasible signed triangle dual. Write

D=\sum_{e\in E(G)}y_e.

Either $D\le0$ , or there exist an integer $r$ and real numbers $M,A$ satisfying

1\le r<n,\qquad 0<M\le r,

D\le A+(n-r)M, \qquad A+(r-1)M\le\frac{r(r-1)}2,

and

r\ge3\quad\Longrightarrow\quad A\le\frac{r(r-1)}6.

This numerical certificate records the information from weighted-neighborhood compression needed to optimize the signed dual objective. Its intended geometric quantities are the size of a weight-selected neighborhood clique, the total signed weight from its maximizing vertex, and the total signed weight inside that clique. The statement does not identify $r$ with the maximum clique size. The number $A$ may be negative.

The nonpositive alternative includes edgeless graphs and the orders zero and one. The guard on the final inequality preserves the small-core cases. This is a formalization target extracted from the mission's C22 candidate; the chordal compression argument remains to be verified.

Preamble

import Definitions.Def_Erdos81_signed_triangle_dual

Formal statement

theorem Erdos81.chordal_signed_dual_compression {n : ℕ}
    (G : SimpleGraph (Fin n)) (hG : Erdos81.IsChordal G)
    (y : Finset (Fin n) → ℝ) (hy : Erdos81.IsSignedTriangleDual G y) :
    Erdos81.signedEdgeWeight G y ≤ 0 ∨
      ∃ (r : ℕ) (M A : ℝ),
        1 ≤ r ∧ r < n ∧ 0 < M ∧ M ≤ (r : ℝ) ∧
        Erdos81.signedEdgeWeight G y ≤ A + ((n : ℝ) - r) * M ∧
        A + ((r : ℝ) - 1) * M ≤ (r : ℝ) * ((r : ℝ) - 1) / 2 ∧
        (3 ≤ r → A ≤ (r : ℝ) * ((r : ℝ) - 1) / 6) := by
  sorry

Source

C22 candidate, Sections 4–5 (clique-suffix elimination and signed-neighborhood compression), equations (5)–(6), with the aggregate edge/triangle constraints of Sections 6 and 8, https://github.com/vibemathing/problem-erdos-81-chordal-clique-partition/blob/09c2b6f3e277eb20fc34d0add65ee8d027c5bb37/research/artifacts/candidates/erdos81-a01-c22-c20-audit.md. The moment inequalities are obtained by summing the incident triangle constraints and, for r >= 3, the core triangle constraints. This is a candidate-derived open lemma, not a result attributed to the 1993 Erdős–Ordman–Zalcstein paper.

View graph