All missions

Motivation and actuarial context

A prospective life insurance reserve describes the expected remaining loss on a policy at a valuation date. An alternative way to understand the insurer's total future loss is to allocate it between individual policy years. Each year produces an insurance cashflow and a change in the reserve needed to support future benefits. When properly centred by the reserve balance, the resulting annual gains have expectation zero. Hattendorff's theorem connects this allocation to the striking result that losses for distinct years are uncorrelated and the variance of total discounted loss is the sum of their individual discounted variances.

The classical finite annual result is covered by Gerber, Life Insurance Mathematics, third edition, §6.7, particularly equations (6.7.3) and (6.7.6)–(6.7.10) [1]. A modern actuarial derivation is developed in the European Actuarial Journal article An elementary derivation of Hattendorff's theorem [2]. The connection to martingale increments is emphasised by Norberg [3] and by Gerber, Leung and Shiu [4].

This mission formalises a finite-scenario annual-loss allocation and Hattendorff-style variance identity. It makes the distinction between a proved algebraic decomposition and the deeper stochastic theorem explicit: annual orthogonality is a hypothesis of the capstone, with its derivation from conditional mortality and reserve dynamics reserved for a subsequent extension. Thus the mission does not claim that an arbitrary pair of yearly cashflows is uncorrelated.

Finite mortality scenarios and expected values

Let $\Omega$ be a finite sample space, and let $w_\omega$ denote the probability assigned to scenario $\omega$. A valid scenario probability law has nonnegative weights summing to one. The mission defines the finite weighted expectation

$$\mathbb E_w[X]=\sum_{\omega\in\Omega}w_\omega X(\omega).$$

Its supporting results establish expected values of constants and linear combinations. For scenario cashflows $X$ and $Y$, weighted variance and covariance are defined by

$$\begin{aligned} \operatorname{Var}_w(X) &=\sum_\omega w_\omega \left(X(\omega)-\mathbb E_w[X]\right)^2,\\ \operatorname{Cov}_w(X,Y) &=\sum_\omega w_\omega \left(X(\omega)-\mathbb E_w[X]\right) \left(Y(\omega)-\mathbb E_w[Y]\right). \end{aligned}$$

The definitions work for arbitrary real arrays of weights, while the actuarial probability interpretation assumes valid scenario probabilities. Finite sums avoid moment-integrability issues without imposing an artificial condition such as independence between years.

Annual insurer gains and reserve changes

Let $C_k(\omega)$ be the net insurer cash outgo during policy year $k$, measured at that year's start, and let $R_k$ be the deterministic opening prospective reserve under a given in-force valuation basis. With per-year discount factor $v$, define the annual gain or loss component

$$G_k(\omega)=C_k(\omega)+vR_{k+1}-R_k.$$

The term $vR_{k+1}$ represents the discounted liability carried into the next year, while $R_k$ is the reserve released from the opening position. The sign convention is insurer loss, so positive values represent net outgo or an adverse change.

If the annual reserve balance is

$$\mathbb E_w[C_k]+vR_{k+1}=R_k,$$

then linearity gives

$$\mathbb E_w[G_k]=0.$$

This is the first actuarial component of Hattendorff's framework: properly reserved annual losses are centred under the valuation basis. The finite scenario weights need to sum to one, and the reserve balance must be assumed or established. Merely defining $G_k$ does not give it zero mean.

Discounted loss allocation and telescoping

The total discounted annual gain through $n$ years is

$$L_n(\omega)=\sum_{0\le k<n}v^kG_k(\omega).$$

Expanding the annual gain definition and telescoping the reserve terms gives the pathwise identity

$$\boxed{ L_n(\omega)= \sum_{0\le k<n}v^k C_k(\omega) +v^n R_n-R_0. }$$

The terminal reserve is retained explicitly. It must not be assumed zero for an arbitrary incomplete policy horizon. This exact finite-period formula corresponds to the annual allocation of loss and reserve changes discussed in [1, §6.7, equation (6.7.3)], with the horizon and terminal liability clearly stated.

The empty-term case has $L_0=0$. Increasing the horizon from $n$ to $n+1$ adds precisely $v^nG_n$. These boundary and recursion lemmas form a useful independent verification layer for the finite sum.

Orthogonality and the variance decomposition

When distinct annual gains have zero covariance,

$$\operatorname{Cov}_w(G_i,G_j)=0 \qquad (i\ne j,\;i,j<n),$$

their discounted aggregate variance has no cross-year terms:

$$\boxed{ \operatorname{Var}_w(L_n) =\sum_{0\le k<n}v^{2k}\operatorname{Var}_w(G_k). }$$

Importantly, uncorrelated does not mean independent. Annual losses are linked by the same insured life, survival history and reserve process. Hattendorff's theorem establishes the required uncorrelatedness from the correct conditional insurance model; the zero-covariance condition is an explicit hypothesis in this mission's finite-scenario algebraic capstone. This distinction is important for the formalisation and is consistent with [1, equations (6.7.6)–(6.7.8)] and the martingale explanation in [3–4].

The supporting theorem on variance of a sum, variance scaling and covariance symmetry makes the algebra behind the annual allocation explicit. Zero-mean gain and zero-covariance assumptions must be separately justified when moving from this finite abstract setting to a particular mortality model.

Capstone and subsequent formal development

The capstone assumes a finite scenario law whose weights sum to one, a sequence of yearly cashflows $C_k$, deterministic reserves $R_k$, a reserve balance for each year $k<n$, and pairwise zero covariance of the resulting annual gains. It then proves three statements together: each year's gain is centred, the discounted variance splits additively by year, and the discounted sum telescopes to net cashflows plus the terminal reserve less opening reserve.

Five definitions establish weighted expectation, annual reserve gain, discounted aggregate gain, variance and covariance. Thirteen supporting theorem targets handle elementary expectation algebra, finite-year telescoping, zero-mean reserve gains, covariance symmetry and orthogonal variance decomposition. A capstone combines these results.

This is explicitly the finite algebraic and reserve-accounting stage, not a complete proof of Hattendorff's theorem for arbitrary life insurance contracts. A later mission should construct the curtate-lifetime annual innovations using the published reserve recursions of Mission XI, establish the conditional mean-zero property from survival information and derive cross-year orthogonality without assuming it. Only that later bridge will discharge the substantive stochastic obligation. No independence claim is made.

Every item is a proposed Lean statement. The isolated-module imports appear before other Lean commands, and no unpublished definition is treated as already available to the live compiler.

References

[1] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, §6.7, Allocation of the Overall Loss to Policy Years, equations (6.7.3)–(6.7.10). Publisher book record.

[2] An elementary derivation of Hattendorff's theorem, European Actuarial Journal (2021), DOI: 10.1007/s13385-020-00256-9. Develops the annual insurer-loss formula using the prospective reserve recurrence.

[3] Norberg, Ragnar (1992), “Hattendorff's theorem and Thiele's differential equation generalized”, Scandinavian Actuarial Journal, pp. 2–14. Places the annual uncorrelated-loss principle in a broader stochastic and martingale setting.

[4] Gerber, Hans U., Leung, Bartholomew P. K. and Shiu, Elias S. W. (2003), “Indicator Function and Hattendorff Theorem”, North American Actuarial Journal, 7(1), pp. 38–47. Relates the actuarial theorem to uncorrelated martingale increments.

Motivation and actuarial context

A traditional life-insurance model may have one way of exiting the insured state, namely death. Many actuarial contracts instead allow multiple mutually exclusive decrements. A policyholder might exit through death, disability, withdrawal or retirement, and different causes may trigger different benefits. A net premium reserve must therefore allow one-year payments that vary by the cause of exit, as well as the liability continuing for policies that do not exit.

Gerber, Life Insurance Mathematics, third edition, Chapter 7 §7.5 [1], derives the multiple-decrement reserve and its one-year recursion, followed by a decomposition of premium into reserve accumulation and the expected cost of the net amounts at risk. The same models are related to the broader multiple-state framework developed in Dickson, Hardy and Waters (2009), Chapter 8, including §8.8 on multiple decrements [2].

This mission formalises the one-year multiple-decrement reserve balance and premium decomposition for a finite set of causes. It is a deliberately local actuarial model: it handles one policy year and deterministic opening and closing reserves, without assuming that the complete lifetime-dependent reserve functions from Missions XI or XII have already been published.

One-year decrement law

Let $J$ be a finite set of mutually exclusive causes of exit. Fix a policy in force at the start of the year. Let $p$ denote the conditional probability of surviving in force to the following year, and $q_j$ the conditional probability of decrement cause $j\in J$ during the year.

The one-year decrement law is valid when

$$p\ge0,\qquad q_j\ge0,\qquad p+\sum_{j\in J}q_j=1.$$

The possible decrement causes are alternative outcomes of the same year. Their probabilities are added because the causes are mutually exclusive; they are not independent risks. The survival probability refers to remaining in force, rather than necessarily being alive in every possible post-decrement state.

The formal model treats $J$ as any finite type. No nonempty-type hypothesis is required: if $J$ is empty, the unit-probability law forces $p=1$ and reduces to certain survival, without exit benefits.

Benefit payments and the annual reserve balance

Let $b_j$ be the benefit payable at the end of the year following exit for cause $j$. The conditional expected exit benefit before discounting is

$$B=\sum_{j\in J}q_jb_j.$$

Let $R$ be the reserve immediately before the current premium, let $R_+$ denote the reserve required at the next annual valuation for surviving policies, and let $v$ be the annual discount factor. Assume the year-end reserve for policies which exit is zero after payment of the cause-specific benefit. Under this timing, the expected present value of the following-year liability is

$$v\left(pR_+ +\sum_{j\in J}q_jb_j\right).$$

The required premium $\Pi$ is defined by the annual reserve balance

$$\boxed{R+\Pi=v\left(pR_+ +\sum_{j\in J}q_jb_j\right).}$$

Equivalently, the formula defines

$$\Pi=v\left(pR_++B\right)-R.$$

This is the discrete conditional one-year multiple-decrement generalisation of the annual life-reserve recursion in [1, equation (7.5.2)]. It does not assert that the reserves $R$ and $R_+$ were derived from a complete prospective valuation, nor that an arbitrary premium chosen externally automatically satisfies the balance. Those tasks require a separate multi-year model.

Savings and risk premium components

The one-year required premium can be separated into two economically interpretable parts. The savings premium grows the opening reserve towards the next reserve:

$$\Pi^{\mathrm{sav}}=vR_+-R.$$

The risk premium finances benefits above or below the amount of reserve that would otherwise remain at the next annual valuation:

$$\Pi^{\mathrm{risk}}= v\sum_{j\in J}q_j(b_j-R_+).$$

Since the decrement law satisfies $\sum_jq_j=1-p$,

$$\begin{aligned} \Pi^{\mathrm{sav}}+\Pi^{\mathrm{risk}} &=vR_+-R+ v\sum_jq_j(b_j-R_+)\\ &=v\left(pR_++\sum_jq_jb_j\right)-R\\ &=\Pi. \end{aligned}$$

Thus the principal premium decomposition is

$$\boxed{\Pi=\Pi^{\mathrm{sav}}+\Pi^{\mathrm{risk}}.}$$

This follows the savings and risk-premium interpretation of [1, equations (7.5.3)–(7.5.5)]. A negative risk premium is possible algebraically when cause benefits are lower than the continuing reserve. The formal theorem does not assume all monetary amounts are nonnegative.

Boundary cases and formal theorem graph

If $p=0$, every in-force policy exits during the year, and the continuing reserve term vanishes:

$$\Pi=vB-R.$$

If no decrement can occur, $p=1$ and $q_j=0$ for every cause, the required premium reduces to the savings component alone,

$$\Pi=\Pi^{\mathrm{sav}}=vR_+-R.$$

If every cause of exit pays exactly the same amount as the following-year reserve, $b_j=R_+$, the risk component is zero. Scaling all monetary benefits and reserve amounts by a common factor scales the premium by that factor.

The draft introduces five definitions: a valid annual decrement law, expected cause benefit, required annual premium, savings premium and risk premium. Eleven supporting theorems establish probability conditions, zero and scaled benefits, reserve balance, zero-survival and no-decrement limits, risk-free exits and the premium decomposition. The capstone combines the one-year reserve balance with the savings/risk identity.

The definitions and theorem types are independent of unconfirmed Prove2Me actuarial declarations from earlier missions. Imports of local definitions are explicitly placed at the beginning of each Lean file, and the proposed statements do not treat a Draft declaration as a published theorem. The proofs of the individual statements remain to be supplied after captain and moderator review.

References

[1] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 7, Multiple Decrements, §7.5, The Net Premium Reserve, equations (7.5.1)–(7.5.5). In particular (7.5.2) is the annual multiple-decrement recursion and (7.5.3)–(7.5.5) separate the savings and risk portions.

[2] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 8, Cambridge University Press, §8.8, Multiple Decrement Models.

[3] Dickson, Hardy and Waters (2009), Chapter 7, Policy Values, annual policy-value recursions. The one-cause formula provides the earlier special case from which the multiple-cause generalisation develops.

Motivation

Many problems in optimization, variational inequalities and saddle-point computation can be written as a monotone inclusion: find $x$ with $0 \in A(x) + B(x)$, where $A$ is a set-valued maximally monotone operator (a subdifferential, a normal cone) and $B$ is single-valued (a gradient, a skew saddle operator). Splitting methods treat $A$ only through its resolvent and $B$ only through forward evaluations. The classical forward-backward method needs $B$ to be cocoercive, which rules out saddle-point operators; Tseng's forward-backward-forward method removes this but needs two evaluations of $B$ per step.

Malitsky and Tam (arXiv:1808.04162, SIAM J. Optim. 30(2), 2020) introduced the forward-reflected-backward method, which needs only monotonicity and Lipschitz continuity of $B$ and one new evaluation of $B$ per iteration. Its step size in Section 2 depends on a global Lipschitz constant $L$ of $B$. Such a constant is often unknown, expensive to estimate, overly conservative, or nonexistent when $B$ is only locally Lipschitz. Section 3 of the paper replaces the fixed step by a linesearch (backtracking) and proves convergence for locally Lipschitz $B$ in finite dimensions. This mission formalizes that result.

Setting

Let $H$ be a finite-dimensional real inner product space. An operator $A : H \rightrightarrows H$ is monotone if $\langle x - y, u - v\rangle \ge 0$ whenever $u \in A(x)$, $v \in A(y)$, and maximally monotone if moreover its graph is not properly contained in the graph of another monotone operator. For $t > 0$ the resolvent $J_{tA} = (I + tA)^{-1}$ is the map with $t^{-1}(w - J_{tA}w) \in A(J_{tA}w)$ for every $w$. A map $B : H \to H$ is monotone if $\langle x - y, B(x) - B(y)\rangle \ge 0$, and locally Lipschitz if every point has a neighbourhood on which $B$ is Lipschitz. The zero set is $(A+B)^{-1}(0) = \{x : -B(x) \in A(x)\}$.

Fix $\delta \in (0,1)$ and $\sigma \in (0,1)$. Given $x_k$, $x_{k-1}$ and the previous step $\lambda_{k-1}$, the trial point at step $t$ is

$$x_{k+1}(t) = J_{tA}\big(x_k - tB(x_k) - \lambda_{k-1}(B(x_k) - B(x_{k-1}))\big).$$

Algorithm 1 starts from arbitrary $x_0, x_{-1} \in H$ and $\lambda_{-1} > 0$. In each iteration it chooses $\rho \in \{1, \sigma^{-1}\}$, sets $\lambda_k = \rho\lambda_{k-1}\sigma^i$ with $i$ the smallest nonnegative integer for which

$$\lambda_k \|B(x_{k+1}) - B(x_k)\| \le \frac{\delta}{2}\|x_{k+1} - x_k\|, \qquad x_{k+1} = x_{k+1}(\lambda_k). \tag{30}$$

The choice of $\rho$ may change from one iteration to the next; $\rho = \sigma^{-1}$ allows the step to grow.

Formalization targets

Goal: Theorem 3.4

If $A$ is maximally monotone, $B$ is monotone and locally Lipschitz, and $(A+B)^{-1}(0) \ne \emptyset$, then every sequence generated by Algorithm 1 satisfies

$$\exists\, \bar x \in (A+B)^{-1}(0): \qquad x_k \to \bar x .$$

The statement fixes no constant: it holds for every $\delta, \sigma \in (0,1)$, every $\lambda_{-1} > 0$, every initial pair and every sequence of choices of $\rho$.

Milestones

1. Lemma 3.2 (any real Hilbert space, $B$ only locally Lipschitz): at any iteration state, some $i$ satisfies (30), so the linesearch terminates.
2. Lemma 3.3: for a zero $x$ there is $\varepsilon > 0$ with

$$\|x_{k+1}-x\|^2+2\lambda_k\langle B(x_{k+1})-B(x_k),x-x_{k+1}\rangle+\big(\tfrac12+\varepsilon\big)\|x_{k+1}-x_k\|^2 \le \|x_k-x\|^2+2\lambda_{k-1}\langle B(x_k)-B(x_{k-1}),x-x_k\rangle+\tfrac12\|x_k-x_{k-1}\|^2,$$

stated for $k \ge 1$ (see Formalization scope). 3. The iterates are bounded and $\|x_k - x_{k+1}\| \to 0$. 4. (33): there is $L > 0$ with $\|B(x_{k+1}) - B(x_k)\| \le L\|x_{k+1} - x_k\|$ for all $k$. 5. The step sizes $(\lambda_k)$ are bounded away from zero.

Significance

The theorem makes the forward-reflected-backward method usable without any knowledge of a Lipschitz constant, and extends it to operators that are only locally Lipschitz, such as gradients of $C^1$ functions without globally Lipschitz gradient or saddle operators of smooth non-quadratic convex-concave functions. The linesearch costs one resolvent and one evaluation of $B$ per trial, and the adaptive factor $\rho = \sigma^{-1}$ lets the steps recover after a conservative phase. The same template (an energy inequality where the linesearch test stands in for the Lipschitz bound, followed by a lower bound on the step sizes) recurs in adaptive and backtracking variants of many first-order methods.

The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal account of Algorithm 1 including the minimality of the backtracking index, which is where informal accounts of linesearch methods tend to be imprecise. It also records one correction: Lemma 3.3 as printed asserts (32) for all $k \in \mathbb N$, but at $k = 0$ the bound concerns initial data that Algorithm 1 never tests, and it fails there. Theorem 3.4 is unaffected.

Difficulty

Two steps do not transfer directly from the constant-step analysis. First, termination of the linesearch requires the limit behaviour of resolvents as the step tends to zero ($J_{tA}(y) \to P_{\overline{\mathrm{dom}\,A}}(y)$, Bauschke–Combettes, Theorem 23.47), combined with continuity of $B$ at the current point; local Lipschitz continuity enters only here and in the last step. Second, the step sizes must be bounded below. The obvious argument combines the accepted test (30) with the Lipschitz bound (33) along the iterates, but (33) concerns accepted points, while a rejected trial step concerns a trial point that is not an iterate. One must show that the rejected trial points also stay in a fixed bounded set, on which $B$ is Lipschitz. Finite dimensionality is used exactly to pass from local Lipschitz continuity to Lipschitz continuity on bounded sets.

Formalization scope

$H$ is a type with [NormedAddCommGroup H] [InnerProductSpace ℝ H] [FiniteDimensional ℝ H]; it is never specialised to EuclideanSpace ℝ (Fin n). The operator vocabulary (monotone, maximally monotone, resolvent) is the published module ThreeOpSplitting.Accel.MonotoneOperators; local Lipschitz continuity is Mathlib's LocallyLipschitz. Conventions committed to:

• Resolvent as hypothesis. The resolvent is a family J : ℝ → H → H with IsResolventFamily A J; for maximally monotone $A$ it exists (Minty) and is unique on $t > 0$. The goal keeps maximal monotonicity of $A$ as well.
• Index shift. Lean's x j is $x_{j-1}$ and lam j is $\lambda_{j-1}$, so lam 0 $=\lambda_{-1}$. Algorithm 1's initialization also names a $\lambda_0$ that the iteration never uses; it is not a parameter.
• Run predicate. IsLinesearchRun J B δ σ lam x requires at every iteration some $\rho \in \{1, \sigma^{-1}\}$ and an index $i$ such that $\lambda_k = \rho\lambda_{k-1}\sigma^i$, $x_{k+1}$ is the trial point at $\lambda_k$, (30) holds, and (30) fails at every smaller index. Every sequence of $\rho$ choices is admitted.
• Mode of convergence. Norm convergence, Filter.Tendsto x atTop (nhds xs).
• Lemma 3.3 for $k \ge 1$. A disclosed correction of the printed "for all $k \in \mathbb N$".
• Hypothesis relaxations in milestones. Lemma 3.3 uses only monotonicity of $A$ and no completeness; the boundedness milestone drops finite dimensionality. Both are stronger than the page.

Trivializing encodings are ruled out: the resolvent is tied to $A$ by IsResolventFamily rather than left free; the minimality clause prevents arbitrarily small accepted steps; $\rho$ is not fixed; convergence is in norm, not weak; and a global Lipschitz hypothesis on $B$, which would reduce the goal to mission 1 of this series in finite dimension, is not assumed. The hypotheses are satisfiable (a sanity file checks $A \equiv \{0\}$, $J = \mathrm{id}$, $B = 0$).

A complete development needs: nonexpansiveness and continuity in the step of resolvents of maximally monotone operators, including the small-step limit to the projection onto $\overline{\mathrm{dom}\,A}$; Lipschitz continuity on compact sets of locally Lipschitz maps; the telescoping argument of Theorem 2.5; and a finite-dimensional closedness argument for the graph of $A + B$. The resolvent facts are reusable well beyond this mission. Proofs of individual milestones, and of the resolvent lemmas as separate items, are welcome.

Selected references

• Y. Malitsky, M. K. Tam, A Forward-Backward Splitting Method for Monotone Inclusions Without Cocoercivity, SIAM J. Optim. 30(2):1451–1472, 2020. arXiv:1808.04162v4, doi:10.1137/18M1207260
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. doi:10.1007/978-3-319-48311-5
• P. Tseng, A modified forward-backward splitting method for maximal monotone mappings, SIAM J. Control Optim. 38(2):431–446, 2000. doi:10.1137/S0363012998338806

Motivation

Strategic open pit mine planning decides which parts of an ore body are excavated, in which period, and where each block of material is sent: to a processing plant, a stockpile or a waste dump. Rivera Letelier, Espinoza, Goycoolea, Moreno and Muñoz (Operations Research 68(5), 2020) state the problem as a mixed-integer program, the precedence-constrained production scheduling problem with clusters (PCPSP-C), which extends the formulation of Bienstock and Zuckerberg (IPCO 2010) to clusters of blocks that are extracted together. The integer versions of this program have large integrality gaps on production scheduling instances (§5, p. 1432), so the authors derive problem-specific cutting planes. This mission concerns the variable-right-hand-side (VRHS) production cuts of §5.2. They combine the precedence order of the clusters with the capacity of a single destination: if a solution sends many blocks to a capacitated destination, the predecessors of those blocks must be fully extracted.

The VRHS cuts are introduced first on a one-period, two-destination set, the mode-knapsack set MK (§5.2.1), and then generalised to the full multi-period clustered model (§5.2.2). Disaggregated formulations with destination choices go back to Boland et al. (Comput. Oper. Res. 2009); cutting planes for the precedence-constrained knapsack structure of open pit scheduling were studied by Bley et al. (Comput. Oper. Res. 2010).

All page references are journal pages of the published Operations Research article.

Setting

An instance has finite sets $\mathcal B$ of blocks, $\mathcal D$ of destinations and $\mathcal C$ of clusters, the latter a partition of $\mathcal B$, and periods $\mathcal T=\{1,\dots,T\}$. Block $b$ lies in cluster $c(b)$ and has weight $q_b\ge 0$. A precedence relation $b_1\prec b_2$ on blocks induces one on clusters ($c_1\prec c_2$ if some block of $c_1$ precedes some block of $c_2$), assumed to be a strict partial order. The arc set $\mathcal A$ is its transitive reduction: $(c,c')\in\mathcal A$ when $c'$ is an immediate predecessor of $c$. The reverse closure of a cluster is $rcl(c)=\{c\}\cup\{c':c\prec c'\}$, the cluster and everything that requires it; for a set $S$ of clusters, $q(S)=\sum_{c\in S}\sum_{b\in c}q_b$.

Variables $x_{c,t}$ give the fraction of cluster $c$ extracted in period $t$, and $y_{b,d,t}$ the fraction of block $b$ sent to destination $d$ in period $t$. The constraints (2)–(7) of p. 1427 are

$$x_{c(b),t}=\sum_{d}y_{b,d,t},\qquad \sum_{t}x_{c,t}\le 1,\qquad \sum_{t'\le t}x_{c,t'}\le\sum_{t'\le t}x_{c',t'}\ \ ((c,c')\in\mathcal A),\qquad Gy\le g,\qquad y\ge 0,$$

together with an integrality condition: full integrality (10), $x_{c,t}\in\{0,1\}$, defines the PCPSP-F, and partial integrality (11), "$\sum_{t'\le t}x_{c,t'}>0$ implies $\sum_{t'\le t}x_{c',t'}=1$ for $(c,c')\in\mathcal A$", defines the PCPSP-P. The general rows $Gy\le g$ include the destination capacity rows (9), $\sum_b q_b\,y_{b,d,t}\le U^d_t$. The cuts use the cumulative variables $w_{c,t}=\sum_{t'=1}^{t}x_{c,t'}$ (17).

The mode-knapsack set MK (p. 1433) fixes a DAG $G=(\mathcal B,\mathcal A)$, weights $q_b>0$ and a capacity $U>0$, and consists of the vectors $(x,y^P,y^W)$ with

$$\sum_b q_b y^P_b\le U,\qquad y^P_b+y^W_b=x_b,\qquad x_b\le 1,\qquad x_b>0\Rightarrow x_{b'}=1\ ((b,b')\in\mathcal A),\qquad y^P,y^W\ge 0.$$

Formalization targets

Goal: Theorem 7 (VRHS cuts), p. 1434

Fix $d\in\mathcal D$, $t\in\mathcal T$ and clusters $c_1\prec c_2\prec\dots\prec c_n$ with $q(rcl(c_1)\setminus rcl(c_n))<U^d_t<q(rcl(c_1))$. Let $\Delta_k=rcl(c_k)\setminus rcl(c_{k+1})$, $\delta_k=q(\Delta_k)$ for $k<n$, and $\Delta_n=rcl(c_n)$, $\delta_n=U^d_t-q(rcl(c_1)\setminus rcl(c_n))$. For constants $0\le\alpha_b\le 1$ ($b\in c_n$), the inequality

$$\sum_{k=1}^{n-1}\sum_{c\in\Delta_k}\sum_{b\in c}q_b y_{b,d,t}+\sum_{b\in c_n}\alpha_b q_b y_{b,d,t}+\sum_{c\in rcl(c_n)\setminus\{c_n\}}\sum_{b\in c}q_b y_{b,d,t}\le\sum_{k=1}^{n}\delta_k w_{c_k,t}\tag{32}$$

is valid for the PCPSP-F, and, when $\sum_{b\in c_n}\alpha_b q_b\le U^d_t-q(rcl(c_1)\setminus rcl(c_n))$ (33), for the PCPSP-P. The goal is the conjunction of the two validity claims.

Milestones

• (29)–(30), p. 1434: under either integrality condition, $w_{c,t}<1$ implies $y_{b,d,t}=0$ for every block of a cluster in $rcl(c)\setminus\{c\}$, and $y_{b,d,t}\le w_{c(b),t}$. The third condition (31) of the page is the capacity row (9) itself.
• (35), p. 1435: $\sum_{c\in\Delta_k}\sum_{b\in c}q_b y_{b,d,t}\le\delta_k w_{c_k,t}$ for $k=1,\dots,n-1$.
• (36), p. 1435: under (33), $\sum_{b\in c_n}\alpha_b q_b y_{b,d,t}\le\delta_n w_{c_n,t}$.
• Theorem 5, p. 1434: in MK, every block $b$ with $q_b\le U$ gives the valid inequality $\sum_{b'\in rcl(b)}q_{b'}y^P_{b'}\le U x_b$.

Significance

A valid inequality removes fractional points of the linear relaxation while keeping every feasible schedule. The VRHS cuts are among the production cuts that the paper evaluates in its computational study (§8), alongside the extraction cuts and the hourglass cuts. Their right-hand side is not a constant but a combination of extraction variables along a chain, which is what lets them couple the destination capacity with the precedence order; the paper's Theorem 5 shows the mechanism on MK, Theorem 7 in the full model. The partial integrality regime, under which the second half of Theorem 7 holds, is the one used by commercial mine planning software (p. 1427).

The results are proved in the paper by case analysis on the first index $k$ with $w_{c_k,t}<1$. None of them has a machine-checked proof. Formalizing them makes explicit which rows of the formulation each cut uses (the destination capacity (9) and the integrality condition), and what role the coefficient condition (33) plays in the partially integral case.

Difficulty

The proof uses that $\Delta_1,\dots,\Delta_{n-1}$ partition $rcl(c_1)\setminus rcl(c_n)$ and are disjoint from $rcl(c_n)$, which requires $rcl(c_{k+1})\subseteq rcl(c_k)$ along the chain. It uses that $w_{c,t}\le w_{c_k,t}$ for every $c\in rcl(c_k)$, and that $w_{c,t}<1$ forces all strict successors of $c$ to be unextracted; both chain the constraints (4) and (11) along covering arcs of a finite strict order, since the formulation constrains only the arcs of $\mathcal A$, not all of $\prec$. A natural first attempt, arguing directly from $\prec$, therefore does not apply. The counting step needs $x\ge 0$, which is not a constraint of the formulation but follows from $x_{c(b),t}=\sum_d y_{b,d,t}$, $y\ge 0$ and the nonemptiness of clusters. In the partial integrality case a fractional $w_{c_n,t}$ is possible, and the bound on the $c_n$ term must come from (33) rather than from integrality.

Formalization scope

Blocks, destinations and clusters are finite types; periods are Fin T, index $t$ standing for period $t+1$. An instance carries the block-to-cluster map, the block precedence, values, discount rate, weights, capacities and $m$ side rows $Gy\le g$. Cluster precedence is derived from block precedence; $\mathcal A$ is its covering relation, and constraints (4) and (11) range over $\mathcal A$ only. The chain $c_1,\dots,c_n$ is a function on $\mathbb N$ read at $1,\dots,n$ with $n\ge 1$, and condition 1 of Theorem 7 is stated for consecutive pairs. In (32), $y$ is taken at the single period $t$ and $w$ is cumulative.

The standing assumptions of §2.1 are hypotheses of every PCPSP-C statement: clusters cover $\mathcal B$ (so each is nonempty), $\prec$ is a strict partial order on clusters, $r>0$, and $q_b\ge 0$. A cut "valid for the PCPSP-F (PCPSP-P)" is stated as: at every point feasible for the formulation with full (partial) integrality whose destination capacity rows (9) hold, the inequality holds. The capacity rows enter as an explicit hypothesis because the paper assumes they are among the rows of $Gy\le g$; without them the cut is false. Validity is never asserted for the LP relaxation, where (29) and (32) fail, so the integrality condition cannot be dropped. Conditions 2 and 3 of Theorem 7 are kept as on the page, although the proof does not use condition 3. In MK, the DAG property, $q>0$ and $U>0$ are hypotheses; an arc $(b,b')$ means that extracting $b$ forces $b'$, and $rcl(b)$ collects $b$ and the blocks from which $b$ is reachable.

The development needs only finite sums, finite sets and orders from Mathlib. Contributions are welcome on the chaining lemma for covering relations of finite strict orders, on the nonnegativity and monotonicity of $w$, and on the partition $\{\Delta_k\}$ of $rcl(c_1)\setminus rcl(c_n)$, which the goal and the milestones share.

Selected references

• O. Rivera Letelier, D. Espinoza, M. Goycoolea, E. Moreno, G. Muñoz, Production Scheduling for Strategic Open Pit Mine Planning: A Mixed-Integer Programming Approach, Operations Research 68(5):1425–1444, 2020. https://doi.org/10.1287/opre.2019.1965
• D. Bienstock, M. Zuckerberg, Solving LP Relaxations of Large-Scale Precedence Constrained Problems, Proc. 14th IPCO, LNCS 6080, 1–14, 2010. https://doi.org/10.1007/978-3-642-13036-6_1
• N. Boland, I. Dumitrescu, G. Froyland, A. M. Gleixner, LP-based disaggregation approaches to solving the open pit mining production scheduling problem with block processing selectivity, Computers & Operations Research 36(4):1064–1089, 2009. https://doi.org/10.1016/j.cor.2007.12.006
• A. Bley, N. Boland, C. Fricke, G. Froyland, A strengthened formulation and cutting planes for the open pit mine production scheduling problem, Computers & Operations Research 37(9):1641–1647, 2010. https://doi.org/10.1016/j.cor.2009.12.008