Weighted signed-dual compression from a clique suffix order

Proved

Erdos81.signed_dual_compression_of_suffix_order

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

chordal-graphscombinatoricsfractional-packinglinear-programming

Assume that every clique in a finite graph admits an injective perfect-elimination rank with that clique as its final block. For any feasible signed triangle dual $y$ , write $D=\sum_{e\in E(G)}y_e$ . Either $D\le0$ , or there are $1\le r<n$ and $0<M\le r$ , together with a real core weight $A$ , such that

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

and, when $r\ge3$ , $A\le r(r-1)/6$ . The proof chooses a vertex and a clique in its neighborhood maximizing the incident signed weight $M$ ; the suffix order charges every outside row by at most $M$ , while the triangle inequalities give the two core moment bounds. This theorem isolates the finite weighted aggregation from the chordal structural lemma and is the algebraic core of the C22 compression argument.

Preamble

import Definitions.Def_Erdos81_signed_triangle_dual

Formal statement

namespace Erdos81

theorem signed_dual_compression_of_suffix_order {n : ℕ}
    (G : SimpleGraph (Fin n))
    (y : Finset (Fin n) → ℝ) (hy : Erdos81.IsSignedTriangleDual G y)
    (hsuffix : ∀ (S : Finset (Fin n)), Erdos81.IsClique G S →
      ∃ rank : Fin n → ℕ, Function.Injective rank ∧
        (∀ ⦃v a b : Fin n⦄, G.Adj v a → G.Adj v b →
          rank v < rank a → rank v < rank b → a ≠ b → G.Adj a b) ∧
        (∀ v : Fin n, v ∉ S → ∀ s ∈ S, rank v < rank s)) :
    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

end Erdos81

Source

C22 candidate, Sections 5–6 (signed-neighborhood compression and aggregate triangle constraints), equations (5)–(6), https://github.com/vibemathing/problem-erdos-81-chordal-clique-partition/blob/09c2b6f3e277eb20fc34d0add65ee8d027c5bb37/research/artifacts/candidates/erdos81-a01-c22-c20-audit.md

View graph