Combinatorics

Graph Theory Operations Research·Captain: mikedeng1

Paths, Trees, and Flowers II: Invariance of the Dual — the Outer Vertices O(G) Are Exactly the Vertices Left Exposed by Some Maximum MatchingResearch Paper

Motivation

A maximum matching of a graph is a largest set of edges no two of which share a vertex. Maximum matchings are rarely unique, and a basic question is which features of them are forced by the graph. J. Edmonds' paper Paths, trees, and flowers (Canad. J. Math. 17 (1965), 449–467) gave the first polynomial-time algorithm for maximum matching in general graphs. Its Section 6, Invariance of the dual, uses the output of that algorithm to answer this question. The vertices that some maximum matching leaves uncovered, their neighbours, and the rest form a decomposition of the graph that does not depend on the matching chosen or on any choice made by the algorithm.

This decomposition is now called the Gallai–Edmonds structure theorem. T. Gallai obtained it independently (Gallai 1963, 1964; see Selected references). It is a standard tool in matching theory (Lovász–Plummer, Matching Theory, 1986): it determines the minimum odd-set cover of Section 5 of the same paper canonically (6.7), and it underlies the Tutte–Berge formula and the analysis of factor-critical graphs.

Timeline. Berge (1957) characterized maximum matchings by the absence of augmenting paths. Gallai (1963–1964) and Edmonds (1965, §6) proved the structure theorem; Edmonds' proof goes through the trees and shrunken blossoms of his algorithm. Witzgall's argument, reported in 6.6, simplifies the converse half.

Setting

A graph $G$ has a finite set of vertices and a finite set of edges, each edge meeting exactly two distinct vertices; parallel edges are allowed. A vertex is exposed for a set of edges $M$ if no edge of $M$ meets it.

An alternating tree $J$ is a tree (a connected graph with one more vertex than edges) whose vertices are split into inner and outer vertices, so that every edge joins an inner vertex to an outer one and every inner vertex meets exactly two edges of $J$ . A planted tree for $M$ with root $r$ is an alternating tree such that $M \cap J$ is a maximum matching of $J$ and $r$ , the vertex of $J$ left exposed by $M \cap J$ , is exposed for $M$ .

Shrinking a vertex set $U$ replaces $U$ by a single pseudovertex. Edges inside $U$ disappear; edges leaving $U$ keep their identity and now meet the pseudovertex. The set $U$ is the pseudovertex's complete expansion. A blossom for $M$ is an odd circuit $B$ for which $M \cap B$ is a maximum matching of $B$ . Shrinking blossoms repeatedly, inside graphs already shrunk, gives the graph $G^* = G/\mathcal P$ , where $\mathcal P$ is a partition of the vertices into blossom sets.

Construction 6.0. Let $M$ be a maximum matching. Run the matching algorithm on $(G, M)$ without augmenting. It grows planted trees $J_1, \dots, J_n$ in $G^*$ , one from each exposed vertex, and shrinks blossoms as they appear. The output satisfies:

the trees are disjoint and planted for $M^* = M/\mathcal P$ ;
every exposed vertex of $G^*$ lies in some tree;
$J_i$ is Hungarian in $G^* - J_1 - \dots - J_{i-1}$ : its outer vertices are joined only to its own inner vertices or to earlier trees;
every pseudovertex is an outer vertex of some $J_i$ .

The outer vertices $O(G)$ are the vertices whose part is a one-vertex outer vertex of some $J_i$ , together with all vertices of pseudovertex expansions. The inner vertices $I(G)$ are the vertices whose part is an inner vertex of some $J_i$ .

Formalization targets

Goal: Theorem 6.2 (a)–(c)

For every maximum matching $M$ and every output of construction 6.0:

\text{(a)}\quad v \in O(G) \iff \exists\, M' \text{ maximum matching of } G \text{ with } v \text{ exposed for } M',

\text{(b)}\quad v \in I(G) \iff v \notin O(G) \text{ and } v \text{ is adjacent to a vertex of } O(G),

\text{(c)}\quad u,v \text{ in the same part of } \mathcal P \iff u = v \text{ or } u, v \text{ in the same component of } O(G)^+,

where $O(G)^+$ is the subgraph induced on $O(G)$ .

Milestones

4.1–4.2: the maximum matchings of an alternating tree.
4.14: lifting a matching through the complete expansion of a pseudovertex, with a free choice of the exposed vertex.
4.15, extension, in the forest form of 4.20.
6.4: adjacency of outer and inner vertices.
6.2 (b) and 6.2 (c) separately.
6.5: every outer vertex is exposable.
6.6: for non-outer $v$ meeting $e \in M$ , $M - e$ is maximum in $G - v$ .
6.6: only outer vertices are ever exposed.

A companion item states that construction 6.0 succeeds for every maximum matching.

Significance

The result. Part (a) characterizes, without reference to any algorithm, the vertices that a maximum matching can miss. Parts (b) and (c) then make $I(G)$ and $G^*$ invariants of $G$ , as 6.1 announces: "the graph $G^*$ is uniquely determined by $G$ alone". Several consequences rest on this invariance: the unique preferred minimum odd-set cover (6.7), the Tutte–Berge deficiency formula read off from $|I(G)|$ and the components of $O(G)^+$ , and the classification of graphs into those with and without perfect matchings in terms of a canonical barrier.

Formalizing it. The theorem has been proved since 1964, but the proof in this paper has not been machine-checked. A formalization requires the paper's own objects: multigraphs with edge identity preserved under contraction, nested blossom shrinking, and alternating and planted trees. These are the objects of Edmonds' blossom algorithm, and they are reusable for any formal treatment of it. Mathlib contains Tutte's theorem for simple graphs but neither shrinking nor the Gallai–Edmonds decomposition.

Difficulty

The statement is about one particular output of a nondeterministic process. The partition into trees depends on the order in which they were grown, and the non-matching tree edges and the blossoms chosen are arbitrary (6.1). An outer vertex of a later tree may be joined to an inner vertex of an earlier one, so the individual trees are not Hungarian in $G^*$ . The tempting argument "each tree is Hungarian, so apply the tree lemma tree by tree" therefore fails. Only the ordered condition, applied in both directions as in 6.4, shows that the outer vertices of all trees together are adjacent only to inner vertices. Moving between $G$ and $G^*$ requires lifting matchings through nested blossoms, which means an induction over the nesting rather than over a single odd circuit.

Formalization scope

Graphs are the published EdmondsMatching65.Polyhedron.Graph V E: finite vertex and edge types, an unordered pair of distinct ends for each edge, parallel edges allowed. Matchings are its IsMatching, and "maximum" means maximum cardinality. A matching of a subgraph is a matching of $G$ contained in the subgraph's edges. Paths are not needed.

Shrinking is contraction along a Finpartition of the vertex set. The vertices of $G^*$ are the parts, and the edges of $G^*$ are the edges of $G$ joining different parts. Blossom sets are an inductive predicate recording the nested odd circuits directly; there is no tower of types.

The output of 6.0 is the structure Config60. It records exactly the invariants the construction establishes and nothing more, and the goal is stated for every such configuration. The configuration must not be weakened. Dropping density, the ordered Hungarian condition, the outerness of pseudovertices or the blossom condition on the parts makes (a) or (b) false. Taking the $J_i$ to be arbitrary trees, or $\mathcal P$ an arbitrary partition, would state a different and false theorem. The goal is not vacuous: exists_config_6_0 asserts that a configuration exists for every maximum matching. Shrinking is defined in 4.9 only for connected sets, so the forest form of 4.15 assumes connected parts.

Welcome contributions: the general theory of alternating trees and Hungarian forests (4.2, 4.17 and their forest forms), the lifting lemma 4.14 for nested odd circuits, and a proof of exists_config_6_0.

Selected references

J. Edmonds, Paths, trees, and flowers, Canadian Journal of Mathematics 17 (1965), 449–467. https://doi.org/10.4153/CJM-1965-045-4
C. Berge, Two theorems in graph theory, Proceedings of the National Academy of Sciences USA 43 (1957), 842–844. https://doi.org/10.1073/pnas.43.9.842
T. Gallai, Kritische Graphen II, Publ. Math. Inst. Hungar. Acad. Sci. 8 (1963), 373–395; Maximale Systeme unabhängiger Kanten, ibid. 9 (1964), 401–413.
L. Lovász and M. D. Plummer, Matching Theory, North-Holland, 1986 (reprinted AMS Chelsea, 2009). https://doi.org/10.1090/chel/367
A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Chapter 24.

16 thms2 active usersReviewed

Completed

Graph Theory Operations Research·Captain: mikedeng1

An Introduction to Timetabling 3: Course Scheduling with Unavailabilities and Preassignments in p Periods Is Equivalent to p-Coloring the Nodes of a GraphResearch Paper

Motivation

Universities schedule lectures and examinations every term. When students choose their courses freely, with no fixed curriculum, the basic requirement is that no student is asked to attend two lectures at the same time. On top of this come local constraints: a course cannot take place at some periods (its teacher or a suitable room is unavailable), and some lectures are fixed in advance at a given period. D. de Werra's invited review An introduction to timetabling (Eur. J. Oper. Res. 19 (1985) 151–162) surveys the graph models of these problems. Its §3.1 shows that course scheduling, with unavailabilities and preassignments, is exactly a node colouring problem. This reduction is the standard starting point for graph colouring heuristics in timetabling, including the examination timetabling literature.

Setting

A course scheduling instance has $q$ courses $K_b$ , course $K_b$ consisting of $k_b$ lectures $l_a$ , and $r$ students; student $i$ takes a set $T_i$ of courses. There are $p$ periods.

The lecture graph $G$ has one lecture-node $m_{ab}$ for each lecture $l_a$ of each course $K_b$ . Two lecture-nodes of the same course are adjacent. Two lecture-nodes of distinct courses $K_b$ , $K_{\bar b}$ are adjacent whenever some student takes both courses.

A feasible course schedule in $p$ periods assigns a period $s(l) \in \{1,\dots,p\}$ to each lecture so that two lectures of one course are at different periods and no student has two lectures at the same period.

A course scheduling problem with unavailabilities and preassignments (CSUP) adds, for each course $K_b$ , a set $U_b$ of forbidden periods, and for some lectures $l$ a prescribed period $\bar k(l)$ . A solution is a feasible schedule with $s(l) \notin U_b$ for every lecture $l$ of $K_b$ and $s(l) = \bar k(l)$ for every preassigned lecture.

The graph $\hat G$ of a CSUP adds one period-node $k$ per period to $G$ . All pairs of period-nodes are adjacent. A lecture-node of $K_b$ is adjacent to period-node $k$ if $k \in U_b$ . A lecture-node of a lecture preassigned to $\bar k$ is adjacent to every period-node $k \neq \bar k$ .

A node colouring with $p$ colours assigns one of $p$ colours to each node so that adjacent nodes get different colours.

Formalization targets

Goal: Proposition 3.1

\text{the CSUP } P \text{ has a solution in } p \text{ periods} \iff \hat G(P) \text{ has a node colouring with } p \text{ colours.}

Milestones

§3.1 (p. 157). Without unavailabilities and preassignments, the feasible schedules in $p$ periods are exactly the node colourings of $G$ with $p$ colours.
Figure 4 (p. 157). For courses $K_1,K_2,K_3$ with $1,2,2$ lectures, student 1 taking $K_1,K_2$ and student 2 taking $K_2,K_3$ , the printed schedule in $4$ periods is feasible.
Proof of Proposition 3.1 (p. 158). Every colouring of $\hat G$ with $p$ colours gives a solution in which lecture $l_a$ of $K_b$ is at period $k$ exactly when $m_{ab}$ has the colour of period-node $k$ , and every solution arises in this way from some colouring.
Proposition 3.2 (p. 158). Let $H$ be a graph on lecture-nodes and a clique of $p$ period-nodes, with some lecture-nodes precoloured consistently with the colours of period-nodes. Removing the precoloured nodes and joining their neighbours to the matching period-nodes gives a graph $\hat G'$ with

H \text{ has a } p\text{-colouring respecting the precolouring} \iff \hat G' \text{ is } p\text{-colourable.}

Significance

The result. Proposition 3.1 turns a family of constrained timetabling problems into one well-studied problem. Any exact or heuristic method for node colouring (sequential colouring, DSATUR, implicit enumeration; §3.2 of the paper) applies directly to course scheduling with forbidden and fixed periods, and lower bounds on the chromatic number become lower bounds on the number of periods. Proposition 3.2 adds that preassignments cost nothing for node colouring: a precoloured instance is again a plain colouring instance. For edge colouring the paper contrasts this with the NP-completeness of precoloured edge colouring.

The formalization. The results are proved on the page in a few lines and are not machine-checked anywhere. This mission makes the reduction precise. It writes out the graph $\hat G$ as a definition, isolates the consistency condition that Proposition 3.2 needs, and states the correspondence between colourings and schedules in a form other formal timetabling and scheduling developments can use. The definitions of course instances, CSUP and $\hat G$ can serve formal work on examination timetabling and on the complexity of timetabling problems.

Difficulty

The forward direction of Proposition 3.1 is direct: colour each lecture-node with its period and each period-node with itself. The converse is where care is needed. A colouring of $\hat G$ need not give period-node $k$ the colour $k$ ; the colours of the period-nodes can be any permutation of the palette. The schedule must therefore be read through the colours of the period-nodes, and the fact that the $p$ period-nodes form a clique is what makes this well defined.

For Proposition 3.2, the obvious reading of the page is false. If two adjacent lecture-nodes are precoloured with the same colour, no colouring respects the precolouring, yet removing both nodes deletes the edge between them and the reduced graph may still be colourable. The same happens when a node is precoloured with the colour of a period-node it is adjacent to. The proposition therefore needs a consistency condition the page leaves implicit. The page's "1–1 correspondence" between colourings fails when precolours are fixed colours of the palette, since $\hat G'$ 's colourings can permute the colours of the period clique; the target is the equivalence of the proposition.

Formalization scope

Courses, students, lectures of a course and periods are indexed from $0$ (Fin q, Fin r, Fin (lectures b), Fin p). A lecture is a dependent pair Σ b, Fin (lectures b), and the nodes of $\hat G$ are Lecture ⊕ Fin p. Graphs and colourings are Mathlib's SimpleGraph, SimpleGraph.Coloring and SimpleGraph.Colorable. Unavailability is per course and preassignment per lecture, as on the page. The set-valued constraint of the Figure 5 example ("1 lecture of $K_3$ at period 1 or 2") is not modelled. Feasibility includes the clique on the lectures of each course even when no student takes the course, because the page's graph contains it. $p = 0$ is allowed.

The paper states Proposition 3.1 as "one can construct a graph $\hat G$ such that …". The existential form is trivially true (pick a complete graph on $p+1$ nodes or an edgeless graph according to the answer), so the goal is stated about the specific graph csupGraph P built in the proof.

Proposition 3.2 is stated for any graph whose period-nodes form a clique, with two disclosed consistency hypotheses: no precoloured node is adjacent to its own period-node, and no two adjacent nodes are precoloured with the same period-node's colour. A sanity file shows that the equivalence fails without them. "Precoloured" means "receives the colour of period-node $k$ ", the reading of the proof of Proposition 3.1.

Not targeted: the NP-completeness remarks (cited, not proved), the heuristics of §3.2–§3.4, and the hypergraph classroom model of §3.5, whose "1–1 correspondence" has the same palette-permutation issue as Proposition 3.2.

Contributions welcome: proofs of the milestones and the goal, and general lemmas about colourings of graphs containing a clique of size equal to the number of colours.

Selected references

D. de Werra, An introduction to timetabling, European Journal of Operational Research 19 (1985) 151–162. https://doi.org/10.1016/0377-2217(85)90167-5
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979 (NP-completeness of graph $p$ -colourability, reference [13] of the paper).
D. Brélaz, New methods to color the vertices of a graph, Communications of the ACM 22 (1979) 251–256. https://doi.org/10.1145/359094.359101

7 thms2 active usersReviewed

Completed

Graph Theory Theoretical Computer Science·Captain: mikedeng1

A Theorem on Boolean Matrices: Warshall's Construction M* Equals the Boolean Sum M ∨ M² ∨ ⋯ ∨ Mᵈ of the Boolean Powers of MResearch Paper

Motivation

A finite directed graph on $d$ vertices is recorded by its adjacency matrix, a $d \times d$ array of zeros and ones. Many questions about the graph are questions about reachability: can vertex $j$ be reached from vertex $i$ by following one or more edges? In the late 1950s this question arose in the analysis of programs. Prosser (Applications of Boolean matrices to the analysis of flow diagrams, 1959) represented the flow diagram of a program by a boolean matrix and read off properties such as which blocks can follow which; Marimont (A new method of checking the consistency of precedence matrices, J. ACM 1959) used the same matrices to check precedence relations for consistency.

In both works the reachability matrix is described as a boolean sum of boolean powers of the adjacency matrix. Computed that way, it costs $d$ boolean matrix products, that is on the order of $d^3$ operations per product. Stephen Warshall's two-page note (A theorem on Boolean matrices, J. ACM 9 (1962) 11–12) proves that a much shorter procedure, $d$ passes of row updates performed in place, gives the same matrix. The same procedure was published in the same year by Floyd as Algorithm 96: Ancestor (Comm. ACM 5 (1962) 344), and its weighted version is Floyd's Algorithm 97: Shortest Path. The procedure is now taught as the Floyd–Warshall or Roy–Warshall algorithm.

Timeline. 1959: Prosser and Marimont describe reachability as a sum of boolean powers. 1959: Roy publishes the same closure construction in French (C. R. Acad. Sci. Paris 249). 1962: Warshall's note proves the in-place construction correct; Floyd's Algorithm 96 publishes it as code, and Algorithm 97 extends it to shortest paths.

Setting

Fix a natural number $d$ and let $M = (m_{ij})$ be a $d \times d$ matrix each of whose entries is $0$ or $1$ .

The boolean product of two such matrices $A$ and $B$ is the matrix $A \wedge B$ with $(A \wedge B)_{ij} = \bigvee_k (a_{ik} \wedge b_{kj})$ : the entry is $1$ when some index $k$ has $a_{ik} = b_{kj} = 1$ .
The boolean sum $A \vee B$ is the entrywise disjunction, $(A \vee B)_{ij} = a_{ij} \vee b_{ij}$ .
The boolean powers are $M^1 = M$ and $M^{p+1} = M^p \wedge M$ .
The introduction's matrix is the power sum

M' \;=\; \bigvee_{p=1}^{d} M^p .

The THEOREM defines $M'$ instead by chains: $m'_{ij} = 1$ if and only if either $m_{ij} = 1$ or there are indices $k_1, \dots, k_n$ with $m_{ik_1} = m_{k_1k_2} = \cdots = m_{k_nj} = 1$ . Footnote 2 states that the two definitions agree.
Warshall's construction $M^*$ : set $M^* = M$ ; for $i = 1, \dots, d$ in turn, for every row $j$ with $m^*_{ji} = 1$ and every column $k$ , set $m^*_{jk} = m^*_{jk} \vee m^*_{ik}$ . Entries are overwritten during a pass and later steps of the same pass read the new values.
Footnote 3 gives a recursive version: $(m_{ij})_0 = m_{ij}$ and $(m_{ij})_{n+1} = (m_{ij})_n \vee \bigl((m_{i,n+1})_n \wedge (m_{n+1,j})_n\bigr)$ , and asserts $m^*_{ij} = (m_{ij})_d$ .

In Lean the matrix is M : Fin d → Fin d → Bool. The power sum is powerSum M, the chain relation ChainRel M i j, the recursion warshallRec M n, all in the namespace WarshallBool.Closure. The construction $M^*$ is the published FloydAlgorithms.ShortestPath.algorithm96 M.

Formalization targets

Goal: the construction computes the power sum

M^* \;=\; \bigvee_{p=1}^{d} M^p \qquad \text{for every } d \text{ and every } d \times d \text{ 0-1 matrix } M .

This is the transformation the introduction asks for, combined with the THEOREM's assertion $M^* = M'$ and footnote 2. The goal has no hypothesis beyond the shape of $M$ .

Milestone 1 (Proved, referenced): the THEOREM

m^*_{ij} = 1 \iff m_{ij} = 1 \text{ or } m_{ik_1} = \cdots = m_{k_nj} = 1 \text{ for some } k_1, \dots, k_n .

It is already on the platform as FloydAlgorithms.ShortestPath.algorithm96_eq_transGen, stated with Mathlib's transitive closure Relation.TransGen, and it is not posed again.

Milestone 2: footnote 2

m_{ij} = 1 \text{ or a chain } i \to k_1 \to \cdots \to k_n \to j \text{ of 1 entries} \iff \Bigl(\bigvee_{p=1}^{d} M^p\Bigr)_{ij} = 1 .

Companion: footnote 3

M^* \;=\; \bigl((m_{ij})_d\bigr)_{i,j} .

This is not a milestone of the goal; it identifies the in-place construction with its stage-by-stage recursion.

Significance

The result. The theorem says that reachability in a directed graph on $d$ vertices, defined through matrix powers, can be computed by $d$ passes of in-place row operations, on the order of $d^2$ row updates instead of $d$ full boolean matrix products. The same scheme, with $(\min, +)$ in place of $(\vee, \wedge)$ , is the Floyd–Warshall shortest-path algorithm; with other semirings it computes regular expressions of finite automata (Kleene, McNaughton–Yamada) and path problems in general. Footnote 3's recursion is the form in which the algorithm is usually proved correct today, and its equivalence with the in-place version is what justifies running it without a second copy of the matrix.

Formalizing it. The chain form of the THEOREM is already machine-checked on Prove2Me (algorithm96_eq_transGen). What this mission adds is the statement in the paper's own terms: the introduction's power sum $\bigvee_{p=1}^d M^p$ , footnote 2's equivalence between powers and chains, which requires that chains can be shortened to length at most $d$ , and footnote 3's in-place versus recursive equivalence. None of these three is on the platform. The paper itself proves only the THEOREM; footnotes 2 and 3 are stated without proof.

Difficulty

Footnote 2 calls the equivalence "trivial", but one direction needs a pigeonhole argument: a chain $i \to k_1 \to \cdots \to k_n \to j$ of arbitrary length witnesses some power $M^{n+1}$ , and the power sum stops at $M^d$ . A chain with repeated indices has to be shortened, and the shortening must keep at least one step, since there is no reflexive part ( $m'_{ii} = 1$ only through a cycle). For a $d$ -cycle the diagonal entries appear only in $M^d$ , so the range $1..d$ is exact.

Footnote 3 compares two computations that read different data. The construction overwrites entries during a pass, and later steps of the same pass read the overwritten values; the recursion reads only the previous stage. The two agree only because of what a pass does and does not overwrite, and the published algorithm96 is three nested left folds over List.finRange, so the comparison has to be made against that concrete loop structure rather than an idealized simultaneous update.

Formalization scope

Matrices are Fin d → Fin d → Bool, with $1$ as true. Indices are $0, \dots, d-1$ instead of the page's $1, \dots, d$ ; the pivot of pass $i$ (1-based) is the 0-based index $i-1$ .
$d = 0$ is allowed; all statements are then trivially true, as on the page.
The boolean product boolProd A B i j is decide (∃ k, A i k = true ∧ B k j = true). Mathlib's matrix product on Matrix (Fin d) (Fin d) Bool is not the boolean product: Bool is a boolean ring there, its addition is exclusive or, and that product counts walks modulo 2. A formalization through * or ^ on Matrix _ _ Bool states a different, false theorem and is ruled out.
boolPow M p is the page's $M^p$ for $p \ge 1$ ; the base boolPow M 0 is the identity matrix, which is not on the page and does not enter the sum. powerSum M i j holds iff boolPow M p i j for some $p \in \{1, \dots, d\}$ . No reflexive closure is included anywhere.
ChainRel M i j is the existence of a list $[k_1, \dots, k_n]$ (possibly empty) making $i, k_1, \dots, k_n, j$ a List.IsChain of true entries.
warshallRec M n uses the 0-based pivot $n$ at stage $n+1$ and is constant after stage $d$ , which footnote 3 never uses.
$M^*$ is the published algorithm96, which fixes the inner loops over rows and columns in ascending order; Warshall leaves that order open, and it does not affect the result.
The goal must not be stated through TransGen, ChainRel or warshallRec, and powerSum is defined from boolPow, not from the closure or the algorithm.

Reusable beyond this mission: the boolean matrix product and powers, the power-sum characterization of the transitive closure of a relation on Fin d (footnote 2), and the in-place/recursive equivalence (footnote 3), which carries over to Floyd's Algorithm 97. Proofs of milestone 2 and of the companion are welcome independently of the goal.

Selected references

S. Warshall, A theorem on Boolean matrices, J. ACM 9(1) (1962) 11–12. https://doi.org/10.1145/321105.321107
R. W. Floyd, Algorithm 96: Ancestor, Comm. ACM 5(6) (1962) 344–345. https://doi.org/10.1145/367766.368166
R. W. Floyd, Algorithm 97: Shortest path, Comm. ACM 5(6) (1962) 345. https://doi.org/10.1145/367766.368168
R. T. Prosser, Applications of Boolean matrices to the analysis of flow diagrams, Proc. Eastern Joint Computer Conference (1959) 133–138. https://doi.org/10.1145/1460299.1460314
R. B. Marimont, A new method of checking the consistency of precedence matrices, J. ACM 6(2) (1959) 164–171. https://doi.org/10.1145/320964.320975
B. Roy, Transitivité et connexité, C. R. Acad. Sci. Paris 249 (1959) 216–218.

5 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

On Cores and Indivisibility 1: The Housing Market's Game Without Side Payments Is BalancedResearch Paper

Motivation

A market in which each trader owns one indivisible good has a basic coordination question: can all goods be reassigned so that no group of traders can withdraw its own goods and improve every member's outcome? Houses are the paper's running example. Monetary transfers and fractional houses are absent, so ordinary convex allocation arguments do not describe the setting. Shapley and Scarf use games without side payments to express what each coalition of owners can achieve, and identify a balance property of this game in their Section 4 theorem (Shapley and Scarf, 1974).

The paper states that a general balanced-game theorem gives a nonempty core once balance has been established. Its Section 4 contribution is the classification of this particular housing market game. The separate top-trading-cycles construction in Section 6 gives another route to a core allocation and is the subject of the second mission in this series (Shapley and Scarf, 1974).

Setting

Let $N$ be a nonempty finite set of traders. Trader $j$ brings one indivisible item $j$ . Trader $i$ 's ranking of item $j$ is represented by a real number $a_{ij}$ . Only comparisons within one trader's row matter: $a_{ij}>a_{ik}$ means that $i$ prefers $j$ to $k$ , while equality represents indifference. No strict-preference or positivity assumption is imposed on the preference matrix $A=(a_{ij})$ .

A coalition $S\subseteq N$ can redistribute the items brought by its members. Its allocation matrix $P$ has $P_{ij}=1$ when trader $i$ receives item $j$ , and zero otherwise. An $S$ -allocation puts exactly one 1 in each column indexed by $S$ and has zeros in rows and columns outside $S$ . An $S$ -permutation is an $S$ -allocation with row sums at most one, so every member of $S$ receives exactly one of the coalition's items. Rows index traders and columns index items.

For a proposed payoff vector $x\in\mathbb R^N$ , define the acceptability matrix

b_{S|ij}(x)= \begin{cases} 1,& i\in S\text{ and }x_i\le a_{ij},\\ 0,&\text{otherwise}. \end{cases}

The coalition payoff set is

V(S)=\{x\in\mathbb R^N:\text{some }S\text{-permutation }P \text{ satisfies }P_{ij}\le b_{S|ij}(x)\text{ for all }i,j\}.

Thus a coalition can reach a payoff threshold if it can give each member an item that member values at least as highly. The comparison is weak, so ties count as acceptable. This is the characteristic function used in the paper's Section 4 (Shapley and Scarf, 1974, pp. 109–110 of the source printing).

A balanced family $T$ is a family of nonempty coalitions with nonnegative real weights $\delta_S$ , zero outside $T$ , such that every trader has total covering weight one:

\sum_{\substack{S\in T\\j\in S}}\delta_S=1 \quad(j\in N).

The weights may be zero even for a coalition listed in $T$ . A balanced game is a game without side payments whose feasible payoff sets obey

\bigcap_{S\in T}V(S)\subseteq V(N)

for every balanced family $T$ . This includes overlapping families, not merely partitions (Shapley and Scarf, 1974, pp. 108–109).

Formalization targets

The goal is the paper's Section 4 theorem:

\text{For every finite nonempty }N\text{ and every }A:N\times N\to\mathbb R,\quad V_A\text{ is a balanced game}.

It contains four requirements. For each nonempty $S$ , $V_A(S)$ is closed; it is downward closed in the coordinates of $S$ ; and its payoff slice after removing the interiors of singleton payoff sets is bounded and nonempty. The fourth requirement is the balanced-family inclusion displayed above.

The milestones name the paper's intervening claims in their order: the three game conditions, the identity $B_N(x)=\sum_{S\in T}\delta_SB_S(x)$ , the doubly stochastic character of a balanced mixture $D=\sum_{S\in T}\delta_SP_S$ , and the existence of a grand-coalition permutation $P_N\le B_N(x)$ when $D\le B_N(x)$ . The final milestone states the matrix existence claim made at the end of Section 4, without committing the theorem statement to a particular construction.

Significance

The result establishes that the finite housing market falls under the paper's general balance framework. In the paper, the cited theorem that balanced games have nonempty cores then yields a core existence conclusion for this market. That general existence theorem is external to the Section 4 proof and is not asserted by this mission's goal (Shapley and Scarf, 1974, pp. 109–110).

The formal development supplies reusable definitions of games without side payments and balanced families alongside the market-specific allocation and acceptability matrices. It also gives precise targets for the matrix claims used in the paper. The source result is proved in print; these Lean statements are proposed formalization targets and their proof bodies remain open. Nearby platform items about transferable-utility games, including the Bondareva–Shapley goal, use a real value for each coalition and do not define this paper's payoff-set game. They are not substituted for these objects.

Difficulty

The challenge is the passage from coalition-wise feasibility to feasibility for all traders together. A balancing family can overlap: choosing one feasible permutation for each coalition does not immediately give a single permutation of $N$ . Their weighted mixture has fractional matrix entries. The condition $B_N(x)\ge D$ also has to survive the move from such a mixture to an actual zero-one permutation matrix. Without that last assertion, the balancing equations alone do not prove the inclusion $V(S)$ requires. Separately, the bounded nonempty payoff-slice condition must be checked for every nonempty coalition; merely proving closedness and downward closure would define a weaker class of games.

Formalization scope

Traders are an arbitrary finite nonempty Lean type, and payoffs live in $N\to\mathbb R$ . The paper's $E^S$ is encoded as the coordinate subspace of vectors zero outside $S$ ; interiors are taken in the product topology on $N\to\mathbb R$ . The boundedness and nonemptiness test applies to the intersection of that subspace with $V(S)$ after removing the singleton interiors. All conditions defining a game quantify over nonempty coalitions. The market formula is also defined at $S=\varnothing$ , where it yields all of $\mathbb R^N$ .

Allocation matrices are real zero-one matrices. An $S$ -permutation retains the paper's column, support, and row conditions; it is not replaced by an unconstrained permutation of all traders. The inequality between matrices is entrywise. The acceptability matrix has a 1 exactly when $i\in S$ and $x_i\le a_{ij}$ ; its columns are not independently restricted to $S$ . Balancing weights are nonnegative, may vanish inside the family, and cover every trader in $N$ . These choices exclude the trivializations $V(N)=\mathbb R^N$ , balance tested only on partitions, and coalitions using outsiders' items.

The definitions need finite-sum and matrix support from Mathlib, while the eventual proof can use Mathlib's doubly stochastic matrix and permutation-matrix library. Contributions that establish the stated game conditions or any of the four sourced matrix milestones are within scope. The paper's Section 8 counterexample and the optional superadditivity observation are outside this mission's attack path.

Selected references

Lloyd S. Shapley and Herbert Scarf, On cores and indivisibility, Journal of Mathematical Economics 1 (1974), 23–37. DOI: 10.1016/0304-4068(74)90033-0. The supplied scan has printed folios 104–123; Section 4 is on folios 109–111.

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design·Captain: mikedeng1

Strategy-Proofness and Arrow's Conditions 2: Strategy-Proof Voting Procedures Correspond One-to-One to Social Welfare Functions Satisfying CS, NNR and IIAResearch Paper

Motivation

Two impossibility theorems frame the theory of collective choice. Arrow's theorem (1951) says that a rule aggregating individual preference orderings into a social ordering, subject to a short list of reasonable conditions, must be dictatorial. The Gibbard–Satterthwaite theorem (Gibbard 1973, Satterthwaite 1975) says that a voting procedure selecting a single alternative, which no voter can manipulate by misreporting, must be dictatorial once at least three outcomes are possible. Both conclusions are the same, and the two conditions—Arrow's axioms and strategy-proofness—look unrelated: one is about the coherence of a social ranking, the other about voters' incentives.

Satterthwaite's paper (Northwestern Discussion Paper No. 122, 1974; J. Econ. Theory 10, 1975) shows that the two conditions are in fact the same condition. Section 4 constructs a one-to-one correspondence between strict strategy-proof voting procedures with full range and strict social welfare functions satisfying Arrow's conditions, under which each social welfare function's top choice is the voting procedure's outcome. This mission formalizes that correspondence.

Timeline. Arrow (1951, 2nd ed. 1963) proved the general possibility theorem with conditions of non-negative response (NNR), citizens' sovereignty (CS), independence of irrelevant alternatives (IIA) and non-dictatorship. Gibbard (1973) proved that strategy-proof game forms with at least three outcomes are dictatorial, by first showing that a strategy-proof procedure induces an Arrovian social welfare function and then applying Arrow's theorem. Satterthwaite (1974/75) gave an independent direct proof of the voting-procedure theorem and proved the correspondence theorem (Theorem 2), which turns Gibbard's construction into an exact equivalence.

Setting

A committee $I_n$ of $n$ individuals chooses from a finite set $S_m$ of $m$ alternatives. A strong order on $S_m$ is a complete, transitive relation $R$ with no indifference between distinct alternatives; $x\,\bar R\,y$ denotes strict preference. Let $\rho_m$ be the set of strong orders and $\rho_m^n$ the set of strict ballot sets $B=(B_1,\dots,B_n)$ .

A strict voting procedure is a map $v:\rho_m^n\to S_m$ ; its range is $T_p=\{v(B):B\in\rho_m^n\}$ . It is strategy-proof if no individual $i$ , at any $B$ , has a ballot $B_i'$ with $v(B_1,\dots,B_i',\dots,B_n)\,\bar B_i\,v(B)$ .
A strict social welfare function is a map $u:\rho_m^n\to\rho_m$ ; $A_B=u(B)$ is the social ordering.
For $W\subseteq S_m$ , $\Psi_W(R)$ is the set of $R$ -best elements of $W$ , and $\theta_W(R)$ is the restriction of $R$ to $W$ .
$u$ underlies $v$ , and $v$ is derived from $u$ , if $\Psi_{S_m}[u(B)]=\{v(B)\}$ for every $B$ .

Arrow's conditions on $u$ : CS—for all $x\ne y$ some $B$ gives $x\,\bar A_B\,y$ ; IIA—if $\theta_W(C_i)=\theta_W(D_i)$ for all $i$ then $\Psi_W(A_C)=\Psi_W(A_D)$ ; NNR—raising an alternative $x$ in individual ballots, with the order of the other alternatives unchanged, never lowers $x$ against any other alternative in the social ordering. PO (Pareto optimality): unanimous strict preference for $x$ over $y$ yields $x\,\bar A\,y$ .

Formalization targets

Goal: Theorem 2 (p. 35)

For $n\ge2$ and $m\ge3$ there is a bijection

\lambda:\{v \text{ strict, strategy-proof},\ T_p=S_m\}\ \longrightarrow\ \{u \text{ strict},\ \text{CS},\ \text{NNR},\ \text{IIA}\}

with $\Psi_{S_m}[\lambda(v)(B)]=\{v(B)\}$ for every $v$ and every $B\in\rho_m^n$ .

Milestones

CS, NNR and IIA imply PO (p. 31, after Arrow), and PO implies CS (p. 31).
Lemma 7 (p. 30): the voting procedure derived from a strict $u$ with CS, NNR, IIA exists, is strategy-proof and has range $S_m$ .
Gibbard's claim (p. 33): for a strict strategy-proof $v$ with range $S_m$ and a fixed strong order $Q$ , the relation $P(B)$ defined by $x\,\bar P\,y\iff x=v[\Delta_{xy}(B_1),\dots,\Delta_{xy}(B_n)]$ is a strong order, and $\mu:B\mapsto P(B)$ underlies $v$ and satisfies PO and IIA.
Uniqueness (p. 34): at most one strict $u$ with PO and IIA underlies a strict strategy-proof $v$ .
NNR (p. 34): such an underlying $u$ satisfies NNR.
Lemma 8 (p. 35): a strict strategy-proof $v$ with range $S_m$ has exactly one underlying strict $u$ with CS, NNR, IIA.

Significance

The correspondence explains why the two impossibility theorems have the same conclusion: for strict preferences, a strategy-proof procedure with full range and an Arrovian social welfare function are two descriptions of one object. In particular either impossibility theorem, together with Theorem 2, yields the other. The paper draws a second consequence: a social welfare function violating rationality or IIA has a derived voting procedure that is manipulable, so Arrow's much-debated conditions are forced by the practical requirement of strategy-proofness.

On the formal side, the platform already has machine-checked proofs of the strict Arrow theorem (AGT.arrow_theorem, unanimity and pairwise IIA) and of the strict full-range Gibbard–Satterthwaite theorem (AGT.gibbard_satterthwaite). Together these determine both sides of Theorem 2 as sets of dictatorships, but neither states the correspondence, the derived/underlying relation, Gibbard's construction or NNR, and nothing on the platform states Lemmas 7 or 8. The milestones here formalize the paper's direct argument, which does not pass through the impossibility theorems.

Difficulty

The obvious argument fails in two places. First, a strategy-proof voting procedure determines only the top of a social ordering, and the whole ordering must be recovered; Gibbard's relation $P$ does this, but proving that $P$ is transitive is the core of Gibbard's proof of the Gibbard–Satterthwaite theorem, which the paper cites rather than proves. Second, NNR as stated allows many individuals to move $x$ at once, while the manipulation argument works with one ballot at a time; one must pass from a single-voter change to an arbitrary one without losing IIA or PO along the way.

A newcomer's first idea is to prove both sides are dictatorships and match dictators. That proves the bijection but needs both impossibility theorems as inputs, and the correspondence must still carry the underlying relation for every procedure.

Formalization scope

Alternatives and individuals are finite types A, ι with decidable equality; $n=|\iota|\ge2$ , $m=|A|\ge3$ throughout.
Weak orders are a structure (relation, completeness, transitivity); strong orders are the subtype with no indifference between distinct elements. Strict ballot sets are functions ι → StrongOrder A, and voting procedures and social welfare functions are defined only on them. Two social welfare functions are therefore equal exactly when they agree on every strict ballot set; this is what makes uniqueness in Lemma 8 and the bijection in Theorem 2 meaningful.
The range $T_p$ is the image of strict ballot sets; " $T_p\equiv S_m$ " is Set.range v = Set.univ.
$\theta_W(C_i)=\theta_W(D_i)$ is agreement of the two relations on $W\times W$ .
CS is stated for $x\ne y$ : as printed ("for every $x,y$ ") it is unsatisfiable at $x=y$ for a strict social ordering, and every statement would become vacuous. NNR's "for some $x$ " is read as "for every $x$ ".
"Derived from" and "underlies" are the same relation $\Psi_{S_m}[u(B)]=\{v(B)\}$ ; Lemma 7 asserts existence of the derived procedure and its properties for every derived procedure.
Gibbard's $\Delta_{xy}$ and $P$ are definitions; $P$ is the reflexive closure of the paper's $\bar P$ .
The PO claim, PO ⇒ CS, uniqueness and the NNR claim are unconditional in the paper; they are stated under §4's standing $n\ge2$ , $m\ge3$ , since with no individuals PO fails.
Theorem 2 is stated as an Equiv together with " $\lambda(v)$ underlies $v$ " for every $v$ . A bare existence of a bijection between the two sets is a cardinality fact and is not the theorem.

Reusable beyond this mission: the strict-preference vocabulary (strong orders, $\Psi_W$ , Arrow's conditions in the paper's form) and Gibbard's $\Delta_{xy}$ construction. Contributions welcome: proofs of each milestone, and bridges to AGT.arrow_theorem and AGT.gibbard_satterthwaite.

Selected references

M. A. Satterthwaite, Strategy-proofness and Arrow's Conditions: Existence and Correspondence Theorems for Voting Procedures and Social Welfare Functions, Northwestern University CMS-EMS Discussion Paper No. 122, rev. Dec. 12, 1974; J. Econ. Theory 10 (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
A. Gibbard, Manipulation of Voting Schemes: A General Result, Econometrica 41 (1973) 587–601. https://doi.org/10.2307/1914083
K. J. Arrow, Social Choice and Individual Values, 2nd ed., Wiley, 1963.

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design·Captain: mikedeng1

Strategy-Proofness and Arrow's Conditions 4: With Indifference Allowed, a Social Welfare Function Satisfying CS, NNR and IIA Is DictatorialResearch Paper

Motivation

A social welfare function turns the rankings of the members of a committee into one ranking for the committee. Arrow's general possibility theorem (Arrow, 1951/1963) shows that, once there are at least three alternatives, no such rule satisfies a short list of conditions that each look harmless unless it follows a single member's ranking. The theorem is the starting point of social choice theory and underlies the study of voting rules, preference aggregation in economics, and rank aggregation in computer science.

Arrow's own setting allows indifference: ballots and the social ordering are weak orders, and the conditions he imposed are citizens' sovereignty, non-negative response, and independence of irrelevant alternatives. Many textbook proofs, and the existing machine-checked versions, instead take strict ballots and replace the first two conditions by the Pareto condition.

Satterthwaite's discussion paper (Satterthwaite, Northwestern DP No. 122, 1974, journal version J. Econ. Theory 10 (1975)) gives a new proof of Arrow's theorem. Strict Arrovian social welfare functions correspond one-to-one to strategy-proof voting procedures with full range, and the Gibbard–Satterthwaite theorem then forces a dictator. His §6 extends the argument to weak orders by decomposing a social welfare function into a tie-breaking step followed by a strict one. This mission formalizes that weak-order extension and the strict theorem it rests on.

Timeline.

1951: Arrow proves the general possibility theorem for weak orders under CS, NNR, IIA and non-dictatorship. The second edition (1963) corrects the first edition's statement.
1973: Gibbard proves that every strategy-proof game form with at least three outcomes is dictatorial (Econometrica 41).
1975: Satterthwaite proves the same independently for voting procedures, and shows that strategy-proof procedures and Arrovian social welfare functions correspond. This gives a proof of Arrow's theorem by way of strategy-proofness.

Setting

A committee $I_n$ of $n$ individuals ranks a finite set $S_m$ of $m$ alternatives. A weak order $R$ on $S_m$ is a complete, transitive relation, and $x\,R\,y$ reads " $x$ is preferred or indifferent to $y$ ". Its strict part is $x\,\bar R\,y$ : $x\,R\,y$ and not $y\,R\,x$ . The weak orders form $\pi_m$ . A strong order is a weak order with no indifference between distinct alternatives, and the strong orders form $\rho_m$ . A ballot set is $B=(B_1,\dots,B_n)\in\pi_m^n$ .

A social welfare function $u$ assigns to every ballot set a social ordering $A=u(B)\in\pi_m$ . A strict social welfare function $\mu$ is defined only on strong ballot sets $\rho_m^n$ and takes values in $\rho_m$ . For $W\subseteq S_m$ , $\Psi_W(R)$ is the set of $R$ -best elements of $W$ , and $\theta_W(R)$ is the restriction of $R$ to $W$ .

CS (citizens' sovereignty): for all distinct $x,y$ some ballot set yields $x\,\bar A\,y$ .
IIA (independence of irrelevant alternatives): if $\theta_W(C_i)=\theta_W(D_i)$ for every $i$ , then $\Psi_W(A_C)=\Psi_W(A_D)$ .
NNR (non-negative response): if $D$ differs from $C$ only by raising an alternative $x$ on some ballots, then $x\,\bar A_C\,z$ implies $x\,\bar A_D\,z$ for all $z\neq x$ .
Dictatorial: some $i$ exists such that $x\,\bar B_i\,y$ implies $x\,\bar A\,y$ for every ballot set and all $x,y$ .

A tie-breaking function $\alpha$ maps every weak ballot set to a strong one while keeping every strict preference. It is regular if each individual's ties are broken by a fixed strong order $Q_i$ .

Formalization targets

Goal: Theorem 3' (p. 49)

For $n\ge 2$ , $m\ge 3$ and any social welfare function $u$ on weak ballot sets,

u \text{ satisfies CS, NNR, IIA} \;\Longrightarrow\; \exists\, i\;\forall B\;\forall x,y:\; x\,\bar B_i\,y \Rightarrow x\,\overline{u(B)}\,y .

The converse is false with indifference, so the goal is one-directional.

Milestones

Theorem 3 (p. 36): for strict $\mu$ , CS, NNR and IIA hold if and only if $\mu$ is dictatorial.
Lemma 10, first sentence (p. 44): if $u$ has range in $\rho_m$ and $u=\mu\circ\gamma$ with $\gamma$ regular and $\mu$ strict Arrovian, then $u$ satisfies IIA, CS and NNR.
Lemma 10, second sentence (p. 44): if $u$ has range in $\rho_m$ and satisfies IIA, CS and NNR, then $u=\mu\circ\alpha$ for a tie-breaking function $\alpha$ and a strict $\mu$ satisfying IIA, CS and NNR.
Lemma 11 (p. 48): breaking the ties of each social ordering $u(B)$ by a strong order $Q$ preserves CS, NNR and IIA and gives range in $\rho_m$ .

Significance

Theorem 3' is Arrow's theorem in the setting Arrow stated it: weak-order ballots, a weak social ordering, and the conditions CS and NNR instead of the Pareto condition. Lemma 10 and Lemma 11 together say that Arrovian social welfare functions with indifference are determined by strict ones up to tie-breaking. This is the structural fact the paper also uses for its weak-order correspondence (Theorem 2').

All results here are proved in the paper. None is formalized as stated. The platform holds a proved strict Arrow theorem, AGT.arrow_theorem, for social welfare functions on strict total orders under unanimity and pairwise IIA. Theorem 3's only-if half follows from it once CS, NNR and IIA are shown to imply the Pareto condition and the two encodings are bridged. The weak-order statement, the tie-breaking lemmas, and the "if" half of Theorem 3 are new to the platform.

Difficulty

Passing from strict to weak orders is the hard step. Restricting a weak ordering to a pair of alternatives does not determine its choice sets on larger sets once ties are present. A social welfare function that satisfies IIA on weak orders need not induce one on strong orders through an arbitrary tie-breaker. Breaking ties ballot by ballot with a non-regular rule can destroy IIA, and breaking ties in the social ordering can destroy NNR unless the same fixed order is used throughout. The obvious reduction is "break all ties and apply the strict theorem", and it fails: the dictator of the tie-broken function could depend on the tie-breaking order. The fact that it does not is part of what must be shown.

Formalization scope

Alternatives and individuals are finite types A and ι with decidable equality. $n$ = Fintype.card ι, $m$ = Fintype.card A, and $n\ge 2$ , $m\ge 3$ are hypotheses as printed. All statements live in StrategyProofArrow.WeakArrow.
A weak order is a structure (a relation with completeness and transitivity). A strong order is the subtype with no indifference between distinct elements. Strong ballot sets are functions into that subtype, so a strict social welfare function is defined on admissible profiles only.
$\theta_W(C)=\theta_W(D)$ is agreement of the two relations on $W\times W$ . $\Psi_W$ is a set, compared as a set, since weak orders can have several best elements.
CS is stated for distinct $x\neq y$ . As printed ("for every $x,y$ ") it is unsatisfiable at $x=y$ , and every theorem would become vacuous. No other trivializing reading is possible: the dictator conclusion is the paper's one-directional negation of ND, not $u(B)=B_i$ , which would be false for weak orders.
Lemma 11's tie-breaker acts on a single ordering. It is encoded as breaking the ties of $u(B)$ by a strong order $Q$ , the "tie-breaking order for $\gamma$ " of the proof of Theorem 3'.
Lemma 10's printed $u^{nm}(B)=u^{nm}[\gamma(B)]$ is read $u(B)=\mu(\gamma(B))$ , following the proof.

The definitions duplicate objects drafted in the sibling missions of this series (weak and strong orders, CS, NNR, IIA). Proofs of the strict theorem from the Gibbard–Satterthwaite theorem, bridges to AGT.arrow_theorem, and reusable lemmas about tie-breaking of weak orders are all welcome.

Selected references

M. A. Satterthwaite, Strategy-proofness and Arrow's Conditions: Existence and Correspondence Theorems for Voting Procedures and Social Welfare Functions, Northwestern University CMS-EMS Discussion Paper No. 122, 1974 (rev. Dec. 12, 1974); J. Econ. Theory 10 (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
K. J. Arrow, Social Choice and Individual Values, 2nd ed., Yale University Press, 1963. https://doi.org/10.12987/9780300186987
A. Gibbard, Manipulation of Voting Schemes: A General Result, Econometrica 41 (1973) 587–601. https://doi.org/10.2307/1914083

6 thms2 active usersReviewed

Completed

Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces VI: The Symmetric Group — ∫ exp(f(A,σ)/16) dP_N ≤ 1/P_N(A) for the Convex Distance on S_NTextbook

Motivation

Concentration of measure on the symmetric group concerns random permutations. A uniformly random permutation of $N$ objects appears in random assignment problems, in sampling without replacement, in the longest increasing subsequence and in the analysis of randomized algorithms. A tail bound for a function of a random permutation is useful when it does not require computing the function's distribution. The symmetric group is not a product space, so the inequalities proved for product spaces do not apply to it directly.

Timeline. B. Maurey [Maurey 1979] gave the first concentration inequality on $S_N$ , for distances that count the coordinates in which two permutations differ. Every permutation can be written uniquely as $\sigma=t_{N,i(N)}\circ\cdots\circ t_{2,i(2)}$ with $i(j)\le j$ , where $t_{i,j}$ is the transposition of $i$ and $j$ . Through this decomposition the Hamming bound (2.1.3) for product spaces carries over to $S_N$ . Milman and Schechtman present the result in their monograph [Milman–Schechtman 1986]. In Chapter 5 of his 1995 memoir Talagrand 1995, M. Talagrand proves the analogue on $S_N$ of his convex hull inequality (Theorem 4.1.1 of the memoir). In the author's words, it improves Maurey's result in the way that Theorem 4.1.1 improves Proposition 2.1.1.

Setting

$S_N$ is the group of permutations of $\{1,\dots,N\}$ and $P_N$ is the uniform probability on it. Fix $A\subseteq S_N$ and $\sigma\in S_N$ . A 0–1 vector $s$ is admissible if some $\tau\in A$ agrees with $\sigma$ at every coordinate where $s$ is zero:

U_A(\sigma)=\bigl\{s\in\{0,1\}^N:\ \exists\tau\in A,\ \forall\ell\le N,\ s_\ell=0\Rightarrow\tau(\ell)=\sigma(\ell)\bigr\}.

$V_A(\sigma)\subseteq[0,1]^N$ is the convex hull of $U_A(\sigma)$ , and

f(A,\sigma)=\inf\Bigl\{\sum_{\ell\le N}s_\ell^2:\ s\in V_A(\sigma)\Bigr\}

is the squared convex distance from $\sigma$ to $A$ . Unlike $f_c$ of Chapter 4, $f$ here is already squared. If $\sigma\in A$ , then $0\in U_A(\sigma)$ and $f(A,\sigma)=0$ . A permutation that agrees with some element of $A$ outside $k$ coordinates has $f(A,\sigma)\le k$ .

The proof uses three variants. $f(A,\sigma,p)$ counts coordinate $p$ twice, $s_p^2+\sum_\ell s_\ell^2$ . $f(A,\sigma,p,m)$ , for $p\ne m$ , restricts that infimum to the face $s_m=0$ (Eq. (5.5)). $g(A,\sigma,i,j)$ drops coordinates $i$ and $j$ (Eq. (5.6)). In $S_{N+1}$ , $G_i=\{\sigma:\sigma(i)=N+1\}$ and $G'_i=\{\sigma:\sigma(N+1)=i\}$ , with uniform probabilities $Q_i$ and $Q'_i$ . $t_i$ is the transposition of $N+1$ and $i$ . The maps $R(\rho)=\rho\circ t_i$ and $R'(\rho)=t_i\circ\rho$ send $G_i$ and $G'_i$ , respectively, onto the permutations fixing $N+1$ , that is, onto $S_N$ .

Formalization targets

Goal: Theorem 5.1

For every $N$ and every $A\subseteq S_N$ ,

\int_{S_N}\exp\frac1{16}f(A,\sigma)\,dP_N(\sigma)\le\frac1{P_N(A)}.\tag{5.2}

The constant $1/16$ is the paper's.

Stronger: Proposition 5.2

For every $A\subseteq S_N$ and every $p\le N$ ,

\int\exp\tfrac1{16}f(A,\sigma,p)\,dP_N\le\tfrac1{P_N(A)}\quad(5.3)_N,\qquad\int\exp\tfrac1{16}f(A,\sigma,\sigma^{-1}(p))\,dP_N\le\tfrac1{P_N(A)}\quad(5.4)_N.

Since $f(A,\sigma)\le f(A,\sigma,p)$ , this pair implies Theorem 5.1.

Milestones

The milestones are the numbered results of the induction step from $N$ to $N+1$ , in the order of the paper:

the deterministic inequalities Lemma 5.3 (5.7) and Lemma 5.7 (5.14);
the transfer lemmas Lemma 5.4 (5.8) and Lemma 5.8 (5.15);
the integral bounds Corollary 5.5 (5.10), Lemma 5.6 (5.11), Corollary 5.9 (5.16) and Lemma 5.10 (5.17).

Significance

The result. Theorem 5.1 has the same form as Theorem 4.1.1. By Markov's inequality, $P_N(A)\,P_N\{f(A,\cdot)\ge t\}\le e^{-t/16}$ . Any function on $S_N$ that is controlled by the convex distance therefore concentrates around its median with Gaussian tails whose scale does not depend on $N$ . Because the convex distance weighs coordinates by an arbitrary unit vector, this includes functions that are Lipschitz only in a weighted, configuration-dependent sense, which a Hamming-distance bound does not reach. This is the setting of random permutation problems such as the longest increasing subsequence and the assignment problem.

Formalizing it. The result has been proved since 1995. To the best of current knowledge none of Chapter 5 has a machine-checked proof, and the platform has no concentration statement on $S_N$ . This mission formalizes the statements and the induction of the chapter. Its reusable output is the convex distance on $S_N$ and the embedding of $S_N$ into $S_{N+1}$ through the blocks $G_i$ , $G'_i$ .

Difficulty

$S_N$ sits inside $\{1,\dots,N\}^N$ through $\sigma\mapsto(\sigma(i))_{i\le N}$ . If $S_N$ were the whole product, (5.2) would follow from Theorem 4.1.1. But $S_N$ is a very small subset of that product, and the uniform measure on $S_N$ is not a product measure. The decomposition into transpositions does give a product structure, but it is highly non-commutative. Coordinate distances in the decomposition do not match coordinate distances of the permutations, so it transfers only the weaker Hamming-type bound. The paper notes that a direct induction on $N$ for (5.2) itself apparently fails. The strengthened pair $(5.3)_N$ , $(5.4)_N$ is needed, and its two halves cross: $(5.4)_{N+1}$ is proved from $(5.3)_N$ , and $(5.3)_{N+1}$ from $(5.4)_N$ .

Formalization scope

$S_N$ is Equiv.Perm (Fin N), with indices from $0$ . In $S_{N+1}$ the point $N+1$ is Fin.last N, and composition is the group product, so $\rho\circ t_i$ is ρ * t N i.
$U_A(\sigma)\subseteq\mathbb R^N$ , and $V_A(\sigma)$ is convexHull ℝ. The functionals $f$ , $f(\cdot,\cdot,p)$ , $f(\cdot,\cdot,p,m)$ and $g$ are infima of explicit sums of squares, so the sup norm on Fin N → ℝ plays no role. They take values in $[0,+\infty]$ , so an empty infimum is $+\infty$ and $f(\emptyset,\sigma)=+\infty$ . The integrand $\exp(z/16)$ is computed in EReal, so $\exp(+\infty)=+\infty$ .
The uniform probabilities $P_N$ , $Q_i$ and $Q'_i$ are explicit finite averages over $S_N$ , $G_i$ and $G'_i$ . $Q_i(A)$ means $|A\cap G_i|/|G_i|$ . $1/P_N(A)$ is computed in ℝ≥0∞, so $A=\emptyset$ gives $+\infty$ on both sides.
$R(\sigma)$ and $R'(\sigma)$ enter through the relation Restricts ρ τ ( $\rho(\ell)=\tau(\ell)$ for $\ell\le N$ ). $R(A_i)$ and $R'(A'_i)$ are the corresponding image sets.
The integral bounds 5.5, 5.6, 5.9 and 5.10 are stated in the paper inside the induction step. Each carries the induction hypothesis it uses as an explicit binder: $(5.3)_N$ , $(5.4)_N$ , or "either" as a disjunction.
A trivializing formalization is ruled out. The distance is the convex-hull distance with sums of squares, not a sup norm or Hamming count. The constant $1/16$ is kept, and the infimum over the empty set is $+\infty$ , not a junk $0$ .
Lemma 4.1.3, the numerical inequality used in the Hölder step, belongs to mission V of this series and is not posed again here.

Contributions are welcome at every level: proofs of the deterministic lemmas, the bijections $G_i\to S_N$ and their measure-transport facts, and the final Hölder–Lemma 4.1.3 step.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205, Chapter 5, pp. 144–150. https://doi.org/10.1007/BF02699376
B. Maurey, Construction de suites symétriques, C. R. Acad. Sci. Paris Sér. A 288 (1979), 679–681 (reference [M1] of the memoir; no DOI).
V. D. Milman, G. Schechtman, Asymptotic theory of finite dimensional normed spaces, Lecture Notes in Math. 1200, Springer, 1986. https://doi.org/10.1007/978-3-540-38822-7

11 thms2 active usersReviewed

Graph Theory Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces X: The Chromatic Number of Random Graphs — χ(G(n,p), m) Lies in an Interval of Length k with High ProbabilityTextbook

Motivation

The chromatic number of the random graph $G(n,p)$ is one of the central random variables of probabilistic combinatorics. Its order of magnitude for constant $p$ , $\chi(G(n,p)) \sim n/(2\log_{1/(1-p)} n)$ , was settled by Bollobás ([B], 1988); the question that remains is how much $\chi$ fluctuates around its typical value. Shamir and Spencer ([S-S], 1987) used the edge- and vertex-exposure martingales to show that $\chi(G(n,p))$ lies, with high probability, in an interval of length about $\sqrt n$ , and for sparse graphs $p = n^{-\alpha}$ in an interval of bounded length.

Chapter 9 of Talagrand's 1995 memoir revisits this question as an application of his convex-hull inequality (Theorem 4.1.1 of the paper, posed in a separate mission of this series). The author states the aim plainly: martingale methods require ingenuity on this problem, and the chapter shows that Theorem 4.1.1 gives somewhat better results "in a completely straightforward manner". The chapter also derives, from the same inequality, an upper bound on the probability that $G(n,p)$ has no independent set of a given size — the quantity that drives the greedy colouring bound, previously obtained by Bollobás with martingales and by Janson's correlation inequality.

Timeline. 1987: Shamir–Spencer, concentration of $\chi(G(n,p))$ by martingales. 1988: Bollobás, the asymptotic value of $\chi(G(n,p))$ for constant $p$ , via a martingale bound on independent sets. 1990: Janson's inequality gives a simpler route to the same independent-set bound. 1995: Talagrand, Theorem 9.1 and Proposition 9.2, both from the convex-hull inequality.

Setting

A graph $G$ on the vertex set $V = \{1,\dots,n\}$ is a subset of $E_0 = \{(i,j);\ i<j\}$ . A set $I \subseteq V$ is independent if no two of its points are joined by an edge. For $A \subseteq V$ , the chromatic number $\chi(G,A)$ is the smallest number of independent sets that cover $A$ , that is, the chromatic number of the subgraph induced on $A$ ; $\chi(G,\emptyset) = 0$ . For an integer $m$ ,

\chi(G,m) = \inf\{\chi(G,A);\ \operatorname{card} A = m\}.

Given $0<p<1$ , the random graph $G(n,p)$ contains each possible edge $(i,j)$ with probability $p$ , independently. Concretely, $x = (x_e)_{e \in E_0} \in \{0,1\}^{E_0}$ carries the product of Bernoulli $(p)$ laws and $G(x)$ is the set of $e$ with $x_e = 1$ .

The vertex-exposure space is $\Omega' = \prod_{j} \Omega_j$ with $\Omega_j = \{0,1\}^{j-1}$ : the coordinate $\omega_j = (\omega_{i,j})_{i<j}$ lists the edges from $j$ to earlier vertices, and $G(\omega)$ contains $(i,j)$ iff $\omega_{i,j}=1$ . Changing one coordinate of $\omega$ changes only edges at one vertex.

For an integer $r$ and $e = (i,j) \in E_0$ , $N(G,e)$ denotes the number of independent sets of $G$ of size $r$ containing $i$ and $j$ .

Formalization targets

Goal: Theorem 9.1

For $k \in \mathbb N$ , $m \le n$ and $t>0$ there is an integer $a$ such that

P\big(\chi(G(n,p),m) \in [a-k,a]\big) \ \ge\ 1 - 2e^{-t^2/8} - P\big(\sup\{\chi(G(n,p),F);\ F\subset V,\ \operatorname{card}F \le t\sqrt m\} > k\big).

The integer $a$ depends on $n,p,m,k,t$ . The last term is zero when $k > t\sqrt m$ , so for such $k$ the chromatic number $\chi(G(n,p),m)$ sits in a window of $k+1$ values except on an event of probability $2e^{-t^2/8}$ .

The deterministic step of the proof, Eq. (9.3)

With $A \subseteq \Omega'$ the set of $\omega$ with $\chi(G(\omega),m) \ge a$ and $\sup\{\chi(G(\omega),F);\ \operatorname{card}F \le t\sqrt m\} \le k$ , and

B = \Big\{\omega;\ \forall (\alpha_j) \ge 0,\ \exists \omega' \in A;\ \sum_j \alpha_j 1_{\{\omega_j \ne \omega'_j\}} \le t\sqrt{\textstyle\sum_j \alpha_j^2}\Big\},

every $\omega \in B$ satisfies $\chi(G(\omega),m) \ge a-k$ .

Proposition 9.2 and Eq. (9.7)

The double count $N = \big(r(r-1)/2\big)^{-1}\sum_{e\in E_0} N(G,e)$ of independent $r$ -sets, and, for $u \ge 0$ and $r \ge 2$ , if with probability greater than $1/2$ the graph $G(n,p)$ has an independent $r$ -set and $u\sqrt{\sum_e N(G(n,p),e)^2} \le \sum_e N(G(n,p),e)$ , then

P\big(G(n,p)\ \text{contains no independent set of size } r\big) \le 2\exp\Big(-\frac{u^2}{r^2(r-1)^2}\Big).

Significance

The results. Theorem 9.1 is a two-sided concentration statement for $\chi(G(n,p),m)$ with an explicit Gaussian error $2e^{-t^2/8}$ and no loss in the exponent from a martingale difference bound; for sparse $p = n^{-\alpha}$ , where small vertex sets are sparse enough to be coloured with few colours, it localises $\chi$ to a bounded window. Proposition 9.2 is the independent-set estimate on which the greedy upper bound for $\chi(G(n,p))$ rests, obtained here with the same tool and constants $2$ and $r^2(r-1)^2$ stated on the page.

Formalizing them. All results are proved on paper; none of them, nor any concentration statement for $\chi(G(n,p))$ , is formalized in Lean or on the platform. A formal development gives a machine-checked model of $G(n,p)$ both as an edge product and as a vertex-exposure product, a statement-level check of how the convex-hull inequality transfers to graph functionals, and a corrected form of Proposition 9.2 (see the scope section): the printed hypothesis (9.4) is satisfied vacuously by graphs without independent $r$ -sets, and the formal statement records the hypothesis the proof uses.

Difficulty

The obvious encoding of $G(n,p)$ is the edge product $\{0,1\}^{E_0}$ , and it is the wrong one for Theorem 9.1: changing the edges at one vertex changes up to $n-1$ coordinates, so a Hamming-type control of $\chi(G,m)$ in the edge coordinates gives fluctuations of order $\sqrt{n^2}$ instead of order $\sqrt m$ . The statement is therefore tied to the vertex-exposure product $\Omega'$ , and transporting the law of $G(n,p)$ to $\Omega'$ and handling the "largest integer $a$ " with $P(\chi \ge a) \ge e^{-t^2/8} + b$ are further steps a formal proof must carry out. For Proposition 9.2 a plain Hamming-distance bound in the edge coordinates gives the wrong dependence on the number of independent sets: a graph with many independent $r$ -sets is turned into one with none by adding an edge inside each of them, and since these sets overlap heavily, the Hamming distance to the graphs without independent $r$ -sets is not determined by their number.

Formalization scope

Vertices are Fin n (0-based). $G(n,p)$ is graphOf x for $x : E_0 \to \mathrm{Bool}$ under gnp n p, the product (Measure.pi) of the law $p\,\delta_1 + (1-p)\,\delta_0$ on Bool, with $E_0$ the subtype $\{(i,j) : i<j\}$ ; all sets of this finite space are measurable. Probabilities are Measure.real, so right-hand sides may be negative, as on the page. $\chi(G,A)$ is Mathlib's chromaticNumber of the induced subgraph in ℕ∞; $\chi(G,m)$ is an infimum in ℕ∞, equal to $+\infty$ when $m>n$ , and Theorem 9.1 carries $m \le n$ , implicit on the page, without which it fails. Comparisons with integers are made in WithTop ℤ. The supremum over small sets $F$ is an ℕ∞ supremum over finsets with $\operatorname{card}F \le t\sqrt m$ . The vertex-exposure space has a coordinate $\{0,1\}^j$ for every 0-based vertex $j$ , the trivial one for $j=0$ included, as in the paper's $\prod_{j\le n}\Omega_j$ ; the weights in $B$ are nonnegative, the setting of Lemma 4.1.2.

Proposition 9.2 is stated with three explicit additions: $r \ge 2$ , $u \ge 0$ , and the event of (9.4) intersected with " $G(n,p)$ contains an independent set of size $r$ ". As printed, (9.4) holds for every $u$ whenever $G(n,p)$ almost surely has no independent $r$ -set (both sums are zero), and the conclusion then fails; the proof selects a graph with $N>0$ , which is exactly the added clause.

A formalization in which $\chi(G,m)$ is a real infimum (junk value $0$ on the empty family), in which the Bochner integral replaces probabilities, or in which the coloured set $A$ ranges over all vertices instead of $m$ -subsets would trivialise or change Theorem 9.1; these are ruled out by the definitions above.

Theorem 4.1.1 (the convex-hull inequality) and Lemma 4.1.2 are posed in their own mission and are not repeated here; a complete development needs them on the finite product $\Omega'$ , the identity in law between the edge and vertex-exposure models, and monotonicity and subadditivity of chromatic numbers of induced subgraphs. The vertex-exposure model and the independent-set counts are reusable for other random-graph functionals. Proofs of any milestone, and of the law identity between the two models, are welcome.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376
E. Shamir, J. Spencer, Sharp concentration of the chromatic number on random graphs $G_{n,p}$ , Combinatorica 7 (1987), 121–129. https://doi.org/10.1007/BF02579208
B. Bollobás, The chromatic number of random graphs, Combinatorica 8 (1988), 49–55. https://doi.org/10.1007/BF02122551
S. Janson, Poisson approximation for large deviations, Random Structures & Algorithms 1 (1990), 221–229. https://doi.org/10.1002/rsa.3240010209
N. Alon, J. Spencer, The Probabilistic Method, Wiley, 1992 ([A-S] in the paper). https://doi.org/10.1002/0471722154

5 thms2 active usersReviewed

Analysis Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces V: The Convex Hull Distance — ∫ exp f_α(A,x) dP ≤ P(A)^{−α}Textbook

Motivation

A product probability space $(\Omega^N, P)$ , $P=\mu^{\otimes N}$ , concentrates its mass: a set $A$ of non-negligible measure is "close" to most points. How closeness is measured decides what the statement can be used for. The Hamming distance (Chapter 2 of the paper) counts coordinates in which a point differs from $A$ ; it gives Gaussian concentration, but only for functions that are Lipschitz for one fixed weighting of the coordinates. Chapter 4 of M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces (Publ. Math. IHÉS 81, 1995), introduces the convex hull distance, which controls every weighted Hamming distance at once with weights chosen after seeing the point. This one inequality is what the second half of the paper uses for the longest increasing subsequence, bin packing, suprema of linear forms, the chromatic number of random graphs, the random assignment problem and the travelling salesman problem, and it is the form in which "Talagrand's inequality" is usually quoted in probability and combinatorics.

History (paper, p. 125). The author first proved the deviation inequality of Theorem 13.2 of the paper for symmetric $\pm1$ variables; W. B. Johnson and G. Schechtman extended it, and their one-dimensional lemma (Lemma 4.1.3 here) led to the abstract setting of Theorem 4.1.1. Section 4.2 sharpens the exponent $1/4$ by replacing $f_c^2/4$ with an exactly optimised penalty $f_\alpha$ .

Setting

Let $(\Omega,\mu)$ be a probability space, $N\ge0$ an integer and $P=\mu^{\otimes N}$ on $\Omega^N$ . For $A\subseteq\Omega^N$ and $x\in\Omega^N$ let

U_A(x)=\{(s_i)_{i\le N}\in\{0,1\}^N;\ \exists y\in A,\ s_i=0\Rightarrow x_i=y_i\},

the set of $0$ – $1$ vectors marking a superset of the coordinates in which $x$ differs from some point of $A$ . Let $V_A(x)$ be its convex hull in $\mathbb R^N$ ; it contains $0$ exactly when $x\in A$ . The convex hull distance $f_c(A,x)$ is the Euclidean distance from $0$ to $V_A(x)$ , and the enlargement of $A$ is

A_t^c=\{x\in\Omega^N;\ f_c(A,x)\le t\}

(the superscript $c$ stands for "convexity", not for a complement). For $\alpha\ge0$ and $u\in[0,1]$ put

\xi(\alpha,u)=\alpha(1-u)\log(1-u)-(\alpha+1-\alpha u)\log\Big(\frac{1+\alpha-\alpha u}{1+\alpha}\Big),

and let $f_\alpha(A,x)=\inf\{\sum_{i\le N}\xi(\alpha,s_i);\ s\in V_A(x)\}$ ; it plays the role of $f_c^2(A,x)$ .

Formalization targets

Goal: Theorem 4.2.4

For $\alpha>0$ and every $A\subseteq\Omega^N$ ,

\int\exp f_\alpha(A,x)\,dP(x)\le\frac{1}{P(A)^{\alpha}}.

The constant is exact (no unspecified constants), and the statement holds for every probability space $\Omega$ and every $N$ .

Milestones

Lemma 4.1.2: $x\in A_t^c$ iff for every real $(\alpha_i)$ some $y\in A$ has $\sum\{\alpha_i;\ x_i\ne y_i\}\le t(\sum\alpha_i^2)^{1/2}$ .
Lemma 4.1.3: $\inf_{0\le\lambda\le1}r^{-\lambda}\exp\frac{(1-\lambda)^2}{4}\le2-r$ for $0\le r\le1$ .
Lemma 4.2.1: $\inf_{0\le\lambda\le1}r^{-\lambda\alpha}\exp\xi(\alpha,1-\lambda)=1+\alpha-\alpha r$ for $0<r<1$ .
Lemma 4.2.2: $\xi(\alpha,\cdot)$ is increasing and convex on $[0,1]$ and $\xi(\alpha,u)\ge\frac{\alpha}{2(\alpha+1)}u^2$ .
Lemma 4.2.3: $1+\alpha-\alpha a\le a^{-\alpha}$ and $a+(1-a)\exp\xi(\alpha,1)\le a^{-\alpha}$ .
Eq. (4.2.6): $P(A_t^c)\ge1-P(A)^{-\alpha}\exp\big(-\frac{\alpha t^2}{2(\alpha+1)}\big)$ .
Corollary 4.2.5: for $t\ge\sqrt{2\log(1/P(A))}$ , $P(A_t^c)\ge1-\exp\big(-\frac12(t-\sqrt{2\log(1/P(A))})^2\big)$ .
Theorem 4.3.1 (two-point space, uniform $\mu$ , $\alpha\ge1$ ): $\int\exp\big(\frac{\alpha}{\alpha+1}f_c^2(A,x)\big)\,dP(x)\le P(A)^{-\alpha}$ .

Significance

The result. At $\alpha=1$ , Lemma 4.2.2 gives $\xi(1,u)\ge u^2/4$ , so the goal contains Theorem 4.1.1,

\int\exp\tfrac14f_c^2(A,x)\,dP(x)\le\frac1{P(A)},\qquad P(A_t^c)\ge1-\frac1{P(A)}e^{-t^2/4},

the convex distance inequality itself. For general $\alpha$ it improves the coefficient of $t^2$ from $1/4$ to the optimal $1/2$ (Corollary 4.2.5), and since $\xi(\alpha,1)=\log(1+\alpha)$ grows with $\alpha$ , it simultaneously controls the number of coordinates in which $x$ must be changed to reach $A$ , recovering features of the $q$ -point inequalities of Chapter 3. Every Part II application of the paper rests on Theorem 4.1.1 or on this sharpening.

Formalizing it. All results here are proved in the paper (the goal's proof is "an obvious adaptation" of that of Theorem 4.1.1, by induction on $N$ ). None of them has a machine-checked proof for a general probability space. Theorem 4.1.1 itself is posed on the platform, still open, for finite alphabets and finite sets (Talagrand.Eexp_mul_mass_le_one, Talagrand.mass_mul_mass_le_exp); it is not posed again here. A proof of the goal settles it for arbitrary $\Omega$ and arbitrary measurable $A$ .

Difficulty

The function $x\mapsto f_\alpha(A,x)$ is not a sum of one-coordinate terms, so no tensorization of a one-dimensional inequality applies directly. Bounding $f_\alpha(A,x)$ pointwise by the distance to a single nearby point of $A$ gives only Hamming-type bounds with a fixed weighting, which is exactly what the convex hull distance is designed to beat; the inequality has to hold for the infimum over the whole hull. The one-coordinate estimate the paper uses is the exact identity of Lemma 4.2.1, which leaves no slack. A further obstacle is analytic: $V_A(x)$ is a convex hull in $\mathbb R^N$ of a set indexed by the possibly uncountable set $A$ , and its infima must be compared across dimensions $N$ and $N+1$ .

Formalization scope

$\Omega^N$ is Fin N → Ω; $P$ is Measure.pi (fun _ : Fin N => μ) with IsProbabilityMeasure μ.
$U_A(x)$ is a set of Fin N → ℝ with values in $\{0,1\}$ ; $V_A(x)$ is convexHull ℝ (U A x). The $\ell^2$ norm is written out as $\sqrt{\sum_i s_i^2}$ : Mathlib's norm on Fin N → ℝ is the sup norm.
$f_c$ and $f_\alpha$ take values in $[0,\infty]$ (ℝ≥0∞); both are $+\infty$ when $A=\varnothing$ . $\exp(+\infty)=+\infty$ (EReal.exp), $P(A)^{-\alpha}=+\infty$ when $P(A)=0$ . No real-valued infimum or Bochner integral is used, so no junk value can make a bound hold for free.
$\xi(\alpha,1)=\log(1+\alpha)$ relies on $0\cdot\log0=0$ , which Mathlib's Real.log 0 = 0 provides.
Measurability. The paper ignores measurability (pp. 81–82). Here $A$ and $x\mapsto f_\alpha(A,x)$ are assumed measurable (explicit hypotheses), integrals are ∫⁻, and $P(A_t^c)$ is the measure of an arbitrary set, i.e. its outer probability, as the paper prescribes.
$\alpha>0$ in the goal; $t\ge0$ for the enlargement; $P(A)>0$ in Corollary 4.2.5, where the paper's hypothesis on $t$ is otherwise unsatisfiable. In §4.3, $\Omega=\{0,1\}$ is Bool with PMF.uniformOfFintype.
A trivializing formalization is ruled out: restricting $\Omega$ to a finite type or $A$ to a finite set would give a strictly weaker statement (and the finite case of Theorem 4.1.1 is already posed elsewhere).
Needed infrastructure: convex hulls of $0$ – $1$ vectors and their behaviour under adding a coordinate, Hölder's inequality for ∫⁻, Fubini for Measure.pi on Fin (N+1), and the one-variable calculus of $\xi$ . The definitions module is the substrate the Part II chapters of the paper use; proofs of the one-variable lemmas and of the induction step are welcome independently.
Corollary 4.3.2 is not included: the paper derives it from Theorem 4.3.1 by optimising over $\alpha\ge1$ , which only covers $t\ge2\sqrt{\log(1/P(A))}$ , and the printed range $t\ge\sqrt{\log(1/P(A))}$ is not established on the page.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376

10 thms2 active usersReviewed

Completed

Analysis Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces I: Control by One Point — ∫ e^{t f(A,x)} dP ≤ P(A)^{−α} exp(Nt²(1+1/α)/8) for the Hamming Distance to ATextbook

Motivation

Concentration of measure is the observation that, on a high-dimensional product probability space, any set that is not too small already contains most of the space within a small neighbourhood. For functions of many independent random variables this yields Gaussian-type tail bounds without any explicit computation of the distribution, and these bounds are the working tool behind the analysis of random combinatorial optimisation problems (bin packing, the travelling salesman problem, the longest increasing subsequence, the assignment problem), random graphs, and empirical processes.

M. Talagrand's 1995 memoir Talagrand 1995 develops a family of such inequalities that hold on an arbitrary product of probability spaces and are proved by induction on the number of coordinates. Chapter 2 opens with the simplest instance, control by one point: the distance from $x$ to a set $A$ is measured by the number of coordinates in which $x$ differs from the best single point $y \in A$ . The method of this chapter is the template for every later chapter of the memoir.

Timeline. Bounds of the form (2.2.7) for the Hamming distance were first obtained with martingale (bounded differences) methods, collected in McDiarmid's survey McDiarmid 1989. Talagrand's 1995 memoir gives the induction proof reproduced here, with exponent $-\tfrac2N(k-\sqrt{\tfrac N2\log\tfrac1{P(A)}})^2$ , which the paper notes is exactly the best bound obtained by martingales. Earlier, the isoperimetric inequality on the discrete cube (Harper, 1966) settles the case of the uniform measure on $\{0,1\}^N$ .

Setting

Let $(\Omega,\Sigma,\mu)$ be a probability space and $N \ge 0$ an integer. Points of the product $\Omega^N$ are written $x=(x_1,\dots,x_N)$ , and $P=\mu^N$ denotes the product probability. For a set $A \subseteq \Omega^N$ and a point $x$ , the Hamming distance to $A$ is

f(A,x)=\min\big\{\operatorname{card}\{i\le N:\ x_i\ne y_i\}\ :\ y\in A\big\},

the least number of coordinates that must be changed to move $x$ into $A$ ; it is $+\infty$ when $A$ is empty. Given positive weights $(a_i)_{i\le N}$ , the weighted Hamming distance replaces the count by $\sum\{a_i: x_i\neq y_i\}$ .

Two families of constants appear. The first is

a(t)=\frac12+\frac{e^t+e^{-t}}4 ,

and the second, for $\alpha>0$ and $t>0$ ,

a(\alpha,t)=\frac{\alpha^{\alpha}}{(\alpha+1)^{\alpha+1}}\,\frac{(e^t-e^{-t/\alpha})^{1+\alpha}}{(1-e^{-t/\alpha})(e^t-1)^{\alpha}},

extended by its limit $a(\alpha,0)=1$ ; one checks $a(1,t)=a(t)$ .

Formalization targets

Goal: Corollary 2.2.3

For every measurable $A\subseteq\Omega^N$ , every $\alpha>0$ and every $t\ge0$ ,

\int e^{t f(A,x)}\,dP(x)\ \le\ \frac{1}{P(A)^{\alpha}}\exp\Big(N\frac{t^2}{8}\Big(1+\frac1\alpha\Big)\Big), \tag{2.2.6}

and, when $P(A)>0$ , for every $k\ge\sqrt{\tfrac N2\log\tfrac1{P(A)}}$ ,

P\big(\{f(A,\cdot)\ge k\}\big)\ \le\ \exp\Big(-\frac2N\Big(k-\sqrt{\tfrac N2\log\tfrac1{P(A)}}\Big)^2\Big). \tag{2.2.7}

Milestones, in attack order

Lemma 2.1.2 — for measurable $0\le g\le1$ on $\Omega$ : $\int\min(e^t,1/g)\,d\mu\int g\,d\mu\le a(t)$ .
Proposition 2.1.1 — $\int e^{tf(A,x)}dP\le a(t)^N/P(A)\le e^{t^2N/4}/P(A)$ for $t>0$ , and $P(f(A,\cdot)\ge k)\le e^{-k^2/N}/P(A)$ .
Remark 2.1.3 — the same with the weighted Hamming distance and $\sum a_i^2$ in place of $N$ .
Eq. (2.2.3) — $a(\alpha,t)=\sup_{0\le u\le1}(1+u(e^t-1))(1-u(1-e^{-t/\alpha}))^{\alpha}$ .
Proposition 2.2.1 — $\int e^{tf(A,x)}dP\le a(\alpha,t)^N/P(A)^{\alpha}$ for $t\ge0$ .
Lemma 2.2.2 — $a(\alpha,t)\le\exp\frac{t^2}8(1+\frac1\alpha)$ .

The goal is the weakest statement of the section that is stated with fully explicit, closed-form constants; the milestones are the steps the paper's proof passes through.

Significance

The result. Inequality (2.2.7) shows that if $P(A)$ is bounded below, the set of points at Hamming distance at least $\sqrt{N/2\cdot\log(1/P(A))}+s$ from $A$ has probability at most $e^{-2s^2/N}$ , with no assumption on $\Omega$ or $\mu$ . Applied to $A=\{F\le M\}$ for a function $F$ that changes by at most one when a coordinate changes, it gives concentration of $F$ around its median at scale $\sqrt N$ . The exponential moment bound (2.2.6) is the form that composes with other estimates, and the free parameter $\alpha$ is what makes the constant $2/N$ in (2.2.7) attainable rather than $1/N$ as in (2.1.3).

Formalizing it. The results are classical and fully proved in the paper; they are not available in Mathlib, and no machine-checked proof of them is known. A formalization supplies the one-coordinate inequalities (Lemma 2.1.2 and its $\alpha$ -version) and the induction over $\Omega^{N+1}=\Omega^N\times\Omega$ as reusable components: every later chapter of the memoir (two-point space, penalties, $q$ points, convex hull distance) follows the same induction with a different one-coordinate lemma.

Difficulty

The bound does not follow from a union bound or from independence of coordinates, because $f(A,\cdot)$ depends on all coordinates jointly through an arbitrary set $A$ : changing one coordinate of $x$ changes $f(A,x)$ by at most one, but which point of $A$ is nearest can change completely. A naive coordinate-by-coordinate estimate loses either the dependence on $P(A)$ or a constant factor in the exponent, and the constant $2/N$ in (2.2.7) is the sharp one, so no slack is available. The one-dimensional inequalities (Lemma 2.1.2 and its $\alpha$ -version) are extremal problems over all measurable functions $0\le g\le1$ rather than over numbers, and Lemma 2.2.2 is a two-parameter inequality in which the closed form (2.2.2) is not convenient. On the measure-theoretic side, all integrands take values in $[0,\infty]$ and $f(A,\cdot)$ need not be measurable in general.

Formalization scope

Space. $(\Omega,\Sigma,\mu)$ is an arbitrary measurable space with a probability measure; $\Omega^N$ is Fin N → Ω (0-based coordinates) and $P$ is Measure.pi (fun _ => μ). $\Omega$ is never restricted to a finite or countable set.
Measurability. The paper ignores measurability and states Proposition 2.1.1 with an upper integral and outer probability. Here $A$ carries MeasurableSet A and the map $x\mapsto f(A,x)$ carries an explicit Measurable hypothesis; probabilities of arbitrary sets are Mathlib's outer measure.
Values. Distances are in $[0,\infty]$ (ℝ≥0∞), so $f(\emptyset,x)=+\infty$ ; integrals are lower Lebesgue integrals ∫⁻ in $[0,\infty]$ ; $e^{tz}$ is EReal.exp; $P(A)^{-1}$ and $P(A)^{-\alpha}$ are computed in $[0,\infty]$ , so $P(A)=0$ makes the right-hand sides $+\infty$ .
Constants. $a(\alpha,t)$ is formula (2.2.2) for $t\ne0$ and $1$ at $t=0$ . Every constant ( $1/4$ , $1/8$ , $2/N$ ) is the paper's.
Ruled out. Defining $f$ through a real infimum (whose junk value on $\emptyset$ is $0$ ), or letting $a(\alpha,0)=0/0=0$ , would make several statements false or trivial; neither is done.

Needed infrastructure: Fubini/Tonelli for Measure.pi split as $\Omega^N\times\Omega$ , Chebyshev–Markov for ∫⁻, and one-variable calculus for (2.2.3)–(2.2.5). The one-coordinate lemmas and the induction scheme are reusable in the later missions of this series. Proofs of individual milestones and alternative proofs (for example via martingales for (2.2.7)) are welcome.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/bf02699376
C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, LMS Lecture Note Ser. 141 (1989), 148–188. https://doi.org/10.1017/CBO9781107359949.008
L. H. Harper, Optimal numberings and isoperimetric problems on graphs, J. Combin. Theory 1 (1966), 385–393. https://doi.org/10.1016/S0021-9800(66)80059-5

8 thms2 active usersReviewed

Completed

Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces IV: Control by q Points — ∫ q^{f(A_1,…,A_q,x)} dP ≤ 1/∏ P(A_i)Textbook

Motivation

A recurring phenomenon in probability is concentration of measure: on a product of many probability spaces, a set of non-negligible measure has a neighbourhood that carries almost all of the mass. M. Talagrand's 1995 memoir Concentration of measure and isoperimetric inequalities in product spaces developed a systematic method — induction over the number of coordinates — that yields such statements for several different ways of measuring "how far" a point is from a set. These inequalities underlie sharp tail bounds for combinatorial optimization problems (bin packing, travelling salesman, longest increasing subsequence), for empirical processes, and for spin glasses, and Part II of the memoir develops several of these applications.

This mission formalizes Section 3 of the memoir, Control by q points. In Section 2 the distance from a point $x$ to a set $A$ counts the coordinates of $x$ that a single point of $A$ fails to reproduce (the Hamming distance). Section 3 lets several points cooperate: a coordinate of $x$ is captured if any one of $q$ chosen points agrees with $x$ there. The memoir's introduction (p. 79) presents Theorem 3.1.1 as a much simpler substitute for the isoperimetric inequality of Talagrand's earlier work on sums of independent Banach-space valued random variables (Talagrand, Ann. Probab. 17 (1989), 1546–1570), whose phenomenon "had a major impact in Probability in Banach spaces"; Chapter 13 of the memoir applies it to tails of such sums.

Setting

Let $(\Omega,\mu)$ be a probability space, $N\ge0$ an integer, and $P=\mu^{\otimes N}$ the product probability on $\Omega^N$ . Fix an integer $q\ge2$ ; this is a standing assumption throughout the section. For $x\in\Omega^N$ and points $y^1,\dots,y^q\in\Omega^N$ , coordinate $i$ of $x$ is captured if $x_i\in\{y^1_i,\dots,y^q_i\}$ . For subsets $A_1,\dots,A_q\subseteq\Omega^N$ the $q$ -point control is

f(A_1,\dots,A_q,x)=\inf\big\{\#\{i\le N: x_i\notin\{y^1_i,\dots,y^q_i\}\};\ y^1\in A_1,\dots,y^q\in A_q\big\}\qquad(3.1.1),

the least number of coordinates of $x$ that remain uncaptured when one point is chosen in each $A_j$ . It is a whole number between $0$ and $N$ , or $+\infty$ when some $A_j$ is empty.

For the sharpening of Section 3.2, given $\alpha>1$ , the number $a(q,\alpha)$ is the unique $x>1$ with

x+q\alpha\,x^{-1/\alpha}=1+q\alpha\qquad(3.2.2).

Formalization targets

Goal: Theorem 3.1.1

For all subsets $A_1,\dots,A_q$ of $\Omega^N$ ,

\int q^{f(A_1,\dots,A_q,x)}\,dP(x)\le\frac{1}{\prod_{i\le q}P(A_i)}\qquad(3.1.2),

and in particular, for $A\subseteq\Omega^N$ and $k\ge0$ ,

P(\{f(A,\dots,A,x)\ge k\})\le\frac{1}{q^k\,P(A)^q}\qquad(3.1.3).

The constant is exact: the base of the exponential moment is $q$ itself, and the dimension $N$ does not appear.

Milestones on the way

Lemma 3.1.2: for $1/q\le g\le1$ , $\int g^{-1}\,d\mu\,(\int g\,d\mu)^q\le1$ .
Corollary 3.1.3: for $0\le g_i\le1$ , $\int\min_{i\le q}(q,1/g_i)\,d\mu\prod_{i\le q}\int g_i\,d\mu\le1$ .
Eq. (3.1.6): the two pointwise comparisons between $f$ on $\Omega^{N+1}$ and $f$ on $\Omega^N$ for sections and projections of the sets.

Sharpening (Section 3.2)

Eq. (3.2.2): $a(q,\alpha)$ is well defined.
Eq. (3.2.1): $\int a(q,\alpha)^{f(A_1,\dots,A_q,x)}\,dP(x)\le1/\prod_{i\le q}P(A_i)^\alpha$ for $\alpha>1$ .
Proposition 3.2.1: there is a universal $q_0$ such that for $q\ge q_0$

P(\{f(A,\dots,A,x)\ge k\})\le\Big(\frac{e}{(e-1)\,q\log q}\Big)^k\Big(\frac1{P(A)}\Big)^{q\log q}.

Significance

Theorem 3.1.1 gives an exponential tail for $f(A,\dots,A,x)$ whose rate $q^{-k}$ is independent of the dimension $N$ and of the space $\Omega$ . Applied with a set $A$ of probability at least $1/2$ , it says that outside an event of probability $2^q q^{-k}$ a random point agrees, on all but $k$ coordinates, with one of $q$ points of $A$ . This is the form in which the memoir (Chapter 13) bounds the tail of $\|\sum_{i\le N}X_i\|$ for independent Banach-space valued $X_i$ : taking $A=\{\|\sum_i x_i\|\le a\}$ , on most of the space the sum is controlled by $q$ points of $A$ up to the $k$ largest terms. Proposition 3.2.1 shows the base can be improved from $q$ to order $q\log q$ for large $q$ , and the memoir's example on $\Omega=\{0,1\}$ shows that this is sharp up to a universal constant in the base.

None of these results has a machine-checked proof. A formalization produces reusable Lean infrastructure for the induction method on product measures (sections and projections of subsets of $\Omega^{N+1}$ , Fubini on Measure.pi, one-coordinate functional inequalities) that the other chapters of the memoir — the Hamming distance of Section 2, penalties of Section 3.3, the convex hull distance of Section 4 — share.

Difficulty

The inequality cannot be obtained by a union bound over choices of $q$ points or by a coordinate-wise martingale argument with bounded differences: both lose a factor depending on $N$ , while (3.1.2) has none. The induction on $N$ needs a functional inequality on one coordinate that holds uniformly over $q$ functions at once, with the exact constant $q$ , and the induction step has to pass through the projections $B_i$ of the sets — which, for measurable $A_i$ , need not be measurable. The exact constant $e/((e-1)q\log q)$ in Proposition 3.2.1 additionally requires quantitative control of the root of (3.2.2) as $q\to\infty$ .

Formalization scope

$\Omega^N$ is Fin N → Ω (coordinates $0,\dots,N-1$ ), $P$ is Measure.pi (fun _ => μ) with [IsProbabilityMeasure μ], and $(x,\omega)\in\Omega^{N+1}$ is Fin.snoc x ω.
$f$ is computed as an infimum in ℕ∞, so an empty $A_j$ gives $+\infty$ , not $0$ ; $q^{+\infty}=+\infty$ ; integrals are ∫⁻ and probabilities are in ℝ≥0∞, where $1/0=+\infty$ . Hence the degenerate case $P(A_i)=0$ makes the right sides infinite and cannot trivialize any statement.
The memoir ignores measurability and prints (3.2.1) with an upper integral. The formal statements take the sets measurable and assume $x\mapsto f(A_1,\dots,A_q,x)$ measurable, which is the memoir's stated convention (Section 2.1).
$q\ge2$ is a hypothesis of every statement; in Proposition 3.2.1 the constant $q_0$ is quantified before every other object, so it is universal.
$a(q,\alpha)$ is defined as $\sup\{x>1: x+q\alpha x^{-1/\alpha}\le1+q\alpha\}$ ; that this is the unique root is a milestone, not an assumption.

A complete development needs the induction step over Measure.pi on Fin (N+1) (splitting off the last coordinate), measurability of sections, and the one-coordinate inequalities. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publications Mathématiques de l'IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376
M. Talagrand, A new look at independence, Annals of Probability 24 (1996), 1–34. https://doi.org/10.1214/aop/1042644705
M. Talagrand, Isoperimetry and integrability of the sum of independent Banach-space valued random variables, Annals of Probability 17 (1989), 1546–1570 (reference [T2] of the memoir).
M. Ledoux, The Concentration of Measure Phenomenon, Mathematical Surveys and Monographs 89, AMS, 2001. https://doi.org/10.1090/surv/089

9 thms2 active usersReviewed

Completed

Number Theory Probability Theoretical Computer Science·Captain: mikedeng1

A New Class of Random Number Generators 1: For Prime m = bʳ + bˢ − 1, Every Nontrivial Add-with-Carry Sequence Is Periodic After r Steps, with Period the Order of b mod mResearch Paper

Why add-with-carry generators

Simulation, Monte Carlo integration and randomized algorithms consume long streams of numbers that should behave like independent uniform draws. A deterministic generator with finite state is eventually periodic, so its period is the first figure of merit: a stream cannot be longer than its cycle. G. Marsaglia and A. Zaman, A new class of random number generators (Ann. Appl. Probab. 1 (1991)), introduced the add-with-carry and subtract-with-borrow generators. They keep $r$ machine words plus one carry bit, use only additions or subtractions of words, and still reach periods such as $2^{640}$ when the base $b$ is near $2^{32}$ (p. 465). The paper's mechanism for this is number-theoretic: the generated digits are the base- $b$ digits of a fraction $k/m$ written backwards, so the period of the generator is the period of a repeating base- $b$ expansion, i.e. the multiplicative order of $b$ modulo $m$ .

Generators of this family were used widely in the following decades (Lüscher's RANLUX generator in lattice field theory is built on subtract-with-borrow), and later work showed that they are equivalent to linear congruential generators with modulus $m$ (Tezuka, L'Ecuyer and Couture 1993). This mission treats the add-with-carry generator. A companion mission treats subtract-with-borrow.

Setting

Fix a base $b \ge 2$ and two lags $r$ and $s$ with $0 < s < r$ . A state (or seed vector) is

x = (x_1, x_2, \dots, x_r, c),

where each $x_i \in \{0, 1, \dots, b-1\}$ is a base- $b$ digit and $c \in \{0, 1\}$ is the carry bit. The digit $x_1$ is the oldest one. The add-with-carry map $f$ (p. 465) is

f(x_1, \dots, x_r, c) = \begin{cases} (x_2, \dots, x_r,\ x_{r+1-s} + x_1 + c,\ 0) & \text{if } x_{r+1-s} + x_1 + c < b,\\ (x_2, \dots, x_r,\ x_{r+1-s} + x_1 + c - b,\ 1) & \text{if } x_{r+1-s} + x_1 + c \ge b, \end{cases}

and the generated sequence of a seed $x$ is $x, f(x), f^2(x), \dots$ . Reading off the last digit of each state gives a digit stream $x_1, \dots, x_r, x_{r+1}, x_{r+2}, \dots$ obeying $x_n = x_{n-r} + x_{n-s} + c \bmod b$ , with the carry updated at each step. The two trivial seeds are $(0, \dots, 0, 0)$ and $(b-1, \dots, b-1, 1)$ . The modulus of the generator is

m = b^r + b^s - 1 .

For $0 \le k < m$ and $j \ge 1$ , the $j$ -th base- $b$ digit of $k/m$ after the point is $d_j(k/m) = \lfloor b \cdot (b^{j-1} k \bmod m) / m \rfloor$ . The order $\operatorname{ord}_m(b)$ is the least $p \ge 1$ with $b^p \equiv 1 \pmod m$ , and $b$ is a primitive root of a prime $m$ when $\operatorname{ord}_m(b) = m - 1$ .

Formalization targets

Goal: the period is the order of $b$

Let $m = b^r + b^s - 1$ be prime, and let $x$ be any seed other than the two trivial seeds. Then $f^r(x)$ is a periodic point of $f$ and

\min\{p \ge 1 : f^{p}(f^{r}(x)) = f^{r}(x)\} = \operatorname{ord}_m(b).

This is the italic summary of p. 472 ("whatever the seed vector, except for the two trivial seeds, the add-with-carry and subtract-with-borrow sequences become periodic after a few iterations of the generating function, and the periods are the order of the base $b$ for the appropriate modulus"), with the claim of §4.2 (p. 467) and its proof (p. 468). The goal fixes no particular $b$ , $r$ , $s$ and does not assume that $b$ is a primitive root. When it is, the period is $b^r + b^s - 2$ , the value announced in §2.

Milestones

§4.1 (p. 467): for $\gcd(k, m) = \gcd(b, m) = 1$ , $p > 0$ is a period of the base- $b$ expansion of $k/m$ iff $\operatorname{ord}_m(b) \mid p$ .
§4.1 (p. 467): if $b$ is a primitive root of the prime $m$ , every proper fraction $k/m$ has least period $m - 1$ .
p. 472: $f(x) = x$ iff $x$ is a trivial seed.
p. 472: $f^r(x)$ is periodic for every seed.
§4.2 (p. 468): for every seed other than $(b-1, \dots, b-1, 1)$ and every $C$ , there is $0 \le k < m$ , positive iff the seed is nonzero, with

x_n = d_{C+1-n}(k/m) \qquad (r + 1 \le n \le C).

p. 472, Method 3: $x$ is periodic iff $c = 0$ and $x_r \cdots x_{s+1} \ge x_{r-s} \cdots x_1$ , or $c = 1$ and $x_r \cdots x_{s+1} \le x_{r-s} \cdots x_1$ (digit strings read as base- $b$ integers).
§2 (p. 465): the instance $b = 10$ , $r = 2$ , $s = 1$ , period $108$ .
§7 (p. 477): the instance $b = 6$ , $r = 21$ , $s = 2$ , period $6^{21} + 6^2 - 2$ .

Significance

The result. The goal reduces the period of the generator, a property of a dynamical system on $2b^r$ states, to the multiplicative order of one residue. That is the computation the paper performs in §6 to certify its recommended generators, and it is how one chooses $b, r, s$ : search for primes $m = b^r + b^s - 1$ and check the order of $b$ . Milestone 5 is stronger than the goal. It needs no primality and identifies the whole output stream, not only its period, with the expansion of a fraction. That identification is what later work used to relate carry generators to linear congruential generators with modulus $m$ . Milestone 6 answers the paper's "periodic seed" puzzle: it says exactly which seeds lie on their own cycle.

Formalizing it. The results are proved in the paper, the general §4.1 facts are classical, and the method-specific rules of §4.5 (milestone 6) are stated there without proof. None of it is machine-checked on Prove2Me or, to our knowledge, in Mathlib, which has orderOf and ZMod but no theory of base- $b$ expansions of rationals. The mission produces a checked link from a concrete integer recurrence to modular arithmetic. That link can serve as a template for other carry-based and lagged generators.

Difficulty

The obvious argument says the digit recurrence is linear, so the period divides something like the order of a companion matrix. This fails because of the carry: $f$ is not linear over $\mathbb{Z}/b$ , and the state $(x_1, \dots, x_r, c)$ does not live in a group in any evident way. The link to the order of $b$ modulo $m$ goes through an identity between a finite digit string and a fraction (milestone 5). Stating it with exact indices is itself delicate: the digits run in reverse order, the fraction depends on the string's length, and the trivial seed $(b-1, \dots, b-1, 1)$ , whose digits are those of $m/m = 1$ , has to be excluded.

A second difficulty is the preperiod. A seed need not lie on its own cycle (p. 472), so the period must be measured after the transient. Bounding that transient by $r$ (milestone 4) and characterising the periodic seeds (milestone 6) are separate combinatorial facts about the carry. The paper states the second without proof.

Formalization scope

Representation. All declarations are in namespace CarryRNG.AWC. Lags are a structure Lags with fields r, s and proofs of $0 < s$ and $s < r$ . A state is a structure with digits x : Fin r → Fin b and carry c : Fin 2, so $c \le 1$ holds by typing. Lean index $i$ is the paper's $x_{i+1}$ : x 0 is $x_1$ (the digit the step drops), and the partner digit $x_{r+1-s}$ is index $r - s$ . step is defined directly from the two-case formula of p. 465, not through $k/m$ . The digit stream out is one-based: the seed digits for $n \le r$ , then the last digit of $f^{\,n-r}(x)$ . digit b m k j is the exact integer formula above, used for $j \ge 1$ only.
Period. "The period" is Mathlib's Function.minimalPeriod. It is $0$ at non-periodic points, so the goal's equation with the positive $\operatorname{ord}_m(b)$ also asserts periodicity. A divisibility or inequality form would be vacuous and is not used. For digit sequences, "period $L$ " is stated as " $p > 0$ is a period iff $L \mid p$ ".
Quantifier readings. "With appropriately chosen base $b$ , lags $r$ and $s$ and seed vector $x$ " (p. 465) is read as: $m$ prime and $x$ not a trivial seed, following p. 468 ("Making $m$ a prime ensures this") and p. 472. "After a few iterations" is "after at most $r$ ", the paper's own bound (p. 472), so the goal is stated at $f^r(x)$ . In milestone 5 the fraction $k$ depends on the length $C$ of the finite string, as in the paper's "arbitrarily long finite string". In milestone 8, "for any set of 21 seed digits" is stated at $f^{21}(x)$ for the same reason.
Corrected misprints. p. 465 prints the second trivial seed as "(9, 9, 9)"; the last entry is the carry, so milestone 7 excludes $(9, 9, 1)$ . p. 473, example (a), prints the Method 3 inequalities reversed; milestone 6 follows p. 472, which exhaustive checks on small parameters confirm. p. 478 repeats the die period with "− 1" for "− 2"; milestone 8 quotes p. 477.
Ruled-out trivializations. The goal is not "some period divides $m - 1$ " and not "every orbit is eventually periodic". Both hold for any self-map of a finite set or are vacuous. The trivial seeds are named states, not excluded by an assumption such as $f(x) \neq x$ .
Infrastructure and contributions. Needed: periods of base- $b$ expansions of rationals (milestones 1–2, reusable beyond this mission) and finite-dynamics facts about minimalPeriod along an orbit. Proofs of any milestone are welcome, as are primality and order certificates for milestone 8 as separate lemmas.

Selected references

G. Marsaglia and A. Zaman, A new class of random number generators, Ann. Appl. Probab. 1(3) (1991), 462–480. https://doi.org/10.1214/aoap/1177005878
S. Tezuka, P. L'Ecuyer and R. Couture, On the lattice structure of the add-with-carry and subtract-with-borrow random number generators, ACM Trans. Model. Comput. Simul. 3(4) (1993), 315–331. https://doi.org/10.1145/159737.159749
R. Couture and P. L'Ecuyer, Distribution properties of multiply-with-carry random number generators, Math. Comp. 66 (1997), 591–607. https://doi.org/10.1090/S0025-5718-97-00827-2
M. Lüscher, A portable high-quality random number generator for lattice field theory simulations, Comput. Phys. Commun. 79 (1994), 100–110. https://doi.org/10.1016/0010-4655(94)90232-1

17 thms2 active usersReviewed

Completed

Graph Theory Operations Research·Captain: mikedeng1

Zur allgemeinen Kurventheorie I: Menger's Theorem for Finite Graphs, If No Fewer Than n Points Separate Two Finite Sets P and Q, Then n Disjoint Paths Join P to QResearch Paper

Motivation

Menger's theorem is the oldest of the min–max theorems of combinatorial optimization. It says that the largest number of disjoint paths joining two sets of vertices of a finite graph equals the smallest number of vertices whose removal disconnects them. The max-flow/min-cut theorem of Ford and Fulkerson (1956), the Kőnig–Egerváry theorem on bipartite matchings (1931), Whitney's characterization of $k$ -connected graphs (1932) and the integrality of network-flow polytopes all belong to its family. In operations research it underlies network reliability (how many vertex failures a network survives) and disjoint routing.

Karl Menger proved it in 1927, in a paper on curves. In Zur allgemeinen Kurventheorie (Fund. Math. 10, pp. 96–115) the graph statement is a lemma, Satz δ (p. 101), on the way to characterizing the order of a point of a regular curve by the number of arcs ending there (the subject of mission II of this series).

Timeline.

1927. Menger states Satz β for compact regular one-dimensional spaces and proves its finite case, Satz δ, for finite unions of arcs, by induction on the number of arcs (Menger 1927).
1931. Kőnig observes that one step of the induction, called "offenbar" on p. 102, is in the bipartite case exactly his matching theorem, and supplies it (Kőnig 1931, see the references). Kőnig's 1936 book gives the first complete graph-theoretic proof.
1932. Whitney derives the two-vertex form for $k$ -connected graphs.
1956. Ford and Fulkerson's max-flow/min-cut theorem gives the flow-theoretic proof; Dantzig and Fulkerson connect it to LP duality.

Setting

Let $G$ be a finite simple graph on a vertex set $V$ , and let $P, Q \subseteq V$ be disjoint sets of vertices.

A set $S \subseteq V$ separates $P$ and $Q$ if every walk of $G$ from a vertex of $P$ to a vertex of $Q$ passes through a vertex of $S$ . The set $S$ may contain vertices of $P$ and of $Q$ ; in particular $S = P$ always separates.

$G$ is $n$ -point connected between $P$ and $Q$ ("n-punktig zusammenhängend", p. 100) if no set of fewer than $n$ vertices separates $P$ and $Q$ :

|S| \ge n \quad\text{for every } S \text{ separating } P \text{ and } Q .

A family of $n$ disjoint $P$ – $Q$ paths consists of paths $W_1, \dots, W_n$ of $G$ , each from a vertex of $P$ to a vertex of $Q$ , whose vertex sets are pairwise disjoint, end vertices included.

The degree (Grad) of $G$ is its number of edges. A part of $G$ is a spanning subgraph $H \le G$ ; it is proper if it lacks an edge of $G$ . $G$ is irreducibly $n$ -point connected between $P$ and $Q$ if it is $n$ -point connected and no proper part is. For a separating set $S$ , the side $K_1$ of $S$ towards $P$ is formed by the components of $G - S$ that meet $P - S$ , together with their edges to $S - P$ ; the side $K_2$ towards $Q$ is defined symmetrically.

In Lean these are Menger27.Graphs.Separates, NPointConnected, HasDisjointPaths, IrreduciblyNPointConnected and sidePart.

Formalization targets

Goal: Satz δ (p. 101)

G \text{ is } n\text{-point connected between disjoint } P \text{ and } Q \quad\Longrightarrow\quad G \text{ contains } n \text{ disjoint } P\text{–}Q \text{ paths.}

This is the direction Menger states; the converse (disjoint paths force every separator to be large) is immediate and is not part of the mission.

Milestones: the proof of Satz δ, in the paper's order (pp. 101–102)

A graph $n$ -point connected between $P$ and $Q$ has at least $n$ edges.
If it has exactly $n$ edges, it consists of $n$ disjoint $P$ – $Q$ paths.
It contains an irreducibly $n$ -point connected part $K'$ .
If $K'$ is irreducible and has more than $n$ edges, it has a vertex $s \notin P \cup Q$ on one of its edges.
Through such an $s$ passes a set $S$ of exactly $n$ vertices separating $P$ and $Q$ in $K'$ .
For an $n$ -vertex separating set $S$ with $|S \cap P| = p$ , the side $K_1$ is $(n-p)$ -point connected between $P - S$ and $S - P$ .
$n - p$ disjoint paths in $K_1$ and $n - q$ disjoint paths in $K_2$ (with $q = |S \cap Q|$ ) combine into $n$ disjoint $P$ – $Q$ paths in $G$ .

Significance

The result. Satz δ is the vertex form of Menger's theorem for two sets, from which the other standard forms follow: the two-vertex form, Whitney's theorem, the edge form (through line graphs), Kőnig's theorem (for bipartite $G$ with $P$ , $Q$ the two sides) and, through a standard reduction, integral max-flow/min-cut for unit capacities. Menger used it as the finite step of his theorem on $n$ -legs at points of regular curves.

Formalizing it. The theorem is proved, with many published proofs. Mathlib at the pinned revision has edge connectivity of simple graphs but no vertex separators between sets and no form of Menger's theorem; nothing on Prove2Me states it in set form. The mission produces a statement of Satz δ about Mathlib's SimpleGraph, together with the intermediate claims of Menger's own induction, so that the original argument, including the step Kőnig completed, can be checked. Related posed items on the platform are the two-vertex Whitney theorem Balinski61.Whitney.whitney_theorem (internally disjoint paths between two vertices) and Kőnig's theorem MatousekLP.Integrality.konig; neither is the set form stated here, and neither is proved yet.

Difficulty

The obvious argument, choosing disjoint paths one at a time, fails: a first path chosen badly can block every completion, so the paths must be chosen together. Menger's induction avoids this by passing to an irreducible part and cutting it at an $n$ -vertex separator, but it needs a vertex outside $P \cup Q$ to cut at (milestone 4). When every vertex of the irreducible part lies in $P \cup Q$ the part is bipartite between $P$ and $Q$ , and the claim is then Kőnig's matching theorem rather than an observation; this is the gap of 1927. The gluing step (milestone 7) is also more delicate than on the page: the paths of the two sides must meet the separator only at their ends, which depends on how the sides are cut out.

Formalization scope

Representation. Menger's gewöhnlich eindimensionaler Raum, a finite union of arcs meeting at most in end points, is read as a finite simple graph G : SimpleGraph V with [Fintype V]; $P$ and $Q$ are Finset V. Vertices are the points of $P \cup Q$ and the end and branch points (Menger's punktförmige Stücke); edges are the arcs between them, subdivided so that there are no loops or parallel edges. Subdivision changes neither separation nor the number of disjoint paths, and a separating point inside an arc can be moved to an end of the arc. Menger's degree (the number of arcs between consecutive punktförmige Stücke) becomes the number of edges, which a subdivision only increases; every milestone stays true.

Conventions and explicit readings of the paper's phrases.

Separation is phrased through walks: every walk from $P$ to $Q$ meets $S$ . Separators may meet $P$ and $Q$ .
Disjointness of $P$ and $Q$ ("fremden", p. 100) is a hypothesis of every theorem, not part of the definition. Paths are disjoint including their end points; with $P \cap Q = \emptyset$ every path has an edge.
"Teil" is a spanning subgraph H ≤ G; "echter Teil" is H < G.
"Offenbar enthält K′ ein punktförmiges Stück s …" (p. 102) is read as: a vertex $s \notin P \cup Q$ lying on an edge of $K'$ .
"In K′ − s sind n − 1 Punkte … so dass … S = {s, s₂, … sₙ}" is read as: a separating set of exactly $n$ vertices containing $s$ .
"Besteht aus n Bögen" (milestone 2) is read as: $n$ disjoint $P$ – $Q$ paths covering every edge.
The side $K_1$ is constructed from $G$ , $P$ and $S$ (sidePart G P S), not quantified over; it has no edges at the vertices of $S \cap P$ , matching Menger's $K_1 \subseteq K' - S$ considered between $P - S\cdot P$ and $S - S\cdot P$ .
The subtractions $n - p$ and $n - q$ are exact, since $|S| = n$ .
On p. 101 the induction hypothesis is printed as "Satz γ"; it is Satz δ.

Trivializations ruled out. Forcing separators to avoid $P \cup Q$ , counting internally disjoint or edge-disjoint paths, or allowing two paths to share an end vertex would each change the theorem; none is done. No hypothesis restricts $n$ , and $n = 0$ is the trivial case, not an excluded one.

Needed infrastructure. Walk surgery (prefixes up to the first visit of a set, concatenation, conversion of walks to paths), transfer of walks along SimpleGraph inclusions, and well-founded induction on the number of edges. Separators and disjoint path families between sets are reusable beyond this mission, for Whitney's theorem, Kőnig's theorem and flow integrality. Proofs by any method are welcome, including a proof of the goal through max-flow/min-cut or an independent argument (Göring's) bypassing the milestones.

Selected references

K. Menger, Zur allgemeinen Kurventheorie, Fundamenta Mathematicae 10 (1927), 96–115. https://doi.org/10.4064/fm-10-1-96-115
D. Kőnig, Gráfok és mátrixok, Matematikai és Fizikai Lapok 38 (1931), 116–119 (no DOI; English discussion in Diestel, Graph Theory, §2.1 and §3.3).
H. Whitney, Congruent graphs and the connectivity of graphs, American Journal of Mathematics 54 (1932), 150–168. https://doi.org/10.2307/2371086
L. R. Ford, D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
F. Göring, Short proof of Menger's theorem, Discrete Mathematics 219 (2000), 295–296. https://doi.org/10.1016/S0012-365X(00)00088-1
R. Diestel, Graph Theory, 5th ed., Springer, 2017, §3.3. https://doi.org/10.1007/978-3-662-53622-3

10 thms2 active usersReviewed

Completed

Graph Theory Linear Optimization Operations Research·Captain: mikedeng1

Integer Programming Formulation of Traveling Salesman Problems: The Miller–Tucker–Zemlin Constraints Exactly Describe the Itineraries with at Most p Cities per TourResearch Paper

Why this formulation matters

The traveling salesman problem asks for a shortest closed route through a set of cities. Writing it as an integer program requires linear constraints whose integer solutions are exactly the routes. The assignment constraints (each city entered once and left once) are not enough: their integer solutions include collections of disjoint cycles, called subtours, that never pass through the starting city. Some extra family of constraints must rule these out.

In 1960 C. E. Miller, A. W. Tucker and R. A. Zemlin gave such a family using one auxiliary real variable per city (J. ACM 7(4), 326–329). Their MTZ constraints have polynomially many rows, $n^2-n$ for $n$ cities, whereas the subtour elimination constraints of Dantzig, Fulkerson and Johnson (1954) (Oper. Res. 2(4)) have one row per subset of cities. They also handle a generalization: a salesman who returns to base several times, visiting at most $p$ cities per trip. This is the basic form of a capacitated vehicle routing problem. MTZ-type constraints remain standard in vehicle routing models and in textbook formulations of the TSP. Their linear relaxations are known to be weaker than those of the subtour elimination formulation (Padberg and Sung, 1991).

The paper attributes the model to Tucker and reports five machine experiments with Gomory's all-integer algorithm. The computational part is outside this mission.

Setting

There are $n$ cities $1,\dots,n$ and a base city $0$ . A tour is a succession of visits to cities without stopping at city $0$ . In problem (1) the salesman leaves $0$ , visits each of the $n$ cities exactly once and returns to $0$ , possibly several times, with at most $p$ cities per tour. Formally, an itinerary is a list $I=(T_1,\dots,T_t)$ of tours. Each tour is a nonempty list of cities other than $0$ of length at most $p$ , and each city $1,\dots,n$ occurs exactly once in the concatenation of the tours. The number $t$ of tours is the number of returns to $0$ . Tour $(c_1,\dots,c_k)$ travels the arcs $(0,c_1),(c_1,c_2),\dots,(c_k,0)$ . $a_{ij}(I)$ denotes the number of times $I$ travels the arc $(i,j)$ . For real distances $d_{ij}$ , the length of $I$ is the sum of $d_{ij}$ over the arcs it travels.

Problem (2) has non-negative integer variables $x_{ij}$ ( $0\le i\ne j\le n$ ) and real variables $u_1,\dots,u_n$ :

\min \sum\sum_{0\le i\ne j\le n} d_{ij}x_{ij}\quad\text{s.t.}\quad \sum_{\substack{i=0\\ i\ne j}}^{n} x_{ij}=1\ (j\ge1),\quad \sum_{\substack{j=0\\ j\ne i}}^{n} x_{ij}=1\ (i\ge1),\quad u_i-u_j+p\,x_{ij}\le p-1\ (1\le i\ne j\le n).

When the number of tours $t$ is fixed, the relation $\sum_{i=1}^n x_{i0}=t$ is added. With $t=1$ and $p\ge n$ , (1) is the standard traveling salesman problem.

Formalization targets

Goal: the equivalence of (1) and (2)

For every $n\ge0$ and every $p\ge1$ :

\{\,x : \exists u,\ (x,u)\ \text{feasible for (2)}\,\} \;=\; \{\,a(I) : I \text{ a legitimate itinerary of (1)}\,\},

with $\sum_{i=1}^n x_{i0}$ equal to the number of tours $t(I)$ , and with the $u_i$ in the converse taken to be non-negative integers. In addition, $\sum\sum_{i\ne j} d_{ij}\,a_{ij}(I)$ equals the length of $I$ for all real $d$ . The paper says that (2) "will be shown to be equivalent to (1)". Its "burden of proof" is that the two feasible sets correspond and the two objectives agree, and the goal states exactly that.

Milestones, in the order of the paper's proof

The constraints of (2) force $x_{ij}\in\{0,1\}$ (p. 327).
Along a path $r_0,\dots,r_m$ of non-base cities with all $x_{r_kr_{k+1}}=1$ , $u_{r_0}-u_{r_m}\le-m$ (p. 328).
A feasible $x$ has no cycle that avoids city $0$ , so all tours include city 0 (pp. 327–328).
For $p\ge1$ , no tour of a feasible $x$ visits more than $p$ cities (p. 328).
The converse: $u_i=$ the position of city $i$ in its tour makes $(a(I),u)$ feasible, with $1\le u_i\le p$ (p. 328).
Under $x=a(I)$ the objective of (2) is the distance travelled in (1) (p. 327).
An itinerary with $t$ tours of at most $p$ cities requires $tp\ge n$ (p. 326).

Significance

The result. The theorem justifies using (2) in place of (1). Because the feasible sets match and the objectives agree, an optimal solution of (2) is an optimal itinerary of (1), and the same holds with the number of tours fixed. It also shows that a compact, polynomial-size family of linear inequalities in auxiliary potentials excludes every subtour. The same idea, with the $u_i$ read as loads or arrival times, underlies the standard capacity and time-window constraints of vehicle routing.

Formalizing it. The result is classical and its proof is short, but the paper argues informally. It follows successor chains, treats "a tour" without defining an itinerary, and leaves several steps implicit, including the hypothesis $p\ge1$ and the distinctness of $r_{p+1}$ and $r_1$ . No machine-checked statement of the MTZ equivalence is recorded on the platform. The remaining work is the whole formal proof: the combinatorics that turns a 0/1 matrix with unit row and column sums and no subtours into a list of tours, the converse labelling, and the bookkeeping identity between the two objectives.

Difficulty

The inequalities themselves are elementary. Each milestone about (2) is a short computation with the potentials $u_i$ . The work is in the passage from a feasible matrix $x$ to an itinerary. The successor walk from city $0$ must be shown to terminate at $0$ and to cover every arc of $x$ . The resulting tours must be listed so that their arc counts reproduce $x$ exactly, including the number of arcs leaving $0$ . That number is not constrained directly in (2). It equals $\sum_{i}x_{i0}$ only through a counting argument on the row and column sums. A proof that only shows some itinerary exists does not establish the correspondence the paper claims.

Formalization scope

Cities are Fin (n + 1) with 0 the base city, which is the paper's indexing. The commitments, each also stated in the items' Formalization Notes, are:

An itinerary is a List of tours, each tour a List of cities. The paper's "legitimate itinerary" is read as: every tour nonempty, free of 0, of length at most $p$ ; the concatenation duplicate-free; every city $1,\dots,n$ present.
"A feasible solution to (2) has $x_{ij}$ which do define a legitimate itinerary" is read as $x=a(I)$ , the arc counts of $I$ , together with $\sum_{i=1}^n x_{i0}=t(I)$ ("The number of returns to city 0 is given by $\sum x_{i0}$ "). Arc counts are counts, so $x_{ij}\in\{0,1\}$ is a theorem, not an encoding choice.
"Together with appropriate $u_i$ " is made explicit as the existence of natural-number $u_i$ , following the paper's remark that the $u_i$ may be taken non-negative integers. The labelling $u_i=j$ is a definition.
Problem (2) has no variables $x_{ii}$ . The matrix $x$ is indexed by all pairs and the clause $x_{ii}=0$ encodes their absence. $u_0$ exists in the encoding but appears in no constraint.
$x_{ij}\in\mathbb N$ ("non-negative integers"), $u_i\in\mathbb R$ ("arbitrary real numbers"), and $p-1$ and $p\,x_{ij}$ are computed in $\mathbb R$ .
Added hypothesis $p\ge1$ in the goal and in milestone 4. The paper does not state it, and the claim is false without it: for $n=1$ , $p=0$ , $x_{01}=x_{10}=1$ is feasible for (2) but no itinerary exists.
The distances $d_{ij}$ are arbitrary reals, with no sign, symmetry or triangle condition, as on the page.
Milestone 2 states the exact summed bound $-m$ . The page prints the weaker $j+1-k$ .
Milestone 3 excludes every cycle of $x$ avoiding $0$ . The page argues for the cycle met while following successors from $0$ , by an argument that applies to any such cycle.

Not formalized: the constraint and variable counts and the elimination of $x_{i0},x_{0j}$ "to produce an equivalent problem with $n^2+n$ inequalities and $n^2$ variables" (p. 328), which the paper does not make precise, and the machine experiments (pp. 328–329).

Trivializing readings are ruled out. The goal identifies $x$ with the arc counts of an itinerary, not merely the existence of some itinerary. The hypotheses are satisfiable: for $n=3$ , $p=2$ , the itinerary $[[1,2],[3]]$ with $u=(1,2,1)$ is feasible for (2), while the subtour $x_{01}=x_{10}=x_{23}=x_{32}=1$ is not, for any $u$ . Contributions welcome: proofs of the milestones, a reusable library of "functional digraph with unit in- and out-degree" decompositions, and the optimization corollary (equal optimal values of (1) and (2)).

Selected references

C. E. Miller, A. W. Tucker, R. A. Zemlin, Integer Programming Formulation of Traveling Salesman Problems, Journal of the ACM 7(4), 326–329, 1960. https://doi.org/10.1145/321043.321046
G. Dantzig, R. Fulkerson, S. Johnson, Solution of a Large-Scale Traveling-Salesman Problem, Operations Research 2(4), 393–410, 1954. https://doi.org/10.1287/opre.2.4.393
M. Padberg, T.-Y. Sung, An analytical comparison of different formulations of the travelling salesman problem, Mathematical Programming 52, 315–357, 1991. https://doi.org/10.1007/BF01582894
R. E. Gomory, Outline of an algorithm for integer solutions to linear programs, Bulletin of the AMS 64(5), 275–278, 1958. https://doi.org/10.1090/S0002-9904-1958-10224-4

9 thms2 active usersReviewed

Completed

Discrete Geometry Functional Analysis Graph Theory·Captain: mikedeng1

The Geometry of Graphs and Some of Its Algorithmic Applications 3: The Complete Graph Kₙ Has Isometric Dimension ⌈log₂ n⌉Research Paper

Motivation

An isometric model of a graph assigns vectors to vertices so that vector distances reproduce shortest-path distances exactly. The choice of norm matters: a graph that needs many Euclidean coordinates may admit a smaller realization under a different norm. Linial, London, and Rabinovich used this freedom to study the dimension of graph metrics and related geometric questions in their 1995 paper on graph embeddings (Linial–London–Rabinovich, 1995). The complete graph is the first calibration point for the invariant. Every two distinct vertices are equally far apart, so the question becomes how many pairwise equidistant points an arbitrary real normed space of dimension $d$ can contain.

The answer is a sharp base-two logarithm. It separates the role of dimension from the particular shape of a norm's unit ball. In particular, a cube equipped with the supremum norm supplies many equidistant vertices, while no norm in the same dimension can accommodate more. Establishing both directions gives a reference case for more complicated graph metrics in the paper's Section 5.

Setting

A finite pseudometric space has a finite point set $X$ and a distance $\delta(x,y)\ge0$ that is symmetric, vanishes on the diagonal, and satisfies the triangle inequality. Distinct points may have distance zero, as the paper explicitly allows. A norm $N$ on $\mathbb R^d$ is nonnegative, vanishes only at the zero vector, is absolutely homogeneous, and satisfies the triangle inequality. It induces the distance $N(u-v)$ between vectors.

An isometric embedding of $(X,\delta)$ into a $d$ -dimensional normed space is a map $\varphi:X\to\mathbb R^d$ with $N(\varphi(x)-\varphi(y))=\delta(x,y)$ for every pair. The isometric dimension $\dim(X,\delta)$ is the least $d$ for which such a norm and map exist. The norm may depend on $X$ and $d$ ; it is part of the realization rather than a fixed background choice. Lemma 5.1 of the paper states that every $m$ -point metric space has an isometric realization in $\ell_\infty^m$ , so this least dimension is taken over a nonempty set (Linial–London–Rabinovich, p. 229).

The complete graph $K_n$ has an edge between every pair of distinct vertices. Its shortest-path distance is zero from a vertex to itself and one between distinct vertices. An isometric realization of $K_n$ is therefore a collection of $n$ points whose pairwise distances are exactly one. The paper's Section 5 treats connected graphs, so this mission takes $n\ge1$ . Its convention is that every logarithm has base two.

Formalization targets

Finite metric spaces have a realization

The foundational target is the paper's finite embedding statement:

|X|=m\quad\Longrightarrow\quad (X,\delta)\hookrightarrow\ell_\infty^m.

It establishes the domain on which the least-dimension definition has its intended meaning. The remaining milestones isolate the geometric assertions used for complete graphs: a difference-body inclusion, separation of the interiors of certain convex-hull translates, and a cardinality bound $n\le2^d$ for equilateral points in $\mathbb R^d$ .

Complete graph dimension

The goal is Proposition 5.4 (Linial–London–Rabinovich, p. 231):

\dim(K_n)=\lceil\log_2 n\rceil\qquad(n\ge1).

The lower bound applies to every real norm on $\mathbb R^d$ . The upper bound has the more specific target $K_n\hookrightarrow\ell_\infty^{\lceil\log_2 n\rceil}$ . Both inequalities, including $n=1$ and dimension zero, are part of the mission.

Significance

The equation determines the optimal dimension for an equilateral finite metric space when the norm is unrestricted. It also bounds the size of an equilateral set in every $d$ -dimensional real normed space by $2^d$ , with equality attainable by vertices of a binary cube under the supremum norm. For graph metrics, it gives a precise baseline against which dimension bounds for trees, cubes, and other connected graphs can be compared. The surrounding section of the paper uses the same geometric vocabulary for those other families (Linial–London–Rabinovich, Section 5).

The mathematical result is proved in the 1995 paper. This mission asks for machine-checked Lean proofs of the specified statements. The local declarations presently encode open proof obligations; compilation checks their types and imports, but does not establish the theorems. A completed development would provide a reusable interface for finite isometric dimension and for equilateral configurations under arbitrary finite-dimensional norms.

Difficulty

The easy direction uses points of a binary cube. The difficult direction must hold uniformly over every possible norm, whose unit ball need not be round or smooth. A direct coordinate count cannot assume that vectors have bounded entries in a prescribed basis. The paper formulates its argument through the convex hull of an equilateral configuration and a comparison of translated sets (Linial–London–Rabinovich, p. 231). Its printed volume line also leaves a degenerate case: if that convex hull has zero volume in the ambient space, cancellation of $\operatorname{vol}(D)$ gives no numerical bound. A complete formal proof must account for such configurations without weakening the theorem to full-dimensional sets.

Formalization scope

The Lean representation of $\mathbb R^d$ is the function space Fin d → ℝ. A norm is an explicit function with all norm axioms, including definiteness and absolute homogeneity. Isometric dimension takes the infimum over dimensions admitting such a norm and an exact distance-preserving map. The complete graph is Mathlib's ⊤ : SimpleGraph (Fin n); its graph distance is converted to a real number. This distance is the discrete zero-or-one metric. The lower bound quantifies over every explicit norm. The cube milestone uses the supremum norm on finite real coordinate vectors. Convex hulls and interiors use the standard topology of this finite-dimensional vector space, which every norm induces.

The formal goal assumes $n\ge1$ , matching the paper's connected-graph convention; $n=1$ remains included, with dimension zero. The logarithmic expression is Nat.clog 2 n, the ceiling of the base-two logarithm, rather than a floor or a real logarithm. The source uses no unspecified asymptotic constant in Proposition 5.4 or its listed milestones. The empty point space is allowed in the general finite embedding lemma; its pairwise claim is vacuous, while the nonempty cases carry the intended content. The dimension definition is only used for realizable finite distances, so a totalized infimum's value on an unrealizable function has no role in the target.

The exact norm axioms and exact distance equality prevent shortcuts through seminorms, truncated distances, or a weaker distortion bound. The cardinality theorem retains lower-dimensional affine configurations; assuming positive ambient volume would discard part of the result. A complete development needs finite pseudometric geometry, the supremum norm, convex hulls and interiors, and a dimension-sensitive measure argument. Those components are useful beyond this graph. The paper's independent results on degrees, trees, cubes, and other graph families, as well as algorithmic running-time claims elsewhere in the article, are outside this mission.

Selected references

N. Linial, E. London, and Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2), 215–245 (1995). DOI: 10.1007/BF01200757.

9 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

On the Job-Shop Scheduling Problem: The Integer Program (2)–(7) with 0–1 Variables y_jk Attains Exactly the Minimum Make-SpanResearch Paper

Motivation

The job-shop scheduling problem asks how to time a set of tasks on shared machines so that every product is finished as early as possible. Around 1959 several authors proposed to solve it with Gomory's then new integer programming (Gomory 1958). The obstacle is the noninterference condition: two tasks on the same machine must not overlap, so one of them must finish before the other starts. That is an "either-or" condition. It describes a nonconvex set, and classical linear programming cannot express it.

A. S. Manne's note On the Job-Shop Scheduling Problem (Operations Research 8 (1960) 219–223) writes the either-or condition as two linear inequalities in integers. It adds one 0–1 variable per pair of tasks that compete for a machine, and it uses a large constant derived from a bound $T$ on the start days. This is the origin of the big-M disjunctive formulation, which remains the standard textbook integer program for job shops and, more broadly, the standard way to linearize a disjunction of two linear inequalities.

Timeline. Johnson (1954) introduced the make-span criterion for two- and three-stage production schedules. Bowman (1959) and Wagner (1959) proposed integer programs for machine scheduling. Manne (1960), stimulated by Bowman's paper, gave the formulation stated here. He counted its unknowns as 275 for 5 machines with 10 tasks each, against 600 for Wagner's formulation on the same example (p. 222).

Setting

There are $n\ge1$ tasks and $M$ machines. Task $j$ requires the single machine $\mu(j)$ for $a_j$ consecutive days, where $a_j$ is an integer. An integer horizon $T$ bounds the start days: the integer unknown $x_j\in\{0,1,\dots,T\}$ is the day on which task $j$ begins. A pair $(j,k)$ with $j<k$ and $\mu(j)=\mu(k)$ is a conflicting pair. For each such pair the tasks must not overlap:

x_j-x_k\ge a_k\quad\text{or else}\quad x_k-x_j\ge a_j. \tag{1}

The instance may also impose precedence $x_j+a_j\le x_k$ for given pairs (5a), exact delays $x_j+a_j+\Theta_{jk}=x_k$ for given pairs (5c), and delivery dates $x_j+a_j\le d_j$ for given tasks (6). A schedule is an $x\in\{0,\dots,T\}^n$ satisfying (1), (5a), (5c) and (6). Its make-span is

\operatorname{ms}(x)=\max_{j}\,(x_j+a_j),

the calendar time needed for all jobs when the shop starts on day $0$ .

Manne's integer program has integer unknowns $x_j$ with $0\le x_j\le T$ , one integer $y_{jk}$ for each conflicting pair, and the minimand $t$ , subject to (5a), (5c), (6),

0\le y_{jk}\le 1,\tag{2}

(T+a_k)\,y_{jk}+(x_j-x_k)\ge a_k,\tag{3}

(T+a_j)(1-y_{jk})+(x_k-x_j)\ge a_j,\tag{4}

and $x_j+a_j\le t$ for every $j$ (7). The value $y_{jk}=1$ means that $j$ precedes $k$ ; $y_{jk}=0$ means that $k$ precedes $j$ .

Formalization targets

Goal: the integer program solves the make-span problem

For every instance and every integer $t^\ast$ ,

t^\ast=\min\{t:\ \exists\,x,y\ \text{integer satisfying } 0\le x_j\le T \text{ and } (2)\text{–}(7)\}\iff t^\ast=\min_{x\ \text{schedule}}\operatorname{ms}(x).

Both minima are required to exist. In particular the program has an optimum exactly when a schedule exists. The paper claims this when it says that "the problem now consists of the minimization of $t$ " subject to (2)–(7) (p. 221).

Milestones

Pair equivalence (p. 220). If $|x_j-x_k|\le T$ , some integer $y_{jk}$ satisfies (2)–(4) if and only if (1) holds.
Equal start days are excluded (p. 220). If $x_j=x_k$ and $a_j,a_k>0$ , no $y_{jk}$ satisfies (2)–(4).
Feasibility correspondence (pp. 220–221). For fixed $x$ and $t$ , some $y$ makes $(x,y,t)$ feasible for (2)–(7) if and only if $x$ is a schedule with $x_j+a_j\le t$ for all $j$ .
The $y_{jk}$ must be discrete (p. 222). With $y_{jk}$ real in $[0,1]$ and $0<a_j,a_k\le T$ , conditions (3)–(4) admit $x_j=x_k$ , where (1) fails.
Counting unknowns (pp. 221–222). With $M$ machines of $p$ tasks each, $n=Mp$ and there are $M\,p(p-1)/2$ conflicting pairs; for $M=5$ , $p=10$ this gives $50+225=275$ unknowns.

Significance

The result. The goal certifies that a single integer program, with one binary variable per conflicting pair, computes the optimal make-span of a job shop with precedence, exact delays and delivery dates. The same pattern is used whenever a disjunction $f\ge0$ or $g\ge0$ of bounded linear forms has to be put into a mixed-integer program: a binary variable selects the active branch, and a constant at least as large as the range of the inactive form switches the other branch off. Milestone 1 is that pattern in its simplest form, and milestone 4 shows why the binary variable cannot be relaxed.

Formalizing it. The paper's argument is informal. It rests on a summary table of admissible values of $y_{jk}$ that holds only when the gap $|x_j-x_k|$ is large enough. A machine-checked version fixes the exact hypotheses: integrality of $y_{jk}$ , the bound $|x_j-x_k|\le T$ , and nonemptiness of the task set. To the best of the curators' knowledge, no machine-checked proof of the correctness of the big-M job-shop formulation exists; the definitions here can serve later scheduling missions that need a disjunctive integer program.

Difficulty

The mathematics is elementary, and the difficulty lies in stating it exactly. The obvious reading, "(3)–(4) are equivalent to (1)", is false without the bound $|x_j-x_k|\le T$ . For instance, with $y_{jk}=0$ condition (4) reads $x_j-x_k\le T$ , which cuts off valid orders if start days may lie beyond the horizon. It is also false for real $y_{jk}$ . Equally, "minimize $t$ subject to (7)" equals the maximum of $x_j+a_j$ only after the optimum over $t$ and over $x$ are interchanged and the empty task set is excluded. A naive formalization that states the schedule side as "the least $t$ with (7)" proves nothing about the make-span.

Formalization scope

Tasks are Fin n (the paper's task $j$ is index $j-1$ ), machines Fin M. Start days, durations, horizon, delays, delivery dates, $y_{jk}$ and $t$ are integers (ℤ), so that $x_j-x_k$ and $1-y_{jk}$ are not truncated. Durations are not assumed positive except in milestones 2 and 4, where positivity is necessary. One definitions file, ManneJobShop.Formulation.Model, holds the instance, the conflicting pairs, schedules, the make-span (Finset.sup', so $n\ge1$ is required via [NeZero n]) and the integer program.

Explicit readings of loose phrases:

"a (large) integer $T$ that will constitute a redundant upper bound upon the unknowns $x_j$ " (p. 219): both the schedule problem and the integer program restrict start days to $0\le x_j\le T$ . Redundancy is not assumed.
"The effect of conditions (3) and (4) may therefore be summarized as follows" (p. 220): stated as the equivalence of milestone 1 and the exclusion of milestone 2, not row by row (for $0<x_j-x_k<a_k$ , condition (3) forces $y_{jk}=1$ , not $\{0,1\}$ ).
"the minimization of $t$ " (p. 221): IsLeast of the feasible values of $t$ , matched against IsLeast of the set of make-spans of schedules.
"necessarily of a discrete nature" (p. 222): existence of a real $y_{jk}\in[0,1]$ satisfying (3)–(4) at $x_j=x_k$ when $0<a_j,a_k\le T$ ("large" $T$ read as $T\ge a_j,a_k$ ).
" $m$ possible conflicting pairs of machine assignments" (p. 222): pairs $j<k$ on the same machine, one $y_{jk}$ each.
"If task $j$ is the last task which the shop is to perform upon the item" (p. 221): a delivery date may be attached to any task, which contains the paper's case.

Trivializing formalizations are ruled out: the make-span is a maximum, not a restatement of (7); $y_{jk}$ is an integer; the horizon appears on both sides; the goal is stated for every instance with $n\ge1$ , including infeasible ones. The (5b) example is (5a) for two pairs. Wagner's comparison, the remarks on Gomory's algorithm, Dantzig's secondary constraints and Monte Carlo methods, and the economic discussion of the make-span are not formalized. Proofs of every milestone and of the goal are welcome.

Selected references

A. S. Manne, On the Job-Shop Scheduling Problem, Operations Research 8(2) (1960) 219–223. https://doi.org/10.1287/opre.8.2.219
E. H. Bowman, The Schedule-Sequencing Problem, Operations Research 7(5) (1959) 621–624. https://doi.org/10.1287/opre.7.5.621
H. M. Wagner, An Integer Linear-Programming Model for Machine Scheduling, Naval Research Logistics Quarterly 6(2) (1959) 131–140. https://doi.org/10.1002/nav.3800060205
R. E. Gomory, Outline of an Algorithm for Integer Solutions to Linear Programs, Bulletin of the AMS 64(5) (1958) 275–278. https://doi.org/10.1090/S0002-9904-1958-10224-4
S. M. Johnson, Optimal Two- and Three-Stage Production Schedules with Setup Times Included, Naval Research Logistics Quarterly 1(1) (1954) 61–68. https://doi.org/10.1002/nav.3800010110

7 thms2 active usersReviewed

Completed

Theoretical Computer Science·Captain: xuanji

Deterministic APSP in O(n^2.99791) time on a Word RAMResearch Paper

Motivation

All-pairs shortest paths (APSP) asks for the exact distance between every ordered pair of vertices in an $n$ -vertex weighted directed graph. Floyd–Warshall solves it in $O(n^3)$ time, and for decades no algorithm beat $n^{3-\delta}$ for any constant $\delta>0$ on graphs with polynomially bounded integer weights. The APSP conjecture of fine-grained complexity asserted that none exists. In 2026, Alman and Vassilevska Williams (arXiv:2610.06783) refuted it with a deterministic $O(n^{2.99942})$ algorithm. That bound is the campaign's first entry, and it is formally proved on the platform.

This entry records the deterministic exponent $2.99791$ , obtained by tightening the accounting in the same algorithm.

Setting

The model is the campaign's fixed deterministic word RAM (foundation mission: Truly Subcubic APSP on a Word RAM). A finite program uses add, subtract and multiply modulo $2^W$ , indirect load and store, a sign branch, and accept or reject, on words of width $W \ge b(\log_2 n + 1)$ . Inputs have integer weights of absolute value at most $n^\kappa$ for a fixed $\kappa$ , and there are no negative cycles. The machine has no source of randomness, so randomized (Las Vegas) algorithms do not count.

Formalization target

The goal is the campaign template with the value $2.99791$ :

\texttt{TrulySubcubicAPSP.APSP.SolvedInTime}\ 2.99791,

which says there is a deterministic word-RAM program that solves APSP in $O(n^{2.99791})$ steps.

How the bound arises

The core of the published algorithm is a data structure for thin min-plus-type products with inner dimension $D = N^\varepsilon$ . It has preprocessing $\tilde O(N^2/D^{\Gamma})$ and queries $\tilde O(D^{q})$ , with parameters $c = L/m$ (recursion ratio) and $\theta = t/m$ (switch threshold). Four changes improve the saving $3 - \omega_{\mathrm{APSP}}$ from $0.00058$ to about $0.0021$ :

All-edges Exact Triangle (paper, footnote 10). APSP reduces to all-edges Exact Triangle, and then to min-plus product, by determining $A\star B$ one bit at a time from $\lfloor A/2\rfloor\star\lfloor B/2\rfloor$ with two all-edges calls per bit, followed by repeated squaring. This keeps the whole Exact Triangle saving, where the decision-version route keeps only a third of it.
Exact binomial tail. With $\beta_d = \binom{L}{m-d}9^{L-m+d}$ , Stirling's formula gives a box-preprocessing tail $D^{-\Gamma(c,\theta)+o(1)}$ , where $\Gamma(c,\theta) = \bigl(cH(1/c) - cH((1-\theta)/c) - \theta\ln 9\bigr)/\ln 4$ . This replaces the paper's geometric estimate $\gamma = \theta\ln((c-1)/9)/\ln 4$ .
Pruned encodings. Encoding branches whose prefix holds more than $m$ copies of the distinguished branch $P_0$ are discarded. This lowers the encoding exponent to $A_{\mathrm{pruned}}(c) = \bigl(\tfrac12 cH(1/c) + (c-1)\ln 3\bigr)/\ln 4$ , so the thinness condition becomes $\varepsilon < 1/(A_{\mathrm{pruned}}+\Gamma)$ .
True middle dimension in the deterministic hashing reduction. Take prime size $n^u$ and block size $n^v$ with $u+v=\varepsilon$ , and balance preprocessing, queries and false-positive scanning. The resulting saving is

\delta_{\det} = \varepsilon\min\Bigl\{\frac{\Gamma}{2},\ \frac{1-2q}{3}\Bigr\},\qquad q(\theta) = \frac{H(\theta)+\theta\ln 9}{\ln 4}.

The explicit parameters $c = 21.915$ , $\theta = 0.116107$ and $\varepsilon = 0.055197$ satisfy the thinness condition ( $\varepsilon_{\max} = 0.0551984\ldots$ ) and give $\delta_{\det} = 0.00209524\ldots$ . Since $3 - 0.00209524 < 2.99791$ , the slack absorbs all polylogarithmic factors.

Significance

The randomized version of the same argument reaches about $2.99601$ by repeating random-prime hashing. That bound is out of reach in this deterministic model. Closing the gap between deterministic and randomized collision handling is a natural next target for the campaign.

Selected references

J. Alman and V. Vassilevska Williams, Truly subcubic APSP (2026). https://arxiv.org/abs/2610.06783
T. Kopelowitz, S. Pettie and E. Porat, Higher lower bounds from the 3SUM conjecture, SODA 2016.
Refined exponent accounting (unpublished AI-assisted calculation, October 2026). This is the source of $2.99791$ and has not been peer reviewed.

5 thms2 active usersReviewed

Completed

Graph Theory Linear Optimization Operations Research+1·Captain: mikedeng1

Approximation Algorithms for Scheduling Unrelated Parallel Machines 1: Binary Search over Rounded LP Vertices Finds a Schedule within Twice the Optimal MakespanResearch Paper

Motivation

Scheduling unrelated parallel machines to minimize the makespan, written $R\,\|\,C_{\max}$ , is one of the basic NP-hard problems of scheduling theory. A set of jobs must each be run on one of several machines, and the time a job takes depends arbitrarily on the machine; the goal is to finish all jobs as early as possible. Before the work formalized here, the best polynomial algorithm known guaranteed only a schedule within $2\sqrt m$ times the optimum (Davis and Jaffe, 1981), a factor that grows with the number of machines $m$ .

Lenstra, Shmoys and Tardos (FOCS 1987; CWI Report OS-R8714, 1987; Math. Programming 46, 1990) gave a polynomial algorithm with guarantee $2$ , independent of $m$ . Their tool is a rounding theorem: a vertex of a natural linear-programming relaxation can be rounded to an integral schedule that exceeds each machine's budget by at most one job. The rounding theorem and the binary-search framework around it became standard material in approximation algorithms.

Setting

There are $n$ jobs and $m\ge 1$ machines. If job $j$ is scheduled on machine $i$ , it takes $p_{ij}$ time units, a positive integer. A schedule $\sigma$ assigns every job $j$ to one machine $\sigma(j)$ . The load of machine $i$ is $\sum_{j:\sigma(j)=i}p_{ij}$ , the makespan of $\sigma$ is the largest load, and $\mathrm{OPT}$ is the minimum makespan over all schedules.

For deadlines $d_1,\dots,d_m$ and a threshold $t$ , let $J_i(t)=\{j: p_{ij}\le t\}$ and $M_j(t)=\{i : p_{ij}\le t\}$ . The linear program (LP) has variables $x_{ij}\ge 0$ for $j\in J_i(t)$ and constraints

\sum_{i\in M_j(t)}x_{ij}=1\quad(j=1,\dots,n),\qquad \sum_{j\in J_i(t)}p_{ij}x_{ij}\le d_i\quad(i=1,\dots,m).

The integer program (IP) replaces $d_i$ by $d_i+t$ and requires $x_{ij}\in\{0,1\}$ . A vertex of (LP) is an extreme point of its feasible polytope. The support graph of a point $\tilde x$ is the bipartite graph on machines and jobs with an edge $(i,j)$ whenever $\tilde x_{ij}>0$ .

A $\rho$ -relaxed decision procedure answers, for a deadline $d$ , either 'no' or a schedule, such that (1) every schedule it returns has makespan at most $\rho d$ , and (2) if it answers 'no', no schedule has makespan at most $d$ . The binary search of Lemma 1 starts from the greedy schedule (each job on a machine where it runs fastest), whose makespan $t$ is an upper bound $u$ , with lower bound $l=\lceil t/m\rceil$ , queries the procedure at $d=\lfloor(u+l)/2\rfloor$ , moves $u$ to $d$ on a schedule and $l$ to $d+1$ on 'no', and outputs the best schedule found once $l=u$ .

The LP rounding procedure answers, on deadline $d$ , by solving (LP) with $d_1=\dots=d_m=t=d$ : 'no' if it is infeasible, and otherwise a 0-1 solution of (IP) obtained by rounding a vertex $\tilde x$ chosen by the LP solver, supported on $\tilde x$ .

Formalization targets

Goal: Theorem 2

For every LP solver (every rule choosing a vertex of (LP) when it is feasible), an LP rounding procedure $D$ exists, and for every such $D$ the output $\sigma_D$ of the binary search satisfies

\operatorname{makespan}(\sigma_D)\le 2\cdot\mathrm{OPT}.

Milestones

The support graph of every vertex of (LP) is a pseudoforest: every set $S$ of machines and $T$ of jobs spans at most $|S|+|T|$ edges (§2, p. 4).
In a machine–job pseudoforest, every set of jobs of degree at least $2$ can be matched injectively into the machines (§2, pp. 4–5).
A schedule supported on a feasible $\tilde x$ with at most one fractional job per machine has loads at most $d_i+t$ (§2, p. 5).
Theorem 1 (Rounding Theorem): every vertex $\tilde x$ of (LP) has a schedule $\sigma$ supported on $\tilde x$ with

\sum_{j:\sigma(j)=i}p_{ij}\le d_i+t\qquad(i=1,\dots,m).

Lemma 1: for every $\rho$ -relaxed decision procedure, the binary search outputs a schedule of makespan at most $\rho\cdot\mathrm{OPT}$ .
A schedule with makespan at most $d$ gives a feasible point of (LP) with $d_i=t=d$ (§3, p. 5).
The LP rounding procedure is $2$ -relaxed (§3, pp. 5–6).

Significance

Theorem 2 gives a constant-factor approximation for $R\,\|\,C_{\max}$ that does not depend on $m$ . The same rounding theorem drives the paper's second algorithm, a $(1+\epsilon)$ -approximation for a fixed number of machines using polynomial space, and the paper's lower bound shows that no polynomial algorithm achieves a factor below $3/2$ unless $\mathrm{P}=\mathrm{NP}$ . The Rounding Theorem, in its later form for generalized assignment by Shmoys and Tardos (1993), is a standard tool for LP-based scheduling and assignment.

The result is proved; it has, to our knowledge, no machine-checked proof. The platform contains Matoušek and Gärtner's textbook version (MatousekLP.Scheduling.lst_two_approximation, Theorem 8.3.4 of Understanding and Using Linear Programming), which uses a different relaxation: one bound minimized parametrically over $T$ , optimal solutions with linearly independent columns, and no per-machine deadlines. This mission formalizes the report's own route: deadlines $d_i$ , arbitrary vertices, binary search over a relaxed decision procedure. A formal proof would also yield reusable statements about extreme points of transportation-type polytopes and matchings in pseudoforests.

Difficulty

The obvious rounding, putting each job on a machine where $\tilde x_{ij}$ is largest, can overload a machine by many jobs at once: nothing in feasibility alone prevents many jobs from each placing a small fraction on the same machine. The bound $d_i+t$ requires that each machine receive at most one job that the vertex treats fractionally, and this fails for general feasible points; it holds only because $\tilde x$ is a vertex. The step that carries the weight is therefore a statement about the combinatorial structure of the support of an extreme point, which must be derived from the linear independence of the tight constraints, followed by a matching argument on the resulting graph. Neither step is available in Mathlib in the form needed.

On the algorithmic side, the binary search must be shown to return a schedule within $\rho\cdot\mathrm{OPT}$ although the decision procedure is only approximately correct; the invariants (the lower bound stays below $\mathrm{OPT}$ , the stored schedule stays within $\rho$ times the upper bound) have to be tracked through a recursion.

Formalization scope

Machines are Fin m, jobs Fin n, processing times a matrix P : Matrix (Fin m) (Fin n) ℕ with all entries positive in Lemma 1 and Theorem 2 (the paper's model, p. 2). Loads, makespans and optimal schedules are the published MatousekLP.Scheduling.Schedule definitions applied to the real matrix $(p_{ij})$ ; $\mathrm{OPT}$ is the makespan of a schedule σopt with IsOptimalSchedule.
(LP) is modelled on full $m\times n$ real matrices with the entries $p_{ij}>t$ fixed to $0$ ; this polytope is affinely isomorphic to the paper's, so vertices (Mathlib's Set.extremePoints) correspond exactly. Theorem 1 and its steps are stated for real deadlines and real $t\ge 0$ , more general than the paper's integers; the paper's proof does not use integrality, and mission 2 of this series needs non-integral $t$ .
Algorithmic wording not formalized. Theorem 2 states "a 2-approximation algorithm ... that runs in time bounded by a polynomial in the input size"; Lemma 1 speaks of polynomial procedures; Theorem 1 adds "this rounding can be done in polynomial time". Running time, the ellipsoid method and vertex finding are not formalized. What is formalized is the guarantee the proofs establish: the binary search, written as a Lean function, returns a schedule within $\rho\cdot\mathrm{OPT}$ (Lemma 1, for every $\rho$ -relaxed procedure) and within $2\cdot\mathrm{OPT}$ for every LP rounding procedure and every choice of vertex (Theorem 2).
Explicit constants: the factor $2$ of Theorem 2 and of the $2$ -relaxed procedure, which comes from $d_i+t$ with $d_i=t=d$ ; the overshoot $t$ of Theorem 1; the initial bounds $u=$ greedy makespan and $l=\lceil u/m\rceil$ (the paper's $t/m$ , rounded up because $\mathrm{OPT}$ is an integer); the query point $\lfloor(u+l)/2\rfloor$ .
The LP solver's choice is quantified over by a vertex selector, returning a vertex when (LP) is feasible and nothing otherwise; one always exists, since the polytope is compact.
Trivializing formalization ruled out. "There is a schedule with makespan at most $2\cdot\mathrm{OPT}$ " is trivially witnessed by an optimal schedule; the goal instead bounds the output of the binary search, whose every 'almost' answer must be a rounding of the solver's vertex, supported on it and feasible for (IP).
Needed infrastructure: extreme points of polytopes given by linear constraints and their tight-constraint rank characterization; bipartite pseudoforests and Hall-type matchings; well-founded recursion for the search. Proofs of any milestone, and reusable lemmas on extreme points of assignment polytopes, are welcome.

Selected references

J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, CWI Report OS-R8714, Centre for Mathematics and Computer Science, Amsterdam, 1987 (the source of this mission's statements and numbering); also Proc. 28th IEEE Symposium on Foundations of Computer Science (1987) 217–224
J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271, https://doi.org/10.1007/BF01585745
E. Davis, J. M. Jaffe, Algorithms for scheduling tasks on unrelated processors, Journal of the ACM 28 (1981) 721–736, https://doi.org/10.1145/322276.322284
D. B. Shmoys, É. Tardos, An approximation algorithm for the generalized assignment problem, Mathematical Programming 62 (1993) 461–474, https://doi.org/10.1007/BF01585178
J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer, 2007, §8.3, https://doi.org/10.1007/978-3-540-30717-4

11 thms2 active usersReviewed

Completed

Linear Optimization Operations Research·Captain: mikedeng1

Algorithms for the Assignment and Transportation Problems: Munkres' Algorithm Terminates on Every Real n × n Matrix, and Its Final Starred Zeros Form a Minimum-Sum AssignmentResearch Paper

Motivation

The assignment problem asks how to assign $n$ men to $n$ jobs, one man per job, so that the total cost (or, equivalently, the total rating) is optimal. It is the simplest combinatorial optimization problem with a nontrivial polynomial-time algorithm, and it appears as a subroutine across operations research: in transportation and network-flow methods, in tracking and data association, in scheduling, and as the relaxation behind branch-and-bound methods for the travelling salesman problem.

The algorithm studied here is the one now usually called the Hungarian method or Kuhn–Munkres algorithm.

1931: Kőnig and Egerváry prove the theorem on lines and independent zeros of a matrix that the method rests on.
1955: H. W. Kuhn gives the Hungarian method, with finiteness argued for integer matrices through a decreasing integer sum (Kuhn 1955). M. Flood restates it as Steps A–D.
1957: J. Munkres gives a fully specified version, in which Step B of Flood's outline (find a minimal set of lines containing all zeros and a maximal set of independent zeros) is carried out by an explicit marking procedure with starred and primed zeros. He proves it correct, shows that the integrality assumption is unnecessary, and bounds the work by a polynomial in $n$ (Munkres 1957).

The mission formalizes Munkres' correctness proof for §1 of that paper.

Setting

Let $A=(x_{ij})$ be a real $n\times n$ matrix, $x_{ij}$ being the cost of assigning man $i$ (row $i$ ) to job $j$ (column $j$ ). A set of entries is independent if no two of them lie in the same line (row or column). An assignment is a permutation $\sigma$ , with $\sigma(r)$ the man doing job $r$ . Its cost is $\sum_r x_{\sigma(r)\,r}$ , and $\sigma$ is an optimal assignment if this cost is at most that of every permutation $\tau$ . Choosing $n$ independent entries of minimum sum is the same as choosing an optimal assignment.

The algorithm. A state of the algorithm holds the current matrix, a set of starred zeros $0^*$ , a set of primed zeros $0'$ , a set of covered rows and a set of covered columns. An entry is non-covered, once-covered or twice-covered according as it lies in zero, one or two covered lines.

Preliminaries. Subtract from each row its smallest element, then from each column its smallest entry. Consider the zeros in turn and star each one that has no starred zero in its row or column. Cover the columns containing a $0^*$ .
Step 1. Prime a non-covered zero. If its row contains no $0^*$ , go to Step 2. Otherwise cover its row and uncover the column of that $0^*$ . When no non-covered zero remains, go to Step 3.
Step 2. Build the alternating sequence $Z_0,Z_1,\dots,Z_{2k}$ . It starts at the $0'$ just found. Each $Z_{2i+1}$ is the $0^*$ in the column of $Z_{2i}$ , each $Z_{2i+2}$ is the $0'$ in the row of $Z_{2i+1}$ , and the sequence stops at a $0'$ with no $0^*$ in its column. Unstar its starred zeros and star its primed zeros. Erase all primes, uncover all rows and cover the columns containing a $0^*$ . Stop if all columns are covered; otherwise return to Step 1.
Step 3. Let $h$ be the smallest non-covered element. Add $h$ to each covered row, subtract $h$ from each uncovered column, and return to Step 1 with all marks kept.

The quantity $n_k$ , the maximal number of independent zeros of the matrix $A_k$ , measures progress.

Formalization targets

Goal: correctness of the algorithm

For every real $n\times n$ matrix $A$ :

\exists\,\text{start};\quad \text{every run is finite};\quad \text{no reachable non-final state is stuck};\quad \text{at a final state } \{0^*\}=\{(\sigma(r),r)\}\ \text{with}\ \sum_r x_{\sigma(r)r}=\min_\tau \sum_r x_{\tau(r)r}.

The four clauses are needed together: optimality at final states alone holds for an algorithm that never stops.

Milestones

Remark (2): subtracting row constants $u_i$ and column constants $v_j$ does not change the optimal assignments.
The zeros starred in the Preliminaries are independent.
At Step 2 the sequence $Z_0,\dots,Z_{2k}$ exists, is unique and has distinct elements.
Step 2 leaves an independent set of starred zeros, larger by one.
Lines containing all the zeros number at least the maximal number of independent zeros.
At Step 3 the starred zeros are a maximal independent set and the covered lines a minimal cover.
At Step 3, $h>0$ ; the transformation subtracts $h$ from non-covered entries, adds $h$ to twice-covered ones, keeps every $0^*$ and $0'$ a zero, and $n_{k+1}\ge n_k$ .
If $n_{k+1}=n_k$ , Step 2 does not occur before the next Step 3, which begins with more covered rows.
While $n_k$ is constant, Step 3 is applied at most $n$ times.
Every row and column of the matrix always contains a zero.
Step 3 decreases the sum of the entries by $n(n-n_k)h$ .

Significance

Correctness of the Hungarian method is the basis of a standard algorithm for the assignment problem and, through it, of methods for transportation problems, minimum-cost bipartite matching and weighted bipartite matching. Its $O(n^3)$ refinements remain in practical use. The invariants of the proof are the primal–dual structure of the problem: the row and column constants subtracted along the way form a dual solution, and the starred zeros at the end are a primal solution satisfying complementary slackness.

The result has been proved since 1957 and is in every textbook on combinatorial optimization. A machine-checked version of Munkres' specific procedure, as a transition system with all its free choices, with finiteness for real (not only integer) matrices, is not available on this platform; Mathlib has no assignment algorithm. The mission produces a verified specification of the algorithm, reusable invariants about covers and independent zeros, and a termination argument that does not rely on integrality.

Difficulty

Optimality at termination is short once the invariants are known. The work lies in two places.

First, the invariants hold only along runs. "Each $0^*$ is covered by precisely one line", "no column contains more than one $0^*$ " and "no row contains more than one $0'$ " fail for arbitrary marked matrices, so they must be carried as an inductive invariant through every move, including the Step 3 transformation, which keeps the primes.

Second, termination. The obvious measure, the sum of the entries, decreases by $n(n-n_k)h$ at each Step 3, but for real entries $h$ can be arbitrarily small, so the decreasing sum gives no bound on the number of steps. The page replaces this argument by the stronger result of p. 35 (milestone 8), which holds for real entries. Turning it into a proof that every run of the nondeterministic move relation is finite, including the moves inside Step 1 and Step 2, is the core of the formalization.

Formalization scope

Matrices and positions. Entries are arbitrary reals, as on p. 35. Positions are Fin n × Fin n (row, column).
Output orientation. The output permutation follows the published definition HeldWolfeCrowder_Assignment_Setting: σ r is the row assigned to column r, the starred positions are $(\sigma(r),r)$ , and optimality is IsOptimalAssignment A σ with respect to the original input matrix.
Nondeterminism. The algorithm is an inductive move relation Step. The order in which the Preliminaries consider the zeros, and the non-covered zero primed in Step 1, are free choices. Every claim holds for every run.
Relational steps. Step 2's sequence and Step 3's $h$ are described relationally. Their existence, and $h>0$ , are theorems, not built into the moves.
Reachable states. Invariants are stated for states reachable from a start state, never for arbitrary states.
Finiteness. Finiteness of every run is accessibility (Acc) of each start state for the reversed move relation.
Termination test after the Preliminaries. "If all columns are covered, stop" is also applied when leaving the Preliminaries. The page goes to Step 1 unconditionally there. If the Preliminaries already star $n$ zeros, Step 3 would then have no non-covered element.
Independent zeros. The maximal number of independent zeros is a finite maximum of cardinalities, so it has no junk value.
Edge case $n=0$ . No positivity of $n$ is assumed. For $n=0$ the start state is final.
Ruled out. A goal stating only optimality at final states, or invariants stated for arbitrary states, would be a trivializing formalization; the goal states termination of every run and absence of stuck states as well.

Not formalized: the operation count $(11n^3+12n^2+31n)/6$ of pp. 35–36, whose cost model is informal; the argument that returning to the standard input after Step 3 is unnecessary (pp. 34–35); König's theorem (Remark (1), cited); and §2 on the transportation problem, which is stated without proof.

Welcome contributions: proofs of the milestones, a general library of lines and independent zeros in matrices (reusable for König–Egerváry), and an executable refinement of the move relation.

Selected references

J. Munkres, Algorithms for the assignment and transportation problems, J. Soc. Indust. Appl. Math. 5 (1957), 32–38. https://doi.org/10.1137/0105003
H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2 (1955), 83–97. https://doi.org/10.1002/nav.3800020109
M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974), 62–88. https://doi.org/10.1007/BF01580223 (source of the published assignment-cost definitions reused here)

15 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Efficient Algorithms for Scheduling Semiconductor Burn-In Operations 4: Batch List Scheduling Is Within B + 1 − 1/m of the Optimal Makespan and Has a Bounded Relative Maximum-Lateness ErrorResearch Paper

Motivation

Semiconductor burn-in ovens can process several jobs at once. A group placed in one oven must remain together until the longest job has finished, so increasing batch size saves oven starts but can delay short jobs. When several ovens are available, a scheduler also has to decide which oven receives each batch. Lee, Uzsoy, and Martin-Vega studied this setting and gave guarantees for a simple rule that first groups an arbitrary job list into batches and then sends those batches to the next available oven (Lee, Uzsoy & Martin-Vega 1992, §§2 and 5). Their bounds give a way to assess this easily specified rule against the best possible schedule, even when finding that schedule is difficult.

The paper treats both makespan, the time when all jobs have finished, and maximum lateness, the largest difference between a job's completion time and its due date. These objectives respond differently to batching. The makespan ignores which particular job finishes late; maximum lateness depends on each job's due date. Proposition 4 relates the lateness guarantee to the makespan guarantee of Proposition 1, making the two results a natural formalization unit (Lee, Uzsoy & Martin-Vega 1992, pp. 772–773).

Setting

There are $n>0$ jobs, indexed by $j$ , with processing times $p_j>0$ and due dates $d_j\ge0$ . All jobs are available at time zero. There are $m>0$ identical batch machines, each able to process at most $B>0$ jobs at once. A batch cannot be interrupted or enlarged after it begins, and its processing time is the largest $p_j$ among its members. A schedule partitions the jobs into nonempty batches, chooses a machine for each batch, and orders the batches on each machine. Batches assigned to a machine run one after another from time zero. Every job in a batch finishes when that batch finishes (Lee, Uzsoy & Martin-Vega 1992, p. 766).

For a set of jobs $J$ , write $C_{\max}^*(J)$ for the least makespan over all valid batchings and machine assignments. Write $L^*(J)$ for the least possible value of $\max_{j\in J}(C_j-d_j)$ , where $C_j$ is job $j$ 's completion time. For the full job set, abbreviate these by $C_{\max}^*$ and $L^*$ . The maximum due date over all jobs is $d_{\max}=\max_jd_j$ .

Batch list scheduling (BLS) begins with any ordering of the jobs. It divides successive entries into full batches of $B$ jobs, apart from a possibly smaller final batch. It then assigns each next batch to a machine that becomes available first. Denote the resulting makespan by $C_{\max}^{\mathrm{BLS}}$ and its maximum lateness by $L$ . The guarantee applies to every initial list; it does not require an earliest-due-date or longest-processing-time order (Lee, Uzsoy & Martin-Vega 1992, p. 771, Algorithm BLS).

Formalization targets

Makespan guarantee

Proposition 1 asserts, for every BLS list,

C_{\max}^{\mathrm{BLS}}\le\left(B+1-\frac1m\right)C_{\max}^*.

The milestone list includes the paper's processing-volume lower bound, $\sum_jp_j/(mB)\le C_{\max}^*$ , and Proposition 1 itself. The latter is stated for arbitrary job subsets as well as the full instance, because the paper applies it to a prefix sub-instance in the proof of Proposition 4 (Lee, Uzsoy & Martin-Vega 1992, p. 772).

Relative maximum-lateness guarantee

The mission's goal is the printed ratio of Proposition 4:

\frac{L-L^*}{L^*+d_{\max}} \le B-\frac1m+\frac{d_{\max}}{L^*+d_{\max}}.

The denominator is positive under the stated conditions, even if the optimal maximum lateness is negative. The remaining milestones record the paper's lower bound $L^*(J)\ge C_{\max}^*(J)-d_{\max}$ for a nonempty sub-instance and its reduction from the full instance to the BLS prefix containing a maximum-lateness job (Lee, Uzsoy & Martin-Vega 1992, p. 773).

Significance

The makespan result controls the cost of using an arbitrary initial list and simple next-available-machine assignments instead of optimizing both the batching and machine allocation. At $B=1$ , its factor becomes $2-1/m$ , the ordinary list-scheduling factor noted by the authors. Proposition 4 gives a corresponding bound for maximum lateness, normalized in a way that remains meaningful when $L^*<0$ (Lee, Uzsoy & Martin-Vega 1992, pp. 772–773).

These are proved results in the 1992 paper. The formalization work is to give their batch model, sub-instance optima, and the printed inequalities machine-checked statements and eventually proofs. The imported library already has definitions of least-loaded list scheduling and optimal assignment makespan for ordinary items on identical machines. This mission adds the batch layer, its lateness objective, and the comparison between the batch algorithm and unrestricted batch schedules. The Lean declarations here compile as open theorem targets; this proposal does not claim completed machine-checked proofs.

Difficulty

The processing time of a batch is a maximum, while its contribution to the volume of jobs is a sum. Treating each batch as an ordinary job gives a list-scheduling instance, but it does not by itself compare that instance's optimum with the optimum over all ways to form batches. That gap is central to the makespan bound. The lateness goal has a second obstacle: the job that determines the BLS maximum lateness may sit in a batch that is not the last to finish, and due dates prevent a direct substitution of a makespan bound for a lateness bound. Moreover, $L^*$ may be negative, so dividing by it would not give a valid relative error. The stated normalization and its positivity require explicit attention (Lee, Uzsoy & Martin-Vega 1992, proof of Proposition 4).

Formalization scope

Jobs are Fin n and machines are Fin m; the paper's first job is Lean index zero. Processing times and due dates are real numbers. The paper's integer-data convention is sufficient for these inequalities but is not needed for their statements. Processing times are positive, all jobs are available at time zero, and the lateness goal requires nonnegative due dates. This last condition makes explicit what the paper's final inequality uses: allowing negative due dates makes Proposition 4 false. The full job set is nonempty. Prefix jobs are the first batches of the given arbitrary list, and the optimal values for a prefix range over every valid batching and assignment of those jobs.

The BLS implementation chunks the list into full batches and a final remainder. A batch is sent to a least-loaded machine, which is the first machine to become free when no idle time is inserted. The published list-scheduling definitions of NumStochOpt.ListScheduling supply this rule and the ordinary assignment optimum. They select the lowest machine index on a tie; identical-machine labels do not affect the resulting completion times. Machine schedules are represented by an ordered batch list and an assignment, with each machine processing its own batches back to back. No bound is obtained by defining the optimum over BLS-shaped consecutive batches, and no theorem fixes a favorable job list.

The mission covers correctness inequalities, not the paper's running-time claims or its later BLPT rule. Useful contributions include proofs of the four milestones, finite-schedule facts showing the optima are attained, and reusable links between batch completion times and least-loaded list scheduling. The parallel batch model can also support other objectives and scheduling rules.

Selected references

C.-Y. Lee, R. Uzsoy, and L. A. Martin-Vega, Efficient Algorithms for Scheduling Semiconductor Burn-In Operations, Operations Research 40(4), 764–775, 1992. DOI: 10.1287/opre.40.4.764.

8 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Application of the Branch and Bound Technique to Some Flow-Shop Scheduling Problems 1: Branch and Bound with the Three-Machine Lower Bound Finds a Minimum-Makespan SequenceResearch Paper

Motivation

In a flow shop every job passes through the same machines in the same order. Choosing the order in which jobs enter the shop so that the last job finishes as early as possible (minimizing the makespan) is one of the oldest problems of scheduling theory. For two machines Johnson (1954) gave an exact sorting rule; for three machines his rule is exact only in special cases, and the general problem was later shown to be NP-hard (Garey, Johnson and Sethi, 1976). Exact methods for three or more machines therefore enumerate sequences, and the question is how to enumerate as few of them as possible.

Ignall and Schrage (1965), at the same time as Lomnicki (Operational Research Quarterly, 1965), introduced branch and bound for the three-machine permutation flow shop. Their lower bound, which adds to the time each machine becomes free the work that remains on it and the least work that must follow on later machines, became the template for the machine-based bounds used in flow-shop branch and bound ever since.

Timeline. 1954: Johnson proves the two-machine rule and shows that for three machines a common job order on all machines loses nothing for the makespan. 1960: Land and Doig introduce branch and bound for integer programs. 1965: Ignall–Schrage and Lomnicki apply it to the three-machine flow shop. 1976: Garey, Johnson and Sethi prove the three-machine makespan problem NP-hard, so exact enumeration with good bounds remains the method for exact solutions.

Setting

There are $n\ge1$ jobs and three machines $A$ , $B$ , $C$ . Job $i$ needs time $a_i$ on $A$ , then $b_i$ on $B$ , then $c_i$ on $C$ . Following Johnson, only permutation schedules are considered: a full sequence is a permutation $\sigma$ of the jobs, processed in that order on all three machines, each operation starting as early as possible. Its makespan is the time machine $C$ finishes the last job.

A node $J_r$ is a partial sequence: an ordered list of $r$ distinct jobs. Its unscheduled set $\bar J_r$ is the set of the other $n-r$ jobs. The attributes $\mathrm{TIMEA}(J_r)$ , $\mathrm{TIMEB}(J_r)$ , $\mathrm{TIMEC}(J_r)$ are the times at which machines $A$ , $B$ , $C$ finish the jobs of $J_r$ processed in order. A full sequence begins with $J_r$ when its first $r$ positions are $J_r$ . The lower bound of a node with $\bar J_r\neq\emptyset$ is

LB(J_r)=\max\Big[\mathrm{TIMEA}(J_r)+\sum_{\bar J_r}a_i+\min_{\bar J_r}(b_i+c_i),\ \mathrm{TIMEB}(J_r)+\sum_{\bar J_r}b_i+\min_{\bar J_r}c_i,\ \mathrm{TIMEC}(J_r)+\sum_{\bar J_r}c_i\Big].

The branch-and-bound procedure keeps a list of nodes ranked by $LB$ , starting from the root (no job scheduled). At each step it removes the first node, creates one child per unscheduled job by appending that job, and inserts the children ranked into the list, a new node going before old nodes of equal bound. It stops when the first node of the list is terminal, i.e. has scheduled $n-1$ jobs, so that its last job is forced.

Formalization targets

Goal: the stopping rule certifies an optimal sequence

\exists k:\ \text{the first node of } \mathrm{run}(k) \text{ is terminal},\qquad\text{and}\qquad \text{first node } P \text{ terminal} \ \Longrightarrow\ \mathrm{makespan}(\sigma_P)\le\mathrm{makespan}(\sigma)\ \ \forall\sigma ,

where $\sigma_P$ is $P$ followed by its one unscheduled job. This is the paper's "the problem is solved: that node's sequence is an optimal one" (p. 402), for any real processing times.

Milestones

Validity of the bound (p. 401): $LB(J_r)\le\mathrm{makespan}(\sigma)$ for every $\sigma$ beginning with $J_r$ , $r<n$ .
Exactness at depth $n-1$ (general form of an observation on p. 403): for $r=n-1$ , $LB(J_{n-1})$ equals the makespan of the completed sequence.
Node counts (p. 403): at least $\tfrac12n(n+1)$ nodes are created before stopping, at most $1+n+n(n-1)+\cdots+n!$ are ever created, and the list never holds more than $n!$ nodes.
Dominance (pp. 403–404): if $J_r$ and $I_r$ contain the same jobs, $\mathrm{TIMEA}(J_r)=\mathrm{TIMEA}(I_r)$ ; if also $\mathrm{TIMEB}(J_r)\le\mathrm{TIMEB}(I_r)$ and $\mathrm{TIMEC}(J_r)\le\mathrm{TIMEC}(I_r)$ , replacing $I_r$ by $J_r$ at the beginning of any sequence does not increase its makespan, and $LB(J_r)\le LB(I_r)$ (p. 404).
The 4-job example (pp. 402–403): the run stops after 6 steps with node 231 first, whose bound 62 is the optimal makespan.
The refined bound (p. 409): the strengthened bound used in the paper's computations is still a lower bound.

Significance

The goal is the correctness theorem of the Ignall–Schrage algorithm: best-first search over partial sequences, with a machine-based bound, returns an optimal permutation. Milestone 1 is the bound's validity, which every later machine-based flow-shop bound generalizes; milestone 4 is the dominance rule that justifies discarding nodes; milestone 3 brackets the effort of the search between the best case $\tfrac12n(n+1)$ and full enumeration.

The paper's arguments are short and informal: validity of the bound is asserted with a one-line reason, and optimality at stopping is argued on the example. None of these results has a machine-checked proof. The formalization makes the procedure itself a precise object (list, insertion rule, stopping rule) and turns the paper's claims into statements about it, so that the correctness of the search is proved rather than illustrated.

Difficulty

Each inequality is elementary, but the goal is a statement about an iterated list-manipulating procedure. The obvious argument "the first node has the smallest bound and the bound is valid" needs an invariant that the paper does not state: at every step, every full sequence begins with some node on the list, and the list is sorted. Both must be proved to survive one step of removal and ranked insertion. Termination is likewise not stated: it needs a measure that strictly decreases, for instance the set of nodes that remain to be created, which requires showing that no node is created twice. A tempting shortcut, proving optimality only among the sequences whose nodes were created, is not the theorem.

Formalization scope

Jobs are Fin n (the paper's job $i$ is $i-1$ ), processing times are arbitrary reals with no sign condition, and full sequences are Equiv.Perm (Fin n). The makespan is the machine- $C$ completion time of Johnson's as-soon-as-possible schedule, taken from the published definition JohnsonFlowShop.ThreeStage.asapSchedule. Nodes are lists of jobs, and the node attributes are the same recursion folded over the list. Minima over $\bar J_r$ are Finset.inf'; on an empty set the auxiliary minimum returns a placeholder $0$ that no statement evaluates.

Explicit readings of the paper's phrases:

"is a lower bound … for any node that emanates from node $P$ " is " $\le$ the makespan of every permutation whose first $r$ positions are $J_r$ ";
"a node that has scheduled all $n$ jobs" is read as a node with $n-1$ jobs, whose sequence is completed by the forced last job. The example (stop at node 231 of a 4-job problem), the node counts and the formula for $LB$ all require this reading;
"the problem is solved: that node's sequence is an optimal one" is termination together with optimality over all $n!$ permutations;
"cannot be hurt by replacing $I_r$ with $J_r$ " compares the completions of $J_r$ and $I_r$ by the same ordering of the remaining jobs;
children are inserted one at a time in increasing job index, each before every node with an equal bound; this reproduces the paper's LIST table;
dominance discarding is not part of the procedure in the goal.

A formalization in which the optimality claim ranges only over sequences the run created, or one that asserts optimality without termination, would be trivial or vacuous and is ruled out by the goal's statement.

Not formalized: the reduction from general schedules to permutation schedules (Johnson's Lemma 3, proved on the platform as JohnsonFlowShop.ThreeStage.same_ordering_dominant), the dominance bookkeeping and its percentages, the two-machine mean-completion problem (a separate mission of this series), the computational tables, and the TIMEB/TIMEC columns of the example's LIST table. No platform item treats flow-shop lower bounds or branch and bound over sequences; the nearest branch-and-bound mission, BiconvexProg.BranchBound (Al-Khayyal and Falk), concerns biconvex programs and is unrelated.

The lemmas a solver will want (the invariant of the list, monotonicity of the completion recursion in its start times, validity of the bound) are reusable for the two-machine mission and for any other machine-based bound. Proofs of the milestones, and of the goal from them, are welcome in any order.

Selected references

E. Ignall and L. Schrage, Application of the branch and bound technique to some flow-shop scheduling problems, Operations Research 13(3), 400–412, 1965. https://doi.org/10.1287/opre.13.3.400
S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1), 61–68, 1954. https://doi.org/10.1002/nav.3800010110
A. H. Land and A. G. Doig, An automatic method of solving discrete programming problems, Econometrica 28(3), 497–520, 1960. https://doi.org/10.2307/1910129
M. R. Garey, D. S. Johnson and R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117

13 thms2 active usersReviewed

Operations Research·Captain: mikedeng1

Sequencing Jobs to Minimize Total Weighted Completion Time Subject to Precedence Constraints 1: The Series-Parallel Algorithm Returns an Optimal SequenceResearch Paper

Motivation

Sequencing jobs on one machine to minimize the total weighted completion time $\sum_j w_jC_j$ is one of the basic problems of scheduling theory. Without precedence constraints it is solved by Smith's ratio rule (1956): sequence the jobs in nonincreasing order of $w_j/p_j$ . With arbitrary precedence constraints the problem is NP-hard, as Lawler shows in the same report. Between these two extremes lies the class of series parallel precedence constraints, which covers chains, rooted trees and their nested combinations, and which is exactly the class that can be assembled from single jobs by "all of this before all of that" and "this independently of that".

Lawler's report (IRIA-LABORIA No. 205, 1976; Annals of Discrete Mathematics 2, 1978) gives an $O(n\log n)$ algorithm for this class, once a decomposition of the constraints is known. It is the standard reference for the polynomial case of $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ .

Timeline.

1956, Smith: the ratio rule, no precedence constraints.
1964, Conway, Maxwell and Miller: parallel chains with unit weights.
1971–1973, Baker, Horn, Adolphson and Hu: rooted trees, in $O(n\log n)$ .
1975, Sidney: job modules and $\rho$ -maximal initial sets, for arbitrary precedence constraints, without an efficient method to find them.
1976/1978, Lawler: series parallel constraints in $O(n\log n)$ ; NP-completeness for arbitrary constraints.

Setting

There are $n$ jobs, forming a finite set $N$ , to be processed by a single machine. Precedence constraints are given by an acyclic digraph $G=(N,A)$ : job $i$ must precede job $j$ if there is a directed path from $i$ to $j$ . Job $j$ has a processing time $p_j>0$ and a real weight $w_j$ (of either sign). A feasible sequence lists every job once and never puts a job before one that must precede it. The machine starts at time $0$ without idle time, so the completion time $C_j$ of job $j$ is the sum of the processing times of $j$ and the jobs before it. The cost of a sequence is $\sum_{j\in N} w_jC_j$ , and an optimal sequence is a feasible sequence of minimum cost.

A transitive series parallel digraph is built from single nodes by series composition $(N_1\cup N_2,\ A_1\cup A_2\cup N_1\times N_2)$ and parallel composition $(N_1\cup N_2,\ A_1\cup A_2)$ of digraphs on disjoint node sets. $G$ is series parallel if its transitive closure is transitive series parallel. A decomposition tree records such a construction: its leaves are the jobs, and its internal nodes are marked $S$ (left son before right son) or $P$ .

Sidney's theory works with three notions. A nonempty $M\subseteq N$ is a module if every job outside $M$ must precede all of $M$ , must follow all of $M$ , or is unconstrained with respect to all of $M$ . A subset $I\subseteq M$ is an initial set of $M$ if it contains, with each of its jobs, every job of $M$ that must precede it. With

\rho(I)=\frac{\sum_{j\in I}w_j}{\sum_{j\in I}p_j},

an initial set $I^*$ is $\rho$ -maximal if $\rho(I^*)\ge\rho(I)$ for every initial set $I$ of $M$ .

A composite job is a sequence of jobs treated as one job whose weight and processing time are the sums over its jobs. Lawler's algorithm works bottom-up on the decomposition tree and represents an optimal sequence for each node's module as a set of composite jobs: a leaf gives its job, a $P$ -node the union of its sons' sets, and an $S$ -node the output of the series procedure (Steps 1–3, p. 11), which absorbs elements of $M_1$ and $M_2$ into a composite job $k=(i,k)$ or $k=(k,j)$ until the ratios separate.

Formalization targets

Goal: the algorithm is correct

For a decomposition tree $T$ of $G$ and any run of the algorithm on $T$ producing the set $F$ of composite jobs, every arrangement $L$ of $F$ in nonincreasing ratio order, with each composite job expanded into its sequence, is an optimal sequence:

\operatorname{flatten}(L)\ \text{is an optimal sequence for } N .

Ties, both in the algorithm's choice of minimal and maximal elements and in the final sort, may be broken arbitrarily.

Milestones

Subtrees are modules (p. 7): the leaves of any subtree of a decomposition tree form a module.
Theorem 1 (p. 7): an optimal sequence for a module extends to an optimal sequence for $N$ in which the module's jobs keep their order.
Existence (Definition 3, p. 8): every module has a $\rho$ -maximal initial set.
Theorem 2 (p. 8): for a $\rho$ -maximal initial set $I$ of a module $M$ , some optimal sequence for $N$ runs $I$ consecutively, before all other jobs of $M$ .
Ratio order (p. 10): composite jobs in nonincreasing ratio order cost no more than in any other order.
Parallel composition (p. 10): the union of two representing sets represents the parallel composition.
Series composition, separated ratios (p. 10): if every ratio in $M_1$ exceeds every ratio in $M_2$ , the union represents the series composition.
Series composition, Steps 1–3 (pp. 10–11): the output of the series procedure represents the series composition.

A companion theorem states that the algorithm always has a run.

Significance

The result places $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ with series parallel constraints in polynomial time. Sidney's module and $\rho$ -maximal initial set machinery, which it uses, is the decomposition later used in approximation algorithms for general precedence constraints; Theorems 1 and 2 hold for arbitrary acyclic constraints.

The algorithm and Sidney's theorems are proved in the literature; none of them has a machine-checked proof. The report proves Theorems 1 and 2 by citation to Sidney's 25 lemmas and argues the algorithm's correctness informally in a few paragraphs. A formal development supplies the missing invariants (what exactly is preserved at each node of the tree) and checks that arbitrary tie-breaking is harmless.

Difficulty

The algorithm's correctness rests on an invariant the page states only in passing: that composite jobs behave as single jobs. Read literally, "nonincreasing ratio order is optimal for $M_1$ and for $M_2$ " does not imply the same for their parallel composition. A composite job of two unconstrained jobs can be optimal on its own module yet blocks a better interleaving once another module is added. The invariant that makes the induction go through is that every composite job is a $\rho$ -maximal initial set of itself, and the series procedure must be shown to preserve it while merging. The second difficulty is Theorems 1 and 2 themselves: exchange arguments over sequences of a whole module, with real weights of either sign, under arbitrary acyclic constraints.

Formalization scope

Jobs have a type $\iota$ with decidable equality; $N$ is a Finset ι; the arcs are a relation G : ι → ι → Prop with endpoints in $N$ , acyclic in the sense that no job reaches itself by a path, and "must precede" is Relation.TransGen G. Processing times are positive on $N$ , weights are arbitrary reals. The objective and optimality are the published SingleMachinePrec.Biclique.WeightedCompletion; feasibility is checked against the arcs of $G$ , which for a sequence listing each job once is the same as against its paths. "Optimal for $M$ " uses the job set $M$ .

The decomposition tree is an inductive SPTree with leaves, $S$ -nodes and $P$ -nodes. It is tied to $G$ by three hypotheses: its leaves are distinct, they are exactly $N$ , and on $N$ the transitive closure of $G$ equals the arc relation of the transitive series parallel digraph the tree builds. Composite jobs are lists of jobs, sets of composite jobs are lists of lists, and their ratio is $\sum w/\sum p$ over the list. The algorithm is an inductive relation (Run, SeriesMerge, SeriesLoop), so every tie-breaking is a run. The dummies of ratio $\pm\infty$ in Step 1 become vacuous conditions on empty sets.

Committed conventions and disclosed deviations:

Lean evaluates $0/0=0$ , so $\rho(\emptyset)=0$ ; $\rho$ -maximality compares nonempty initial sets only and requires the maximal set to be nonempty, and composite jobs are nonempty.
Modules use the disjunction of (4.1)–(4.3); for acyclic $G$ and nonempty $M$ this is the page's "exactly one".
"Represents an optimal sequence" includes the composite invariant (every nonempty proper prefix has ratio at most the whole). Without it the parallel and series milestones are false.
In the parallel and series milestones, $M_1$ , $M_2$ and $M_1\cup M_2$ are assumed to be modules, as on the page (the sons of a node of the decomposition tree and the node itself). Without this, a path through a job outside $M_1\cup M_2$ could constrain two of its jobs while feasibility on $M_1\cup M_2$ does not see it, and the series milestone would be false.
The introduction's "nondecreasing order of the ratios" (p. 1) is a slip for the nonincreasing order used in §5; the formalization uses nonincreasing.

The goal assumes nothing about modules, Theorem 2 or subtrees, only the tree, the data and a run, and the companion theorem shows that runs exist, so the goal is neither trivial nor vacuous.

Needed infrastructure: exchange arguments for $\sum w_jC_j$ on lists, restriction of sequences to modules, induction over decomposition trees. Theorems 1 and 2 and the ratio-order lemma are reusable in any $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ development. Proofs of any milestone, and of the goal from the milestones, are welcome.

Selected references

E. L. Lawler, Sequencing jobs to minimize total weighted completion time subject to precedence constraints, IRIA-LABORIA Rapport de Recherche No. 205, December 1976. https://hal.science/hal-04716371v1. Journal version: Annals of Discrete Mathematics 2 (1978), 75–90. https://doi.org/10.1016/S0167-5060(08)70323-6
J. B. Sidney, Decomposition algorithms for single-machine sequencing with precedence relations and deferral costs, Operations Research 23 (1975), 283–298. https://doi.org/10.1287/opre.23.2.283
W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3 (1956), 59–66. https://doi.org/10.1002/nav.3800030106
J. Valdes, R. E. Tarjan, E. L. Lawler, The recognition of series parallel digraphs, SIAM Journal on Computing 11 (1982), 298–313. https://doi.org/10.1137/0211023

11 thms2 active usersReviewed

Operations Research Probability·Captain: mikedeng1

Subadditive Ergodic Theory 6: The Ulam–Hammersley Constant of the Longest Increasing Subsequence Satisfies (8/π)^{1/2} ≤ c ≤ δ^{1/2} + δ^{−1/2}Research Paper

Motivation

Ulam asked, in the early 1960s, how long the longest increasing subsequence of a random permutation typically is. The question is a test case for a whole class of problems in combinatorial probability: a quantity defined by an optimisation over exponentially many configurations (here, all subsequences) whose typical size has to be found without enumerating them. The same structure appears in last-passage percolation, in the patience-sorting card game, in sequence comparison, and in scheduling problems where the longest chain of a random partial order determines a makespan.

J. F. C. Kingman's IMS Special Invited Paper Subadditive ergodic theory (Ann. Probab. 1 (1973), 883–899) presents Ulam's problem in §2.4 as an application of the subadditive ergodic theorem, following J. M. Hammersley, and then proves explicit bounds on the limiting constant. This mission formalizes those bounds.

Timeline.

Ulam (1961) raised the question and conjectured, from simulations, that the typical length grows like a constant times $\sqrt n$ .
Erdős and Szekeres (1935) had already shown deterministically that every permutation of $n$ elements has an increasing or a decreasing subsequence of length at least $\sqrt n$ .
Hammersley (A few seedlings of research, Proc. Sixth Berkeley Symp. 1 (1972), 345–394) proved, by embedding the permutation in a planar Poisson process and applying a subadditivity argument, that $n^{-1/2}$ times the length converges in probability to a constant $c$ , and showed $\tfrac12\pi\le c\le e$ .
Kingman (1973), the paper of this mission, refined the bounds to $(8/\pi)^{1/2}\le c\le\delta^{1/2}+\delta^{-1/2}$ , that is $1.59<c<2.49$ .
Logan and Shepp (1977) and Vershik and Kerov (1977) later identified the constant exactly. That later work is not part of this mission.

Setting

Let $\mathcal S_n$ be the group of permutations of $\{1,2,\dots,n\}$ . For $\sigma\in\mathcal S_n$ , a sequence of positions $1\le i_1<i_2<\dots<i_k\le n$ is ascending if $\sigma(i_1)<\sigma(i_2)<\dots<\sigma(i_k)$ . The length of the longest ascending sequence, $l(\sigma)$ , is the largest such $k$ .

The uniform distribution on $\mathcal S_n$ gives each of the $n!$ permutations probability $1/n!$ , so an event $A\subseteq\mathcal S_n$ has probability $P\{A\}=|A|/n!$ . Let $\pi_n$ denote a permutation drawn from this distribution. The sequence $n^{-1/2}\,l(\pi_n)$ converges in probability to a real number $c$ if, for every $\varepsilon>0$ ,

P\{|n^{-1/2}\,l(\pi_n)-c|>\varepsilon\}\to0\qquad(n\to\infty).

For integers $k\ge1$ , $\nu_k(\sigma)$ denotes the number of ascending sequences of length $k$ in $\sigma$ . For $0<\alpha<b$ write

E(\alpha,b)=2\alpha+(b-\alpha)\log(b-\alpha)-\alpha\log\alpha-b\log b ,

the exponent appearing in Kingman's condition (2.4.8). (The paper calls the second variable $\beta$ ; in Lean it is $b$ , because $\beta$ also names the constant below.)

Formalization targets

Goal: Theorem 8

Let $c$ be the limit in probability of $n^{-1/2}l(\pi_n)$ . Let $\delta$ be the unique positive root of $\log(1+\delta)=2\delta/(1+\delta)$ , and $\beta=\delta^{1/2}+\delta^{-1/2}$ . Then

\Big(\frac8\pi\Big)^{1/2}\le c\le\beta \tag{2.4.4}

and hence

1.59<c<2.49. \tag{2.4.5}

Numerically $\delta\approx3.9216$ and $\beta\approx2.4853$ . The goal states (2.4.4) and (2.4.5) as printed, together with the existence and uniqueness of $\delta$ .

Milestones

Theorem 7 (Hammersley). There is an absolute constant $c$ such that $n^{-1/2}l(\pi_n)\to c$ in probability.
The double integral of the lower-bound argument: $\int_0^\infty\!\int_0^\infty x\,e^{-\frac12(x+y)^2}\,dx\,dy=(\pi/8)^{1/2}$ .
First moment of $\nu$ : for $k\ge1$ , $E(\nu_k)=\binom nk(k!)^{-1}$ .
Subsequence count: if $l(\sigma)\ge k$ then $\nu_k(\sigma)\ge\binom{l(\sigma)}k$ .
(2.4.7): for $1\le k\le r$ , $P\{l(\pi)\ge r\}\le\binom nk\big[k!\binom rk\big]^{-1}$ .
(2.4.8): if $0<\alpha<b$ and $E(\alpha,b)<0$ , then $P\{l(\pi)\ge b\,n^{1/2}\}\to0$ .
The optimisation: $\inf\{b>0:\exists\alpha\in(0,b),\ E(\alpha,b)<0\}=\delta^{1/2}+\delta^{-1/2}$ .

Significance

The result. Theorem 8 was, at the time, the sharpest rigorous information about Ulam's constant. Its upper bound comes from a first-moment computation that applies to any random structure in which long increasing chains can be counted; the same calculation bounds the longest chain in random partial orders and the height of random $k$ -dimensional orders. The lower bound shows that a greedy path through a Poisson process already achieves a positive fraction of the optimum, an argument reused for last-passage percolation models.

Formalizing it. All results here are proved in the literature; none is open. To the best of our knowledge none of them has been machine-checked. A complete development produces: an exact non-asymptotic tail bound on the longest increasing subsequence ((2.4.7)), useful on its own; a Stirling-type asymptotic for products of binomial coefficients at scale $\sqrt n$ ; and, through Theorem 7, a formal existence proof of the Ulam constant. Theorem 7 is the substantial piece: the paper's proof is a sketch through a continuous-parameter subadditive ergodic theorem and a planar Poisson process.

Difficulty

The upper bound needs care with asymptotics: (2.4.7) holds for each $n$ , but the passage to (2.4.8) uses Stirling's formula with $k$ and $r$ integers tending to infinity at rate $\sqrt n$ , and the infimum in milestone 7 is not attained (the admissible set is open), so the argument must produce, for every $b>\beta$ , a suitable $\alpha$ .

The lower bound is where the obvious approach fails. A first-moment or counting argument gives only upper bounds on $l$ ; a lower bound requires exhibiting long ascending sequences. The paper's argument does this with a greedy path in a planar Poisson process, which is not a statement about uniform permutations and needs the Poissonization of Theorem 7 to transfer back. Proving $c\ge(8/\pi)^{1/2}$ directly from the counting definition of $l$ is not available. Both bounds also need the existence of $c$ , which is Theorem 7.

Formalization scope

$\mathcal S_n$ is Equiv.Perm (Fin n); the permutation is named $\sigma$ in Lean because $\pi$ is Real.pi.
$l(\sigma)$ is the largest cardinality of a finite set of positions on which $\sigma$ is strictly increasing; $\nu_k(\sigma)$ is the number of such sets with exactly $k$ elements.
Probabilities under the uniform law are proportions $|A|/n!$ . Convergence in probability depends only on the law of each $\pi_n$ (the paper notes this on p. 895), so no common probability space is introduced. Time is $n\in\mathbb N$ , and at $n=0$ Lean reads $l/\sqrt0$ as $0$ , which does not affect a limit.
The constant of Theorem 8 enters as a hypothesis: the goal is stated for every real $c$ to which $n^{-1/2}l(\pi_n)$ converges in probability. Such a limit is unique, and Theorem 7 shows it exists. No sign or bound on $c$ is assumed. The goal and milestone 7 assert that the positive root $\delta$ exists and is unique, so the upper bound cannot hold vacuously for want of a root.
The double integral is stated as a value only; the claim that it is the mean of i.i.d. increments of a Poisson greedy path is not formalized.

Needed infrastructure: counting arguments on Finset.powersetCard; Stirling's formula (Mathlib has Stirling.tendsto_stirlingSeq_sqrt_pi); elementary calculus for the root $\delta$ ; Gaussian-type integrals on the quadrant. Theorem 7 additionally needs Poisson point processes in the plane, which Mathlib lacks, or another route to the existence of the limit. Contributions of that infrastructure are welcome and reusable well beyond this mission. The counting bounds (milestones 3–5) are independent of Theorem 7 and are a natural first target.

Selected references

J. F. C. Kingman, Subadditive ergodic theory, Annals of Probability 1(6) (1973), 883–899. https://doi.org/10.1214/aop/1176996798
J. M. Hammersley, A few seedlings of research, Proc. Sixth Berkeley Symposium on Mathematical Statistics and Probability, Vol. 1 (1972), 345–394. https://projecteuclid.org/euclid.bsmsp/1200514101
S. M. Ulam, Monte Carlo calculations in problems of mathematical physics, in Modern Mathematics for the Engineer, Second Series, McGraw-Hill (1961), 261–281.
P. Erdős and G. Szekeres, A combinatorial problem in geometry, Compositio Mathematica 2 (1935), 463–470. http://www.numdam.org/item/CM_1935__2__463_0/

9 thms2 active usersReviewed

Completed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Flowshop and Jobshop Schedules: Complexity and Approximation 4: The 3-Partition Job Shop on Two Machines Has a Schedule of Finish Time 2tB, Preemptive or Not, Iff a 3-Partition ExistsResearch Paper

Motivation

In a job shop, each job has an ordered list of tasks, and each task must use a specified machine. A production planner may be able to interrupt a task and resume it later, yet still be unable to find a short schedule efficiently. Gonzalez and Sahni studied how the ability to preempt changes the difficulty of minimizing the time at which all jobs are complete. Their 1978 paper establishes complexity results for flow shops and job shops and then examines approximation schedules when exact optimization is difficult (Gonzalez and Sahni, 1978).

This mission concerns the paper's two-machine construction from 3-PARTITION. It is the reduction used for their claim that finding an optimal preemptive or non-preemptive finish-time schedule remains NP-complete when input size is measured by the sum of task lengths. The formal target isolates the decision equivalence proved for the constructed instance. It gives solvers a precise schedule statement to establish without conflating the scheduling theorem with the separate complexity-class argument.

Setting

A 3-PARTITION input $C$ comprises an integer $t\ge0$ , a positive integer target $B$ , and $s=3t$ positive integer sizes $a_1,\ldots,a_s$ . A valid input satisfies

\sum_{i=1}^{s}a_i=tB,\qquad B/4<a_i<B/2\quad(1\le i\le s).

It has a 3-partition when the $s$ indices can be assigned to $t$ disjoint groups, each containing exactly three indices and having total size $B$ . The strict bounds rule out groups of other cardinalities at that sum and are part of the source problem, not a convenience added for formalization. When $t=0$ , the input has no sizes or groups and the empty grouping is a solution.

The paper builds a job shop $JS(C)$ with machines $P_1,P_2$ and $s+1$ jobs. For $1\le i\le s$ , job $i$ has a task of length $a_i$ on $P_1$ , followed by a task of length $a_i$ on $P_2$ . The last job, $s+1$ , has $2t$ tasks, each of length $B$ . Its tasks alternate between the machines, starting on $P_2$ . This last order matters: reversing it would produce a different construction. The source gives the decision threshold $\tau=2tB$ (Lemma 7, p. 44).

A non-preemptive schedule gives each task one continuous processing interval. A preemptive schedule may divide an operation into finitely many positive-length intervals. In either case, jobs obey their task order, distinct pieces on the same machine do not overlap, and processing starts at or after time zero. Write $FT(S)$ for the time at which all tasks of schedule $S$ have finished. The paper allows the same job to revisit a machine, as the final job does here.

Formalization targets

Lemma 7: the constructed instance

For every valid $C$ , the main goal states both the paper's preemptive equivalence and the non-preemptive form established by its two directions:

\begin{aligned} \exists S\text{ preemptive for }JS(C): FT(S)\le2tB &\iff C\text{ has a 3-partition},\\ \exists S\text{ non-preemptive for }JS(C): FT(S)\le2tB &\iff C\text{ has a 3-partition}. \end{aligned}

The milestones follow the source's proof text: the schedule supplied by a solution in Lemma 7(a), the timing forced on the final job, the exclusion of short preemptive schedules in Lemma 7(b), and the preemptive equivalence stated in the proof. The final-job milestone describes the occupied time slots of the paper's Figure 4, independently of how many adjacent pieces a formal schedule uses.

Significance

The equivalence transfers the distinction between solvable and unsolvable 3-PARTITION inputs to an exact finish-time threshold in a job shop with only two machines. It also establishes the non-preemptive decision equivalence for this construction, because a solution yields a non-preemptive schedule while an unsolvable input rules out even the more permissive preemptive schedules. These facts supply the scheduling part of the paper's strong NP-completeness claim; membership in NP is handled separately by Lemma 6 (pp. 44–45).

The result is proved in the source paper. The work proposed here is a machine-checked development of its explicit reduction equivalence and the finite-piece scheduling model needed to state it. The milestone theorems expose statements that can be reused when formalizing other preemptive scheduling reductions. The shared job-shop instance and 3-PARTITION input are already published definitions; the particular reduction instance and preemptive schedule predicate are new local definitions.

Difficulty

Preemption makes a task's processing time distributable across intervals. Merely checking that each machine has enough total capacity does not characterize feasible schedules: every job's operations must still occur in order, and pieces of different jobs must avoid one another on each machine. The converse direction must constrain every preemptive schedule that meets the threshold, not only a schedule having the visual pattern in Figure 4. A schedule can also represent one uninterrupted interval as several adjacent pieces, so piece count alone cannot express the source's timing claim.

Formalization scope

Machines are Fin 2, with $P_1$ numbered $0$ and $P_2$ numbered $1$ . Jobs are Fin (3t+1); the final job is index $3t$ . Its zero-based operation $i$ uses machine $1$ for even $i$ and machine $0$ for odd $i$ . The definition uses the published JobShopLTAS.Core.Instance for ordered operations, machines, real processing times, and non-preemptive feasibility. It uses the published ResourceScheduling.Chain.ThreePartition for $t,B,a_i$ , validity, and solutions. Those objects have the same conventions as the paper here. The local preemptive model uses finitely many positive-length pieces per task, whose durations sum exactly to that task's processing time. The threshold is the explicit real cast of $2tB$ ; no real infimum or division by a possibly zero optimum appears.

The goal is specific to the instance the paper constructs from each valid input. A free job-shop instance, a freely chosen schedule, or an extra hypothesis that the input has a solution would erase the reduction's content. Validity carries $B>0$ , total $tB$ , and both strict bounds on each $a_i$ . The case $t=0$ remains in scope: the constructed job has no tasks and its finish-time threshold is zero. All existing tasks have positive length whenever the input is valid, so the published non-preemptive predicate's treatment of zero-length tasks does not affect this mission.

The paper states “3-Partition $\alpha$ preemptive JOFT with $m=2$ ” and connects it to NP-completeness for preemptive and non-preemptive scheduling when complexity is measured by the sum of task lengths. The Lean theorem states the proof's two decision equivalences with constant $2tB$ and machine count $2$ . It does not formalize $\alpha$ as a polynomial-time many-one reduction, the unary task-length measure, NP-completeness, or Lemma 6's NP-membership argument. Contributions that establish the reduction statements, the schedule construction, or general finite-piece scheduling facts are within scope.

Selected references

Teofilo Gonzalez and Sartaj Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 1978, pp. 36–52. DOI: 10.1287/opre.26.1.36.

9 thms2 active usersReviewed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Flowshop and Jobshop Schedules: Complexity and Approximation 2: The 3-Partition Flow Shop on Three Machines Has a Preemptive Schedule of Finish Time 2tB Iff a 3-Partition ExistsResearch Paper

Motivation

A flow shop is the simplest multi-stage production model: every job passes through the same machines in the same order, and the question is how to sequence the work so that everything is finished as early as possible. Gonzalez and Sahni's 1978 paper in Operations Research settled the computational complexity of the preemptive version of this problem, in which a task may be interrupted and resumed later on the same machine. For two machines the optimal finish time is computed by Johnson's rule, and preemption does not help. The paper shows that with three machines the preemptive problem is already NP-complete, and its second result, Theorem 2, strengthens this to NP-completeness in the strong sense: the problem stays hard even when the task times are written in unary.

Strong NP-completeness matters because it rules out a pseudo-polynomial algorithm, one whose running time is polynomial in the sum of the task lengths. The preemptive three-machine flow shop ( $F3\mid pmtn\mid C_{\max}$ in later notation) is a standard entry in complexity classifications of scheduling problems, and Theorem 2 is the reference for its status. The paper notes that Garey and Johnson obtained a proof independently.

Timeline. Johnson (1954) solved the two-machine flow shop. Garey, Johnson and Sethi (1976) proved the non-preemptive three-machine flow shop NP-complete in the strong sense. Gonzalez and Sahni (1978) treated the preemptive case: Theorem 1 (ordinary NP-completeness via Partition) and Theorem 2 (strong NP-completeness via 3-Partition), the subject of this mission.

Setting

A flow shop has $m\ge 1$ processors $P_1,\dots,P_m$ and a finite set of jobs. Task $j$ of job $i$ runs on $P_j$ and takes time $t_{j,i}\ge 0$ ; zero times are allowed. For each job, task $j\ge 2$ can begin only after task $j-1$ has been completed, and schedules start at time $0$ .

A preemptive schedule is given, as in the paper's footnote on p. 40, by finitely many pieces $(s,f)$ per task: the task is processed on its processor during $[s,f)$ . Pieces have $0\le s<f$ , pieces on the same processor do not overlap, the pieces of a task have total length $t_{j,i}$ , and a piece of task $j'$ starts only after every piece of every earlier task $j<j'$ of the same job has ended. A task has no preemption when it is processed in at most one piece; a non-preemptive schedule has no preemption anywhere. The completion time of job $i$ is $f_i(S)$ , the end of its last piece, and the finish time is $FT(S)=\max_i f_i(S)$ .

3-Partition. An instance $C=(a_1,\dots,a_s,B)$ , $s=3t$ , consists of a positive integer $B$ and nonnegative integers $a_i$ with $\sum_i a_i=tB$ and $B/4<a_i<B/2$ . It has a 3-partition if $\{1,\dots,s\}$ splits into $t$ disjoint sets $L_1,\dots,L_t$ , each of three elements with $\sum_{j\in L_k}a_j=B$ .

The instance FS. From $C$ the proof of Lemma 4 builds a three-processor flow shop with $s+t+2$ jobs:

jobs $1,\dots,s$ : times $(a_i,\,0,\,a_i)$ on $(P_1,P_2,P_3)$ ;
job $s+1$ : $(0,\,2B,\,B)$ ;
jobs $s+i+1$ , $1\le i\le t-2$ : $(B,\,2B,\,B)$ ;
job $s+t$ : $(B,\,2B,\,0)$ ;
job $s+t+1$ : $(0,\,0,\,B)$ ;
job $s+t+2$ : $(B,\,0,\,0)$ .

Each processor carries total work exactly $2tB$ , and the threshold is $\tau=2tB$ .

Formalization targets

Goal: Theorem 2, as Lemma 4's equivalence

For every 3-Partition instance $C$ with $t\ge 2$ ,

\exists\,S \text{ preemptive schedule of } FS:\ FT(S)\le 2tB \quad\Longleftrightarrow\quad C \text{ has a 3-partition},

and every task time of $FS$ satisfies $t_{j,i}\le 2B$ . The second clause records that the instance's numbers are bounded by those of $C$ , the reduction's contribution to "the problem size being measured as the sum of the length of the tasks".

Milestones

Lemma 3 (p. 40). For a flow shop with $m\ge 1$ processors, every preemptive schedule $S$ can be replaced by a schedule $S'$ with no preemptions on $P_1$ and on $P_m$ and $FT(S')=FT(S)$ .
Lemma 4(a) (p. 41). If $C$ has a 3-partition, $FS$ has a non-preemptive schedule with $FT\le 2tB$ .
First step of Lemma 4(b) (pp. 41–42). In every preemptive schedule of $FS$ with $FT\le 2tB$ , the jobs among $1,\dots,s$ whose $P_1$ task is completed by time $2B$ have $\sum t_{1,i}=B$ .
Lemma 4(b) (pp. 41–42). If $C$ has no 3-partition, every preemptive schedule of $FS$ has $FT>2tB$ .

Significance

The result. Theorem 2 places the preemptive three-machine flow shop among the strongly NP-hard scheduling problems, so no algorithm polynomial in the number of jobs and the total processing time exists unless P = NP. It also shows that allowing preemption, which makes several single-stage problems (such as $P\mid pmtn\mid C_{\max}$ ) easy, does not help for three-stage flow shops. Lemma 3, that preemptions on the first and last machines can be removed without changing the finish time, holds for any number of machines and is a reusable structural fact about flow-shop schedules.

Formalizing it. The result is proved on paper, and its proof of the "only if" direction is an informal busy-processor argument repeated window by window. As far as is known, no part of it has a machine-checked proof. A formal development has to make the interval accounting rigorous: why each processor is busy throughout $[0,2tB]$ , why exactly $B$ units of element jobs end on $P_1$ by $2B$ , and how the argument restarts on $[2B,2tB]$ . Lemma 3 needs an exchange argument on piece representations. Both are new for the platform.

Difficulty

The direction "3-partition $\Rightarrow$ schedule" is a direct construction. The hard direction is the converse. Preemption lets any task be split across many intervals, so the usual non-preemptive arguments, which reason about the order in which whole tasks run, do not apply directly. The paper's argument that the window $[0,2B]$ must contain exactly three element jobs of total $B$ on $P_1$ depends on every processor being continuously busy, and turning "otherwise there is idle time" into a precise statement requires a careful account of which jobs are available to each processor at each moment. The induction on windows is then not a literal restriction of the schedule to a smaller instance, because pieces may cross the boundary at $2B$ .

Formalization scope

Times are real numbers; the 3-Partition data are natural numbers cast to $\mathbb R$ . Processors are Fin m with $P_1=$ 0; in $FS$ , $P_1,P_2,P_3$ are 0, 1, 2.
The 3-Partition instance is the published ResourceScheduling.Chain.ThreePartition (0-based indices, t parts, b $=B$ , Valid, HasSolution), whose definition is the paper's p. 37 problem.
Preemptive schedules are finite sets of pieces per task; precedence is required between every pair of tasks $j<j'$ of a job, so a zero task occupies no time and does not break the job's order. Finish time is a maximum over jobs with baseline $0$ , never an unattained supremum.
"No preemptions on $P_j$ " means at most one piece per task on $P_j$ .
Not formalized: "NP-complete", the reduction symbol $\propto$ , "the problem size being measured as the sum of the length of the tasks", and Lemma 2 (membership in NP). The goal states the equivalence Lemma 4 proves for the constructed instance, plus the bound $t_{j,i}\le 2B$ on its task times.
Added hypothesis: $t\ge 2$ . For $t<2$ the paper's job indices $s+1$ and $s+t$ coincide with conflicting times, so the construction is undefined there.
The first step of Lemma 4(b) is read as: the sum of $t_{1,i}$ over element jobs whose $P_1$ task has completed by time $2B$ equals $B$ .
A trivializing formalization is ruled out: the schedules quantified over are all preemptive schedules of the specific instance $FS(C)$ , the threshold $2tB$ is explicit, and the validity conditions $B/4<a_i<B/2$ are kept, so the schedule side cannot match the weaker "partition into $t$ groups of sum $B$ ".

Contributions welcome: the interval-accounting lemmas (busy processors, work available before a time), Lemma 3's exchange argument, and the schedule of Figure 2.

Selected references

T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1):36–52, 1978. https://doi.org/10.1287/opre.26.1.36
M. R. Garey, D. S. Johnson, R. Sethi, The Complexity of Flowshop and Jobshop Scheduling, Mathematics of Operations Research 1(2):117–129, 1976. https://doi.org/10.1287/moor.1.2.117
S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. https://doi.org/10.1002/nav.3800010110
M. R. Garey, D. S. Johnson, "Strong" NP-Completeness Results: Motivation, Examples, and Implications, Journal of the ACM 25(3):499–508, 1978. https://doi.org/10.1145/322077.322090

8 thms2 active usersReviewed

Missions

Paths, Trees, and Flowers II: Invariance of the Dual — the Outer Vertices O(G) Are Exactly the Vertices Left Exposed by Some Maximum MatchingResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.2 (a)–(c)

Milestones

Significance

Difficulty

Formalization scope

Selected references

An Introduction to Timetabling 3: Course Scheduling with Unavailabilities and Preassignments in p Periods Is Equivalent to p-Coloring the Nodes of a GraphResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Theorem on Boolean Matrices: Warshall's Construction M* Equals the Boolean Sum M ∨ M² ∨ ⋯ ∨ Mᵈ of the Boolean Powers of MResearch Paper

Motivation

Setting

Formalization targets

Goal: the construction computes the power sum

Milestone 1 (Proved, referenced): the THEOREM

Milestone 2: footnote 2

Companion: footnote 3

Significance

Difficulty

Formalization scope

Selected references

On Cores and Indivisibility 1: The Housing Market's Game Without Side Payments Is BalancedResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Strategy-Proofness and Arrow's Conditions 2: Strategy-Proof Voting Procedures Correspond One-to-One to Social Welfare Functions Satisfying CS, NNR and IIAResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 35)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Strategy-Proofness and Arrow's Conditions 4: With Indifference Allowed, a Social Welfare Function Satisfying CS, NNR and IIA Is DictatorialResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3' (p. 49)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Concentration of Measure and Isoperimetric Inequalities in Product Spaces VI: The Symmetric Group — ∫ exp(f(A,σ)/16) dP_N ≤ 1/P_N(A) for the Convex Distance on S_NTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 5.1

Stronger: Proposition 5.2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Concentration of Measure and Isoperimetric Inequalities in Product Spaces X: The Chromatic Number of Random Graphs — χ(G(n,p), m) Lies in an Interval of Length k with High ProbabilityTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 9.1

The deterministic step of the proof, Eq. (9.3)

Proposition 9.2 and Eq. (9.7)

Goal: the period is the order of $b$