Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
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.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
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.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
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.
The sharp Hlawka inequality for Schatten -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 . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The eigenvalues of the Laplacian of a graph carry metric information about the graph. The second-smallest one, , was named the algebraic connectivity by Fiedler (Fiedler 1973), who showed it is positive exactly for connected graphs. N. Alon and V. D. Milman (J. Combin. Theory Ser. B 38 (1985) 73–88) showed that a large also forces two further properties: small diameter and a concentration of measure phenomenon, in which almost every vertex is close to any set containing half the vertices. They used these facts to build explicit expanders and superconcentrators, which are sparse networks with strong connectivity guarantees used in the theory of computation and in communication network design.
This mission covers Section 2 of that paper, "The Main Tools": the edge-count inequality (Lemma 2.1), the isoperimetric inequalities (Theorems 2.5 and 2.6), and the resulting diameter bound (Theorem 2.7).
Timeline:
Let be a finite, connected, simple graph on vertices. Write for the degree of a vertex , for the maximum degree, and for the adjacency matrix. The Laplacian is the matrix
For real functions on with scalar product , the quadratic form of is . The eigenvalues of , counted with multiplicity, are real and are written . The algebraic connectivity is the second-smallest of them.
For vertices , is the number of edges of a shortest path from to . For disjoint vertex sets the paper writes for the distance between them, and for their relative sizes, and () for the set of edges with both endpoints in (in ). denotes the integer part of .
Each statement keeps the paper's explicit constants. The goal is the endpoint of this chain and the paper's headline graph-theoretic bound.
Theorem 2.7 gives, for any family of graphs of bounded maximum degree whose algebraic connectivity stays bounded away from zero, a diameter of order . By the paper's Remark 2.8, the 4-regular graphs constructed in its Section 4 show that this order cannot be improved. Theorem 2.6 is a discrete concentration of measure inequality: the proportion of vertices at distance more than from a set of relative size decays exponentially in . It is the graph analogue of the Gromov–Milman concentration for manifolds, and Section 3 of the paper applies it to cubes and other product graphs. Theorem 2.5 is the input for the construction of expanders from graphs with a spectral gap (Theorem 4.3 of the paper).
All results are proved in the paper, and the formal work here is a machine-checked version of known proofs. As far as could be determined, none of the four inequalities (Lemma 2.1, Theorems 2.5–2.7) has been formalized in Lean or elsewhere. Mathlib has the Laplacian matrix, its positive semidefiniteness, and the relation between its kernel and connected components, but no statement about its second eigenvalue. The spectral facts (milestones 1–2), stated for Mathlib's Matrix.IsHermitian.eigenvalues₀, are reusable for any future work on algebraic connectivity.
The combinatorial steps are short. The work is at the interface between the spectral definition and the quadratic form. Mathlib defines eigenvalues through the spectral theorem for a Hermitian matrix, sorted into a list. Obtaining Rayleigh's principle for the second eigenvalue from that list, with the constant functions as the eigenvector of , takes a Courant–Fischer-type argument over an orthonormal eigenbasis. It does not follow from positive semidefiniteness alone. Strict positivity of additionally needs that the kernel of is one-dimensional for a connected graph.
Theorem 2.6 iterates Theorem 2.5 over a sequence of neighbourhoods with a real step length , so it needs bookkeeping of integer parts and of real-valued distance thresholds. Theorem 2.7 then combines Theorem 2.6 with Remark 2.3 and needs the estimate with the integer part kept. Replacing by the real number inside it changes the statement.
SimpleGraph V on a Fintype vertex type with decidable adjacency. Every item assumes G.Connected and (the goal writes , as the paper does).G.lapMatrix ℝ. is the mission definition AlonMilman.Diameter.lambda1: the eigenvalue at index of eigenvalues₀, which lists the eigenvalues in decreasing order. It is by convention when , a case no theorem uses.SimpleGraph.diam without connectivity, since that is for a disconnected graph.SimpleGraph.dist (a natural number). "The distance between and is " is encoded as for all , . Because the bounds weaken as decreases, this is equivalent to the paper's exact distance. In Theorem 2.6 is real and the hypothesis is strict.AlonMilman.Diameter.edgesWithin G A. All counts are cast to before subtraction, is a real quotient, is Nat.floor, is Real.logb 2, and is Real.log.Contributions welcome: proofs of any milestone, and in particular general Mathlib-style lemmas for Rayleigh quotients and eigenvalues₀, which have uses beyond this mission.
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:
States form a finite set and actions a finite nonempty set . A stage cost is given for every state and action, together with a discount factor and an initial state . For every action and state a nonempty set of probability vectors in the simplex is given: the possible rows of the transition matrix . Rectangularity means that every row is chosen independently: one stage of nature is a family with -th row of in , and the set of such families is .
A controller policy assigns an action to each state at each stage; the set of all of them is , and the stationary ones (the same map at every stage) form . A nature policy picks one element of per stage; the set is , and the stationary ones form . Starting from , the state law evolves by . The discounted costs over horizon and over the infinite horizon are
For a controller class and a nature class the robust values are and . Finally and .
The second line is the paper's "the gap goes to zero at a geometric rate ", with the constant the paper's own argument produces.
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 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).
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 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 is a min–max value. The obvious attempt to exchange the infimum over with the supremum over from that per-nature fact alone fails; the exchange requires a duality statement for the stationary game.
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. is defined from the forward state distribution (not from a Bellman recursion) and reads only stages , so the finite-horizon values over infinite sequences are exactly the paper's values (3) and (4) with stage costs and zero terminal cost. is the sum of the series of nonnegative stage costs, which converges for and equals . Every min and max of the paper is a real infimum ⨅ or supremum ⨆; all families are nonempty and lie in , and attainment is not assumed anywhere. The discount factor satisfies , as in §4 of the paper.
The rate in the goal is the explicit bound ; 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.
Given a -connected graph, many connectivity algorithms run in time that grows with the number of edges . A sparse certificate is a spanning subgraph with only edges that is still -connected; computing one first and running the expensive algorithm on it replaces by in the bound. Finding a -connected spanning subgraph with the minimum number of edges is NP-complete for every fixed (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 . They showed that the prefix unions 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:
A graph has a finite node set with and a finite edge set ; 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 , is the spanning subgraph with edge set .
The local node-connectivity of nodes in a graph on is if and are adjacent in , and otherwise the minimum size of a node set whose deletion leaves no – path. The node connectivity is .
Procedure FOREST keeps a label on each node, initially . While some node is unscanned, it chooses an unscanned node of largest label; for each unscanned edge it puts into the class , increases by one if , and increases by one; then it marks scanned. Ties are broken arbitrarily. The time instants are the states between these elementary operations; denotes the class at an instant, and its final value. Put
For a simple graph and the classes of any completed run of FOREST, for ,
The statement is local: it holds pair by pair, not only for the global minimum, and for every tie-breaking of the procedure.
A companion item states the paper's announcement in §3: is -node-connected for every .
Theorem 3.1 at shows that the first classes of FOREST form a -node-connected spanning subgraph whenever is, and the edge-count analysis of the companion mission bounds its size by . Since FOREST runs in linear time, any algorithm testing can be run on instead of ; the paper uses this to improve the bound for testing from to , and similar gains for computing the number of node-disjoint paths between two nodes. The local form (3.1) is what makes the – 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.
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 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 of size in , the classes at the moments the nodes of 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.
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 (, 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.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.Many real-world disjunctive models are not unions of polyhedra in a single shared space, but unions of polyhedra in different spaces linked by a logical implication: some action affecting one set of entities has consequences for another. Balas's treatment of such models (§17 of the book, following [17]) reduces to understanding a single auxiliary object attached to each polytope in isolation: its dominant, the set of points that dominate (coordinatewise) some feasible point. Dominants and their duals, blockers, have a long history in combinatorial optimization — blocking-pair theory for covering and packing polyhedra traces to Fulkerson (D. R. Fulkerson, Blocking and anti-blocking pairs of polyhedra, Mathematical Programming 1 (1971), 168–194, https://doi.org/10.1007/BF01584085) — but this chapter develops a self-contained, constructive theory tailored to polytopes inside the unit cube, culminating in an exact, facet-complete description of the dominant for an arbitrary such polytope.
For a polyhedron , the dominant is , and the blocker is — the covering inequalities valid for
. (The blocker is not the reverse polar of 02b-polarity: restricting to the nonnegative
orthant is essential and changes the object.) For , the upper-separation
value is ; a violated covering inequality for
exists exactly when . A polytope is upper
monotone (with respect to ) if — the natural "closure" condition
under which the theory of this chapter applies cleanly.
For , write . Given and a coordinate subset , the projection keeps only the -coordinates, letting the rest range freely. is the set of valid inequalities of with exactly on , tight at linearly independent points of .
Proposition 13.1. For an upper monotone (each a single inequality in ), .
Theorem 13.3. For () upper monotone,
Theorem 13.5. For the same and any , with the greatest coordinate value satisfying and : and , an explicit, computable value.
Theorem 13.7 (goal). For an arbitrary polytope (not necessarily upper monotone):
and every one of these inequalities is facet-defining for .
Corollary 13.8. Every facet-defining inequality of has at most nonzero coefficients.
The targets move from the intersection-distributivity fact (13.1) through an explicit, exponentially-large but fully closed-form facet system for the single-inequality case (13.3) and its constructive, polynomial evaluation recipe (13.5) to the fully general facet characterization (13.7, requiring no monotonicity assumption at all) and its immediate corollary on facet sparsity (13.8).
Theorem 13.7 is a rare case in polyhedral combinatorics of a complete and exact facet description obtained for the dominant of an arbitrary polytope, not merely a valid relaxation or an algorithmic separation oracle — every facet is accounted for, and every listed inequality is genuinely a facet, not merely valid. Corollary 13.8's support bound is the mechanism that makes Theorem 13.10 (not part of this mission) tractable: it lets the facets of a dominant built from a disjunction of polytopes in different spaces be characterized purely in terms of each factor's own low-dimensional facets, avoiding an exponential blowup in the combined space.
Both directions are proved in the source (Balas's own treatment, following the joint framework of [17]) but have no counterpart on this platform: nothing existing treats dominants, blockers, or upper monotonicity. This mission produces the first Lean statements of all five targets.
The obvious shortcut for Theorem 13.7 is to state only the validity half of the claim (every inequality from is valid for ) and treat "facet-defining" as a decoration — after all, Proposition 13.1's polar-style validity argument generalizes easily. But the theorem's actual force is the converse: not merely that these inequalities suffice to describe , but that none of them is redundant, and no other facet exists. The book's own converse proof needs a genuine perturbation argument (splitting a facet candidate with fewer than independent tight points into two distinct valid inequalities averaging back to it, contradicting facetness) — this is where the real content lives, and a formalization that only captures the forward direction would understate the theorem substantially.
For Theorem 13.5, the difficulty is that and are themselves defined in
terms of , so "the largest satisfying [a condition stated in terms of
and ]" is a genuinely self-referential extremal characterization, not a
closed-form formula one could simply plug into — hence its faithful statement (via IsGreatest
over an explicit, self-referential candidate set) rather than an unwound algebraic expression.
The ambient space is Fin n → ℝ throughout, matching the series default. Dominant/Blocker
are given their own names (not reusing, even informally, 02b-polarity's polar/reverse-polar
vocabulary), per BRIEF.md's explicit warning that the nonnegativity restriction makes these
different objects. PolyDim/IsFacet are restated from 02b-polarity/11a-intersection-cuts
(affine dimension via Module.finrank of vectorSpan, faces via IsExtreme), since Chapter 2
already pins these down precisely for this series and Chapter 13's own facet claims use the same
notion. IsUpperMonotone is stated exactly as Definition 4 (P = P⁺ ∩ [0,1]ⁿ), not paraphrased
as coordinatewise monotonicity, per BRIEF.md's explicit warning that these are different
conditions.
IsInIS (membership in ) uses LinearIndependent ℝ directly for the "|S| linearly
independent points" hypothesis, matching the book's own wording; since every such point satisfies
, a linear dependence among them is automatically an affine dependence (the coefficients
of any nontrivial linear relation among them must sum to zero), so this is not a weakening of the
more familiar "affinely independent" reading a reader might otherwise expect. A trivializing
formalization to rule out explicitly: describing Theorem 13.7's using only the validity half
of the claim (dropping "each of these inequalities is facet-defining for ") — this mission
states both conjuncts, since the facet-exactness is the theorem's genuine content beyond a
Farkas-style validity certificate.
This mission depends on no other chunk's Lean definitions; it restates the affine-dimension/facet
vocabulary of 02b-polarity/11a-intersection-cuts only informally, per the series convention.
Corollary 13.6 (an -time algorithmic claim for computing ) is out-of-cone per
BRIEF.md: it is fully quantified, not a veto-V3 case, but is a computational-complexity
statement outside this mission's polyhedral-characterization scope.
Many graph algorithms for connectivity questions run in time proportional to the number of edges. When the question is only whether a graph is -edge-connected, or what its local edge-connectivities are up to a threshold , most edges are irrelevant: a spanning subgraph with edges already carries the answer. Such a subgraph is called a sparse certificate. Computing one first and running the expensive algorithm on it replaces by in the running time of connectivity testing, of Matula-type edge-connectivity algorithms, and of – 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:
A graph is finite and undirected, has 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 , is the spanning subgraph with edge set . It is a forest if it has no cycle; two parallel edges form a cycle. It is a maximal spanning forest in , for , if adding any edge of to creates a cycle.
The local edge-connectivity is the minimum number of edges of whose removal leaves no path from to ; parallel edges count separately. It is when .
Procedure FOREST keeps a label on every node, initially , and classes , initially empty. While an unscanned node exists, it picks an unscanned node of largest label; for every unscanned edge from to a node , it puts into , increases by one if , increases by one, and marks scanned; then it marks scanned. Ties among nodes and the order of edges are free. On termination, .
For every graph and every completed execution of FOREST on :
(2.1) says that one search produces, for every threshold at once, a subgraph with at most edges that keeps every local edge-connectivity up to . Any algorithm whose running time grows with can then be run on in place of ; §4 of the paper uses this to speed up -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 when .
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.
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 records only which classes touch , not which component of each class contains . The paper's argument needs Lemma 2.4(a): at the moment an edge is added to its ends already lie in one tree of . 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.
V with , 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.ℕ∞ over separating edge sets, at . (2.1) is kept "for all ", as printed.The Gomory mixed-integer (GMI) cut is the single most widely deployed cutting plane in practical mixed-integer programming: every commercial solver generates it, from a simplex tableau row, essentially for free. Yet the GMI cut is not the strongest cut derivable from the same row: once a subset of the variables is known to be integer-constrained, that integrality can be used to tighten the cut's coefficients further, a technique due to Balas and Jeroslow that predates and motivates most of the general disjunctive-cut machinery of this book (E. Balas and R. G. Jeroslow, Strengthening cuts for mixed integer programs, European Journal of Operational Research 4 (1980), 224–234, https://doi.org/10.1016/0377-2217(80)90106-X). This mission formalizes the culmination of that line of work: two refinements of the GMI cut, each strictly stronger than the plain GMI coefficient on part of the variable set, obtained by applying monoidal cut strengthening — optimizing a cut's coefficients over an algebraic monoid of admissible integer shifts — to the two-term split disjunction that produces the GMI cut in the first place (E. Balas and R. Jeroslow, as above; the monoidal strengthening framework itself due to R. E. Gomory and E. L. Johnson, and formalized in the generality used here by G. Nemhauser and L. Wolsey and by J. -P. P. Richard, Y. Li and A. Miller).
Fix a row of a simplex tableau: , with for , integer for in a subset , and . If is itself integer-constrained, every feasible solution satisfies the split disjunction , from which the ordinary GMI cut follows, with uniformly over all of .
For a general -term disjunction with a known background lower bound on each term's left side, the cut monoid is
Given the disjunction and the lower bounds, replacing each term's coefficient (for in the integer-constrained set ) with for any fixed leaves the disjunction — and hence the disjunctive cut it implies — valid; optimizing this replacement over the whole monoid strengthens the resulting cut. For the normalized -term disjunction (each right-hand side scaled to a common reference), the unstrengthened cut coefficient is .
Theorem 11.19. For the general -term disjunctive-cut situation, every satisfying the background lower bound and the disjunction also satisfies the monoidally-strengthened cut , with
Proposition 11.22. For the normalized disjunction, and any fixed monoid elements (), every integer on satisfying the disjunction and the background lower bound also satisfies the strengthened disjunction with each term's coefficients shifted by — the fact that licenses optimizing over the whole monoid afterward.
Corollary 11.25. For each disjunct index , the cut is valid, with on and elsewhere — a version of monoidal strengthening needing no optimization over at all.
Theorem 11.26 (goal). Specializing the same monoidal strengthening machinery to the two-term split disjunction itself: both and are valid cuts, with given by a three-case piecewise formula (eq. (11.55)) refining the GMI coefficient on part of , and symmetric (eq. (11.56)).
The targets move from the general monoidal-strengthening theorem (11.19) through its validity engine in normalized form (Proposition 11.22, directly cited by the intermediate Theorem 11.23 that the goal specializes) and its optimization-free cousin (Corollary 11.25, immediately preceding the goal in the same subsection) to the concrete payoff for the single most-used cut in practice.
Theorem 11.26's cuts are not a theoretical curiosity: Corollary 11.27 (not drafted this pass) gives an explicit, checkable condition under which each cut is strictly stronger than the plain GMI cut, and Example 4 (p. 187–188) gives a fully worked six-variable instance where the improvement is concrete and numerically verifiable. Since the GMI cut is generated by essentially every mixed-integer solver at essentially every node of a branch-and-cut search, a cheap, always-valid strengthening of it — derivable from the same tableau row with no extra data beyond knowing which variables are integer-constrained — has direct practical reach far beyond this one book.
Both directions are proved in the source (Balas and Jeroslow 1980 for the underlying strengthening idea; this book's own Theorem 11.19/Proposition 11.22/Theorem 11.23 chain for the general monoidal framework applied here) but have no counterpart on this platform: nothing existing treats monoidal cut strengthening, the cut monoid itself, or a refinement of the GMI cut. This mission produces the first Lean statements of all four targets.
The obvious shortcut for Theorem 11.26 is to collapse 's three-case definition into the plain GMI formula applied uniformly — after all, that formula already gives a valid cut, and the strengthened cases can only make individual coefficients smaller (better). But a uniform formula reproduces exactly the plain GMI cut and can never be strictly stronger than it, which is the entire content the goal theorem (via Corollary 11.27) is building toward; the piecewise case split over (where ), (where ), and the rest is not incidental bookkeeping but the mechanism by which integrality actually buys something.
For Proposition 11.22 and Theorem 11.19, the difficulty is that the strengthening must remain valid simultaneously for every choice of the monoid element (or ) — not merely for some cleverly chosen one — since Theorem 11.19's conclusion then takes an infimum over the entire monoid , which is generally infinite. Fixing a single "obviously good" and stopping there would prove a weaker, non-optimized statement.
The ambient space is Fin n → ℝ throughout, matching the series default, with the disjunction
index set Q represented as Fin q and the cut monoid CutMonoid q : Set (Fin q → ℤ). Theorem
11.19 is formalized with scalar per-term coefficients (one real number per disjunct
and variable ), rather than the fully general "each term a multi-row system " framing the book's surrounding prose (§11.8's opening) sketches before specializing: every
downstream result this mission needs (Proposition 11.22 onward, via (11.38)) is already stated at
the single-inequality-per-term level, so this is not a weakening relative to what is actually
used, only relative to a more general preamble that is never itself given a numbered, formalizable
statement. AlphaJStrengthened uses sInf over the (possibly infinite) monoid literally, not a
fixed near-optimal representative. AlphaPlus/AlphaMinus use the exact three-case structure of
(11.55)/(11.56) — collapsing them into the uniform GMI formula is the trivializing formalization
this mission rules out, since a uniform formula could never realize the theorem's actual
(strictly stronger, on part of the domain) claim.
This mission depends on no other chunk's Lean definitions; it restates 11a-intersection-cuts's
disjunctive-cut vocabulary only informally (the underlying disjunctive-cut idea, not any specific
Lean declaration), per the series convention. A complete development needs: properties of sInf
over an unbounded-below-safe subset of ℤ-indexed reals, and case analysis on Int.floor/
Int.ceil for the piecewise formulas. The cut-monoid and unstrengthened/strengthened-coefficient
definitions are reusable by any later mission touching monoidal strengthening (e.g. a future
mission on Theorem 11.23's full Lopsided-cut construction or the multiple-term-disjunction
material of §11.9.2–11.9.3, not drafted this pass).
Chapter 6 built lift-and-project (L&P) cuts from a cut-generating LP, and Chapter 7 surveyed alternative nonlinear constructions reaching the same integer hull. This chapter asks a sharper question: how do L&P cuts relate, coefficient for coefficient, to older, more classical cutting planes — simple disjunctive cuts and mixed integer Gomory cuts, derived directly from a simplex tableau rather than from an auxiliary LP? The answer is an exact correspondence: every L&P cut from a basic solution of the cut-generating LP is equivalent to a specific simple disjunctive cut from a specific tableau basis, and conversely. This correspondence is not merely of theoretical interest — it converts a question about an infinite family of cuts into a finite, countable one (bases of a linear system), and it is what lets the chapter's capstone result, Theorem 8.7, establish a uniform rank bound of (the number of 0-1 variables) across four cut families at once, by proving it for one and transporting the proof to the other three.
(eq. (8.1)) is the cut-generating LP for the disjunction , with an added normalization constraint that makes its feasible polytope bounded — so a "basic solution" can be identified with an extreme point of that polytope. Given a basic solution with and basic -components indexed by (Lemma 8.1-8.2), the submatrix of indexed by is nonsingular, giving a simplex tableau in which is expressed as (eq. (8.5)). The simple disjunctive cut from applied to this row has coefficients , (eq. (8.7)-(8.8)).
The rank of the LP relaxation with respect to (a) unstrengthened L&P cuts, (b) simple disjunctive cuts, (c) strengthened L&P cuts, (d) mixed integer Gomory cuts (equivalently, strengthened simple disjunctive cuts) is at most , the number of 0-1 variables.
Lemma 8.1 (basicness forces ), Lemma 8.2 (a basic solution's index sets give a nonsingular submatrix), Lemma 8.3 (), Theorem 8.4A (a basic L&P cut equals a simple disjunctive cut), Theorem 8.4B (the converse: every simple disjunctive cut from a valid basis equals some basic L&P cut), and Theorem 8.5 (the same correspondence, strengthened).
The results themselves. Theorems 8.4A/8.4B are, in the book's own words, an "exact correspondence between lift-and-project cuts for a mixed 0-1 program and earlier cuts from the literature" — placing L&P cuts, simple disjunctive cuts, and (via Theorem 8.5) mixed integer Gomory cuts on the same logical footing, all generated by choosing a basis of one underlying linear system. Theorem 8.7 is the payoff: a single uniform bound covering four cut families that the literature had previously bounded (if at all) by separate arguments, and by contrast to the unbounded rank of pure-integer fractional Gomory cuts, exhibiting a case where the mixed 0-1 structure yields much stronger guarantees.
Formalizing it. No object in this mission exists on the platform prior to it or in Mathlib.
This mission restates 06-lift-project-cuts's apparatus and Theorem 6.4's strengthened
cut formula locally, per the series convention that a draft mission cannot import another draft
mission's definitions, adapted throughout to this chapter's normalized and its
disjunction on a single fixed coordinate .
Formalizing "basic solution" required a genuine choice: unlike Chapter 6, 's
normalization constraint makes its feasible set a bounded polytope, so this mission identifies
"basic solution" with an extreme point of that polytope (Set.extremePoints) for Lemma 8.1 (whose
own statement has no reference to specific index sets), while Lemmas 8.2 onward take the basic
index sets directly as hypothesis data, matching how those theorems are themselves
phrased ("let the basic components... be indexed by and "). Theorem 8.7's rank bound
required designing one generic HasRankAtMost predicate, parametrized by an abstract cut-closure
operator, applicable uniformly to all four families — mirroring the book's own proof structure,
which establishes the bound for one family and transports it to the other three via Theorems
8.4A/8.4B and 8.5, rather than arguing each part from scratch.
The row/variable identification gap (see MODERATION_NOTES.md). The book's own eq. (8.4)-
(8.5) identifies certain rows of the augmented, -row matrix (those that are
bound constraints ) with the variables they bound, so that a chosen nonbasic row set
doubles as a set of "nonbasic variables." This mission's abstract row type does not track that
identification (matching the abstraction already used throughout 06-lift-project-cuts and
07-higher-dim): Surplus instead defines the tableau row's nonbasic quantities directly as the
slack expression , a genuine affine function of for every
row, which reduces to itself exactly when row is that bound constraint — mathematically
equivalent to the book's own substitution, stated without needing the row-to-variable lookup.
Eq. (8.10)'s "" strengthening-eligibility test has the same gap; this mission takes
the row-positions eligible for strengthening as an explicit Finset parameter rather than deriving
membership from row identity.
Corollary 8.6 is out of scope for this mission — see HARD.md. Its facet-counting bound
depends on the same row/variable identification (the printed bound is ,
excluding row specifically because it is 's own bound row) and would additionally require
a general notion of "number of facets of a polyhedron" that this mission's abstraction, and
Mathlib, do not provide; it does not feed Theorem 8.7's own proof, which cites only Theorems
8.4A/8.4B and 8.5.
Theorem 8.7 is stated via one generic HasRankAtMost predicate applied to SplitConvexify (part
a) and three closure operators (SimpleDisjClosureOfSet, StrengthenedLPClosureOfSet,
MIGClosureOfSet, parts b-d) defined by intersecting a represented polyhedron with every cut of
the corresponding family, then lifted to bare sets by quantifying over every linear representation
— since, unlike the split-convexification closure, these three cut families are defined via an
explicit basis or CGLP solution and so genuinely need some concrete representation of the
current polyhedron at each step of the recursion (the same representation-dependence Theorem
7.5's Lovász-Schrijver iteration required in 07-higher-dim).
A mixed 0-1 program's feasible region is a disjunctive set built from the split disjunctions , one per binary variable — a special case general enough that Chapter 2's convex-hull machinery applies directly, yet structured enough to produce closed-form cutting planes efficiently. The resulting lift-and-project (L&P) cuts, generated by solving a small auxiliary linear program (the cut-generating LP, CGLP) rather than by hand-derived combinatorial argument, were part of a cluster of ideas that drove a dramatic improvement in commercial mixed-integer solvers' practical performance from the mid-1990s onward. This chapter develops the theory that makes L&P cuts computationally practical: how to bound how many rounds of cutting are needed (disjunctive rank), what can and cannot be guaranteed about intermediate fractional solutions during sequential convexification, how to generate a cut cheaply by solving the CGLP only over the LP relaxation's active variables and lift the result back to the full variable space in closed form, and how to strengthen a single-disjunction cut into one valid for the whole integer program using the integrality of the other 0-1 variables.
For the mixed 0-1 program , let
be its LP relaxation (written after folding in the bound
constraints) and its disjunctive
feasible set. Sequential convexification produces , then , and so on. The
cut-generating LP (CGLP) for the disjunction on coordinate asks for and
multipliers , scalars , satisfying , $\alpha
(CGLP)^R, whose solution can
be lifted back to a solution of the full (CGLP) in closed form.with valid for the whole mixed 0-1 program, strengthening a cut valid only for the single disjunction on .
Theorem 6.1 (an extreme point of cut off at a facet of cannot be fractional in without being fractional in too), Theorem 6.2 (an explicit closed-form extension of a restricted CGLP solution to the full CGLP), and Corollary 6.3 (the same fact, stated transparently via a formula and asserted feasible for the full CGLP).
The results themselves. Theorem 6.4 is what turns lift-and-project cuts from "valid for one binary variable's split" into genuine cuts for the whole mixed-integer program, using no information beyond the integrality of the other 0-1 variables — this strengthening step is part of why L&P cuts became practically competitive with other cutting-plane families. Theorem 6.2 and Corollary 6.3's cut-lifting property is, independently, what makes generating L&P cuts affordable at industrial scale: solving the CGLP only over a problem's few hundred active variables rather than its hundreds of thousands of total variables, then reading off the remaining coefficients in closed form.
Formalizing it. No object in this mission — the cut-generating LP, its restricted version, or the mixed-integer cut-lifting formula — exists on the platform prior to this mission or in Mathlib. This mission restates the disjunctive-set and convex-hull vocabulary of the earlier missions in this series locally (per the series convention that a draft mission cannot import another draft mission's definitions), applied specifically to the split disjunction on a single 0-1 variable.
The natural first attempt at Theorem 6.1 assumes that once has been "locked in" by sequential convexification, every subsequent cut generated while processing later variables respects that integrality — the book's own Figures 6.1-6.2 refute this directly, exhibiting facet- defining cuts that cut through the interior of an edge at a point fractional in every coordinate. Theorem 6.1's genuine content is the narrower but still useful fact that extreme points of the right intersection cannot exhibit this failure. The difficulty in Theorem 6.4 is recognizing that naively substituting for varying integer vectors gives a family of valid cuts, not a single one — the theorem's content is the closed-form choice of (via rounding up or down, whichever yields the smaller coefficient) that is provably optimal within this family, not merely one valid choice among many.
All results are stated over Fin n → ℝ with the CGLP's row space left as an abstract finite
type M (rather than fixing the exact m+p+n-row block structure the book's own augmented
matrix à has), since the substantive content of every theorem in this chapter depends only on
dot products against columns of Ã, never on which literal row a given bound constraint occupies.
Alpha1/Alpha2 (Corollary 6.3's row-restricted dot products) and Alpha1_64/Alpha2_64
(Theorem 6.4's eq.-(6.4) values, which add or subtract / at the disjunction coordinate)
are kept as separate definitions throughout, per BRIEF.md's explicit warning that the two
chapters' "" notation refers to different formulas despite the shared symbol.
Theorem 6.2's closed-form extension is formalized via the values it assigns (matching every
printed formula for ū_{m+i}, v̄_{m+i}, ᾱ_i), without committing to the book's own literal
row-block indexing (m+i vs. m+n+i) for the fresh rows a full reading of the source does not
fully disambiguate for variables outside the 0-1 index set — Corollary 6.3, the chapter's own
"more transparent" restatement of the same fact, is instead formalized with an explicit fresh-row
construction (AtilExt, BtilExt) verifying genuine feasibility for the extended (CGLP). In
Theorem 6.4, is stated as an explicit hypothesis, matching BRIEF.md's flag that
this positivity (needed for 's division) is implicit in the CGLP feasibility setup
rather than a free-standing assumption of the printed theorem.
A trivializing formalization is ruled out explicitly: Theorem 6.4's conclusion is stated as
genuine validity for the full MIPDisjunctiveSet (imposing simultaneously on every ), not merely as the closed-form formula for with no accompanying validity claim,
which would omit the theorem's actual mathematical content.
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.
Let be -dimensional Euclidean space with distance . A system of linear inequalities
is given by vectors and numbers . Each inequality defines a closed half-space , and the solution set is the polytope , assumed nonempty. Its affine hull is an -dimensional flat ; this mission assumes , that is, .
A relaxation step with parameter from a point chooses a half-space at maximal distance from , the point nearest to , and moves to
For the new point is the mirror image of in the boundary hyperplane of . A run is a sequence in which every point outside is followed by a relaxation step. The run terminates if some ; otherwise it is an infinite sequence.
A sequence outside is Fejér-monotone with respect to if and for all and all .
For a flat and a point , the locus
is a sphere of dimension centred at the orthogonal projection of onto and lying in the flat through that centre normal to . The paper calls it a spherical surface having as its axis. For it consists of two points symmetric with respect to the hyperplane .
Assume is nonempty and .
Case 1 (). Every run either terminates or converges to a point of :
Case 2 (). Every run either terminates or ends on one sphere with axis :
Case 1 is Agmon's theorem; Case 2 is the paper's own contribution.
An additional item, Corollary 1, states that for and an infinite reflexion run, the hyperplanes used for all contain and hence .
The result. Theorem 2 completes the description of the reflexion method. Combined with Theorem 1 (termination when ), 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 that reveals the flat: by Corollary 1 the hyperplanes used from some point on contain . 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.
Fejér monotonicity alone gives boundedness and convergence of every distance , , but not convergence of the sequence. When lies in a proper flat, those distances fix a point only up to a sphere about , 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 the obstacle is to exclude an oscillation on that sphere. For 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.
EuclideanSpace ℝ (Fin n); the system is a : Fin m → EuclideanSpace ℝ (Fin n), b : Fin m → ℝ, with inner ℝ (a i) x. Half-spaces are closed (). Distances to half-spaces are Metric.infDist.(polytope a b).Nonempty), as the paper assumes from the outset. is affineSpan ℝ (polytope a b), so "" holds by construction, and "" is affineSpan ℝ (polytope a b) ≠ ⊤. No separate natural number is introduced.lam.p : ℕ → E with a relaxation step after every point outside . Termination is ∃ N, p N ∈ A; an infinite sequence is ∀ ν, p ν ∉ A.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.MapClusterPt x atTop q), not points of the closure of its range. Boundary is the topological frontier.IsRelaxStepVia), which the relation hides. Its last sentence, on reducing the dimension, is commentary and is not formalized.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 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 , 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 perturbation of size less than .
Points live in with the Euclidean inner product and norm . Labels are . A binary classifier is any map , and for the linear classifier is .
The -Bernoulli model. Fix a sign vector and a bias . A sample is drawn by choosing uniformly in and then, independently for each coordinate , setting with probability and with probability . So , and each coordinate carries a weak signal of strength about the label.
Errors. The classification error of is . For the ball is , and the -robust classification error of is
The adversary may move anywhere in the ball, including off the hypercube.
Thresholding. The thresholding map is if and otherwise. The classifier studied is , with computed from one training sample .
There is a universal constant such that, whenever and is one sample of the model with ,
The constant is left existential; only the scaling is fixed. The failure probability is the one the paper proves for the same classifier.
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 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.
The concentration steps are standard, but the natural first approach to the goal fails: a bound on the classification error of the linear classifier says nothing about its robust error, and for of order the robust error of every linear classifier is close to . The goal concerns the nonlinear classifier , whose robustness rests on the data lying exactly on the hypercube and on the adversary's budget being below ; neither fact is visible to an argument about linear classifiers. A second difficulty is bookkeeping: the paper uses three forms of the estimator (, , ), a training sample and a test sample with the same name, and a failure event that must hold for all at once.
is EuclideanSpace ℝ (Fin d). Labels and hypercube coordinates are Bool ( true). Because the model is finite, every probability is a finite sum of the weights ; no measure theory is involved. Conventions committed to:
A formalization that bounds only the standard error of , drops , uses the Euclidean ball, or lets the estimator see 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.
Chapter 2 gives a compact lifted description of the closed convex hull of a disjunctive set once it is written as a union of polyhedra (its disjunctive normal form, DNF). But most discrete optimization problems present their feasible region the opposite way: as a conjunction of many small disjunctions (the conjunctive normal form, CNF) — "linear constraints, and , and , and so on" — each easy to reason about on its own but expensive to convert to DNF directly, since converting a CNF with conjuncts of terms each can blow the DNF up to as many as polyhedra. Chapter 4 develops the machinery for moving between these two extremes without paying that combinatorial cost all at once: the basic step, which merges two conjuncts into one, and the hull-relaxation, an intermediate polyhedral relaxation that tightens monotonically with every basic step performed, converging exactly to the true convex hull once the disjunctive set reaches DNF.
A disjunctive set is in regular form (RF) if with each a union of polyhedra. is elementary if every is a halfspace (the RF is then the CNF), and improper if literally equals a single polyhedron . Writing for the improper indices, is 's polyhedral part. The hull-relaxation of a regular form is
a relaxation of distinct from itself: it convexifies each conjunct before intersecting, which is generally weaker. A basic step replaces two conjuncts () of a regular form by their intersection (itself brought to DNF via distributivity), reducing the number of conjuncts by one; repeating this times brings any regular form to DNF. For a convex set , its extreme direction vectors are the extreme rays of its recession cone.
For a sequence of regular forms of the same disjunctive set, with in CNF, in DNF, and each obtained from by a basic step:
Theorem 4.1 (, the basic-step identity), Theorem 4.4 (the hull of a union of halfspaces is or the halfspace itself), Lemma 4.5 ( for a CNF ), and Lemma 4.6 (, driving each inclusion of the chain).
Theorem 4.8 (an exact extreme-point/extreme-direction criterion for when Lemma 4.6 is equality), Corollary 4.9 (a worked case where merging "0-1" disjunctions brings no gain), and Theorem 4.10 (any regular form is the projection of a mixed 0-1 program using no more binary variables than the original CNF).
The results themselves. Theorem 4.7 turns the exponential CNF-to-DNF blowup into a controllable, monotone process: rather than converting all at once, a solver can perform basic steps selectively — wherever Theorem 4.8's criterion promises a genuine tightening — and always have a valid, improving polyhedral relaxation available at every intermediate stage. Theorem 4.10 is what makes this practical for integer programming specifically: it shows the number of 0-1 variables needed never has to grow, no matter how many basic steps are performed, only the number of continuous lifted variables does.
Formalizing it. No object in this mission — regular form, the hull-relaxation operator, basic steps, or extreme direction vectors — exists on the platform prior to this mission or in Mathlib. This mission restates the disjunctive-set and convex-hull vocabulary of the earlier missions in this series locally (per the series convention that a draft mission cannot import another draft mission's definitions).
The obvious first attempt collapses h-rel to cl conv throughout, reasoning that since the
chain ends at , the intermediate terms should behave the same way.
This is exactly backwards: h-rel is always at least as large as the true convex hull at every
intermediate stage (Lemma 4.6 gives containment, not equality, in general), and the chapter's own
Example 1 exhibits a CNF whose hull-relaxation strictly exceeds
until enough basic steps have been performed. The real difficulty Theorem 4.8 isolates is
recognizing which basic steps actually tighten the relaxation: merging conjuncts whose extreme
points and directions already coincide with those of the pairwise intersections gains nothing
(Corollary 4.9's worked case), while merging conjuncts that interact more intricately can produce
a strictly tighter bound — and no general rule beyond Theorem 4.8's own extreme-point criterion
identifies which case holds.
All results are stated over Fin n → ℝ with matrices Matrix (Fin m) (Fin n) ℝ. A regular
form's conjuncts are represented as an arbitrary function T → Set (Fin n → ℝ) (rather than
requiring every conjunct's internal polyhedral structure to be uniformly tracked through the whole
chapter), with IsDisjunctiveUnion/IsElementaryDisjunction as existential well-formedness
predicates asserting each conjunct genuinely is a union of polyhedra/halfspaces where that matters.
IsBasicStepOf states a basic step abstractly via an index-type equivalence, since its
mathematical content is which two conjuncts merge and into what, not any particular relabeling
scheme; Theorem 4.7's own sequence of regular forms is a dependent family T : Fin (t+1) → Type*
precisely because each basic step genuinely changes the index type (one fewer conjunct).
Theorem 4.7's three-part conclusion (initial equality, step-by-step containments, final equality) is stated as a conjunction rather than a single chained relation, since Lean has no native mixed equality/containment chain notation; this preserves the chapter's own warning that only the last hull-relaxation in the chain is asserted equal to the true convex hull. Theorem 4.10's index set (which term of each original disjunction a given conjunct's disjunct picked) is taken as given structural data satisfying the book's own defining relationship, matching the source's own treatment of as a named auxiliary index set rather than a from-scratch construction. Chapter 4's §4.5–4.6 (a machine-sequencing application with its own bespoke scheduling objects, Theorems 4.11–4.12) is out of scope for this mission — it introduces application-specific vocabulary not shared by the chapter's general hull-relaxation theory, not because it is difficult.
A trivializing formalization is ruled out explicitly: every theorem is stated for generic finite index types, never fixed at a small size that would collapse a union or intersection to a single term, and the chapter's own propositional-logic DNF/CNF conversion (informal narrative via truth tables in §1.3) is not itself a formalization target — this mission works entirely at the polyhedral-set level the chapter's own numbered results occupy.
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:
This mission is the first of three built on the Motzkin–Schoenberg paper: it covers the full-dimensional case, Theorem 1.
Let be -dimensional Euclidean space. A system of linear inequalities
is given by rows and constants . The -th inequality defines the closed half-space , and the set of solutions is the polytope . The system is assumed consistent, so is nonempty. The dimension of is the dimension of its affine hull; means that is not contained in any hyperplane.
Fix a relaxation parameter with . From a point one relaxation step is:
For , is the mirror image of in the boundary hyperplane of . Iterating from a starting point gives a sequence ; the process terminates when some , and otherwise produces an infinite sequence of points outside .
A sequence of points outside is Fejér-monotone with respect to if and for all and all .
Assume and . For every starting point and every choice of farthest half-space at every step:
The goal is the paper's theorem as stated, both cases in one statement. It fixes no constants and no rates.
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 : for each there are planar examples where the iteration never stops. The companion missions of this series treat (Theorem 2, where reflexion may settle on a sphere around the affine hull of ) 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.
The first idea is that monotone distances to every point of force convergence. They do not in general: Fejér-monotonicity only bounds the sequence and makes each distance converge, and when lies in a hyperplane a Fejér-monotone sequence can keep oscillating between two mirror-image points. Convergence genuinely needs the full dimension of , 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 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.
EuclideanSpace ℝ (Fin n); the rows are vectors a i, and is inner ℝ (a i) x. Half-spaces are closed. Distances to sets are Metric.infDist.IsRelaxStep a b lam p p', and any maximizing index 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.p : ℕ → E in which each point outside 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.lam, because λ is a Lean keyword.affineSpan ℝ A = ⊤, following the paper's own gloss " is not contained in any hyperplane". "Boundary" is frontier A, and convergence is Tendsto p atTop (𝓝 l).affineSpan ℝ A = ⊤, which includes the paper's polytope.Useful infrastructure: the closed form for and the nearest point in a half-space; the characterization of via a nonempty interior for convex sets. The Fejér-monotone convergence lemma and the half-space projection lemmas are reusable beyond this mission.
Computing the convex hull of a disjunctive set — a union of finitely many polyhedra — is generally hard in direct proportion to how many polyhedra are in the union: Chapter 2's Theorem 2.1 gives a compact lifted description, but working with it still means reasoning about all the disjunctions of the program simultaneously. A natural question, with obvious practical consequences for integer and combinatorial optimization, is whether the convex hull can instead be built up incrementally: impose one disjunction, take the convex hull of what results, then impose the next disjunction on that, and so on. If this "sequential convexification" procedure always reached the true convex hull, computing facets of a hard disjunctive set would reduce to a sequence of much easier single-disjunction computations. Balas shows the answer is negative in general — a two-variable integer program is a standard counterexample — but identifies an important class of disjunctive programs, the facial ones, for which sequential convexification always works. This class includes 0-1 programming (pure or mixed), nonconvex quadratic programming, separable programming, and the linear complementarity problem, though not general integer programming.
Let . A disjunctive program in conjunctive normal form has constraint set
for a finite set and, for each , a finite set of halfspace data — one elementary disjunction per . The program is facial if every inequality appearing in some disjunction defines a face of , i.e. is an extreme subset of for every such . Fixing an ordering of , the sequential-convexification recursion sets (step zero) to be the base polyhedron and, for each subsequent step, imposes the next disjunction and reconvexifies: .
For the necessity direction, write and, reversing every inequality, .
This is the weakest correct statement of the recursion's endpoint: it asserts the sequential procedure reaches exactly (not, say, some fixed superset), and — since is universally quantified — that this holds regardless of the order in which disjunctions are imposed.
for a union of finitely many polyhedra and opposite halfspaces .
The results themselves. Theorem 3.1 is what makes sequential convexification a practical tool rather than a theoretical curiosity: for a 0-1 program with binary variables, it lets the convex hull be built in stages, each requiring only the facets of a two-term disjunction — tractable, in contrast to generating facets of the full integer hull directly. Theorem 3.3 puts the boundary of applicability on rigorous footing: faciality is sufficient but not necessary, and Theorem 3.3 pins down the exact condition, showing precisely why sequential convexification is a genuinely restrictive property (holding for 0-1 programs but not general integer programs) rather than a universal fact about unions of polyhedra.
Formalizing it. No object in this mission — faciality, the sequential-convexification recursion, or the relative-boundary constraint condition — exists on the platform prior to this mission or in Mathlib. This mission restates the disjunctive-set vocabulary of the earlier missions in this series locally (per the series convention that a draft mission cannot import another draft mission's definitions) and is otherwise self-contained.
The natural first guess is that sequential convexification should always work, since at each step the procedure only discards points excluded by a valid disjunction. The book's own two-variable integer-programming example (imposing integrality on , then on ) refutes this directly: the resulting set strictly contains the true integer hull. The reason faciality repairs this is subtle and is exactly what Lemma 3.2 isolates: the recursion's correctness at each step needs the previous partial hull, intersected with the new disjunction's halfspace, to already equal the convex hull of the intersection taken before convexifying — and this commutation of convex hull and halfspace intersection is exactly what fails when the halfspace does not respect a face of the underlying polyhedron. Theorem 3.3 shows this is not merely Lemma 3.2's specific route to a sufficient condition, but the precise dividing line: the "if" direction says checking the boundary condition only for segments between two points already suffices, which is what makes facial sufficiency provable by induction in the first place.
All results are stated over Fin n → ℝ with matrices Matrix (Fin m) (Fin n) ℝ. The disjunction
structure uses a finite index type S with a dependent family of finite index types Qidx : S → Type*, matching the book's S, Q_j. Faciality (Facial) uses Mathlib's IsExtreme directly,
matching the book's own primary definition of "defines a face" rather than its immediate
"clearly equivalent" restatement (F₀ ⊆ {d_i x ≤ d_{i0}}). The relative boundary in Theorem 3.3
("the boundary of in the affine space spanned by ") is Mathlib's
intrinsicFrontier, the standard formalization of a set's boundary relative to its own affine
hull. The book's own "" in the constraint boundary condition's conclusion (rather than
"", which set-membership syntax would require for a set on the left) is read as set
inclusion, the only mathematically sound reading, and is transcribed as ⊆ in the Lean statement
while the milestone's verbatim text preserves the book's own "" unchanged, per the
verbatim-quotation convention.
A trivializing formalization is ruled out explicitly: Theorem 3.1 is stated for an arbitrary
finite S and Qidx, not fixed at a small size (e.g. |S| = 1, which would make the recursion's
endpoint trivially equal to a single step and prove nothing about sequencing), and the recursion's
ordering σ is universally quantified rather than fixed to a canonical choice, matching the
theorem's own order-independence claim.
Theorem 2.1 (the previous mission in this series) shows that the closed convex hull of a union of polyhedra has a compact description after lifting to a higher-dimensional space. That description comes in two dual flavors: a primal one, as the projection of an explicit lifted polyhedron, and a polar one, characterizing the hull's facets directly via a cone built from the disjuncts' own data. Both flavors matter in practice: a cutting-plane algorithm needs to know exactly which inequalities are facet-defining (so as not to waste effort generating redundant cuts), and the two routes — projection and polarity — offer complementary tools for deciding this. This mission formalizes both routes and the machinery connecting them, closing out Chapter 2 of Balas, Disjunctive Programming (Springer, 2018).
The projection route (§2.2–2.3) develops general facts about projecting an arbitrary polyhedron that predate and underlie the disjunctive-programming application: the classical projection formula via extreme rays of a projection cone, how dimension and facet structure behave under projection, and a refinement (via a coordinate transformation) that eliminates the redundant inequalities the plain projection formula can produce. The polarity route (§2.4) develops the reverse polar, an object introduced by Balas specifically for this purpose, whose iterated application recovers the closed convex hull of a disjunctive set directly, culminating in an exact characterization of when an inequality is facet-defining purely in terms of extreme rays of an explicit cone .
For a matrix system with rows, let , and let be its projection onto the -space. The projection cone is . A vector is an extreme ray of a cone if , , and the ray it generates is an extreme subset of . The dimension of a polyhedron is the dimension of its affine hull, and a set is a facet of if it is a proper face of of dimension . Partitioning 's rows into those tight throughout (the equality subsystem) and the rest, and denote the rank of the tight rows' combined and -only submatrices, respectively.
For , the polar is and the reverse polar is ; more generally the scaled polar at level is . For a disjunctive set with and , the cone .
For a full-dimensional disjunctive set () and :
Proposition 2.13 ( bounded), Theorem 2.14 ( when ), Corollary 2.15 (), Theorem 2.16 (the scaled polar stabilizes: ), and Corollary 2.17 () — each the weakest statement needed for the next.
Theorem 2.5 (), Proposition 2.6 (projection preserves integrality), Theorem 2.7 (), Corollaries 2.8–2.10 (facet/face behavior under projection), and Proposition 2.11 / Corollary 2.12 (sharper facet characterizations via a coordinate-transformed projection cone).
The results themselves. Theorem 2.18 is the practical payoff of the entire polarity apparatus: it turns "is this inequality facet-defining for the convex hull of a union of polyhedra" from a geometric question into an algebraic one about extreme rays of an explicit, finitely-generated cone built directly from the disjuncts' own constraint data — exactly the kind of question a cutting-plane algorithm needs answered to avoid generating redundant cuts. The projection track is foundational general polyhedral theory in its own right (Theorem 2.5's formula underlies Benders decomposition and classical Fourier-Motzkin elimination as special cases, per the book's own remarks), independently useful beyond the disjunctive setting.
Formalizing it. No object in this mission — polars, reverse polars, projection cones, extreme
rays of a cone, or the dimension/facet apparatus of a polyhedron — exists on the platform prior to
this mission or in Mathlib (a q=polar search returns only an unrelated cyclic-polytope
construction from the Hirsch-conjecture series, with different conventions and object). This
mission restates the disjunctive-set vocabulary of the companion ConvexHull mission locally
(per the series convention that a draft mission cannot import another draft mission's
definitions) and builds the polarity apparatus from scratch on top of it.
The natural first attempt at Theorem 2.18 tries to characterize facets of directly from the lifted-polyhedron representation of Theorem 2.1, projecting facet by facet. This misses the point of the polarity route entirely: Theorem 2.18's proof instead goes through , showing a vertex of corresponds to a nonhomogeneous subset of rank of 's own defining system being tight — algebra entirely in the dual space of multipliers, never touching the lifted polyhedron's facets directly. The two obstacles Theorem 2.14 and Proposition 2.13 exist to clear are, respectively: reverse polars do not satisfy the ordinary polar's clean involution property (an extra summand appears, capturing recession directions the reverse-polar construction alone cannot see), and reverse polars are either empty or automatically unbounded (never merely "small"), which is why the apparatus needs the normalization throughout.
All results are stated over finite index sets and matrices Matrix (Fin (m h)) (Fin n) ℝ
(disjunctive-set data, m : Q → ℕ dependent) or Matrix (Fin m) (Fin p) ℝ /
Matrix (Fin m) (Fin q) ℝ (projection-track data). PolyDim and IsFacet are stated generically
over any real vector space (via Module.finrank of vectorSpan and Mathlib's IsExtreme), so the
same definitions serve both Poly2-shaped pairs and cl conv F ⊆ Fin n → ℝ directly in Theorem
2.18. IsExtremeRay is likewise stated generically, reused for cones in plain vector space,
(v,v0)-space, and the triple (v,w,v0)-space Proposition 2.11 needs.
Two results (Proposition 2.11, Corollary 2.12) build on a coordinate-transformed polyhedron
Q̃/cone W̃ that the book itself only cites from [14] rather than constructing; consistent with
the book's own treatment, this mission takes W̃ (or its (v,v0)-projection) as given data
together with its defining relationship to Proj_x(Q), rather than re-deriving the transformation
— a choice recorded in MODERATION_NOTES.md, not a weakening of either statement's content.
Proposition 2.11's complexity remark ("O(max{m,q}³)") is a proof aside about the transformation's
cost, not part of either result's mathematical claim, and is out of scope per the book-wide
disposition (triage.json).
A trivializing formalization is ruled out explicitly: the projection-track results are stated for
generic m, p, q, never fixed at small values, and Theorem 2.18 is stated for a generic finite
disjunctive index set Q, not specialized to |Q| = 1 (which would collapse W_0 to ordinary
LP polarity and prove nothing about unions).
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 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.
Write . A state is and an input value is . Fix . The delayed BCN (2.2) is
with arbitrary Boolean functions , collected into one map with . A trajectory is the window of the last states; its last entry is the current state. One step maps under the input to . A control sequence of length is , with inputs chosen freely; denotes the trajectory after steps from an initial trajectory .
The transition-count matrix has rows and columns indexed by trajectories: is the number of input values taking trajectory to trajectory in one step. For a set of forbidden trajectories, is with the rows and columns of replaced by zeros, and is with those rows and columns deleted.
The notions of controllability are:
A real square matrix of size is reducible (Definition 3.7) if a simultaneous permutation of rows and columns brings it to block upper-triangular form with square diagonal blocks; it is irreducible otherwise, so every matrix is irreducible.
counts the control sequences of length steering to while avoiding ; counts those steering the initial trajectory to ; is the set of trajectories with current state .
for every , , , every update map and every forbidden set . It is the most general criterion of the paper.
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.
The criteria replace a question about control sequences of unbounded length by a finite test on one nonnegative integer matrix of size . 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 , 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 (zeroed) and (deleted) must not be confused.
The central step is the passage between three objects: reachability under the dynamics, positivity of entries of powers of , and the block-triangular definition of irreducibility. The counting identity for powers of 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 zero matrix is irreducible by Definition 3.7 yet has no positive power, which is exactly why Definition 3.11 allows while Definition 3.1 does not. A proof that routes through "some power of is entrywise positive", following the printed Lemma 3.9, proves a false intermediate statement.
Conventions committed to in Lean:
Fin n → Bool (true is the paper's 1); a trajectory is Fin μ → State n with index 0 the oldest state and index the current state; is a standing assumption (NeZero μ); are arbitrary and no assumption is placed on the update functions.Matrix.IsIrreducible, which differs on matrices.Controllability is defined through the dynamics and control sequences, never as positivity of entries of powers of ; a formalization that defines reachability by 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 (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 with , are welcome.
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 and represent a 0–1 point by the matrix , impose linear (and for semidefinite) constraints on such matrices, and project back to . 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 : iterating it times on any relaxation in variables yields exactly the 0–1 hull (Theorem 1.4 of the paper).
Vectors live in with coordinates ; the space of the original problem is the hyperplane , and polytopes are replaced by the convex cones they generate.
For convex cones , the matrix cone consists of the real matrices such that
adds the condition that is positive semidefinite. The projections are and , where is the 0th unit vector. The cut operator is , and its iterates are , .
Two families of hyperplanes appear in the proofs: and , the hyperplanes through the two opposite facets of in direction .
For every closed convex cone ,
The statement is uniform in and in : no polyhedrality, no bound on the number of constraints, and no assumption that contains a 0–1 point.
Theorem 1.4 is what makes a hierarchy rather than a single cut: the relaxations reach the 0–1 hull after at most rounds, so the -rank of a valid inequality (the least with the inequality valid for ) is a well-defined number between and . 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 constraints) state their results against, and a checked proof of the column characterization (iii″) that all of those proofs use.
The inclusion follows from Lemma 1.1 once each is known to be a convex cone. The reverse inclusion is the content. A first attempt shows that one round of forces one coordinate to be integral, and then iterates; but is not contained in the union of and , only in their Minkowski sum (Lemma 1.3), so a point of 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 to again be a closed convex cone inside so that Lemma 1.3 can be reapplied. Closedness of the projection is not automatic: a linear image of a closed cone need not be closed.
Option ι for a finite type ι; none is and some i is , and is the cardinality of ι, which may be .PointedCone.hull ℝ S; and are defined as spans of 0–1 vectors, as on the page, not by the inequality description .Contributions welcome: proofs that is a closed convex cone contained in whenever is, a proof of , 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.
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?
A generator is with a state set , a finite alphabet of events, a partial transition function , an initial state and marker states . Extending to strings, the generated language is the set of strings for which is defined, and the marked language is the subset of those that end in . The closure of a language is its set of prefixes; is closed if . Throughout, is assumed trim in the sense : every generated string can be completed to a marked one.
The alphabet is split into controllable events and uncontrollable events . A supervisor consists of a deterministic, accessible automaton , whose state set may be infinite, and a map assigning to each state the set of controllable events it enables; uncontrollable events are always enabled. The closed loop runs and 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 , and the controlled language .
is complete if its automaton never refuses an event that the plant can execute and enables; it is proper if it is complete and
that is, every closed-loop string can be completed to a marked task. A language is controllable if and . For , is the class of controllable sublanguages of and the class of sublanguages of with .
Given , the Supervisory Marking Problem (SMP) asks for a proper with , and the Supervisory Control Problem (SCP) for a proper with .
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 .
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 is regular and computable when is finite and 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.
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 containing skips the content of the supremal-element milestone; the goal is stated with the actual union.
α with [Fintype α]; strings are List α, the empty string is [], and is s ++ [σ]. Languages are Set (List α); the closure is pre K = {s | ∃ t, s ++ t ∈ K}.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.Ec → Bool; an event outside is enabled by definition, so uncontrollable events cannot be disabled.sSup in the complete lattice Set (List α).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.
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) 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 .
For fixed there was, before this paper, no polynomial-time algorithm that either decides that a graph has clique-width at least or outputs a decomposition of clique-width bounded by a function of ; the best known algorithm, by Johansson (2001), gave width . Oum and Seymour (J. Combin. Theory Ser. B 96 (2006)) closed this gap with approximation , through rank-width and a factor-3 approximation for the branch-width of symmetric submodular functions.
Timeline:
All graphs are finite and simple. For a finite set , a function is submodular if and symmetric if .
A branch-decomposition of is a pair where is a tree with at least two vertices and all degrees at most , and is a bijection from onto the leaves of . Removing an edge of splits the leaves in two; the width of is of the set of elements of on one side. The width of is the largest edge width, and the branch-width is the least width of a branch-decomposition, with when .
A set is well-linked with respect to if for every partition of and every with , .
Let be the adjacency matrix of over . For disjoint , is the rank of the submatrix of with rows and columns , and the cut-rank function is . The rank-width is .
A -expression is a term built from constants (a vertex with label ), the operators (; add all edges between labels and ), (relabel into ) and disjoint union . Its value is the labelled graph it produces; has clique-width if some -expression has value isomorphic to .
An interpolation of is a function on disjoint pairs that agrees with on , is monotone, submodular in the sense , and has .
For a graph with at least one vertex and an integer :
The same explicit condition decides which side of the approximation holds; this is what the paper's algorithm certifies.
The dichotomy turns clique-width, for which no exact polynomial algorithm is known even for fixed , 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 -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, -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.
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 , gets stuck at a leaf carrying a set with : a split of into two parts of -value below has to be found, and it must be found from the failure of well-linkedness of a set that is not obviously related to . The paper's device is the interpolation , which attaches a matroid to whose base has exactly 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 -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 matrix of rank . Its lower bound needs the tree structure of a -expression to be read as a branch-decomposition.
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 , all neighbour sets of size at most , and an injective map from onto the vertices of degree ; the side of an edge is found by reachability from after deleting . Branch-width, rank-width and clique-width are never computed as minima: "" is the predicate " and , or a branch-decomposition of width at most exists", lower bounds say that every branch-decomposition has a wide edge, and "" is " has a -expression". Labels are Fin k. The value of a -expression has as vertex type the occurrences of constants (a nested sum type), and requires . 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 algorithm; there is no cost model on the page, and the goal states the certificate the algorithm returns instead. Without the running time, " or " 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 , widths defined by an unguarded infimum (which is on an empty family), -expressions whose value is not the graph up to isomorphism or whose may join equal labels, and Theorem 5.1 stated for .
Correction of Theorem 5.1. As printed, Theorem 5.1 fails for : a singleton is always well-linked, but the edgeless graph on two vertices has cut-rank identically and branch-width . The milestone carries the hypothesis ; the goal uses the theorem only at size .
The graph with no vertex is excluded from the goal and from the upper bound of Proposition 6.3, since it has no -expression for any . 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.
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 for the greedy algorithm on minimum-cardinality set cover, a result that still underlies the standard 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).
An input is a finite family of finite sets. Its covered set is . A subcover is a subfamily with , and its measure is
The optimum is the least measure of a subcover; since every subcover has measure at least , an optimal subcover is one with the least possible overlapping. The subproblem EC admits only families in which every set has at most points.
Algorithm C2 keeps a subfamily SUB (initially empty), the unused sets LEFT (initially ) and the uncovered points UNCOV (initially ). While UNCOV is nonempty it chooses LEFT minimizing
the number of already-covered points of per newly covered point, and moves 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 at the moment it is chosen, and the cumulative overlap of a run returning is the sum of these overlaps.
For all and ,
and for all sufficiently large , . In the size-free form used here, for every :
The result. The measure 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 from optimal for this one. Theorem 6 shows that the ratio rule C2 is within of the least-overlap cover, and the lower bound shows that no analysis of C2 can beat . The two bounds differ by less than for every . 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.
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 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 and that the paper drops using must be controlled as well, and the relation must itself be proved from optimality. The lower bound needs an explicit run of C2 through ties on an input with points, checking at every stage that the intended set is a ratio minimizer.
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. is a minimum over the finite, nonempty set of subcovers (Finset.inf'), never a junk value.RunOV.Real.log; is Mathlib's harmonic k.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 SUB), and the explicit lower-bound run.
Many problems in signal processing, statistics and function interpolation ask for a solution of a linear system that uses as few columns of 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 , 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 -minimization under an 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.
Sparse approximate solution (SAS). Given a matrix , a vector and a tolerance , find a vector with whose number of nonzero entries, written , is as small as possible. Here is the Euclidean norm.
Exact Cover by 3-sets (X3C). An instance is a ground set and a list of subsets of , each with exactly three elements. An exact cover is a sub-collection , , such that every element of occurs in exactly one set of .
The transformation. From an X3C instance build the SAS instance with
In Lean, 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 is onesVec m, is Matrix.toEuclideanLin (incidence C) x, and is nnz x.
For every X3C instance as above,
This is the sentence the proof of Theorem 1 (p. 228) establishes: "the constructed instance of SAS has a solution with or fewer entries if and only if the given instance of X3C has a solution."
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 -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).
The forward direction is a direct computation. The converse contains the only real step, which the paper passes over with "it is clear". From one gets only that every entry of is in ; the entries of themselves are arbitrary reals, possibly negative or not equal to , so need not be an indicator vector and 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 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 (for instance, taking the with ) does not work.
EuclideanSpace ℝ (Fin m) and EuclideanSpace ℝ (Fin n), so ‖·‖ is the paper's . Using the sup norm of Fin m → ℝ would give a different statement.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.hC.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.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 of its 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 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 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.
Fix a depth and branch widths , with . A regular ternary scenario tree has scenarios, one for each index tuple , where is the successor chosen at level . Choosing successor adds the increment , and scenario is the vector with
All scenarios have probability . The distance between scenarios is the maximum norm .
Deleting the scenarios of an index set and moving each deleted scenario's probability to a nearest kept scenario costs the reduction distance
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 scenarios is .
Let and let with and . Then any two distinct scenarios are at distance at least ; there is a set of scenarios each paired with a scenario outside it at distance exactly ; and for each with ,
with the minimum attained.
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 for each …". 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 , and the definition of when some widths vanish. No machine-checked version of this result or of the reduction distance is known to exist.
The lower bound is routine: two distinct scenarios first differ at some level , where their coordinates differ by or . The substance is attainment: one must exhibit, for every , a kept set of size whose every deleted scenario lies at distance exactly from some kept one. The obvious candidate, keeping the scenarios that take the middle branch at level , has every other scenario at distance exactly from a kept one, but it keeps scenarios and so covers only . Going down to 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 and accumulate on top of the one at level . The paper's proof of this step is not written out, and it depends on the widths of the two levels below : the hypothesis is essential, and the result is false without it (for and one has , not ).
Finset.inf' over the complement of ; the complement must be nonempty, so no default value arises. is stated as IsLeast of the set of all values with : the goal asserts both the lower bound for every and attainment by some . A formalization that exhibits a single with , or states an infimum without attainment, or drops any hypothesis on , is a different (and in the last case false) statement.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 by a measure supported on 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 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.
Fix a horizon and level parameters , with . A regular binary scenario tree has scenarios. A scenario is determined by a branch at every level , and is the vector with
All scenarios start at the root and carry probability . Scenarios are compared in the maximum norm .
Deleting the scenarios with indices in and moving each deleted scenario's probability to a nearest kept scenario costs the reduction cost
which by Theorem 2.1 of the paper is the minimal Kantorovich-type distance between and a measure supported on the kept scenarios. The minimal reduction distance for kept scenarios is .
In the Lean development, scenarios are indexed by σ : Fin K → Fin 2 (Fin-index is tree level , value is the branch , value is ), lev σ k is the branch at level , scenario δ σ : Fin (K+1) → ℝ is , and redCost δ J hJ is .
Let , , and . Then any two distinct scenarios are at distance at least ; there is a set of scenarios each of which has a partner outside at distance exactly ; and for every with
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 . Section 4 of the paper uses it (Example 4.1, ) 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 distinct pairs … at distance exactly " is false as an exact count (for , 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 degenerates when some , although the proposition still holds; the mission defines by branch indices.
The lower bound is a direct computation. The content is the matching upper bound: a set 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 . That handles only half of the scenarios with a single partner each, and it cannot reach 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 is exactly where the hypothesis enters. Without it, eq. (20) fails: for , and the true minimum is , not . The passage from to general also needs care: the deleted set must shrink while each remaining deleted scenario keeps its partner among the kept ones.
Fin K → Fin 2, which has exactly elements. The paper's -tuple has a level-0 entry with no choice, so it is dropped, and the vector keeps its coordinates with .δ : ℕ → ℝ, with and the arg min stated for only. is not assumed, because the paper allows and the proposition holds with zeros.Fin (K+1) → ℝ, which is the maximum norm, and is written out.Finset.inf'.IsLeast over the set of attained values , , so both the lower bound and attainment are part of the goal. A proof of for a single exhibited , or a real infimum without attainment, does not prove the goal.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 is welcome. Contributions of proofs of the milestones individually, in any order, are welcome.
Multistage and two-stage stochastic programs are solved numerically on a discrete probability distribution: a finite set of scenarios with probabilities . The size of the resulting optimization problem grows with , 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.
Let be a finite-dimensional real vector space with a norm , let , and let be continuous and nondecreasing with . The cost between two points of is
It is nonnegative, symmetric, and zero on the diagonal.
The original distribution is with and . Deleting the scenarios in a set and assigning new weights , , to the kept ones gives . The distance between and is the optimal value of the transportation problem
The reduction cost of deleting is
and the optimal reduction problem (8) minimizes over all with , where is the number of scenarios to keep.
Forward selection builds the kept set greedily. With and , it chooses
Fast forward selection (Algorithm 2.4) computes the same choices through an updated cost matrix: , , , and .
For and every run of Algorithm 2.4, with any tie-breaking in the arg min,
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 is the reduction cost of the scenarios deleted so far. Combined with Theorem 2.1, is the optimal transportation distance between 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.
The mathematics is elementary; the difficulty is bookkeeping. The recursion for refers to the previous step's column , which itself was updated, so unrolling it to a minimum over is an induction on in which the index sets , the 1-based step counter and the complement structure all move together. The natural first attempt, identifying with the minimum over the complement of , is off by one step: the correct set is the complement of , which contains itself. For Theorem 2.1 the lower bound requires using that for kept scenarios and that every plan ships all of somewhere outside ; the attainment part requires constructing the plan explicitly from the choice , including scenarios for which several kept scenarios are equally near.
ω : Fin N → E with E a finite-dimensional real normed space; the paper's closed set plays no role beyond containing the scenarios and is omitted. Scenarios need not be distinct.ℝ → ℝ with the paper's assumptions imposed on (IsGrowthFunction); every theorem carries them, together with and .Finset.inf', never a real infimum with a default value.u : ℕ → Fin N with 1-based steps. is the printed recursion, extended to all indices; runs are any sequences satisfying the arg-min conditions, so every tie-breaking rule is covered.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 is a gradient), convex–concave saddle-point problems (where 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 per iteration. The reflected projected gradient method of Malitsky (SIAM J. Optim., 2015) uses one evaluation of but evaluates it at , a point that may lie outside the domain of . 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 , 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.
Let be a finite-dimensional real inner product space with inner product and norm . Let and write . Let . The variational inequality is
The standing assumptions are:
The proximal operator of is . Let be the golden ratio, so that . For a step and arbitrary starting points , the Golden Ratio Algorithm generates, for ,
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 .
If is -Lipschitz on (), (C1)–(C3) hold, and , then there is with
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.
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 evaluated only at points of , where it is defined. This matters when is expensive (a large matrix–vector product, a simulation) or undefined outside the feasible set (for instance an operator involving on the positive orthant). The analysis also explains the constant: the averaging weight is the largest with , and the step bound 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 .
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.
The naive approach, to show that decreases, fails: GRAAL is not Fejér monotone in , because the forward step is taken from the average and uses rather than at the new point. The quantity that decreases is an energy mixing with the successive difference , 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 is merely lower semicontinuous and extended-valued, is a separate step. On the formal side, takes the value , so the prox-inequality and the variational inequality must be handled in extended arithmetic without letting decide anything.
E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E].E → EReal. (C2) is IsProperConvexLSC g: never , somewhere finite, convex epigraph , and LowerSemicontinuous g on all of E. is effDom g = {x | g x ≠ ⊤}.E → E; monotonicity and the Lipschitz bound are required on effDom g only. The step range is 0 < λ, λ ≤ φ / (2 * L) with 0 < L and φ = Real.goldenRatio.solutionSet g F: points of effDom g satisfying (1) for every , evaluated in EReal.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: and are free and the entry is unused.∃ 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 and every point is a solution and constant sequences form a run of (6); a formalization under which IsGRAALRun has no instances, or in which may be empty, is ruled out. Two hypotheses are added to printed statements and flagged in their notes: in Lemma 1, which is false without it, and in Eq. (14), needed at because the paper's is only defined on .
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.
The nearest common ancestor (nca) problem asks, for a fixed rooted tree and a sequence of vertex pairs , 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):
Fix and let be the complete binary tree of depth . A vertex is identified with the path from the root to it, a word of at most left or right turns; the root is the empty word and has vertices. Following the paper's Appendix (pp. 354–355):
The vertices of are numbered from to in symmetric order (in-order): at every vertex, first the left subtree, then the vertex, then the right subtree. is the number of and the vertex numbered . For (Fig. 1 of the paper) the root is , its children and , and the leaves . denotes bitwise exclusive or and the base-two logarithm.
Two procedures of §3 use only numbers, heights and :
The algorithm to compute (p. 342) runs the nca depth algorithm to obtain and then the depth algorithm on . The goal states that it returns the nearest common ancestor: for all vertices of , with the output of the nca depth algorithm and ,
In the order the paper uses them:
Two supporting statements pin the definitions to the paper: is a bijection onto , and the longest common prefix is the deepest common ancestor.
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).
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 , where is its left-to-right position. That counting argument sums the sizes of the subtrees that precede 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 .
List Bool of length at most (false = left). Ancestry is the prefix relation, the longest common prefix, depth the length, and height . None of these structural notions uses the numbering.Nat.log 2 x, which agrees for . is ^^^ on , and floor division is / on .Proofs of any milestone are welcome.