Proposition 2 — algorithm AllocOpt solves the allocation optimization (7.22)

Let the data of Section 7.4 satisfy its standing assumptions (see AllocData): locations $M = \{1, \dots, \bar M\}$ with $\bar M \ge 1$, integer gridpoints $0 = r^m_0 < \cdots < r^m_{n(m)}$ with $n(m) \ge 1$ for $m \in M$ and $0 = r^0_0 < \cdots < r^0_{n(0)}$ for location $0$, values $c^m_n$ of convex functions at the gridpoints, the slopes $\hat c^m_n$ of (7.19), the piecewise linear functions $\tilde C_m$ of (7.20)–(7.21), and a convex function $f$ on $\mathbb R_+$.

Then Algorithm AllocOpt (Definition 4), run with any rule for breaking ties in its $\arg\min$ steps, terminates with values $c^0 = (c^0_n)_{n \in N_0}$ that satisfy (7.22) for every $n \in N_0 = \{0, 1, \dots, n(0)\}$:

In words, marginal allocation — repeatedly giving the next block of units to the location whose current marginal cost $\hat c^m_{n^*(m)}$ is smallest — solves the separable convex piecewise linear allocation problem exactly, simultaneously for every target total $r^0_n$. In Section 7.3 this computes the nested cost functions (7.14), (7.15) and (7.17) of the multi-echelon pooling model.

Formalization Note The book's Proposition 2 also bounds the number of calculations by $O\bigl((1 + \log_2 \bar M) \sum_{m \in M_0} n(m)\bigr)$; that half is not stated (an operation count with no machine model). The minimum is stated as (a) some feasible integer allocation $r = (r_m)$ attains the value and (b) no feasible integer allocation has a smaller value. Termination is structural in Lean (see AllocOpt). The tie-breaking rule is universally quantified; the book leaves it open.