Sufficient optimality condition for the greedy set $\{l_1,\dots,l_{N-n}\}$ of rule (11)

Proved

ScenarioReduction.ForwardSelection.backward_optimality

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

p2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1scenario-reductionstochastic-programming

Let $N\ge 2$ , let $\omega_1,\dots,\omega_N$ be scenarios with probabilities $p_i>0$ , $\sum_ip_i=1$ , let $c$ be the cost (3), let $1\le n<N$ , and let $l_1,\dots,l_{N-n}$ be selected by rule (11). Suppose that for every $i=1,\dots,N-n$ the set

\arg\min_{j\neq l_i}c(\omega_{l_i},\omega_j)\setminus\{l_1,\dots,l_{i-1},l_{i+1},\dots,l_{N-n}\}

is nonempty. Then $L=\{l_1,\dots,l_{N-n}\}$ is a solution of (8): it has $N-n$ elements and

D_L=\min\bigl\{D_J:J\subset\{1,\dots,N\},\ \#J=N-n\bigr\}.

When the condition holds, the greedy backward choice solves the set-covering problem (8) exactly; this is the motivation the paper gives for its backward reduction algorithms.

Formalization Note The conclusion bundles the nonemptiness of the complement of $L$ (needed for $D_L$ to be defined) with the explicit cardinality $\#L=N-n$ (so $L$ is feasible for (8)) and the statement that $D_L$ is the least element of $\{D_J:\#J=N-n\}$ .

Preamble

import Mathlib
import Definitions.Def_ScenarioReduction_ForwardSelection_fmCost
import Definitions.Def_ScenarioReduction_ForwardSelection_reductionCost
import Definitions.Def_ScenarioReduction_ForwardSelection_IsBackwardGreedy

Formal statement

namespace ScenarioReduction.ForwardSelection

/-- Sufficient optimality condition, Heitsch–Römisch 2003, p. 191. If `l₁, …, l_{N-n}` are selected
by rule (11) and, for every `i`, some minimizer of `c(ω_{lᵢ}, ωⱼ)` over `j ≠ lᵢ` lies outside
`{l₁, …, l_{i-1}, l_{i+1}, …, l_{N-n}}`, then `J = {l₁, …, l_{N-n}}` solves problem (8): it has
`N − n` elements and `D_J` is the minimum of `D_{J'}` over all `J'` with `#J' = N − n`. -/
theorem backward_optimality {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {N : ℕ} (h : ℝ → ℝ) (hh : IsGrowthFunction h) (ω₀ : E)
    (ω : Fin N → E) (p : Fin N → ℝ) (hp : ∀ i, 0 < p i) (hsum : ∑ i, p i = 1)
    (hN : 1 < N) (n : ℕ) (hn1 : 1 ≤ n) (hnN : n < N) (l : ℕ → Fin N)
    (hl : IsBackwardGreedy (scenCost h ω₀ ω) p hN (N - n) l)
    (hcond : ∀ i ∈ Finset.Icc 1 (N - n), ∃ j : Fin N, j ≠ l i ∧
      (∀ j' : Fin N, j' ≠ l i → scenCost h ω₀ ω (l i) j ≤ scenCost h ω₀ ω (l i) j') ∧
      j ∉ ((Finset.Icc 1 (N - n)).erase i).image l) :
    ∃ hL : ((Finset.Icc 1 (N - n)).image l)ᶜ.Nonempty,
      ((Finset.Icc 1 (N - n)).image l).card = N - n ∧
      IsLeast {x : ℝ | ∃ J : Finset (Fin N), ∃ hJ : Jᶜ.Nonempty, J.card = N - n ∧
          x = reductionCost (scenCost h ω₀ ω) p J hJ}
        (reductionCost (scenCost h ω₀ ω) p ((Finset.Icc 1 (N - n)).image l) hL) := by sorry

end ScenarioReduction.ForwardSelection

Source

Heitsch, Römisch, Scenario Reduction Algorithms in Stochastic Programming, Comput. Optim. Appl. 24 (2003), p. 191, paragraph after eq. (12)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. Let $E$ be a finite-dimensional real normed vector space. Fix a natural number $N$ and write $[N] = \{0, 1, \dots, N-1\}$ for the index set of size $N$ . The data are:

a function $h : \mathbb{R} \to \mathbb{R}$ satisfying the predicate $\mathrm{IsGrowthFunction}(h)$ ;
a point $\omega_0 \in E$ ;
scenarios $\omega_0', \dots$ given as a map $\omega : [N] \to E$ , $j \mapsto \omega_j$ ;
weights $p : [N] \to \mathbb{R}$ with $p_j > 0$ for every $j$ and $\sum_{j \in [N]} p_j = 1$ ;
a natural number $n$ ;
a sequence $l : \mathbb{N} \to [N]$ , $i \mapsto l_i$ , defined for every natural number $i$ (including $i = 0$ ).

Write $c = \mathrm{scenCost}(h, \omega_0, \omega)$ . It is a two-argument function on $[N] \times [N]$ whose values can be compared with $\le$ . The statement uses four notions that are defined elsewhere and not shown here: $\mathrm{IsGrowthFunction}$ , $\mathrm{scenCost}$ , $\mathrm{IsBackwardGreedy}$ and $\mathrm{reductionCost}$ . Their definitions are not available to this read-back, so they are treated as opaque. Nothing below depends on what they unfold to.

Hypotheses.

$1 < N$ .
$1 \le n < N$ , so $N - n$ lies between $1$ and $N-1$ .
$\mathrm{IsBackwardGreedy}(c, p, N-n, l)$ holds. The proof of $1 < N$ is also passed to this predicate.
For every $i \in \{1, \dots, N-n\}$ $i \in {1, \dots, N - n}$ there is some $j \in [N]$ $j \in [N]$ with all three of the following properties:
- $j \ne l_i$ ;
- $j$ minimizes $c(l_i, \cdot)$ over the indices other than $l_i$ :

c(l_i, j) \le c(l_i, j') \quad \text{for all } j' \in [N],\ j' \ne l_i;

$j \notin \{\, l_k : k \in \{1, \dots, N-n\},\ k \ne i \,\}$ .

Conclusion. Let $J^* = \{l_1, \dots, l_{N-n}\} \subseteq [N]$ , the set of values of $l$ at positions $1$ through $N-n$ . The statement asserts three things:

The complement $[N] \setminus J^*$ is nonempty. The proof of this fact is supplied to $\mathrm{reductionCost}$ .
$|J^*| = N - n$ . This means $l_1, \dots, l_{N-n}$ are pairwise distinct.
$\mathrm{reductionCost}(c, p, J^*)$ is the least element of the set of real numbers

\bigl\{\, \mathrm{reductionCost}(c, p, J) \;:\; J \subseteq [N],\ [N] \setminus J \ne \emptyset,\ |J| = N - n \,\bigr\}.

Being the least element means it belongs to the set and is $\le$ every member of it.

The value $\mathrm{reductionCost}(c, p, J)$ is a real number, and it also takes a proof that $J$ 's complement is nonempty. Because $N - n < N$ , every $J$ with $|J| = N - n$ automatically has a nonempty complement, so that side condition does not shrink the set being minimized over.

Degenerate and edge cases.

Sizes. The hypotheses rule out $N \le 1$ , $n = 0$ and $n \ge N$ , so the index set is never empty or a single point and $N - n \ge 1$ .
Subtraction. $N - n$ is subtraction of natural numbers, but since $n < N$ it never truncates.
Distinctness. The last condition in hypothesis 4 does not forbid repeated values among the $l_k$ . Hypothesis 4 as written does not require distinctness, and the conclusion asserts it. Whether distinctness, or anything else, is forced by $\mathrm{IsBackwardGreedy}$ cannot be determined from the code shown.
Unused positions. Only $l_1, \dots, l_{N-n}$ appear in hypothesis 4 and in the conclusion. The values $l_0$ and $l_i$ for $i > N - n$ are constrained, if at all, only through $\mathrm{IsBackwardGreedy}$ .
Extreme case $n = 1$ . Here $J^*$ is meant to have $N-1$ elements. For each $i$ , the witness $j$ must avoid $l_i$ and the other $N-2$ selected indices, and must also minimize $c(l_i, \cdot)$ off $l_i$ .
Unused data. The space $E$ , the point $\omega_0$ , the scenarios $\omega$ and the function $h$ enter only through $c$ and the predicate $\mathrm{IsGrowthFunction}(h)$ . The hypotheses $p_j > 0$ and $\sum_j p_j = 1$ are used only through whatever $\mathrm{IsBackwardGreedy}$ and $\mathrm{reductionCost}$ do with $p$ .
Vacuity. Whether the hypotheses can all hold at once, or might be vacuous, depends on the opaque predicates $\mathrm{IsGrowthFunction}$ and $\mathrm{IsBackwardGreedy}$ . It cannot be determined from this code.

Human review

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

View graph

Sufficient optimality condition for the greedy set {l1,…,lN−n}\{l_1,\dots,l_{N-n}\}{l1​,…,lN−n​} of rule (11)

Sufficient optimality condition for the greedy set $\{l_1,\dots,l_{N-n}\}$ of rule (11)