Prove2Me

Eq. (3.6) — 2x(W)+x(W:V−W)+x(T)+s(W)+t(T)=b(W)+d(T)2x(W)+x(W:V-W)+x(T)+s(W)+t(T)=b(W)+d(T)

Proved
PadbergRao.UpperBound.eq_3_6

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∈REx\in\mathbb{R}^E be any point, and let s=b−Axs=b-Ax and t=d−xt=d-x be the slack vectors of the constraints Ax≤bAx\le b and x≤dx\le d. For every W⊆VW\subseteq V and every T⊆(W:V−W)T\subseteq (W:V-W),

2x(W)+x(W:V−W)+x(T)+s(W)+t(T)=b(W)+d(T),2x(W)+x(W:V-W)+x(T)+s(W)+t(T)=b(W)+d(T),

where x(W)=∑e∈E(W)xex(W)=\sum_{e\in E(W)}x_e, x(W:V−W)=∑e∈(W:V−W)xex(W:V-W)=\sum_{e\in(W:V-W)}x_e, x(T)=∑e∈Txex(T)=\sum_{e\in T}x_e, s(W)=∑i∈Wsis(W)=\sum_{i\in W}s_i and t(T)=∑e∈T(de−xe)t(T)=\sum_{e\in T}(d_e-x_e).

The identity is obtained by adding the rows of Ax+s=bAx+s=b indexed by WW and the rows of x+t=dx+t=d indexed by TT. It is what turns the blossom inequality (3.3) into a cut condition.

Formalization Note The identity is stated for an arbitrary real vector xx; neither feasibility nor positivity of b,db,d is needed.

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

/-- Padberg–Rao (1982), p. 75, Eq. (3.6): adding the rows of `Ax + s = b` with index in `W`
and the rows of `x + t = d` with index in `T ⊆ (W : V − W)` gives
`2x(W) + x(W : V − W) + x(T) + s(W) + t(T) = b(W) + d(T)`. -/
theorem eq_3_6 {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) :
    2 * (∑ e ∈ edgesWithin G W, x e) + (∑ e ∈ cutEdges G W, x e) + (∑ e ∈ T, x e)
        + (∑ i ∈ W, slack G b x i) + (∑ e ∈ T, ((d e : ℝ) - x e))
      = (∑ i ∈ W, (b i : ℝ)) + ∑ e ∈ T, (d e : ℝ) := 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.6) (with (3.4))
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