Proof of Proposition 3.1: $\#I_=N/4$ and $\#J_=\tfrac34N$

Proved

ScenarioReduction.BinaryTree.IStar_card

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

combinatoricsp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1scenario-reduction

Let $K\in\mathbb N$ and $k_0\ge1$ with $k_0+2\le K$ , and let $N=2^K$ . The set $I_*$ of scenarios of the regular binary tree whose branch at level $k_0$ differs from the branch at level $k_0+1$ and whose branches at levels $k_0+1$ and $k_0+2$ agree, and its complement $J_*=\{1,\dots,N\}\setminus I_*$ , have

\#I_*=2^{k_0-1}\cdot2\cdot2^{K-k_0-2}=\tfrac14\,2^K=\tfrac N4,\qquad \#J_*=N-\#I_*=\tfrac34N.

The set $J_*$ is the deleted set that attains the minimal reduction cost when $n=N/4$ scenarios are kept.

Formalization Note $N/4$ and $\frac34N$ are written as $2^{K-2}$ and $3\cdot2^{K-2}$ , exact since $K\ge3$ . $I_*$ is defined by branch indices rather than by the signs of $\delta^k_{i_k}$ (see the definition IStar); the two agree when $\delta^{k_0},\delta^{k_0+1},\delta^{k_0+2}>0$ , and the count is a statement about indices only.

Preamble

import Mathlib
import Definitions.Def_ScenarioReduction_BinaryTree_IStar

Formal statement

namespace ScenarioReduction.BinaryTree

theorem IStar_card (K k0 : ℕ) (hk0 : 1 ≤ k0) (hk0K : k0 + 2 ≤ K) :
    (IStar K k0).card = 2 ^ (K - 2) ∧ (IStar K k0)ᶜ.card = 3 * 2 ^ (K - 2) := by sorry

end ScenarioReduction.BinaryTree

Source

Heitsch, Römisch, Scenario Reduction Algorithms in Stochastic Programming, Comput. Optim. Appl. 24 (2003), p. 197, proof of Proposition 3.1, display for #I_* and #J_*

Read-back

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

Let $K, k_0 \in \mathbb{N}$ with $1 \le k_0$ and $k_0 + 2 \le K$ . Consider the set $I_*(K, k_0)$ of maps $\sigma : \{0,\dots,K-1\} \to \{0,1\}$ such that:

$\sigma(k_0-1) \ne \sigma(k_0)$ , and
$\sigma(k_0) = \sigma(k_0+1)$ .

In level terms: the entries at levels $k_0+1$ and $k_0+2$ agree, and the entry at level $k_0$ is the opposite value. The statement asserts

|I_*(K,k_0)| = 2^{K-2} \quad\text{and}\quad |I_*(K,k_0)^c| = 3\cdot 2^{K-2},

where the complement is taken within the set of all $2^K$ maps.

Degenerate cases. The hypotheses force $K \ge 3$ . So the natural-number subtraction $K - 2$ does not truncate, and all three levels $k_0, k_0+1, k_0+2$ lie in $\{1, \dots, K\}$ . No default level values arise.

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

Proof of Proposition 3.1: #I∗=N/4\#I_*=N/4#I∗​=N/4 and #J∗=34N\#J_*=\tfrac34N#J∗​=43​N

Proof of Proposition 3.1: $\#I_=N/4$ and $\#J_=\tfrac34N$