§3, pp. 93–94 — in (3.3) the condition w_n ≥ 0 is automatic for integer w

Proved

ChinesePostman.Polyhedron.w_nonneg_automatic

by mikedeng1 · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

chinese-postmanp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1parity

Let $G$ be a finite graph (parallel edges allowed, no loops) and $b_n\in\{0,1\}$ the parity of the degree of node $n$ . Let $x\in\mathbb Z^E$ and $w\in\mathbb Z^N$ satisfy $x_e\ge 0$ for every edge and

\sum_{e\in E}a_{ne}x_e-2w_n=b_n\qquad (n\in N). \tag{3.3}

Then $w_n\ge 0$ for every node $n$ .

Hence the restrictions $w_n\ge 0$ can be dropped, and the variables $w_n$ eliminated, which is the step from the polyhedron in $(x,w)$ of p. 91 to the polyhedron in $x$ alone.

Preamble

import Mathlib
import Definitions.Def_ChinesePostman_Polyhedron_Setting

Formal statement

namespace ChinesePostman.Polyhedron

theorem w_nonneg_automatic {V E : Type} [Fintype V] [DecidableEq V] [Fintype E] [DecidableEq E]
    (G : Graph V E) (x : E → ℤ) (w : V → ℤ)
    (hx : ∀ e, 0 ≤ x e) (h33 : ∀ n, incidentSum G x n - 2 * w n = bParity G n) :
    ∀ n, 0 ≤ w n := by sorry

end ChinesePostman.Polyhedron

Source

Edmonds and Johnson, Matching, Euler tours and the Chinese postman, Math. Programming 5 (1973), pp. 93–94, §3, after (3.6)

Human review

Endorsed by Shuze Chen · Oct 6, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph