Theorem 5.3 — the s-t Path Decomposable Subgraph Polytope

Disproved

Disjunctive.ExtendedFormulations.path_decomposable_subgraph_polytope

by Shuze Chen · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsdisjunctive-programminggraph-theorypolytopes

This is Theorem 5.3 of Balas's Disjunctive Programming, a further analogue of Theorem 5.1 for path decompositions of an acyclic digraph.

For an acyclic digraph $G = (V,A)$ with distinguished nodes $s,t$ , the $s$ - $t$ Path Decomposable Subgraph Polytope (convex hull of incidence vectors of $W \subseteq V \setminus \{s,t\}$ such that $G(W \cup \{s,t\})$ admits an $s$ - $t$ path decomposition) is defined by

0 \le x_i \le 1\ (i \in V), \qquad x(S \setminus \Gamma^*(S)) - x(\Gamma^*(S) \setminus S) \le 0 \quad (S \subseteq V \setminus \{s,t\}),

where $\Gamma^*(S)$ is $\Gamma(S)$ with $t$ replaced by $s$ whenever $t \in \Gamma(S)$ — folding path-endings at $t$ back to the common source $s$ so the same "out-neighborhood exchange" inequality template as Theorem 5.2 applies.

Formalization Note. IsPathDecomposable (companion definition) is the degree-constrained arc encoding of "admits a path decomposition"; GammaStar implements the $t \to s$ folding exactly as displayed.

Preamble

import Mathlib
import Definitions.Def_Disjunctive_ExtendedFormulations_Basic

Formal statement

namespace Disjunctive.ExtendedFormulations

/-- Theorem 5.3 (Balas §5.2.3, p. 75-76, [13]): the `s`-`t` Path Decomposable Subgraph Polytope
of an acyclic digraph `(V,A)` is defined by the system `0 ≤ x_i ≤ 1`, `x(S \ Γ*(S)) − x(Γ*(S) \
S) ≤ 0`, `S ⊆ V \ {s,t}`. The polytope's points are incidence vectors of subsets of `V \ {s,t}`,
so both sides fix `x_s = x_t = 0`; without that the unit vector `e_s` satisfies the system and is
not in the polytope. Acyclicity is the page's own hypothesis on the digraph. -/
theorem path_decomposable_subgraph_polytope {V : Type*} [Fintype V] [DecidableEq V]
    (A : V → V → Prop) [DecidableRel A] (s t : V) (hst : s ≠ t)
    (hacyclic : IsAcyclicDigraph A) :
    PathDecomposableSubgraphPolytope A s t =
      {x : V → ℝ | (∀ i, 0 ≤ x i ∧ x i ≤ 1) ∧ x s = 0 ∧ x t = 0 ∧
        ∀ S : Finset V, s ∉ S → t ∉ S →
          xSum x (S \ GammaStar A s t S) - xSum x (GammaStar A s t S \ S) ≤ 0} := by sorry

end Disjunctive.ExtendedFormulations

Source

Balas, Disjunctive Programming, Springer 2018, DOI 10.1007/978-3-030-00148-3, p. 75, Theorem 5.3

Human review

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

View graph