All missions

Motivation

The Hartree-Fock method approximates the ground state of an interacting many-electron system by the best single Slater determinant. It is the starting point of essentially all of quantum chemistry and of mean-field theories in condensed-matter physics: post-Hartree-Fock methods (configuration interaction, coupled cluster, perturbation theory) expand around it, and its orbital energies are the standard first estimate of ionization and excitation energies. E. Koch's lecture notes Mean-Field Theory: Hartree-Fock and BCS (Jülich Autumn School on Correlated Electrons, 2016) derive the method entirely within second quantization: Slater determinants are products of creation operators acting on a vacuum, variations are generated by one-body unitaries $e^{i\lambda\hat M}$, and the stationarity condition becomes an algebraic statement about matrix elements. The central result of the Hartree-Fock section is the Brillouin theorem: a Slater determinant is stationary exactly when the Hamiltonian does not couple it to its single excitations.

Timeline of the ideas involved: Hartree introduces the self-consistent field (1928); Fock and Slater add exchange through antisymmetrized wave functions (1930); Koopmans relates orbital energies to ionization energies (1934); Brillouin formulates the single-excitation condition (1934); Thouless gives the representation of Slater determinants by exponentials of one-body operators (1960).

Setting

Fix $K$ orthonormal reference orbitals $\phi_0,\dots,\phi_{K-1}$; an orbital is a coefficient vector $\varphi\in\mathbb C^K$ with $\langle\varphi|\chi\rangle=\sum_\mu\overline{\varphi_\mu}\chi_\mu$. The Fock space has orthonormal basis $|S\rangle$, $S\subseteq\{0,\dots,K-1\}$ (the set of occupied orbitals). The creation operator $c^\dagger_i$ maps $|S\rangle$ to $(-1)^{\#\{j\in S:\,j>i\}}|S\cup\{i\}\rangle$ if $i\notin S$ and to $0$ otherwise; the annihilation operator $c_i$ is its adjoint, and for a general orbital $c^\dagger_\varphi=\sum_\mu\varphi_\mu c^\dagger_\mu$. The vacuum is $|0\rangle=|\emptyset\rangle$.

The Slater determinant of orbitals $\alpha_1,\dots,\alpha_N$ is $|\Phi\rangle=c^\dagger_{\alpha_N}\cdots c^\dagger_{\alpha_1}|0\rangle$. A one-body operator with matrix $M$ is $\hat M=\sum_{\alpha\beta}M_{\alpha\beta}c^\dagger_\alpha c_\beta$. For a hermitian $M$ the operators $e^{i\lambda\hat M}$ map Slater determinants to Slater determinants, and the energy functional along such a variation is

$$E_M(\lambda)=\langle\Phi|e^{i\lambda\hat M}\,\hat H\,e^{-i\lambda\hat M}|\Phi\rangle .$$

For the concrete Hamiltonian of Sec. 3.2,

$$\hat H=\sum_{n,m}c^\dagger_nT_{nm}c_m+\sum_{n>n',\,m>m'}c^\dagger_nc^\dagger_{n'}\bigl(U_{nn',mm'}-U_{nn',m'm}\bigr)c_{m'}c_m,$$

the Fock matrix of the determinant with occupied reference orbitals $S$ is $F_{nm}=T_{nm}+\sum_{m'\in S}(U_{nm',mm'}-U_{nm',m'm})$, with diagonal entries the orbital energies $\varepsilon_m$.

Formalization targets

Goal: the Brillouin theorem (Eqs. (62)–(63))

For a hermitian $\hat H$ and orthonormal $\alpha_1,\dots,\alpha_N$,

$$\Bigl(\forall M=M^\dagger:\ E_M'(0)=0\Bigr)\iff\Bigl(\forall\,\varphi_o\in\operatorname{span}\{\alpha_n\},\ \varphi_v\perp\{\alpha_n\}:\ \langle\Phi|c^\dagger_{\varphi_o}c_{\varphi_v}\hat H|\Phi\rangle=0\Bigr).$$

It asserts no specific Hamiltonian, no particle number and no basis choice; it is the basis-independent form of the source's condition (63).

Milestones

The milestone list follows the source's own steps: the anticommutation relations (15); the overlap formula (7)/(46); the action of $c_\varphi$, $c^\dagger_\varphi$ on a determinant (42); the one-body density matrix (43) and Wick's theorem (45); the transformation of vacuum and creators under $e^{i\lambda\hat M}$ (57), (59); the first-order variation (61)–(62). For the two-body Hamiltonian it adds the Fock-matrix form of the Brillouin condition (64), the Hartree-Fock energy, Koopmans' theorem (66) and the electron-hole excitation energy (67).

Significance

The Brillouin theorem turns the nonlinear variational problem over all Slater determinants into a condition on finitely many matrix elements; for a two-body Hamiltonian it says that the occupied–virtual block of the Fock matrix vanishes, which is the self-consistency condition solved by every Hartree-Fock code. Koopmans' theorem and the particle-hole formula give the physical interpretation of the orbital energies.

All results are classical and proved in the source and in standard textbooks. What this mission adds is a machine-checked account of second quantization on a finite orbital basis: the anticommutation relations, determinant overlaps and Wick's theorem for Slater determinants are reusable for any later formalization of configuration interaction, coupled cluster or BCS theory.

Difficulty

The source's arguments are short manipulations of operator identities, but each hides bookkeeping that is easy to get wrong: fermionic signs when operators are reordered, the identification of Slater determinants with ordered products of creators, and the Laplace expansion behind Wick's theorem. The variational step requires differentiating a matrix exponential on Fock space and identifying the derivative with a commutator. The direction from the Brillouin condition back to stationarity needs the hermiticity of $\hat H$ and a decomposition of an arbitrary hermitian $M$ into occupied–occupied, virtual–virtual and occupied–virtual blocks; the first two blocks act on $|\Phi\rangle$ only by a scalar. The Fock-matrix milestones additionally need the exchange symmetry $U_{nn',mm'}=U_{n'n,m'm}$ of two-body matrix elements stated in Sec. 2.3.2; without it the stated formulas fail.

Formalization scope

Fock space over $K$ orbitals is represented concretely: vectors are functions on Finset (Fin K) and operators are complex matrices indexed by Finset (Fin K). Creators carry the sign $(-1)^{\#\{j\in S:\,j>i\}}$, so ordered products of creators of increasing orbitals give $+|S\rangle$. All quantities are complex; the exponential is NormedSpace.exp; stationarity is HasDerivAt … 0 0 for a function $\mathbb R\to\mathbb C$. Orthonormality of the occupied orbitals is an explicit hypothesis wherever the source assumes it. The source works with a possibly infinite orbital basis; here the basis is finite, as in the variational setting of its Sec. 3.

The equivalence in the goal cannot be satisfied vacuously: hermiticity of $\hat H$ and orthonormality of the orbitals are both satisfiable, and both sides quantify over all admissible $M$, respectively all occupied and virtual orbitals.

Two printed formulas are not taken verbatim: Eq. (60) lacks the minus sign in the exponent and is omitted, and Eq. (61) prints the first-order commutator in the opposite order; the milestone records the correct derivative $i\langle\Phi|[\hat M,\hat H]|\Phi\rangle$, which leaves (62) unchanged.

Contributions welcome: a general API for products of creation and annihilation operators in this model (sign lemmas, normal ordering), which all milestones share.

Selected references

• E. Koch, Mean-Field Theory: Hartree-Fock and BCS, in E. Pavarini, E. Koch, J. van den Brink, G. Sawatzky (eds.), Quantum Materials: Experiments and Theory, Modeling and Simulation Vol. 6, Forschungszentrum Jülich, 2016. http://www.cond-mat.de/events/correl16
• A. Szabo and N. S. Ostlund, Modern Quantum Chemistry: Introduction to Advanced Electronic Structure Theory, Dover, 1996.
• T. Koopmans, Über die Zuordnung von Wellenfunktionen und Eigenwerten zu den einzelnen Elektronen eines Atoms, Physica 1 (1934) 104–113.

Motivation

The zeroth law of thermodynamics is the principle that makes temperature a meaningful notion. In the formulation of Fowler and Guggenheim, and in the standard textbooks of Guggenheim, Buchdahl and Bailyn, it states: if two systems are both in thermal equilibrium with a third system, then they are in thermal equilibrium with each other. It was named by R. H. Fowler in the 1930s, after the first, second and third laws were already established, because it is logically prior to them: it is what justifies the use of thermometers and the assignment of a single "temperature" to each equilibrated system.

Mathematically, the content of the law is a statement about a binary relation. Together with the convention that each system is in equilibrium with itself, it turns thermal equilibrium into an equivalence relation, and an equivalence relation is exactly what is needed to "tag" every system with a label (an empirical temperature) so that two systems are in equilibrium precisely when their labels agree. This mission formalizes that chain of reasoning as presented in the Wikipedia article Zeroth law of thermodynamics.

Setting

Let $S$ be a set (a type) whose elements are thermodynamic systems, each in its own state of internal equilibrium, and let $\mathrm{TE}$ be a binary relation on $S$; $\mathrm{TE}(A,B)$ reads "$A$ is in thermal equilibrium with $B$". No further structure is assumed.

• The zeroth law (right-Euclidean form) is the property

$$\forall A,B,C\in S,\quad \mathrm{TE}(A,C)\ \wedge\ \mathrm{TE}(B,C)\ \Longrightarrow\ \mathrm{TE}(A,B).$$

• Planck's form (left-Euclidean form) is the property

$$\forall A,B,C\in S,\quad \mathrm{TE}(C,A)\ \wedge\ \mathrm{TE}(C,B)\ \Longrightarrow\ \mathrm{TE}(A,B).$$

• Reflexivity is the convention $\mathrm{TE}(A,A)$ for all $A$.
• A map $t : S\to T$ into any set $T$ is an empirical temperature for $\mathrm{TE}$ if

$$\forall A,B\in S,\quad \mathrm{TE}(A,B)\iff t(A)=t(B).$$

Formalization targets

Goal: existence of temperature

$$\Big(\forall A,\ \mathrm{TE}(A,A)\Big)\ \wedge\ \text{zeroth law} \ \Longrightarrow\ \exists\,T,\ \exists\, t:S\to T,\ t \text{ is an empirical temperature for } \mathrm{TE}.$$

This is the "existence of temperature" postulate of Fowler and Guggenheim: the condition for thermal equilibrium is equality of a single-valued function of the state. The labelling set $T$ is left arbitrary, as in the source ("the labeling may be quite arbitrary").

Milestones

1. Reflexivity + zeroth law $\Rightarrow$ $\mathrm{TE}$ is an equivalence relation.
2. Reflexivity + Planck's form $\Rightarrow$ $\mathrm{TE}$ is an equivalence relation.
3. Under reflexivity, the zeroth law and Planck's form are equivalent.
4. Consequence: symmetry of thermal equilibrium.
5. Consequence: transitivity of thermal equilibrium.
6. A reflexive, transitive relation need not be an equivalence relation.
7. An equivalence relation partitions the systems into classes of mutual equilibrium.
8. An equivalence relation admits an empirical-temperature tagging.

Significance

The result is the logical foundation of thermometry: it is what allows any one system to serve as a thermometer for all others, and it underlies every empirical temperature scale and, via the second law, the absolute scale. The statements here are elementary and are known; the value of the mission is a clean, reusable formal vocabulary for thermal equilibrium (the two Euclidean forms of the law and the notion of an empirical temperature) on which formalizations of later parts of axiomatic thermodynamics can build.

Difficulty

None of the steps is deep. The point that needs care is that the zeroth law alone does not give an equivalence relation: reflexivity is an additional convention, and the source stresses that a reflexive and transitive relation is not automatically symmetric. Each milestone therefore states its reflexivity hypothesis explicitly.

Formalization scope

Systems form an arbitrary type S (possibly empty), and thermal equilibrium is an arbitrary relation TE : S → S → Prop. Equivalence relations are Lean's Equivalence; partitions use Mathlib's Setoid.IsPartition. The labelling type of an empirical temperature lives in the same universe as S. The richer structure of real-valued temperature (ordering into "hotter" and "colder", continuity) is explicitly not part of the zeroth law according to the source and is out of scope. Definitions ZerothLaw, ZerothLawPlanck, IsEmpiricalTemperature are shared by all statements, in the namespace ZerothLawThermo.

Selected references

• Wikipedia contributors, Zeroth law of thermodynamics, revision 1328026962. https://en.wikipedia.org/w/index.php?title=Zeroth_law_of_thermodynamics&oldid=1328026962
• R. Fowler, E. A. Guggenheim, Statistical Thermodynamics, Cambridge University Press, 1939 (corrected 1965), p. 56.
• E. H. Lieb, J. Yngvason, The physics and mathematics of the second law of thermodynamics, Physics Reports 310 (1999) 1–96. https://arxiv.org/abs/cond-mat/9708200

Motivation

The conservation of momentum, of mechanical energy and of mass are the three bookkeeping laws on which elementary Newtonian mechanics and continuum mechanics rest. In Newtonian mechanics each of them is not an extra postulate but a theorem: momentum conservation follows from Newton's second and third laws, conservation of mechanical energy follows from Newton's second law when the forces are derived from a potential, and conservation of total mass in a fluid follows from the continuity equation. This mission asks for machine-checked proofs of these classical derivations, in the form in which they appear in the encyclopedia articles Momentum, Conservation of energy and Conservation of mass.

Historically, Huygens (1669) listed both the total momentum and the total vis viva $\sum_i m_i v_i^2$ as invariants of collisions; Leibniz (1676–1689) promoted the vis viva; the distinction between elastic and inelastic collisions and the general principle of energy conservation were clarified only in the 19th century. Lomonosov (1756) and Lavoisier (1773) established conservation of mass in chemical reactions; its continuum form is the continuity equation of fluid dynamics.

Setting

All motion takes place in Euclidean space $\mathbb{R}^d$ (any dimension $d$; $d = 3$ is the physical case), with the standard inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$.

• A system of $N$ particles has masses $m_i > 0$, positions $x_i(t)$, velocities $v_i(t) = \dot x_i(t)$ and accelerations $a_i(t) = \dot v_i(t)$, for $i = 1,\dots,N$ and all times $t \in \mathbb{R}$.
• Newton's second law: $m_i a_i(t)$ equals the net force on particle $i$.
• Newton's third law for internal forces: the force $F_{ij}$ exerted on $i$ by $j$ satisfies $F_{ij} = -F_{ji}$.
• The total momentum is $P(t) = \sum_i m_i v_i(t)$, the centre of mass is $R(t) = M^{-1}\sum_i m_i x_i(t)$ with $M = \sum_i m_i$, the kinetic energy is $\sum_i \tfrac12 m_i \|v_i\|^2$.
• A pair potential is a function $\varphi_{ij} = \varphi_{ji}$ of the distance $r_{ij} = \|x_i - x_j\|$; the force it produces on $i$ is $-\varphi_{ij}'(r_{ij})\,(x_i - x_j)/r_{ij}$ (e.g. gravity, $\varphi_{ij}(r) = -G m_i m_j / r$).
• A fluid has density $\rho(t,x)$ and velocity field $u(t,x)$; the continuity equation is $\partial_t \rho + \nabla\cdot(\rho u) = 0$, and the total mass is $\int_{\mathbb{R}^n} \rho(t,x)\,dx$.

Target

The goal theorem is the conservation of both total momentum and total mechanical energy for an isolated $N$-body system interacting through symmetric pair potentials, along any collision-free trajectory:

$$P(t) = P(s), \qquad \sum_i \tfrac12 m_i\|v_i(t)\|^2 + \sum_{i<j}\varphi_{ij}\big(\|x_i(t)-x_j(t)\|\big) = \text{the same expression at } s.$$

Milestones:

1. Conservation of momentum under Newton's third law (any internal forces).
2. Uniform rectilinear motion of the centre of mass, with velocity $P/M$.
3. Conservation of mechanical energy for a particle in a conservative force field $F = -\nabla V$.
4. The work–energy theorem: change in kinetic energy equals the work $\int \langle F, v\rangle\,dt$.
5. Head-on elastic collision of two bodies: the final velocities are either the initial ones or the classical formulas.
6. Perfectly inelastic collision: common final velocity and the kinetic energy lost, $\tfrac12\frac{m_A m_B}{m_A+m_B}(u_A-u_B)^2$.
7. Conservation of total mass for a compactly supported $C^1$ solution of the continuity equation.

Significance

These are the textbook consequences of Newton's laws used throughout mechanics, astronomy and engineering: momentum conservation determines the outcome of collisions and explosions, energy conservation gives first integrals that reduce equations of motion, and mass conservation is the first of the Euler equations of fluid dynamics. The results themselves are classical and fully known; the work in this mission is formalization. The platform already contains specialised instances (for example a two-body centre-of-mass statement and energy conservation in the Kepler problem); this mission states the general $N$-body, arbitrary-dimension versions and the continuum mass law, which can be reused by later mechanics missions.

Difficulty

The algebraic milestones (collisions) are elementary. The analytic ones require care: energy conservation needs the chain rule for $V \circ x$ and for the norm $\|x_i - x_j\|$, which is differentiable only away from collisions; the work–energy theorem needs the fundamental theorem of calculus for a continuous integrand; mass conservation needs differentiation under the integral sign and the vanishing of the integral of the divergence of a compactly supported $C^1$ vector field, a form of the divergence theorem that must be assembled from one-dimensional integration by parts.

Formalization scope

• Space is EuclideanSpace ℝ (Fin d); time is ℝ; trajectories are defined for all times, and derivatives are given explicitly through HasDerivAt hypotheses ($\dot x_i = v_i$, $\dot v_i = a_i$) rather than through deriv.
• Masses are strictly positive. The $N$-body goal assumes that no two particles ever coincide (collision-free trajectory), so that the pair forces are defined; pair potentials are only required to be differentiable on $(0,\infty)$.
• No definitions are introduced; every quantity is written out explicitly in each statement.
• In milestone 5 the trivial outcome (velocities unchanged) is kept as an explicit alternative instead of being excluded by a hypothesis, so the statement is never vacuous.
• In milestone 7 the continuity equation is written with partial derivatives deriv / fderiv, the density and the velocity field are jointly $C^1$ in $(t,x)$, and the density vanishes outside a fixed ball for all times. The integral is the Lebesgue integral on $\mathbb{R}^n$.

Selected references

• Wikipedia, Momentum, sections "Many particles", "Conservation", "Application to collisions" — https://en.wikipedia.org/wiki/Momentum
• Wikipedia, Conservation of energy — https://en.wikipedia.org/wiki/Conservation_of_energy
• Wikipedia, Conservation of mass, section "Formulation and examples" — https://en.wikipedia.org/wiki/Conservation_of_mass

Motivation

Multistage stochastic programs model decisions taken over time while uncertain data are revealed: generation scheduling in hydro-thermal power systems, capacity expansion, unit commitment, portfolio management. When the uncertainty is represented by a finite scenario tree, the problem becomes one very large deterministic program, and decomposition algorithms solve it stage by stage. For linear problems the standard methods are nested Benders decomposition and its sampling variant, stochastic dual dynamic programming (SDDP), introduced by Pereira and Pinto (1991). Both rely on the convexity of the value functions, which they approximate from below by linear cuts.

Many applications need integer decisions (on/off status of generators, investment choices), and integer variables destroy convexity. Zou, Ahmed and Sun (Math. Program. 175 (2019) 461–502) observed that when the state variables passed between stages are binary, exact convex polyhedral representations still exist on the binary points. They proposed stochastic nested decomposition (SND) and its stage-wise independent special case SDDiP, and identified three properties of cuts (valid, tight, finite) under which the algorithms converge. This mission formalizes that convergence theorem, Theorem 2 of the paper.

Timeline. Birge (1985) gave nested decomposition for multistage linear programs; Pereira and Pinto (1991) introduced SDDP. Philpott and Guan (2008) proved almost sure finite convergence of SDDP-type methods for linear problems, and Girardeau, Leclère and Philpott (2015) extended convergence to convex problems. Zou, Ahmed and Sun (2019) proved finite convergence with probability one for mixed integer problems with binary states and abstract valid, tight and finite cuts, and showed that their Lagrangian cuts have the first two properties.

Setting

Let $\mathcal T$ be a scenario tree with stages $1,\dots,T$, root $1$, parent map $a(n)$ and children $\mathcal C(n)$. The nodes of the last stage are the scenarios. Node probabilities satisfy $p_n>0$, $p_1=1$, and $p_n=\sum_{m\in\mathcal C(n)}p_m$ before the last stage, and $q_{nm}=p_m/p_n$. Each node has a linear cost $f_n(x_n,y_n)$ and a nonempty compact mixed integer polyhedral set $X_n$ (assumption (A1)). The state $x_n\in\{0,1\}^d$ is binary, the local variables $y_n$ are general, and the root's parent state $\bar x_0$ is fixed. The problem in local-copy form (2.1) is

$$\min\sum_{n\in\mathcal T}p_nf_n(x_n,y_n)\quad\text{s.t.}\quad(z_n,x_n,y_n)\in X_n,\ z_n=x_{a(n)},\ x_n\in\{0,1\}^d .$$

Its value functions satisfy the recursion (2.3): $Q_n(x_{a(n)})=\min\{f_n(x_n,y_n)+\mathcal Q_n(x_n)\}$ over the nodal feasible set, with the expected cost-to-go function $\mathcal Q_n(x)=\sum_{m\in\mathcal C(n)}q_{nm}Q_m(x)$.

The SND algorithm keeps an under-approximation $\psi^i_n$ of each $\mathcal Q_n$: the maximum of a lower bound $L_n$ and the aggregated cuts $\sum_{m\in\mathcal C(n)}q_{nm}(v^\ell_m+(\pi^\ell_m)^\top x)$ collected so far (3.2). Each iteration $i$ samples $M$ scenarios with replacement. In the forward step it solves the nodal problems $P^i_n(x^i_{a(n)},\psi^i_n)$ from the root down, which yields the forward tree solution $\{(x^i_n,y^i_n)\}$ of (3.6). In the backward step, at every sampled node it generates one cut per child at the state $x^i_n$ and adds their aggregate to $\psi_n$. Cuts are valid if $Q_m(x)\ge v^i_m+(\pi^i_m)^\top x$ on $\{0,1\}^d$ (3.4). They are tight if they equal the value $\underline Q^i_m(x^i_n,\psi^{i+1}_m)$ of the child's updated nodal problem at $x^i_n$ (3.5). They are finite if only finitely many distinct cuts occur. Assumption (A3) requires the nodal solver to return the same optimal solution whenever it is given the same problem.

Formalization targets

Goal: Theorem 2 (p. 474)

With sampling with replacement, valid, tight and finite cuts, and a solver satisfying (A3), the following holds with probability one:

$$\exists\, i_0\ \ \forall i\ge i_0:\quad \{(x^i_n,y^i_n)\}_{n\in\mathcal T}\ \text{is an optimal solution of (2.1)}.$$

Milestones, in the order the proof uses them

1. Valid cuts give under-approximations, $\psi^i_n\le\mathcal Q_n$ and $\underline Q^i_n\le Q_n$ (proof of Claim 1, p. 475).
2. Claim 1: if $\psi^i_n(x^i_n)=\mathcal Q_n(x^i_n)$ for all $n$, the forward solution is optimal for (2.1) (p. 475).
3. With finitely many possible cuts, the approximations $\{\psi^i_n\}$ change only in finitely many iterations (pp. 474–475).
4. (3.8a)–(3.8f): a sampled node whose children are exact becomes exact after its backward step (p. 476).
5. Under sampling with replacement, every scenario is sampled in infinitely many iterations, almost surely (p. 476).
6. Claim 2: almost surely, no infinite block of unchanged approximations has a non-optimal forward solution (p. 475).

Significance

Theorem 2 separates the convergence of nested decomposition from the choice of cuts. Any cut family with the three properties yields an exact algorithm for multistage stochastic integer programs with binary states. The paper verifies the properties for integer optimality cuts and, through its Theorem 3, shows that Lagrangian cuts from the local-copy reformulation are valid and tight. The convergence of SDDiP, the variant used in computations, follows from the same theorem, and binary expansion of general integer states extends the reach to mixed integer state spaces.

The result is proved in the paper; no machine-checked proof exists. A formal development would turn its informal points into checked statements: that the minima are attained, that the DP recursion is equivalent to the extensive form, and that the finiteness of cuts is global. It would also supply a reusable framework (scenario trees with node probabilities, cut-based approximations, sampled runs) for the convergence theory of SDDP-type methods.

Difficulty

No single step is deep; the difficulty is the interaction of the pieces. A tempting argument says the approximations stop changing, so the algorithm stops at an optimum. But a stalled run need not be optimal: if a node at which $\psi_n$ is inexact is never sampled again, nothing changes and the forward solution stays suboptimal. The proof must therefore combine three things: the deterministic finiteness of changes, an almost sure statement about sampling, and the exactness chain (3.8). That chain depends on tightness with respect to the updated approximation of the child, and it fails if tightness refers to the approximation from before the backward step. The equivalence between optimality for the DP recursion and for the extensive form (2.1), used without proof in Claim 1, also requires a backward induction over the tree.

Formalization scope

The tree is the platform definition StochasticProg.Multistage.Tree H, with stage $t$ of the paper equal to stage = t − 1. Binary vectors are Fin d → Bool, embedded in $\mathbb R^d$. The copy variable $z_n$ is eliminated through $z_n=x_{a(n)}$. Minima are written as infima over sets that the standing assumptions make nonempty, bounded below and attained. Lean iterations are numbered from $0$, and the run is infinite (stopping criteria and bounds play no role).

Readings of informal words. "Optimal solution of (2.1)" means a feasible tree solution of least cost $\sum_np_nf_n$ among all feasible tree solutions. "After a finite number of iterations" means from some iteration on, in every iteration (∀ᶠ i in atTop). "With probability one" refers to a probability space carrying independent draws, $M\ge1$ per iteration, each with law $\{p_n:n\in S_T\}$. "Finite" cuts means one finite set for the whole run, as the proof uses it, not a different finite set per iteration. (A3) means the solver is a function of the node, the parent state and the approximation, and returns an optimal solution.

Added hypotheses, which the paper uses without stating them: $p_n>0$; every nodal problem is feasible for every binary parent state, which replaces (A2) (not used by Theorem 2); and the lower bounds under-estimate, $L_n\le\mathcal Q_n$, which is Algorithm 1's "initial under-approximation".

Trivializing formalizations are ruled out: tightness refers to the child's approximation after its own update, optimality is for the true extensive form and not relative to $\psi$, and the probability statement is over independent sampling, not over a fixed sample sequence assumed to visit every scenario.

Contributions welcome: the attainment lemmas for nodal minima, the DP/extensive-form equivalence on trees, and the second Borel–Cantelli argument for repeated sampling. All of these are reusable for other SDDP-type convergence results.

Selected references

• J. Zou, S. Ahmed, X. A. Sun, Stochastic dual dynamic integer programming, Math. Program. 175 (2019) 461–502. https://doi.org/10.1007/s10107-018-1249-5
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Math. Program. 52 (1991) 359–375. https://doi.org/10.1007/BF01582895
• A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Oper. Res. Lett. 36 (2008) 450–455. https://doi.org/10.1016/j.orl.2008.01.013
• P. Girardeau, V. Leclère, A. B. Philpott, On the convergence of decomposition methods for multistage stochastic convex programs, Math. Oper. Res. 40 (2015) 130–145. https://doi.org/10.1287/moor.2014.0664
• J. R. Birge, Decomposition and partitioning methods for multistage stochastic linear programs, Oper. Res. 33 (1985) 989–1007. https://doi.org/10.1287/opre.33.5.989

Motivation

Multistage stochastic integer programs model sequential decisions under uncertainty in which some decisions are discrete: unit commitment in power systems, capacity expansion, production planning with setups. Their linear (continuous) counterparts are routinely solved by nested decomposition methods such as stochastic dual dynamic programming (SDDP; Pereira and Pinto, 1991), which approximate each node's expected cost-to-go function from below by a maximum of linear cuts. With integer variables the cost-to-go functions are no longer convex, and cuts from linear programming duality are in general not exact at the points where they are generated.

Zou, Ahmed and Sun (Math. Program. 175 (2019) 461–502) restrict the state variables passed between stages to be binary and introduce a local copy $z_n$ of the parent's state at every node. Dualizing only the copy constraint $z_n = x_{a(n)}$ gives a class of cuts, the Lagrangian cuts, which the authors call "one of the major results of the paper" (p. 478). Their Theorem 3 shows that these cuts are valid (they never overestimate the true value function) and tight (they reproduce the current approximate value at the binary state where they are generated). Together with finiteness, these are the sufficient conditions of the paper's Definition 2 under which SND and SDDiP find an optimal solution in finitely many iterations with probability one (Theorem 2 of the paper, the subject of a companion mission).

Setting

Fix a node $n$ of the scenario tree and an iteration $i$ of the algorithm. The node has:

• a nodal constraint set $X_n \subseteq \mathbb R^d \times \mathbb R^d \times \mathbb R^\ell$ of triples $(z_n, x_n, y_n)$, where $x_n$ is the node's state, $y_n$ its local variables and $z_n$ the local copy of the parent's state. By assumption (A1) $X_n$ is nonempty, compact and mixed integer polyhedral: the points of a polyhedron $\{w : Aw \ge b\}$ with some coordinates integer;
• a linear objective $f_n(x_n, y_n) = c^\top x_n + e^\top y_n$;
• children $m \in \mathcal C(n)$ with conditional probabilities $q_{nm} \ge 0$, a lower bound $L_n$, and the children's cut coefficients $(v^\ell_m, \pi^\ell_m)$ for $\ell = 1, \dots, i$.

The approximate expected cost-to-go (3.2) is

$$\psi^{i+1}_n(x) = \min\Big\{\theta : \theta \ge L_n,\ \theta \ge \sum_{m} q_{nm}\big(v^\ell_m + (\pi^\ell_m)^\top x\big),\ \ell = 1,\dots,i\Big\},$$

and the updated forward problem (3.1) at a parent state $\hat x$ has value

$$\underline Q^i_n(\hat x, \psi^{i+1}_n) = \min\{ f_n(x,y) + \psi^{i+1}_n(x) : (z,x,y) \in X_n,\ z = \hat x,\ x \in \{0,1\}^d\}.$$

Let $X'_n = \{(z,x,y) \in X_n : x \in \{0,1\}^d,\ z \in [0,1]^d\}$ and let $X''_n$ add a variable $\theta \ge L_n$ that dominates every aggregated cut. The Lagrangian function and Lagrangian dual (4.3)–(4.4) are

$$\mathcal L^i_n(\pi) = \min_{(z,x,y,\theta)\in X''_n} f_n(x,y) + \theta - \pi^\top z, \qquad (R^i_n):\ \max_{\pi\in\mathbb R^d}\ \mathcal L^i_n(\pi) + \pi^\top \hat x .$$

An optimal $\hat\pi$ and $\hat v = \mathcal L^i_n(\hat\pi)$ define the Lagrangian cut $\theta \ge \hat v + \hat\pi^\top x_{a(n)}$. Given true value functions $Q_m$ of the children and $\mathcal Q_n = \sum_m q_{nm} Q_m$, the true nodal value (2.3) is $Q_n(x_a) = \min\{f_n(x,y) + \mathcal Q_n(x) : (z,x,y) \in X_n,\ z = x_a,\ x \in \{0,1\}^d\}$.

Formalization targets

Goal: Theorem 3 at one node

For binary $\hat x \in \{0,1\}^d$ and $\hat\pi$ optimal for $(R^i_n)$:

$$\hat v + \hat\pi^\top \hat x = \underline Q^i_n(\hat x, \psi^{i+1}_n) \qquad \text{(tightness, (3.5))},$$

and, if the children's cuts are valid for $Q_m$ on $\{0,1\}^d$ and $\mathcal Q_n \ge L_n$ there,

$$Q_n(x_a) \ge \hat v + \hat\pi^\top x_a \quad \text{for all } x_a \in \{0,1\}^d \qquad \text{(validity, (3.4))}.$$

The paper's statement for the whole collection of cuts of an iteration follows by applying this at every sampled node from the last stage backwards, exactly as its proof does by induction.

Milestones

1. (4.5): $\hat v + \hat\pi^\top\hat x = \min\{f_n + \theta : (z,x,y,\theta) \in \mathrm{conv}(X''_n),\ z = \hat x\}$, for any parent state at which $(R^i_n)$ has an optimal solution.
2. Binary face: for binary $\hat x$, $\mathrm{conv}(X''_n) \cap \{z = \hat x\} = \mathrm{conv}(X''_n \cap \{z = \hat x\})$.
3. Tightness (display after (4.5)).
4. Validity, base case: at a last-stage node, $Q_n(x_a) \ge \mathcal L^i_n(\pi) + \pi^\top x_a$.
5. Validity, induction step ((4.6) and the display after it).

Significance

Tightness at binary states is what separates Lagrangian cuts from the cuts of continuous relaxations or of a direct Lagrangian relaxation of the constraints coupling stages: the paper's Example 2 shows a direct relaxation whose cut is not tight even at a binary state, and Example 1 shows that with a non-binary state the duality gap is positive. With valid, tight and finite cuts, SND and SDDiP become exact algorithms for multistage stochastic integer programs with binary states, and through binarization they approximate problems with general mixed-integer states.

The result is proved in the paper; no machine-checked proof of it is known. Formalizing it requires a Lean statement of Geoffrion's theorem for this nodal problem (Lagrangian duality equals optimization over the convex hull of a mixed integer set), which is of independent use for integer programming, and the binary-face fact for sets inside the unit cube.

Difficulty

The validity half is weak duality and is short. The difficulty is in tightness. Step (4.5) is a strong duality statement for a nonconvex set: it needs that the convex hull of $X''_n$ is a polyhedron, which follows only because $X_n$ is compact and mixed integer polyhedral (so $X'_n$ is a finite union of polytopes), and then linear programming duality with attainment over that polyhedron. Neither the polyhedrality of convex hulls of finite unions of polytopes with a common recession direction nor finite-dimensional LP strong duality in the needed form is readily available in Mathlib. A tempting shortcut, Lagrangian duality from convex analysis with a Slater point, does not apply: a binary $\hat x$ lies on the boundary of the projection of $\mathrm{conv}(X''_n)$ onto $z$, so the constraint qualification fails and polyhedrality is genuinely needed.

Formalization scope

States, copies and multipliers are vectors in $\mathbb R^d$ (Fin d → ℝ); a state is binary when each coordinate is $0$ or $1$. Points of $X''_n$ are tuples (z, x, y, θ). Assumption (A1) is three fields of the node structure (nonempty, compact, mixed integer polyhedral after concatenating coordinates). Cuts are indexed by Fin i and children by Fin nC; probabilities are only required to be nonnegative. A last-stage node is nC = 0 with L = 0. The constraint $z \in [0,1]^d$ (2.1c) is kept in $X'_n$ and folded into $X_n$ in (2.3) and (3.1), as in the paper.

Readings of informal words:

• "min" in $\psi^{i+1}_n$, $\mathcal L^i_n$, $\underline Q^i_n$, $Q_n$: the definitions use sInf of the set of objective values, and every theorem states the minimum as an attained least element (IsLeast) or as a lower bound over all feasible points, so no junk value of sInf on an empty or unbounded set is used. The hypothesis $X''_n \ne \emptyset$ makes $\mathcal L^i_n$ a genuine minimum.
• "$\hat\pi$ optimal for (4.3)": maximizes $\pi \mapsto \mathcal L^i_n(\pi) + \pi^\top\hat x$ over all of $\mathbb R^d$.
• "the cuts are valid": $Q_n(x_a) \ge \hat v + \hat\pi^\top x_a$ is stated as a lower bound over every feasible point of (2.3), which is the paper's convention $Q_n = +\infty$ on infeasible states.
• The induction hypothesis of the validity proof is made explicit: all children's cuts $\ell = 1,\dots,i$ are valid, and $\mathcal Q_n \ge L_n$ on binary states.
• Tightness is stated with $\psi^{i+1}_n$; the proof's last line writes $\psi^i_n$, a misprint.

A trivializing formalization is ruled out: $\underline Q^i_n$ is the primal value of the forward problem (3.1) with $\psi^{i+1}_n$ from (3.2) and is never defined through the dual, and validity is required at every binary $x_a$, not only at $\hat x$.

A complete development needs: polyhedrality of convex hulls of bounded mixed integer sets, LP strong duality with attainment (or Geoffrion's theorem directly), Carathéodory-type reasoning in product spaces, and the fact that a binary point which is a positive convex combination of points of $[0,1]^d$ equals each of them. The first two are reusable well beyond this mission. Proofs of individual milestones are welcome independently; the validity milestones are accessible first.

Selected references

• J. Zou, S. Ahmed, X. A. Sun, Stochastic dual dynamic integer programming, Math. Program. 175 (2019) 461–502. https://doi.org/10.1007/s10107-018-1249-5
• A. M. Geoffrion, Lagrangean relaxation for integer programming, Math. Program. Study 2 (1974) 82–114. https://doi.org/10.1007/BFb0120690
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Math. Program. 52 (1991) 359–375. https://doi.org/10.1007/BF01582895