Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 25Formalized record≤ 5Open frontier

38 provers on it14 of 16 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 25Formalized record≤ 5Open frontier

38 provers on it14 of 16 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Control Theory Dynamic Programming Operations Research+1·Captain: mikedeng1

Robust Control of Markov Decision Processes with Uncertain Transition Matrices 3: Stationary Policies Suffice and the Stationary/Time-Varying Uncertainty Gap Vanishes GeometricallyResearch Paper

Motivation

A Markov decision process (MDP) is controlled with transition probabilities estimated from data, and optimal policies computed for the estimated model can perform badly when the estimates are off. Robust MDPs replace the single transition model by a set of models and optimize the worst case over that set. Two readings of "the set" are possible. In the stationary uncertainty model, the unknown transition matrices are fixed but unknown; this is the reading that confidence regions from statistics support, but the resulting min–max problem is hard to solve. In the time-varying uncertainty model, an adversary ("nature") may pick different matrices at every stage; this relaxation is solved exactly by robust dynamic programming. Nilim and El Ghaoui (Oper. Res. 2005) solve the second problem in place of the first, and Theorem 4 of their paper justifies the substitution for discounted costs: in the infinite horizon the two readings, and the restriction to stationary controllers, all give the same value, and in the finite horizon the two readings differ by an amount that decays geometrically in the horizon.

Timeline:

1973: Satia and Lave study MDPs with uncertain transition probabilities (Oper. Res. 21).
1994: Puterman's monograph collects the nominal theory, including the optimality of stationary deterministic policies for discounted finite MDPs (Wiley).
2001: Bagnell, Ng and Schneider state a robust Bellman recursion for stationary games without proof (CMU-RI-TR-01-25).
2005: Iyengar (Math. Oper. Res. 30) and Nilim and El Ghaoui independently prove the robust Bellman recursion under rectangular uncertainty; Nilim and El Ghaoui add Theorem 4.
2013: Wiesemann, Kuhn and Rustem extend robust MDPs beyond rectangular sets (Math. Oper. Res. 38).

Setting

States form a finite set $\mathcal X = \{0,\dots,n-1\}$ and actions a finite nonempty set $\mathcal A$ . A stage cost $c(i,a)\ge 0$ is given for every state and action, together with a discount factor $0<\nu<1$ and an initial state $i_0$ . For every action $a$ and state $i$ a nonempty set $\mathcal P_i^a$ of probability vectors in the simplex $\Delta_n$ is given: the possible rows of the transition matrix $P^a$ . Rectangularity means that every row is chosen independently: one stage of nature is a family $(P^a)_{a\in\mathcal A}$ with $i$ -th row of $P^a$ in $\mathcal P_i^a$ , and the set of such families is $\mathcal Q$ .

A controller policy $\pi=(\mathbf a_0,\mathbf a_1,\dots)$ assigns an action $\mathbf a_t(i)$ to each state at each stage; the set of all of them is $\Pi$ , and the stationary ones (the same map at every stage) form $\Pi_s$ . A nature policy $\tau=(P_t^a)$ picks one element of $\mathcal Q$ per stage; the set is $\mathcal T$ , and the stationary ones form $\mathcal T_s$ . Starting from $\mu_0 = e_{i_0}$ , the state law evolves by $\mu_{t+1}(j)=\sum_i \mu_t(i)P_t^{\mathbf a_t(i)}(i,j)$ . The discounted costs over horizon $N$ and over the infinite horizon are

C_N(\pi,\tau)=\sum_{t=0}^{N-1}\nu^t\sum_i\mu_t(i)\,c(i,\mathbf a_t(i)),\qquad C_\infty(\pi,\tau)=\lim_{N\to\infty}C_N(\pi,\tau).

For a controller class $\mathcal C\in\{\Pi,\Pi_s\}$ and a nature class $\mathcal S\in\{\mathcal T,\mathcal T_s\}$ the robust values are $\phi_\infty(\mathcal C,\mathcal S)=\inf_{\pi\in\mathcal C}\sup_{\tau\in\mathcal S}C_\infty(\pi,\tau)$ and $\phi_N(\Pi,\mathcal S)=\inf_{\pi\in\Pi}\sup_{\tau\in\mathcal S}C_N(\pi,\tau)$ . Finally $c_{\max}=\max_{i,a}c(i,a)$ and $\varepsilon_N=\nu^Nc_{\max}/(1-\nu)$ .

Formalization targets

Goal: Theorem 4 (p. 786)

\phi_\infty(\Pi,\mathcal T)=\phi_\infty(\Pi_s,\mathcal T_s)=\phi_\infty(\Pi_s,\mathcal T)=\phi_\infty(\Pi,\mathcal T_s),

0\le \phi_N(\Pi,\mathcal T)-\phi_N(\Pi,\mathcal T_s)\le \frac{\nu^N c_{\max}}{1-\nu}\quad\text{for every }N .

The second line is the paper's "the gap goes to zero at a geometric rate $\nu$ ", with the constant the paper's own argument produces.

Milestones (proof order of the paper)

Eq. (34): $C_N(\pi,\tau)\le C_\infty(\pi,\tau)\le C_N(\pi,\tau)+\varepsilon_N$ for all $\pi\in\Pi$ , $\tau\in\mathcal T$ , $N$ .
Eq. (35): $\phi_N(\Pi,\mathcal T)\le\phi_\infty(\Pi,\mathcal T)\le\phi_N(\Pi,\mathcal T)+\varepsilon_N$ .
Step (e): the same sandwich for $\phi_N(\Pi,\mathcal T_s)$ and $\phi_\infty(\Pi,\mathcal T_s)$ .
Eq. (33): for every $\varepsilon>0$ and all large $N$ , $\phi_\infty(\Pi_s,\mathcal T_s)-\varepsilon\le\phi_N(\Pi,\mathcal T)\le\phi_\infty(\Pi_s,\mathcal T_s)$ .
Step (c): for every stationary $\pi$ , $\sup_{\tau\in\mathcal T}C_\infty(\pi,\tau)=\sup_{\tau\in\mathcal T_s}C_\infty(\pi,\tau)$ , hence $\phi_\infty(\Pi_s,\mathcal T)=\phi_\infty(\Pi_s,\mathcal T_s)$ .
Step (d), nominal fact: for stationary $\tau$ , $\inf_{\pi\in\Pi}C_N(\pi,\tau)\to\inf_{\pi\in\Pi_s}C_\infty(\pi,\tau)$ .
Step (d): $\phi_\infty(\Pi,\mathcal T_s)=\phi_\infty(\Pi_s,\mathcal T_s)$ .

Significance

The first half of Theorem 4 says that, for discounted robust MDPs with rectangular uncertainty, nothing is gained by either player from non-stationary behaviour: the controller may restrict itself to stationary deterministic policies and nature's time variation buys it nothing. This is what makes the stationary game (6), solved by the robust Bellman recursion of Theorem 3, the right infinite-horizon object. The second half is a quantitative guarantee for practitioners: solving the tractable time-varying problem (4) instead of the statistically motivated but hard stationary problem (3) costs at most $\nu^Nc_{\max}/(1-\nu)$ in value.

The result is proved on paper. As far as a search of the platform shows (September 2026), no robust MDP result has a machine-checked proof here; the nominal counterpart, optimality of stationary policies for discounted finite MDPs, is on the platform as BertsekasDP.discounted_main_theorem in a different model encoding (state-dependent control sets). A complete development contributes a reusable encoding of robust MDPs with time-varying and stationary adversaries, the truncation estimates for discounted costs, and a formal record of one step whose printed argument is incomplete (Step (d), see Difficulty).

Difficulty

The truncation estimates (34), (35) and Step (e) are elementary. The equalities in (31) are not: they compare values of games whose players have infinite-dimensional strategy sets, and the paper writes "min" and "max" where the infima and suprema need not be attained, since the row sets are neither closed nor convex. Two steps of the printed proof rely on results the mission does not import. Step (a) identifies $\phi_N(\Pi,\mathcal T)$ with iterates of the robust Bellman recursion, which is Theorems 1 and 3 of the paper (formalized in sibling missions of this series). Step (c) says only "following similar steps as in Step (a)". Step (d) is incomplete as printed: it shows that for each fixed stationary nature the controller's best time-varying and best stationary responses agree, which is a statement about a max–min value, whereas $\phi_\infty(\Pi,\mathcal T_s)$ is a min–max value. The obvious attempt to exchange the infimum over $\Pi$ with the supremum over $\mathcal T_s$ from that per-nature fact alone fails; the exchange requires a duality statement for the stationary game.

Formalization scope

States are Fin n; the action type is finite and nonempty. The row sets are an arbitrary family rows a i ⊆ stdSimplex ℝ (Fin n) with each set nonempty; nonemptiness is implicit in the paper and explicit here, and no convexity or closedness is assumed. A stage of nature is the subtype of families A → Fin n → (Fin n → ℝ) whose rows lie in the given sets, so rectangularity is built in. Controller policies are sequences ℕ → Fin n → A, nature policies sequences of stage choices; stationary policies of either player are the constant sequences. $C_N$ is defined from the forward state distribution (not from a Bellman recursion) and reads only stages $<N$ , so the finite-horizon values over infinite sequences are exactly the paper's values (3) and (4) with stage costs $\nu^tc$ and zero terminal cost. $C_\infty$ is the sum of the series of nonnegative stage costs, which converges for $0\le\nu<1$ and equals $\lim_N C_N$ . Every min and max of the paper is a real infimum ⨅ or supremum ⨆; all families are nonempty and lie in $[0,c_{\max}/(1-\nu)]$ , and attainment is not assumed anywhere. The discount factor satisfies $0<\nu<1$ , as in §4 of the paper.

The rate in the goal is the explicit bound $\nu^Nc_{\max}/(1-\nu)$ ; a formalization stating only that the gap tends to zero, or stating (31) with the infinite-horizon cost replaced by a Bellman fixed point, proves a different theorem and is not accepted.

A complete development needs: the stochastic-matrix facts for the forward distribution, geometric-series bounds, robust value iteration for the time-varying and the stationary adversary, and nominal stationarity of discounted MDPs. The model and truncation estimates are reusable for any discounted robust MDP result. Contributions of any milestone, and of proofs of Step (c) and Step (d) by any route, are welcome.

Selected references

A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887
J. K. Satia, R. E. Lave, Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
J. A. Bagnell, A. Y. Ng, J. Schneider, Solving Uncertain Markov Decision Processes, Technical Report CMU-RI-TR-01-25, Carnegie Mellon University, 2001.
W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov Decision Processes, Mathematics of Operations Research 38(1):153–183, 2013. https://doi.org/10.1287/moor.1120.0566

10 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

A Linear-Time Algorithm for Finding a Sparse k-Connected Spanning Subgraph of a k-Connected Graph 2: FOREST's Forests E_i Preserve Local Node-Connectivity up to i in a Simple GraphResearch Paper

Motivation

Given a $k$ -connected graph, many connectivity algorithms run in time that grows with the number of edges $|E|$ . A sparse certificate is a spanning subgraph with only $O(k|V|)$ edges that is still $k$ -connected; computing one first and running the expensive algorithm on it replaces $|E|$ by $k|V|$ in the bound. Finding a $k$ -connected spanning subgraph with the minimum number of edges is NP-complete for every fixed $k \ge 2$ (Garey and Johnson, problem GT31), so the question is how cheaply a sparse, not necessarily minimum, certificate can be found.

Nagamochi and Ibaraki (Algorithmica 7 (1992) 583–596) answered this with a single linear-time scanning procedure, FOREST, which partitions the edges into classes $E_1, E_2, \dots, E_{|E|}$ . They showed that the prefix unions $E_1 \cup \dots \cup E_k$ are certificates for edge-connectivity and, for simple graphs, for node-connectivity. The node-connectivity result is the subject of this mission; the edge-connectivity result is the preceding mission of this series.

Timeline:

1980: Galil gives an algorithm testing $\kappa(G) \ge k$ whose running time depends on $|E|$ (SIAM J. Comput. 9).
Before 1992 (as cited on p. 583): Suzuki et al. give $O(|E|)$ -time algorithms for sparse 2- and 3-node-connected spanning subgraphs; Nishizeki and Poljak find, for general $k$ , a $k$ -node-connected spanning subgraph with at most $k(|V|-1)$ edges in $O(|V|^{1/2}|E|^2)$ time.
1992: Nagamochi and Ibaraki prove that FOREST, which runs in $O(|V| + |E|)$ time, yields a $k$ -node-connected spanning subgraph $G_k$ of every simple $k$ -node-connected graph, with $|E(G_k)| \le k|V| - k(k+1)/2$ . Their Theorem 3.1 states a stronger, local form.
1993: Cheriyan, Kao and Thurimella isolate "scan-first search" as the general principle behind such certificates (SIAM J. Comput. 22 (1993)).

Setting

A graph $G = (V, E)$ has a finite node set $V$ with $|V| \ge 2$ and a finite edge set $E$ ; each edge has an unordered pair of two distinct end nodes. In this mission the graph is simple: no two edges have the same end nodes. For $F \subseteq E$ , $(V, F)$ is the spanning subgraph with edge set $F$ .

The local node-connectivity $\kappa(x, y; H)$ of nodes $x, y$ in a graph $H$ on $V$ is $|V| - 1$ if $x$ and $y$ are adjacent in $H$ , and otherwise the minimum size of a node set $W \subseteq V - \{x, y\}$ whose deletion leaves no $x$ – $y$ path. The node connectivity is $\kappa(G) = \min_{x, y} \kappa(x, y; G)$ .

Procedure FOREST keeps a label $r(v) \ge 0$ on each node, initially $0$ . While some node is unscanned, it chooses an unscanned node $x$ of largest label; for each unscanned edge $e = (x, y)$ it puts $e$ into the class $E_{r(y)+1}$ , increases $r(x)$ by one if $r(x) = r(y)$ , and increases $r(y)$ by one; then it marks $x$ scanned. Ties are broken arbitrarily. The time instants are the states between these elementary operations; $E^*_i$ denotes the class $i$ at an instant, and $E_i$ its final value. Put

G_i = (V,\ E_1 \cup E_2 \cup \dots \cup E_i).

Formalization targets

Goal: Theorem 3.1

For a simple graph $G$ and the classes of any completed run of FOREST, for $1 \le i \le |E|$ ,

\kappa(x, y; G_i) \ \ge\ \min\{\kappa(x, y; G),\ i\} \qquad \text{for any } x, y \in V. \tag{3.1}

The statement is local: it holds pair by pair, not only for the global minimum, and for every tie-breaking of the procedure.

Milestones, in the order the proof uses them

Lemma 2.2: at every instant, a node $v$ meets $E_i$ exactly for $i = 1, \dots, r(v)$ .
Lemma 2.4(b): at every instant, a $u$ – $v$ path in $E^*_j$ yields $u$ – $v$ paths in every $E^*_i$ , $i < j$ .
In-degree at most one (§2, p. 588): orienting each edge from the earlier-scanned to the later-scanned end, every node has at most one entering arc in each class.
Lemma 3.1: if an $x$ – $y$ path of $E^*_j$ has the form $x, u_1, \dots, u_k = w, y$ with $k = 1$ or $u_1$ scanned before $w$ , then any $w$ – $x$ and $w$ – $y$ paths in $E^*_i$ ( $i < j$ ) share a node other than $w$ .
Lemma 3.2: for a node cut set $W = \{w_1, \dots, w_i\}$ of $G_{i+1}$ (in scan order) separating a component $X$ from the rest $Y$ , immediately after $w_t$ is scanned every $X$ – $Y$ path of $E^*_t$ passes through $w_t$ , and $E^*_j$ has no $X$ – $Y$ path for $t + 1 \le j \le i + 1$ .

A companion item states the paper's announcement in §3: $G_k$ is $k$ -node-connected for every $1 \le k \le \kappa(G)$ .

Significance

Theorem 3.1 at $i = k$ shows that the first $k$ classes of FOREST form a $k$ -node-connected spanning subgraph whenever $G$ is, and the edge-count analysis of the companion mission bounds its size by $k|V| - k(k+1)/2$ . Since FOREST runs in linear time, any algorithm testing $\kappa(G) \ge k$ can be run on $G_k$ instead of $G$ ; the paper uses this to improve the bound for testing $\kappa(G) \ge k$ from $O(\max\{k^2|V|^{1/2}, k|V|\}|E|)$ to $O(\max\{k^3|V|^{3/2}, k^2|V|^2\})$ , and similar gains for computing the number of node-disjoint paths between two nodes. The local form (3.1) is what makes the $s$ – $t$ applications possible.

The result is proved on paper. As far as a search of the platform shows, neither FOREST nor local node-connectivity has a machine-checked treatment there; Mathlib has no notion of vertex connectivity of a pair of nodes. This mission produces a formal model of FOREST as a nondeterministic transition system and the statements needed to verify the paper's proof step by step.

Difficulty

For edge-connectivity the analogous statement follows from a general principle: any sequence of maximal spanning forests, each taken in what remains of the graph, preserves local edge-connectivity up to its length. The obvious attempt is to prove (3.1) the same way, from the fact that each $E_i$ is a maximal spanning forest of what the earlier classes leave. The paper gives no such argument for node-connectivity: its proof uses the specific scan order of FOREST in an essential way, through the orientation of edges from earlier- to later-scanned nodes and the in-degree bound of that orientation (Lemmas 3.1 and 3.2). The argument tracks, for a hypothetical node cut $W$ of size $i$ in $G_{i+1}$ , the classes at the moments the nodes of $W$ are scanned, which requires reasoning about intermediate states of the algorithm and about paths in several classes at once. None of this reduces to a static property of the output partition.

Formalization scope

Graphs. A node type V and an edge type E, both finite, with ends : E → Sym2 V; loop-freeness is ∀ e, ¬ (ends e).IsDiag and simplicity is Function.Injective ends. The standing assumptions of p. 583 and p. 589 ( $|V| \ge 2$ , no self-loop, a simple graph when node-connectivity is discussed) appear as hypotheses; §2 items are stated for loopless graphs, as on the page.
Connectivity. $\kappa(x, y; (V, F))$ is valued in $\mathbb N_\infty$ : $|V| - 1$ on adjacent pairs, the minimum node cut otherwise, and $\top$ when $x = y$ , where (3.1) holds trivially.
FOREST. A nondeterministic step relation with three steps (select, scan, finish), a run of length $K$ from the initial state, and completion when every node is scanned. Every tie-breaking is allowed, so the theorems quantify over all completed runs. A time instant is a state of a run; "scanned before" compares positions in the run's selection order; "immediately after $w_t$ has been scanned" is the state right after the finish step of $w_t$ .
Excluded. The running time " $O(|V| + |E|)$ " and everything in §4 (the connectivity-testing algorithms and their bounds) are not stated: the paper fixes no machine model. The edge bounds on $|E_i|$ belong to the edge-connectivity mission.
Ruled out. Stating (3.1) for an arbitrary partition into maximal spanning forests, or reading the classes $E^*_j$ of Lemmas 3.1–3.2 off the final state, would state a different theorem from the one the paper proves; the classes are those of a run of FOREST at the instant the page specifies.
Infrastructure. Reachability avoiding a node set, walks and paths in SimpleGraph, and invariants of the FOREST transition system. The definitions duplicate those of the edge-connectivity mission by design and are candidates for a shared layer. Contributions of general lemmas about the run (label invariants, monotonicity of classes along a run) are welcome.

Selected references

H. Nagamochi, T. Ibaraki, A linear-time algorithm for finding a sparse $k$ -connected spanning subgraph of a $k$ -connected graph, Algorithmica 7 (1992), 583–596. https://doi.org/10.1007/BF01758778
Z. Galil, Finding the vertex connectivity of graphs, SIAM J. Comput. 9 (1980), 197–199. https://doi.org/10.1137/0209016
J. Cheriyan, M.-Y. Kao, R. Thurimella, Scan-first search and sparse certificates: an improved parallel algorithm for $k$ -vertex connectivity, SIAM J. Comput. 22 (1993), 157–174. https://doi.org/10.1137/0222013
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979.

9 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

A Linear-Time Algorithm for Finding a Sparse k-Connected Spanning Subgraph of a k-Connected Graph 1: The FOREST Decomposition Preserves Local Edge-ConnectivityResearch Paper

Motivation

Many graph algorithms for connectivity questions run in time proportional to the number of edges. When the question is only whether a graph is $k$ -edge-connected, or what its local edge-connectivities are up to a threshold $k$ , most edges are irrelevant: a spanning subgraph with $O(k|V|)$ edges already carries the answer. Such a subgraph is called a sparse certificate. Computing one first and running the expensive algorithm on it replaces $|E|$ by $k|V|$ in the running time of connectivity testing, of Matula-type edge-connectivity algorithms, and of $s$ – $t$ flow computations used as connectivity oracles.

Nagamochi and Ibaraki (Algorithmica 7, 1992) gave a procedure, FOREST, that computes such a certificate for edge-connectivity and, on simple graphs, for node-connectivity, with a single graph search. The same partition of the edges into forests is the engine of their deterministic minimum-cut algorithm for multigraphs (SIAM J. Discrete Math. 5, 1992), which later became the maximum-adjacency ordering of the Stoer–Wagner minimum-cut algorithm (J. ACM 44, 1997).

Timeline:

1927: Menger identifies the minimum number of edges separating two nodes with the maximum number of edge-disjoint paths between them.
1992: Nagamochi and Ibaraki publish Procedure FOREST and prove that its $i$ -th prefix preserves local edge-connectivity up to $i$ in multigraphs, and local node-connectivity up to $i$ in simple graphs.
1993: Cheriyan, Kao and Thurimella (SIAM J. Comput. 22) obtain sparse certificates by scan-first search; Frank, Ibaraki and Nagamochi (J. Graph Theory 17) give a shorter proof for the node-connectivity case.
1994: Nishizeki and Poljak (Discrete Appl. Math. 55) publish the forest-decomposition lemma (Lemma 2.1 below), found independently.

Setting

A graph $G = (V, E)$ is finite and undirected, has $|V| \ge 2$ nodes, may have multiple edges (several edges with the same pair of end nodes), and has no self-loop. It is simple if no two edges have the same end nodes. For $F \subseteq E$ , $(V, F)$ is the spanning subgraph with edge set $F$ . It is a forest if it has no cycle; two parallel edges form a cycle. It is a maximal spanning forest in $(V, H)$ , for $F \subseteq H$ , if adding any edge of $H \setminus F$ to $F$ creates a cycle.

The local edge-connectivity $\lambda(x, y; H)$ is the minimum number of edges of $H$ whose removal leaves no path from $x$ to $y$ ; parallel edges count separately. It is $\infty$ when $x = y$ .

Procedure FOREST keeps a label $r(v) \in \mathbb{N}$ on every node, initially $0$ , and classes $E_1, E_2, \dots, E_{|E|}$ , initially empty. While an unscanned node exists, it picks an unscanned node $x$ of largest label; for every unscanned edge $e$ from $x$ to a node $y$ , it puts $e$ into $E_{r(y)+1}$ , increases $r(x)$ by one if $r(x) = r(y)$ , increases $r(y)$ by one, and marks $e$ scanned; then it marks $x$ scanned. Ties among nodes and the order of edges are free. On termination, $G_i = (V, E_1 \cup \cdots \cup E_i)$ .

Formalization targets

Goal: Theorem 2.1 (pp. 588–589), without the running time

For every graph $G$ and every completed execution of FOREST on $G$ :

every edge lies in exactly one class $E_i$ , $1 \le i \le |E|$ ;
for $i = 1, \dots, |E|$ ,

\lambda(x, y; G_i) \ge \min\{\lambda(x, y; G),\ i\} \qquad \text{for all } x, y \in V; \tag{2.1}

$|E_i| \le |V| - 1$ for all $i$ ;
if $G$ is simple, $|E_i| \le |V| - i$ for $i \le |V| - 1$ and $E_i = \emptyset$ for $i \ge |V|$ .

Milestones

Lemma 2.2 (p. 587): during the execution, a node $v$ has incident edges in exactly the classes $E_1, \dots, E_{r(v)}$ .
Lemma 2.3 (p. 587): each $(V, E_i)$ is a forest at every instant.
Lemma 2.4 (p. 588): (a) an edge $(u, v)$ added to $E_i$ has its end nodes joined by a path in $E_{i-1}$ ; (b) a path in $E_j$ between $u$ and $v$ yields a path in every $E_i$ , $i < j$ .
Lemma 2.5 (p. 588): each output $(V, E_i)$ is a maximal spanning forest in $G - E_1 \cup \cdots \cup E_{i-1}$ .
Lemma 2.1 (p. 584): any sequence of successive maximal spanning forests satisfies (2.1).

Companions

the sparse certificate (p. 589): if $\lambda(x, y; G) \ge k$ for all $x, y$ , then $G_k$ is $k$ -edge-connected with $|E(G_k)| \le k(|V| - 1)$ , and $|E(G_k)| \le k|V| - k(k+1)/2$ for simple $G$ ;
Lemma 2.6 (p. 589): for $k \le \delta(G)$ , $G_k$ has a node of degree exactly $k$ .

Significance

(2.1) says that one search produces, for every threshold $k$ at once, a subgraph with at most $k(|V|-1)$ edges that keeps every local edge-connectivity up to $k$ . Any algorithm whose running time grows with $|E|$ can then be run on $G_k$ in place of $G$ ; §4 of the paper uses this to speed up $k$ -connectivity tests and the computation of local connectivities. The same forest partition is the structural fact behind the Nagamochi–Ibaraki and Stoer–Wagner minimum-cut algorithms. Lemma 2.6 shows that the certificate is tight: its edge-connectivity is exactly $k$ when $\lambda(G) \ge k$ .

The results are proved in the paper. No machine-checked proof of them is known. Formalizing them means formalizing a graph search with free tie-breaking as a transition system, reasoning about invariants of all its executions, and proving a cut-counting statement for multigraphs. Mathlib's connectivity notions, such as SimpleGraph.IsEdgeReachable, do not see parallel edges, so the multigraph cut theory here is new.

Difficulty

Lemma 2.1 is a short cut argument once maximality is available. The difficulty is showing that FOREST, which assigns each edge to a class by looking only at the label of one end node, produces maximal forests in the successive residual graphs (Lemma 2.5). The obvious invariant, that the class of an edge is the first forest it does not close a cycle in, is not what line 7 computes. The label $r(y)$ records only which classes touch $y$ , not which component of each class contains $y$ . The paper's argument needs Lemma 2.4(a): at the moment an edge is added to $E_i$ its ends already lie in one tree of $E_{i-1}$ . That relies on the choice of the unscanned node of largest label, on the order of lines 8 and 9, and on an argument about the scan order of tree roots.

Formalization scope

Graphs. A graph is a finite node type V with $|V| \ge 2$ , a finite edge type E, and ends : E → Sym2 V with no diagonal value (no self-loops). Parallel edges are distinct elements of E. Simplicity is injectivity of ends, and edge subsets are Finset E. A forest is an edge set in which every edge is a bridge, a condition that sees parallel edges.
Connectivity. $\lambda$ is an infimum in ℕ∞ over separating edge sets, $\infty$ at $x = y$ . (2.1) is kept "for all $x, y$ ", as printed.
FOREST. FOREST is a nondeterministic step relation (select, scan, finish) on explicit states: labels, class index per edge ( $0$ = unscanned), scanned nodes, current node and selection order. The theorems quantify over every run from the initial state, so no tie-breaking rule is fixed. "At some time instant" is a state of the run; "upon completion" is a run whose last state has every node scanned. Lemma 2.2 is stated at every state, not only after a scan block (the other steps change neither labels nor classes). Lemma 2.4(a) assumes $i \ge 2$ , since $E_0$ does not exist.
Exclusions. Theorem 2.1's clause "is found in $O(|V| + |E|)$ time", the bucket implementation, and the time bound of the certificate are not formalized: the paper fixes no machine model. The goal consists of the structural conclusions only. The bound printed "if $G$ is multiple" is stated for every loopless graph.
Non-triviality. The goal is about the classes of a run of FOREST. An arbitrary partition of $E$ into maximal spanning forests is Lemma 2.1's hypothesis, not a formalization of Theorem 2.1. A statement in which the classes are unconstrained variables, or in which the run hypotheses cannot be met, would be trivial. A separate sanity file checks that a complete run on the triangle $K_3$ exists and attains $|E_1| = |V| - 1$ , $|E_2| = |V| - 2$ .
Welcome contributions. Useful reusable infrastructure includes:
- a cut and Menger layer for finite multigraphs;
- forest and bridge lemmas for edge-indexed graphs;
- invariant-style reasoning over runs.

Selected references

H. Nagamochi, T. Ibaraki, A linear-time algorithm for finding a sparse $k$ -connected spanning subgraph of a $k$ -connected graph, Algorithmica 7 (1992) 583–596. https://doi.org/10.1007/BF01758778
H. Nagamochi, T. Ibaraki, Computing edge-connectivity in multigraphs and capacitated graphs, SIAM J. Discrete Math. 5 (1992) 54–66. https://doi.org/10.1137/0405004
T. Nishizeki, S. Poljak, $k$ -connectivity and decomposition of graphs into forests, Discrete Appl. Math. 55 (1994) 295–301. https://doi.org/10.1016/0166-218X(94)90014-0
J. Cheriyan, M.-Y. Kao, R. Thurimella, Scan-first search and sparse certificates: an improved parallel algorithm for $k$ -vertex connectivity, SIAM J. Comput. 22 (1993) 157–174. https://doi.org/10.1137/0222013
A. Frank, T. Ibaraki, H. Nagamochi, On sparse subgraphs preserving connectivity properties, J. Graph Theory 17 (1993) 275–281. https://doi.org/10.1002/jgt.3190170302
M. Stoer, F. Wagner, A simple min-cut algorithm, J. ACM 44 (1997) 585–591. https://doi.org/10.1145/263867.263872

10 thms3 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming XI: The Cut-Generating LP Under a Ray NormalizationTextbook

Motivation

Lift-and-project (L&P) cuts strengthen the linear relaxation of a mixed 0-1 program by separating a fractional point from the convex hull of a disjunction such as $x_k \le 0 \lor x_k \ge 1$ . Generating an optimal L&P cut means solving the cut-generating linear program (CGLP), a linear program lifted to a space with one new pair of variables per constraint of the original tableau — considerably larger than the tableau itself. Balas and Bonami showed that this higher-dimensional LP need not be solved explicitly at all: an optimal (or near-optimal) L&P cut can instead be produced by ordinary simplex pivots in the original LP tableau, each such pivot implicitly performing an entire block of pivots in the CGLP (E. Balas and P. Bonami, Generating lift-and-project cuts from the LP simplex tableau: open source implementation and testing of new variants, Mathematical Programming Computation 1 (2009), 165–199, https://doi.org/10.1007/s12532-009-0006-4). This correspondence is what made L&P cuts practical in commercial solvers: Perregaard's implementation in XPRESS needed only 5% of the iterations and 1.5% of the time of solving the CGLP explicitly, and Bonami's public implementation in COIN-OR put the method within reach of any solver.

A second, independent line of work asks how the CGLP's feasible region should be normalized. The textbook normalization (fixing the sum of the CGLP multipliers to $1$ ) is scale-dependent — rescaling one constraint of the original system changes which cut the CGLP returns — so Balas and Perregaard proposed the ray normalization $\alpha y = 1$ instead (E. Balas and M. Perregaard, Lift-and-project for mixed 0-1 programming: recent progress, Discrete Applied Mathematics 123 (2002), 129–154, https://doi.org/10.1016/S0166-218X(01)00340-7). Under this normalization the CGLP's optimal value has a clean geometric meaning: it is exactly the distance, measured along a fixed ray from the point being separated, to the convex hull of the disjunctive set. This mission formalizes both results: the pivot correspondence (Theorem 10.1) and the optimal-value characterization under the ray normalization (Theorem 10.2, Theorem 10.3, and Corollary 10.4).

Setting

Fix a finite index set $M$ for the rows of a simplex tableau over $n$ variables, a matrix $A \in \mathbb R^{M \times n}$ , and a right-hand side $b : M \to \mathbb R$ , so that the tableau reads $A x \ge b$ (a "tilde" is dropped from the informal $\tilde A, \tilde b$ notation for the optimal-basis tableau of the linear relaxation). A basis is an injection $\iota : \mathrm{Fin}\, n \to M$ picking out $n$ of the rows; write $\hat A$ for the $n \times n$ submatrix $\hat A_{ij} = A_{\iota(i), j}$ and $\hat b$ for the corresponding subvector. From these, the standard tableau quantities are read off: $\bar a_{k0} := e_k \hat A^{-1} \hat b$ , $\bar a_{kj} := -(\hat A^{-1})_{kj}$ , and the surplus of row $i \in M$ at a point $x$ , $\mathrm{Surplus}_i(x) := (Ax - b)_i$ .

Fix a distinguished row $k$ with a fractional basic variable, and a candidate pivot row $i \ne k$ . For $\ell$ ranging over the nonbasic columns $J$ , set $\gamma_\ell := -\bar a_{k\ell}/\bar a_{i\ell}$ ; this is the value of a parameter $\gamma$ at which the combined source row

x_k + \gamma x_i + \sum_{j \in J} (\bar a_{kj} + \gamma \bar a_{ij}) x_j = \bar a_{k0} + \gamma \bar a_{i0} \tag{10.1$_\gamma$}

has its $j$ -th coefficient pass through $0$ . The simple disjunctive cut obtained by applying the split disjunction $z \le 0 \lor z \ge 1$ (where $z$ is the left side of (10.1 $_\gamma$ )) to this row is the object CombinedCutSet.

On the CGLP side, $(\mathrm{CGLP})_k$ is the cut-generating LP associated with the disjunction $-x_k \ge 0 \lor x_k \ge 1$ from Chapter 8: it has one pair of nonnegative multiplier variables $(u_\rho, v_\rho)$ per row $\rho \in M$ , plus $u_0, v_0 \ge 0$ , tied together by the normalization $\sum_\rho u_\rho + u_0 + \sum_\rho v_\rho + v_0 = 1$ , and its feasible solutions $(\alpha, u, u_0, v, v_0, \beta)$ correspond exactly to valid cuts $\alpha x \ge \beta$ for the disjunction. A basic feasible solution to $(\mathrm{CGLP})_k$ is described by a valid partition $(M_1, M_2)$ of the nonbasic rows, with $u_\rho = 0$ off $M_1$ and $v_\rho = 0$ off $M_2$ .

Separately, fix a disjunctive set and write $P_D \subseteq \mathbb R^n$ for its convex hull — the object every cut ultimately wants to separate a point from. For a fixed direction $y \in \mathbb R^n$ and point $\bar x \in \mathbb R^n$ , $(\mathrm{CGLP})_y$ is the cut-generating LP under the ray normalization: pairs $(\alpha, \beta)$ with $\alpha x \ge \beta$ valid for every $x \in P_D$ and $\alpha y = 1$ , minimizing the objective $\alpha \bar x - \beta$ .

Formalization targets

Theorem 10.1. For a genuine ordered pivot chain $j_1, \dots, j_t$ inside $J$ (no repeats, each consecutive pair flipping the sign of $\bar a_{k,\cdot}$ as $\gamma$ increases — rule (b) of the theorem), the simple disjunctive cut from the combined row at $\gamma = \gamma_{j_t}$ equals the lift-and-project cut $\{x : \beta \le \alpha x\}$ associated with a basic feasible solution to $(\mathrm{CGLP})_k$ for the resulting basis $J' := (J \cup \{i\}) \setminus \{j_t\}$ :

\mathrm{CombinedCutSet}(k, i, J, \gamma_{j_t}) = \{x : \beta \le \alpha x\}.

Theorem 10.2. If $(\mathrm{CGLP})_y$ is feasible, it has a finite minimum if and only if the ray meets the disjunctive hull:

\text{finite min} \iff \exists\, \lambda \in \mathbb R,\ \bar x + \lambda y \in P_D.

Theorem 10.3 (goal). If $(\mathrm{CGLP})_y$ has an optimal solution $(\tilde\alpha, \tilde\beta)$ , its optimal value is exactly the signed distance to $P_D$ along the ray, and the corresponding boundary point lies exactly on the optimal hyperplane:

\bar x^{\mathsf T} \tilde\alpha - \tilde\beta = \lambda^* := \min\{\lambda : \bar x + \lambda y \in P_D\}, \qquad (\bar x + \lambda^* y)^{\mathsf T} \tilde\alpha = \tilde\beta.

Corollary 10.4. Taking $y := x^* - \bar x$ for a point $x^*$ in the lifted polyhedron $P_Q$ gives an optimal solution whose hyperplane separates $\bar x$ and meets the segment $(\bar x, x^*]$ at the point closest to $x^*$ .

The targets are ordered from the purely combinatorial pivot correspondence (10.1, independent of the ray normalization) through the abstract feasibility/boundedness dichotomy (10.2) to the concrete value formula that is this mission's goal (10.3), with the geometric illustration (10.4) as a companion result using the same machinery with a specific choice of ray.

Significance

Theorem 10.1 is the theoretical justification for every commercial L&P-cut implementation cited above: it says the pivot correspondence is not an approximation or a heuristic shortcut but an exact identity between a single LP pivot and a specific, describable sequence of CGLP pivots, which is what lets a solver generate an (quasi-)optimal L&P cut at the cost of ordinary simplex pivots instead of solving a much larger LP. Theorem 10.3 gives the ray-normalized CGLP an exact geometric meaning — its value is a distance, not merely a linear-programming optimum — which is what makes the ray normalization the more robust alternative to the scale-dependent constant-sum normalization used elsewhere in the book (§9), and is the basis for the geometric picture (Corollary 10.4, Fig. 10.3) of how a lift-and-project cut relates to the lifted polyhedron $P_Q$ .

Both directions are proved in the source text (Balas and Bonami 2009 for Theorem 10.1; Balas and Perregaard 2002 for Theorems 10.2/10.3 and Corollary 10.4) but have no formalized counterpart on this platform: no existing item treats cut-generating LPs, ray normalizations of a projection cone, or the correspondence between two different pivoting processes. This mission produces the first Lean statements of both.

Difficulty

The obvious temptation for Theorem 10.1 is to existentially weaken "the sequence of $t$ pivots defined as follows" to "there exists some sequence of pivots realizing the same cut" — which would be true but not what the theorem says, and would erase the entire content that makes the result useful (an algorithm, not just an existence claim). The formalization instead carries the explicit ordered chain j1 :: middle ++ [jt] as data, with the three-part construction (rules (a), (b), (c)) encoded as hypotheses on that specific list via List.IsChain, so the theorem proved is the constructive one the book states, not a weaker existential shadow of it.

For Theorem 10.3, the proof pattern in the book resists a shortcut: showing $\lambda_0 = \lambda^*$ requires deriving a contradiction from each strict inequality ( $\lambda_0 > \lambda^*$ violates optimality of the point on $P_D$ 's boundary; $\lambda_0 < \lambda^*$ contradicts optimality of $(\tilde\alpha, \tilde\beta)$ for $(\mathrm{CGLP})_y$ via a competing separating hyperplane), so there is no way to avoid formalizing both directions of the boundedness dichotomy already needed for Theorem 10.2 first.

Formalization scope

The ambient space is $\mathrm{Fin}\ n \to \mathbb R$ throughout, matching the rest of the series. $(\mathrm{CGLP})_y$ 's feasibility (IsCGLPYFeasible) is stated directly as validity of $(\alpha, \beta)$ for $P_D$ under $\alpha y = 1$ , not through an explicit representation of the projection cone's extreme rays — this matches how the book's own Theorems 10.2/10.3 and Corollary 10.4 are phrased purely in terms of $(\alpha,\beta)$ -validity for $P_D$ , never in terms of a specific disjunction's multipliers, so this is not a weakening relative to the source. $P_D$ (the disjunctive hull that $(\mathrm{CGLP})_y$ is defined against) and $P_Q$ (the lifted polyhedron whose supporting hyperplane Corollary 10.4 describes) are kept as two independent Set (Fin n → ℝ) parameters with no assumed relationship between them, matching the book's own text, which never states one; conflating them would be a trivializing formalization that this mission explicitly avoids. "The point closest to $x^*$ " on the segment $(\bar x, x^*]$ is formalized via IsGreatest on the parameter $t \in (0, 1]$ at which the optimal hyperplane meets the segment, rather than via an unformalized Euclidean-distance minimization, since that is what "closest" means for points colinear with $\bar x$ and $x^*$ on a single ray.

Corollary 10.4 corrects a typo in the printed text: the corollary as printed reads "let $y := \bar x$ for some $x^* \in P_Q$ ", omitting " $x^* -$ " before $\bar x$ ; the very next line's figure caption gives the intended formula unambiguously as $y = x^* - \bar x$ , and the formalization uses the corrected formula (see MODERATION_NOTES.md).

This mission depends on no other chunk's Lean definitions — the CGLP and tableau apparatus needed here (originally introduced in Chapters 8 and 9) is restated locally, per the series' convention against importing another draft mission's definitions across chunks that are being drafted concurrently. A complete development needs: Farkas-type separation for the boundedness dichotomy in Theorem 10.2, and careful bookkeeping of finite index sets and their images under the basis maps $\iota, \iota'$ for Theorem 10.1. The tableau infrastructure (Ahat, Bhat, Abar0, Abar, GammaOf) is reusable by any later mission touching the simplex-tableau side of lift-and-project cuts.

Selected references

E. Balas and P. Bonami, Generating lift-and-project cuts from the LP simplex tableau: open source implementation and testing of new variants, Mathematical Programming Computation 1 (2009), 165–199. https://doi.org/10.1007/s12532-009-0006-4
E. Balas and M. Perregaard, Lift-and-project for mixed 0-1 programming: recent progress, Discrete Applied Mathematics 123 (2002), 129–154. https://doi.org/10.1016/S0166-218X(01)00340-7
E. Balas, Disjunctive Programming, Springer, 2018, Chapter 10, §10.1 and §10.6. https://doi.org/10.1007/978-3-030-00148-3

8 thms3 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming X: Solving the Cut-Generating LP on the Simplex TableauTextbook

Motivation

Chapter 8 established an exact correspondence between lift-and-project cuts and simple disjunctive cuts, but its practical payoff is what this chapter develops: the cut-generating LP (CGLP)_k never needs to be formulated or solved on its own. Every pivot of (CGLP)_k can instead be mimicked directly on the much smaller simplex tableau of the original LP relaxation — replacing a large auxiliary linear program with bookkeeping on a tableau the solver already has. This chapter works out that correspondence at the level of individual pivots: which tableau pivot improves the resulting cut, and by how much, answered entirely in terms of ordinary tableau coefficients and two closed-form evaluation functions.

Setting

S:={1,…,m+p} and N:={m+p+1,…,m+p+n} index the surplus and structural variables of (LP) respectively — giving a direct correspondence between (LP)'s own variables and the surplus variables of Ãx≥b̃. For a basic solution with nonbasic set J (row set M1∪M2 from Chapter 8), Â:=Ã_J is the resulting nonsingular submatrix, and row k of the tableau reads x_k+ Σ_{j∈J}ā_{kj}s_j=ā_{k0}. Adding γ times row i to row k gives the composite row (9.10), x_k+γx_i+Σ_{j∈J}(ā_{kj}+γā_{ij})s_j=ā_{k0}+γā_{i0}, from which a new simple disjunctive cut can be read off whenever 0<ā_{k0}+γā_{i0}<1.

Formalization targets

Theorem 9.3 (goal) — the most-improving pivot column

The pivot column in row i most improving the cut from row k is indexed by l*∈J minimizing f⁺(γ_l) (if ā_{kl}ā_{il}<0) or f⁻(γ_l) (if ā_{kl}ā_{il}>0), over all l∈J with -ā_{k0}/ā_{i0}<γ_l<(1-ā_{k0})/ā_{i0}, γ_l:=-ā_{kl}/ā_{il}.

The chain of results building toward it

Lemma 9.1 (the tableau coefficients' closed form, eq. (9.4)-(9.5)) and Theorem 9.2 (the reduced costs of the CGLP columns u_i,v_i in terms of tableau coefficients, eq. (9.6)) are the two milestones the goal's own machinery is built from. Proposition 9.4, a bridge to Chapters 10-11's general split disjunctions, is included as a genuine milestone despite its payoff lying mostly outside this chapter.

Significance

The results themselves. This chapter is what makes lift-and-project cuts practical: instead of solving an (m+p+n)-row auxiliary LP from scratch for every candidate cut, a single pivot on the (LP)'s own tableau — guided by reduced costs that are themselves closed-form functions of tableau entries — identifies whether an improving cut exists and which one it is. Theorem 9.3's evaluation functions f⁺,f⁻ are exactly the tool a cutting-plane implementation would compute at every candidate pivot.

Formalizing it. No object in this mission exists on the platform prior to it or in Mathlib. This mission restates 08-cut-correspondence's (CGLP)_k apparatus locally, per the series convention and BRIEF.md's explicit instruction, and extends it with this chapter's own generalization to an arbitrary tableau row (needed since Lemma 9.1/Theorem 9.2 concern every basic variable's row, not only the disjunction row k).

Difficulty

Lemma 9.1's book proof is a four-case block-matrix verification (structural/surplus, basic/nonbasic); this mission instead states its content as the identity it is actually for — that the closed-form coefficients express every row's slack as an affine function of the nonbasic rows' slacks, for every point x — which follows tautologically from x=Â⁻¹b̂+Â⁻¹s_J's own definition once stated this way, without needing to reconstruct the block-matrix case analysis. Theorem 9.2's difficulty is that "reduced cost" is not already available as a formalized LP concept in this mission's apparatus; rather than build a generic LP reduced-cost theory, this mission follows the book's own derivation directly — explicitly constructing the pivoted-out extension of a basic solution (eq. (9.7)-(9.9)) and asserting that its objective value decomposes with r_{u_i},r_{v_i} as coefficients, which is genuine, non-circular content matching the proof's own final step ("we can then read the reduced costs... as the coefficients").

Formalization scope

This chapter makes the row/variable identification of Chapters 6-8 fully explicit (N directly indexes the structural variables), but no theorem's own displayed formula in this chunk needs that correspondence beyond what SurplusM's row-general treatment (this chunk's own generalization of 08-cut-correspondence's Surplus) already provides — see MODERATION_NOTES.md for why the S/N/B/R/P/Q block structure is proof machinery, not part of the stated content, throughout.

Theorem 9.3's range condition on γ_l, truncated in BRIEF.md's own excerpt, was completed by reading the PDF directly (confirmed identical to the range derived earlier in the same section): -ā_{k0}/ā_{i0}<γ_l<(1-ā_{k0})/ā_{i0}.

Selected references

E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 9.
E. Balas, M. Perregaard, A precise correspondence between lift-and-project cuts, simple disjunctive cuts, and mixed integer Gomory cuts for 0-1 programming, Mathematical Programming B 94 (2003), 221–245 (cited in the text as [33], the origin of the tableau-pivoting procedure this chapter derives Lemma 9.1 and Theorem 9.2 from).

9 thms3 active usersReviewed

Completed

Combinatorics Linear Optimization Operations Research+1·Captain: Shuze Chen

Disjunctive Programming VI: Extended Formulations for Perfectly Matchable Subgraph PolytopesTextbook

Motivation

Many polytopes that arise from combinatorial optimization problems have no small facet description in their natural variable space, yet become describable by a compact linear system once lifted to a higher-dimensional space of auxiliary variables and projected back down — Chapter 2's own extended formulation of the convex hull of a disjunctive set is one instance of this phenomenon. This chapter turns the idea around: rather than using projection to build a compact formulation, it uses projection to prove integrality of a formulation that is already compact but whose integrality is not obvious from any standard sufficient condition (total unimodularity, balancedness, etc.). The technique is illustrated on three closely related combinatorial polytopes built from perfectly matchable, assignable, and path-decomposable vertex subsets of a graph or digraph — each proved integral by lifting to an edge- or arc-variable space where total unimodularity is easy to check, then projecting.

Setting

For a finite vertex set $V$ , the incidence vector of $W \subseteq V$ is $1$ on $W$ , $0$ elsewhere, and $x(S) := \sum_{i \in S} x_i$ . A graph $G(W)$ has a perfect matching if there is a fixed-point-free involution on $W$ respecting adjacency. The PMS (Perfectly Matchable Subgraph) polytope of $G$ is $\mathrm{conv}(X)$ where $X$ is the set of incidence vectors of such $W$ ; $N(S) := \{j \notin S : (i,j) \in E \text{ for some } i \in S\}$ .

For a digraph $(V,A)$ : $G(W)$ is assignable if it admits a cycle decomposition (a permutation of $W$ respecting arcs), giving the Assignable Subgraph Polytope. For an acyclic digraph with distinguished nodes $s,t$ : $G(W \cup \{s,t\})$ admits an $s$ - $t$ path decomposition if a collection of interior-node-disjoint $s$ - $t$ paths covers it, giving the $s$ - $t$ Path Decomposable Subgraph Polytope over $W \subseteq V \setminus \{s,t\}$ . $\Gamma(S)$ and $\Gamma^*(S)$ are the corresponding out-neighborhood operators. For an arbitrary graph, $c(S)$ counts the connected components of the induced subgraph $G(S)$ .

Formalization targets

Theorem 5.1 (goal) — the PMS polytope of a bipartite graph

0 \le x_i \le 1\ (i \in V), \qquad x(V_1) - x(V_2) = 0, \qquad x(S) - x(N(S)) \le 0\ \ (S \subseteq V_1).

Theorem 5.2 — the Assignable Subgraph Polytope

0 \le x_i \le 1\ (i \in V), \qquad x(S \setminus \Gamma(S)) - x(\Gamma(S) \setminus S) \le 0 \quad (S \subseteq V).

Theorem 5.3 — the $s$ - $t$ Path Decomposable Subgraph Polytope

0 \le x_i \le 1\ (i \in V), \qquad x(S \setminus \Gamma^*(S)) - x(\Gamma^*(S) \setminus S) \le 0 \quad (S \subseteq V \setminus \{s,t\}).

Theorem 5.4 — the PMS polytope of an arbitrary graph

0 \le x_i \le 1\ (i \in V), \qquad x(S) - x(N(S)) \le |S| - c(S)

for every $S$ all of whose components are single nodes or nonbipartite with odd order — the weakest faithful statement, since dropping the side condition would assert the inequality for subsets it does not hold for.

Significance

The results themselves. Each theorem gives an explicit, checkable linear system defining a polytope that arises naturally from a combinatorial covering/decomposition property, turning "does $G(W)$ have property $X$ " into a linear-programming feasibility question. Theorem 5.1 is the one the book proves in full and the template for the other three: bipartite matching, digraph assignment, and acyclic-digraph path decomposition are structurally parallel problems (all reduce to checking a König–Hall-type combinatorial condition), and the same lift-and-project technique handles all three uniformly. Theorem 5.4 extends the idea to arbitrary (non-bipartite) graphs at the cost of a sharper right-hand side and a component-based side condition, connecting to Edmonds' classical matching-polytope theory while remaining a genuinely different object (a polytope of coverable vertex sets, not of matchings themselves).

Formalizing it. No object in this mission — the PMS, Assignable, or Path Decomposable Subgraph polytopes, or their defining neighbor operators — exists on the platform prior to this mission. The closest platform result, MetricTSP.pm_polytope_decomposition (Edmonds' perfect matching polytope theorem, in edge-variable space over a fixed vertex set requiring every vertex matched), is a genuinely different object from Theorem 5.4's PMS polytope (vertex-variable space, vertices may be left unmatched by design) and is not reused as a kind: reference item; it is noted here as related, not equivalent.

Difficulty

The natural first attempt tries to verify each polytope's integrality directly, by checking a known sufficient condition (total unimodularity, balancedness) on the displayed vertex-space system itself. This fails: the book states explicitly that (5.5)'s coefficient matrix is not totally unimodular, which is exactly why the lift-to-edge-variables step is necessary at all. The real content of each theorem is the two-part argument: (1) the lifted system in edge/arc variables is totally unimodular (checkable directly), so its polyhedron is integral; and (2) the vertex- space system is exactly the projection of the lifted one — a nontrivial fact requiring Chapter 2's projection machinery, not merely an unfolding of definitions. Theorem 5.4's extra difficulty, flagged explicitly in the text, is that its projection cone is not pointed, so the proof must work with a finite generating set rather than extreme rays, and it suffices to find a subset of generators producing every facet rather than a complete generating set — a genuinely harder argument the book itself outsources to a citation.

Formalization scope

Undirected graphs use Mathlib's SimpleGraph; digraphs use a bare relation A : V → V → Prop (not required symmetric or irreflexive, matching the book's unrestricted notion). Bipartition is recorded via part : V → Bool (decidable by construction) rather than two Set V halves, keeping the sums x(V_1), x(V_2) computable over Finsets throughout. IsAssignable uses Equiv.Perm on the vertex-set subtype, since a cycle decomposition is exactly a permutation. IsComponentOf and IsBipartiteOn (Theorem 5.4) are built directly from reachability and 2-colorability rather than Mathlib's induced-subgraph/ConnectedComponent API, matching the "maximal connected subset" reading of "component" the book's own prose intends.

IsPathDecomposable (Theorem 5.3) encodes "admits an $s$ - $t$ path decomposition" via a degree-constrained arc set (every interior node has exactly one incoming and one outgoing chosen arc, none entering $s$ or leaving $t$ , at least one leaving $s$ ) rather than an explicit list of vertex-disjoint paths — provably equivalent by the standard fact that an acyclic arc set with this degree pattern always decomposes into such a path family, and considerably lighter to state and reason about than constructing Path objects directly.

A trivializing formalization is ruled out explicitly: every theorem keeps the fractional box constraint $0 \le x_i \le 1$ rather than the integral $x_i \in \{0,1\}$ (per BRIEF.md's own warning, dropping the relaxation collapses the claim to a restatement of the combinatorial definition), and Theorem 5.1 is stated only for bipartite graphs — never generalized to subsume Theorem 5.4's genuinely different inequality system and side condition.

Selected references

E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 5, §5.2.
M. O. Ball, U. Derigs, An analysis of alternate strategies for implementing matching algorithms, Networks 13 (1983) (cited in the text as [13], the origin of Theorems 5.2 and 5.3).
W. R. Pulleyblank, J. Edmonds, Facets of 1-matching polyhedra, in Hypergraph Seminar, Springer Lecture Notes in Mathematics 411 (1974) — the origin of the perfectly matchable subgraph polytope literature (cited in the text as [34], the origin of Theorem 5.1).
L. Lovász, M. D. Plummer, Matching Theory, Elsevier, 1986 (cited in the text as [35], the origin of Theorem 5.4).

7 thms3 active usersReviewed

Completed

Linear Optimization Numerical Analysis Optimization·Captain: mikedeng1

The Relaxation Method for Linear Inequalities II: For a Lower-Dimensional Solution Polytope Infinite Reflexions Settle on a Sphere with Axis L_rResearch Paper

Motivation

Finding a point that satisfies a finite system of linear inequalities is the feasibility half of linear programming, and it is the problem that iterative projection methods were designed for. In 1954 S. Agmon (The relaxation method for linear inequalities, Canad. J. Math. 6, 382–392) and T. S. Motzkin and I. J. Schoenberg (The relaxation method for linear inequalities, Canad. J. Math. 6, 393–404) analysed the simplest such method: from a point that violates the system, move towards the most violated half-space. The method is a precursor of the perceptron algorithm and of projection and reflection algorithms for convex feasibility problems.

The paper distinguishes whether the solution set is full-dimensional or not. This mission covers the case in which it is not (Theorem 2 of the paper); the full-dimensional case is a separate mission of the same series.

Timeline.

1922. L. Fejér observes that the points "closest" to a set, in a point-wise sense, form its convex hull (cited on p. 393).
1954. Agmon proves that for a parameter $0 < \lambda < 2$ an infinite relaxation sequence converges to a point of the solution set.
1954. Motzkin and Schoenberg reprove Agmon's result and treat the extreme parameter $\lambda = 2$ , the reflexion method: it always terminates when the solution set is full-dimensional (Theorem 1), and when it is not, an infinite reflexion sequence ends on a sphere around the affine hull of the solution set (Theorem 2, Case 2).

Setting

Let $E_n$ be $n$ -dimensional Euclidean space with distance $|x - y|$ . A system of $m$ linear inequalities

\sum_{j=1}^n a_{ij}x_j + b_i \geqslant 0 \qquad (i = 1, \dots, m)

is given by vectors $a_i \in E_n$ and numbers $b_i$ . Each inequality defines a closed half-space $H_i = \{x : \langle a_i, x\rangle + b_i \geqslant 0\}$ , and the solution set is the polytope $A = \bigcap_i H_i$ , assumed nonempty. Its affine hull is an $r$ -dimensional flat $L_r$ ; this mission assumes $r < n$ , that is, $L_r \neq E_n$ .

A relaxation step with parameter $\lambda$ from a point $p \notin A$ chooses a half-space $H_j$ at maximal distance from $p$ , the point $q \in H_j$ nearest to $p$ , and moves to

p_1 = p + \lambda (q - p).

For $\lambda = 2$ the new point is the mirror image of $p$ in the boundary hyperplane $\pi_j$ of $H_j$ . A run is a sequence $p_0, p_1, \dots$ in which every point outside $A$ is followed by a relaxation step. The run terminates if some $p_N \in A$ ; otherwise it is an infinite sequence.

A sequence $q_0, q_1, \dots$ outside $A$ is Fejér-monotone with respect to $A$ if $q_\nu \neq q_{\nu+1}$ and $|q_{\nu+1} - a| \leqslant |q_\nu - a|$ for all $a \in A$ and all $\nu$ .

For a flat $L$ and a point $c \notin L$ , the locus

X(L, c) = \{x : |x - a| = |c - a| \text{ for all } a \in L\}

is a sphere of dimension $n - r - 1$ centred at the orthogonal projection of $c$ onto $L$ and lying in the flat through that centre normal to $L$ . The paper calls it a spherical surface having $L$ as its axis. For $r = n - 1$ it consists of two points symmetric with respect to the hyperplane $L$ .

Formalization targets

Goal: Theorem 2

Assume $A$ is nonempty and $L_r \neq E_n$ .

Case 1 ( $0 < \lambda < 2$ ). Every run either terminates or converges to a point of $A$ :

(\exists N,\ p_N \in A) \ \lor\ (\exists\, l \in A,\ p_\nu \to l).

Case 2 ( $\lambda = 2$ ). Every run either terminates or ends on one sphere with axis $L_r$ :

(\exists N,\ p_N \in A) \ \lor\ \big(\exists\, \nu_0,\ \exists\, c \notin L_r,\ \forall \nu \geqslant \nu_0,\ p_\nu \in X(L_r, c)\big).

Case 1 is Agmon's theorem; Case 2 is the paper's own contribution.

Milestones (the paper's own intermediate claims)

§2, (1.10): $X(L, p)$ is the sphere of the normal flat at the projection $b$ of $p$ , centred at $b$ through $p$ , and $L$ is exactly the set of points equidistant from all points of that sphere.
§1: an infinite run with $0 < \lambda \leqslant 2$ is Fejér-monotone with respect to $A$ .
Lemma 1, Case 2: if $r < n$ , a Fejér-monotone sequence either converges or all its limit points lie on one sphere $X(L_r, c)$ with $c \notin L_r$ .
§5: the limit of a convergent infinite run lies in $A$ , on its boundary.
(3.2)/(3.7): if $r < n$ and an infinite run does not converge, then $\inf_\nu |p_{\nu+1} - p_\nu| > 0$ .
§8: an infinite reflexion run ( $\lambda = 2$ ) does not converge.

An additional item, Corollary 1, states that for $r < n$ and an infinite reflexion run, the hyperplanes $\pi_{j_\nu}$ used for $\nu > \nu_0$ all contain $A$ and hence $L_r$ .

Significance

The result. Theorem 2 completes the description of the reflexion method. Combined with Theorem 1 (termination when $r = n$ ), it says that the reflexion method either finds a solution or, when the solution set is flat, falls into a motion on a sphere about $L_r$ that reveals the flat: by Corollary 1 the hyperplanes used from some point on contain $L_r$ . The paper notes that such hyperplanes can be used to reduce the problem to a lower dimension. Case 1 is the convergence theorem for under- and over-relaxation.

The formalization. The results are proved and classical, and no machine-checked proof of either theorem is known. This mission produces a Lean statement and, eventually, a proof of the convergence theory of the relaxation method for linear inequalities. Reusable pieces: Fejér monotonicity and its limit-point structure (Lemma 1), and the geometry of spheres with an affine axis. Proofs of individual milestones and of Corollary 1 are welcome contributions.

Difficulty

Fejér monotonicity alone gives boundedness and convergence of every distance $|p_\nu - a|$ , $a \in A$ , but not convergence of the sequence. When $A$ lies in a proper flat, those distances fix a point only up to a sphere about $L_r$ , so the naive argument "the distances converge, hence the points converge" fails exactly in this mission's case. Lemma 1, Case 2 replaces convergence by the weaker statement that limit points lie on one sphere. For $0 < \lambda < 2$ the obstacle is to exclude an oscillation on that sphere. For $\lambda = 2$ oscillation does happen, and the claim is that the run eventually lies on the sphere exactly, not just near it. That requires the finiteness of the family of half-spaces, not only compactness.

Formalization scope

Space and data. EuclideanSpace ℝ (Fin n); the system is a : Fin m → EuclideanSpace ℝ (Fin n), b : Fin m → ℝ, with $\sum_j a_{ij}x_j =$ inner ℝ (a i) x. Half-spaces are closed ( $\geqslant$ ). Distances to half-spaces are Metric.infDist.
Standing hypotheses. The polytope is nonempty ((polytope a b).Nonempty), as the paper assumes from the outset. $L_r$ is affineSpan ℝ (polytope a b), so " $A \subset L_r$ " holds by construction, and " $r < n$ " is affineSpan ℝ (polytope a b) ≠ ⊤. No separate natural number $r$ is introduced.
The step is a relation. The paper makes $F_\lambda$ single-valued by an unspecified pre-assigned rule for ties in (1.5). Here a step may use any maximizing index $j$ , and every theorem quantifies over all runs, so each statement holds for every tie-breaking rule. The parameter $\lambda$ is named lam.
Runs. A run is any sequence p : ℕ → E with a relaxation step after every point outside $A$ . Termination is ∃ N, p N ∈ A; an infinite sequence is ∀ ν, p ν ∉ A.
Spheres. axisSphere L c is the locus (1.10). Every statement that uses it as a sphere requires c ∉ L, which rules out the degenerate one-point locus. Without that requirement, Case 2 of Theorem 2 and Case 2 of Lemma 1 would be weaker than the paper's.
Limit points are cluster points of the sequence (MapClusterPt x atTop q), not points of the closure of its range. Boundary is the topological frontier.
Explicit choices recorded against the page.
1. Lemma 1, Case 2 is stated for an arbitrary nonempty set $A$ rather than for the polytope. This is stronger, and the proof uses only that $A$ spans $L_r$ .
2. The Fejér property (§1), the §5 limit claim and (3.2) are stated for $0 < \lambda \leqslant 2$ , because the paper proves them for $\lambda < 2$ and reuses them for $\lambda = 2$ in §§6–8. The §5 claim is also stated without a dimension hypothesis.
3. The §8 non-convergence claim is stated without the section's assumption $r < n$ , which its argument (§§5–6) does not use.
4. Corollary 1 records the index used at each step (IsRelaxStepVia), which the relation hides. Its last sentence, on reducing the dimension, is commentary and is not formalized.
Ruled out. A formalization that fixes a tie-breaking rule, that asserts the statements only for some run, or that allows the sphere's point $c$ to lie in $L_r$ does not state Theorem 2.

Selected references

T. S. Motzkin and I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 393–404. doi:10.4153/CJM-1954-038-x
S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 382–392. doi:10.4153/CJM-1954-037-2
L. Fejér, Ueber die Lage der Nullstellen von Polynomen, die aus Minimumforderungen gewisser Arten entspringen, Mathematische Annalen 85 (1922), 41–48 (reference 2 of the paper).

10 thms3 active usersReviewed

Completed

Machine Learning Probability Statistics·Captain: mikedeng1

Adversarially Robust Generalization Requires More Data 4: Robust Learning from One Thresholded Sample in the Bernoulli ModelResearch Paper

Motivation

Classifiers trained to high standard accuracy can be fooled by small, deliberately chosen perturbations of their inputs, so-called adversarial examples (Szegedy et al., 2014; Goodfellow et al., 2015). Training methods that aim at robustness against perturbations bounded in the $\ell_\infty$ norm reach high robust accuracy on the training set while robust test accuracy stays far lower, a gap much larger than the standard generalization gap (Madry et al., 2018). Schmidt, Santurkar, Tsipras, Talwar and Mądry (arXiv:1804.11285) ask whether this gap is intrinsic: does learning a robust classifier need more data than learning an accurate one?

They answer with two simple data distributions. In a Gaussian model the robust sample complexity is larger than the standard one by a factor of order $\sqrt d$ , for every learning algorithm. In a Bernoulli model on the hypercube, linear classifiers suffer the same penalty, but a nonlinear classifier does not. This mission formalizes the second half of that picture: in the Bernoulli model, thresholding the input and then applying the linear classifier learned from one single sample is robust against every $\ell_\infty$ perturbation of size less than $1$ .

Setting

Points live in $\mathbb R^d$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|_2$ . Labels are $y\in\{\pm1\}$ . A binary classifier is any map $f:\mathbb R^d\to\{\pm1\}$ , and for $w\in\mathbb R^d$ the linear classifier is $f_w(x)=\operatorname{sgn}(\langle w,x\rangle)$ .

The $(\theta^\star,\tau)$ -Bernoulli model. Fix a sign vector $\theta^\star\in\{\pm1\}^d$ and a bias $\tau\in(0,\tfrac12]$ . A sample $(x,y)$ is drawn by choosing $y$ uniformly in $\{\pm1\}$ and then, independently for each coordinate $i$ , setting $x_i=y\theta^\star_i$ with probability $\tfrac12+\tau$ and $x_i=-y\theta^\star_i$ with probability $\tfrac12-\tau$ . So $x\in\{\pm1\}^d$ , and each coordinate carries a weak signal of strength $2\tau$ about the label.

Errors. The classification error of $f$ is $\mathbb P_{(x,y)}[f(x)\ne y]$ . For $\varepsilon\in\mathbb R$ the $\ell_\infty$ ball is $\mathcal B^\varepsilon_\infty(x)=\{x'\in\mathbb R^d:\|x'-x\|_\infty\le\varepsilon\}$ , and the $\ell_\infty^\varepsilon$ -robust classification error of $f$ is

\mathbb P_{(x,y)}\big[\exists\,x'\in\mathcal B^\varepsilon_\infty(x):\ f(x')\ne y\big].

The adversary may move $x$ anywhere in the ball, including off the hypercube.

Thresholding. The thresholding map $T:\mathbb R^d\to\mathbb R^d$ is $T(x)_i=+1$ if $x_i\ge0$ and $T(x)_i=-1$ otherwise. The classifier studied is $f_{\hat w}\circ T$ , with $\hat w=yx$ computed from one training sample $(x,y)$ .

Formalization targets

Goal: Theorem 10 (p. 8)

There is a universal constant $c>0$ such that, whenever $\tau\ge c\,d^{-1/4}$ and $(x,y)$ is one sample of the model with $\hat w=yx$ ,

\mathbb P_{(x,y)}\Big[\exists\,\varepsilon<1:\ \mathrm{RobErr}_\varepsilon\big(f_{\hat w}\circ T\big)>\tfrac1{100}\Big]\ \le\ \exp\!\Big(-\frac{\tau^2d}{2}\Big).

The constant $c$ is left existential; only the scaling $\tau\gtrsim d^{-1/4}$ is fixed. The failure probability is the one the paper proves for the same classifier.

Milestones

Lemma 24 (p. 31): $\mathbb P\big[\langle z,\theta^\star\rangle\le2\tau d-\sqrt{2d\log(1/\delta)}\big]\le\delta$ for $z=xy$ .
Lemma 25 (p. 31): for $\hat w=z/\|z\|_2$ , $\mathbb P[\langle\hat w,\theta^\star\rangle\le\tau\sqrt d]\le\exp(-\tau^2d/2)$ .
Lemma 26 (p. 32): for a fixed unit $w$ with $\langle w,2\tau\theta^\star\rangle\ge0$ , $\mathbb P[\langle w,z\rangle\le0]\le\exp(-2\tau^2\langle w,\theta^\star\rangle^2)$ .
Theorem 27 (p. 32): with probability at least $1-\exp(-\tau^2d/2)$ , $f_{\hat w}$ has classification error at most $\exp(-2\tau^4d)$ .
Corollary 28 (p. 33): if $\tau\ge(\log(1/\beta)/(2d))^{1/4}$ , then with probability at least $1-\exp(-\tau^2d/2)$ , $f_{\hat w}$ has classification error at most $\beta$ .
Thresholding identity (§2.2, p. 7): $T(\mathcal B^\varepsilon_\infty(x))=\{x\}$ for every $x\in\{\pm1\}^d$ and $0\le\varepsilon<1$ .

Significance

Together with the lower bound for linear classifiers in the same model (Theorem 9 of the paper), Theorem 10 shows that robust sample complexity depends on the hypothesis class and on the data distribution, not only on the perturbation size: a fixed nonlinear preprocessing step closes a gap that no linear classifier can close. The paper's Gaussian model shows the opposite behaviour, where every learner pays the $\sqrt d$ penalty, so the two models together separate "robustness is information-theoretically expensive" from "robustness is expensive for a restricted class". The authors also report that an explicit thresholding layer improves robust training on MNIST, which motivates the model.

The result is proved in the paper. To the platform's knowledge it has no machine-checked proof. Formalizing it yields a complete, finite and self-contained robust-learning upper bound, the single-sample standard-generalization bounds of Theorem 27 and Corollary 28 as reusable statements, and a worked instance of one-sided Hoeffding bounds for weighted sums of hypercube coordinates.

Difficulty

The concentration steps are standard, but the natural first approach to the goal fails: a bound on the classification error of the linear classifier $f_{\hat w}$ says nothing about its robust error, and for $\varepsilon$ of order $\tau$ the robust error of every linear classifier is close to $\tfrac12$ . The goal concerns the nonlinear classifier $f_{\hat w}\circ T$ , whose robustness rests on the data lying exactly on the hypercube and on the adversary's budget being below $1$ ; neither fact is visible to an argument about linear classifiers. A second difficulty is bookkeeping: the paper uses three forms of the estimator ( $yx$ , $z/\|z\|_2$ , $yx/\|x\|_2$ ), a training sample and a test sample with the same name, and a failure event that must hold for all $\varepsilon<1$ at once.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d). Labels and hypercube coordinates are Bool ( $+1\leftrightarrow$ true). Because the model is finite, every probability is a finite sum of the weights $\tfrac12\prod_i(\tfrac12\pm\tau)$ ; no measure theory is involved. Conventions committed to:

coordinates of $x$ are independent given $y$ (the paper's "sampling each coordinate", as its proofs use it);
$0<\tau\le\tfrac12$ in every theorem, since $\tfrac12-\tau$ must be a probability;
$\operatorname{sgn}(0)$ is taken as $+1$ (a tie is classified $+1$ ); $T$ sends $0$ to $+1$ , as printed;
the $\ell_\infty$ ball is written coordinatewise, never as the Euclidean ball;
"with probability at least $1-q$ , the error is at most $\beta$ " is stated as "the failure event has probability at most $q$ ";
the goal's "for any $\varepsilon<1$ " is inside the event, one good sample for all $\varepsilon$ ;
added hypotheses, each forced by a degenerate case where the printed statement is false: $d\ge1$ in Lemma 24, $\beta>0$ in Corollary 28, $\varepsilon\ge0$ in the thresholding identity.

A formalization that bounds only the standard error of $f_{\hat w}$ , drops $T$ , uses the Euclidean ball, or lets the estimator see $\theta^\star$ would be a different and easier statement; the goal rules each of these out.

A complete development needs one-sided Hoeffding bounds for weighted sums of independent bounded variables on a finite product space (Mathlib has the measure-theoretic version, ProbabilityTheory.measure_sum_ge_le_of_iIndepFun with hasSubgaussianMGF_of_mem_Icc) and the transfer between the finite-sum encoding and a product measure. Both are reusable beyond this mission. Proofs of any milestone, and a bridge lemma from bprob to Measure.pi, are welcome. The other missions of this series (Gaussian lower bound, Bernoulli lower bound for linear classifiers, Gaussian upper bound) formalize the paper's remaining main results.

Selected references

L. Schmidt, S. Santurkar, D. Tsipras, K. Talwar, A. Mądry, Adversarially Robust Generalization Requires More Data, NeurIPS 2018; arXiv:1804.11285v2. https://arxiv.org/abs/1804.11285
A. Madry, A. Makelov, L. Schmidt, D. Tsipras, A. Vladu, Towards Deep Learning Models Resistant to Adversarial Attacks, ICLR 2018. https://arxiv.org/abs/1706.06083
C. Szegedy et al., Intriguing properties of neural networks, ICLR 2014. https://arxiv.org/abs/1312.6199
I. Goodfellow, J. Shlens, C. Szegedy, Explaining and Harnessing Adversarial Examples, ICLR 2015. https://arxiv.org/abs/1412.6572
P. Rigollet, J.-C. Hütter, High Dimensional Statistics, lecture notes, MIT, 2017. https://math.mit.edu/~rigollet/PDFs/RigNotes17.pdf

8 thms3 active usersReviewed

Completed

Linear Optimization Numerical Analysis Optimization·Captain: mikedeng1

The Relaxation Method for Linear Inequalities I: For a Full-Dimensional Solution Polytope the Relaxation Converges and the Reflexion Method TerminatesResearch Paper

Motivation

Finding a point that satisfies a finite system of linear inequalities is the feasibility problem underlying linear programming, and it is also the basic step of many methods in signal and image reconstruction, where the system is too large to be solved by elimination. The relaxation method attacks it one inequality at a time: from the current point, move towards the half-space that is violated the most. Each step costs one pass over the rows and no factorization, which is why this family of iterations (with its relatives: Kaczmarz's method for equations, the projection methods for convex feasibility, and the perceptron algorithm) has been studied continuously since the early 1950s.

Timeline:

1922. Fejér observes that the set of points of $E_n$ that no other point dominates in distance to a closed set $A$ is the convex hull of $A$ (Motzkin and Schoenberg 1954, p. 393). This idea of moving to a point that is closer to every point of $A$ drives the method.
1954. Agmon (Canad. J. Math. 6, 382–392) proves that for a relaxation parameter $0 < \lambda < 2$ the iterates either reach the solution set or converge to a point on its boundary.
1954. Motzkin and Schoenberg (Canad. J. Math. 6, 393–404) reprove Agmon's theorem from a single lemma about Fejér-monotone sequences and treat the extreme case $\lambda = 2$ , the reflexion method. When the solution set has full dimension, reflexion always stops after finitely many steps; no parameter $0 < \lambda < 2$ has this property.

This mission is the first of three built on the Motzkin–Schoenberg paper: it covers the full-dimensional case, Theorem 1.

Setting

Let $E_n$ be $n$ -dimensional Euclidean space. A system of $m$ linear inequalities

\sum_{j=1}^n a_{ij}x_j + b_i \ge 0 \qquad (i = 1, \dots, m)

is given by rows $a_i \in E_n$ and constants $b_i \in \mathbb R$ . The $i$ -th inequality defines the closed half-space $H_i = \{x : \langle a_i, x\rangle + b_i \ge 0\}$ , and the set of solutions is the polytope $A = \bigcap_{i=1}^m H_i$ . The system is assumed consistent, so $A$ is nonempty. The dimension $r$ of $A$ is the dimension of its affine hull; $r = n$ means that $A$ is not contained in any hyperplane.

Fix a relaxation parameter $\lambda$ with $0 < \lambda \le 2$ . From a point $p \notin A$ one relaxation step is:

choose $j$ with $\operatorname{dist}(p, H_j) = \max_i \operatorname{dist}(p, H_i)$ , a farthest half-space;
let $q \in H_j$ be the point with $|p - q| = \operatorname{dist}(p, H_j)$ ;
set $p_1 = p + \lambda (q - p)$ .

For $\lambda = 2$ , $p_1$ is the mirror image of $p$ in the boundary hyperplane of $H_j$ . Iterating from a starting point $p_0$ gives a sequence $p_0, p_1, p_2, \dots$ ; the process terminates when some $p_N \in A$ , and otherwise produces an infinite sequence of points outside $A$ .

A sequence $q_0, q_1, \dots$ of points outside $A$ is Fejér-monotone with respect to $A$ if $q_i \ne q_{i+1}$ and $|q_{i+1} - a| \le |q_i - a|$ for all $a \in A$ and all $i$ .

Formalization targets

Goal: Theorem 1 (p. 395)

Assume $A \ne \emptyset$ and $r = n$ . For every starting point and every choice of farthest half-space at every step:

\text{Case 1: } 0 < \lambda < 2 \implies \big(\exists N,\ p_N \in A\big) \ \lor\ \big(p_\nu \to l \text{ for some } l \in \partial A\big),

\text{Case 2: } \lambda = 2 \implies \exists N,\ p_N \in A .

The goal is the paper's theorem as stated, both cases in one statement. It fixes no constants and no rates.

Milestones

§1, pp. 393–394. For $p \notin H_j$ , $q$ the point of $H_j$ nearest to $p$ and $p_1 = p + \lambda(q - p)$ with $0 < \lambda \le 2$ : $p_1 \ne p$ and $|p_1 - a| \le |p - a|$ for all $a \in A$ , strictly when $\lambda < 2$ ; for $\lambda = 2$ equality holds exactly at the points of $A$ on the boundary $\pi_j$ of $H_j$ . Stated for any violated half-space, as on the page, so it covers every relaxation step.
§5, p. 398. An infinite relaxation sequence is Fejér-monotone with respect to $A$ .
Lemma 1, Case 1, p. 397. If $A$ has dimension $n$ , every Fejér-monotone sequence converges to a point.
§5, p. 399. The limit of a convergent infinite relaxation sequence lies on the boundary of $A$ .

Significance

The result. Case 1 guarantees that the relaxation method never diverges or oscillates: it either solves the system or converges to a boundary solution. Case 2 gives more: for full-dimensional solution sets the reflexion method is a finite algorithm for linear feasibility. Remark 3(b) of the paper shows that this is special to $\lambda = 2$ : for each $0 < \lambda < 2$ there are planar examples where the iteration never stops. The companion missions of this series treat $r < n$ (Theorem 2, where reflexion may settle on a sphere around the affine hull of $A$ ) and reflexion in a general bounded convex set (Theorem 3).

Formalizing it. Both cases are proved in the paper; to our knowledge none is formalized in Lean or Mathlib. The mission produces a reusable model of relaxation for linear inequalities and a Lean proof of a general convergence statement for Fejér-monotone sequences, which also applies to other projection methods. Formalizing the proof in the order of the paper (Lemma 1, then §§5–6) is the intended route; alternative proofs are welcome.

Difficulty

The first idea is that monotone distances to every point of $A$ force convergence. They do not in general: Fejér-monotonicity only bounds the sequence and makes each distance $|q_\nu - a|$ converge, and when $A$ lies in a hyperplane a Fejér-monotone sequence can keep oscillating between two mirror-image points. Convergence genuinely needs the full dimension of $A$ , and the formal argument has to use that hypothesis in an essential way.

For Case 2, the difficulty is that a reflexion step does not shrink the distance to points of $A$ on the reflecting hyperplane, so there is no uniform decrease to count. Termination must also use that the system has finitely many inequalities: for the infinite family of supporting half-spaces of a convex body, treated in the third mission of this series, reflexion need not terminate. A proof that works for a single step, or one that uses a fixed tie-breaking rule, does not cover the statement.

Formalization scope

The space is EuclideanSpace ℝ (Fin n); the rows are vectors a i, and $\sum_j a_{ij} x_j$ is inner ℝ (a i) x. Half-spaces are closed. Distances to sets are Metric.infDist.
The relaxation step is a relation IsRelaxStep a b lam p p', and any maximizing index $j$ is allowed at every step. The paper makes the step single-valued by "some pre-assigned rule"; quantifying over all runs of the relation covers every such rule, so each theorem is at least as strong as the paper's.
A run is a sequence p : ℕ → E in which each point outside $A$ is followed by a relaxation step (IsRelaxRun). Termination is ∃ N, p N ∈ A; an infinite sequence is ∀ ν, p ν ∉ A. Every theorem is stated for every run, never for one run.
The parameter $\lambda$ is named lam, because λ is a Lean keyword.
Nonemptiness of $A$ ("assumed from the outset not to be void") is an explicit hypothesis. $r = n$ is affineSpan ℝ A = ⊤, following the paper's own gloss " $A$ is not contained in any hyperplane". "Boundary" is frontier A, and convergence is Tendsto p atTop (𝓝 l).
Lemma 1, Case 1 is stated for an arbitrary set $A$ with affineSpan ℝ A = ⊤, which includes the paper's polytope.
The milestones of §5 (Fejér-monotonicity of the sequence, the limit on the boundary) are stated for $0 < \lambda \le 2$ and without the dimension hypothesis. The paper proves them in §5 for $0 < \lambda < 2$ and reuses the same argument in §6 for $\lambda = 2$ .
Rows with $a_i = 0$ are allowed (they give $H_i = E_n$ once $A \ne \emptyset$ ); no nondegeneracy hypothesis is imposed.
Ruled out: a formalization of Case 2 that asserts termination for some starting point or some choice of indices, or one whose run hypothesis cannot be satisfied, would be vacuous. A relaxation step exists from every point outside a nonempty $A$ , so the statement constrains every sequence the method can produce.

Useful infrastructure: the closed form $\operatorname{dist}(p, H) = \max(0, -(\langle u, p\rangle + c))/|u|$ for $u \ne 0$ and the nearest point in a half-space; the characterization of $\operatorname{affineSpan} = \top$ via a nonempty interior for convex sets. The Fejér-monotone convergence lemma and the half-space projection lemmas are reusable beyond this mission.

Selected references

T. S. Motzkin and I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 393–404. https://doi.org/10.4153/CJM-1954-038-x
S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 382–392. https://doi.org/10.4153/CJM-1954-037-2
H. H. Bauschke and J. M. Borwein, On projection algorithms for solving convex feasibility problems, SIAM Review 38 (1996), 367–426. https://doi.org/10.1137/S0036144593251710

7 thms3 active usersReviewed

Completed

Machine Learning Probability Statistics·Captain: mikedeng1

Adversarially Robust Generalization Requires More Data 2: A Robust-Error Lower Bound for Linear Classifiers in the Bernoulli ModelResearch Paper

Motivation

Classifiers trained by standard methods reach high accuracy on image benchmarks and yet change their prediction under perturbations of each pixel that are invisible to a human. Training against such perturbations (adversarial training) improves robustness, but on CIFAR10 and SVHN the robust test accuracy stays far below the robust training accuracy: robust models overfit. Schmidt, Santurkar, Tsipras, Talwar and Mądry (arXiv:1804.11285, 2018) asked whether this gap is a failure of current methods or an information-theoretic fact about the number of samples needed. They introduced two simple data models in which a single sample suffices for standard accuracy and proved that robust accuracy needs many more samples.

This mission formalizes their lower bound for the second model, the Bernoulli model on the hypercube, which was designed to resemble MNIST (whose images are close to binary). In this model the lower bound holds for linear classifiers, and the paper shows separately that a non-linear classifier (thresholding followed by a linear rule) escapes it. The result therefore isolates a concrete way in which the model class, not only the amount of data, governs robust generalization.

Setting

Let $d\ge0$ and $\tau>0$ . Points are $x\in\{\pm1\}^d\subset\mathbb R^d$ , labels $y\in\{\pm1\}$ . For a parameter $\theta^\star\in\{\pm1\}^d$ , the $(\theta^\star,\tau)$ -Bernoulli model draws $y$ uniformly from $\{\pm1\}$ and then, independently for every coordinate $i$ , sets $x_i=y\theta^\star_i$ with probability $\tfrac12+\tau$ and $x_i=-y\theta^\star_i$ with probability $\tfrac12-\tau$ (Definition 7). The two classes are noisy copies of the opposite vertices $\pm\theta^\star$ .

The adversary may move a test point anywhere in the $\ell_\infty$ ball

\mathcal B^\varepsilon_\infty(x)=\{x'\in\mathbb R^d:\|x'-x\|_\infty\le\varepsilon\},

leaving the hypercube. The $\ell_\infty^\varepsilon$ -robust classification error of a classifier $f:\mathbb R^d\to\{\pm1\}$ is (Definition 3)

\beta(f)=\Pr_{(x,y)}\big[\exists x'\in\mathcal B^\varepsilon_\infty(x):\ f(x')\ne y\big].

A linear classifier is $f_w(x)=\operatorname{sgn}\langle w,x\rangle$ for $w\in\mathbb R^d$ . A linear-classifier learning algorithm $g_n$ is any function from $n$ labelled samples to a weight vector $w\in\mathbb R^d$ .

The lower bound is Bayesian: $\theta^\star$ is drawn uniformly from $\{\pm1\}^d$ , the learner receives $n$ independent samples $S$ from the $(\theta^\star,\tau)$ -model, outputs $w=g_n(S)$ , and is charged the robust error of $f_w$ on a fresh sample, averaged over $\theta^\star$ and $S$ . The posterior mean $\mathbb E[\theta^\star_i\mid S]=\Pr[\theta^\star_i=+1\mid S]-\Pr[\theta^\star_i=-1\mid S]$ measures how much the learner can know about coordinate $i$ .

Formalization targets

Goal: Theorem 31 (p. 35)

For $0<\tau\le\tfrac14$ , $0\le\varepsilon<3\tau$ , $0<\gamma<\tfrac12$ and every linear learner $g_n$ : if

n\le\frac{\varepsilon^2\gamma^2}{5000\,\tau^4\log(4d/\gamma)},

then

\mathbb E_{\theta^\star,S}\big[\beta(f_{g_n(S)})\big]\ge\tfrac12-\gamma .

Milestones

Eqs. (4)–(5), p. 33: in one dimension the posterior odds of $\theta$ equal $\prod_k\big(\tfrac{1/2+\tau}{1/2-\tau}\big)^{y_kx_k}$ .
Lemma 29, p. 33: for $\tau\le\tfrac14$ and $n\le1/\tau^2$ , with probability $1-\delta$ ,

\Big|\log\tfrac{\Pr[\theta=+1\mid S]}{\Pr[\theta=-1\mid S]}\Big|\le15\tau\sqrt{2n\log(2/\delta)} .

Proof of Theorem 31, p. 36: with probability $1-\gamma/2$ , $|\mathbb E[\theta^\star_i\mid S]|\le15\tau\sqrt{2n\log(4d/\gamma)}$ for all $i$ .
§4, p. 10: $\sup_{\|\Delta\|_\infty\le\varepsilon}\langle yw,\Delta\rangle=\varepsilon\|w\|_1$ , so $w$ robustly classifies $(x,y)$ iff $\langle yw,x\rangle>\varepsilon\|w\|_1$ .
Proof of Theorem 31, p. 37: when $\theta^\star$ has independent coordinates with means bounded by $b$ in absolute value, a fresh sample satisfies $\langle w,yx\rangle\le\frac{2\tau b}{\gamma}\|w\|_1$ with probability at least $(1-\gamma)/2$ .

The goal keeps the paper's explicit constants ( $5000$ , $3\tau$ , $\log(4d/\gamma)$ ) because Theorem 31 is itself the explicit form of the paper's asymptotic Theorem 9.

Significance

With $\tau\asymp d^{-1/4}$ a single sample already yields a linear classifier with small standard error (Theorem 8 of the paper), while Theorem 31 shows that for $\varepsilon$ of order $\tau$ every linear learner needs on the order of $\sqrt d/\log d$ samples to get expected robust error below $\tfrac12-\gamma$ against an $\ell_\infty$ adversary (the paper's Theorem 9 states this as $n\le c_2\varepsilon^2\gamma^2 d/\log(d/\gamma)$ for $\tau=c_1d^{-1/4}$ ). The companion upper bound (Theorem 10) shows that thresholding the input first makes one sample enough for any $\varepsilon<1$ . Together these give a rigorous example in which robust generalization is polynomially harder than standard generalization for a model class, and in which a change of model class removes the gap.

The theorem and its proof are published and not in doubt. The platform holds no statement of this lower bound, of Lemma 29, or of the ℓ∞/ℓ1 robustness criterion for linear classifiers (searched 2026-09-26). The mission produces a checked statement of the result with every hypothesis explicit, including the tie convention and the domain of $\varepsilon$ that the printed statement leaves implicit, and a finite, measure-free encoding of a Bayesian learning lower bound that other hypercube models can reuse.

Difficulty

The obvious attempt bounds the robust error of the best classifier the learner could output, but the learner is arbitrary: it may output any $w$ , including ones that use the samples in unusual ways. The argument must therefore hold for every function of the samples, which is why $\theta^\star$ is random and why the error is averaged over it; for a fixed $\theta^\star$ the learner $g_n\equiv\theta^\star$ is robust and the statement is false. The technical difficulty is to pass from "the posterior of every coordinate is nearly uniform" (a statement about $d$ separate one-dimensional problems) to a bound on the margin $\langle w,yx\rangle$ relative to $\|w\|_1$ that holds for every $w$ at once, uniformly in how $w$ spreads its weight across coordinates. Concentration of $\langle w,yx\rangle$ is not available for a general $w$ (a single heavy coordinate defeats it), so only a weak, constant-probability tail bound survives, which is why the final error is $\tfrac12-\gamma$ rather than close to $1$ .

Formalization scope

Everything is finite. Hypercube points are sign vectors Fin d → Bool, labels are Bool with true ↦ $+1$ , and every probability is an explicit finite sum of weights; no measure theory is involved. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d). Committed conventions:

The coordinates of $x$ are sampled independently (the reading of "sampling each coordinate" that the paper's proofs use).
$\|\cdot\|_\infty\le\varepsilon$ and $\|w\|_1$ are written coordinatewise; the adversary's ball is the $\ell_\infty$ ball, not the Euclidean one.
$f_w(x)=+1$ when $\langle w,x\rangle=0$ (the paper's $\operatorname{sgn}(0)$ is not in $\{\pm1\}$ ).
The robust error is Definition 3's event $\exists x'\in\mathcal B^\varepsilon_\infty(x),\ f(x')\ne y$ , not the margin criterion; the equivalence is milestone 4.
Added hypotheses: $\varepsilon\ge0$ in the goal (for $\varepsilon<0$ the ball is empty and the printed statement fails at $n=0$ ), and $\delta>0$ in Lemma 29 (at $\delta=0$ Lean's $\log(2/0)=0$ makes it false). Posteriors are defined by Bayes' rule as ratios of joint weights.

The learner is any function of the samples to $\mathbb R^d$ ; restricting to a specific learner, fixing $\theta^\star$ , letting the learner output an arbitrary classifier (for which the theorem is false), or bounding only the standard error ( $\varepsilon=0$ ) would each trivialize or falsify the target and are excluded. Useful infrastructure: Hoeffding's inequality for sums of independent $\pm1$ variables, Markov's inequality over finite sums, and the ℓ∞/ℓ1 duality on EuclideanSpace. Related platform work: the other three missions of this series (the Gaussian lower bound, the Gaussian robust upper bound, and the Bernoulli thresholding upper bound). Contributions of general lemmas on finite product measures over the hypercube are welcome.

Selected references

L. Schmidt, S. Santurkar, D. Tsipras, K. Talwar, A. Mądry, Adversarially Robust Generalization Requires More Data, arXiv:1804.11285v2, 2018; NeurIPS 2018. https://arxiv.org/abs/1804.11285
I. Goodfellow, J. Shlens, C. Szegedy, Explaining and Harnessing Adversarial Examples, ICLR 2015. https://arxiv.org/abs/1412.6572
A. Mądry, A. Makelov, L. Schmidt, D. Tsipras, A. Vladu, Towards Deep Learning Models Resistant to Adversarial Attacks, ICLR 2018. https://arxiv.org/abs/1706.06083
S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001

7 thms3 active usersReviewed

Completed

Control Theory Dynamical Systems Graph Theory+1·Captain: mikedeng1

On Controllability of Delayed Boolean Control Networks: Trajectory Controllability Avoiding Forbidden Trajectories Iff the Reduced Transition-Count Matrix Is IrreducibleResearch Paper

Motivation

Boolean networks model gene regulatory networks by giving each gene an on/off value and updating all values synchronously by logical rules (Kauffman, 1969). Adding external Boolean inputs gives Boolean control networks (BCNs), in which a designer (a drug, an intervention) chooses the inputs over time. The basic control-theoretic question is controllability: can the inputs drive the network from any configuration to any other? Cheng and Qi (Automatica 2009) answered it for BCNs using the semi-tensor product of matrices, which rewrites a BCN as a linear recursion on canonical basis vectors.

Biological regulation is not instantaneous: transcription and translation introduce delays, so the next value of a gene can depend on several past values. Lu, Zhong, Ho, Tang and Cao (SIAM J. Control Optim. 2016) study delayed BCNs, in which the update reads the last $\mu$ states, and give criteria for two kinds of controllability, including the case where some configurations are dangerous and must be avoided (in biology, states corresponding to disease). The mission formalizes their criteria.

Setting

Write $\mathcal D=\{0,1\}$ . A state is $x=(x_1,\dots,x_n)\in\mathcal D^n$ and an input value is $u\in\mathcal D^m$ . Fix $\mu\ge1$ . The delayed BCN (2.2) is

x_i(t+1)=f_i\big(u(t),x(t-\mu+1),\dots,x(t)\big),\qquad i=1,\dots,n,

with arbitrary Boolean functions $f_i:\mathcal D^{m+\mu n}\to\mathcal D$ , collected into one map $F$ with $x(t+1)=F(u(t),X(t))$ . A trajectory is the window $X(t)=(x(t-\mu+1),\dots,x(t))$ of the last $\mu$ states; its last entry is the current state. One step maps $X(t)$ under the input $u(t)$ to $X(t+1)=(x(t-\mu+2),\dots,x(t+1))$ . A control sequence of length $k$ is $U=(u(0),\dots,u(k-1))$ , with inputs chosen freely; $y(i)=X(i)$ denotes the trajectory after $i$ steps from an initial trajectory $y(0)$ .

The transition-count matrix $Q$ has rows and columns indexed by trajectories: $Q_{b,a}$ is the number of input values $u$ taking trajectory $a$ to trajectory $b$ in one step. For a set $C_t$ of forbidden trajectories, $Q_{C_t}$ is $Q$ with the rows and columns of $C_t$ replaced by zeros, and $\mathbb Q_{C_t}$ is $Q$ with those rows and columns deleted.

The notions of controllability are:

Trajectory controllable (Definition 3.1): from every initial trajectory, every trajectory $X_d$ equals $X(k)$ for some $k\ge1$ and some control sequence.
Trajectory controllable under $C_t$ (Definition 3.11): for all trajectories $a,b\notin C_t$ there are $k\ge0$ and a control sequence steering $y(0)=a$ to $y(k)=b$ with $y(i)\notin C_t$ for $i=0,\dots,k$ .
State controllable (Definition 4.1): from every initial trajectory, every state equals $x(k)$ for some $k>0$ and some control sequence.

A real square matrix $A$ of size $N\ge2$ is reducible (Definition 3.7) if a simultaneous permutation of rows and columns brings it to block upper-triangular form $\begin{pmatrix}A_{11}&A_{12}\\0&A_{22}\end{pmatrix}$ with square diagonal blocks; it is irreducible otherwise, so every $1\times1$ matrix is irreducible.

$\mathbb N_1(k;y_a,y_b,C_t)$ counts the control sequences of length $k$ steering $y_a$ to $y_b$ while avoiding $C_t$ ; $\mathbb N_2(k;a,b_s)$ counts those steering the initial trajectory $a$ to $x(k)=b_s$ ; $\Xi^{p}_\mu$ is the set of trajectories with current state $p$ .

Formalization targets

Goal: Theorem 3.12

\text{the delayed BCN is trajectory controllable under } C_t\iff \mathbb Q_{C_t}\ \text{is irreducible},

for every $\mu\ge1$ , $n$ , $m$ , every update map and every forbidden set $C_t$ . It is the most general criterion of the paper.

Milestones

Proposition 3.5: for $k>0$ , $\mathbb N_1(k;y_a,y_b,C_t)=y_b^{\mathsf T}(Q_{C_t})^ky_a$ .
Remark 3: $\mathbb N_1(k;y_a,y_b)=y_b^{\mathsf T}Q^ky_a$ .
Theorem 3.10: trajectory controllable $\iff$ $Q$ irreducible.
Theorem 4.3: $\mathbb N_2(k;a,b_s)=\sum_{b\in\Xi^{b_s}_\mu}b^{\mathsf T}Q^ka$ .
Theorem 5.1: the same count while avoiding forbidden states $C_s$ , with $Q$ zeroed on the trajectories containing a state of $C_s$ .
Corollary 5.3: trajectory controllability implies state controllability.

A supporting item, Lemma 3.9 (corrected form), relates Definition 3.7 to positivity of entries of powers for nonnegative matrices of size at least 2.

Significance

The criteria replace a question about control sequences of unbounded length by a finite test on one nonnegative integer matrix of size $2^{\mu n}$ . The counting identities give more than a yes/no answer: they enumerate the control sequences achieving a transfer, which is what a designer choosing among interventions needs, and they handle forbidden states by passing to forbidden trajectories.

The results are proved in the paper; none of them has a machine-checked proof. Formalizing them yields a reusable Lean model of delayed (and, for $\mu=1$ , ordinary) Boolean control networks defined directly through their dynamics, together with a checked bridge from dynamic reachability to the combinatorics of nonnegative matrices. A formal version also pins down points the printed text leaves loose: Lemma 3.9 as printed is false (it characterizes primitive, not irreducible, matrices), and the two different matrices $Q_{C_t}$ (zeroed) and $\mathbb Q_{C_t}$ (deleted) must not be confused.

Difficulty

The central step is the passage between three objects: reachability under the dynamics, positivity of entries of powers of $Q$ , and the block-triangular definition of irreducibility. The counting identity for powers of $Q$ is a statement about sequences of inputs, not about paths in a graph, so the bijection between control sequences and weighted walks has to be established with the avoidance constraint carried at every intermediate time, including the endpoints. The equivalence between Definition 3.7 and strong connectivity is the classical graph-theoretic characterization, but it has edge cases the obvious argument misses: a $1\times1$ zero matrix is irreducible by Definition 3.7 yet has no positive power, which is exactly why Definition 3.11 allows $k=0$ while Definition 3.1 does not. A proof that routes through "some power of $\mathbb Q_{C_t}$ is entrywise positive", following the printed Lemma 3.9, proves a false intermediate statement.

Formalization scope

Conventions committed to in Lean:

A state is Fin n → Bool (true is the paper's 1); a trajectory is Fin μ → State n with index 0 the oldest state and index $\mu-1$ the current state; $\mu\ge1$ is a standing assumption (NeZero μ); $n,m\ge0$ are arbitrary and no assumption is placed on the update functions.
Matrices are indexed by trajectories rather than by the paper's index $j$ of $\delta^j_{2^{\mu n}}$ . The paper's $Q=L\ltimes\mathbf 1_{2^m}$ is obtained by the simultaneous relabelling of Lemma 2.6, and every statement (entries of powers, sums over sets of trajectories, Definition 3.7) is invariant under it. $\mathbb Q_{C_t}$ is indexed by the subtype of allowed trajectories.
Irreducibility is Definition 3.7 applied to the matrix with entries cast to $\mathbb R$ ; it is not Mathlib's Matrix.IsIrreducible, which differs on $1\times1$ matrices.
Pinned readings: Definition 3.1 and Definition 4.1 use $k\ge1$ ; Definition 3.11 uses $k\ge0$ ; Proposition 3.5, Theorem 4.3 and Theorem 5.1 are stated for $k>0$ (Proposition 3.5 is false at $k=0$ when $y_a=y_b\in C_t$ ); Remark 3 holds for all $k\ge0$ . "Avoiding $C_s$ " in Theorem 5.1 means that no state $x(i)$ , $i=1-\mu,\dots,k$ , lies in $C_s$ , which is the theorem's own middle term $\mathbb N_1(k;a,b,\Xi^{C_s})$ . $\Xi^p_\mu$ is defined semantically by eq. (4.3), since the printed index range in (4.4) is a misprint. Lemma 3.9 is included in corrected form with $N\ge2$ .

Controllability is defined through the dynamics and control sequences, never as positivity of entries of powers of $Q$ ; a formalization that defines reachability by $(Q^k)_{b,a}>0$ would reduce Theorems 3.10 and 3.12 to library facts and is ruled out.

Needed infrastructure: the correspondence between control sequences and products of entries of $Q$ (the core of Proposition 3.5), and the equivalence of Definition 3.7 with strong connectivity of the support graph for nonnegative matrices (Mathlib's Matrix.IsIrreducible, Matrix.isIrreducible_iff_exists_pow_pos and Matrix.pow_apply_pos_iff_nonempty_path cover much of the second part for sizes at least 2). Both are reusable beyond this mission, for ordinary BCNs, probabilistic BCNs and finite automata. Contributions of either piece, or of the semi-tensor-product bridge identifying $Q$ with $L\ltimes\mathbf 1_{2^m}$ , are welcome.

Selected references

J. Lu, J. Zhong, D. W. C. Ho, Y. Tang, J. Cao, On Controllability of Delayed Boolean Control Networks, SIAM J. Control Optim. 54(2):475–494, 2016. https://doi.org/10.1137/140991820
D. Cheng, H. Qi, Controllability and observability of Boolean control networks, Automatica 45(7):1659–1667, 2009. https://doi.org/10.1016/j.automatica.2009.03.006
S. A. Kauffman, Metabolic stability and epigenesis in randomly constructed genetic nets, J. Theoret. Biol. 22(3):437–467, 1969. https://doi.org/10.1016/0022-5193(69)90015-0
A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM Classics in Applied Mathematics 9, 1994. https://doi.org/10.1137/1.9781611971262

9 thms3 active usersReviewed

Completed

Convex Optimization Linear Optimization Operations Research+1·Captain: mikedeng1

Cones of Matrices and Set-Functions and 0–1 Optimization I: n Rounds of the Lovász–Schrijver N Operator Give the 0–1 HullResearch Paper

Motivation

A 0–1 integer program asks for the best 0–1 vector satisfying a system of linear inequalities. Its linear relaxation is easy to optimize over, but the relaxation is usually much larger than the convex hull of the 0–1 solutions. Lift-and-project methods close this gap systematically: they lift the relaxation to a higher-dimensional space, add constraints that every 0–1 point satisfies there, and project back, obtaining a tighter relaxation that still contains every 0–1 solution.

L. Lovász and A. Schrijver introduced one of the two standard lift-and-project hierarchies in Cones of matrices and set-functions and 0–1 optimization (SIAM J. Optim., 1991). Their operators $N$ and $N_+$ represent a 0–1 point $x$ by the matrix $xx^{\mathsf T}$ , impose linear (and for $N_+$ semidefinite) constraints on such matrices, and project back to $\mathbb R^{n+1}$ . The same paper applies the operators to the stable set polytope, where one round already produces the odd hole, odd wheel, clique and odd antihole constraints. The Lovász–Schrijver hierarchy, the Sherali–Adams hierarchy (1990) and Lasserre's semidefinite hierarchy (2001) are the three reference lift-and-project methods; their rank lower bounds are a standard tool for proving that a relaxation cannot solve a combinatorial problem in few rounds.

This mission formalizes the first structural fact about the operator $N$ : iterating it $n$ times on any relaxation in $n$ variables yields exactly the 0–1 hull (Theorem 1.4 of the paper).

Setting

Vectors live in $\mathbb R^{n+1}$ with coordinates $x_0, x_1, \dots, x_n$ ; the space $\mathbb R^n$ of the original problem is the hyperplane $x_0 = 1$ , and polytopes are replaced by the convex cones they generate.

A convex cone is a nonempty set closed under addition and nonnegative scaling. For a set $S$ , $\operatorname{cone}(S)$ is the set of nonnegative combinations of finitely many vectors of $S$ .
The polar cone of $K$ is $K^* = \{u : u^{\mathsf T}x \ge 0 \text{ for all } x \in K\}$ .
A 0–1 vector has every coordinate, $x_0$ included, equal to $0$ or $1$ . The cube cone $Q$ is the cone spanned by the 0–1 vectors with $x_0 = 1$ ; it is the cone over the unit cube.
For a convex cone $K$ , $K^\circ$ is the cone spanned by the 0–1 vectors in $K$ . For $K \subseteq Q$ this is the cone over the convex hull of the 0–1 points of the relaxation.

For convex cones $K_1, K_2 \subseteq Q$ , the matrix cone $M(K_1, K_2)$ consists of the $(n+1)\times(n+1)$ real matrices $Y = (y_{ij})$ such that

$Y$ is symmetric;
$y_{ii} = y_{0i}$ for $1 \le i \le n$ (the diagonal equals the 0th column);
$u^{\mathsf T} Y v \ge 0$ for every $u \in K_1^*$ and $v \in K_2^*$ .

$M_+(K_1, K_2)$ adds the condition that $Y$ is positive semidefinite. The projections are $N(K_1, K_2) = \{Ye_0 : Y \in M(K_1, K_2)\}$ and $N_+(K_1, K_2) = \{Ye_0 : Y \in M_+(K_1, K_2)\}$ , where $e_0$ is the 0th unit vector. The cut operator is $N(K) = N(K, Q)$ , and its iterates are $N^0(K) = K$ , $N^t(K) = N(N^{t-1}(K))$ .

Two families of hyperplanes appear in the proofs: $H_i = \{x : x_i = 0\}$ and $G_i = \{x : x_i = x_0\}$ , the hyperplanes through the two opposite facets of $Q$ in direction $i$ .

Formalization targets

Goal: Theorem 1.4

For every closed convex cone $K \subseteq Q$ ,

N^n(K) = K^\circ .

The statement is uniform in $n$ and in $K$ : no polyhedrality, no bound on the number of constraints, and no assumption that $K$ contains a 0–1 point.

Milestones

Condition (iii″). For a closed convex cone $K \subseteq Q$ and a symmetric $Y$ with $y_{ii} = y_{0i}$ : $Y \in M(K, Q)$ if and only if every column of $Y$ is in $K$ and the difference of the first column and any other column is in $K$ .
Lemma 1.1. For closed convex cones $K_1, K_2 \subseteq Q$ ,

(K_1 \cap K_2)^\circ \subseteq N_+(K_1, K_2) \subseteq N(K_1, K_2) \subseteq K_1 \cap K_2 .

Lemma 1.3. For a closed convex cone $K \subseteq Q$ and every $1 \le i \le n$ ,

N(K) \subseteq (K \cap H_i) + (K \cap G_i).

Claim (4) in the proof of Theorem 1.4. For every set $T$ of $t \ge 1$ coordinates, with $\bar F$ the union of the faces of the unit cube that fix the coordinates in $T$ to $0$ or $1$ ,

N^t(K) \subseteq \operatorname{cone}(K \cap \bar F).

The remark after Lemma 1.1. $N(K_1 \cap K_2, K_1 \cap K_2) \subseteq N(K_1, K_2) \subseteq N(K_1 \cap K_2, Q)$ .

Significance

Theorem 1.4 is what makes $N$ a hierarchy rather than a single cut: the relaxations $K \supseteq N(K) \supseteq N^2(K) \supseteq \dots$ reach the 0–1 hull after at most $n$ rounds, so the $N$ -rank of a valid inequality (the least $t$ with the inequality valid for $N^t(K)$ ) is a well-defined number between $0$ and $n$ . The rest of the paper measures combinatorial constraints by this rank: odd hole constraints have rank one on the stable set polytope, and the rank of a stable set inequality is bounded by its defect. Rank lower bounds for lift-and-project hierarchies, in the literature that followed, all presuppose this finite convergence.

The theorem is proved in the paper; to the best of available knowledge none of the Lovász–Schrijver operators has been formalized in a proof assistant. A formalization provides machine-checked definitions of the matrix cones and the cut operators that later missions in this series (odd holes, the defect bound, the $N_+$ constraints) state their results against, and a checked proof of the column characterization (iii″) that all of those proofs use.

Difficulty

The inclusion $K^\circ \subseteq N^n(K)$ follows from Lemma 1.1 once each $N^t(K)$ is known to be a convex cone. The reverse inclusion is the content. A first attempt shows that one round of $N$ forces one coordinate to be integral, and then iterates; but $N(K)$ is not contained in the union of $K \cap H_i$ and $K \cap G_i$ , only in their Minkowski sum (Lemma 1.3), so a point of $N(K)$ is not itself integral in any coordinate. The induction must carry a statement about cones spanned by intersections with unions of cube faces, and it needs each iterate $N^t(K)$ to again be a closed convex cone inside $Q$ so that Lemma 1.3 can be reapplied. Closedness of the projection $N(K)$ is not automatic: a linear image of a closed cone need not be closed.

Formalization scope

Coordinates of $\mathbb R^{n+1}$ are indexed by Option ι for a finite type ι; none is $x_0$ and some i is $x_i$ , and $n$ is the cardinality of ι, which may be $0$ .
$\operatorname{cone}(S)$ is Mathlib's PointedCone.hull ℝ S; $Q$ and $K^\circ$ are defined as spans of 0–1 vectors, as on the page, not by the inequality description $0 \le x_i \le x_0$ .
$M(K_1, K_2)$ is defined by condition (iii) through the polar cones; the column form (iii″) is a milestone, not the definition.
The operators $N$ , $N_+$ and the iterates are defined on arbitrary sets; the hypotheses (convex cone, contained in $Q$ , closed) are carried by the theorems.
Closedness. The paper tacitly takes its cones closed (they are polyhedral in all its applications), and the rewriting (iii′) on p. 169 needs it. Every statement here assumes the cones closed. Without this the goal is false: for $K = \{x : 0 < x_1 < x_0\} \cup \{0\}$ in $\mathbb R^2$ , $K^\circ = \{0\}$ while $N(K) = Q$ .
In the proof of Theorem 1.4 the page places the cube $Q'$ in the hyperplane " $x_0 = 0$ "; this is a misprint for $x_0 = 1$ , and claim (4) is formalized with $x_0 = 1$ .
Not formalized in this mission: Lemma 1.2 (the dual description of $N(K)^*$ ), Lemma 1.5 (the $N_+$ analogue of Lemma 1.3, part of a later mission), and the algorithmic results of Section 1.c.

Contributions welcome: proofs that $N(K)$ is a closed convex cone contained in $Q$ whenever $K$ is, a proof of $Q^* = \operatorname{cone}\{e_i, e_0 - e_i\}$ , and lemmas on cones spanned by the intersection of a generating set with a supporting hyperplane; these are reusable by the other missions of the series.

Selected references

L. Lovász and A. Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM Journal on Optimization 1(2) (1991) 166–190. https://doi.org/10.1137/0801013
H. D. Sherali and W. P. Adams, A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems, SIAM Journal on Discrete Mathematics 3(3) (1990) 411–430. https://doi.org/10.1137/0403036
J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM Journal on Optimization 11(3) (2001) 796–817. https://doi.org/10.1137/S1052623400366802
M. Laurent, A comparison of the Sherali–Adams, Lovász–Schrijver, and Lasserre relaxations for 0–1 programming, Mathematics of Operations Research 28(3) (2003) 470–496. https://doi.org/10.1287/moor.28.3.470.16391

8 thms3 active usersReviewed

Completed

Control Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Supervisory Control of a Class of Discrete Event Processes I: Minimally Restrictive Supervisors Exist iff the Supremal Controllable Legal Sublanguage Contains the Minimal Acceptable LanguageResearch Paper

Motivation

Manufacturing cells, communication protocols, traffic systems and database transaction managers are naturally described not by differential equations but by sequences of discrete events: a machine starts, a part arrives, a message is lost. Ramadge and Wonham's 1987 paper (SIAM J. Control Optim. 25(1)) set up a control theory for such systems in which the plant is an automaton, the controller is another automaton that may disable some events, and specifications are formal languages. The framework, now called supervisory control theory or the Ramadge–Wonham framework, is the standard model for the logical control of discrete event systems and underlies the textbook treatment in Cassandras and Lafortune (Introduction to Discrete Event Systems, 2008) and Wonham and Cai (Supervisory Control of Discrete-Event Systems, 2019).

The question the paper answers is the basic synthesis question of the theory: given a plant, a set of legal behaviours and a set of minimally acceptable behaviours, when does a controller exist that keeps the plant legal, achieves at least the acceptable behaviour, and never deadlocks, and what is the least restrictive such controller?

Setting

A generator is $\mathcal G = (Q, \Sigma, \delta, q_0, Q_m)$ with a state set $Q$ , a finite alphabet $\Sigma$ of events, a partial transition function $\delta : \Sigma \times Q \to Q$ , an initial state $q_0$ and marker states $Q_m \subseteq Q$ . Extending $\delta$ to strings, the generated language $L(\mathcal G)$ is the set of strings $w$ for which $\delta(w, q_0)$ is defined, and the marked language $L_m(\mathcal G)$ is the subset of those that end in $Q_m$ . The closure $\bar K$ of a language $K$ is its set of prefixes; $K$ is closed if $K = \bar K$ . Throughout, $\mathcal G$ is assumed trim in the sense $L(\mathcal G) = \bar L_m(\mathcal G)$ : every generated string can be completed to a marked one.

The alphabet is split into controllable events $\Sigma_c$ and uncontrollable events $\Sigma_u = \Sigma - \Sigma_c$ . A supervisor $\mathcal S = (S, \phi)$ consists of a deterministic, accessible automaton $S = (X, \Sigma, \xi, x_0, X_m)$ , whose state set $X$ may be infinite, and a map $\phi$ assigning to each state $x$ the set of controllable events it enables; uncontrollable events are always enabled. The closed loop $\mathcal S/\mathcal G$ runs $S$ and $\mathcal G$ in lockstep: an event occurs when the plant can execute it, the supervisor enables it, and the supervisor's automaton can follow it. This defines the languages $L(\mathcal S/\mathcal G)$ , $L_m(\mathcal S/\mathcal G)$ and the controlled language $L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G) \cap L_m(\mathcal G)$ .

$\mathcal S$ is complete if its automaton never refuses an event that the plant can execute and $\phi$ enables; it is proper if it is complete and

\bar L_m(\mathcal S/\mathcal G) = \bar L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G),

that is, every closed-loop string can be completed to a marked task. A language $K$ is controllable if $K \subseteq L(\mathcal G)$ and $\bar K \Sigma_u \cap L(\mathcal G) \subseteq \bar K$ . For $L \subseteq L(\mathcal G)$ , $\mathbf C_{\mathcal G}(L)$ is the class of controllable sublanguages of $L$ and $\mathbf F_{\mathcal G}(L)$ the class of sublanguages $K$ of $L$ with $K = \bar K \cap L_m(\mathcal G)$ .

Given $\emptyset \neq L_a \subseteq L_g \subseteq L_m(\mathcal G)$ , the Supervisory Marking Problem (SMP) asks for a proper $\mathcal S$ with $L_a \subseteq L_m(\mathcal S/\mathcal G) \subseteq L_g$ , and the Supervisory Control Problem (SCP) for a proper $\mathcal S$ with $L_a \subseteq L_c(\mathcal S/\mathcal G) \subseteq L_g$ .

Formalization targets

Goal: Theorem 7.1 (pp. 218–219)

\text{SMP solvable} \iff \sup \mathbf C_{\mathcal G}(L_g) \supseteq L_a, \qquad \text{SCP solvable} \iff \sup\{\mathbf C_{\mathcal G}(L_g) \cap \mathbf F_{\mathcal G}(L_g)\} \supseteq L_a,

and in each case the solving supervisor can be taken minimally restrictive: its marked (respectively controlled) language equals the supremal element and contains that of every proper supervisor whose language lies in $L_g$ .

Milestones

Proposition 4.1 (i), (ii): marking is independent of control; every $K \subseteq L_m(\mathcal G)$ , or $K \subseteq L \cap L_m(\mathcal G)$ for an achievable closed $L$ , is the marked language of a complete supervisor.
Proposition 5.1: a complete supervisor realizes $(L_m, L_c, L) = (K_1, K_2, K_3)$ iff $K_1 \subseteq K_2$ , $K_2 = K_3 \cap L_m(\mathcal G)$ and $K_3$ is closed and controllable.
Theorem 6.1 (i), (ii): a proper supervisor with $L_m(\mathcal S/\mathcal G) = K$ exists iff $K$ is controllable; one with $L_c(\mathcal S/\mathcal G) = K$ exists iff $K$ is controllable and $L_m(\mathcal G)$ -closed.
Proposition 7.1: $\mathbf C_{\mathcal G}(L)$ and $\mathbf F_{\mathcal G}(L)$ contain $\emptyset$ and are closed under arbitrary unions.
The supremal elements (p. 218): $\sup \mathbf C_{\mathcal G}(L)$ , $\sup \mathbf F_{\mathcal G}(L)$ and $\sup\{\mathbf C_{\mathcal G}(L) \cap \mathbf F_{\mathcal G}(L)\}$ belong to their classes.

Significance

Theorem 7.1 reduces the existence of a correct, non-blocking controller to a single language inclusion, and identifies the supremal controllable sublanguage as the behaviour of the least restrictive solution. That object is the backbone of the later theory: modular and decentralized control, control under partial observation, and the computational results that $\sup \mathbf C_{\mathcal G}(L)$ is regular and computable when $\mathcal G$ is finite and $L$ regular all start from it.

The result is proved in the paper and has been taught for decades; it is not open. Mathlib has no model of generators with partial transitions, supervisors or controllability (its DFA has a total transition function and a single accepted language), and no formalization of this theory exists on the platform. This mission provides one: a reusable Lean model of generators with partial transitions, supervisors with possibly infinite state, closed loops and controllability, together with the paper's existence theorems stated against it. A second mission on the same paper (quotients of supervisors, Theorem 10.1) builds on the same objects.

Difficulty

The combinatorial core of Proposition 7.1 is a short prefix-closure computation. The work lies in the constructions: to show existence, a supervisor must be built for an arbitrary controllable language, which in general is not regular, so the supervisor needs an infinite state set (for example strings of the target language) together with a proof that the closed loop generates exactly the intended language, is complete, and is proper. The converse directions require relating the closed-loop run to separate runs of the plant and of the supervisor's automaton. The naive shortcut of reading the "sup" as an arbitrary member of $\mathbf C_{\mathcal G}(L_g)$ containing $L_a$ skips the content of the supremal-element milestone; the goal is stated with the actual union.

Formalization scope

The alphabet is a type α with [Fintype α]; strings are List α, the empty string is [], and $s\sigma$ is s ++ [σ]. Languages are Set (List α); the closure is pre K = {s | ∃ t, s ++ t ∈ K}.
A generator is a structure with a state type Q : Type, a partial transition δ : α → Q → Option Q, an initial state and a marker set. No finiteness is assumed on states, of the plant or of the supervisor. Supervisors and generators live in Type 1.
$\phi$ maps states to Ec → Bool; an event outside $\Sigma_c$ is enabled by definition, so uncontrollable events cannot be disabled.
The closed loop is the product run from $(x_0, q_0)$ ; the accessible part in the paper's display (2.1) changes no language and is not built.
Standing assumptions carried by every theorem: $\Sigma$ finite, $L(\mathcal G) = \bar L_m(\mathcal G)$ , supervisor automata accessible (as a hypothesis on every input supervisor and a conjunct of every "there exists a supervisor").
$\sup$ is sSup in the complete lattice Set (List α).
A formalization in which the closed loop ignores $\phi$ or the plant, in which completeness is dropped from properness, or in which the supervisor is restricted to finitely many states, is not the paper's theorem and is ruled out by the definitions above.

Welcome contributions: the basic run lemmas (closed-loop runs project to plant and supervisor runs), the string-state supervisor construction, and proofs of the milestones in the given order.

Selected references

P. J. Ramadge and W. M. Wonham, Supervisory Control of a Class of Discrete Event Processes, SIAM J. Control Optim. 25(1):206–230, 1987. https://doi.org/10.1137/0325013
W. M. Wonham and P. J. Ramadge, On the Supremal Controllable Sublanguage of a Given Language, SIAM J. Control Optim. 25(3):637–659, 1987. https://doi.org/10.1137/0325036
C. G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems, 2nd ed., Springer, 2008. https://doi.org/10.1007/978-0-387-68612-7
W. M. Wonham and K. Cai, Supervisory Control of Discrete-Event Systems, Springer, 2019. https://doi.org/10.1007/978-3-319-77452-7

12 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Linear algebra+2·Captain: mikedeng1

Approximating Clique-Width and Branch-Width: Well-Linked Sets Certify Clique-WidthResearch Paper

Motivation

Clique-width is a graph parameter introduced by Courcelle and Olariu (Discrete Appl. Math. 101 (2000)) that measures how far a graph is from being built by a few labelled operations. Every problem expressible in monadic second-order logic with quantification over vertices and vertex sets (MSO $_1$ ) can be solved in linear time on graphs given together with a decomposition of bounded clique-width (Courcelle, Makowsky and Rotics, Theory Comput. Syst. 33 (2000)). Bounded clique-width is more general than bounded tree-width: complete graphs have unbounded tree-width but clique-width $2$ .

For fixed $k$ there was, before this paper, no polynomial-time algorithm that either decides that a graph has clique-width at least $k+1$ or outputs a decomposition of clique-width bounded by a function of $k$ ; the best known algorithm, by Johansson (2001), gave width $2k\log n$ . Oum and Seymour (J. Combin. Theory Ser. B 96 (2006)) closed this gap with approximation $2^{3k+2}-1$ , through rank-width and a factor-3 approximation for the branch-width of symmetric submodular functions.

Timeline:

1991: Robertson and Seymour introduce branch-width of graphs and hypergraphs (J. Combin. Theory Ser. B 52).
2000: Courcelle and Olariu define clique-width; Courcelle, Makowsky and Rotics solve MSO $_1$ problems on graphs given with a $k$ -expression.
2001: Johansson gives a $2k\log n$ approximation.
2006: Oum and Seymour define rank-width, prove $\mathrm{rwd}(G) \le \mathrm{cwd}(G) \le 2^{\mathrm{rwd}(G)+1}-1$ , and give an $O(n^9 \log n)$ algorithm that outputs a $(2^{3k+2}-1)$ -expression or certifies clique-width above $k$ .

Setting

All graphs are finite and simple. For a finite set $V$ , a function $f : 2^V \to \mathbb{Z}$ is submodular if $f(X)+f(Y) \ge f(X\cap Y)+f(X\cup Y)$ and symmetric if $f(X) = f(V\setminus X)$ .

A branch-decomposition of $f$ is a pair $(T, L)$ where $T$ is a tree with at least two vertices and all degrees at most $3$ , and $L$ is a bijection from $V$ onto the leaves of $T$ . Removing an edge $e$ of $T$ splits the leaves in two; the width of $e$ is $f$ of the set of elements of $V$ on one side. The width of $(T, L)$ is the largest edge width, and the branch-width $\mathrm{bw}(f)$ is the least width of a branch-decomposition, with $\mathrm{bw}(f) = f(\emptyset)$ when $|V| \le 1$ .

A set $W \subseteq V$ is well-linked with respect to $f$ if for every partition $(X, Y)$ of $W$ and every $Z$ with $X \subseteq Z \subseteq V\setminus Y$ , $f(Z) \ge \min(|X|, |Y|)$ .

Let $A(G)$ be the adjacency matrix of $G$ over $\mathrm{GF}(2)$ . For disjoint $X, Y \subseteq V(G)$ , $\mathrm{cutrk}^*_G(X, Y)$ is the rank of the submatrix of $A(G)$ with rows $X$ and columns $Y$ , and the cut-rank function is $\mathrm{cutrk}_G(X) = \mathrm{cutrk}^*_G(X, V(G)\setminus X)$ . The rank-width $\mathrm{rwd}(G)$ is $\mathrm{bw}(\mathrm{cutrk}_G)$ .

A $k$ -expression is a term built from constants $\cdot_i$ (a vertex with label $i \in \{1,\dots,k\}$ ), the operators $\eta_{i,j}$ ( $i \ne j$ ; add all edges between labels $i$ and $j$ ), $\rho_{i\to j}$ (relabel $i$ into $j$ ) and disjoint union $\oplus$ . Its value is the labelled graph it produces; $G$ has clique-width $\mathrm{cwd}(G) \le k$ if some $k$ -expression has value isomorphic to $G$ .

An interpolation of $f$ is a function $f^*$ on disjoint pairs $(X, Y)$ that agrees with $f$ on $(X, V\setminus X)$ , is monotone, submodular in the sense $f^*(A,B)+f^*(C,D) \ge f^*(A\cap C, B\cup D) + f^*(A\cup C, B\cap D)$ , and has $f^*(\emptyset,\emptyset)=f(\emptyset)$ .

Formalization targets

Goal: Theorem 1.1, certificate form

For a graph $G$ with at least one vertex and an integer $k \ge 1$ :

\exists\, W,\ |W| = 3k+1,\ W \text{ well-linked for } \mathrm{cutrk}_G \;\Longrightarrow\; \mathrm{cwd}(G) \ge k+1,

\nexists\, W,\ |W| = 3k+1,\ W \text{ well-linked for } \mathrm{cutrk}_G \;\Longrightarrow\; \mathrm{cwd}(G) \le 2^{3k+2}-1.

The same explicit condition decides which side of the approximation holds; this is what the paper's algorithm certifies.

Milestones

Proposition 4.1: properties of an interpolation, including that $X \mapsto f^*(X, B) - f(\emptyset)$ is a matroid rank function on $V\setminus B$ when $f(\{v\}) - f(\emptyset) \le 1$ .
Proposition 4.2: $f_{\min}(X,Y) = \min_{X\subseteq Z\subseteq V\setminus Y} f(Z)$ is an interpolation.
Theorem 5.1: a well-linked set of size $k$ forces $\mathrm{bw}(f) \ge k/3$ (for $k \ne 1$ ).
Theorem 5.2: no well-linked set of size $k$ implies $\mathrm{bw}(f) \le k$ , when $f(\{v\}) \le 1$ .
Proposition 6.1: $\mathrm{rk}\,M[X_1,Y_1] + \mathrm{rk}\,M[X_2,Y_2] \ge \mathrm{rk}\,M[X_1\cup X_2, Y_1\cap Y_2] + \mathrm{rk}\,M[X_1\cap X_2, Y_1\cup Y_2]$ .
Corollary 6.2: submodularity of $\mathrm{cutrk}^*_G$ and $\mathrm{cutrk}_G$ .
Section 6 claim: $\mathrm{cutrk}_G$ is symmetric submodular and $\mathrm{cutrk}^*_G$ interpolates it.
Proposition 6.3: $\mathrm{rwd}(G) \le \mathrm{cwd}(G) \le 2^{\mathrm{rwd}(G)+1}-1$ .

Significance

The dichotomy turns clique-width, for which no exact polynomial algorithm is known even for fixed $k$ , into a parameter that can be approximated with an explicit witness in each direction. Downstream, every algorithm for graphs of bounded clique-width that needs a $k$ -expression as input becomes applicable to graphs given without one, at the cost of an exponential blow-up of the width.

The result is proved in the literature; this mission formalizes it. To our knowledge none of the objects involved — branch-width of set functions, rank-width, cut-rank, $k$ -expressions, clique-width — has been formalized in Mathlib, and the submodularity of submatrix rank (Proposition 6.1) is absent from Mathlib's Matrix.rank API. The formal development would give reusable definitions of branch-decompositions of arbitrary integer set functions, of cut-rank, and of clique-width, and a machine-checked link between the combinatorial and the linear-algebraic width parameters.

Difficulty

The upper bound in Theorem 5.2 is the core. The natural approach, growing a branch-decomposition one leaf split at a time while keeping the width at most $k$ , gets stuck at a leaf carrying a set $B$ with $f(B) = k$ : a split of $B$ into two parts of $f$ -value below $k$ has to be found, and it must be found from the failure of well-linkedness of a set that is not obviously related to $B$ . The paper's device is the interpolation $f^*$ , which attaches a matroid to $B$ whose base has exactly $f(B)$ elements. Formalizing this requires handling partial branch-decompositions, their extensions, and a maximality argument over trees, none of which exists in Mathlib.

Proposition 6.3's upper bound is a second, independent difficulty: a rank-decomposition must be converted into a $k$ -expression by an induction over a rooted binary tree, with a relabelling argument bounding the number of labels by the number of distinct nonzero rows of a $\mathrm{GF}(2)$ matrix of rank $k$ . Its lower bound needs the tree structure of a $k$ -expression to be read as a branch-decomposition.

Formalization scope

The ground set is a Fintype V with DecidableEq V; subsets are Finset V; set functions are Finset V → ℤ, as in the paper. A branch-decomposition is a tree T : SimpleGraph (Fin n) with $n \ge 2$ , all neighbour sets of size at most $3$ , and an injective map $L$ from $V$ onto the vertices of degree $1$ ; the side of an edge $uw$ is found by reachability from $u$ after deleting $uw$ . Branch-width, rank-width and clique-width are never computed as minima: " $\mathrm{bw}(f) \le k$ " is the predicate " $|V| \le 1$ and $f(\emptyset) \le k$ , or a branch-decomposition of width at most $k$ exists", lower bounds say that every branch-decomposition has a wide edge, and " $\mathrm{cwd}(G) \le k$ " is " $G$ has a $k$ -expression". Labels $\{1,\dots,k\}$ are Fin k. The value of a $k$ -expression has as vertex type the occurrences of constants (a nested sum type), and $\eta_{i,j}$ requires $i \ne j$ . Cut-rank uses Matrix.rank over ZMod 2 of submatrices of SimpleGraph.adjMatrix. An interpolation is a function on all pairs of subsets whose axioms are imposed on disjoint pairs only.

Running time is not formalized. The paper's Theorem 1.1 asserts an $O(n^9\log n)$ algorithm; there is no cost model on the page, and the goal states the certificate the algorithm returns instead. Without the running time, " $\mathrm{cwd}(G) \ge k+1$ or $\mathrm{cwd}(G) \le 2^{3k+2}-1$ " holds for every graph, so that reading is ruled out as a formalization of the goal; so are well-linkedness with respect to anything other than $\mathrm{cutrk}_G$ , widths defined by an unguarded infimum (which is $0$ on an empty family), $k$ -expressions whose value is not the graph up to isomorphism or whose $\eta$ may join equal labels, and Theorem 5.1 stated for $k = 1$ .

Correction of Theorem 5.1. As printed, Theorem 5.1 fails for $k = 1$ : a singleton is always well-linked, but the edgeless graph on two vertices has cut-rank identically $0$ and branch-width $0 < 1/3$ . The milestone carries the hypothesis $k \ne 1$ ; the goal uses the theorem only at size $3k+1 \ge 4$ .

The graph with no vertex is excluded from the goal and from the upper bound of Proposition 6.3, since it has no $k$ -expression for any $k$ . Contributions welcome: proofs of the milestones, lemmas on branch-decompositions (suppressing degree-2 vertices, extending partial decompositions), and submatrix-rank submodularity, which is reusable beyond this mission.

Selected references

S. Oum and P. Seymour, Approximating clique-width and branch-width, J. Combin. Theory Ser. B 96 (2006) 514–528. https://doi.org/10.1016/j.jctb.2005.10.006
B. Courcelle and S. Olariu, Upper bounds to the clique width of graphs, Discrete Appl. Math. 101 (2000) 77–114. https://doi.org/10.1016/S0166-218X(99)00184-5
B. Courcelle, J. A. Makowsky and U. Rotics, Linear time solvable optimization problems on graphs of bounded clique-width, Theory Comput. Syst. 33 (2000) 125–150. https://doi.org/10.1007/s002249910009
N. Robertson and P. D. Seymour, Graph minors. X. Obstructions to tree-decomposition, J. Combin. Theory Ser. B 52 (1991) 153–190. https://doi.org/10.1016/0095-8956(91)90061-N

14 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

Approximation Algorithms for Combinatorial Problems V: The Overlap-Ratio Greedy C2 Is Within 1 + ln k of the Least-Overlap Cover on EC(k)Research Paper

Motivation

David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9 (1974) 256–278) was one of the first systematic worst-case analyses of polynomial-time heuristics for NP-complete optimization problems. Its Section 5 proves the harmonic bound $\sum_{j=1}^k 1/j$ for the greedy algorithm on minimum-cardinality set cover, a result that still underlies the standard $\ln n$ approximation guarantee.

Section 6, the subject of this mission, asks what happens when the cost of a cover is its total size rather than its number of sets. This problem, SET COVERING II (EC), is the optimization version of the EXACT COVER recognition problem of Karp's list (Karp 1972): a family has a disjoint subcover exactly when the optimum equals the number of covered points. Johnson shows that the change of measure breaks the cardinality greedy but that a greedy rule based on an overlap ratio recovers essentially the same guarantee. The same accounting (paying for each newly covered point) later became the standard analysis of greedy weighted set cover (Chvátal 1979).

Setting

An input is a finite family $F = \{S_1, \dots, S_p\}$ of finite sets. Its covered set is $T = \bigcup_{S \in F} S$ . A subcover is a subfamily $F' \subseteq F$ with $\bigcup_{S\in F'} S = T$ , and its measure is

m_{EC}(F') = \sum_{S \in F'} |S|.

The optimum $F^*$ is the least measure of a subcover; since every subcover has measure at least $|T|$ , an optimal subcover is one with the least possible overlapping. The subproblem EC $(k)$ admits only families in which every set has at most $k$ points.

Algorithm C2 keeps a subfamily SUB (initially empty), the unused sets LEFT (initially $F$ ) and the uncovered points UNCOV (initially $T$ ). While UNCOV is nonempty it chooses $S' \in$ LEFT minimizing

\mathrm{Ratio}(S) = \frac{|S - \mathrm{UNCOV}|}{|S \cap \mathrm{UNCOV}|},

the number of already-covered points of $S$ per newly covered point, and moves $S'$ from LEFT to SUB, removing its points from UNCOV. When several sets tie, any of them may be chosen; a subcover is choosable by C2 if some sequence of admissible choices returns it.

The overlap of a chosen set is $|S' - \mathrm{UNCOV}|$ at the moment it is chosen, and the cumulative overlap $\mathrm{OV}(F_1)$ of a run returning $F_1$ is the sum of these overlaps.

Formalization targets

Goal: Theorem 6 (p. 271)

For all $k \ge 1$ and $n > 0$ ,

R[C2, EC(k)](n) \le 1 + \ln(k) \le \sum_{j=1}^k \frac1j + \frac12,

and for all sufficiently large $n$ , $R[C2, EC(k)](n) \ge \sum_{j=1}^k (1/j)$ . In the size-free form used here, for every $k \ge 1$ :

every subcover $M$ choosable by C2 on an input of EC $(k)$ satisfies $m_{EC}(M) \le (1 + \ln k)\,F^*$ ;
$1 + \ln k \le \sum_{j=1}^k 1/j + 1/2$ ;
some input of EC $(k)$ with $F^* > 0$ has a choosable subcover with $m_{EC}(M) \ge \big(\sum_{j=1}^k 1/j\big) F^*$ .

Milestones (proof of Theorem 6, pp. 271–272)

the measure of the output is $|T| + \mathrm{OV}(F_1)$ ;
if C2 may choose a set with $\mathrm{Ratio}(S') \ge y$ , then $(y+1)\,|\mathrm{UNCOV}| \le F^*$ ;
with $a = F^*/|T|$ and $x = |T - \mathrm{UNCOV}|/|T|$ , the next chosen set has $\mathrm{Ratio}(S') \le a/(1-x) - 1$ ;
on EC $(k)$ , $\mathrm{OV}(F_1) \le |T|\,(a[\ln(k) + 1] - 1)$ ;
the analytic inequality $1 + \ln(k) \le \sum_{j=1}^k 1/j + 1/2$ ;
the lower-bound input (Fig. 1 of the paper with every set of $F_1$ filled out to exactly $k$ points) on which C2 may pay $\sum_{j=1}^k 1/j$ times the optimum.

Significance

The result. The measure $\sum|S|$ penalizes overlap, and the paper notes (without proof, p. 270) that an algorithm returning an optimal cover for the cardinality measure can be a factor $k$ from optimal for this one. Theorem 6 shows that the ratio rule C2 is within $1 + \ln k$ of the least-overlap cover, and the lower bound shows that no analysis of C2 can beat $\sum_{j=1}^k 1/j$ . The two bounds differ by less than $1/2$ for every $k$ . The theorem was an early instance of a logarithmic guarantee for a weighted covering problem, where each set's cost is its size.

Formalizing it. The theorem has been proved since 1974; no machine-checked proof is known to exist. The mission produces a formal model of the EC problem and of C2 as a nondeterministic process, the overlap identity, and the discrete form of the paper's area-under-a-curve estimate. The last is the part the paper argues informally, through a step function and an integral.

Difficulty

The cardinality argument for C1 counts the sets chosen; here the sets have different sizes, so it does not apply. The overlap C2 pays per newly covered point is not bounded by a constant: early choices can be free and late ones cost up to $k-1$ per point, and the bound on the cumulative overlap must hold against the whole run, for every sequence of tie-breaks.

In a formal proof the integral must be replaced by a sum. Covered points arrive in blocks (one block per chosen set), the charge is constant on a block but the bound depends on the covered fraction at the start of the block, and the sum has to be compared with a logarithm. The terms $a\ln a$ and $a/k$ that the paper drops using $1 \le a \le k$ must be controlled as well, and the relation $1 \le a \le k$ must itself be proved from optimality. The lower bound needs an explicit run of C2 through ties on an input with $k \cdot k!$ points, checking at every stage that the intended set is a ratio minimizer.

Formalization scope

Inputs. A family is p : ℕ with S : Fin p → Finset α (0-based, repetitions allowed; a repeated set counts twice in the measure if both copies are chosen, which C2 never does). Subcovers and SUB, LEFT are index sets. $F^*$ is a minimum over the finite, nonempty set of subcovers (Finset.inf'), never a junk value.
Algorithm. C2 is a step relation on states (SUB, LEFT, UNCOV). The choice at Step 3 is existential over all minimizers, so every result quantifies over every choosable output (the paper's WORST). $\mathrm{Ratio}(S)$ is $+\infty$ when $S \cap \mathrm{UNCOV} = \emptyset$ ; the formal rule requires the chosen set to meet UNCOV and compares ratios by cross-multiplication, with no division.
Overlap. The cumulative overlap depends on the run, not on the output alone, so it is carried by an inductive run relation RunOV.
No problem size. The paper's $R[A, P](n)$ maximizes over inputs of size at most $n$ in an unspecified encoding. Upper bounds are stated for every input and every choosable output; the lower bound exhibits one input and one choosable output. Given monotonicity of $R$ in $n$ , these are equivalent to the paper's claims. Ratios are stated multiplicatively, so $F^* = 0$ does not create a vacuous bound.
Numbers. Measures are natural numbers cast to $\mathbb R$ ; $\ln$ is Real.log; $\sum_{j=1}^k 1/j$ is Mathlib's harmonic k.
Ruled out. A deterministic tie-break would prove a weaker upper bound and could not realize the lower-bound run, and a ratio with $x/0 = 0$ would make disjoint-from-UNCOV sets the most attractive choice. The formalization uses neither.

The overlap identity and the discrete integral comparison are reusable for any greedy covering analysis that charges cost per newly covered point. Contributions welcome include proofs of the milestones, the invariants of the C2 run relation (SUB and LEFT partition the indices; UNCOV $= T - \bigcup$ SUB), and the explicit lower-bound run.

Selected references

D. S. Johnson, Approximation algorithms for combinatorial problems, J. Comput. System Sci. 9 (1974), 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
V. Chvátal, A greedy heuristic for the set-covering problem, Math. Oper. Res. 4 (1979), 233–235. https://doi.org/10.1287/moor.4.3.233

10 thms3 active usersReviewed

Completed

Combinatorics Linear algebra Theoretical Computer Science·Captain: mikedeng1

Sparse Approximate Solutions to Linear Systems 2: An Exact Cover by 3-Sets Exists iff Its Incidence System Has a 1/2-Approximate Solution with at Most m/3 NonzerosResearch Paper

Motivation

Many problems in signal processing, statistics and function interpolation ask for a solution of a linear system $Ax\approx b$ that uses as few columns of $A$ as possible: a sparse approximate solution. Natarajan's 1995 paper Sparse Approximate Solutions to Linear Systems (SIAM J. Comput. 24(2):227–234) was motivated by radial basis interpolation, where each column corresponds to a basis function and fewer columns mean a cheaper interpolant. The paper does two things. It proves that finding the sparsest approximate solution is computationally hard (§2, Theorem 1), and it analyses a greedy column-selection algorithm whose number of chosen columns is within a factor, depending on the conditioning of $A$ , of the optimum (§3, Theorem 2; a separate mission of this series).

The hardness theorem is the reason the second half of the paper exists: once exact minimization is ruled out, one settles for approximation guarantees. It is cited throughout the compressed-sensing literature as the canonical statement that $\ell_0$ -minimization under an $\ell_2$ error constraint is NP-hard, and is the starting point for the later theory of when convex relaxations recover sparse solutions.

The argument follows the classical reduction from Exact Cover by 3-sets (X3C) to minimum-weight solutions of linear systems in Garey and Johnson (1979), pp. 221 and 246, adapted to an approximate right-hand side.

Setting

Sparse approximate solution (SAS). Given a matrix $A\in\mathbb R^{m\times n}$ , a vector $b\in\mathbb R^m$ and a tolerance $\varepsilon>0$ , find a vector $x\in\mathbb R^n$ with $\|Ax-b\|_2\le\varepsilon$ whose number of nonzero entries, written $\|x\|_0=|\{j : x_j\neq0\}|$ , is as small as possible. Here $\|\cdot\|_2$ is the Euclidean norm.

Exact Cover by 3-sets (X3C). An instance is a ground set $S=\{s_1,\dots,s_m\}$ and a list $C=c_1,\dots,c_n$ of subsets of $S$ , each with exactly three elements. An exact cover is a sub-collection $\hat C=\{c_j : j\in J\}$ , $J\subseteq\{1,\dots,n\}$ , such that every element of $S$ occurs in exactly one set of $\hat C$ .

The transformation. From an X3C instance build the SAS instance with

the incidence matrix $A\in\mathbb R^{m\times n}$ : $A_{ij}=1$ if $s_i\in c_j$ and $A_{ij}=0$ otherwise, so column $j$ is the characteristic vector of $c_j$ ;
the all-ones vector $b=(1,1,\dots,1)\in\mathbb R^m$ ;
the tolerance $\varepsilon=\tfrac12$ .

In Lean, $S$ is Fin m, the collection is C : Fin n → Finset (Fin m) with hC : ∀ j, (C j).card = 3, an exact cover is an index set J with IsExactCover C J, the matrix is incidence C, the vector $b$ is onesVec m, $Ax$ is Matrix.toEuclideanLin (incidence C) x, and $\|x\|_0$ is nnz x.

Formalization targets

Goal: correctness of the reduction

For every X3C instance $(S,C)$ as above,

\bigl(\exists J,\ \{c_j\}_{j\in J}\text{ is an exact cover of }S\bigr)\iff\bigl(\exists x\in\mathbb R^n,\ \|Ax-b\|_2\le\tfrac12\ \text{and}\ 3\,\|x\|_0\le m\bigr).

This is the sentence the proof of Theorem 1 (p. 228) establishes: "the constructed instance of SAS has a solution with $m/3$ or fewer entries if and only if the given instance of X3C has a solution."

Milestones

Forward direction. If $\{c_j\}_{j\in J}$ is an exact cover, the indicator vector $x=\mathbf 1_J$ satisfies $Ax=b$ and $3\|x\|_0=m$ .
Entry bounds. For every $x$ with $\|Ax-b\|_2\le\frac12$ , each entry of $Ax$ lies in $[\frac12,\frac32]$ .
Lower bound on sparsity. For every such $x$ , $m\le3\|x\|_0$ .
Exact cover from a sparse solution. If moreover $3\|x\|_0\le m$ , the sets $c_j$ with $x_j\neq0$ form an exact cover.

Significance

The result. The equivalence shows that deciding whether a sparse approximate solution with a prescribed number of nonzeros exists is at least as hard as X3C, which is NP-complete. Consequently no polynomial-time algorithm computes the optimum of SAS unless P = NP, and approximation algorithms such as the greedy method of §3 are the natural object of study. The same instance shows hardness persists for 0/1 matrices, a right-hand side of all ones and a constant tolerance, so the difficulty does not come from ill-conditioned data or from vanishing precision.

Formalizing it. The reduction is proved in the paper; this mission produces a machine-checked proof of its correctness, the combinatorial core of every NP-hardness claim for $\ell_0$ -constrained least squares. No prior machine-checked version is known to exist, on the platform or elsewhere. The complexity-theoretic wrapper is out of scope (see below).

Difficulty

The forward direction is a direct computation. The converse contains the only real step, which the paper passes over with "it is clear". From $\|Ax-b\|_2\le\frac12$ one gets only that every entry of $Ax$ is in $[\frac12,\frac32]$ ; the entries of $x$ themselves are arbitrary reals, possibly negative or not equal to $1$ , so $x$ need not be an indicator vector and $Ax=b$ need not hold. The exact-cover property must therefore be extracted from support sizes alone: every element is covered by some column in the support, the support has at most $m/3$ columns of three elements each, and a counting argument forces the chosen sets to be pairwise disjoint. Reading off a cover from the values of $x$ (for instance, taking the $j$ with $x_j=1$ ) does not work.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin m) and EuclideanSpace ℝ (Fin n), so ‖·‖ is the paper's $\|\cdot\|_2$ . Using the sup norm of Fin m → ℝ would give a different statement.
The tolerance is exactly $\varepsilon=\frac12$ , as printed.
The collection is indexed, C : Fin n → Finset (Fin m): repeated sets are allowed and are distinct indices; an exact cover is a set of indices, and on the SAS side one nonzero entry is counted per index, so both sides treat duplicates consistently.
" $m/3$ or fewer" is written $3\|x\|_0\le m$ , never with natural-number division. With this form the equivalence holds for every $m$ (both sides are false when $3\nmid m$ ), which absorbs the paper's "without loss of generality $m$ is a multiple of 3"; no divisibility hypothesis is assumed. For $m=0$ both sides are true.
The hypothesis that every set has exactly three elements is essential for the converse (with $m=9$ , $O=\{s_3,\dots,s_9\}$ , $c_1=\{s_1\}\cup O$ , $c_2=\{s_2\}\cup O$ , $c_3=O$ , the vector $x=(1,1,-1)$ solves $Ax=b$ with $3\|x\|_0=m$ , yet $C$ has no exact cover since $c_1$ and $c_2$ must both be chosen) and is kept as hC.
Not formalized: the infinite-precision RAM machine model, polynomial-time many-one reductions, polynomial-time computability of the transformation (evident: an $m\times n$ 0/1 matrix), and the NP-completeness of X3C (cited by the paper from Garey–Johnson). The goal is therefore the correctness of the transformation, not a statement titled "SAS is NP-hard". A statement that only records the forward direction, or that fixes $x$ to be a 0/1 vector on the SAS side, would trivialize the converse and is not the target.
Tools a solver will need are in Mathlib: coordinate bounds for the Euclidean norm (PiLp.norm_apply_le), Finset.card_biUnion_le, and Finset.card_biUnion for disjoint unions. Contributions of a reusable exact-cover API, or of a polynomial-time reduction framework that could later wrap this equivalence into an NP-hardness theorem, are welcome.

Selected references

B. K. Natarajan, Sparse Approximate Solutions to Linear Systems, SIAM Journal on Computing 24(2):227–234, 1995. https://doi.org/10.1137/s0097539792240406
M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979 (X3C: problem [SP2], p. 221; minimum weight solution to linear equations: [MP5], p. 246).
F. P. Preparata and M. I. Shamos, Computational Geometry: An Introduction, Springer, 1985 (the real RAM model). https://doi.org/10.1007/978-1-4612-1098-6

6 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Scenario Reduction Algorithms in Stochastic Programming III: The Minimal Reduction Distance of a Regular Ternary Scenario TreeResearch Paper

Motivation

Multistage stochastic programs are solved on a finite scenario tree: a discrete probability distribution whose support points are paths of a random process. Realistic trees have far too many scenarios for the resulting optimization problem, so practitioners reduce the tree, keeping $n$ of its $N$ scenarios and redistributing the probability of the deleted ones. The reduction should keep the reduced distribution as close as possible to the original one in a probability metric that controls the optimal value of the stochastic program (Dupačová, Gröwe-Kuska, Römisch, Math. Program. 95 (2003)).

Choosing the best $n$ scenarios is a set-covering problem and NP-hard, and the algorithms used in practice (backward reduction, fast forward selection) are heuristics without error guarantees. Heitsch and Römisch (2003) therefore derived test instances with an exactly known optimum: regular binary and ternary scenario trees, for which the minimal reduction distance has a closed form once $n$ is not too small. This mission formalizes the ternary case, Proposition 3.2 of that paper. The binary case (Proposition 3.1) is a separate mission of the same series.

Setting

Fix a depth $K \in \mathbb{N}$ and branch widths $\delta^1, \dots, \delta^K \ge 0$ , with $\delta^0 = 0$ . A regular ternary scenario tree has $N = 3^K$ scenarios, one for each index tuple $(i_1, \dots, i_K) \in \{1, 2, 3\}^K$ , where $i_k$ is the successor chosen at level $k$ . Choosing successor $i_k$ adds the increment $\delta^k_{i_k} = (i_k - 2)\,\delta^k \in \{-\delta^k, 0, \delta^k\}$ , and scenario $i$ is the vector $\omega_i = (\omega_i^0, \dots, \omega_i^K) \in \mathbb{R}^{K+1}$ with

\omega_i^k = \sum_{j=0}^{k} \delta^j_{i_j}, \qquad k = 0, \dots, K \quad \text{(eq. (19))}.

All scenarios have probability $p_i = 1/N$ . The distance between scenarios is the maximum norm $c(\omega_i, \omega_j) = \|\omega_i - \omega_j\|_\infty = \max_{0 \le k \le K} |\omega_i^k - \omega_j^k|$ .

Deleting the scenarios of an index set $J$ and moving each deleted scenario's probability to a nearest kept scenario costs the reduction distance

D_J = \sum_{i \in J} p_i \min_{j \notin J} \|\omega_i - \omega_j\|_\infty \quad \text{(eq. (8))},

which by Theorem 2.1 of the paper is the optimal transport-type distance between the original distribution and the best distribution supported on the kept scenarios. The minimal reduction distance to $n$ scenarios is $D^{min}_n = \min\{D_J : \#J = N - n\}$ .

Formalization targets

Goal: Proposition 3.2 (7/9-solution)

Let $K \ge 3$ and let $k_0 \in \arg\min_{1 \le k \le K} \delta^k$ with $k_0 \le K - 2$ and $\max\{\delta^{k_0+1}, \delta^{k_0+2}\} \le 2\delta^{k_0}$ . Then any two distinct scenarios are at distance at least $\delta^{k_0}$ ; there is a set of $\tfrac79 N$ scenarios each paired with a scenario outside it at distance exactly $\delta^{k_0}$ ; and for each $n \in \mathbb{N}$ with $\tfrac29 N \le n < N$ ,

D^{min}_n = \min\{D_J : \#J = N - n\} = \frac{N - n}{N}\,\delta^{k_0} \quad \text{(eq. (21))},

with the minimum attained.

Milestones

Distinct scenarios satisfy $\|\omega_i - \omega_j\|_\infty \ge \delta^{k_0}$ .
Every $J$ with $\#J = N - n$ has $D_J \ge \frac{N-n}{N}\delta^{k_0}$ .
The index set $I_{**}$ of the proof has $\#I_{**} = \tfrac29 N$ , and its complement $J_{**}$ has $\tfrac79 N$ elements.
Every $j \in J_{**}$ has a partner $i \in I_{**}$ with $\|\omega_i - \omega_j\|_\infty = \delta^{k_0}$ .
Example 4.2: for $K = 6$ and $(\delta^1, \dots, \delta^6) = (0.7, 0.9, 1.2, 1.5, 2.6, 3.3)$ , $D^{min}_n = 0.7\,\frac{N-n}{N}$ for $162 \le n < 729$ .

Significance

The result gives an exact optimal value for an NP-hard reduction problem on an infinite family of instances. Heitsch and Römisch use it in their numerical section to measure how far the heuristics' reduced trees are from optimal (Examples 4.1 and 4.2 are the binary and ternary test trees of that study). A closed form of this kind is also the only way to certify that a heuristic is exactly optimal on some instances rather than only competitive with other heuristics.

The proposition is proved in the paper, but the published proof of its central step is one sentence: "Similarly as in Proposition 3.1 it can be shown that there exists an index $i \in I_{**}$ for each $j \in J_{**}$ …". A formal proof supplies that case analysis, which is absent from the literature. The formalization also settles two points the printed statement leaves loose (see Formalization scope): the count of pairs at distance $\delta^{k_0}$ , and the definition of $I_{**}$ when some widths vanish. No machine-checked version of this result or of the reduction distance $D_J$ is known to exist.

Difficulty

The lower bound is routine: two distinct scenarios first differ at some level $l$ , where their coordinates differ by $\delta^l$ or $2\delta^l$ . The substance is attainment: one must exhibit, for every $n \ge \tfrac29 N$ , a kept set of size $n$ whose every deleted scenario lies at distance exactly $\delta^{k_0}$ from some kept one. The obvious candidate, keeping the scenarios that take the middle branch at level $k_0$ , has every other scenario at distance exactly $\delta^{k_0}$ from a kept one, but it keeps $\tfrac13 N$ scenarios and so covers only $n \ge \tfrac13 N$ . Going down to $\tfrac29 N$ kept scenarios forces a deleted scenario and its partner to differ at more than one level, and since coordinates are running sums the differences at levels $k_0+1$ and $k_0+2$ accumulate on top of the one at level $k_0$ . The paper's proof of this step is not written out, and it depends on the widths of the two levels below $k_0$ : the hypothesis $\max\{\delta^{k_0+1}, \delta^{k_0+2}\} \le 2\delta^{k_0}$ is essential, and the result is false without it (for $K = 3$ and $(\delta^1, \delta^2, \delta^3) = (1, 3, 3)$ one has $D^{min}_6 = 31/27$ , not $7/9$ ).

Formalization scope

A scenario is an index tuple $\sigma : \mathrm{Fin}\,K \to \mathrm{Fin}\,3$ ; $\sigma(r)$ is the successor at paper level $r + 1$ , with $\mathrm{Fin}\,3$ values $0, 1, 2$ standing for the paper's $i = 1, 2, 3$ . The widths are $\delta : \mathbb{N} \to \mathbb{R}$ , of which only $\delta(1), \dots, \delta(K)$ are used; the standing assumption $\delta^k \in \mathbb{R}_+$ (p. 196) is the hypothesis $\delta(k) \ge 0$ for $1 \le k \le K$ . Scenarios live in $\mathrm{Fin}(K+1) \to \mathbb{R}$ , whose Mathlib norm is the maximum norm. Probabilities are uniform, $1/3^K$ .
$D_J$ is defined for a general finite index set, probabilities and cost, with the inner minimum a Finset.inf' over the complement of $J$ ; the complement must be nonempty, so no default value arises. $D^{min}_n$ is stated as IsLeast of the set of all values $D_J$ with $\#J = N - n$ : the goal asserts both the lower bound for every $J$ and attainment by some $J$ . A formalization that exhibits a single $J$ with $D_J = \frac{N-n}{N}\delta^{k_0}$ , or states an infimum without attainment, or drops any hypothesis on $k_0$ , is a different (and in the last case false) statement.
$\tfrac29 N \le n$ is written $2 \cdot 3^K \le 9n$ , and $\tfrac79 N$ as $7 \cdot 3^{K-2}$ .
Pairs. As printed, "there are $\tfrac79 N$ distinct pairs of scenarios such that the distance between the members of each pair is exactly $\delta^{k_0}$ " is false as an exact count (for $K = 3$ and $\delta = (1,1,1)$ there are 130 such pairs, not 21). The goal states what the proof constructs: a set $J_{**}$ of $\tfrac79 N$ scenarios, each paired with a scenario outside $J_{**}$ at distance exactly $\delta^{k_0}$ .
$I_{**}$ . The paper defines $I_{**}$ by testing whether the increments $\delta^k_{i_k}$ vanish. When one of $\delta^{k_0}, \delta^{k_0+1}, \delta^{k_0+2}$ is $0$ this no longer identifies the middle branch and the count $\tfrac29 N$ fails, although the proposition remains true. The formalization defines $I_{**}$ by branch indices (middle branch versus outer branches), which agrees with the paper whenever these three widths are positive. No positivity hypothesis is added to the goal.
Welcome contributions: a reusable library for regular scenario trees (first differing level, distance of paths), and the case analysis of milestone 4. The binary mission of this series needs the same lower-bound argument with the constant $2\delta^{k_0}$ .

Selected references

H. Heitsch, W. Römisch, Scenario Reduction Algorithms in Stochastic Programming, Computational Optimization and Applications 24 (2003), 187–206. https://doi.org/10.1023/A:1021805924152
J. Dupačová, N. Gröwe-Kuska, W. Römisch, Scenario reduction in stochastic programming: An approach using probability metrics, Mathematical Programming 95 (2003), 493–511. https://doi.org/10.1007/s10107-002-0331-0

9 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Scenario Reduction Algorithms in Stochastic Programming II: The Minimal Reduction Distance of a Regular Binary Scenario TreeResearch Paper

Why exact reduction distances matter

Multistage stochastic programs are solved on a finite scenario tree, a discrete probability measure whose atoms are paths of a stochastic process. The size of the deterministic equivalent grows with the number of scenarios, so practitioners replace the original measure $P=\sum_{i=1}^N p_i\delta_{\omega_i}$ by a measure supported on $n<N$ of its scenarios. Stability theory for stochastic programs (Dupačová, Gröwe-Kuska and Römisch, Math. Program. 95 (2003), doi:10.1007/s10107-002-0331-0) bounds the change of the optimal value by a probability metric between the two measures, which leads to the optimal scenario reduction problem: choose which $N-n$ scenarios to delete so that this distance is smallest.

That problem is a set-covering problem and is NP-hard, and the algorithms that Heitsch and Römisch study in the same paper (backward reduction, fast forward selection) are heuristics without error guarantees. To test them one needs original measures whose optimal reduction distance is known exactly. Section 3 of Heitsch and Römisch, Scenario Reduction Algorithms in Stochastic Programming, Comput. Optim. Appl. 24 (2003) (doi:10.1023/A:1021805924152) supplies such instances: regular binary and ternary scenario trees, for which the minimal distance to any reduced tree with at least a fixed fraction of the scenarios is an explicit formula. This mission formalizes the binary case, Proposition 3.1.

Setting

Fix a horizon $K\in\mathbb N$ and level parameters $\delta^1,\dots,\delta^K\ge0$ , with $\delta^0=0$ . A regular binary scenario tree has $N=2^K$ scenarios. A scenario is determined by a branch $i_k\in\{1,2\}$ at every level $k=1,\dots,K$ , and is the vector $\omega_i=(\omega_i^0,\dots,\omega_i^K)\in\mathbb R^{K+1}$ with

\omega_i^k=\sum_{j=0}^k\delta^j_{i_j},\qquad \delta^j_{i_j}=(2i_j-3)\,\delta^j\in\{-\delta^j,+\delta^j\}.\tag{19}

All scenarios start at the root $\omega_i^0=0$ and carry probability $p_i=1/N$ . Scenarios are compared in the maximum norm $\|\omega-\tilde\omega\|_\infty=\max_{k=0,\dots,K}|\omega^k-\tilde\omega^k|$ .

Deleting the scenarios with indices in $J\subset\{1,\dots,N\}$ and moving each deleted scenario's probability to a nearest kept scenario costs the reduction cost

D_J=\sum_{i\in J}p_i\min_{j\notin J}\|\omega_i-\omega_j\|_\infty,\tag{8}

which by Theorem 2.1 of the paper is the minimal Kantorovich-type distance between $P$ and a measure supported on the kept scenarios. The minimal reduction distance for $n$ kept scenarios is $D^{min}_n=\min\{D_J:\#J=N-n\}$ .

In the Lean development, scenarios are indexed by σ : Fin K → Fin 2 (Fin-index $r$ is tree level $r+1$ , value $0$ is the branch $-\delta$ , value $1$ is $+\delta$ ), lev σ k is the branch at level $k$ , scenario δ σ : Fin (K+1) → ℝ is $\omega_\sigma$ , and redCost δ J hJ is $D_J$ .

Formalization targets

Goal: Proposition 3.1 (3/4-solution)

Let $K\ge3$ , $k_0\in\arg\min_{1\le k\le K}\delta^k$ , $k_0\le K-2$ and $\max\{\delta^{k_0+1},\delta^{k_0+2}\}\le2\delta^{k_0}$ . Then any two distinct scenarios are at distance at least $2\delta^{k_0}$ ; there is a set $J_*$ of $\frac34N$ scenarios each of which has a partner outside $J_*$ at distance exactly $2\delta^{k_0}$ ; and for every $n\in\mathbb N$ with $\frac N4\le n<N$

D^{min}_n=\min\{D_J:\#J=N-n\}=\frac{N-n}{N}\,2\delta^{k_0}.\tag{20}

Milestones

Two scenarios that first differ at level $l$ are at distance $\ge2\delta^l\ge2\delta^{k_0}$ .
$D_J\ge\frac{N-n}{N}2\delta^{k_0}$ for every $J$ with $\#J=N-n$ .
The index set $I_*$ (branch at $k_0$ opposite to the common branch at $k_0+1,k_0+2$ ) has $\#I_*=N/4$ , so $\#J_*=\frac34N$ .
Every $j\in J_*$ has a partner $i\in I_*$ with $\|\omega_i-\omega_j\|_\infty=2\delta^{k_0}$ .
Example 4.1: for $K=10$ and the paper's parameters, Proposition 3.1 applies with $k_0=1$ and $D^{min}_n=\frac{N-n}{N}$ for $256\le n<1024$ .

Significance

The result. Proposition 3.1 gives the exact optimum of an NP-hard combinatorial problem on an explicit, parametrized family of instances of every size $N=2^K$ . Section 4 of the paper uses it (Example 4.1, $N=1024$ ) as ground truth for the relative accuracy of backward reduction and fast forward selection. Without it, the quality of a heuristic reduction on a large tree could only be compared with other heuristics or with lower bounds.

The formalization. The proposition is proved in the paper; to our knowledge no machine-checked version exists. A formal proof certifies the benchmark values, and the statement also corrects the printed text in two places. First, "there are $\frac34N$ distinct pairs … at distance exactly $2\delta^{k_0}$ " is false as an exact count (for $K=3$ , $\delta=(1,1,1)$ there are twenty such pairs, not six), so the goal states "at least", in the form the proof exhibits. Second, the paper's sign-based definition of $I_*$ degenerates when some $\delta^k=0$ , although the proposition still holds; the mission defines $I_*$ by branch indices.

Difficulty

The lower bound is a direct computation. The content is the matching upper bound: a set $J$ of the prescribed size for which every deleted scenario has a kept scenario at the minimal possible distance. A natural first attempt pairs scenarios that differ only at level $k_0$ . That handles only half of the scenarios with a single partner each, and it cannot reach $\frac34N$ deleted scenarios. Once scenarios differ at more than one level, their maximum-norm distance is a maximum of several partial sums, and keeping all of them at most $2\delta^{k_0}$ is exactly where the hypothesis $\max\{\delta^{k_0+1},\delta^{k_0+2}\}\le2\delta^{k_0}$ enters. Without it, eq. (20) fails: for $K=3$ , $\delta=(1,3,3)$ and $n=2$ the true minimum is $\frac52$ , not $\frac32$ . The passage from $n=N/4$ to general $n\ge N/4$ also needs care: the deleted set must shrink while each remaining deleted scenario keeps its partner among the kept ones.

Formalization scope

The index type is Fin K → Fin 2, which has exactly $2^K$ elements. The paper's $(K+1)$ -tuple has a level-0 entry with no choice, so it is dropped, and the vector $\omega$ keeps its $K+1$ coordinates with $\omega^0=0$ .
The parameters are δ : ℕ → ℝ, with $\delta^k\ge0$ and the arg min stated for $k=1,\dots,K$ only. $\delta^k>0$ is not assumed, because the paper allows $\delta^k\in\mathbb R_+$ and the proposition holds with zeros.
The cost is Mathlib's norm on Fin (K+1) → ℝ, which is the maximum norm, and $p_i=1/2^K$ is written out.
$D_J$ requires a nonempty set of kept scenarios, and its inner minimum is a finite Finset.inf'.
$D^{min}_n$ is stated with IsLeast over the set of attained values $D_J$ , $\#J=N-n$ , so both the lower bound and attainment are part of the goal. A proof of $D_{J}\le\frac{N-n}{N}2\delta^{k_0}$ for a single exhibited $J$ , or a real infimum without attainment, does not prove the goal.
" $\frac N4\le n$ " is written $2^K\le4n$ , and $\frac34N$ is $3\cdot2^{K-2}$ .
The pairs claim is "at least $\frac34N$ pairs", expressed as a set $J_*$ of that size with a partner outside $J_*$ for every member.
All hypotheses on $k_0$ appear in the goal; dropping any of them makes (20) false.

Useful infrastructure: sup-norm lemmas for Fin n → ℝ (pi_norm_le_iff_of_nonneg, norm_le_pi_norm), Finset.inf' lemmas, and counting functions Fin K → Fin 2 with prescribed values (Fintype.card_fun, Fintype.card_pi). The tree and reduction-cost definitions are shared in spirit with the ternary-tree mission of this series (Proposition 3.2), and a proof whose structure transfers to $d=3$ is welcome. Contributions of proofs of the milestones individually, in any order, are welcome.

Selected references

H. Heitsch, W. Römisch, Scenario Reduction Algorithms in Stochastic Programming, Computational Optimization and Applications 24 (2003), 187–206. doi:10.1023/A:1021805924152
J. Dupačová, N. Gröwe-Kuska, W. Römisch, Scenario reduction in stochastic programming: An approach using probability metrics, Mathematical Programming 95 (2003), 493–511. doi:10.1007/s10107-002-0331-0

9 thms3 active usersReviewed

Completed

Operations Research Optimal Transport Optimization·Captain: mikedeng1

Scenario Reduction Algorithms in Stochastic Programming I: Fast Forward Selection Realizes the Forward Selection PrincipleResearch Paper

Why reduce scenarios

Multistage and two-stage stochastic programs are solved numerically on a discrete probability distribution: a finite set of scenarios $\omega_1,\dots,\omega_N$ with probabilities $p_1,\dots,p_N$ . The size of the resulting optimization problem grows with $N$ , and scenario sets produced by sampling or by historical data are often far too large to be solved directly. Scenario reduction replaces the original distribution by one supported on a small subset of the scenarios, chosen so that the optimal value and solutions of the stochastic program change as little as possible.

Stability theory for stochastic programs (Rachev and Römisch, 2002) shows that this change is controlled by a probability distance of Fortet–Mourier type, which for discrete measures is bounded by the value of a transportation problem. Dupačová, Gröwe-Kuska and Römisch (2003) turned this into a combinatorial problem and proposed greedy backward and forward heuristics. Heitsch and Römisch (2003) gave faster versions of both heuristics; the forward version, fast forward selection, is the subject of this mission. Implementations of these reduction heuristics are distributed with the GAMS modelling system (SCENRED) and are used in energy and finance applications of stochastic programming.

Setting

Let $E$ be a finite-dimensional real vector space with a norm $\|\cdot\|$ , let $\omega_0\in E$ , and let $h:[0,\infty)\to[0,\infty)$ be continuous and nondecreasing with $h(0)=0$ . The cost between two points of $E$ is

c(\omega,\tilde\omega)=\max\bigl\{1,\,h(\|\omega-\omega_0\|),\,h(\|\tilde\omega-\omega_0\|)\bigr\}\,\|\omega-\tilde\omega\| .

It is nonnegative, symmetric, and zero on the diagonal.

The original distribution is $P=\sum_{i=1}^N p_i\delta_{\omega_i}$ with $p_i>0$ and $\sum_i p_i=1$ . Deleting the scenarios in a set $J\subset\{1,\dots,N\}$ and assigning new weights $q_j\ge 0$ , $\sum_{j\notin J}q_j=1$ , to the kept ones gives $Q=\sum_{j\notin J}q_j\delta_{\omega_j}$ . The distance $D(J;q)$ between $P$ and $Q$ is the optimal value of the transportation problem

D(J;q)=\min\Bigl\{\sum_{i=1}^N\sum_{j\notin J}c(\omega_i,\omega_j)\eta_{ij}:\ \eta_{ij}\ge 0,\ \sum_{i}\eta_{ij}=q_j,\ \sum_{j\notin J}\eta_{ij}=p_i\Bigr\}.

The reduction cost of deleting $J$ is

D_J=\sum_{i\in J}p_i\min_{j\notin J}c(\omega_i,\omega_j),

and the optimal reduction problem (8) minimizes $D_J$ over all $J$ with $\#J=N-n$ , where $n$ is the number of scenarios to keep.

Forward selection builds the kept set greedily. With $J^{[0]}=\{1,\dots,N\}$ and $J^{[i]}=\{1,\dots,N\}\setminus\{u_1,\dots,u_i\}$ , it chooses

u_i\in\arg\min_{u\in J^{[i-1]}}D_{J^{[i-1]}\setminus\{u\}},\qquad i=1,\dots,n. \tag{16}

Fast forward selection (Algorithm 2.4) computes the same choices through an updated cost matrix: $c^{[1]}_{ku}=c(\omega_k,\omega_u)$ , $c^{[i]}_{ku}=\min\{c^{[i-1]}_{ku},c^{[i-1]}_{ku_{i-1}}\}$ , $z^{[i]}_u=\sum_{k\in J^{[i-1]}\setminus\{u\}}p_kc^{[i]}_{ku}$ , and $u_i\in\arg\min_{u\in J^{[i-1]}}z^{[i]}_u$ .

Formalization targets

Goal: Theorem 2.5

For $1\le n\le N$ and every run $u_1,\dots,u_n$ of Algorithm 2.4, with any tie-breaking in the arg min,

u_i\ \text{satisfies (16)}\quad\text{and}\quad z^{[i]}_{u_i}=D_{J^{[i]}}\qquad(i=1,\dots,n).

Milestones

Theorem 2.1 (redistribution). For $J$ with at least one kept scenario, $D_J=\min_q D(J;q)$ , and the minimum is attained at $\bar q_j=p_j+\sum_{i\in J,\,j(i)=j}p_i$ for every choice of nearest kept scenarios $j(i)$ .
Eq. (10). $D_{\{1,\dots,N\}\setminus\{u\}}=\sum_{i=1}^Np_ic(\omega_i,\omega_u)$ , so (8) with $\#J=N-1$ is problem (10).
Eq. (12). The sum $lb$ of the $N-n$ smallest single-deletion costs $p_l\min_{j\neq l}c(\omega_l,\omega_j)$ , taken in the greedy order (11), is at most $D_J$ for every $J$ with $\#J=N-n$ .
Optimality condition (p. 191). If each $l_i$ has a nearest other scenario outside $\{l_1,\dots,l_{N-n}\}\setminus\{l_i\}$ , then $\{l_1,\dots,l_{N-n}\}$ solves (8).
Eq. (17), unrolled recursion. For any index sequence, $c^{[i]}_{ku}=\min_{j\notin J^{[i-1]}\setminus\{u\}}c(\omega_k,\omega_j)$ for $u\in J^{[i-1]}$ .
Eq. (17), conclusion. For any index sequence, $z^{[i]}_u=D_{J^{[i-1]}\setminus\{u\}}$ for $u\in J^{[i-1]}$ .

Significance

Theorem 2.5 certifies that the cheap update of Algorithm 2.4 (one pairwise minimum per matrix entry and step) produces exactly the greedy forward selection defined through the reduction costs, and that the running objective $z^{[i]}_{u_i}$ is the reduction cost of the scenarios deleted so far. Combined with Theorem 2.1, $z^{[i]}_{u_i}$ is the optimal transportation distance between $P$ and the best measure on the kept scenarios, which is the quantity practitioners monitor to decide how many scenarios to keep. The lower bound (12) and the optimality condition give a posteriori quality certificates for any reduced set.

All results of this mission are proved in the paper or in the works it cites (Dupačová et al., 2003); none is open. To the best of a platform search, none has been machine-checked. The mission provides a verified specification of a widely deployed algorithm, a formal link between a combinatorial set-covering objective and a finite transportation problem, and definitions (reduction cost, transportation plans with a partially free target marginal, greedy runs with arbitrary tie-breaking) reusable by the regular-tree missions of this series and by later scenario-tree construction papers.

Difficulty

The mathematics is elementary; the difficulty is bookkeeping. The recursion for $c^{[i]}$ refers to the previous step's column $u_{i-1}$ , which itself was updated, so unrolling it to a minimum over $\{u,u_1,\dots,u_{i-1}\}$ is an induction on $i$ in which the index sets $J^{[i]}$ , the 1-based step counter and the complement structure all move together. The natural first attempt, identifying $c^{[i]}_{ku}$ with the minimum over the complement of $J^{[i]}$ , is off by one step: the correct set is the complement of $J^{[i-1]}\setminus\{u\}$ , which contains $u$ itself. For Theorem 2.1 the lower bound requires using that $c(\omega_i,\omega_i)=0$ for kept scenarios and that every plan ships all of $p_i$ somewhere outside $J$ ; the attainment part requires constructing the plan explicitly from the choice $j(\cdot)$ , including scenarios for which several kept scenarios are equally near.

Formalization scope

Scenarios are ω : Fin N → E with E a finite-dimensional real normed space; the paper's closed set $\Omega\subset\mathbb R^s$ plays no role beyond containing the scenarios and is omitted. Scenarios need not be distinct.
$h$ is a function ℝ → ℝ with the paper's assumptions imposed on $[0,\infty)$ (IsGrowthFunction); every theorem carries them, together with $p_i>0$ and $\sum_ip_i=1$ .
The functions $f_0$ , $g$ and the stochastic program (1)–(2) that motivate $c$ appear in no statement.
$D(J;q)$ is the paper's finite transportation problem (p. 188), not the Kantorovich functional on measures. Weights $q$ and plans $\eta$ are indexed by all of $\{1,\dots,N\}$ with entries at deleted indices fixed to $0$ .
$D_J$ requires a proof that the complement of $J$ is nonempty; minima are Finset.inf', never a real infimum with a default value.
Algorithm 2.4 is a relation on sequences u : ℕ → Fin N with 1-based steps. $c^{[i]}$ is the printed recursion, extended to all indices; runs are any sequences satisfying the arg-min conditions, so every tie-breaking rule is covered.
The paper's standing restriction $n<N$ is relaxed to $n\le N$ in Theorem 2.5; the statement remains true at $n=N$ .
A trivializing formalization is ruled out: defining $c^{[i]}$ or $z^{[i]}$ directly as the minimum over the selected set or as $D_{J^{[i-1]}\setminus\{u\}}$ would make Theorem 2.5 hold by definition, and proving it for one fixed tie-breaking rule would prove less than the paper; neither is done.
Proofs of the milestones, alternative proofs of Theorem 2.1 via LP duality, and a verified executable implementation of Algorithm 2.4 are all welcome.

Selected references

H. Heitsch, W. Römisch, Scenario Reduction Algorithms in Stochastic Programming, Computational Optimization and Applications 24 (2003), 187–206. https://doi.org/10.1023/A:1021805924152
J. Dupačová, N. Gröwe-Kuska, W. Römisch, Scenario reduction in stochastic programming: an approach using probability metrics, Mathematical Programming 95 (2003), 493–511. https://doi.org/10.1007/s10107-002-0331-0
S. T. Rachev, W. Römisch, Quantitative stability in stochastic programming: the method of probability metrics, Mathematics of Operations Research 27 (2002), 792–818. https://doi.org/10.1287/moor.27.4.792.304

12 thms3 active usersReviewed

Completed

Convex Optimization Numerical Analysis Operations Research+1·Captain: mikedeng1

Golden Ratio Algorithms for Variational Inequalities I: The Golden Ratio Algorithm with a Fixed Step Converges to a Solution of a Monotone Variational InequalityResearch Paper

Motivation

A monotone variational inequality asks for a point at which a monotone operator and a convex function are in equilibrium. It unifies convex minimization (where $F$ is a gradient), convex–concave saddle-point problems (where $F$ is the skew gradient of a Lagrangian), Nash equilibria of monotone games, and complementarity problems in economics and traffic assignment. In operations research, first-order methods for such problems are the workhorse behind large-scale saddle-point formulations of linear and conic programs, where only one operator evaluation and one projection or proximal step per iteration are affordable.

The classical method for Lipschitz monotone operators is Korpelevich's extragradient method (1976) and its proximal variant, Tseng's forward–backward–forward method (2000); both need two evaluations of $F$ per iteration. The reflected projected gradient method of Malitsky (SIAM J. Optim., 2015) uses one evaluation of $F$ but evaluates it at $2z^k-z^{k-1}$ , a point that may lie outside the domain of $g$ . Malitsky's Golden Ratio Algorithm (GRAAL), introduced in Golden Ratio Algorithms for Variational Inequalities (preprint 2018; published in Mathematical Programming, doi:10.1007/s10107-019-01416-w), uses one evaluation of $F$ , always at a feasible point, and one proximal step per iteration. Its fixed-step version, Theorem 1 of that paper, is the subject of this mission; the explicit, adaptive-step version (Theorem 2) is a separate mission of this series.

Setting

Let $\mathcal E$ be a finite-dimensional real inner product space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\| = \sqrt{\langle\cdot,\cdot\rangle}$ . Let $g:\mathcal E\to(-\infty,+\infty]$ and write $\operatorname{dom} g = \{x : g(x)<+\infty\}$ . Let $F:\operatorname{dom} g\to\mathcal E$ . The variational inequality is

\text{find } z^*\in\mathcal E \quad\text{such that}\quad \langle F(z^*), z-z^*\rangle + g(z)-g(z^*)\ \ge\ 0\qquad \forall z\in\mathcal E. \tag{1}

The standing assumptions are:

(C1) the solution set $S$ of (1) is nonempty;
(C2) $g$ is proper (never $-\infty$ , finite somewhere), convex, and lower semicontinuous;
(C3) $F$ is monotone: $\langle F(u)-F(v),u-v\rangle\ge0$ for all $u,v\in\operatorname{dom} g$ .

The proximal operator of $g$ is $\operatorname{prox}_g(z) = \operatorname{argmin}_x\{g(x)+\tfrac12\|x-z\|^2\}$ . Let $\varphi = \frac{\sqrt5+1}{2}$ be the golden ratio, so that $\varphi^2 = 1+\varphi$ . For a step $\lambda>0$ and arbitrary starting points $z^1,\bar z^0\in\mathcal E$ , the Golden Ratio Algorithm generates, for $k\ge1$ ,

\bar z^k = \frac{(\varphi-1)z^k + \bar z^{k-1}}{\varphi},\qquad z^{k+1} = \operatorname{prox}_{\lambda g}\big(\bar z^k - \lambda F(z^k)\big). \tag{6}

The first line is a convex combination of the newest iterate and the previous average; the second is a forward–backward step taken from the average rather than from $z^k$ .

Formalization targets

Goal: Theorem 1

If $F$ is $L$ -Lipschitz on $\operatorname{dom} g$ ( $L>0$ ), (C1)–(C3) hold, and $\lambda\in\big(0,\frac{\varphi}{2L}\big]$ , then there is $z^*\in S$ with

z^k\to z^*\qquad\text{and}\qquad \bar z^k\to z^*\qquad(k\to\infty).

Both sequences converge, to one and the same solution. The goal is stated with the paper's exact step range; no rate is claimed, as the paper claims none.

Milestones

Eq. (4), the prox-inequality: for proper convex lsc $g$ ,

\bar x = \operatorname{prox}_g z \iff \langle\bar x - z, x-\bar x\rangle\ge g(\bar x)-g(x)\quad\forall x\in\mathcal E.

Eq. (12), an identity using only the averaging step of (6): for every point $z^*$ ,

\|z^{k+1}-z^*\|^2 = (1+\varphi)\|\bar z^{k+1}-z^*\|^2-\varphi\|\bar z^k-z^*\|^2+\tfrac1\varphi\|z^{k+1}-\bar z^k\|^2 .

Eq. (14), the energy inequality: for $z^*\in S$ and $k\ge2$ ,

(1+\varphi)\|\bar z^{k+1}-z^*\|^2+\tfrac\varphi2\|z^{k+1}-z^k\|^2\le(1+\varphi)\|\bar z^k-z^*\|^2+\tfrac\varphi2\|z^k-z^{k-1}\|^2-\varphi\|z^k-\bar z^k\|^2 .

Lemma 1 (Bauschke–Combettes, Theorem 5.5): a sequence that is Fejér monotone with respect to a nonempty set $C$ and whose cluster points all lie in $C$ converges to a point of $C$ .

Significance

The result. Theorem 1 shows that monotone variational inequalities with a Lipschitz operator can be solved with one operator evaluation and one proximal step per iteration, with $F$ evaluated only at points of $\operatorname{dom} g$ , where it is defined. This matters when $F$ is expensive (a large matrix–vector product, a simulation) or undefined outside the feasible set (for instance an operator involving $\log x$ on the positive orthant). The analysis also explains the constant: the averaging weight $\varphi$ is the largest $c$ with $1/c\ge c-1$ , and the step bound $\varphi/(2L)$ follows from it. The fixed-step analysis is the template for the explicit, adaptive-step EGRAAL of the same paper (Theorem 2), which needs only local Lipschitz continuity of $F$ .

The formalization. The theorem has a published proof, and no machine-checked version of it or of GRAAL is known. Mathlib contains the golden ratio, Lipschitz conditions, lower semicontinuity and cluster points, but no proximal operator of an extended-valued function, no prox-inequality and no Fejér-monotonicity convergence lemma. This mission produces those pieces and a complete convergence proof for a first-order VI method, which are reusable for projected gradient, forward–backward, extragradient and reflected-gradient analyses.

Difficulty

The naive approach, to show that $\|z^k-z^*\|$ decreases, fails: GRAAL is not Fejér monotone in $z^k$ , because the forward step is taken from the average $\bar z^k$ and uses $F(z^k)$ rather than $F$ at the new point. The quantity that decreases is an energy mixing $\|\bar z^k-z^*\|^2$ with the successive difference $\|z^k-z^{k-1}\|^2$ , and both the averaging identity and the Lipschitz estimate must produce matching coefficients for the cross terms to cancel. The energy inequality alone gives only boundedness and vanishing successive differences; convergence of the whole sequence, and the fact that the limit solves (1) when $g$ is merely lower semicontinuous and extended-valued, is a separate step. On the formal side, $g$ takes the value $+\infty$ , so the prox-inequality and the variational inequality must be handled in extended arithmetic without letting $\infty-\infty$ decide anything.

Formalization scope

$\mathcal E$ is a type E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E].
$g$ is E → EReal. (C2) is IsProperConvexLSC g: never $\bot$ , somewhere finite, convex epigraph $\{(x,t)\in E\times\mathbb R: g(x)\le t\}$ , and LowerSemicontinuous g on all of E. $\operatorname{dom} g$ is effDom g = {x | g x ≠ ⊤}.
$F$ is a total function E → E; monotonicity and the Lipschitz bound $\|F(u)-F(v)\|\le L\|u-v\|$ are required on effDom g only. The step range is 0 < λ, λ ≤ φ / (2 * L) with 0 < L and φ = Real.goldenRatio.
$S$ is solutionSet g F: points of effDom g satisfying (1) for every $z\in E$ , evaluated in EReal.
The proximal step is the argmin predicate IsProxPoint (fun x => λ * g x) w z⁺, not a choice function, so no junk value is involved. A run of (6) is IsGRAALRun g F λ z zbar on sequences ℕ → E indexed as in the paper: $z^1$ and $\bar z^0$ are free and the entry $z^0$ is unused.
The conclusion is ∃ zs ∈ solutionSet g F, Tendsto z atTop (𝓝 zs) ∧ Tendsto zbar atTop (𝓝 zs).

The hypotheses of the goal are jointly satisfiable, so the theorem is not vacuous: for $g\equiv0$ and $F\equiv0$ every point is a solution and constant sequences form a run of (6); a formalization under which IsGRAALRun has no instances, or in which $S$ may be empty, is ruled out. Two hypotheses are added to printed statements and flagged in their notes: $C\neq\emptyset$ in Lemma 1, which is false without it, and $z^1\in\operatorname{dom} g$ in Eq. (14), needed at $k=2$ because the paper's $F$ is only defined on $\operatorname{dom} g$ .

Welcome contributions: existence and uniqueness of the proximal point of a proper convex lsc function in finite dimensions; the prox-inequality; Fejér-monotonicity lemmas; the energy inequality; and the final convergence argument. The prox and Fejér infrastructure is independent of the golden ratio and is shared with the second mission of this series.

Selected references

Y. Malitsky, Golden Ratio Algorithms for Variational Inequalities, preprint, Optimization Online 6598, 2018. https://optimization-online.org/wp-content/uploads/2018/05/6598.pdf ; published in Mathematical Programming. https://doi.org/10.1007/s10107-019-01416-w
H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011 (2nd ed. 2017). https://doi.org/10.1007/978-3-319-48311-5
G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Ekonomika i Matematicheskie Metody 12 (1976) 747–756.
P. Tseng, A modified forward–backward splitting method for maximal monotone mappings, SIAM J. Control Optim. 38 (2000) 431–446. https://doi.org/10.1137/S0363012998338806
Y. Malitsky, Projected reflected gradient methods for monotone variational inequalities, SIAM J. Optim. 25 (2015) 502–520. https://doi.org/10.1137/14097238X

8 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Number Theory+1·Captain: mikedeng1

Fast Algorithms for Finding Nearest Common Ancestors II: Nearest Common Ancestors in a Complete Binary Tree by Symmetric-Order ArithmeticResearch Paper

Motivation

The nearest common ancestor (nca) problem asks, for a fixed rooted tree and a sequence of vertex pairs $(v, w)$ , for the deepest vertex that is an ancestor of both. It is a basic step in suffix-tree string algorithms and is equivalent to range-minimum queries (Bender, Farach-Colton, 2000). Harel and Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13 (1984) 338–355, gave the first algorithm answering each query on a static tree in constant time on a random-access machine after linear preprocessing.

Their construction reduces the general problem to the case of a complete binary tree, where §3 of the paper shows that nca queries can be answered "by direct calculation" on vertex numbers: multiplication, division, powers of two, the base-two logarithm and bitwise exclusive or. The later simplification of Schieber and Vishkin (1988) is built on the same in-order numbering of a complete binary tree. This mission formalizes that arithmetic core.

Timeline, as reviewed in the paper's §1 (pp. 338–340):

1976: Aho, Hopcroft and Ullman (SIAM J. Comput. 5) give an $O(n + m\alpha(m+n, n))$ -time off-line algorithm on a pointer machine, and for static trees a random-access algorithm with $O(n \log\log n)$ preprocessing and $O(\log\log n)$ time per query.
1976: van Leeuwen (unpublished report) gives an $O(n + m \log\log n)$ -time algorithm for linking roots and static trees that runs on a pointer machine in $O(n)$ space.
1980: Harel (Proc. 21st FOCS) gives a preliminary version of the paper's results.
1984: Harel and Tarjan prove that pointer machines need $\Omega(\log\log n)$ time per query on static trees (Theorem 1), and give the $O(n)$ -preprocessing, $O(1)$ -query random-access algorithm whose base case is the subject of this mission.

Setting

Fix $d \ge 0$ and let $T$ be the complete binary tree of depth $d$ . A vertex is identified with the path from the root to it, a word of at most $d$ left or right turns; the root is the empty word and $T$ has $n = 2^{d+1} - 1$ vertices. Following the paper's Appendix (pp. 354–355):

$w$ is an ancestor of $v$ ( $v$ a descendant of $w$ ) if the word $w$ is a prefix of the word $v$ ; every vertex is its own ancestor. $v$ and $w$ are unrelated if neither is an ancestor of the other.
The depth of $v$ is its distance to the root; its height $h(v)$ is the length of the longest path from a leaf to $v$ , which in $T$ is $d - \operatorname{depth}(v)$ .
$\operatorname{nca}(v, w)$ is the vertex of greatest depth that is an ancestor of both: the longest common prefix.

The vertices of $T$ are numbered from $1$ to $n$ in symmetric order (in-order): at every vertex, first the left subtree, then the vertex, then the right subtree. $\mathrm{sym}(v)$ is the number of $v$ and $\mathrm{sym}^{-1}(i)$ the vertex numbered $i$ . For $d = 4$ (Fig. 1 of the paper) the root is $16$ , its children $8$ and $24$ , and the leaves $1, 3, 5, \dots, 31$ . $i \oplus j$ denotes bitwise exclusive or and $\lg$ the base-two logarithm.

Two procedures of §3 use only numbers, heights and $d$ :

the nca depth algorithm: return $d - h(v)$ if $\mathrm{sym}(w) \in [\mathrm{sym}(v) - 2^{h(v)} + 1, \mathrm{sym}(v) + 2^{h(v)} - 1]$ ; else $d - h(w)$ if the same holds with $v, w$ exchanged; else $d - \lfloor \lg(\mathrm{sym}(v) \oplus \mathrm{sym}(w)) \rfloor$ ;
the depth algorithm: given $v$ and a depth $d_2 \le \operatorname{depth}(v)$ , with $h = d - d_2$ , return $\mathrm{sym}^{-1}\bigl(2^{h+1}\lfloor \mathrm{sym}(v)/2^{h+1}\rfloor + 2^h\bigr)$ .

Formalization targets

Goal: the nca algorithm is correct

The algorithm to compute $\operatorname{nca}(v,w)$ (p. 342) runs the nca depth algorithm to obtain $d_0$ and then the depth algorithm on $(v, d_0)$ . The goal states that it returns the nearest common ancestor: for all vertices $v, w$ of $T$ , with $d_0$ the output of the nca depth algorithm and $h = d - d_0$ ,

\mathrm{sym}(\operatorname{nca}(v,w)) = 2^{h+1}\left\lfloor \frac{\mathrm{sym}(v)}{2^{h+1}} \right\rfloor + 2^h .

Milestones

In the order the paper uses them:

Numbers at height $h$ (p. 341): the vertices of height $h$ are numbered $2^h, 3\cdot 2^h, 5\cdot 2^h, \dots$ from left to right.
Lemma 1: $h(v)$ is the largest $h$ with $2^h \mid \mathrm{sym}(v)$ .
Lemma 2: the descendants of $v$ are the vertices numbered in $[\mathrm{sym}(v) - 2^{h(v)} + 1, \mathrm{sym}(v) + 2^{h(v)} - 1]$ .
Lemma 3: for a height $h \ge h(v)$ , the height- $h$ ancestor of $v$ has number $2^{h+1}\lfloor \mathrm{sym}(v)/2^{h+1}\rfloor + 2^h$ .
Lemma 4: for unrelated $v, w$ ,

h(\operatorname{nca}(v,w)) = \lfloor \lg(\mathrm{sym}(v) \oplus \mathrm{sym}(w)) \rfloor .

The nca depth algorithm returns $\operatorname{depth}(\operatorname{nca}(v,w))$ .
The depth algorithm returns the number of the depth- $d_2$ ancestor of $v$ .

Two supporting statements pin the definitions to the paper: $\mathrm{sym}$ is a bijection onto $\{1, \dots, 2^{d+1} - 1\}$ , and the longest common prefix is the deepest common ancestor.

Significance

The constant-time nca computation on complete binary trees is the base case of the whole paper: §§4–5 embed an arbitrary tree into a moderately sized complete binary tree through a compressed tree and a balanced binary tree, and every query ends with the arithmetic of §3. The same idea, that in-order numbers encode ancestry in their low-order bits, underlies the Schieber–Vishkin algorithm. Lemma 1 identifies the height with the 2-adic valuation of the number, and Lemma 4 identifies the nca height with the position of the highest differing bit.

The results are proved in the paper, with the proofs left as "easy to verify". No machine-checked version of this numbering or of these four lemmas is known to exist in Mathlib or on this platform. A formal development supplies proofs of the four lemmas and the two algorithms, and a reusable library connecting in-order ranks of a complete binary tree to binary arithmetic (Nat.log, bitwise xor, 2-adic valuation).

Difficulty

The numbering is defined by a traversal order, while the lemmas speak about divisibility, floor division and exclusive or. The work lies in connecting the rank of a vertex in symmetric order to its closed form $(2j+1)\cdot 2^{h(v)}$ , where $j$ is its left-to-right position. That counting argument sums the sizes of the subtrees that precede $v$ and is where most of the effort goes. Lemma 4 then needs the observation that two unrelated numbers agree in all bits above the height of their nca and differ in the bit at that height. This is a statement about Nat.testBit of the exclusive or, and it fails for related vertices. The algorithm statements add a case analysis whose first two cases overlap when $v = w$ .

Formalization scope

A vertex of the tree of depth $d$ is a List Bool of length at most $d$ (false = left). Ancestry is the prefix relation, $\operatorname{nca}$ the longest common prefix, depth the length, and height $d - \text{length}$ . None of these structural notions uses the numbering.
$\mathrm{sym}(v)$ is the number of vertices whose in-order sort key is lexicographically at most that of $v$ . The key is the path with left $\mapsto 0$ , right $\mapsto 2$ , followed by $1$ . The numbering is not defined by the closed form or by a recursion on numbers: a definition of that kind would make the height- $h$ numbering and Lemma 1 immediate and move the content of the mission into an uncheckable definition.
$\lfloor \lg x \rfloor$ is Nat.log 2 x, which agrees for $x \ge 1$ . $\oplus$ is ^^^ on $\mathbb N$ , and floor division is / on $\mathbb N$ .
Interval tests $a \in [b - c + 1, b + c - 1]$ are written additively as $b + 1 \le a + c$ and $a + 1 \le b + c$ . The subtractions $d - h(v)$ and $d - d_2$ never truncate for heights and depths of vertices.
Lemma 3 states explicitly that $h \le d$ (" $h$ is a height") and that the ancestor exists. The depth algorithm assumes $d_2 \le \operatorname{depth}(v)$ , as printed.
$\mathrm{sym}^{-1}$ is not defined as a function. The goal and the depth algorithm state that a vertex has the computed number if and only if it is the nearest common ancestor (respectively the ancestor at depth $d_2$ ), which says that $\mathrm{sym}^{-1}$ of that number is that vertex.
The $O(1)$ time bounds are not formalized, since the random-access machine model is out of scope.

Proofs of any milestone are welcome.

Selected references

D. Harel and R. E. Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13(2) (1984), 338–355. https://doi.org/10.1137/0213024
A. V. Aho, J. E. Hopcroft and J. D. Ullman, On Finding Lowest Common Ancestors in Trees, SIAM J. Comput. 5(1) (1976), 115–132. https://doi.org/10.1137/0205011
B. Schieber and U. Vishkin, On Finding Lowest Common Ancestors: Simplification and Parallelization, SIAM J. Comput. 17(6) (1988), 1253–1262. https://doi.org/10.1137/0217079
M. A. Bender and M. Farach-Colton, The LCA Problem Revisited, LATIN 2000, LNCS 1776, 88–94. https://doi.org/10.1007/10719839_9

11 thms3 active usersReviewed

Completed

Numerical Analysis Operations Research Optimization·Captain: mikedeng1

Pattern Search Algorithms for Bound Constrained Minimization: Generalized Pattern Search Drives the Projected Stationarity Measure to ZeroResearch Paper

Motivation

Pattern search methods minimize a function $f:\mathbb R^n\to\mathbb R$ by comparing values of $f$ at points of a structured set of trial points, without evaluating or approximating derivatives. Coordinate search and the method of Hooke and Jeeves (Hooke–Jeeves 1961) are the classical members of the family. Such methods remain in use when derivatives are unavailable, unreliable or expensive, for instance when $f$ is the output of a simulation, and practical problems of this kind usually carry simple bounds on the variables.

Torczon (SIAM J. Optim. 1997) gave a global convergence theory for pattern search on unconstrained problems: under compactness of the level set and continuous differentiability of $f$ , $\liminf_k\|\nabla f(x_k)\|=0$ , and under stronger hypotheses $\lim_k\|\nabla f(x_k)\|=0$ . Lewis and Torczon extended this theory to bound constrained problems (ICASE Report 96-20, 1996; SIAM J. Optim. 1999). The extension is not automatic: the paper exhibits a pattern search method for unconstrained problems (Box's evolutionary operation with factorial designs) that fails on bound constrained ones, and identifies the structural condition on the pattern that restores convergence.

Timeline.

1961: Hooke and Jeeves introduce "direct search" pattern methods.
1987–1988: Calamai and Moré (Math. Program. 1987) and Conn, Gould and Toint (SIAM J. Numer. Anal. 1988) develop the projected-gradient stationarity theory for bound and linear constraints, for methods that use derivatives.
1997: Torczon proves global convergence of generalized pattern search for unconstrained problems.
1996/1999: Lewis and Torczon prove the bound constrained theory formalized here.

Setting

The problem is

\min f(x)\quad\text{subject to}\quad \ell\le x\le u,

with $\ell,u$ vectors of extended reals and $\ell_j<u_j$ for every $j$ ; $\ell_j=-\infty$ or $u_j=+\infty$ is allowed. The feasible region is $\Omega=\{x:\ell\le x\le u\}$ , $P$ is the coordinatewise projection onto $\Omega$ , $g=\nabla f$ , and $L_\Omega(y)=\{x\in\Omega:f(x)\le f(y)\}$ is the feasible level set. A stationary point is an $x\in\Omega$ with $\langle g(x),z-x\rangle\ge0$ for all $z\in\Omega$ . The stationarity measure is

q(x)=P\bigl(x-g(x)\bigr)-x,

which vanishes exactly at stationary points.

A generalized pattern search method is fixed by a nonsingular basis matrix $B\in\mathbb R^{n\times n}$ , a finite set $\mathcal M$ of nonsingular integer matrices, a rational $\tau>1$ , an integer $w_0<0$ and nonnegative integers $w_1,\dots,w_L$ . At iteration $k$ the generating matrix is $C_k=[M_k\ \ {-M_k}\ \ L_k]=[\Gamma_k\ \ L_k]$ with $M_k\in\mathcal M$ , $L_k$ an integer matrix containing a zero column, and $BM_k$ diagonal. A trial step is $\Delta_kBc$ for a column $c$ of $C_k$ . The step $s_k$ is a trial step with $x_k+s_k\in\Omega$ , and it must decrease $f$ whenever some feasible trial step from the core $\Delta_kB\Gamma_k$ does. The iterate moves, $x_{k+1}=x_k+s_k$ , exactly when $f(x_k+s_k)<f(x_k)$ . The step length $\Delta_k$ is multiplied by $\theta=\tau^{w_0}<1$ after an unsuccessful iteration and by some $\tau^{w_i}\ge1$ after a successful one. The Strong Hypotheses additionally require $f(x_k+s_k)$ to be no larger than the best feasible core trial value whenever that value is below $f(x_k)$ .

Formalization targets

Goal: Theorem 3.3

If $L_\Omega(x_0)$ is compact, $f$ is continuously differentiable, the columns of the $C_k$ are uniformly bounded, $\Delta_k\to0$ , and the Strong Hypotheses hold, then

\lim_{k\to\infty}\|q(x_k)\|=0 .

Milestones

Lemma 2.1, Theorem 2.2, Lemma 2.3: the unconstrained results the paper recalls from Torczon (1997): nonzero steps have length at least $\zeta_*\Delta_k$ ; the iterates lie on the translated lattice $x_0+\beta^{r_{LB}}\alpha^{-r_{UB}}\Delta_0B\,\mathbb Z^n$ (with $\tau=\beta/\alpha$ ); bounded columns give $\Delta_k\ge\psi_*\|s_k^i\|$ .
Proposition 3.1 (6), (8): $\|q(x)\|\le\|g(x)\|$ , and $x$ is stationary iff $q(x)=0$ .
All iterates lie in $L_\Omega(x_0)$ (§4, p. 10).
Propositions 4.1–4.3: a descent estimate along short steep directions; a feasible core step with $g_k^Ts\le-n^{-1/2}\|q_k\|\|s\|$ whenever $q_k\ne0$ and the step length is small; a uniform $\delta$ (and, under the Strong Hypotheses, a $\sigma$ ) with $f(x_{k+1})\le f(x_k)-\sigma\|q(x_k)\|\|s_k\|$ when $\Delta_k<\delta$ and $\|q(x_k)\|>\eta$ .
Corollary 4.4 and Theorem 4.5: $\liminf\|q(x_k)\|\ne0$ keeps $\Delta_k$ bounded away from zero, whereas compactness alone forces $\liminf\Delta_k=0$ .
Theorem 3.2: $\liminf_k\|q(x_k)\|=0$ .

Significance

Theorem 3.2 shows that a method which never computes a gradient still has a subsequence approaching first-order stationarity for the bound constrained problem, even though it cannot enforce a sufficient decrease condition measured by the projected gradient. Theorem 3.3 upgrades this to the whole sequence, so every limit point of the iterates is a KKT point. These results justify the bound constrained variants of coordinate search and Hooke–Jeeves discussed in §5 of the paper, and they are the template for the later theory of pattern search under linear constraints and generating set search.

The results are proved in the paper, and three of the milestones are proved in Torczon (1997). None of them has a machine-checked proof. Formalizing them produces a Lean model of generalized pattern search (patterns, exploratory moves, step-length updates) that later missions on direct search, mesh adaptive direct search or linearly constrained pattern search can reuse, and checks the details the paper handles briefly: the lattice argument, the feasibility of the chosen coordinate step, and uniform constants.

Difficulty

The obvious argument copies the unconstrained proof with $\nabla f$ replaced by $q$ . The step that fails is the existence of a good trial step: in the unconstrained case some pattern direction makes an acute angle with $-\nabla f(x_k)$ , but near the boundary of $\Omega$ that direction may leave the feasible region, and a feasible direction may not be a descent direction. For a general pattern no uniform choice exists, and the paper's counterexample in §5.2 shows convergence can fail. The diagonality of $BM_k$ is what makes the pattern contain coordinate directions, one of which is both feasible and a descent direction of quality $n^{-1/2}\|q_k\|$ (Proposition 4.2). The second difficulty is Theorem 4.5, which uses no derivatives: it rests on the rationality of $\tau$ and the integrality of the $C_k$ , which confine the iterates to a lattice that meets the compact set $L_\Omega(x_0)$ in finitely many points.

Formalization scope

Points are EuclideanSpace ℝ (Fin n) with the Euclidean norm; the bounds are Fin n → EReal with the hypothesis $\ell_j<u_j$ for all $j$ , so infinite bounds are allowed as in the paper. Paper coordinates $1,\dots,n$ are Lean's Fin n. The gradient is Mathlib's gradient f. A run of the method is a structure of sequences $(x_k,\Delta_k,s_k,M_k,L_k)$ together with a predicate IsGPSRun that encodes §2.1–§2.4 clause by clause; the parameter $m\ge1$ is the number of columns of $L_k$ (the paper's $p-2n$ ). $\tau$ is rational and the $C_k$ are integer matrices, as the lattice argument requires. " $\min\{f(x_k+y):\dots\}<f(x_k)$ " over the finite set of feasible core trial points is encoded as "some feasible core trial step strictly decreases $f$ ". $\liminf$ statements are encoded with ∃ᶠ, not Filter.liminf. The modulus of continuity $\omega$ is not formed as a real supremum; Proposition 4.1 takes an explicit radius $\delta>\|d\|$ .

Standing assumptions and every departure from the page:

Smoothness. The page assumes $f$ continuously differentiable on $L_\Omega(x_0)$ . The mission assumes $f$ is $C^1$ on an open set $U\supseteq\Omega$ . The proofs evaluate $\nabla f$ along segments to trial points that lie in $\Omega$ but generally outside $L_\Omega(x_0)$ , and $L_\Omega(x_0)$ may have empty interior, so the page's hypothesis does not define what the proofs use.
Strong Hypothesis 3. The page prints $f(x_k+s_k)<\min\{\cdots\}$ . No core step can satisfy the strict form, which would exclude coordinate search, which the paper says satisfies it. The mission uses $\le$ , the form of Torczon (1997) and the one the proof of Proposition 4.3 uses. The theorem with $\le$ implies the one with $<$ .
The nonemptiness of $\{w_1,\dots,w_L\}$ is made explicit.
Proposition 3.1 (7) is omitted: its $P(g(x))$ is a projected gradient the paper does not define.
Proposition 4.2 quantifies over every step length below $\nu_k$ , because $\nu_k$ does not depend on $\Delta_k$ .

The run predicate is not vacuous: an explicit run of coordinate search on $f(x)=x$ over $[0,\infty)$ satisfies IsGPSRun, the Strong Hypotheses, bounded columns, $\Delta_k\to0$ and compactness of $L_\Omega(x_0)$ . That check is proved in Lean without sorry, so the goal cannot be closed by exhibiting an unsatisfiable hypothesis.

A complete development needs the mean value theorem along segments, uniform continuity of $\nabla f$ near the compact set $L_\Omega(x_0)$ , finiteness of a discrete lattice inside a compact set, and elementary facts about the coordinatewise projection. The projection and lattice lemmas are reusable beyond this mission. Proofs of any milestone, alternative proofs, and a general statement of Proposition 3.1 for closed convex $\Omega$ are welcome.

Selected references

R. M. Lewis and V. Torczon, Pattern Search Algorithms for Bound Constrained Minimization, ICASE Report No. 96-20 (NASA CR-198306), 1996; SIAM J. Optim. 9(4):1082–1099, 1999. https://doi.org/10.1137/S1052623496300507
V. Torczon, On the Convergence of Pattern Search Algorithms, SIAM J. Optim. 7(1):1–25, 1997. https://doi.org/10.1137/S1052623493250780
P. H. Calamai and J. J. Moré, Projected Gradient Methods for Linearly Constrained Problems, Math. Program. 39:93–116, 1987. https://doi.org/10.1007/BF02592073
A. R. Conn, N. I. M. Gould and P. L. Toint, Global Convergence of a Class of Trust Region Algorithms for Optimization with Simple Bounds, SIAM J. Numer. Anal. 25(2):433–460, 1988. https://doi.org/10.1137/0725029
R. Hooke and T. A. Jeeves, "Direct Search" Solution of Numerical and Statistical Problems, J. ACM 8(2):212–229, 1961. https://doi.org/10.1145/321062.321069

16 thms3 active usersReviewed

Completed

Combinatorics Complexity Theory Theoretical Computer Science·Captain: mikedeng1

Fast Algorithms for Finding Nearest Common Ancestors I: A Lower Bound for Pointer MachinesResearch Paper

Motivation

The nearest common ancestor problem asks, for a rooted tree and two of its vertices $x$ and $y$ , for the deepest vertex that is an ancestor of both, written $\operatorname{nca}(x,y)$ . It appears as a subroutine in string algorithms (suffix trees), in graph algorithms (path queries, dominators) and in the analysis of set-union structures. Aho, Hopcroft and Ullman (On finding lowest common ancestors in trees, SIAM J. Comput. 5, 1976) posed it in several versions, differing in how much the tree changes while the queries are answered.

Harel and Tarjan (Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13, 1984) study how the answer depends on the machine model. On a random-access machine, where addresses can be computed arithmetically, they preprocess a static tree in linear time and then answer each query in constant time. On a pointer machine, where memory can only be traversed by following pointers, their §2 shows that no representation of the tree allows constant-time queries: $\Omega(\log\log n)$ steps are needed in the worst case. This mission formalizes that lower bound.

Timeline.

1976: Aho, Hopcroft and Ullman give an $O(\log\log n)$ -per-query random-access algorithm for static trees.
1976: van Leeuwen (Finding lowest common ancestors in less than logarithmic time, unpublished report, reference [14] of Harel–Tarjan) gives an $O(n + m\log\log n)$ algorithm for static trees that runs on a pointer machine.
1984: Harel and Tarjan prove Theorem 1, the matching $\Omega(\log\log n)$ lower bound for pointer machines, and the $O(1)$ -per-query random-access algorithm.

Setting

A pointer machine stores its data as a collection of nodes. Each node has a fixed number of fields, and a pointer field holds either a node or nil. The machine can follow a pointer from a node it holds, but it cannot compute an address. Following Harel and Tarjan (p. 340), a static tree is represented by a list structure: each tree vertex $v$ is represented by a single node $\mathrm{rep}(v)$ , distinct vertices by distinct nodes, and the structure may contain further nodes that represent no vertex. Each node has two pointer fields; the paper reduces any fixed number of pointers to two "without loss of generality". To answer a query on $x$ and $y$ , the machine is given pointers to $\mathrm{rep}(x)$ and $\mathrm{rep}(y)$ and must return a pointer to $\mathrm{rep}(\operatorname{nca}(x,y))$ .

The node $b$ is accessible from $a$ in $j$ steps or less if it can be reached from $a$ by following at most $j$ pointers. Write $\mathrm{acc}_j(a)$ for the set of such nodes. A run of $t$ steps from input nodes $a$ and $b$ is a sequence $n_1,\dots,n_t$ in which each $n_s$ is the content of a pointer field of a node among $a, b, n_1, \dots, n_{s-1}$ . A query with answer $c$ is answered in $k$ steps if some run of at most $k$ steps holds $c$ .

The tree is the complete binary tree $T$ of height $h$ , with $n = 2^h$ leaves. Its vertices are the words $w \in \{0,1\}^{\le h}$ (the root-to-vertex path, $0$ = left), the ancestors of $v$ are its prefixes, the depth of $w$ is $|w|$ and its height is $h - |w|$ . Then $\operatorname{nca}(x,y)$ is the longest common prefix of $x$ and $y$ . Logarithms are binary: $\lg = \log_2$ .

Formalization targets

Goal: Theorem 1 in the explicit form of its proof

For every $h$ , every node type, every list structure with two pointers per node and every injective representation $\mathrm{rep}$ of the complete binary tree with $n = 2^h$ leaves: if every nca query on two leaves is answered in $k$ steps, then

k > \lg\lg n - 2 .

This is the last display of the proof (p. 341), which is what the paper's $\Omega(\log\log n)$ means. The representation is arbitrary and is quantified before the query bound, so the bound holds for every representation.

Milestones: the claims of the proof

A query answered in $k$ steps reaches only nodes in $\mathrm{acc}_k(\mathrm{rep}(x)) \cup \mathrm{acc}_k(\mathrm{rep}(y))$ .
$|\mathrm{acc}_j(a)| \le 2^{j+1} - 1$ for every node $a$ .
With $A_x$ the set of vertices whose nodes are accessible from $\mathrm{rep}(x)$ in $k$ steps or less: for a nonleaf $w$ with children $u, v$ , either $w \in A_x$ for every leaf $x$ below $u$ , or $w \in A_y$ for every leaf $y$ below $v$ .
A vertex of height $i \ge 1$ lies in $A_x$ for at least $2^{i-1}$ leaves $x$ .

\sum_{x \in L} |A_x| \ge \frac{n}{2}\lg n,

where $L$ is the set of leaves.

Significance

The result. Theorem 1 shows that van Leeuwen's pointer-machine algorithm for static trees is optimal up to a constant factor, and that the constant-time queries of the paper's §§3–5 depend on address arithmetic. It is an early nontrivial lower bound for pointer machines on a natural problem; the paper compares it with Tarjan's lower bound for disjoint-set union on a pointer machine (J. Comput. System Sci. 18, 1979).

Formalizing it. The theorem is proved in the paper; as far as could be determined no machine-checked version exists, and Mathlib has no pointer-machine model. The mission produces an explicit, reusable definition of pointer-machine runs and accessibility together with a complete proof of the explicit bound. A formal model of this kind is the precondition for stating any other pointer-machine lower bound.

Difficulty

The statement must hold for every representation, including structures with many auxiliary nodes and arbitrary pointers between tree nodes. Arguing about one natural representation, such as parent pointers, where a leaf is far from its ancestors, says nothing about other representations: a structure with shortcut pointers or auxiliary nodes may bring some ancestors close to some leaves, and the bound must survive every such choice. In the formal setting the counting also has to handle overlaps: nodes reachable from several leaves, nodes that represent no vertex, and pointer cycles.

Formalization scope

Model. Nodes form an arbitrary type N, not necessarily finite. ptr : N → Fin 2 → Option N gives the two pointer fields (none = nil), and rep : Vertex h → N is required to be injective. acc ptr j a is defined recursively. Run ptr a b t held is an inductive predicate for runs of $t$ steps, AnsweredIn asks for some run of at most $k$ steps holding the answer, and AnswersLeafQueriesIn ptr rep k requires this for every pair of leaves.
Conventions.
- Two pointer fields per node, as the paper's "without loss of generality" reduction allows; the reduction itself is not formalized.
- Only queries on two leaves are assumed answerable. This is weaker than all queries, so the theorem is at least as strong as the paper's.
- Time is counted as pointer-following steps. Mutation of the structure during a query and non-pointer fields are not modelled: neither lets the machine hold a node it has not reached by following pointers. The clause "the algorithm remembers nothing between queries" is built into the static structure.
- Vertex h is {s : List Bool // s.length ≤ h}, nca is the longest common prefix, and a separate theorem identifies it with the Appendix's deepest common ancestor. $n = 2^h$ counts leaves, not vertices.
- $\lg$ is Real.logb 2. For $h = 0$ Lean's $\log_2 0 = 0$ gives the true statement $k > -2$ ; for $h \ge 1$ , $\lg\lg n = \log_2 h$ .
- Cardinalities in the milestones are Set.encard in $\mathbb N \cup \{\infty\}$ , so finiteness is part of each claim. Divisions are cleared: $h\,2^h \le 2\sum_x |A_x|$ .
Ruling out trivial formalizations. The hypothesis AnswersLeafQueriesIn is satisfiable: the parent-pointer representation answers every leaf query in $h$ steps. If rep were not injective, a constant rep would answer every query in zero steps, so injectivity is kept in the goal. The milestones do not need it and do not assume it.
Infrastructure. The goal needs finite-set counting over the leaves of the complete binary tree and a double count over heights. The run and accessibility definitions are reusable for other pointer-machine arguments. Proofs of the milestones, and of the ℕ form $h < 2^{k+2}$ that the goal reduces to, are welcome.

Selected references

D. Harel, R. E. Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13(2):338–355, 1984. https://doi.org/10.1137/0213024
A. V. Aho, J. E. Hopcroft, J. D. Ullman, On finding lowest common ancestors in trees, SIAM J. Comput. 5(1):115–132, 1976. https://doi.org/10.1137/0205011
A. Schönhage, Storage modification machines, SIAM J. Comput. 9(3):490–508, 1980. https://doi.org/10.1137/0209036
R. E. Tarjan, A class of algorithms which require nonlinear time to maintain disjoint sets, J. Comput. System Sci. 18(2):110–127, 1979. https://doi.org/10.1016/0022-0000(79)90042-4

8 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Numerical Analysis+1·Captain: mikedeng1

Proximal Newton-Type Methods for Minimizing Composite Functions II: Local Linear and Superlinear Convergence of the Inexact Proximal Newton MethodResearch Paper

Motivation

Many estimation problems in statistics, signal processing and bioinformatics minimize a composite function $f = g + h$ : a smooth convex loss $g$ plus a convex but nonsmooth penalty or constraint $h$ , such as the lasso's $\ell_1$ norm or the indicator of a convex set. Proximal Newton-type methods handle such problems by minimizing, at each iterate $x_k$ , a model $\hat f_k = \hat g_k + h$ in which $g$ is replaced by its second-order Taylor expansion. Widely used solvers of this kind (glmnet, newGLMNET, QUIC) never solve these model subproblems exactly; they stop an inner iterative solver early by some heuristic. Lee, Sun and Saunders (arXiv:1206.1623v13, 2014) proposed an adaptive stopping rule for the inner solver and proved that it preserves fast local convergence. This mission formalizes that local convergence theory (§3.4 of the paper).

Timeline:

1982: Dembo, Eisenstat and Steihaug introduce inexact Newton methods for smooth equations and prove local linear and superlinear convergence under a relative-residual condition with forcing terms $\eta_k$ (doi:10.1137/0719025).
1996: Eisenstat and Walker propose self-adjusting forcing terms that avoid oversolving (doi:10.1137/0917003).
2012–2014: Lee, Sun and Saunders transfer the relative-residual condition to composite functions, replacing gradients by composite gradient steps, and prove Theorems 3.10 and 3.11.
2016: Byrd, Nocedal and Oztoprak analyze inexact proximal Newton methods for $\ell_1$ -regularized problems under an additional sufficient-descent condition on the subproblem (doi:10.1007/s10107-015-0941-y).

Setting

Work in $\mathbb R^n$ with the Euclidean inner product. The smooth part $g:\mathbb R^n\to\mathbb R$ is twice continuously differentiable and strongly convex with constant $m>0$ : $g(y)\ge g(x)+\nabla g(x)^T(y-x)+\frac m2\|x-y\|^2$ for all $x,y$ . Its gradient $\nabla g$ is Lipschitz with constant $L_1$ , its Hessian $\nabla^2 g$ is Lipschitz with constant $L_2$ , and $\nabla^2 g(x)\preceq MI$ for a constant $M>0$ . The nonsmooth part $h$ is proper, closed and convex, and may take the value $+\infty$ ; it is given by its domain $D$ and its values on $D$ . The problem is $\min_x f(x)=g(x)+h(x)$ , and $x^\star$ denotes its (unique) optimal solution.

The proximal mapping of $h$ is $\operatorname{prox}_h(v)=\arg\min_y h(y)+\frac12\|y-v\|^2$ . The composite gradient step with step length $t>0$ is

G_{tf}(x)=\tfrac1t\big(x-\operatorname{prox}_{th}(x-t\nabla g(x))\big),

with $G_f=G_{1f}$ ; it vanishes exactly at minimizers of $f$ and plays the role of the gradient. The step $G_{f/M}$ is the unit step on $f/M=g/M+h/M$ . The model at $x_k$ is $\hat f_k=\hat g_k+h$ with $\hat g_k(y)=g(x_k)+\nabla g(x_k)^T(y-x_k)+\frac12(y-x_k)^T\nabla^2 g(x_k)(y-x_k)$ .

The inexact proximal Newton method with unit step lengths produces $x_{k+1}=x_k+\Delta x_k$ , where the direction $\Delta x_k$ is any point satisfying the adaptive stopping condition

\|G_{\hat f_k/M}(x_k+\Delta x_k)\|\le\eta_k\,\|G_{f/M}(x_k)\|\qquad(2.24)

for a forcing term $\eta_k\ge0$ . The Eisenstat–Walker choice is

\eta_k=\min\Big\{\frac m2,\ \frac{\|G_{\hat f_{k-1}/M}(x_k)-G_{f/M}(x_k)\|}{\|G_{f/M}(x_{k-1})\|}\Big\}.\qquad(2.25)

Formalization targets

Goal: Theorem 3.10 (p. 17)

There are $\bar\eta\in(0,m/2)$ , $\delta>0$ and $r\in[0,1)$ such that, whenever $0\le\eta_k\le\bar\eta$ for all $k$ and $\|x_0-x^\star\|<\delta$ ,

\|x_{k+1}-x^\star\|\le r\,\|x_k-x^\star\|\quad\text{for all }k.

For every forcing sequence with $\eta_k\ge0$ , $\eta_k\to0$ , there is $\delta>0$ such that every run with $\|x_0-x^\star\|<\delta$ converges to $x^\star$ q-superlinearly: for every $\varepsilon>0$ , eventually $\|x_{k+1}-x^\star\|\le\varepsilon\|x_k-x^\star\|$ .

Both parts are asserted together. The statement fixes no constant beyond the existence of $\bar\eta$ , $\delta$ and $r$ .

Milestones

§2.1, property 3: $G_f(x)=0$ if and only if $x$ minimizes $f$ .
Lemma 2.2: $\|G_f(x)\|\le(L_1+1)\|x-x^\star\|$ .
Lemma 3.8: $\|G_f(x)-G_{\hat f_k}(x)\|\le\frac{L_2}2\|x-x_k\|^2$ .
Lemma 3.9: $(x-y)^T(G_{tf}(x)-G_{tf}(y))\ge\frac m2\|x-y\|^2$ for $0<t\le1/L_1$ .
Theorem 3.11: with the forcing terms (2.25), the method converges q-superlinearly from every start sufficiently close to $x^\star$ .

Significance

Theorem 3.10 justifies stopping the inner solver of a proximal Newton method at a relative accuracy that is set by the current optimality measure $\|G_{f/M}(x_k)\|$ : a constant small forcing term keeps linear convergence, and forcing terms that decay to zero recover superlinear convergence, with no sufficient-descent condition on the subproblem and for a generic nonsmooth $h$ . Theorem 3.11 shows that the self-adjusting choice (2.25) achieves the superlinear regime automatically. Together they are the composite analogue of the inexact Newton theory used in most large-scale smooth solvers.

The results are proved in the paper. No machine-checked proof of any of them is known, and the platform contains no proximal mapping, composite gradient step or inexact Newton condition. A formalization adds a checked proximal-operator toolkit (existence and nonexpansiveness of $\operatorname{prox}$ , the optimality characterization of $G_f$ , strong monotonicity of $G_{tf}$ ) and a precise form of the theorem: the paper's proofs mix two scalings of the composite step and cite a lemma where another is meant, so the formal proof settles which constants are valid.

Difficulty

The obvious argument compares the inexact step with the exact proximal Newton step and treats the gap as a perturbation. For composite functions this fails: the exact step is defined by a nonsmooth inclusion, and the stopping condition bounds a residual of the model's composite gradient step, not the distance to the model's minimizer. The link between the two is strong monotonicity of the composite gradient step (Lemma 3.9), which requires controlling the proximal mapping of a general closed convex $h$ jointly with the curvature of $g$ ; for $h=0$ it is immediate, and for general $h$ it is the central step. A second difficulty is that the threshold on $\eta_k$ is not scale invariant: a threshold below $m/2$ chosen arbitrarily does not give convergence, so the admissible $\bar\eta$ has to come out of the analysis.

Formalization scope

The space is EuclideanSpace ℝ (Fin n). The nonsmooth part is a pair $(D,h)$ : $D$ nonempty and convex, $h$ convex on $D$ , and the extended function ( $h$ on $D$ , $+\infty$ off $D$ ) lower semicontinuous; indicator functions of closed convex sets are included. The proximal mapping is a total function chosen among the minimizers over $D$ , which exist uniquely under these hypotheses. $G_{f/M}$ , $G_{\hat f_k/M}$ and $G_{tf}$ are functions of the split $(g,D,h)$ and a scalar, never of $f$ alone. The Hessian is the derivative of the gradient map, measured in operator norm. Sequences are indexed from $k=0$ ; a run requires $x_0\in D$ and $x_k+\Delta x_k\in D$ . Rates are stated without quotients.

" $x_0$ sufficiently close to $x^\star$ " is an existential radius chosen before the run; assuming $x_k\to x^\star$ , letting the radius depend on the run, or reading part 1 as "for every $\bar\eta<m/2$ " (which is false: $g(x)=2x^2$ , $h=0$ , $\eta_k\equiv\frac32$ diverges) are ruled out. The forcing sequence of Theorem 3.10 is fixed in advance; that of Theorem 3.11 depends on the iterates through (2.25), with a free first term $\eta_0\in[0,m/2]$ .

A complete development needs existence, uniqueness and firm nonexpansiveness of the proximal mapping of an extended-valued closed convex function, the subgradient characterization of $\operatorname{prox}$ , and a second-order Taylor bound for $C^2$ functions with Lipschitz Hessian. These are reusable well beyond this mission. Contributions of any of them, of the milestones, or of alternative proofs of Lemma 3.9 are welcome.

Selected references

J. D. Lee, Y. Sun, M. A. Saunders, Proximal Newton-type methods for minimizing composite functions, arXiv:1206.1623v13, 2014; SIAM J. Optim. 24(3), 2014. https://arxiv.org/abs/1206.1623
R. S. Dembo, S. C. Eisenstat, T. Steihaug, Inexact Newton methods, SIAM J. Numer. Anal. 19(2), 1982. https://doi.org/10.1137/0719025
S. C. Eisenstat, H. F. Walker, Choosing the forcing terms in an inexact Newton method, SIAM J. Sci. Comput. 17(1), 1996. https://doi.org/10.1137/0917003
R. H. Byrd, J. Nocedal, F. Oztoprak, An inexact successive quadratic approximation method for L-1 regularized optimization, Math. Program. 157, 2016. https://doi.org/10.1007/s10107-015-0941-y

9 thms3 active usersReviewed

Completed

Graph Theory Operations Research Optimization+1·Captain: mikedeng1

A New Approach to the Maximum-Flow Problem 2: The Nonsaturating-Push Bound for FIFO Push-RelabelResearch Paper

Motivation

The maximum-flow problem asks how much of a commodity can be sent from a source to a sink through a network whose edges carry capacities. It is a basic model of operations research. Transportation, scheduling, bipartite matching and image segmentation reduce to it, and it is the inner step of many combinatorial algorithms.

Goldberg and Tarjan introduced the push–relabel (preflow) method in A New Approach to the Maximum-Flow Problem (J. ACM 35(4), 1988). Ford–Fulkerson-type algorithms augment along whole source–sink paths. The push–relabel method instead moves excess flow across single edges, guided by integer distance labels on the vertices. Whatever order its local operations are applied in, it is correct and performs $O(n^2 m)$ of them (§3 of the paper). Section 4 shows that one particular order, processing the active vertices first-in, first-out, cuts the dominant term, the number of nonsaturating pushes, to $O(n^3)$ . The method and its FIFO and highest-label variants are the standard practical maximum-flow codes.

Timeline:

1956: Ford and Fulkerson, augmenting paths and max-flow min-cut.
1970–72: Dinic, and Edmonds and Karp, give polynomial augmenting-path bounds.
1974: Karzanov introduces preflows and obtains $O(n^3)$ .
1982: Shiloach and Vishkin give a parallel $O(n^2 \log n)$ preflow algorithm with a first-in, first-out flavour.
1988: Goldberg and Tarjan, the generic push–relabel method, the FIFO bound of this mission, and $O(nm \log(n^2/m))$ with dynamic trees.

Setting

A flow network has a finite vertex set $V$ with $n = |V|$ , a capacity $c(v,w) \ge 0$ on every ordered pair, a source $s$ and a sink $t \neq s$ . The edges are the pairs with $c(v,w) > 0$ , and there are no loops. A preflow is a function $f$ on vertex pairs with $f(v,w) \le c(v,w)$ and $f(v,w) = -f(w,v)$ . Its excess $e(v) = \sum_u f(u,v)$ must be nonnegative at every $v \neq s$ . The residual capacity is $r_f(v,w) = c(v,w) - f(v,w)$ . A labeling $d$ assigns each vertex a value in $\mathbb{N} \cup \{\infty\}$ . A vertex $v \notin \{s,t\}$ is active if $d(v) < \infty$ and $e(v) > 0$ .

The two basic operations (Fig. 1 of the paper) are:

push $(v,w)$ , applicable when $v$ is active, $r_f(v,w) > 0$ and $d(v) = d(w)+1$ . It sends $\delta = \min(e(v), r_f(v,w))$ from $v$ to $w$ . The push is saturating if $r_f(v,w) = 0$ afterwards and nonsaturating otherwise.
relabel $(v)$ , applicable when $v$ is active and $d(v) \le d(w)$ for every residual edge $(v,w)$ . It sets $d(v) \leftarrow \min\{d(w)+1 : r_f(v,w) > 0\}$ .

The algorithm starts by saturating every edge leaving $s$ , with $d(s) = n$ and $d(v) = 0$ for $v \neq s$ .

In the first-in, first-out algorithm (§4), each vertex $v$ scans a fixed list $L(v)$ of its neighbours through a current edge. The push/relabel $(v)$ operation pushes through the current edge if possible. Otherwise it advances the current edge, or, at the end of the list, returns to the first edge and relabels $v$ . Active vertices wait in a queue $Q$ , initially $\{v \in V - \{s,t\} : c(s,v) > 0\}$ . The discharge operation removes the front vertex $v$ and repeats push/relabel $(v)$ until $e(v) = 0$ or $d(v)$ increases. Every vertex that becomes active meanwhile is appended to $Q$ , and $v$ is appended too if it is still active. Passes over the queue are defined inductively. Pass 1 consists of the discharges of the initially queued vertices. Pass $i+1$ consists of the discharges of vertices added during pass $i$ .

Formalization targets

Goal: Corollary 4.4 (p. 931)

For every network, every edge-list order, every initial queue order, and every run of the FIFO algorithm,

\#\{\text{nonsaturating pushes}\} \le 4n^3 .

The constant is the printed one.

Milestones

Lemma 4.1 (p. 929): the push/relabel operation relabels only when relabeling is applicable.
Lemma 3.5 (p. 926): from any vertex with positive excess, the source is reachable in the residual graph.
Lemma 3.7 (p. 927): at any time, $d(v) \le 2n-1$ for every vertex.
Lemma 3.8 (p. 927): at most $2n-1$ relabelings per vertex and at most $(2n-1)(n-2) < 2n^2$ in total.
Lemma 4.3 (p. 930): at most $4n^2$ passes over the queue.

Significance

Corollary 4.4 is the combinatorial core of Theorem 4.5, which states that the FIFO algorithm runs in $O(n^3)$ time. Theorem 4.2 shows that the remaining work of the implementation is $O(nm)$ plus constant time per nonsaturating push. The bound of Corollary 4.4 is therefore what separates the $O(n^3)$ FIFO method from the $O(n^2 m)$ bound of the generic method, which matters on dense networks. The same pass-counting argument is reused for the parallel algorithm of §6 and underlies later analyses of highest-label and wave variants.

The results are proved in the paper. Formalizing them adds an analysis of a push–relabel algorithm, which the platform does not yet have. Its existing network-flow material states max-flow min-cut and Ford–Fulkerson termination in an arc-based model with nonnegative flows (the Introduction to Linear Optimization missions). The mission builds a precise operational model of the FIFO implementation, with edge lists, current edges and a queue carrying pass numbers, and states an explicit operation count for it. A companion mission in this series treats the generic algorithm's correctness and its $(2n-1)(n-2) + 2nm + 4n^2m$ operation bound.

Difficulty

The obvious argument is the potential-function count of §3, over the sum of the labels of active vertices. It yields only $4n^2 m$ and does not use the queue discipline at all. The $4n^3$ bound has to charge nonsaturating pushes to passes over the queue, and then bound the number of passes by the total growth of the labels. Neither step is visible in the generic algorithm, because both depend on the order in which vertices are processed.

Making this rigorous requires invariants of the implementation that the paper uses silently:

a vertex is in the queue exactly when it is active, and at most once;
pass numbers are nondecreasing along the queue;
current edges only move forward between relabelings.

Lemma 4.1 in particular depends on the current-edge scan: an edge passed over earlier stays inadmissible until $v$ is relabeled.

Formalization scope

The Lean development works in namespace GoldbergTarjan.FIFO. Vertices form a type V with [Fintype V] [DecidableEq V], and $n$ is Fintype.card V. Capacities are c : V → V → ℝ with c ≥ 0 and c v v = 0. Flows are antisymmetric real functions on all ordered pairs, not nonnegative arc flows. Excess is computed from the flow. Labels are in ℕ∞, and the empty minimum in relabel is ⊤.

The state of the algorithm consists of the flow, the labels, the current-edge index cur v into the edge list L v, and the queue Q : List (V × ℕ), each entry tagged with its pass number. Push/relabel (Fig. 3) is a total function, and a discharge (Fig. 4) is a relation carrying the number of push/relabel operations it performs. A run consists of the states S 0, …, S K with S 0 the initial state and consecutive states related by one discharge. The printed variant of Fig. 4, which stops as soon as $v$ is relabeled, is the one formalized. Counts are natural numbers over all push/relabel operations of all discharges. The number of passes is the largest pass tag of a discharged entry.

All constants are explicit, exactly as printed:

$2n-1$ (Lemmas 3.7, 3.8);
$(2n-1)(n-2)$ and $2n^2$ (Lemma 3.8);
$4n^2$ (Lemma 4.3);
$4n^3$ (Corollary 4.4).

No asymptotic notation is used, and no $m \ge n-1$ assumption is made.

A model without current edges, where relabeling happens whenever no push applies, would make Lemma 4.1 vacuous and change the algorithm. Pass numbers that are not propagated by the "added during pass $i$ " rule would make the pass count arbitrary. Both are ruled out by the definitions. A sorry-free check, outside the proposal, exhibits a three-vertex network with two legal discharges, two passes and no nonsaturating push, so the run hypotheses are satisfiable.

Reusable beyond this mission are the network, preflow, push and relabel definitions and Lemma 3.5, which is about an arbitrary preflow. Contributions welcome: invariants of FIFO runs (preflow, valid labeling, queue = active set, cur within bounds), proofs of the milestones, and the reduction of Corollary 4.4 to Lemma 4.3.

Selected references

A. V. Goldberg, R. E. Tarjan, A New Approach to the Maximum-Flow Problem, Journal of the ACM 35(4):921–940, 1988. https://doi.org/10.1145/48014.61051
A. V. Karzanov, Determining the maximal flow in a network by the method of preflows, Soviet Math. Doklady 15:434–437, 1974.
Y. Shiloach, U. Vishkin, An O(n² log n) parallel max-flow algorithm, Journal of Algorithms 3(2):128–146, 1982. https://doi.org/10.1016/0196-6774(82)90013-X
L. R. Ford, D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5
J. Edmonds, R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, Journal of the ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699

10 thms3 active usersReviewed

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Robust Control of Markov Decision Processes with Uncertain Transition Matrices 3: Stationary Policies Suffice and the Stationary/Time-Varying Uncertainty Gap Vanishes GeometricallyResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4 (p. 786)

Milestones (proof order of the paper)

Significance

Difficulty

Formalization scope

Selected references

A Linear-Time Algorithm for Finding a Sparse k-Connected Spanning Subgraph of a k-Connected Graph 2: FOREST's Forests E_i Preserve Local Node-Connectivity up to i in a Simple GraphResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.1

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

A Linear-Time Algorithm for Finding a Sparse k-Connected Spanning Subgraph of a k-Connected Graph 1: The FOREST Decomposition Preserves Local Edge-ConnectivityResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.1 (pp. 588–589), without the running time

Milestones

Companions

Significance

Difficulty

Formalization scope

Selected references

Disjunctive Programming XI: The Cut-Generating LP Under a Ray NormalizationTextbook

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Disjunctive Programming X: Solving the Cut-Generating LP on the Simplex TableauTextbook

Motivation

Setting

Formalization targets

Theorem 9.3 (goal) — the most-improving pivot column

The chain of results building toward it

Significance

Difficulty

Formalization scope

Selected references

Disjunctive Programming VI: Extended Formulations for Perfectly Matchable Subgraph PolytopesTextbook

Motivation

Setting

Formalization targets

Theorem 5.1 (goal) — the PMS polytope of a bipartite graph

Theorem 5.2 — the Assignable Subgraph Polytope

Theorem 5.3 — the sss-ttt Path Decomposable Subgraph Polytope

Theorem 5.4 — the PMS polytope of an arbitrary graph

Significance

Difficulty

Formalization scope

Selected references

The Relaxation Method for Linear Inequalities II: For a Lower-Dimensional Solution Polytope Infinite Reflexions Settle on a Sphere with Axis L_rResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2

Milestones (the paper's own intermediate claims)

Significance

Difficulty

Formalization scope

Selected references

Adversarially Robust Generalization Requires More Data 4: Robust Learning from One Thresholded Sample in the Bernoulli ModelResearch Paper

Motivation

Setting

Theorem 5.3 — the $s$ - $t$ Path Decomposable Subgraph Polytope