Eq. (17), unrolled recursion — $c^{[i]}_{ku}=\min\{c^{[1]}_{ku},c^{[1]}_{ku_{i-1}},\dots,c^{[1]}_{ku_1}\}=\min_{j\notin J^{[i-1]}\setminus\{u\}}c(\omega_k,\omega_j)$

Proved

ScenarioReduction.ForwardSelection.cStep_eq_min

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

greedy-algorithmp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1scenario-reductionstochastic-programming

Let $\omega_1,\dots,\omega_N$ be scenarios, $c$ the cost (3), and $u_1,u_2,\dots$ any sequence of indices, with $J^{[i]}=\{1,\dots,N\}\setminus\{u_1,\dots,u_i\}$ and $c^{[i]}$ the recursively updated cost matrices of Algorithm 2.4. For every step $i\ge 1$ , every $u\in J^{[i-1]}$ and every $k$ ,

c^{[i]}_{ku}=\min\bigl\{c^{[1]}_{ku},c^{[1]}_{ku_{i-1}},\dots,c^{[1]}_{ku_1}\bigr\}=\min_{j\notin J^{[i-1]}\setminus\{u\}}c(\omega_k,\omega_j).

This is the step of the proof of Theorem 2.5 that unwinds the pairwise update of Algorithm 2.4 into the inner minimum of the forward selection principle (16).

Formalization Note No run hypothesis is assumed: the identity holds for every sequence $u$ . The minimum on the right is Finset.inf' over the complement of $J^{[i-1]}\setminus\{u\}$ , which is $\{u,u_1,\dots,u_{i-1}\}$ .

Preamble

import Mathlib
import Definitions.Def_ScenarioReduction_ForwardSelection_fmCost
import Definitions.Def_ScenarioReduction_ForwardSelection_reductionCost
import Definitions.Def_ScenarioReduction_ForwardSelection_IsFastForwardRun

Formal statement

namespace ScenarioReduction.ForwardSelection

/-- Eq. (17), Heitsch–Römisch 2003, p. 194 (the unrolled recursion). For any sequence `u`, any
step `i ≥ 1` and any `v ∈ J^{[i-1]}`, the recursively computed cost of Algorithm 2.4 is
`c^{[i]}_{kv} = min{c^{[1]}_{kv}, c^{[1]}_{k u_{i-1}}, …, c^{[1]}_{k u₁}} = min_{j ∉ J^{[i-1]} ∖ {v}} c(ωₖ, ωⱼ)`. -/
theorem cStep_eq_min {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {N : ℕ} (h : ℝ → ℝ) (hh : IsGrowthFunction h) (ω₀ : E)
    (ω : Fin N → E) (u : ℕ → Fin N) (i : ℕ) (hi : 1 ≤ i) (v : Fin N)
    (hv : v ∈ Jstep u (i - 1)) (k : Fin N) :
    cStep (scenCost h ω₀ ω) u i k v =
      ((Jstep u (i - 1)).erase v)ᶜ.inf' (compl_erase_nonempty _ _)
        (fun j => scenCost h ω₀ ω k j) := by sorry

end ScenarioReduction.ForwardSelection

Source

Heitsch, Römisch, Scenario Reduction Algorithms in Stochastic Programming, Comput. Optim. Appl. 24 (2003), p. 194, proof of Theorem 2.5, eq. (17), lines 2–6

Read-back

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

Setting and hypotheses.

$E$ is a finite-dimensional real normed vector space.
$h:\mathbb R\to\mathbb R$ is continuous and nondecreasing on $[0,\infty)$ , with $h(0)=0$ and $h\ge0$ there.
$\omega_0\in E$ , $N\in\mathbb N$ , and $\omega'_0,\dots,\omega'_{N-1}\in E$ indexed by $[N]=\{0,\dots,N-1\}$ .
$u:\mathbb N\to[N]$ is an arbitrary sequence $u_1,u_2,\dots$ . It need not come from any selection rule, and repeats are allowed.
$i\ge1$ , and $k\in[N]$ is arbitrary.
$v\in J^{[i-1]}=[N]\setminus\{u_1,\dots,u_{i-1}\}$ .

Definitions.

Cost matrix: $C_{kj}=\max\{1,h(\|\omega'_k-\omega_0\|),h(\|\omega'_j-\omega_0\|)\}\,\|\omega'_k-\omega'_j\|$ .
Recursive costs: $c^{[1]}_{kv}=C_{kv}$ , and $c^{[i]}_{kv}=\min\{c^{[i-1]}_{kv},c^{[i-1]}_{k\,u_{i-1}}\}$ for $i\ge2$ .

Claim.

c^{[i]}_{kv}=\min_{j\in[N]\setminus(J^{[i-1]}\setminus\{v\})}C_{kj}.

Because $v\in J^{[i-1]}$ , the index set of the minimum is exactly $\{v,u_1,\dots,u_{i-1}\}$ .

Degenerate cases.

For $i=1$ : $J^{[0]}=[N]$ , the minimum is over $\{v\}$ alone, and the claim reads $c^{[1]}_{kv}=C_{kv}$ .
$k=v$ is allowed, in which case both sides equal $0$ because $C_{vv}=0$ .
The existence of $v$ forces $N\ge1$ .
Repeated values among $u_1,\dots,u_{i-1}$ simply repeat elements of the index set.
No weights $p$ appear.

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