Graph Theory

Motivation

Single-machine scheduling with precedence constraints asks for an order in which one machine processes jobs while respecting prescribed comparisons between them. For the objective of minimizing total weighted completion time, the structure of the precedence order can influence the quality of approximation algorithms. Ambühl, Mastrolilli, Mutsanas, and Svensson connect one such approach to coloring a graph built from the order's incomparable pairs. A bounded number of colors would make a certain class of coloring-based guarantees uniform over the class of precedence orders. Their Theorem 4.3 shows that canonical interval orders have no such uniform bound for this particular graph. Ambühl et al., §4.2, p. 658

An interval order is a partial order whose elements can be represented by closed real intervals, with one element strictly before another when the first interval ends before the second begins. Interval orders are a familiar restriction of general precedence systems. The paper distinguishes them from semiorders, represented by intervals of equal length, for which it reports a three-element realizer bound and a corresponding scheduling guarantee. The chromatic obstruction here explains why that particular bounded-color route cannot be extended uniformly from semiorders to all interval orders. It does not assert that every scheduling approach to interval orders fails. Ambühl et al., §§3–4.2, pp. 656–658

Setting

For an integer $n\ge2$, let $[n]$ be a linearly ordered set with $n$ points. The canonical interval order $I_n$ has one element for every pair of distinct points $a<b$ in $[n]$, viewed as the closed interval $[a,b]$. For two such intervals, write $S\le_{I_n}T$ when $S=T$ or the right endpoint of $S$ is strictly less than the left endpoint of $T$. Thus intervals that touch at an endpoint remain incomparable. The formalization represents each interval by its two-element endpoint set, and its order relation is equivalent to this endpoint rule. Ambühl et al., §4.2, p. 658

For any partial order $P$ on a ground set $N$, an ordered incomparable pair is $(x,y)$ with neither $x\le_P y$ nor $y\le_P x$. Both $(x,y)$ and $(y,x)$ are vertices when $x$ and $y$ are incomparable. A linear extension of $P$ is a linear order on the same elements that contains all comparisons of $P$. It reverses $(x,y)$ if it places $y$ before $x$. The graph $G_P$ has the ordered incomparable pairs as vertices. Two distinct vertices form an edge when no linear extension reverses both, while each singleton can be reversed by some linear extension. This singleton condition is the minimality clause in the paper's definition through its hypergraph of incomparable pairs. Ambühl et al., §2.1, p. 655, §3, p. 656

A proper $k$-coloring assigns one of $k$ colors to every vertex of $G_P$ so that endpoints of an edge have different colors. The graph's chromatic number $\chi(G_P)$ is the least positive number of colors that works, when the graph is nonempty. The mission uses the equivalent predicate that no proper map into a fixed $k$-element color set exists once $n$ is large enough. This also gives a clear interpretation at $k=0$.

Formalization targets

The goal is Theorem 4.3: for each fixed integer $k$, all sufficiently large canonical interval orders have incomparable-pairs graphs with chromatic number greater than $k$. With $k\ge0$, the Lean target is

$$\forall k\in\mathbb N,\ \exists n_0\ge2,\ \forall n\ge n_0,\quad G_{I_n}\text{ is not $k$-colorable}.$$

The paper states $k$ as an integer. Its negative cases are immediate from nonnegativity of chromatic numbers; the target states the substantive range. The threshold $n_0$ may depend on $k$, while $I_n$ and $G_{I_n}$ are constructed from $n$ rather than supplied as arbitrary objects. Ambühl et al., Theorem 4.3, p. 658

Two assertions from the theorem's proof serve as milestones. First, $\chi(G_{I_n})$ is nondecreasing as $n$ increases. Second, for four endpoints $i<j<\ell<m$, the vertices $(\{i,j\},\{j,\ell\})$ and $(\{j,\ell\},\{\ell,m\})$ are adjacent in $G_{I_n}$. They are recorded with their wording and provenance from §4.2. A separately published theorem on hypergraph Ramsey numbers is included as a reference because the source uses that theorem in its large-$n$ argument. Ambühl et al., proof of Theorem 4.3, p. 658

Significance

The result provides a precise structural limitation: across the canonical interval orders, the chromatic numbers of $G_{I_n}$ cannot be bounded by one constant. The graph $G_P$ is a specific graph of ordered incomparable pairs, distinct from other graphs that can be associated with a scheduling instance. Thus the conclusion addresses the bounded-color approach attached to this graph, without asserting an algorithmic impossibility for interval-order scheduling. The paper contrasts this limitation with the bounded-realizer situation for semiorders. Ambühl et al., §§3–4.2, pp. 656–658

The theorem is proved in the 2011 paper. The remaining work in this mission is a machine-checked development of its definition layer, its two stated supporting assertions, and the unbounded-color conclusion. The partial-order property of $I_n$ is already proved in the definition file; the three theorem statements are open proof targets in the proposal. A completed formalization would also give reusable components for finite interval orders, ordered incomparable pairs, and coloring arguments in dimension theory.

Difficulty

A pair of intervals overlapping or touching is easy to recognize as incomparable, but graph adjacency has a stronger meaning: it quantifies over every linear extension of the entire partial order. A local test based only on the four displayed intervals would silently change the graph. Likewise, the fact that two vertices have different endpoint descriptions does not by itself make them adjacent. The formal argument must connect the canonical interval representation to the global extension-based edge condition, then show that a bounded coloring cannot persist as the endpoint set grows. Ambühl et al., proof of Theorem 4.3, p. 658

Formalization scope

The endpoint set is Fin n, hence indexed $0,\ldots,n-1$ rather than the paper's $1,\ldots,n$; the shift preserves order. Elements of $I_n$ are exactly two-element subsets of this set. The order relation includes equality and strict separation of endpoint sets and is proved to be a partial order. The graph is defined for an arbitrary binary relation so it can be reused, but every target here applies it to the concrete partial order $I_n$. Vertices are ordered incomparable pairs, and adjacency retains both singleton reversibility and failure of simultaneous reversibility. Defining adjacency directly from the desired four-point pattern would trivialize the target and is excluded.

Colorable n k means existence of a proper function from all vertices of $G_{I_n}$ to Fin k. For an empty graph, zero-colorability is allowed by this representation. The theorem therefore includes a threshold $n_0\ge2$ and quantifies over every $n\ge n_0$; the assertion itself forces the threshold past any empty-graph exceptions. The formal target uses natural $k$; the paper's negative integer values need no separate theorem. No asymptotic notation or unspecified constants occur. The source's Ramsey number $R(3:4,\ldots,4)$ is not hard-coded into the goal, because the source asserts existence of a suitable threshold, not that the least threshold equals that value.

The printed adjacency justification names an alternating-cycle pair set different from the two adjacent vertices in the preceding sentence. The milestone formalizes the adjacency assertion itself and records the printed explanation verbatim for review; it does not turn the mismatched pair set into a hypothesis. The mission needs finite order embeddings, linear extensions, graph colorings, and a finite Ramsey theorem. The existing published Ramsey theorem is referenced as a reusable result. No scheduling approximation algorithm, polynomial-time statement, or numerical scheduling guarantee is formalized in this mission.

Selected references

• Christoph Ambühl, Monaldo Mastrolilli, Nikolaos Mutsanas, and Ola Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4), 653–669, 2011. DOI: 10.1287/moor.1110.0512

Motivation

Single-machine scheduling with precedence constraints, written $1|\mathrm{prec}|\sum w_jC_j$ in the notation of Graham et al., asks for an order of $n$ weighted jobs on one machine that respects a given partial order and minimizes the weighted sum of completion times. The problem is strongly NP-hard (Lawler 1978; Lenstra and Rinnooy Kan 1978), and closing its approximability gap is listed by Schuurman and Woeginger among ten outstanding open problems in scheduling theory. Several 2-approximation algorithms are known (Schulz 1996; Hall et al. 1997; Chudak and Hochbaum 1999; Chekuri and Motwani 1999; Margot et al. 2003).

A line of work by Chudak and Hochbaum, Correa and Schulz, and Ambühl and Mastrolilli showed that the problem is a special case of minimum weighted vertex cover in a graph built from the precedence order. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) observed that this graph is the graph of incomparable pairs of dimension theory, and used that identification to obtain $(2-2/f)$-approximations for orders of fractional dimension at most $f$. This mission formalizes that framework: the identification of the two graphs and the rounding guarantee of the paper's Theorem 5.1.

Setting

An instance $S$ consists of a finite set $N$ of jobs, a partial order $P$ on $N$ (reflexive, antisymmetric, transitive; $(i,j)\in P$ with $i\ne j$ means job $i$ finishes before job $j$ starts), processing times $p_j\ge 0$ and weights $w_j\ge 0$.

Two jobs $x,y$ are incomparable, $x\parallel y$, when neither $(x,y)$ nor $(y,x)$ lies in $P$. The set $\operatorname{inc}(P)$ of incomparable pairs consists of ordered pairs and is closed under swapping. A linear extension of $P$ is a linear order $L\supseteq P$ on $N$; it reverses $(x,y)\in\operatorname{inc}(P)$ when $y<x$ in $L$. A nonempty multiset $L_1,\dots,L_t$ of linear extensions is a $k:t$-realizer if every incomparable pair is reversed by at least $k$ of them. The fractional dimension $\operatorname{fdim}(P)$ is the least ratio $t/k$ over all $k:t$-realizers.

The vertex cover graph $G^S_P$ has the incomparable pairs as nodes; nodes $(i,j)$ and $(k,\ell)$ are adjacent if $j=k$ and $i=\ell$, or $j=k$ and $(i,\ell)\in P$, or $(i,\ell),(k,j)\in P$ (symmetrically closed). Node $(i,j)$ has weight $w_{(i,j)}=p_iw_j$, and $w(C)=\sum_{u\in C}w_u$. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$. The LP relaxation [CS-LP] asks for $x\in[0,1]^{\operatorname{inc}(P)}$ with $x_u+x_v\ge1$ on every edge, minimizing $\sum_u w_ux_u$. For a solution $x$ write $V_a=\{u: x_u=a\}$, and for a linear extension $L$ let $I_{1/2}(L)$ be the pairs of $V_{1/2}$ reversed in $L$.

The graph of incomparable pairs $G_P$ (Felsner and Trotter 2000) also has the incomparable pairs as vertices; two of them are adjacent when the pair of them is a minimal set of incomparable pairs that no linear extension reverses entirely.

Formalization targets

Goal: Theorem 5.1 (p. 658)

For an instance $S$, a $k:t$-realizer $L_1,\dots,L_t$ of $P$, and a half-integral optimal solution $x$ of [CS-LP], put $C_i=V_1\cup\bigl(V_{1/2}\setminus I_{1/2}(L_i)\bigr)$. Then every $C_i$ is a vertex cover of $G^S_P$, and

$$\frac1t\sum_{i=1}^t w(C_i)\;\le\;\Bigl(2-\frac{2}{t/k}\Bigr)\mathrm{OPT}.$$

Milestones

• Proposition 3.2 (p. 657): $G^S_P=G_P$.
• Footnote 4 (p. 659): the pairs reversed by a linear extension are independent in $G^S_P$.
• Eq. (4): $\frac1t|\{i: L_i\text{ reverses }u\}|\ge k/t$ for every incomparable pair $u$.
• Eq. (5): $\frac1t\sum_i w(I_{1/2}(L_i))\ge \frac kt\,w(V_{1/2})$.
• Hochbaum's observation (§5, p. 659): for half-integral feasible $x$, $V_1\cup C$ covers $G^S_P$ whenever $C$ covers $G^S_P[V_{1/2}]$.
• Eqs. (6)–(8): $\frac1t\sum_iw(C_i)\le w(V_1)+(1-\frac kt)w(V_{1/2})\le 2(1-\frac kt)(w(V_1)+\frac12w(V_{1/2}))\le(2-\frac2{t/k})\mathrm{OPT}$ when $P$ is not a linear order.

Significance

The result. Combined with the cited Theorem 2.1 (Ambühl–Mastrolilli 2009; Correa–Schulz 2005), which turns an $\alpha$-approximate vertex cover of $G^S_P$ into an $\alpha$-approximate schedule, Theorem 5.1 gives a $(2-2/f)$-approximation for $1|\mathrm{prec}|\sum w_jC_j$ whenever the precedence order has an efficiently samplable realizer with $t/k\le f$. The paper applies it to interval orders ($3/2$), convex bipartite orders and semiorders ($4/3$), orders of bounded degree and orders of interval dimension two; for the earlier special classes it matched or improved the best known ratios, and for the last two it gave the first results. Proposition 3.2 makes the dimension theory of posets (realizers, critical pairs, fractional dimension) directly available to the vertex cover approach.

Formalizing it. The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. The mission produces a Lean development of incomparable pairs, linear extensions, $k$-fold realizers and the hypergraph of incomparable pairs, which other dimension-theory missions can reuse, and a verified LP-rounding argument for half-integral vertex cover solutions under a distribution of independent sets.

Difficulty

Most of the rounding argument is arithmetic over finite sums. The central nontrivial step is the inclusion $G_P\subseteq G^S_P$ in Proposition 3.2: for two incomparable pairs that are not adjacent under the three-case rule, one must construct a single linear extension reversing both. This needs an extension of $P$ by two new comparabilities whose transitive closure is still antisymmetric, followed by Szpilrajn's theorem; checking that every potential cycle is excluded by the three cases is the actual content. The opposite inclusion, and footnote 4, follow from transitivity and antisymmetry of linear orders. A second point of care is the inequality $t\ge 2k$ used in step (7): it is not part of the definition of a realizer, and follows from each linear extension reversing exactly one of $(x,y)$ and $(y,x)$.

Formalization scope

• Jobs form a finite type N; the precedence order is a relation P : N → N → Prop with IsPartialOrder, carried by the structure Instance. Processing times and weights are nonnegative reals.
• $\operatorname{inc}(P)$ is the subtype IncPair P of N × N; a linear extension is a relation with IsLinearOrder containing P; a $k:t$-realizer is a family Fin t → LinearExtension P with $t>0$. Reversal of $(x,y)$ means $y<x$ in $L$ throughout; the page's "$y>x$" in Eq. (4) and "$\mathrm{Prob}[j>i]$" in Eq. (5) are the same family of inequalities because $\operatorname{inc}(P)$ is symmetric.
• $G^S_P$ is the symmetric closure of the printed three-case rule on distinct nodes. $G_P$ is defined through linear extensions and hyperedge minimality, never through the three-case rule, so Proposition 3.2 is a genuine statement and not a definitional equality.
• [CS-LP] drops the constant term $\sum_jp_jw_j+\sum_{(i,j)\in P}p_iw_j$ of [CS-IP], which does not affect optimality. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$, taken over a finite nonempty family.
• Not formalized: "efficiently samplable", "polynomial time" and "randomized algorithm". The expectation over a uniformly sampled $L_i$ is stated as the average $\frac1t\sum_{i=1}^t$, which is equivalent to it and stronger than the existence of one good index. The existence of a half-integral optimal [CS-LP] solution (Nemhauser–Trotter, cited) is a hypothesis on $x$. The conversion of a vertex cover into a schedule (Theorem 2.1, cited) is not formalized; the goal is stated for vertex covers of $G^S_P$.
• Constants: $2-2/(t/k)$ in real arithmetic; it equals $2-2k/t$, and equals $2$ when $k=0$.
• The paper assumes $\operatorname{fdim}(P)\ge2$, i.e. $P$ is not a linear order. Eqs. (6)–(8) carry that hypothesis as the paper does; the goal omits it because for a linear order both sides are $0$.
• Conclusion (a), that each $C_i$ is a vertex cover, is part of the goal and is not assumed.

Contributions welcome: proofs of the milestones in any order, and a reusable Szpilrajn-style lemma producing a linear extension that reverses a prescribed set of compatible incomparable pairs.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the approximability of single-machine scheduling with precedence constraints, Math. Oper. Res. 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• C. Ambühl, M. Mastrolilli, Single machine precedence constrained scheduling is a vertex cover problem, Algorithmica 53(4), 2009 (reference [2] of the paper).
• J. R. Correa, A. S. Schulz, Single-machine scheduling with precedence constraints, Math. Oper. Res. 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
• G. R. Brightwell, E. R. Scheinerman, Fractional dimension of partial orders, Order 9(2):139–158, 1992 (reference [7]).
• S. Felsner, W. T. Trotter, Dimension, graph and hypergraph coloring, Order 17(2):167–177, 2000 (reference [13]).
• D. S. Hochbaum, Efficient bounds for the stable set, vertex cover and set packing problems, Discrete Appl. Math. 6(3):243–254, 1983 (reference [20]).
• G. L. Nemhauser, L. E. Trotter, Vertex packings: structural properties and algorithms, Math. Programming 8(1):232–248, 1975 (reference [29]).

Motivation

Sparse graphs whose adjacency spectrum is concentrated near zero, expanders, are used throughout theoretical computer science: in error-correcting codes, derandomization, sorting and routing networks, and the construction of pseudorandom objects (Hoory, Linial and Wigderson, survey). The best possible spectral expansion for a $d$-regular graph is governed by the Alon–Boppana bound $2\sqrt{d-1}$, and graphs attaining it, Ramanujan graphs, were constructed explicitly by Lubotzky, Phillips and Sarnak (LPS 1988) and by Margulis. These constructions exist only for special degrees ($d = p+1$ with $p$ prime) and special numbers of vertices (orders of $PSL(2,\mathbb F_q)$ or $SL(2,\mathbb F_q)$). Applications often need a graph of a prescribed size $n$.

N. Alon's paper Explicit expanders of every degree and size (arXiv:2003.11673v1; Combinatorica 41, 2021) shows how to obtain explicit near-Ramanujan graphs on exactly $n$ vertices. This mission formalizes the spectral core of its Theorem 1.2: a Ramanujan graph on $m$ vertices can be enlarged to $n = m + r$ vertices, with degree raised by one, while the nontrivial eigenvalues stay within a constant factor of optimal.

Setting

Let $V$ be a finite set of $m \ge 1$ vertices. A $(n,d,\lambda)$-graph is a $d$-regular graph on $n$ vertices whose adjacency matrix $A$ satisfies $|\mu| \le \lambda$ for every nontrivial eigenvalue $\mu$, that is, every eigenvalue other than the top eigenvalue $d$ of the constant vector $\mathbf 1$. For a symmetric $A$ with $A\mathbf 1 = d\,\mathbf 1$, the nontrivial eigenvalues are those with an eigenvector $f \ne 0$ satisfying $\sum_v f(v) = 0$. Graphs may carry loops, at most one per vertex, and a loop adds one to the degree: it is a diagonal entry $1$ of $A$.

Fix an integer $p \ge 0$ and let $H$ be an $(m, p+1, 2\sqrt p)$-graph on $V$, a $(p+1)$-regular Ramanujan graph. Let $R = \{u_1, \dots, u_r\}$ be $r$ new vertices and let $W_1, \dots, W_r \subseteq V$ be pairwise disjoint sets of $p+2$ vertices each. Put $W = \bigcup_i W_i$ and $L = V \setminus W$. The graph $G$ on $U = V \cup R$ is obtained from $H$ by joining each $u_i$ to every vertex of $W_i$ and adding one loop at each vertex of $L$. Its adjacency matrix is

$$A_G = A_H + A_R + A_L,$$

where $A_H$ is the adjacency matrix of $H$ (zero on $R$), $A_R$ that of the stars joining $u_i$ to $W_i$, and $A_L$ the diagonal matrix of the loops. Every vertex of $G$ has degree $p+2$.

Formalization targets

Goal: Theorem 1.2, spectral core

$$A_G \text{ is an } \Big(m+r,\; p+2,\; \sqrt{2(p+1)} + \sqrt p + \frac{(p+1)\,r}{m}\Big)\text{ matrix.}$$

The paper states $\lambda \le \sqrt{2(d-1)} + \sqrt{d-1} + o(1)$ for $d = p+2$; its proof gives $\sqrt{2(p+1)} + \sqrt p + o(1)$, which is stronger, and the error term it produces is $(p+1)r/m$. The goal is parametrised by $H$, $r$ and the sets $W_i$, so it does not depend on how $m$ and $r$ are chosen.

Milestones

1. The variational characterization of the nontrivial eigenvalues: for a symmetric matrix with constant row sums and $\lambda \ge 0$, $|\mu| \le \lambda$ for every nontrivial eigenvalue if and only if $|f^tAf| \le \lambda\|f\|^2$ whenever $\sum f = 0$.
2. The Cauchy–Schwarz display: $\sum_U f = 0$ implies $|\sum_V f|^2 = |\sum_R f|^2 \le |R| \sum_R f^2$.
3. Inequality (3): $|f^tA_Hf| \le b^2(p+1) + c^2\, 2\sqrt p$ with $b^2 = (\sum_V f)^2/m$ and $c^2 = \sum_V f^2 - b^2$.
4. Display (4): $f^tA_Lf = \sum_{v\in L} f^2(v)$.
5. Inequality (5): $|f^tA_Rf| \le \frac{p+2}{x}\sum_R f^2 + x\sum_W f^2$ for every $x > 0$.
6. Inequality (6): for $\sum_U f = 0$ and $x > 0$,

$$|f^tA_Gf| \le (2\sqrt p+1)\sum_L f^2 + (2\sqrt p+x)\sum_W f^2 + \frac{p+2}{x}\sum_R f^2 + (p+1)\frac rm \sum_R f^2.$$

Significance

With $H$ the Lubotzky–Phillips–Sarnak graph on $m = |SL(2,\mathbb F_q)|$ vertices for the largest suitable prime $q$ with $m \le n$, and $r = n - m$, the distribution of primes in arithmetic progressions gives $r = o(m)$, and the goal yields an explicit $(n, p+2, \lambda)$-graph with $\lambda \le (1+\sqrt2)\sqrt{d-1} + o(1)$ for every sufficiently large $n$. This is within a factor of about $1.21$ of the Ramanujan bound $2\sqrt{d-1}$, for every number of vertices, by an elementary modification of an existing graph. The statement is useful independently of LPS: any Ramanujan graph, or any graph with a bound on its nontrivial eigenvalues, can be padded to a nearby size in the same way.

The result is proved in the paper. No formalization of it, of the $(n,d,\lambda)$ notion, or of the variational characterization of nontrivial eigenvalues for regular graphs exists on the platform. The mission produces a checked version of the spectral argument, and the variational characterization (milestone 1) is a general fact about symmetric matrices with constant row sums that applies to any spectral expander argument.

Difficulty

The vertices of $W$ and $L$ lie in the old graph $H$, whose spectrum is controlled, but the new vertices of $R$ are not; and a vector orthogonal to $\mathbf 1$ on $U$ need not be orthogonal to the constant vector on $V$. Bounding $f^tA_Gf$ by applying the Ramanujan bound for $H$ to $f$ restricted to $V$ therefore fails: the restriction has a component along the trivial eigenvector of $H$, whose eigenvalue $p+1$ is large. The argument must show that this component is small, of order $r/m$, and must balance the star edges between $R$ and $W$ against the loops on $L$ so that every vertex class gets the same coefficient. The naive bound $|f^tA_Rf| \le \|A_R\|\,\|f\|^2 = \sqrt{p+2}\,\|f\|^2$ added to $2\sqrt p$ for $H$ and $1$ for $L$ gives a constant larger than $\sqrt{2(p+1)}+\sqrt p$; the stated constant needs the weighted estimate.

On the Lean side, milestone 1 concerns the spectrum of a symmetric matrix on the invariant subspace $\mathbf 1^\perp$, while Mathlib states the spectral theorem for the whole space.

Formalization scope

• Vertices of $G$ are the disjoint union $V \oplus \mathrm{Fin}\, r$. $G$ is represented by its real adjacency matrix, since it has loops; $H$ is a Mathlib SimpleGraph with adjMatrix.
• The $(n,d,\lambda)$ predicate is stated for matrices: $|V| = n$, symmetry, $A\mathbf 1 = d\,\mathbf 1$, and $|\mu| \le \lambda$ for every eigenpair $(\mu, f)$ with $f \ne 0$ and $\sum f = 0$. For simple graphs, $d$-regularity is added.
• The paper's $o(1)$ terms are replaced by the explicit quantities its proof produces: $(p+1)r/m$ in the goal, and $(p+1)\frac rm\sum_R f^2$ in (6). Inequality (3) is stated with the corrected relation $b^2 + c^2 = \sum_V f^2$; the paper's "$b^2 + c^2 = 1$" holds only for unit restrictions.
• The bound uses $\sqrt p = \sqrt{d-2}$, as in the proof and the abstract, which implies the printed $\sqrt{d-1}$.
• $p$ is any natural number. The hypothesis "$p$ prime, $p \equiv 1 \pmod 4$" serves only to obtain $H$ from LPS, and $H$ is a hypothesis here. The sets $W_i$ are arbitrary pairwise disjoint sets of size $p+2$, not the paper's consecutive blocks of a numbering of $SL(2,\mathbb F_q)$.
• Out of scope: the existence of the prime $q$ and the estimate $n - m = o(m)$; the numbering of $SL(2,\mathbb F_q)$; the "strongly explicit" and polynomial-time claims; the LPS construction (Theorem 2.1, cited); the variant that replaces loops by a matching for even $n$.
• The goal cannot be satisfied trivially: dropping the condition $\sum f = 0$ makes it false, since $p+2$ is always an eigenvalue, and for $p \ge 2$ and small $r/m$ the bound is below $p + 2$ (for $p = 5$ it is about $5.70 + 6r/m$). At $p = 1$ the bound $3 + 2r/m$ is at least the degree $3$, so that case holds trivially; it is the paper's statement there as well.
• Contributions welcome: proofs of each milestone, especially the variational characterization, which is reusable for mission 3 of this series and for any regular-graph spectral argument.

Selected references

• N. Alon, Explicit expanders of every degree and size, arXiv:2003.11673v1, 2020; Combinatorica 41 (2021). https://arxiv.org/abs/2003.11673
• A. Lubotzky, R. Phillips, P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988) 261–277. https://doi.org/10.1007/BF02126799
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bull. AMS 43 (2006) 439–561. https://doi.org/10.1090/S0273-0979-06-01126-8

Motivation

Many systems consist of a finite number of sites whose states influence one another only locally: fruit trees in an orchard that are diseased or healthy, power sources that are working or broken, individuals holding one of several views. Chapter 9 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) asks which joint distributions such systems have in equilibrium. Earlier chapters of the book produce product-form distributions in which the components are independent; spatial models instead give a limited dependence, and §9.1 makes that notion precise through Markov fields.

The central characterization, that a positive random field is Markov with respect to a graph exactly when it factorizes over the cliques of that graph, is the theorem of Hammersley and Clifford (1971, unpublished manuscript), with published proofs by Besag (1974), Grimmett (1973) and Preston (1973). It underlies Gibbs random fields in statistical mechanics, spatial statistics, image analysis and graphical models. Kelly's §§9.2–9.3 then use it to identify the equilibrium distributions of interacting-particle Markov processes ("spatial processes"), connecting it to reversibility and partial balance.

Setting

There are $J$ sites, the vertices of a finite graph $G$; $\partial j$ is the set of neighbours of site $j$ and $G-j$ the set of sites other than $j$. Site $j$ carries an attribute $n_j$ from a finite set $\mathcal N_j$, and a state is $\mathbf n=(n_1,\dots,n_J)$ in $\mathcal S=\mathcal N_1\times\cdots\times\mathcal N_J$. For a set of sites $H$, $\mathbf n_H$ is the vector of attributes of the sites in $H$. The operator $T_j^m$ changes the attribute of site $j$ to $m$.

A random field is a function $\pi$ on $\mathcal S$ with $\pi(\mathbf n)>0$ for every state and $\sum_{\mathbf n}\pi(\mathbf n)=1$. The conditional probability that site $j$ has attribute $n_j$ given all other sites is

$$P(n_j\mid\mathbf n_{G-j}) = \frac{\pi(\mathbf n)}{\sum_{m\in\mathcal N_j}\pi(T_j^m\mathbf n)}. \qquad (9.1)$$

$\pi$ is a Markov field if $P(n_j\mid\mathbf n_{G-j}) = P(n_j\mid\mathbf n_{\partial j})$ for every $j$ and $\mathbf n$ (9.2): the attribute of a site depends on the rest of the system only through its neighbours. A simplex is a single site or a set of sites any two of which are neighbours; $\mathcal C$ is the set of simplices of $G$.

A spatial process is a Markov process $\mathbf n(t)$ on $\mathcal S$ with rates $q$ such that (i) only one component changes at a time, (ii) $q(\mathbf n,T_j^m\mathbf n)$ depends on $\mathbf n$ only through $n_j$ and $\mathbf n_{\partial j}$, and (iii) $T_j^m\mathbf n$ can be reached from $\mathbf n$ by transitions that do not alter $\mathbf n_{G-j}$. The general spatial process of §9.3 has rates

$$q(\mathbf n,T_j^m\mathbf n)=\lambda_j(n_j,m)\,\frac{\Phi(\mathbf n)}{\Phi_{G-j}(\mathbf n_{G-j})} \qquad (9.15)$$

for positive functions $\Phi$, $\Phi_{G-j}$.

Formalization targets

Goal: Theorem 9.2 (p. 186)

A random field $\pi$ is a Markov field if and only if

$$\pi(\mathbf n) = B\prod_{C\in\mathcal C}\phi_C(\mathbf n_C), \qquad \mathbf n\in\mathcal S, \qquad (9.5)$$

for some constant $B$ and functions $\phi_C$.

Milestones

• Lemma 9.1 (p. 185): the conditional probabilities $P(n_j\mid\mathbf n_{G-j})$, $j\in G$, $\mathbf n\in\mathcal S$, determine the random field uniquely.
• Theorem 9.3 (p. 189): the equilibrium distribution of a reversible spatial process is a Markov field.
• Theorem 9.4 (p. 193): for the rates (9.15), with $\alpha_j>0$ solving $\alpha_j(n)\sum_m\lambda_j(n,m)=\sum_m\alpha_j(m)\lambda_j(m,n)$ (9.16), the equilibrium distribution is

$$\pi(\mathbf n) = B\,\frac{\prod_{j=1}^J\alpha_j(n_j)}{\Phi(\mathbf n)}, \qquad (9.17)$$

and it satisfies the partial balance equations (9.18) site by site.

Significance

Theorem 9.2 turns a statement about conditional laws, which is how local interaction is usually specified, into an explicit parametrization of the joint law by clique potentials. On a lattice with binary attributes it reduces a Markov field to one parameter per site and one per pair of adjacent sites, giving the form $\pi(\mathbf n)=B\alpha^M\beta^R$ (9.9). Theorem 9.3 shows that local, reversible dynamics produce Markov-field equilibria, and Theorem 9.4 gives a family of non-reversible processes, containing the closed migration process of Chapter 2, whose equilibria are still explicit; its partial balance equations are the bridge to §9.4.

All four results are classical and proved in the book. They are not, to our knowledge, machine-checked in this discrete form. The platform has an open statement of Hammersley–Clifford in a different setting, HighDimStat.GraphicalModels.thm11_8_hammersley_clifford (Wainwright, High-Dimensional Statistics, Theorem 11.8): a random vector in $\mathbb R^V$ with a strictly positive Lebesgue density and the global (separation) Markov property. Neither statement implies the other as formalized, so this mission poses Kelly's finite, local version separately. A formal proof here also gives reusable infrastructure: conditional probabilities of a distribution on a finite product space, and factorizations over the cliques of a graph.

Difficulty

The "if" direction is routine. The "only if" direction is where the content lies: the functions $\phi_C$ must be produced from $\pi$ alone, and a product over the cliques of $G$ must reproduce $\pi$ at every state, not only at the states whose nonzero attributes sit on a single clique. The natural first idea, one factor per site read off from the conditional laws, fails as soon as two sites interact. The Markov property must also be brought from its explicit form (9.2), which involves a marginal over the non-neighbours, into a usable statement about $\pi$ itself. Strict positivity is essential: without it the "only if" direction is false (Exercise 9.2.2). For Theorem 9.3, condition (iii) cannot be dropped: Exercise 9.2.2 gives a reversible process satisfying (i) and (ii) whose equilibrium is not a Markov field, so any argument that uses only the local form of the rates fails.

Formalization scope

• Sites form an arbitrary finite type V with decidable equality; attributes at site j form a finite type N j, which may differ between sites. States are dependent functions (j : V) → N j, and $T_j^m\mathbf n$ is Function.update n j m. The graph is a Mathlib SimpleGraph V, so $\partial j$ is G.neighborSet j.
• A random field is a real function, positive at every state, with finite sum $1$. $P(n_j\mid\mathbf n_{\partial j})$ is the conditional probability computed from $\pi$ (a ratio of finite sums), so (9.2) is stated literally.
• Simplices are the nonempty cliques of the given graph $G$, including single sites. The factorization ranges over exactly these sets; a product over all subsets of sites, or over the cliques of the complete graph, would make the goal trivially true and is ruled out.
• Theorems 9.3 and 9.4 are read at the level of rates: "equilibrium distribution of a reversible process" is a positive distribution summing to one in detailed balance with $q$ (the published KellyStochasticNetworks.DetailedBalance), and "equilibrium distribution" in 9.4 is a positive distribution summing to one satisfying the equilibrium equations (KellyStochasticNetworks.FullBalance), together with its uniqueness under irreducibility. The Markov process itself is not constructed. The state space is always finite, so all sums are finite.
• Contributions welcome: proofs of any item, general lemmas on conditional laws over finite product spaces, and a formal account of the general Hammersley–Clifford theorem that both this mission and the Wainwright statement could use.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979, Chapter 9. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• J. Besag, Spatial interaction and the statistical analysis of lattice systems, J. Roy. Statist. Soc. B 36 (1974), 192–236. https://doi.org/10.1111/j.2517-6161.1974.tb00999.x
• G. R. Grimmett, A theorem about random fields, Bull. London Math. Soc. 5 (1973), 81–84. https://doi.org/10.1112/blms/5.1.81
• C. J. Preston, Generalized Gibbs states and Markov random fields, Adv. Appl. Probab. 5 (1973), 242–261. https://doi.org/10.2307/1426035
• M. J. Wainwright, High-Dimensional Statistics, Cambridge University Press, 2019, Theorem 11.8. https://doi.org/10.1017/9781108627771

Motivation

A matching of a graph is a set of edges no two of which share a vertex. A matching with as many edges as possible is a basic object of combinatorial optimization. Assignment problems, pairing and scheduling problems, and the Chinese postman problem reduce to it, and it is the standard example of a problem with a polynomial-time algorithm that is not an instance of linear programming over a bipartite structure.

For bipartite graphs the problem was settled by the 1950s, through the theorems of König and Hall and the Hungarian method of Kuhn, whose correctness rests on linear programming duality. As Berge notes on p. 842, that duality "no longer subsists when the graph is not bipartite". C. Berge's three-page note of 1957 (doi:10.1073/pnas.43.9.842) gave the criterion that works for every graph: a matching is maximum exactly when it admits no augmenting chain.

Timeline.

• 1931–1935: König and Hall characterize maximum matchings and systems of distinct representatives in bipartite graphs.
• 1947: Tutte characterizes graphs with a perfect matching (doi:10.1112/jlms/s1-22.2.107).
• 1950: Gallai studies the structure of graphs with respect to their maximum matchings (cited by Berge as the source of his Lemma 1).
• 1955: Kuhn gives the Hungarian method for the bipartite assignment problem (doi:10.1002/nav.3800020109).
• 1957: Berge proves that a matching is maximum if and only if no alternating chain joins two neutral points (Theorem 1 of this paper).
• 1965: Edmonds turns the criterion into a polynomial-time algorithm for general graphs by shrinking odd cycles ("blossoms") (doi:10.4153/CJM-1965-045-4).

Setting

Let $G = (X, U)$ be a finite graph without loops or multiple edges, with vertex set $X$ and edge set $U$. A matching is a set $V_0 \subseteq U$ of edges no two of which have a vertex in common. Its size $|V_0|$ is its number of edges. A matching is maximum if no matching of $G$ has more edges. This is a statement about cardinality: a matching to which no edge can be added (maximal under inclusion) need not be maximum.

Fix a matching $V_0$. Its edges are strong, all other edges weak. A vertex is neutral if no strong edge contains it, and $N$ is the set of neutral points. An alternating chain is a walk in $G$ that does not use the same edge twice and in which, of any two consecutive edges, one is strong and the other weak. Vertices may repeat.

For the milestones, Berge adds a new vertex $\bar a$ joined by strong edges to every neutral point, which gives a graph $\bar G$. Whenever an alternating chain of $\bar G$ runs from $\bar a$ to a vertex $x$, its last edge $(z, x)$ carries an arrow from $z$ to $x$. The non-neutral vertices then fall into four classes:

• $I$, the inaccessible points, at which no edge carries an arrow;
• $W$, the weak points, which receive arrows on weak edges only;
• $S$, the strong points, which receive arrows on strong edges only;
• the medium points, which receive both kinds.

The mission's Lean development uses the same names: IsNeutral, IsAlternatingChain, IsMaximumMatching, barGraph, Arrow, IsInaccessible, IsWeakPt, IsStrongPt, IsMedium.

Formalization targets

Goal: Theorem 1 (p. 843)

$$V_0 \text{ is maximum} \iff \text{no alternating chain connects a neutral point } a \text{ to a neutral point } a' \ne a .$$

The statement fixes nothing beyond finiteness: the graph need not be connected, and no bound on its size is assumed.

Milestones

1. Proof of Theorem 1, first paragraph. An alternating chain $W$ between distinct neutral points makes $(V_0 \setminus W) \cup (W \setminus V_0)$ a larger matching.
2. Lemma 5. If $|N| \le 1$, then $V_0$ is maximum.
3. Lemma 2. If $\bar a$ is inaccessible, then $S \cup N$ is internally stable (an independent set).
4. Lemma 3. If $\bar a$ is inaccessible and there are no medium and no inaccessible points, then $S \cup N$ is a maximum internally stable set, $W$ is a minimum cover, and $V_0$ is maximum.
5. Lemma 4. If $\bar a$ is inaccessible, the edges leaving a connected component $Z$ of $I$ are weak and carry no arrow, the outside neighbours of $Z$ are weak points, and $|Z| \ge 2$.
6. Lemma 1 (Gallai), corrected. If $\bar a$ is inaccessible, the components of the medium points, enlarged by the neutral points that receive a weak arrow, have exactly one strong edge entering them, have all other boundary edges weak and directed outward, and have at least three vertices.

Significance

Theorem 1 reduces the optimality of a matching, a statement about all matchings of the graph, to the absence of one kind of local structure. Its consequences include:

• correctness of every augmenting-path algorithm for maximum matching, including Edmonds' blossom algorithm and the Hopcroft–Karp and Micali–Vazirani refinements;
• the standard proofs of the Tutte–Berge formula and of the Gallai–Edmonds structure theorem, which start from it.

A matching that is not maximum can be certified by exhibiting the chain, and a maximum matching is certified by the labelling of Lemmas 1–4.

Theorem 1 has been proved since 1957 and appears in every textbook on matching theory. It is not formalized in Mathlib at the revision this mission uses. Mathlib has matchings as subgraphs, perfect matchings, alternating cycles and Tutte's theorem, but no augmenting-path characterization. This mission adds a formal statement of the theorem, together with the labelling of Berge's proof in a form that later missions on Edmonds' algorithm can reuse.

Difficulty

The "only if" direction is a local computation: the symmetric difference along an augmenting chain is again a matching, with one more edge. Even this needs care, because an alternating chain is only a trail and may a priori revisit vertices, while the augmentation needs a path.

The converse is the substance. In bipartite graphs, a search from the neutral points that alternates weak and strong edges labels each vertex at most one way, and its failure yields a cover of the same size as the matching. In general graphs an odd cycle lets a vertex be reached both through a strong and through a weak edge (the medium points). The bipartite labelling then fails, and no cover of size $|V_0|$ need exist: in a triangle the maximum matching has one edge and the minimum cover two. The proof has to treat these odd structures separately, and that is what Lemmas 1 and 4 do.

Formalization scope

• Graphs and matchings. The graph is a Mathlib SimpleGraph V on a Fintype V. The paper's "unoriented graph (or 1-dimensional regular complex)" may have parallel edges, but a matching uses at most one edge of a parallel class, so nothing is lost. The matching is a subgraph M with M.IsMatching, and its size is M.edgeSet.ncard. Maximum means cardinality-maximum over all matching subgraphs. Internally stable sets and covers are Mathlib's IsIndepSet and IsVertexCover.
• Alternating chains. An alternating chain is a walk that is a trail (no repeated edge; vertices may repeat), with alternation between consecutive edges.
• $\bar G$ and arrows. $\bar G$ lives on Option V, with $\bar a$ = none. An arrow needs an alternating chain of positive length from $\bar a$.
• Readings of ambiguous phrases.
  • "$\bar a$ is inaccessible" means that no arrow is directed to $\bar a$. Read literally ("not adjacent to a directed edge"), the phrase fails whenever $N \neq \emptyset$.
  • "Edges adjacent to $Z$" (and to $Y$) are the edges with exactly one endpoint in the set.
  • The paper's medium class $M$ is IsMedium in Lean, because M names the matching.
• Results not formalized.
  • Lemma 1 is false as printed. On a triangle with one matched edge, the two medium points form $Y$ with $|Y| = 2$, and their neighbour is neutral. The mission states a corrected form, labelled as such, in which neutral blossom bases are added to $Y$.
  • Lemma 6 (shrinking) is false. On the path $u$–$x$–$y$–$v$ with extra edges $y$–$t$, $t$–$q$, the set $A = \{x, y, t\}$ and $V_0 = \{xy, tq\}$, the matching is maximum on $A$ and on the shrunk graph, yet $\{ux, yv, tq\}$ is larger.
  • Theorem 2 (a minimum cover built from the labels) is false. Take a neutral vertex joined to the stems of two triangles, with the stems and the triangles matched. The construction yields a cover of 6 vertices, while one of 5 exists.
  • Neither false result is formalized, and the cases of the proof of Theorem 1 that rest on them are not milestones. The algorithmic remarks on p. 844 are procedures, not claims, and are not formalized either.
• Ruled-out trivializations. None of the following is a faithful encoding:
  • reading "maximum" as inclusion-maximal;
  • allowing an alternating chain to join a neutral point to itself (the one-vertex chain would then always exist);
  • reading "$\bar a$ is inaccessible" in a way that is never or always true;
  • imposing alternation on only some pairs of edges.

Any proof of the goal is welcome, whether it follows Berge's induction, uses the symmetric difference of two matchings, or goes through the Tutte–Berge formula. Reusable infrastructure is especially welcome: augmentation along a path, the symmetric difference of two matchings as a union of paths and cycles, and trails that alternate with respect to a matching.

Selected references

• C. Berge, Two theorems in graph theory, Proc. Natl. Acad. Sci. USA 43(9) (1957), 842–844. doi:10.1073/pnas.43.9.842
• W. T. Tutte, The factorization of linear graphs, J. London Math. Soc. 22 (1947), 107–111. doi:10.1112/jlms/s1-22.2.107
• H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2 (1955), 83–97. doi:10.1002/nav.3800020109
• J. Edmonds, Paths, trees, and flowers, Canadian J. Math. 17 (1965), 449–467. doi:10.4153/CJM-1965-045-4

Motivation

In the secretary problem, $n$ items with nonnegative values arrive one at a time in a uniformly random order, and an online algorithm must decide on each arrival, irrevocably, whether to keep it. The classical version keeps one item; the rule that observes a $1/e$ fraction of the arrivals and then takes the first item better than everything seen picks the best item with probability at least $1/e$ (Ferguson 1989).

Babaioff, Immorlica and Kleinberg (SODA 2007; journal version J. ACM 2018) introduced the matroid secretary problem: the kept set must be independent in a known matroid. It models online auctions in which the feasible sets of winners have matroid structure, for example hiring along the edges of a network without closing a cycle. They gave a $16$-competitive algorithm when the matroid is graphic, i.e. the items are the edges of a graph and a set is feasible when it contains no cycle.

Timeline for graphic matroids:

• 2007, Babaioff–Immorlica–Kleinberg: $16$-competitive.
• 2009, Babaioff–Dinitz–Gupta–Immorlica–Talwar (SODA 2009, Theorem 1.5): $3e\approx 8.15$-competitive, through a random reduction to partition matroids. This mission formalizes that result.
• 2009, Korula–Pál (ICALP 2009): $2e$-competitive, by a different reduction.

Setting

Let $G=(V,E)$ be a finite simple graph. Each edge $e$ has a value $v(e)\ge 0$. A set $S\subseteq E$ is independent in the graphic matroid of $G$ if the graph $(V,S)$ has no cycle. The offline optimum is

$$\mathrm{OPT}(G,v)=\max\Big\{\sum_{e\in S}v(e): S\subseteq E\ \text{acyclic}\Big\}.$$

The edges arrive in a uniformly random order. An algorithm sees each edge and its value on arrival and decides at once whether to select it. The selected set must be acyclic. The algorithm is $\alpha$-competitive if $\mathrm{OPT}(G,v)\le\alpha\cdot\mathbb E[\text{value of the selected set}]$ for every $G$ and every $v\ge 0$.

A partition matroid on a subset $U'\subseteq E$ is given by a family $P$ of nonempty, pairwise disjoint parts with union $U'$: a set is independent when it lies in $U'$ and meets each part at most once. Its max-weight base has value $\mathrm{val}(P,v)=\sum_{p\in P}\max_{e\in p}v(e)$.

Definition 5.1. A random partition $\mu$ (a probability distribution on such families, chosen from $G$ alone) is an $\alpha$-partition scheme if every partition in its support has only acyclic independent sets, and for every $v\ge 0$,

$$\mathrm{OPT}(G,v)\le \alpha\cdot\mathbb E_{P\sim\mu}[\mathrm{val}(P,v)].$$

The random partition of Lemma 5.3. Pick an edge $\{u,w\}$ uniformly at random. With probability $\tfrac12$ colour $u$ red and $w$ blue, otherwise the reverse. Colour every other vertex red or blue independently with probability $\tfrac12$. Each red vertex $x$ gets a part: the red-blue edges at $x$. Then repeat on the edges with both endpoints blue, with fresh randomness.

The algorithm. Draw the partition, let the edges arrive, and on each part run the classical secretary rule on that part's arrivals. Output all selected edges.

Formalization targets

Goal: Theorem 1.5

For every finite simple graph $G$ and every $v\ge 0$:

1. every possible output of the algorithm is an acyclic set of edges of $G$;

$$\mathrm{OPT}(G,v)\le 3e\cdot\mathbb E[\mathrm{ALG}].$$

Part 1 is needed for the statement to have content: an algorithm that selects every edge would otherwise satisfy part 2.

Milestones

• Section 2, p. 4. On $m\ge1$ arrivals, the classical rule selects the maximum with probability at least $1/e$.
• Theorem 5.4, first clause. For a fixed partition $P$, the per-part rule outputs a set independent in the partition matroid, and $\mathrm{val}(P,v)\le e\cdot\mathbb E_\pi[\mathrm{ALG}]$.
• Lemma 5.3, independence. Every partition the random construction can produce is a partition matroid on a subset of $E$, and each of its independent sets is a forest.
• Lemma 5.3. The construction is a $3$-partition scheme.
• Section 5, p. 10. Any $\alpha$-partition scheme for a graphic matroid, combined with the per-part rule, gives a feasible, $e\alpha$-competitive algorithm.

Significance

The theorem shows that the graphic matroid secretary problem admits a constant-competitive algorithm with a small explicit constant. It does so through a reduction: a random partition matroid that is feasible for the original matroid and loses only a constant factor in expectation. The reduction separates the combinatorics (Lemma 5.3) from the online part (Theorem 5.4). The same framework gives algorithms for uniform and transversal matroids and for the weighted and discounted variants on any matroid with an $\alpha$-partition property.

The result is proved in the paper; it has not been formalized. The mission contributes a machine-checked version of the reduction, a formal treatment of a recursively defined random partition, and the classical secretary bound in a reusable finite form. The constant $3e$ is not the best known for graphic matroids (Korula–Pál improve it to $2e$), so the formal goal is this algorithm's guarantee, not the best possible ratio.

Difficulty

The online half is routine once the classical bound is available: the relative order of the edges in each part is uniform, and the parts are disjoint. The difficulty is Lemma 5.3. The natural idea of using a fixed optimal forest to build the partition is ruled out because the partition must be chosen before the values are seen. The expectation bound must therefore hold for every valuation at once, for a law that depends on the graph only. The construction is recursive and random: its expected value is not a closed-form sum, and any bound has to be carried through the random sequence of blue-blue subgraphs. Feasibility needs an invariant across rounds: the parts created later live inside the blue-blue edges of every earlier round.

Formalization scope

• Graph. A SimpleGraph on a Fintype vertex type with decidable adjacency. The edges are G.edgeFinset, and acyclicity of $S$ is (SimpleGraph.fromEdgeSet S).IsAcyclic. Multigraphs are not covered.
• Values. Values are a real function v : Sym2 V → ℝ with ∀ e, 0 ≤ v e; only the values on edges matter.
• OPT is a Finset.sup' over acyclic subsets of the edge set. A partition is a finite family of nonempty, pairwise disjoint parts inside the edge set. Its max-weight base value is the sum of the part maxima.
• Random partition. A PMF defined by well-founded recursion on the number of edges. Empty parts are dropped, and edges with two red endpoints are discarded.
• Random order. The edges are numbered by a fixed enumeration. An arrival order is a permutation of the numbers, and expectation over the order is the average over all $|E|!$ permutations.
• Classical rule. It samples $\lfloor m/e\rfloor$ arrivals of a part with $m$ edges. Ties are broken by preferring the smaller edge number among equal values.
• Constants. Competitiveness is multiplicative ($\mathrm{OPT}\le 3e\cdot\mathbb E[\mathrm{ALG}]$), so a zero expectation is not a loophole.
• Ruling out trivial formalizations. In Definition 5.1 the random partition is fixed before the valuation, and the independence requirement holds for every partition in its support. A partition allowed to depend on $v$ would make every matroid $1$-partitionable.

A complete development needs the classical secretary bound in finite form, the uniformity of induced sub-orders of a uniform permutation, expectations of PMF.bind along a well-founded recursion, and facts about forests in SimpleGraph. The first two, and a general graphic-matroid layer, are reusable beyond this mission. Proofs of any milestone, alternative proofs of Lemma 5.3, and extensions to the uniform and transversal cases of Theorem 5.2 are welcome.

Selected references

• M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proc. 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009. https://doi.org/10.1137/1.9781611973068.135
• M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, SODA 2007, pp. 434–443. https://dl.acm.org/doi/10.5555/1283383.1283429
• M. Babaioff, N. Immorlica, D. Kempe, R. Kleinberg, Matroid Secretary Problems, Journal of the ACM 65(6), 2018. https://doi.org/10.1145/3212512
• N. Korula, M. Pál, Algorithms for Secretary Problems on Graphs and Hypergraphs, ICALP 2009, LNCS 5556. https://doi.org/10.1007/978-3-642-02930-1_42
• T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493

Motivation

Project scheduling assigns start times to the activities of a project subject to constraints between them. The classical critical path method (CPM) of Kelley and Walker (1959) and the program evaluation and review technique (PERT) allow only minimum time lags: activity $j$ may start no earlier than a given time after activity $i$ starts. Practice also needs maximum time lags: activity $j$ must start no later than a given time after $i$. These express deadlines, release dates, time windows and "no wait" couplings. Once maximum time lags are allowed, the project network has cycles and negative arc weights, and even the existence of a schedule is no longer automatic.

This mission is the first of a series on Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003), a standard reference for resource-constrained project scheduling with general temporal constraints. Chapter 1 contains the temporal part of the theory: feasibility, earliest and latest schedules, floats, and the distance order. Every later chapter adds resource constraints on top of this layer.

Timeline. Roy (1964) introduced the Metra Potential Method, which is scheduling on activity-on-node networks with minimum time lags. Neumann (1975, Sect. 6.4) treated time windows through potentials on networks with arbitrary arc weights. Bartusch, Möhring and Radermacher (1988, Annals of Operations Research 16) developed the general theory of scheduling project networks with resource constraints and time windows, including the feasibility criterion stated below. The book collects these results in Chapter 1.

Setting

A project consists of $n\ge 1$ real activities $1,\dots,n$ and two fictitious activities, $0$ (project beginning) and $n+1$ (project completion), so the node set is $V=\{0,1,\dots,n+1\}$. Each activity $i$ has an integer duration $p_i$, with $p_0=p_{n+1}=0$ and $p_i>0$ for real activities.

A minimum time lag $d^{\min}_{ij}$ between two different activities becomes an arc $\langle i,j\rangle$ of weight $\delta_{ij}=d^{\min}_{ij}$. A maximum time lag $d^{\max}_{ij}$ becomes a backward arc $\langle j,i\rangle$ of weight $\delta_{ji}=-d^{\max}_{ij}$. There is at most one arc per ordered pair, keeping the tightest lag. The result is the activity-on-node (AoN) network $N=(V,E,\delta)$, whose integer weights may be positive, negative or zero and which in general contains cycles. The book establishes that for every node $i$ there is a path from $0$ to $i$ of nonnegative length and a path from $i$ to $n+1$ of length at least $p_i$ (p. 8, from Definition 1.1.1 and Remarks 1.1.2). This is the standing assumption of the chapter.

A schedule is a vector $S=(S_0,\dots,S_{n+1})$ of real start times with $S_0=0$ and $S_i\ge 0$. It is time-feasible if it satisfies the temporal constraints

$$S_j-S_i\ \ge\ \delta_{ij}\qquad(\langle i,j\rangle\in E),$$

and $\mathcal S_T$ is the set of time-feasible schedules. A time-feasible schedule minimizing the project duration $S_{n+1}$ is time-optimal.

The length of a path or cycle is the sum of its arc weights. For an integer $L=LS_{n+1}$, which is either a prescribed maximum project duration $\bar d$ or the shortest project duration, the temporal scheduling network $N^+$ adds the backward arc $\langle n+1,0\rangle$ with weight $-L$. The distance $d_{ij}$ is the length of a longest path from $i$ to $j$ in $N^+$, with $d_{ii}=0$. The earliest and latest start times are $ES_i=d_{0i}$ and $LS_i=-d_{i0}$, the earliest completion time is $EC_i=ES_i+p_i$, and the total float is $TF_i=LS_i-ES_i$. The distance order $\prec_D$ is defined for $i\ne j$ by: $i\prec_D j$ if $d_{ij}>0$, or $d_{ij}=0$ and $d_{ji}<0$.

Formalization targets

Goal: Theorem 1.3.3 (p. 10)

$$\mathcal S_T\ne\emptyset\quad\Longleftrightarrow\quad N\ \text{contains no cycle of positive length}.$$

The statement contains no constants. It is the consistency criterion for the temporal constraints and the entry condition for everything else in the book.

Milestones

1. Distances, §1.3, p. 11, Eq. (1.3.3). If $N^+$ has no cycle of positive length, then $d$ satisfies $d_{ij}\ge\delta_{ij}$ on $E^+$ and the triangle inequality $d_{ij}\ge d_{ih}+d_{hj}$, and it is the smallest family that does.
2. Earliest and latest schedules, §1.3, p. 12. Under the same hypothesis and the standing assumption, $ES=(d_{0i})_i$ is time-feasible and lies below every time-feasible schedule. $LS=(-d_{i0})_i$ is time-feasible, satisfies $LS_{n+1}\le L$, and lies above every time-feasible schedule $S$ with $S_{n+1}\le L$.
3. Remark 1.3.2 (p. 10). If $\mathcal S_T\ne\emptyset$, there is an integer-valued time-optimal schedule.
4. Proposition 1.3.8 (p. 15). For a real activity $i$, $[LS_i,EC_i[\ne\emptyset$ if and only if $i$ is critical ($TF_i=0$) or near-critical ($0<TF_i<p_i$). A further item of the mission, not a milestone, states the claim of §1.4, p. 17 (after Definition 1.4.3): if $N^+$ has no cycle of positive length, $\prec_D$ is a strict order on $V$.

Significance

The result itself. Theorem 1.3.3 tells when the temporal constraints of a project can be met at all. Milestones 1 and 2 identify the earliest and latest schedules with longest path lengths, which makes temporal scheduling a pair of longest-path computations (a forward pass from $0$ and a backward pass to $0$). Remark 1.3.2 justifies working in integer time. The distance order and the base time intervals $[LS_i,EC_i[$ are the inputs of the resource-constrained methods in Chapters 2 and 3: priority rules schedule along $\prec_D$, and base time intervals give lower bounds on resource usage.

Formalizing it. These results are classical and proved, but the book does not prove Theorem 1.3.3; it points to Neumann (1975) and Bartusch et al. (1988). To our knowledge they have no machine-checked form in this generality, with arbitrary integer weights, cycles, fictitious start and end nodes, and the backward arc of $N^+$. The CPM results for acyclic event networks with nonnegative durations already on Prove2Me are a special case. The definitions of this mission (project, AoN network, schedule, $N^+$, distances) are intended as the shared substrate for the later missions of the series, which add renewable and cumulative resources.

Difficulty

The necessity direction of the goal is a telescoping sum around a cycle. The sufficiency direction needs a schedule, and the natural candidate $S_i=d_{0i}$ requires three things: longest path lengths must be well defined, they must be finite, and they must satisfy the temporal constraints. With negative weights and cycles, the maximum over walks is unbounded when a positive cycle exists, and a walk-based definition gives nothing. A path-based definition gives a finite maximum but loses the concatenation property, so the triangle inequality becomes a statement about removing nonpositive cycles from walks. $S_0=0$ and $S_i\ge 0$ further depend on the standing assumption: without it, an arc $\langle i,0\rangle$ with positive weight makes $\mathcal S_T$ empty although no cycle is positive. The same combinatorics of walks, paths and cycles is behind milestones 1 and 2 and the distance-order item.

Formalization scope

Nodes are Fin (n + 2): $0$ is the project beginning and Fin.last (n + 1) the project completion. The field one_le_n records $n\ge 1$. Durations are natural numbers with $p_0=p_{n+1}=0$ and $p_i>0$ for real activities. Arc weights are arbitrary integers on a loop-free Finset of ordered pairs, so parallel arcs cannot occur. Start times are real; integrality appears only as Remark 1.3.2.

Walks are functions Fin (m + 1) → Fin (n + 2). A path is an injective walk, and a cycle is a closed walk with at least one arc and distinct nodes apart from the repeated endpoint. Distances are maxima over the finitely many paths, valued in WithBot ℤ with $\bot=-\infty$ for unreachable pairs. No supremum over an unbounded set is taken. $ES_i$ and $LS_i$ convert these to integers with junk value $0$ for $-\infty$, and every milestone that uses them carries the hypotheses under which the distances are finite. The backward arc of $N^+$ has weight $-L$ for an integer parameter $L$. If $N$ already contains an arc $\langle n+1,0\rangle$, the two arcs merge into one carrying the larger weight, as in the book's convention for parallel lags. The standing assumption of p. 8 is a named predicate and a hypothesis of the goal and of milestones 2 and 4.

A trivializing formalization is ruled out: weights are signed integers and cycles are allowed, so the no-positive-cycle condition is not vacuous, and the standing assumption is satisfiable by projects with maximum time lags.

A complete development needs cycle removal from closed walks, the Bellman-type characterization of longest paths without positive cycles, and total unimodularity or a direct integrality argument for Remark 1.3.2. The walk, path and distance layer is reusable for any difference-constraint system. Proofs of milestones and lemmas on walk decomposition are welcome.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. https://doi.org/10.1007/978-3-540-24800-2
• M. Bartusch, R. H. Möhring, F. J. Radermacher, "Scheduling project networks with resource constraints and time windows", Annals of Operations Research 16 (1988), 201–240. https://doi.org/10.1007/BF02283745
• K. Neumann, Operations Research Verfahren, Band III, Hanser, 1975, Sect. 6.4.
• B. Roy, Les problèmes d'ordonnancement: applications et méthodes, Dunod, 1964.
• J. E. Kelley, M. R. Walker, "Critical-path planning and scheduling", Proceedings of the Eastern Joint Computer Conference, 1959, 160–173. https://doi.org/10.1145/1460299.1460318
• R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows, Prentice Hall, 1993, Sect. 5.4 and 5.6.