Signed edge dual for fractional edge-and-triangle partitions

Definition

Erdos81_signed_triangle_dual

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

chordal-graphscombinatoricsfractional-packinglinear-programmingtriangle-packing

Let $G$ be a finite simple graph. A feasible signed triangle dual assigns a real weight $y_e$ to every unordered edge such that

y_e\le1\quad(e\in E(G)),\qquad \sum_{e\in E(T)}y_e\le1\quad(T\text{ a triangle of }G).

Its objective is the total signed edge weight

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

There is no lower bound on an edge weight. This is the dual interface for fractional partitions with exact edge loads and with pieces restricted to edges and triangles. Keeping the weights signed is necessary because the primal edge constraints are equalities.

Formalization Note A weight function is defined on finite vertex sets. Only the two-element sets in the existing canonical edge partition contribute to the objective or edge constraints. A triangle's three edges are its two-element subsets; values on other sets are irrelevant.

Definition code

import Definitions.Def_Erdos81_edgePairPartition
import Mathlib.Algebra.BigOperators.Group.Finset.Basic

namespace Erdos81

/-- The total signed weight of the unordered graph edges. -/
noncomputable def signedEdgeWeight {n : ℕ} (G : SimpleGraph (Fin n))
    (y : Finset (Fin n) → ℝ) : ℝ :=
  ∑ e ∈ edgePairPartition G, y e

/-- The dual of the exact fractional edge-and-triangle partition problem.
Edge weights are signed; only upper bounds are imposed. -/
def IsSignedTriangleDual {n : ℕ} (G : SimpleGraph (Fin n))
    (y : Finset (Fin n) → ℝ) : Prop :=
  (∀ e ∈ edgePairPartition G, y e ≤ 1) ∧
  ∀ C : Finset (Fin n), C.card = 3 → IsClique G C →
    (∑ e ∈ C.powersetCard 2, y e) ≤ 1

end Erdos81

Source

C22 candidate, Section 3, equation (4), https://github.com/vibemathing/problem-erdos-81-chordal-clique-partition/blob/09c2b6f3e277eb20fc34d0add65ee8d027c5bb37/research/artifacts/candidates/erdos81-a01-c22-c20-audit.md; Boyd and Vandenberghe, Convex Optimization, Section 5.2.1, printed p. 224, equations (5.17)–(5.20), https://web.stanford.edu/~boyd/cvxbook/bv_cvxbook.pdf .

View graph