All missions

Motivation

A busy runway is the bottleneck of an airport, and the order in which arriving or departing aircraft use it determines how many operations fit into an hour. Consecutive aircraft must be spaced by minimum separations that depend on both aircraft (a light aircraft behind a heavy one needs a long gap because of wake turbulence), so reordering the first-come-first-served (FCFS) queue can raise throughput considerably. Unrestricted reordering is unacceptable in practice: it makes the controllers' job harder and can push one aircraft to the back of the queue indefinitely. Following Dear (1976), constrained position shifting (CPS) allows each aircraft to move at most $k$ positions away from its FCFS position, with $k$ between 1 and 3 in practice.

Earlier algorithms for CPS either exploited a small number of aircraft types and ignored time windows and precedence constraints (Psaraftis 1980), or needed exponentially many parallel processors (Trivizas 1998), and Carr (2004) conjectured that runway scheduling under CPS has exponential complexity in general. Balakrishnan and Chandran (Oper. Res. 58(6), 2010) showed that, for fixed $k$, the problem with time windows and precedence constraints is solved by dynamic programming on a network whose size is linear in the number of aircraft. This mission formalizes the core of that result: the network, its precedence pruning, and the dynamic program for the minimum makespan.

Setting

There are $n\ge 1$ aircraft, labelled $0,\dots,n-1$ in FCFS order, and the landing positions are also $0,\dots,n-1$. An instance consists of

1. the maximum position shift $k\in\mathbb N$;
2. separations $\delta_{ab}\ge 0$, the minimum time between a leading aircraft $a$ and a trailing aircraft $b$, satisfying the triangle inequality $\delta_{ac}\le\delta_{ab}+\delta_{bc}$ (which holds for wake-vortex separations in arrivals-only or departures-only operation);
3. a time window $[e(a),l(a)]$ for each aircraft;
4. a finite set of precedence pairs $(x,y)$ of distinct aircraft, meaning that $x$ lands before $y$.

A $k$-CPS sequence is a bijection $\sigma$ from positions to aircraft with $|\sigma(p)-p|\le k$ for all $p$. A feasible schedule is such a $\sigma$ with landing times $t_p$ such that $e(\sigma(p))\le t_p\le l(\sigma(p))$, $\delta_{\sigma(p)\sigma(q)}\le t_q-t_p$ for all positions $p<q$, and every precedence pair is respected. The makespan is $t_{n-1}$, the landing time of the last aircraft.

The CPS network has stages $p=1,\dots,n$. A node of stage $p$ is a list of $\min\{2k+1,p\}$ distinct aircraft occupying the positions that end at $p-1$, each within $k$ of its FCFS position; its last entry is its final aircraft. An arc joins a stage-$p$ node $i$ to a stage-$(p+1)$ node $j$ when the first $\min\{2k,p\}$ entries of $j$ are the last $\min\{2k,p\}$ entries of $i$. A source-sink path picks one node per stage, joined by arcs, and its sequence puts the final aircraft of the stage-$(q+1)$ node at position $q$. The pruned network $G$ deletes the nodes that violate a precedence pair $(x,y)$: those containing $y$ before $x$, or $y$ at a position less than $x-k$, or $x$ at a position greater than $y+k$.

On $G$, with $e(j),l(j)$ the window of the final aircraft of $j$, $\delta_i(j)$ the separation between the final aircraft of $i$ and $j$, and $P(j)$ the predecessors of $j$, the dynamic program is $T^*(j)=e(j)$ at stage 1 and

$$T^*(j)=\max\Big\{e(j),\ \min_{i\in P(j):\,T^*(i)\le l(i)}\big(T^*(i)+\delta_i(j)\big)\Big\}\qquad(1)$$

with $\min\emptyset=+\infty$.

Formalization targets

Goal: §4.1, the minimum makespan rule

$$\exists\ \text{feasible schedule}\iff \exists\, j\in G_n:\ T^*(j)\le l(j),$$ $$\min\{\text{makespan of a feasible schedule}\}=\min\{T^*(j): j\in G_n,\ T^*(j)\le l(j)\},$$

where $G_n$ is stage $n$ of $G$; the second identity is stated as "$\tau$ is the least makespan iff $\tau$ is the least admissible $T^*(j)$" for every real $\tau$.

Milestones

1. Theorem 1. $\sigma$ is a $k$-CPS sequence iff it is the sequence of a source-sink path of the CPS network.
2. Lemma 1 (Case I). For $a<b$, a path whose sequence puts $a$ after $b$ has a node containing $b$ before $a$.
3. Lemma 2 (Case II). For $a<b$, in the position-constrained network, a path whose sequence puts $a$ before $b$ has a node containing $a$ before $b$.
4. §3.1 conclusion. The source-sink paths of $G$ are exactly the $k$-CPS sequences respecting all precedence pairs.
5. Lemma 3. For every node $j$ of $G$, $T^*(j)$ is the earliest landing time of the final aircraft of $j$ over all partial schedules ending at $j$, and $+\infty$ exactly when there is none.

Significance

The network turns a search over permutations into a shortest-path-like computation over $O(n(2k+1)^{2k+1})$ nodes, so for the small values of $k$ used in practice the minimum makespan with time windows and precedence constraints is computed in time linear in $n$. The same network underlies the paper's algorithms for total delay (§5.2) and, in a time-expanded form, for arbitrary separable costs without the triangle inequality (§6).

The paper's proofs are short and informal. A formalization pins down exactly what $T^*(j)$ means (the paper describes it only as "arrival time of the final aircraft of node $i$ in an optimal solution"), makes precise which nodes the precedence pruning removes, and checks the correctness of the stage-$n$ rule. The result has not been machine-checked before.

Difficulty

Two features of the model make the correctness of the network nontrivial. First, a node records only a window of at most $2k+1$ consecutive positions, so nothing local prevents a path from using the same aircraft twice or omitting one; Theorem 1 asserts that the global sequence is nevertheless a permutation, and Lemmas 1 and 2 assert that precedence, a global property of the sequence, is detected inside single nodes. Second, the recursion (1) adds the separation only between consecutive aircraft, while feasibility constrains every pair of aircraft; the triangle inequality is what reconciles the two, and without it Lemma 3 fails.

The obvious reading of §4.1 also fails: taking the least $T^*(j)$ over all stage-$n$ nodes, as the paper prints, can select a node whose final aircraft lands after its latest time. The goal filters stage $n$ by $T^*(j)\le l(j)$.

Formalization scope

All data are real numbers; aircraft and positions are Fin n, 0-based; stages are 1-based natural numbers; [NeZero n] encodes $n\ge 1$. Separations are pairwise in the definition of feasibility, never only consecutive. The recursion takes values in WithTop ℝ, with $\top=+\infty$; optima are stated with IsLeast over sets of makespans, never with a real infimum. Precedence pairs are a Finset of ordered pairs of distinct aircraft, covering both of the paper's cases.

Explicit readings of loose phrases:

• "corresponding source-sink path" (Theorem 1) is the path whose final aircraft, stage by stage, form the sequence, as defined in the proof;
• "the values of $T^*(\cdot)$" (Lemma 3) are earliest landing times over partial schedules ending at the node: paths in $G$ with times satisfying the windows of the earlier aircraft, the earliest time of the last one, and all pairwise separations;
• "the minimum makespan is the lowest value of $T^*(\cdot)$ among all nodes in stage $n$" is corrected to the nodes with $T^*(j)\le l(j)$, which is the paper's own feasibility check;
• the Case II position filter uses the printed rule ($<b-k$, $>a+k$).

Not formalized: running times (Proposition 1 and the $O(k)$ preprocessing remark), the predecessor pointers and tie-breaking that reconstruct an optimal sequence, the removal of nodes unreachable from the source or the sink (it does not change the set of source-sink paths), asymmetric shifts (§3.2) and disjoint time windows.

A formalization that defines feasibility with consecutive separations only, defines $T^*$ by the recursion and states Lemma 3 as an unfolding, or states Theorem 1 as "some CPS sequence exists iff some path exists" would be trivial; the statements here avoid all three.

The definitions (instance, $k$-CPS sequences, the CPS network and its pruning) are shared with the two other missions of this series (total delay, discrete time) and may be consolidated later. Proofs of the milestones, and lemmas about the window structure of the network, are welcome.

Selected references

• H. Balakrishnan, B. G. Chandran, Algorithms for Scheduling Runway Operations Under Constrained Position Shifting, Operations Research 58(6), 1650–1665, 2010. https://doi.org/10.1287/opre.1100.0869
• H. N. Psaraftis, A Dynamic Programming Approach for Sequencing Groups of Identical Jobs, Operations Research 28(6), 1347–1359, 1980. https://doi.org/10.1287/opre.28.6.1347
• R. G. Dear, The Dynamic Scheduling of Aircraft in the Near Terminal Area, MIT Flight Transportation Laboratory Report R76-9, 1976.
• D. A. Trivizas, Optimal Scheduling with Maximum Position Shift (MPS) Constraints: A Runway Scheduling Application, Journal of Navigation 51(2), 250–266, 1998.
• F. R. Carr, Robust Decision-Support Tools for Airport Surface Traffic, Ph.D. thesis, Massachusetts Institute of Technology, 2004.

Motivation

Runway capacity is the binding constraint at many busy airports. An aircraft landing or taking off behind another must wait a minimum separation time that depends on the two aircraft's weight classes, because of wake vortices; the US Federal Aviation Administration publishes these spacing requirements. Reordering aircraft changes the sum of the separations incurred and hence the delays, but unrestricted reordering is unacceptable to airlines and controllers: an aircraft that arrived early could be pushed to the end of the queue. Constrained position shifting (CPS), introduced by Psaraftis (1980) and used in the United States and Europe since, allows each aircraft to move at most $k$ positions from its first-come-first-served (FCFS) position.

Balakrishnan and Chandran (Operations Research 58(6), 2010) recast CPS scheduling as dynamic programming on a layered network, the CPS network, whose size is polynomial in the number of aircraft $n$ for fixed $k$. Their §4 minimizes the makespan (the landing time of the last aircraft). §5.2 minimizes the total delay, equivalently the average delay, which measures passenger and airline cost more directly. This mission formalizes §5.2.

Setting

There are $n$ aircraft labelled $1,\dots,n$ in FCFS order, a maximum position shift $k\in\mathbb N$, separations $\delta_{ab}\ge 0$ (the minimum time between leading aircraft $a$ and trailing aircraft $b$), and a finite set of precedence pairs $(x,y)$ with $x\ne y$, meaning that $x$ must land before $y$. The separations satisfy the triangle inequality $\delta_{ac}\le\delta_{ab}+\delta_{bc}$, as wake-vortex separations do for arrivals-only or departures-only operations.

A $k$-CPS sequence is a permutation $\sigma$ of the aircraft (position $p$ receives aircraft $\sigma(p)$) with $|\sigma(p)-p|\le k$ for every $p$. A feasible schedule is a $k$-CPS sequence that places $x$ before $y$ for each precedence pair, together with landing times $t_1,\dots,t_n$ (by position) such that

$$t_p\ge 0,\qquad t_q-t_p\ge\delta_{\sigma(p)\sigma(q)}\quad(p<q).$$

There are no time windows. Its total delay is $t_1+\dots+t_n$, measured from time $0$, at which all aircraft are available.

The CPS network has stages $1,\dots,n$. A node of stage $p$ is a sequence of $\min\{2k+1,p\}$ distinct aircraft that can occupy positions $p-\min\{2k+1,p\}+1,\dots,p$ (each within $k$ of its position). Its last aircraft is its final aircraft. An arc joins a stage-$p$ node $i$ to a stage-$(p+1)$ node $j$ when the sequences overlap: the first $\min\{2k,p\}$ aircraft of $j$ are the last $\min\{2k,p\}$ aircraft of $i$. A source-sink path picks one node per stage, and its sequence assigns position $p$ to the final aircraft of the stage-$p$ node. Precedence is incorporated by deleting every node that places $y$ before $x$ for some pair $(x,y)$, or that places an aircraft outside the positions a pair allows it (§3.1). The result is the pruned network $G$. For nodes $i,j$, $\delta_i(j)$ is the separation between their final aircraft.

For a node $j$ in stage $p$ and times $t_1,\dots,t_p$ along a path to $j$, the paper uses the partial objective

$$\theta_j(p)=t_1+\dots+t_{p-1}+(n-p+1)\,t_p .$$

Formalization targets

Goal: the shortest-path equivalence (§5.2, p. 1656)

Give the arc $(i,j)$ from stage $p-1$ to stage $p$ the distance $(n-p+1)\delta_i(j)$, and source and sink arcs distance $0$. Then a feasible schedule exists if and only if $G$ has a source-sink path, and

$$\min_{(\sigma,t)\ \text{feasible}}\ \sum_{p=1}^{n}t_p\;=\;\min_{v\ \text{source-sink path of }G}\ \sum_{p=2}^{n}(n-p+1)\,\delta_{v_{p-1}}(v_p),$$

where each minimum exists exactly when the other does.

Milestones

1. Theorem 1 with Lemmas 1–2 (pp. 1652–1654): the source-sink paths of $G$ are exactly the $k$-CPS sequences respecting the precedence pairs.
2. Proposition 2 (p. 1656): in a schedule of minimum total delay, $t_p-t_{p-1}=\delta_{\sigma(p-1)\sigma(p)}$ for every $p\ge 2$.
3. Proposition 3 (p. 1656): all paths from the source to a node lying on some source-sink path contain the same set of aircraft.
4. The recursion of §5.2 (p. 1656): with $\theta^*_j(p)$ the minimum of $\theta_j(p)$ over partial schedules ending at $j$, $\theta^*_j(1)=0$ and

$$\theta^*_j(p)=\min_{i\in P(j)}\big(\theta^*_i(p-1)+(n-p+1)\,\delta_i(j)\big),$$

where $P(j)$ is the set of predecessors of $j$ in $G$.

Significance

The result turns a sequencing problem over up to $n!$ orders into a shortest-path computation on a directed acyclic graph with $O(n(2k+1)^{2k+1})$ nodes, and it does so while respecting precedence constraints, which earlier CPS algorithms (Psaraftis 1980; Trivizas 1998) could not handle. It is the average-delay counterpart of the makespan algorithm of §4 and shares its network. The same network carries the discrete-time models of §6.

The paper's proof of the equivalence is one sentence ("follows from properties of shortest paths and is omitted here"). Propositions 2 and 3 are proved in a few lines, and Theorem 1 by an argument about windows of $2k+1$ consecutive positions. None of these results has a machine-checked proof. A formal development makes explicit the conventions the prose leaves implicit (the time origin, pairwise separations, which nodes Proposition 3 refers to) and checks that the recursion and the shortest-path value really compute the minimum total delay.

Difficulty

The arc distances weight the separation into stage $p$ by $n-p+1$, the number of aircraft whose landing it delays. The equivalence needs two directions. A path's length must be the total delay of the schedule that lands each aircraft at its predecessor's time plus the separation, and that schedule must satisfy every pairwise separation, not only the consecutive ones; this is where the triangle inequality enters. Conversely, every feasible schedule must have total delay at least the length of its sequence's path, and every feasible sequence must be a path of $G$. The last point is Theorem 1 with precedence pruning: a node sees only $2k+1$ consecutive positions, so detecting a violated precedence pair inside one node requires the position filter of §3.1 for pairs that reverse FCFS order. Proposition 3 is false for nodes that lie on no source-sink path, which the printed statement does not exclude.

Formalization scope

Aircraft and positions are Fin n, 0-based, and stages are 0-based natural numbers, so the arc into stage $s$ has distance $(n-s)\delta_i(j)$. Separations are real, nonnegative and satisfy the triangle inequality; feasibility requires them between every pair of positions. Landing times are real and nonnegative. The paper fixes no time origin, but its path length equals the total delay exactly when delays are measured from $0$, and without a lower bound on the times the objective has no minimum. Minima are stated with IsLeast on sets of values, never with a real infimum. Feasibility and the existence of a path are stated separately, because the equality of least elements alone does not force them to exist.

The following loose phrases are given explicit readings. "In an optimal solution" (Proposition 2) means a feasible schedule whose total delay is at most that of every feasible schedule. "The CPS network" in Proposition 3 means nodes lying on a source-sink path, stated for the network without precedence pruning, which also covers the pruned one. "$\theta^*$" means the least element of the set of values of $\theta_j(p)$ over partial schedules ending at $j$, and the printed $\theta^*_j(s)$ is read as $\theta^*_j(p)$. The boundary value $\theta^*_j(1)=0$ is not printed and is stated explicitly. Precedence pruning uses the printed Case II rule. Running times (the $O(n(2k+1)^{2k+2})$ bound) are not formalized.

A trivializing formalization would require separations only between consecutive aircraft, define the minimum by the recursion itself, or use a network whose nodes need not be distinct or admissible. Here the minimum is defined directly over feasible schedules, separations are pairwise, and the nodes are checked against the paper's Figure 1 (stage sizes 2, 4, 7, 14, 14, 7 and 13 paths for $n=6$, $k=1$).

The development needs finite sums, permutations of Fin n and lists. The network layer (stages, arcs, precedence pruning, Theorem 1) is shared with the makespan and discrete-time missions of this series and reusable for any CPS objective. Proofs of any milestone, alternative proofs of the goal, and generalizations (asymmetric shifts, §3.2) are welcome.

Selected references

• H. Balakrishnan, B. G. Chandran, Algorithms for Scheduling Runway Operations Under Constrained Position Shifting, Operations Research 58(6), 1650–1665, 2010. https://doi.org/10.1287/opre.1100.0869
• H. N. Psaraftis, A Dynamic Programming Approach for Sequencing Groups of Identical Jobs, Operations Research 28(6), 1347–1359, 1980. https://doi.org/10.1287/opre.28.6.1347
• R. G. Dear, Y. S. Sherif, An Algorithm for Computer Assisted Sequencing and Scheduling of Terminal Area Operations, Transportation Research Part A 25(2–3), 129–139, 1991.
• D. A. Trivizas, Optimal Scheduling with Maximum Position Shift (MPS) Constraints: A Runway Scheduling Application, Journal of Navigation 51(2), 250–266, 1998.
• R. de Neufville, A. Odoni, Airport Systems: Planning, Design, and Management, McGraw-Hill, 2003.

Motivation

A submodular function on a finite set $V$ is a function $f$ on subsets of $V$ with $f(X \cup Y) + f(X \cap Y) \le f(X) + f(Y)$. Minimizing such a function is one of the central tractable problems of combinatorial optimization: it contains minimum cuts in directed graphs, matroid intersection and polymatroid problems, and many scheduling and facility-location subproblems. Grötschel, Lovász and Schrijver showed in 1981 that it can be done in polynomial time with the ellipsoid method; in 2000, Schrijver (JCTB 80, 346–355) and, simultaneously, Iwata, Fleischer and Fujishige (J. ACM 48, 2001) gave the first combinatorial strongly polynomial algorithms.

In many applications the function is not defined on all subsets of $V$ but only on a ring family: a collection closed under union and intersection, such as the order ideals of a precedence relation in scheduling, or the sets of a closure system. The last section of Schrijver's paper (§6, pp. 353–354) shows that nothing is lost: any algorithm minimizing submodular functions on all subsets of $V$ also minimizes a submodular function given only on a ring family. This mission formalizes that reduction.

Setting

Let $V$ be a finite set. A collection $\mathcal C$ of subsets of $V$ is a ring family if $X \cup Y \in \mathcal C$ and $X \cap Y \in \mathcal C$ whenever $X, Y \in \mathcal C$. A real function $f$ is submodular on $\mathcal C$ if

$$f(X \cup Y) + f(X \cap Y) \le f(X) + f(Y) \qquad (X, Y \in \mathcal C).$$

Following the paper, $\mathcal C$ is normalized: $\emptyset \in \mathcal C$, $V \in \mathcal C$, and $M_u \ne M_v$ for all $u \ne v$, where $M_v$ is the smallest set of $\mathcal C$ containing $v$. (Elements with the same $M_v$ can be identified.) Under this normalization $\mathcal C$ is the family of lower ideals of a partial order on $V$.

For $X \subseteq V$, the closure $\overline X$ is the smallest set of $\mathcal C$ containing $X$. For $v \in V$, $L_v$ is the largest set of $\mathcal C$ not containing $v$. The paper defines weights

$$c(v) := \max\{0,\ f(L_v) - f(L_v \cup \{v\})\} \qquad (23)$$

with the modular extension $c(X) := \sum_{v \in X} c(v)$, and the function on all subsets of $V$

$$g(X) := f(\overline X) + c(\overline X) \qquad (X \subseteq V). \qquad (26)$$

In Lean, $V$ is a type with [Fintype V] [DecidableEq V], subsets are Finset V, $\mathcal C$ is C : Set (Finset V), and the objects above are IsRingFamily C, SubmodularOn C f, closure C X, M C v, L C v, cw C f v (for $c(v)$), csum C f X (for $c(X)$) and g C f X, all in the namespace SchrijverSFM.Ring.

Formalization targets

Goal: the reduction

Under the normalization above, for $f$ submodular on $\mathcal C$:

$$g \text{ is submodular on all subsets of } V,$$

and, if $U \subseteq V$ minimizes $g(U) - c(U)$ over all subsets of $V$, then $\overline U \in \mathcal C$ and

$$f(\overline U) \le f(T) \qquad \text{for all } T \in \mathcal C.$$

Both conjuncts are needed: the second alone follows almost from the definitions, while the first is what makes an all-subsets algorithm applicable to $g - c$ in the first place.

Milestones

1. $\mathcal C$ is the collection of all lower ideals of some partial order on $V$ (p. 353).
2. $L_v$ is the largest set in $\mathcal C$ not containing $v$, equal to the union of the $M_u$ not containing $v$, and $L_v \cup \{v\} \in \mathcal C$ (p. 353, (23)).
3. The one-element step (25): $f(X) \le f(Y) + c(v)$ for $X, Y \in \mathcal C$, $Y = X \cup \{v\}$, $v \notin X$.
4. Monotonicity (24): $f(Y) + c(Y) \ge f(X) + c(X)$ for $X \subseteq Y$ in $\mathcal C$.
5. The closure identities $\overline X \cup \overline Y = \overline{X \cup Y}$ and $\overline X \cap \overline Y \supseteq \overline{X \cap Y}$.
6. Display (27): $g$ is submodular.
7. Transfer of minimizers: if $U$ minimizes $g - c$ over $2^V$, then $\overline U$ minimizes $f$ over $\mathcal C$.

Significance

The reduction means that a single algorithm for unconstrained submodular minimization serves for every ring family, given only the sets $M_v$. This is how ring-family constrained problems (for example minimum-cost closures and precedence-constrained scheduling objectives) are routinely handed to general submodular-minimization codes, and it is the standard justification for stating submodular minimization algorithms over $2^V$ only.

On the formal side, the mission produces a small reusable layer on ring families of finite sets (closure operator, the lower-ideal representation, the largest set avoiding an element) together with the monotonization trick (24), which is of independent use whenever a function on a lattice of sets has to be made monotone by a modular correction. The result is classical and its proof in the paper is complete; to our knowledge no machine-checked version exists. Companion mission I of this series formalizes the algorithm of §§2–5 itself; this mission does not depend on it, since the algorithm enters only as the hypothesis that a minimizer $U$ of $g - c$ is given.

Difficulty

Every step is elementary, but two points are easy to get wrong. First, (24) is proved on the page by assuming $Y = X \cup \{v\}$; reducing the general case $X \subseteq Y$ to such one-element steps inside $\mathcal C$ requires the normalization $M_u \ne M_v$: without it a ring family can jump by more than one element (for $\mathcal C = \{\emptyset, V\}$ with $|V| = 2$ the inequality (24) fails for suitable $f$). Second, the weights $c(v)$ evaluate $f$ at $L_v \cup \{v\}$, which belongs to $\mathcal C$ only because of the same normalization; a formalization that drops it lets values of $f$ outside $\mathcal C$ leak into $c$ and $g$. The submodularity proof (27) also needs the asymmetric closure facts — equality for unions but only containment for intersections — which is exactly why the monotonicity (24) is required.

Formalization scope

• $V$ is a finite type with decidable equality; subsets are Finset V; $\mathcal C$ is a Set (Finset V).
• $f$ is a real function on all of Finset V; only its values on $\mathcal C$ matter, and under the hypotheses no other value enters $c$, $g$ or the conclusions. The paper allows any ordered field; the formalization uses $\mathbb R$.
• The normalization of p. 353 is assumed as hypotheses: ∅ ∈ C, Finset.univ ∈ C, and M C u ≠ M C v for u ≠ v. No hypothesis $f(\emptyset) = 0$ is made; §6 does not use it.
• The closure is the intersection (Finset.inf) of the sets of $\mathcal C$ containing $X$, and $L_v$ the union (Finset.sup) of the sets of $\mathcal C$ avoiding $v$; their default values on an empty family are never reached under the hypotheses.
• $c(X)$ is the modular extension $\sum_{v \in X} c(v)$; the $\max\{0, \cdot\}$ in (23) is kept, so $c \ge 0$.
• Submodularity of $g$ on all subsets is the published platform definition NonmonotoneSubmod.Shared.Submodular.
• Not formalized: the running-time claims of §6 ("we can find $c$ by $2|V|$ oracle calls", strongly polynomial time) and the oracle model; there is no machine model.
• The goal does not assume (24) or (27), and it is not the minimizer-transfer statement alone, which would be near-definitional.

Contributions welcome: proofs of the milestones in the order listed, general lemmas on closure operators of ring families of Finsets, and the lower-ideal representation, which is reusable beyond this mission.

Selected references

• A. Schrijver, A combinatorial algorithm minimizing submodular functions in strongly polynomial time, J. Combin. Theory Ser. B 80 (2000), 346–355. https://doi.org/10.1006/jctb.2000.1989
• S. Iwata, L. Fleischer, S. Fujishige, A combinatorial strongly polynomial algorithm for minimizing submodular functions, J. ACM 48 (2001), 761–777. https://doi.org/10.1145/502090.502096
• M. Grötschel, L. Lovász, A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1 (1981), 169–197. https://doi.org/10.1007/BF02579273

Why stability of two-stage programs matters

A linear two-stage stochastic program with fixed recourse chooses a here-and-now decision $x$ before a random vector $\xi$ is observed, and pays a recourse cost afterwards. It is the basic model of stochastic programming, used in capacity planning, energy and supply-chain models. In practice the distribution $\mu$ of $\xi$ is never known exactly: it is estimated from data, replaced by a discrete scenario approximation, or perturbed for robustness. The question is how much the optimal value and the optimal decisions can move when $\mu$ is replaced by a nearby $\nu$, and in which distance between probability measures "nearby" should be measured.

Rachev and Römisch (Math. Oper. Res. 27(4), 2002, doi:10.1287/moor.27.4.792.304; the mission cites the authors' preprint from edoc.hu-berlin.de) answer this with the method of probability metrics: they derive from the structure of the integrand a canonical distance on measures for each class of models. For linear two-stage programs the canonical distance is the Fortet–Mourier metric of order 2.

Timeline. Robinson and Wets (1987) studied qualitative stability of two-stage programs with respect to weak convergence of measures. Walkup and Wets (1969) had earlier established the piecewise-bilinear structure of the second-stage value function used here. Römisch and Schultz (1991) proved a quantitative stability result for two-stage programs with complete recourse in the Wasserstein metric $W_2$. The present paper (published 2002) replaces complete recourse by relatively complete recourse plus dual feasibility, and $W_2$ by the metric $\zeta_2$, which it bounds by a multiple of $W_2$ (p. 13).

Setting

Let $X\subseteq\mathbb R^m$ be a nonempty polyhedron and $\Xi\subseteq\mathbb R^s$ a polyhedron. Fix $c\in\mathbb R^m$, an $(r,\overline m)$-matrix $W$, and data $q(\xi)\in\mathbb R^{\overline m}$, $h(\xi)\in\mathbb R^r$ and an $(r,m)$-matrix $T(\xi)$ depending affine linearly on $\xi$. The second-stage value is

$$\Phi(u,t)=\inf\{uy:\ Wy=t,\ y\ge0\},$$

with $\operatorname{pos}W=\{Wy:y\ge0\}$ and $D=\{u:\{z:W'z\le u\}\ne\emptyset\}$. The integrand is $f_0(\xi,x)=cx+\Phi(q(\xi),h(\xi)-T(\xi)x)$ when $h(\xi)-T(\xi)x\in\operatorname{pos}W$ and $q(\xi)\in D$, and $+\infty$ otherwise. For a Borel probability measure $\nu$ on $\Xi$ the problem is

$$\min\Big\{\int_\Xi f_0(\xi,x)\,\nu(d\xi):x\in X\Big\},$$

with optimal value $v(\nu)$ and solution set $S(\nu)$. Two assumptions are made: (A1) $h(\xi)-T(\xi)x\in\operatorname{pos}W$ and $q(\xi)\in D$ for all $(\xi,x)\in\Xi\times X$; (A2) $\mu$ has a finite second moment.

The Fortet–Mourier metric $\zeta_2$ on $\mathcal P_2(\Xi)$, the probability measures on $\Xi$ with finite second moment, is

$$\zeta_2(\mu,\nu)=\sup_{f\in\mathcal F_2(\Xi)}\Big|\int_\Xi f\,d\mu-\int_\Xi f\,d\nu\Big|,\quad \mathcal F_2(\Xi)=\{f:|f(\xi)-f(\tilde\xi)|\le\max\{1,\|\xi\|,\|\tilde\xi\|\}\|\xi-\tilde\xi\|\}.$$

For an open bounded $\mathcal U\supseteq S(\mu)$, the growth function is $\psi(\tau)=\inf\{\int_\Xi f_0(\xi,x)\,\mu(d\xi)-v(\mu): d(x,S(\mu))\ge\tau,\ x\in X\cap\operatorname{cl}\mathcal U\}$, and $\Psi(\eta)=\eta+\psi^{-1}(2\eta)$ with $\psi^{-1}(t)=\sup\{\tau\ge0:\psi(\tau)\le t\}$.

Formalization targets

Goal: Theorem 3.3 (p. 13)

Under (A1), (A2), $S(\mu)\ne\emptyset$ and $\mathcal U$ an open bounded neighbourhood of $S(\mu)$, there are $L>0$ and $\delta>0$ such that for every $\nu\in\mathcal P_2(\Xi)$ with $\zeta_2(\mu,\nu)<\delta$:

$$|v(\mu)-v(\nu)|\le L\,\zeta_2(\mu,\nu),\qquad \emptyset\ne S(\nu)\subseteq S(\mu)+\Psi(L\,\zeta_2(\mu,\nu))\,\mathbb B.$$

The constants are existential, so the goal does not depend on any particular estimate of them.

Milestones

1. Lemma 3.1 (p. 11): $\Phi$ is finite and continuous on the polyhedral cone $D\times\operatorname{pos}W$, piecewise of the form $C_ju\cdot t$ on finitely many polyhedral cones with disjoint interiors, convex in $t$ and concave in $u$.
2. Proposition 3.2 (p. 11): $f_0$ is a normal convex integrand, and for $\|x\|\le r$ it satisfies $|f_0(\xi,x)-f_0(\tilde\xi,x)|\le Lr\max\{1,\|\xi\|,\|\tilde\xi\|\}\|\xi-\tilde\xi\|$, a Lipschitz bound in $x$ with factor $\hat L\max\{1,\|\xi\|^2\}$, and $|f_0(\xi,x)|\le Kr\max\{1,\|\xi\|^2\}$.
3. $\mathcal P_{\mathcal F_{\mathcal U}}\supseteq\mathcal P_2(\Xi)$ (p. 13): every measure with finite second moment satisfies the integrability conditions of the general theory.
4. Corollary 2.8 (p. 10): the general Lipschitz stability theorem in the metric $\zeta_g$ for convex models whose integrands lie, up to a factor $L$, in the class $\mathcal F_g$.

Significance

The theorem says that, under the two natural well-posedness conditions of linear recourse models, optimal values are Lipschitz continuous and solution sets move by at most $\Psi(L\zeta_2)$, where $\zeta_2$ only sees test functions with the local Lipschitz growth of the integrand. Since $\zeta_2\le(1+\int\|\xi\|^2d\mu+\int\|\xi\|^2d\nu)^{1/2}W_2$, the result contains the earlier $W_2$ stability theorem.

The results are proved in the paper, except Lemma 3.1, which it cites from Walkup and Wets (1969). None of them is formalized in Mathlib or on Prove2Me. A formalization would provide a checked model of the two-stage recourse function, the Fortet–Mourier metrics, and an end-to-end quantitative stability theorem for stochastic programs, none of which exist in Mathlib.

Difficulty

The obvious argument bounds $|v(\mu)-v(\nu)|$ by $\sup_x|\int f_0(\cdot,x)\,d(\mu-\nu)|$ and then by $L\zeta_2$. Two steps fail. First, the supremum ranges over all of $X$, which may be unbounded, while $f_0(\cdot,x)/L$ lies in $\mathcal F_2$ only for $x$ in a bounded set; the argument must localize to $X\cap\operatorname{cl}\mathcal U$ and then show, using convexity, that for $\nu$ close to $\mu$ the localized and global problems coincide. Second, the Lipschitz estimate in $\xi$ for $f_0$ requires the piecewise-bilinear structure of $\Phi$ (Lemma 3.1) and a chaining argument across the polyhedral pieces of $\Xi$; the integrand is not differentiable.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The paper never fixes its norm and all its constants are existential, so the Euclidean norm is a faithful instance. Second-stage vectors $u,t,y,z$ are coordinate vectors Fin k → ℝ; index sets are 0-based.
• A polyhedron is a finite intersection of closed half-spaces. The standing assumptions are: $X$ a nonempty polyhedron, $\Xi$ a polyhedron, $q,h,T$ affine maps.
• A measure in $\mathcal P(\Xi)$ is a Borel probability measure on $\mathbb R^s$ with $\nu(\Xi^c)=0$; $\int_\Xi f_0(\xi,x)\,\nu(d\xi)$ is the extended-real integral of the published DupacovaWets.Consistency.expect over $\nu$ restricted to $\Xi$.
• $\Phi$, $f_0$, $v$ and $\psi$ are extended-real infima ($+\infty$ over an empty set); "min" in $\psi$ is read as an infimum. $\zeta_2$, $\zeta_g$, $\psi^{-1}$ and $\Psi$ take values in $[0,\infty]$, and the distance to a set is the extended distance ($+\infty$ to $\emptyset$).
• To rule out trivializations: every value bound states that $v(\mu)$, $v(\nu)$ are finite before comparing them, so the extended-real arithmetic $\infty-\infty$ cannot make it vacuous; in $\zeta_2$ a test function that is not integrable for both measures contributes $+\infty$, never a junk $0$.
• Disclosed readings: Proposition 3.2 leaves its radius $r$ unquantified; it is stated with the constants first and then every $r\ge1$. Lemma 3.1's "$\operatorname{pos}W\times D$" is read as $D\times\operatorname{pos}W$, in the order of $\Phi$'s arguments. Corollary 2.8 adds $\mu,\nu\in\mathcal P_{\mathcal F_{\mathcal U}}(\Xi)$, an assumption of Theorem 2.2 that its proof invokes; Theorem 3.3 needs no such addition, because milestone 3 supplies it.
• Needed infrastructure: LP duality and the Walkup–Wets decomposition of $\Phi$; normal integrands and measurability of their infima; integrability under moment conditions; the general stability theorems (Theorems 2.2–2.3 of the paper) for $d=0$. The definitions of $\zeta_p$, $\mathcal F_g$ and normal integrands are reusable well beyond this mission. Contributions toward any milestone, and proofs of the auxiliary facts (for example, that every $f\in\mathcal F_2(\Xi)$ is integrable for $\nu\in\mathcal P_2(\Xi)$), are welcome.

Selected references

• S. T. Rachev, W. Römisch, Quantitative stability in stochastic programming: The method of probability metrics, Mathematics of Operations Research 27(4) (2002) 792–818. https://doi.org/10.1287/moor.27.4.792.304 (cited here from the authors' preprint, edoc.hu-berlin.de)
• D. W. Walkup, R. J-B Wets, Lifting projections of convex polyhedra, Pacific Journal of Mathematics 28 (1969) 465–475 (the paper's [55]).
• S. M. Robinson, R. J-B Wets, Stability in two-stage stochastic programming, SIAM Journal on Control and Optimization 25 (1987) 1409–1416 (the paper's [37]).
• W. Römisch, R. Schultz, Stability analysis for stochastic programs, Annals of Operations Research 30 (1991) 241–266 (the paper's [40]).
• R. T. Rockafellar, R. J-B Wets, Variational Analysis, Springer (the paper's [38]; normal integrands, Chapter 14).
• S. T. Rachev, Probability Metrics and the Stability of Stochastic Models, Wiley, Chichester 1991 (the paper's [32]).

Motivation

A Markov decision process is specified by numbers: transition probabilities and rewards. In practice these numbers are estimated from data, elicited from experts, or produced by aggregating the states of a larger model, and in each case what is actually known is a range for each parameter rather than its value. Givan, Leach and Dean (Artificial Intelligence, 2000) introduced bounded-parameter MDPs (BMDPs) to reason about a whole family of MDPs at once: every transition probability is only known to lie in a closed interval. Their motivation was state-space aggregation, where grouping states with similar but not identical dynamics yields exactly such interval bounds, and the same object later reappeared as the interval or "box" uncertainty set of robust MDPs (Nilim and El Ghaoui, 2005; Iyengar, 2005) and of optimistic exploration in reinforcement learning (Strehl and Littman, 2008).

Over such a family, the value of a policy is no longer a number but an interval, and "optimal" needs a definition. This mission formalizes the paper's answer: two total orders on intervals, the corresponding optimal policies, and the Bellman-like equations their interval value functions satisfy.

Setting

An exact MDP $M=\langle Q,A,F,R\rangle$ has a finite set $Q$ of states, a finite nonempty set $A$ of actions, transition probabilities $F_{pq}(\alpha)\ge 0$ with $\sum_{q}F_{pq}(\alpha)=1$, a reward $R(q)\in\mathbb R$ for each state and a discount rate $0\le\gamma<1$. A policy is a map $\pi:Q\to A$; $\Pi$ is the set of all policies. The value function $V_{M,\pi}(p)$ is the expected discounted sum of rewards $\sum_{t\ge 0}\gamma^t\,\mathbb E[R(X_t)\mid X_0=p]$ along the Markov chain with transitions $F_{pq}(\pi(p))$. The operators

$$VI_{M,\pi}(v)(p)=R(p)+\gamma\sum_{q}F_{pq}(\pi(p))\,v(q),\qquad VI_{M,\alpha}(v)(p)=R(p)+\gamma\sum_{q}F_{pq}(\alpha)\,v(q)$$

act on value functions $v:Q\to\mathbb R$. $V_1\le_{\mathrm{dom}}V_2$ is the statewise order.

A BMDP $M_\updownarrow$ gives for each $p,q,\alpha$ an interval $[F_\downarrow{}_{pq}(\alpha),F_\uparrow{}_{pq}(\alpha)]\subseteq[0,1]$ with $\sum_q F_\downarrow{}_{pq}(\alpha)\le 1\le\sum_q F_\uparrow{}_{pq}(\alpha)$, a reward $R$ and a discount rate $\gamma$. Its members $M\in M_\updownarrow$ are the exact MDPs with that $R$ and $\gamma$ and with $F^M_{pq}(\alpha)\in[F_\downarrow{}_{pq}(\alpha),F_\uparrow{}_{pq}(\alpha)]$. The interval value of a policy is

$$V_\updownarrow{}_\pi(q)=\Big[\min_{M\in M_\updownarrow}V_{M,\pi}(q),\ \max_{M\in M_\updownarrow}V_{M,\pi}(q)\Big]=[V_\downarrow{}_\pi(q),V_\uparrow{}_\pi(q)].$$

Intervals are compared by the optimistic order, which compares upper bounds first and breaks ties by lower bounds, and the pessimistic order, which compares lower bounds first:

$$[l_1,u_1]\le_{\mathrm{opt}}[l_2,u_2]\iff u_1<u_2\ \vee\ (u_1=u_2\wedge l_1\le l_2),\qquad [l_1,u_1]\le_{\mathrm{pes}}[l_2,u_2]\iff l_1<l_2\ \vee\ (l_1=l_2\wedge u_1\le u_2).$$

A policy $\pi_{\mathrm{opt}}$ is optimistically optimal if $V_\updownarrow{}_{\pi_{\mathrm{opt}}}(q)\ge_{\mathrm{opt}}V_\updownarrow{}_\pi(q)$ for all $\pi$ and $q$; pessimistically optimal is defined with $\ge_{\mathrm{pes}}$. The optimal interval value functions are $V_\updownarrow{}_{\mathrm{opt}}=V_\updownarrow{}_{\pi_{\mathrm{opt}}}$ and $V_\updownarrow{}_{\mathrm{pes}}=V_\updownarrow{}_{\pi_{\mathrm{pes}}}$.

Formalization targets

Goal: Theorem 9, equations (25) and (26)

At every state $p$,

$$V_\updownarrow{}_{\mathrm{opt}}(p)=\max_{\alpha\in A,\ \le_{\mathrm{opt}}}\Big[\min_{M\in M_\updownarrow}VI_{M,\alpha}(V_\downarrow{}_{\mathrm{opt}})(p),\ \max_{M\in M_\updownarrow}VI_{M,\alpha}(V_\uparrow{}_{\mathrm{opt}})(p)\Big],$$

and the same with $\mathrm{pes}$ in place of $\mathrm{opt}$. The maximum over actions is for the total order on intervals: attained by some action and an upper bound for every action.

Milestones

In the order the proof uses them: Theorem 3 (second sentence: $V_{M,\pi}$ is the unique fixed point of $VI_{M,\pi}$); Theorem 6 (comparison: $u\le_{\mathrm{dom}}VI_{M,\pi}(u)$ implies $u\le_{\mathrm{dom}}V_{M,\pi}$, and its three variants); Lemma 1 (every member's values and backups are bracketed by finitely many order-maximizing MDPs); Lemma 2 (statewise composition of member MDPs dominates, or is dominated by, both components); Theorem 7 ($\pi$-maximizing and $\pi$-minimizing MDPs exist among the order-maximizing ones); Corollary 1 ($V_\downarrow{}_\pi$ and $V_\uparrow{}_\pi$ are a minimum and a maximum for $\le_{\mathrm{dom}}$); Lemma 3 (statewise composition of policies improves the upper, resp. lower, bounds); Theorem 8 (optimistically and pessimistically optimal policies exist).

Significance

Theorem 9 is the interval analogue of the Bellman optimality equation. It is what makes the optimal interval value functions computable: the paper's interval value iteration algorithms $IVI_\updownarrow{}_{\mathrm{opt}}$ and $IVI_\updownarrow{}_{\mathrm{pes}}$ (Section 5) iterate exactly the right-hand sides of (25) and (26). The lower half of (26) is the max-min equation of robust dynamic programming with rectangular box uncertainty, and the upper half of (25) is the max-max equation behind optimistic planning; Theorem 9 states both, together with the tie-breaking second component, in one model. Theorems 7 and 8 are of independent use: a single member MDP is worst (or best) for a policy at all states at once, and the partial orders on interval value functions nevertheless have maxima over policies.

None of these results has a machine-checked proof. The platform has robust Bellman equations in other models (costs, general rectangular sets, a sup over nature) but nothing on BMDPs, interval value functions, or the orders $\le_{\mathrm{opt}}$ and $\le_{\mathrm{pes}}$. The mission produces the paper's optimality theory end to end, from the comparison principle for exact MDPs to the two Bellman-like equations, on a model shared with the companion mission on interval policy evaluation.

Difficulty

The orders $\le_{\mathrm{opt}}$ and $\le_{\mathrm{pes}}$ are total on intervals but only partial on interval value functions, and they are lexicographic. The obvious construction of an optimal policy, switching statewise to whichever of two policies has the better interval, fails: the composed policy need not dominate either component in $\le_{\mathrm{opt}}$, because lower bounds can get worse at states where the upper bounds do not change (the paper says so explicitly, eq. (20)). Existence therefore needs a two-stage argument. A second obstacle is that $V_\downarrow{}_\pi$ and $V_\uparrow{}_\pi$ are defined statewise, as minima over an uncountable family; that one member attains them at every state simultaneously is a theorem (Theorem 7), and the Bellman-like equations rest on it. Finally, the inner minima in (25) act on $V_\downarrow{}_{\mathrm{opt}}$, the lower bound of an optimistically chosen policy, which is not the componentwise best lower bound over policies; the equation couples the two components through the tie-break.

Formalization scope

$Q$ and $A$ are finite types, $A$ is nonempty; $Q$ may be empty. An exact MDP is a structure with transition function F p α q $=F_{pq}(\alpha)$, stochastic rows, reward $R:Q\to\mathbb R$ and discount $0\le\gamma<1$. $V_{M,\pi}$ is defined as the convergent series $\sum_t\gamma^tP_\pi^tR$, not as a solution of (2). Rewards of the BMDP are tight, as the paper assumes from footnote 3 on; reward intervals are not formalized. Members of $M_\updownarrow$ form a subtype of exact MDPs with the BMDP's $R$ and $\gamma$. The minima and maxima of Definition 3 and of (25)–(26) are the real infimum and supremum over that subtype, which is nonempty and on which values are bounded, so no junk value enters. Intervals are pairs (lower, upper); the orders (17) are spelled out. Policies are deterministic stationary maps $Q\to A$, the paper's $\Pi$. An ordering of $Q$ is a bijection Fin |Q| ≃ Q, and the index $r$ of Definition 1 is the largest index at which expression (9) does not exceed 1 (the page's phrase admits ties; only the largest index keeps the remaining mass inside its interval). Definition 8 is read as $V_\updownarrow{}_{\mathrm{opt}}=V_\updownarrow{}_{\pi_{\mathrm{opt}}}$ for an optimistically optimal $\pi_{\mathrm{opt}}$, so the goal is quantified over all optimistically (pessimistically) optimal policies; Theorem 8 is the milestone that makes this quantification non-vacuous. Lemma 3 is stated as in the Appendix (p. 36): part (d) concerns $\pi_4=\pi_1\oplus_{\mathrm{pes}}\pi_2$, where p. 17 misprints $\pi_3$.

A formalization in which members carry their own discount, rows need not sum to one, the minima range over all functions $Q\to A\to Q\to\mathbb R$, or $V_\updownarrow{}_{\mathrm{opt}}$ is the componentwise supremum over policies would make several statements false or trivial; each is ruled out above.

Contributions welcome beyond proofs of the milestones: a reusable theory of discounted policy evaluation for finite MDPs (the series representation, the fixed-point characterization, monotonicity of $VI_{M,\pi}$), which other missions on finite MDPs can import.

Selected references

• R. Givan, S. Leach, T. Dean, Bounded-parameter Markov decision processes, Artificial Intelligence 122 (2000). https://doi.org/10.1016/S0004-3702(00)00047-3
• A. Nilim, L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. https://doi.org/10.1287/opre.1050.0216
• G. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30(2), 2005. https://doi.org/10.1287/moor.1040.0129
• A. Strehl, M. Littman, An analysis of model-based interval estimation for Markov decision processes, Journal of Computer and System Sciences 74(8), 2008. https://doi.org/10.1016/j.jcss.2007.08.009
• M. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Regev's On Lattices, Learning with Errors, Random Linear Codes, and Cryptography (J. ACM 56(6), 2009, Article 34; doi:10.1145/1568318.1568324) introduced the Learning with Errors (LWE) problem and built a public-key cryptosystem on it. The source for this mission is that published J. ACM article. The paper's main theorem, a quantum reduction from worst-case lattice problems to LWE, is outside this series; this mission formalizes a self-contained piece of finite combinatorics from §5.

In the cryptosystem the public key is a list of $m$ LWE samples, and a bit is encrypted by adding up a uniformly random subset of them. Semantic security rests on one fact: if the public key were truly uniform, the sum of a random subset of it would be close to uniform, so the ciphertext would carry no information about the bit. Claim 5.3 (p. 34:36) makes this precise for an arbitrary finite abelian group $G$. It is a special case of the leftover hash lemma of Impagliazzo and Zuckerman (1989), in which the family of functions $b \mapsto \sum_i b_i g_i$ indexed by $g \in G^l$ is a universal hash family. Variants of the same statement appear in the security proofs of most lattice-based encryption schemes that use random subset sums, including the dual-Regev and GPV-style constructions.

Setting

Let $G$ be a finite abelian group, written additively, with $|G|$ elements, and let $l \ge 0$ be an integer. For $g = (g_1, \dots, g_l) \in G^l$ and $b = (b_1, \dots, b_l) \in \{0,1\}^l$ the subset sum $\sum_i b_i g_i$ is the sum of the $g_i$ with $b_i = 1$ (the empty subset gives $0$). The distribution of the sum of a uniformly random subset of $g_1, \dots, g_l$ is

$$P_g(h) = \frac{1}{2^l}\,\bigl|\{\, b \in \{0,1\}^l \mid \textstyle\sum_i b_i g_i = h \,\}\bigr|, \qquad h \in G.$$

The paper defines the statistical distance of two densities as $\int |\varphi_1 - \varphi_2|$, with range $[0,2]$, and notes that the same definition applies to discrete random variables (p. 34:14). The distance of $P_g$ from the uniform distribution on $G$ is therefore

$$\Delta(g) = \sum_{h \in G} \Bigl| P_g(h) - \frac{1}{|G|} \Bigr|,$$

with no factor $\tfrac12$. Expectations and probabilities over $g$ refer to a uniform choice of $g_1, \dots, g_l \in G$, that is, the uniform distribution on all $|G|^l$ tuples, repetitions allowed: $\mathrm{Exp}_g[F(g)] = |G|^{-l}\sum_{g \in G^l} F(g)$.

In Lean these objects are RegevLWE.SubsetSum.subsetSum, P, statDistUniform and expectG.

Formalization targets

Goal: Claim 5.3

$$\mathop{\mathrm{Exp}}_g\bigl[\Delta(g)\bigr] \le \sqrt{\frac{|G|}{2^l}} \qquad\text{and}\qquad \Pr_g\Bigl[\Delta(g) > \sqrt[4]{|G|/2^l}\Bigr] \le \sqrt[4]{\frac{|G|}{2^l}}.$$

Both sentences of the claim are in the goal. The second is what the security proof (Lemma 5.4, p. 34:37) uses: for all but a $\sqrt[4]{|G|/2^l}$ fraction of public keys, the random subset sum is within $\sqrt[4]{|G|/2^l}$ of uniform. The constants are exactly as printed.

Milestones

1. The $\ell_2$ norm as a collision probability (p. 34:36). For every $g$, with $b, b'$ independent and uniform in $\{0,1\}^l$,

$$\sum_{h} P_g(h)^2 = \Pr_{b,b'}\Bigl[\textstyle\sum_i b_i g_i = \sum_i b'_i g_i\Bigr] \le \frac{1}{2^l} + \Pr_{b,b'}\Bigl[\textstyle\sum_i b_i g_i = \sum_i b'_i g_i \Bigm| b \neq b'\Bigr].$$

2. Collisions of distinct subsets (p. 34:37). For any $b \neq b'$, $\Pr_g[\sum_i b_i g_i = \sum_i b'_i g_i] = 1/|G|$.
3. Expected $\ell_2$ norm (p. 34:37). $\mathrm{Exp}_g[\sum_h P_g(h)^2] \le 1/2^l + 1/|G|$.
4. Cauchy–Schwarz and the $\ell_2$ identity (p. 34:37), pointwise in $g$:

$$\sum_h \Bigl|P_g(h) - \frac{1}{|G|}\Bigr| \le |G|^{1/2}\Bigl(\sum_h \Bigl(P_g(h) - \frac{1}{|G|}\Bigr)^2\Bigr)^{1/2}, \qquad \sum_h \Bigl(P_g(h) - \frac{1}{|G|}\Bigr)^2 = \sum_h P_g(h)^2 - \frac{1}{|G|}.$$

Significance

The result. Claim 5.3 is the step in the security proof of Regev's cryptosystem that removes the public key from the picture: once the key is replaced by uniform samples (by the LWE assumption), the claim shows that an encryption is statistically close to uniform, independently of the encrypted bit. The parameter choice $m \ge (1+\epsilon)(n+1)\log p$ of Lemma 5.4 is exactly what makes $|G|/2^m$ negligible for $G = \mathbb{Z}_p^n \times \mathbb{Z}_p$. Without the claim the cryptosystem would have a hardness assumption but no reduction from it.

Formalizing it. The claim is proved, with a complete argument in the paper; nothing here is open. To our knowledge no machine-checked proof of this statement, or of the leftover hash lemma for subset-sum hash families over a general finite abelian group, exists in Mathlib or on the platform. A formal proof gives a reusable, constant-exact statement of the subset-sum leftover hash lemma with the paper's normalization of statistical distance. The four milestones are standard facts about finite averages and collision probabilities that recur in many cryptographic security proofs.

Difficulty

There is no deep step; the work is in organizing finite counting arguments without loss. Two points need care. The collision fact $\Pr_g[\sum_i b_i g_i = \sum_i b'_i g_i] = 1/|G|$ holds for every pair $b \neq b'$ only because the coefficients $b_i - b'_i$ lie in $\{-1, 0, 1\}$: for a general linear form over a group with torsion, a nonzero coefficient vector need not give a uniformly distributed sum, so an argument that treats the coefficients as arbitrary integers fails. And passing from the $\ell_2$ bound to the expected $\ell_1$ distance requires the exchange of expectation and square root in the right direction (concavity), which is easy to misapply. The bound must hold for every finite abelian group and every $l$, including $l = 0$ and $|G| = 1$, with no asymptotic slack.

Formalization scope

• $G$ is any type with [AddCommGroup G] [Fintype G] [DecidableEq G]; $l : ℕ$, and $l = 0$ is allowed (then $P_g$ is the point mass at $0$ and the claim holds). No hypothesis is added to the paper's statement: $|G| \ge 1$ holds for every group.
• $\{0,1\}^l$ is encoded as Fin l → Bool; $g$ ranges over all functions Fin l → G, so the uniform choice of $g$ is over all $|G|^l$ tuples with repetition, not over $l$-element subsets of $G$.
• Every expectation and probability is an exact finite average with real values: $\mathrm{Exp}_g[F] = |G|^{-l}\sum_g F(g)$, and $\Pr_g[E]$ is the number of tuples satisfying $E$ divided by $|G|^l$. Probabilities over $(b, b')$ are counts over the $(2^l)^2$ pairs; the conditional probability given $b \neq b'$ divides by $(2^l)^2 - 2^l$. At $l = 0$ the paper's conditional probability is undefined; Lean's convention $0/0 = 0$ makes milestone 1 read $1 \le 1$ there, which is consistent with the paper.
• The statistical distance is $\sum_h |P_g(h) - 1/|G||$, without $\tfrac12$. A formalization with the $\tfrac12$-normalized total variation distance would state a weaker result (half the bound) and is excluded. "More than" in the second sentence is strict, "at most" is $\le$. The fourth root is Real.sqrt (Real.sqrt x).
• Milestone 4 states only the first two steps of the paper's final chain (the Cauchy–Schwarz inequality and the identity), pointwise in $g$; the remaining two steps (Jensen for the square root and the substitution of milestone 3) are part of the goal. Its milestone text quotes the whole chain for context.
• No definitions beyond the four above are needed, and no measure theory. Proofs of the milestones, and alternative proofs of the goal (for instance via Fourier analysis on $G$), are welcome.

Selected references

• O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, Journal of the ACM 56(6), Article 34, 2009. doi:10.1145/1568318.1568324
• R. Impagliazzo and D. Zuckerman, How to Recycle Random Bits, Proc. 30th IEEE FOCS, 248–253, 1989. doi:10.1109/SFCS.1989.63486
• J. Håstad, R. Impagliazzo, L. A. Levin and M. Luby, A Pseudorandom Generator from any One-way Function, SIAM Journal on Computing 28(4), 1364–1396, 1999. doi:10.1137/S0097539793244708