Proposition 3.2, proof — $\#I_{} = \frac29 N$ and $\#J_{} = \frac79 N$

Proved

ScenarioReduction.TernaryTree.card_IStarStar

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

combinatoricsp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1scenario-reductionscenario-tree

Let $K \ge 3$ , $N = 3^K$ , and $1 \le k_0 \le K - 2$ . Let $I_{**}$ be the set of scenarios of a regular ternary tree that take the middle branch at level $k_0$ and outer branches at levels $k_0+1, k_0+2$ , or an outer branch at level $k_0$ and middle branches at levels $k_0+1, k_0+2$ , and let $J_{**} = \{1, \dots, N\} \setminus I_{**}$ . Then

\#I_{**} = 3^{k_0-1} \cdot 6 \cdot 3^{K-k_0-2} = \tfrac29\,3^K = \tfrac29 N, \qquad \#J_{**} = N - \#I_{**} = \tfrac79 N.

The count shows that the reduction kept at $I_{**}$ has exactly $\tfrac29 N$ scenarios, the threshold of Proposition 3.2.

Formalization Note $\tfrac29 N$ and $\tfrac79 N$ are written as $2 \cdot 3^{K-2}$ and $7 \cdot 3^{K-2}$ (natural-number exponents, $K \ge 3$ ). $I_{**}$ is defined by branch indices, not by the values of the increments; see the definition IStarStar.

Preamble

import Mathlib
import Definitions.Def_ScenarioReduction_TernaryTree_IStarStar

Formal statement

namespace ScenarioReduction.TernaryTree

theorem card_IStarStar (K k0 : ℕ) (hk0 : 1 ≤ k0) (hk0K : k0 ≤ K - 2) (hK : 3 ≤ K) :
    (IStarStar K k0).card = 2 * 3 ^ (K - 2) ∧ (IStarStar K k0)ᶜ.card = 7 * 3 ^ (K - 2) := by sorry

end ScenarioReduction.TernaryTree

Source

Heitsch, Römisch, Scenario Reduction Algorithms in Stochastic Programming, Comput. Optim. Appl. 24 (2003), pp. 198–199, proof of Proposition 3.2, definition of I_** and the display on p. 199

Read-back

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

Setting. Consider the $3^K$ branch assignments $\sigma : \{0, \dots, K-1\} \to \{0,1,2\}$ . Say that $\sigma$ is:

middle at level $l$ if $1 \le l \le K$ and $\sigma(l-1) = 1$ ;
outer at level $l$ if $1 \le l \le K$ and $\sigma(l-1) \in \{0,2\}$ .

$I_{**}(K, k_0)$ is the set of assignments that satisfy at least one of these patterns:

middle at $k_0$ , outer at $k_0+1$ and outer at $k_0+2$ ;
outer at $k_0$ , middle at $k_0+1$ and middle at $k_0+2$ .

Hypotheses.

$K \ge 3$ .
$1 \le k_0$ .
$k_0 \le K - 2$ . Since $K \ge 3$ , this is genuine subtraction and means $k_0 + 2 \le K$ .

Claim. Both of the following hold:

|I_{**}(K,k_0)| = 2 \cdot 3^{K-2} \qquad\text{and}\qquad \bigl|\text{complement of } I_{**}(K,k_0)\bigr| = 7 \cdot 3^{K-2}.

Here the complement is taken within the set of all $3^K$ assignments.

Degenerate cases. The hypotheses rule out every $K \le 2$ and $k_0 = 0$ . The exponent $K-2$ is therefore at least $1$ , so no truncated subtraction occurs. The smallest admissible case is $K = 3$ , $k_0 = 1$ , where the claim reads $6$ and $21$ .

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

Proposition 3.2, proof — #I∗∗=29N\#I_{**} = \frac29 N#I∗∗​=92​N and #J∗∗=79N\#J_{**} = \frac79 N#J∗∗​=97​N

Proposition 3.2, proof — $\#I_{} = \frac29 N$ and $\#J_{} = \frac79 N$