Prove2Me

Eq. (3.7) — a blossom inequality is violated iff xˉ(W:V−W)+d(T)−2xˉ(T)+sˉ(W)<1\bar x(W:V-W)+d(T)-2\bar x(T)+\bar s(W)<1

Proved
PadbergRao.UpperBound.eq_3_7

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatorial-optimizationgraph-theorymatchingp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let G=(V,E)G=(V,E) be a finite simple graph with node capacities bb and edge bounds dd, let xˉ∈RE\bar x\in\mathbb{R}^E and let sˉ=b−Axˉ\bar s=b-A\bar x be its node slacks. For every W⊆VW\subseteq V and every T⊆(W:V−W)T\subseteq (W:V-W),

xˉ(W)+xˉ(T)>12(b(W)+d(T)−1)  ⟺  xˉ(W:V−W)+d(T)−2xˉ(T)+sˉ(W)<1,\bar x(W)+\bar x(T)>\tfrac12\bigl(b(W)+d(T)-1\bigr) \iff \bar x(W:V-W)+d(T)-2\bar x(T)+\bar s(W)<1,

where xˉ(W)=∑e∈E(W)xˉe\bar x(W)=\sum_{e\in E(W)}\bar x_e and xˉ(W:V−W)\bar x(W:V-W) is the sum of xˉe\bar x_e over the cut-set of WW.

The right-hand side is a cut-set condition: edges of (W:V−W)−T(W:V-W)-T appear with value xˉe\bar x_e, edges of TT in complemented form de−xˉed_e-\bar x_e, and each node of WW contributes its slack. This rewriting of the violated blossom inequality is what the proof of Theorem 3.1 uses.

Formalization Note The equivalence is stated for an arbitrary real vector xˉ\bar x; the oddness of b(W)+d(T)b(W)+d(T) plays no role in it.

Preamble
import Mathlib
import Definitions.Def_PadbergRao_UpperBound_bMatchingSystem
Formal statement
namespace PadbergRao.UpperBound

/-- Padberg–Rao (1982), p. 75, Eq. (3.7): for `T ⊆ (W : V − W)`, the point `x̄` violates the
blossom inequality (3.3), `x̄(W) + x̄(T) > ½(b(W) + d(T) − 1)`, if and only if
`x̄(W : V − W) + d(T) − 2x̄(T) + s̄(W) < 1`. -/
theorem eq_3_7 {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (b : V → ℕ) (d : Sym2 V → ℕ) (x : Sym2 V → ℝ) (W : Finset V) (T : Finset (Sym2 V))
    (hT : T ⊆ cutEdges G W) :
    ((∑ i ∈ W, (b i : ℝ)) + (∑ e ∈ T, (d e : ℝ)) - 1) / 2
        < (∑ e ∈ edgesWithin G W, x e) + ∑ e ∈ T, x e ↔
      (∑ e ∈ cutEdges G W, x e) + (∑ e ∈ T, (d e : ℝ)) - 2 * (∑ e ∈ T, x e)
        + (∑ i ∈ W, slack G b x i) < 1 := by sorry

end PadbergRao.UpperBound
Source
Padberg, Rao, Odd Minimum Cut-Sets and b-Matchings, Math. Oper. Res. 7 (1982), p. 75, Section 3, Eq. (3.7) (equivalence with (3.3) used on p. 77 in the proof of Theorem 3.1)
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph