Lemma 8.3.2 — subgraphs of the support graph have no more edges than vertices

Proved

MatousekLP.Scheduling.support_subgraph_edges_le

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

basic-feasible-solutionbipartite-graphlinear-programmingp2o-batch-b23bp2o-gran-per-chapterp2o-plan-bookp2o-v1scheduling

Let $d_{ij} > 0$ be running times of $n$ jobs on $m$ machines, let $T \in \mathbb{R}$ , and let $(t, x)$ be an optimal solution of the linear program $\mathrm{LPR}(T)$ that satisfies Assumption 8.3.1 (the columns of the constraint matrix belonging to the nonzero $x_{ij}$ are linearly independent). Let $G = (M \cup J, E)$ with $E = \{\{i,j\} : x_{ij} > 0\}$ be the support graph of $x$ .

Then every subgraph of $G$ has at most as many edges as vertices: if $M' \subseteq M$ , $J' \subseteq J$ and $E' \subseteq E$ is a set of edges each joining a machine of $M'$ to a job of $J'$ , then

|E'| \le |M'| + |J'| .

This counting property is what makes the support of a basic optimal solution sparse enough to be rounded: it forces the graph to be a forest with at most one extra edge per component.

Formalization Note A subgraph is given by vertex sets M' : Finset (Fin m), J' : Finset (Fin n) and an edge set E' ⊆ supportEdges x whose pairs (i, j) satisfy i ∈ M' and j ∈ J'; this covers both deleting edges and deleting vertices with their incident edges. The standing assumption $d_{ij} > 0$ of Section 8.3 is a hypothesis.

Preamble

import Mathlib
import Definitions.Def_MatousekLP_Scheduling_Schedule
import Definitions.Def_MatousekLP_Scheduling_LPRelaxation

Formal statement

namespace MatousekLP.Scheduling

/-- Lemma 8.3.2 (Matoušek–Gärtner, p. 152). Let `(t, x)` be an optimal solution of
`LPR(T)` satisfying Assumption 8.3.1, and let `G = (M ∪ J, E)` be its support graph,
`E = {{i, j} : x_ij > 0}`. In any subgraph of `G` — a set `M'` of machines, a set
`J'` of jobs, and a set `E' ⊆ E` of edges joining `M'` to `J'` — the number of
edges is at most the number of vertices. -/
theorem support_subgraph_edges_le {m n : ℕ} (d : Matrix (Fin m) (Fin n) ℝ)
    (hd : ∀ i j, 0 < d i j) (T t : ℝ) (x : Matrix (Fin m) (Fin n) ℝ)
    (hopt : LPROptimal d T t x) (hA : Assumption831 d T x)
    (M' : Finset (Fin m)) (J' : Finset (Fin n)) (E' : Finset (Fin m × Fin n))
    (hE'E : E' ⊆ supportEdges x) (hE'V : ∀ e ∈ E', e.1 ∈ M' ∧ e.2 ∈ J') :
    E'.card ≤ M'.card + J'.card := by sorry

end MatousekLP.Scheduling

Source

Matoušek & Gärtner, Understanding and Using Linear Programming, Springer 2007, p. 152, Lemma 8.3.2

Human review

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

View graph