Combinatorics

Completed

Theoretical Computer Science·Captain: marwahaha

3SUM in O(n^1.999074) Time on a Word RAMOpen Problem

Prove a deterministic $O(n^{1.999074})$ algorithm for integer 3SUM in the campaign's shared word-RAM model, improving the verified $1.999112$ bound.

A promising parameter choice is $c=22$ , $\theta=0.11229$ , $D=\lfloor n^{0.054}\rfloor$ , and $g=\lceil D^{0.0343}\rceil$ . Lean-checked arithmetic certificates give $\gamma>0.0686$ , $q\le0.431369<0.4314$ , and $0.054<R_c$ . The predicted Exact Triangle saving is $\delta=0.0018522$ , giving a 3SUM cutoff of $1.9990739$ and a strict margin below the target.

The algorithmic claim remains open. The milestones are to establish the faster inner solver, then verify the integer computations for $D$ and $g$ and prove the total Exact Triangle cost, including preprocessing and scans. The existing verified reductions and foundation definitions can then be reused. The numerical certificates alone do not prove the mission.

41 thms3 active usersReviewed

Operations Research Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces XI: The Random Assignment Problem — Fluctuations of the Optimal Cost of Order (log N)²/(√N log log N)Textbook

Motivation

The assignment problem asks for a one-to-one matching of $N$ agents to $N$ tasks that minimizes the total cost. It is one of the basic problems of combinatorial optimization and is solved in polynomial time by the Hungarian method. Its random version, in which the $N^2$ costs are independent random variables, is a standard model for the typical behavior of optimization problems on random inputs, and it has been studied in probability, operations research and statistical physics.

Timeline:

Walkup (1979) showed that the expected optimal cost $E(L_N)$ of the random assignment problem with independent uniform $[0,1]$ costs stays bounded as $N \to \infty$ (doi:10.1137/0208036).
Karp (1987) proved $E(L_N) \le 2$ .
Talagrand (1995), in the article this mission formalizes, bounded the fluctuations of $L_N$ around its median by $K(\log N)^2/(\sqrt N \log\log N)$ , as a showcase of his concentration inequality for product measures (doi:10.1007/BF02699376).
Aldous (2001) proved the limit $E(L_N) \to \pi^2/6$ , the value predicted by Mézard and Parisi (doi:10.1002/rsa.1015).

This mission is Chapter 10 of Talagrand's article.

Setting

Fix $N$ and two sets $I$ and $J$ of cardinal $N$ . An assignment is a one-to-one map $\tau$ from $I$ onto $J$ . Given a cost matrix $a = (a_{i,j})_{i \in I, j \in J}$ , the cost of $\tau$ is $\sum_{i \in I} a_{i,\tau(i)}$ . In the random problem the costs are $X_{i,j}$ , independent and uniformly distributed on $[0,1]$ , and the optimal cost is the random variable

L_N = \min\Big\{ \sum_{i \in I} X_{i,\tau(i)} \;;\; \tau \text{ assignment} \Big\}.

A median of $L_N$ is any real $M$ with $P(L_N \le M) \ge 1/2$ and $P(L_N \ge M) \ge 1/2$ .

The argument uses digraphs. A digraph is a subset $D \subseteq I \times J$ , and for $S \subseteq I$ the set of neighbors is $D(S) = \{ j \in J ;\ \exists i \in S,\ (i,j) \in D \}$ . For $\alpha \ge 2$ , $D$ is $\alpha$ -expanding if for every $S \subseteq I$

\operatorname{card} S \le \tfrac N2 \Rightarrow \operatorname{card} D(S) \ge \min\big(\alpha \operatorname{card} S, \tfrac N2\big), \qquad \operatorname{card} S \ge \tfrac N2 \Rightarrow \operatorname{card} D(S) \ge N - \tfrac 1\alpha (N - \operatorname{card} S).

For $u > 0$ the threshold digraph is $D_u = \{(i,j) ;\ X_{i,j} \le 2uN^{-1}\log N\}$ : it keeps only the cheap edges.

Formalization targets

Goal: Theorem 10.5

There is a universal constant $K$ such that for $N \ge 3$ , every median $M$ of $L_N$ and every $t \ge 0$ ,

t \le \sqrt{\log N} \Rightarrow P\Big(|L_N - M| \ge \frac{K t (\log N)^2}{\sqrt N \log\log N}\Big) \le 2 e^{-t^2},

t \ge \sqrt{\log N} \Rightarrow P\Big(|L_N - M| \ge \frac{K t^3 \log N}{\sqrt N \log t^2}\Big) \le 2 e^{-t^2}.

The constant $K$ is left unspecified, as in the paper.

Milestones, in attack order

Lemma 10.1 (deterministic): in an $\alpha$ -expanding digraph with $\alpha^m \ge N/2$ , every $i \in I$ lies on a cycle $i = i_1, \dots, i_{n+1} = i$ of distinct points, $n \le 2m$ , with $(i_\ell, \tau(i_{\ell+1})) \in D$ .
Corollary 10.2 (deterministic in the costs): if $D_u$ is $\alpha$ -expanding and $\alpha^m \ge N/2$ , every optimal assignment satisfies $X_{i,\tau(i)} \le 4muN^{-1}\log N$ .
Lemma 10.4: for independent events of probability $p$ , fewer than $\delta p N$ occur with probability at most $\exp(-Np/K(\delta))$ .
Proposition 10.3: for a universal $K$ and $u > K$ with $u \log N \le N$ , $D_u$ is $u\log N$ -expanding with probability at least $1 - N^{-u/K}$ .

Significance

The expected value of $L_N$ is of the same order as a single cost, yet $L_N$ is a function of $N^2$ independent variables. A generic bounded-difference bound in all $N^2$ coordinates gives no useful concentration at this scale. Theorem 10.5 shows that the fluctuations are at most of order $(\log N)^2/(\sqrt N \log\log N)$ , and by the remark after the theorem, so is the standard deviation of $L_N$ . The chapter is a worked example of how a concentration inequality in product spaces is combined with a combinatorial localization argument, the reduction to small costs, and that pattern recurs in the study of random combinatorial optimization problems.

Status: the theorem and its lemmas are proved in the paper. As far as a search of the platform shows, none of them has a machine-checked proof. The two posed statements of Theorem 4.1.1 on the platform (finite-alphabet form) are the concentration inequality the proof calls on; formalizing this chapter adds the combinatorics of expanding digraphs, the random-graph estimate Proposition 10.3 and the final assembly.

Difficulty

The naive approach applies a concentration inequality directly to $L_N$ as a function of the $N^2$ costs, each of which can change $L_N$ by up to $1$ . That loses all control, because the variance proxy grows with the number of coordinates. The central step is to show that, with high probability, an optimal assignment only uses costs of order $N^{-1}(\log N)^2$ . This requires the cycle structure of Lemma 10.1, and it requires showing that the sparse random digraph $D_u$ has expansion uniformly over all subsets $S$ of $I$ , whose number is exponential in $N$ . Proposition 10.3 has to beat that union bound, and its proof covers only one of the two expansion conditions in detail; the condition (10.2) for large sets is "left to the reader". The final step combines the truncation with Theorem 4.1.1 and a careful choice of parameters for the two ranges of $t$ .

Formalization scope

The Lean development lives in the namespace TalagrandConc.Assignment and commits to the following conventions:

$I = J =$ Fin N, assignments are Equiv.Perm (Fin N), and $L_N$ is optCost, a Finset.inf' over all permutations (no junk value).
The probability space is the cost matrices Fin N × Fin N → ℝ with costLaw N, the product of Lebesgue measure restricted to $[0,1]$ . The coordinates are the $X_{i,j}$ .
Cardinalities of subsets are Set.ncard on the finite type Fin N. $\alpha$ -expansion includes $\alpha \ge 2$ as part of the definition.
Probabilities are in ℝ≥0∞, and $1 - N^{-u/K}$ is truncated subtraction there.
Universal constants are existentially quantified before every object they are uniform over. $K(\delta)$ in Lemma 10.4 is chosen after $\delta$ and before everything else.
Implicit side conditions of the paper are stated: $m \ge 1$ in Lemma 10.1 and Corollary 10.2, $n \ge 1$ for the cycle, $N \ge 1$ in Proposition 10.3, $t \ge 0$ in Theorem 10.5.

A cycle of length $n = 0$ would satisfy Lemma 10.1 vacuously. The formal statement therefore requires $n \ge 1$ , which rules out that trivializing reading. Similarly, Theorem 10.5 fixes one constant $K$ for all $N$ ; a $K$ depending on $N$ would make the bound empty.

Infrastructure: the product of uniform laws on a finite index set, iterated expansion arguments for bipartite digraphs, a lower-tail Chernoff bound for independent events, and the union bound over subsets are reusable beyond this mission. Theorem 4.1.1 of the paper is posed elsewhere on the platform and is not restated here. The bound (8.1.1) used in Step 2 of the proof belongs to another chapter of the series. Contributions of proofs of any milestone, or of intermediate displayed estimates such as (10.5), (10.6) and (10.9), are welcome.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. doi:10.1007/BF02699376
D. W. Walkup, On the expected value of a random assignment problem, SIAM J. Comput. 8 (1979), 440–442. doi:10.1137/0208036
R. M. Karp, An upper bound on the expected cost of an optimal assignment, in Discrete Algorithms and Complexity, Academic Press (1987), 1–4.
J. M. Steele, Probability Theory and Combinatorial Optimization, SIAM (1997). doi:10.1137/1.9781611970029
D. J. Aldous, The ζ(2) limit in the random assignment problem, Random Structures Algorithms 18 (2001), 381–418. doi:10.1002/rsa.1015

7 thms3 active usersReviewed

Completed

Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces VIII: The Longest Increasing Subsequence — Gaussian Concentration of L_N around Its Median MTextbook

Why the longest increasing subsequence

Pick $N$ independent points $X_1, \dots, X_N$ uniformly in $[0,1]$ and let $L_N$ be the length of the longest increasing subsequence. Because the points are almost surely distinct, $L_N$ has the law of the longest increasing subsequence of a uniform random permutation of $\{1, \dots, N\}$ . This is Ulam's problem, one of the most studied random combinatorial quantities. Hammersley (1972) showed $\mathbb E L_N / \sqrt N$ converges, and Vershik–Kerov and Logan–Shepp (1977) identified the limit as $2$ . That leaves the size of the fluctuations of $L_N$ around its typical value.

Timeline.

Frieze (1991, [F] in the paper) and Bollobás–Brightwell (1992, [B-B]) proved concentration of $L_N$ around its mean with martingale methods, on deviation scales larger than $N^{1/4}$ .
Talagrand (1995), Section 7.1, derived from his convex hull inequality a two-sided Gaussian-type bound around the median on the scale $\sqrt{M_N} \asymp N^{1/4}$ , with explicit constants and no logarithmic loss. This is the target of the mission.
Baik, Deift and Johansson (1999) showed that the true fluctuations are of order $N^{1/6}$ , with Tracy–Widom limit law, so Talagrand's scale is not sharp. Its value is that it comes from a short, general principle.

Section 7.2 of the same paper applies the same idea to the longest common subsequence of two random words, a quantity tied to the edit distance used in genetics and speech recognition.

Setting

Let $\Omega = [0,1]$ and $N \ge 0$ . For $x = (x_1, \dots, x_N) \in \Omega^N$ , $L_N(x)$ is the largest integer $p$ for which there are indices $i_1 < \dots < i_p$ with $x_{i_1} \le \dots \le x_{i_p}$ . For $a > 0$ , the level set is $A(a) = \{x \in \Omega^N ;\ L_N(x) \le a\}$ .

Fix a probability $\mu$ on $[0,1]$ without atoms (Lebesgue measure, for instance) and let $P = \mu^{\otimes N}$ be the product probability on $\Omega^N$ ; the coordinates are the random points $X_i$ . A median of $L_N$ is a number $M$ with $P(L_N \le M) \ge 1/2$ and $P(L_N \ge M) \ge 1/2$ .

The tool is Talagrand's convex hull distance. For $A \subseteq \Omega^N$ and $x \in \Omega^N$ , let $U_A(x)$ be the set of $s \in \{0,1\}^N$ for which some $y \in A$ agrees with $x$ at every coordinate $i$ with $s_i = 0$ ; let $V_A(x)$ be its convex hull in $\mathbb R^N$ ; and let $f_c(A,x)$ be the Euclidean distance from $0$ to $V_A(x)$ (with $f_c(A,x) = +\infty$ if $A = \emptyset$ ).

A function $L_N : \Omega^N \to \mathbb N$ on an arbitrary probability space $(\Omega, \mu)$ is a configuration function if, for every $x$ , some set $J$ of exactly $L_N(x)$ coordinates satisfies $L_N(y) \ge \operatorname{card}\{i \in J ;\ y_i = x_i\}$ for all $y$ .

For two sequences $x = (x_1, \dots, x_N)$ and $y = (y_1, \dots, y_{N'})$ , $L_{N,N'}(x;y)$ is the largest $p$ with $i_1 < \dots < i_p$ , $j_1 < \dots < j_p$ and $x_{i_\ell} = y_{j_\ell}$ for all $\ell \le p$ .

Formalization targets

Goal: Theorem 7.1.2 (p. 153)

For every median $M$ of $L_N$ and every $u > 0$ ,

P(L_N \ge M + u) \le 2\exp\Big(-\frac{u^2}{4(M+u)}\Big), \qquad P(L_N \le M - u) \le 2\exp\Big(-\frac{u^2}{4M}\Big).

Milestones

Lemma 7.1.1 (p. 153). For $a > 0$ and every $x$ , $a \ge L_N(x) - f_c(A(a),x)\sqrt{L_N(x)}$ ; in particular $L_N(x) \ge a + v$ implies $f_c(A(a),x) \ge v/\sqrt{a+v}$ .
Theorem 7.1.3 (p. 154). The two bounds of the goal hold for every configuration function on any product probability space.
Eq. (7.2.3) (p. 155). For the longest common subsequence $L(x)$ of the two halves of $x \in [0,1]^{N+N'}$ : $a \ge L(x) - 2\sqrt2\, f_c(A(a),x)\sqrt{L(x)}$ .
Theorem 7.2.1 (p. 154). For two independent i.i.d. sequences with common real law and a median $M$ of $L_{N,N'}$ :

P(L_{N,N'} \ge M + u) \le 2\exp\Big(-\frac{u^2}{32(M+u)}\Big), \qquad P(L_{N,N'} \le M - u) \le 2\exp\Big(-\frac{u^2}{32M}\Big).

Significance

The result. Since $M_N$ is of order $\sqrt N$ , the goal confines $L_N$ to a window of width of order $N^{1/4}$ around its median with Gaussian-type tails. For $u$ much larger than $M$ the upper bound becomes exponential in $u$ , the natural tail of a quantity bounded by the size of a witnessing configuration. Theorem 7.1.3 isolates what is used: every integer quantity certified by a configuration of exactly its own size has the same concentration. This abstraction became the notion of certifiable functions used widely in random graph theory and probabilistic combinatorics (see the treatment of Talagrand's inequality in Alon–Spencer, The Probabilistic Method). For the longest common subsequence, the bound is useful when the alphabet is large and $M \ll N$ , where it improves on Azuma's inequality.

Formalizing it. All four results are proved in the paper; none is formalized in Lean as far as a search of the Prove2Me corpus shows. A finite-alphabet certifiable-function inequality (Talagrand.certifiable_concentration) has been posed on the platform as an open statement; it uses a Lipschitz hypothesis and no median, so it is a relative of Theorem 7.1.3, not the same statement. The mission produces a general- $\Omega$ formalization of the configuration-function principle, its application to the continuous Ulam problem, and the common-subsequence variant.

Difficulty

The deterministic inequalities (Lemma 7.1.1, Eq. (7.2.3)) relate the Euclidean distance $f_c$ , defined through a convex hull in $\mathbb R^N$ , to purely combinatorial counts of disagreeing coordinates; this needs the infimum defining $f_c$ to be attained and a duality between the convex hull and its extreme points. The probabilistic step rests on Talagrand's convex hull inequality (Theorem 4.1.1, Eq. (4.1.2)), $\int \exp(f_c^2(A,x)/4)\, dP(x) \le 1/P(A)$ , for a general product probability; that inequality is not in Mathlib. A bounded-difference (Azuma or McDiarmid) argument does not suffice: changing one point changes $L_N$ by at most $1$ , which gives deviations of order $\sqrt N$ , not $\sqrt M$ . The point of the configuration property is that only the $L_N(x)$ coordinates of a witness matter.

Formalization scope

Product space. $\Omega^N$ is Fin N → Ω (0-based), and $P$ is Measure.pi (fun _ => μ). For the goal, $\Omega$ is unitInterval and $\mu$ is any probability measure on it with $\mu\{t\} = 0$ for all $t$ . Theorem 7.2.1 uses the product of Measure.pi measures on (Fin N → ℝ) × (Fin N' → ℝ) for a probability $\mu$ on $\mathbb R$ . Eq. (7.2.3) lives on Fin (N + N') → unitInterval, with the first $N$ coordinates forming the first sequence.
Increasing means weakly increasing ( $\le$ ), as printed. Index sequences are strictly increasing maps Fin p → Fin N. $L_N$ and $L_{N,N'}$ take values in ℕ.
Convex hull distance. $f_c$ takes values in ℝ≥0∞, with the Euclidean norm written out as $\sqrt{\sum_i s_i^2}$ . Mathlib's default norm on Fin N → ℝ is the sup norm and would give a different, much weaker statement. The deterministic inequalities are stated in the rearranged form $L \le a + c\, f_c \sqrt L$ in $[0, +\infty]$ .
Median: $P(Z \le M) \ge 1/2$ and $P(Z \ge M) \ge 1/2$ ; the statements hold for every median.
Measurability. The paper treats all functions as measurable. In Theorem 7.1.3 this convention is the explicit hypothesis that the configuration function is measurable. The concrete $L_N$ and $L_{N,N'}$ carry no hypothesis.
Degenerate corner. When $M = 0$ , Lean's division gives $u^2/(4M) = 0$ , so the lower-tail bound reads " $\le 2$ ". The event $\{L \le -u\}$ is then empty, so no content is lost.
No trivialization. Using the sup norm in $f_c$ , using a real-valued infimum (which is $0$ on an empty $A(a)$ ), or putting the conclusion of Theorem 4.1.1 among the hypotheses would each make a statement trivial or empty. None of these is done.

The mission uses the shared definition of the convex hull distance from Section 4.1. A general- $\Omega$ proof of Eq. (4.1.2) and of the attainment of $f_c$ would be reusable for every Part II chapter of the paper. Contributions are welcome in particular for the deterministic Lemma 7.1.1 and Eq. (7.2.3), the measurability of $L_N$ and $L_{N,N'}$ , and the reduction of Theorem 7.1.2 to Theorem 7.1.3.

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
A. Frieze, On the length of the longest monotone subsequence in a random permutation, Ann. Appl. Probab. 1 (1991), 301–305. https://doi.org/10.1214/aoap/1177005939
B. Bollobás, G. Brightwell, The height of a random partial order: concentration of measure, Ann. Appl. Probab. 2 (1992), 1009–1018. https://projecteuclid.org/journals/annals-of-applied-probability/volume-2/issue-4
A. M. Vershik, S. V. Kerov, Asymptotics of the Plancherel measure of the symmetric group and the limiting form of Young tables, Soviet Math. Dokl. 18 (1977), 527–531.
J. Baik, P. Deift, K. Johansson, On the distribution of the length of the longest increasing subsequence of random permutations, J. Amer. Math. Soc. 12 (1999), 1119–1178. https://doi.org/10.1090/S0894-0347-99-00307-0
N. Alon, J. H. Spencer, The Probabilistic Method, 4th ed., Wiley, 2016. https://doi.org/10.1002/9781119062042

8 thms3 active usersReviewed

Completed

Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces II: The Two-Point Space — an N-Free Exponential Bound for the One-Sided Hamming Distance under a Second MeasureTextbook

Motivation

The concentration of measure phenomenon says that in a product probability space a set of probability not too small is "large" in the sense that most points lie within a small distance of it. M. Talagrand's 1995 memoir Concentration of measure and isoperimetric inequalities in product spaces develops this phenomenon through exponential moment bounds for distances to sets. Its Section 2.1 treats the Hamming distance on an arbitrary product space and recovers the bounds obtainable by martingale methods (McDiarmid, On the method of bounded differences, 1989).

Section 2.3, the subject of this mission, specialises to the two-point space $\{0,1\}^N$ with biased coordinates. This is the setting of the binomial law, of random subsets of a finite set, and of monotone properties of random graphs. Two things happen there that do not happen in general. First, the bias $p$ of the coordinates enters the bound through the variance $p(1-p)$ , which gives sharper tails when $p$ is close to $0$ or $1$ . Second, when one counts only the coordinates where $x$ has a $1$ and the point of $A$ has a $0$ , and measures $A$ under a second, more heavily biased product measure, the exponential moment bound becomes independent of the dimension $N$ . The paper calls this the first of its results that "apparently cannot be obtained via martingales". Bounds of this one-sided kind are the natural tool for upper tails of increasing functions on the biased cube, the regime of the binomial law near $Np_1$ when samples are drawn at rate $p<p_1$ .

Setting

Let $\Omega=\{0,1\}$ . For $p\in[0,1]$ let $\mu$ be the probability on $\Omega$ with $\mu(\{1\})=p$ , $\mu(\{0\})=1-p$ , and let $P=\mu^N$ be the product probability on $\Omega^N$ , whose points are written $x=(x_1,\dots,x_N)$ . For a set $A\subseteq\Omega^N$ and a point $x\in\Omega^N$ , the Hamming distance from $x$ to $A$ is

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

the least number of coordinates of $x$ that must be changed to land in $A$ . The one-sided distance counts only changes from $1$ to $0$ :

f^{+}(A,x)=\min\big\{\operatorname{card}\{i\le N:\ x_i=1,\ y_i=0\}:\ y\in A\big\}.

Both are $+\infty$ when $A$ is empty. A second probability $\mu_1$ on $\Omega$ has $p_1=\mu_1(\{1\})$ , and $P_1=\mu_1^N$ . For $\alpha>0$ and $t\ge 0$ the paper uses two constants,

b(\alpha,t,p)=((1-p)e^{t}+p)(p+(1-p)e^{-t/\alpha})^{\alpha}\quad(p\ge \tfrac12),\qquad b(\alpha,t,p)=b(\alpha,t,1-p)\quad(p\le\tfrac12),

a(\alpha,t)=\max\Big(1,\ (1-p+pe^{t})(p_1e^{-t/\alpha}+1-p_1)^{\alpha}\Big).

In the Lean development these are hammingDistToSet, oneSidedDistToSet, bConst, aConst, the measure productMeasure N p, and the integrand expMul t z $=e^{tz}$ .

Formalization targets

Goal: Theorem 2.3.4

If $p_1>p$ , then for every $N$ , every $A\subseteq\Omega^N$ , every $\alpha>0$ and every $t\ge 0$ ,

\int e^{t f^{+}(A,x)}\,dP(x)\le\frac{a(\alpha,t)^N}{P_1(A)^{\alpha}}.

For small $t$ one has $a(\alpha,t)=1$ . When $0<p<p_1<1$ and $\alpha=1$ , the paper's explicit threshold is $e^{t}\le p_1(1-p)/(p(1-p_1))$ . At equality, the bound becomes $\int (p_1(1-p)/(p(1-p_1)))^{f^{+}(A,x)}dP\le 1/P_1(A)$ , with no dependence on $N$ . The main theorem also includes the endpoint cases $p=0$ and $p_1=1$ without using this ratio.

Milestones

Proposition 2.3.1. For $t\ge0$ , $\alpha\ge1$ : $\displaystyle\int e^{tf(A,x)}\,dP(x)\le \frac{b(\alpha,t,p)^N}{P(A)^\alpha}$ .
Corollary 2.3.2, Eq. (2.3.4). There is a universal $K$ such that for $\alpha\ge1$ , $0\le t\le1$ :

\int e^{tf(A,x)}\,dP(x)\le\frac{1}{P(A)^\alpha}\exp N\Big[p(1-p)\Big(1+\frac1\alpha\Big)\frac{t^2}{2}+Kt^3\Big].

Corollary 2.3.2, Eq. (2.3.5). There is a universal $K$ such that for $(4p(1-p)N\log\frac1{P(A)})^{1/2}\le k\le p(1-p)N$ :

P(\{f(A,x)\ge k\})\le\exp\Big(-\frac{1}{2p(1-p)N}\Big(k-\sqrt{2p(1-p)N\log\tfrac{1}{P(A)}}\Big)^2+\frac{Kk^3}{(p(1-p))^3N^2}\Big).

Lemma 2.3.5. If $a\le b\le 1$ , then

\frac{1-p}{b^{\alpha}}+p\min\Big(\frac{1}{a^{\alpha}},\frac{e^{t}}{b^{\alpha}}\Big)\le\frac{a(\alpha,t)}{(ap_1+b(1-p_1))^{\alpha}}.

Milestones 1–3 concern the two-sided Hamming distance; milestone 4 is the one-coordinate inequality behind the goal.

Significance

The results. Proposition 2.3.1 and Corollary 2.3.2 give, for every set $A$ in the biased cube, a tail bound for the Hamming distance whose Gaussian part has the variance $p(1-p)N$ of the binomial law, not the worst case $N/4$ . The paper notes that this matches the quality of the optimal isoperimetric inequalities that are known only for hereditary (monotone) sets. Theorem 2.3.4 is a statement with no dimension in it: it controls how many $1$ s of a $\mu^N$ -sample must be switched off to reach a set $A$ that is not small under the more biased $\mu_1^N$ .

Formalizing it. These results are proved in the paper; the local Prove2Me index contains no machine-checked proof of these statements. Mathlib has the Bernoulli measure, finite products of measures and lower Lebesgue integrals, but no exponential moment bound for these distances to sets. A complete development would add reusable facts about biased Boolean products, their distance functions and exponential moments, and the uniform cubic error term in Corollary 2.3.2.

Difficulty

The obvious route to a Hamming-distance tail bound is a martingale (bounded differences) argument. It yields $e^{-2k^2/N}$ -type bounds that do not see the bias $p$ , and its variance proxy grows with $N$ , so it gives no bound independent of $N$ ; the paper states that Theorem 2.3.4 apparently cannot be obtained this way. Theorem 2.3.4 measures $A$ under $P_1$ while the integral is under $P$ , so a one-coordinate estimate must account for two different probabilities and keep the factor $a(\alpha,t)$ exactly equal to $1$ for small $t$ . Lemma 2.3.5 must handle $a=0$ as well as interior values. Corollary 2.3.2 requires a cubic error bound uniform in $p\in[0,1]$ and $\alpha\ge1$ .

Formalization scope

$\Omega$ is Bool with $1$ = true; $P$ reuses the published TalagrandCore.bernPi Bernoulli product measure with p : unitInterval converted to a nonnegative real, over Fin N (0-based coordinates). Every subset of $\{0,1\}^N$ is measurable, so the paper's convention of ignoring measurability costs nothing here.
Distances take values in ℝ≥0∞, with $f(\emptyset,x)=+\infty$ ; integrals are lower Lebesgue integrals ∫⁻ in $[0,\infty]$ ; $P(A)^{-\alpha}$ is computed in $[0,\infty]$ , so $P(A)=0$ gives $+\infty$ .
Theorem 2.3.4 and Lemma 2.3.5 are stated for $\alpha>0$ , the range under which Section 2.2 introduces the exponent $\alpha$ (the theorem's page does not restate it). Proposition 2.3.1 and Corollary 2.3.2 keep the page's $\alpha\ge 1$ . The standing hypothesis $p_1>p$ appears as a binder.
The universal constants of Corollary 2.3.2 are quantified before $p$ , $N$ , $A$ , $\alpha$ , $t$ , $k$ . In Eq. (2.3.5), $0<p<1$ , $N\ge1$ and $P(A)>0$ are assumed, which is where the displayed formula is defined.
A trivializing formalization is ruled out: the integrals are not Bochner integrals (which vanish on non-integrable functions), the empty set and $P_1(A)=0$ are handled through $+\infty$ , not junk zeros, and the two different distances of the section carry different names.

The mission also imports the published TalagrandCore.bernPi definition for the Boolean product law. Reusable pieces include evaluation of $\int$ over $\{0,1\}$ under a Bernoulli measure and facts about product measures over Fin N. Contributions to any of the four milestones or the goal 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 Series 141 (1989), 148–188. https://doi.org/10.1017/CBO9781107359949.008
M. Ledoux, The Concentration of Measure Phenomenon, AMS Mathematical Surveys and Monographs 89 (2001). https://doi.org/10.1090/surv/089

8 thms3 active usersReviewed

Completed

Number Theory Probability Theoretical Computer Science·Captain: mikedeng1

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

Motivation

A pseudorandom number generator replaces repeated random sampling with a deterministic update of a small state. Its useful lifetime depends on the length and structure of the resulting orbit. In Marsaglia and Zaman’s 1991 paper, the subtract-with-borrow generators use only digit subtraction and a one-bit borrow while attaining cycles that can be almost as long as the whole set of digit tuples. The mathematical question is exact: which fraction encodes an output sequence, when does an arbitrary seed enter a cycle, and how long is that cycle?

This mission concerns the paper’s first subtract-with-borrow rule, called Method 1 in §4.5. The paper also studies a second rule that reverses the order of the two subtracted digits. Its modulus and period analysis differ. The distinction matters because the same state format supports both rules while their arithmetic claims are different.

Setting

Choose an integer base $b\ge2$ and lags $0<s<r$ . A state is a row of $r$ digits and one borrow bit, $(x_1,\ldots,x_r,c)$ , where each $x_i$ is in $\{0,\ldots,b-1\}$ and $c\in\{0,1\}$ . The leftmost digit $x_1$ is the oldest. One update discards it, shifts the remaining digits left, and appends a new digit. Put $t=x_{r+1-s}-x_1-c$ . If $t\ge0$ , the appended digit is $t$ and the new borrow is zero. If $t<0$ , the appended digit is $t+b$ and the new borrow is one. Write this deterministic map as $f$ .

The digits emitted after the seed obey $x_n=x_{n-s}-x_{n-r}-c$ modulo $b$ , with $c$ updated at each step. The associated modulus is $m=b^r-b^s+1$ . For $0\le k<m$ , write $d_j(k/m)$ for the $j$ th digit after the point in the base- $b$ expansion of $k/m$ , with $j\ge1$ . The digit stream is read in reverse order when it is matched to an expansion: the latest generated digit in a finite block is the first fractional digit. A state is strictly periodic when it is already on a cycle under $f$ ; otherwise it may pass through a transient before reaching one.

Two states have period one: $(0,\ldots,0,0)$ and $(b-1,\ldots,b-1,1)$ . These are the trivial seeds. They are exceptions to the order-of-base period formula. A third useful object is the multiplicative order $\operatorname{ord}_m(b)$ , the least positive $p$ for which $b^p\equiv1\pmod m$ . Since $m\equiv1\pmod b$ , the base is coprime to this modulus.

Formalization targets

Exact cycle period

For prime $m=b^r-b^s+1$ and any nontrivial seed $z$ , the goal identifies the minimal state period after the transient:

\operatorname{period}_f\bigl(f^r(z)\bigr)=\operatorname{ord}_m(b).

The assertion includes both that $f^r(z)$ is on a cycle and that its period is exactly the order. It makes no primitive-root assumption. If $b$ is a primitive root modulo $m$ , the right side specializes to $m-1=b^r-b^s$ , the full period discussed in §3 of the paper.

Supporting results

The milestones state that the fractional digits of $k/m$ have least period $\operatorname{ord}_m(b)$ when $k$ and $b$ are coprime to $m$ ; that a primitive root yields digit period $m-1$ ; that the two trivial seeds are precisely the fixed points; and that every seed reaches a cycle after at most $r$ updates. They also formalize the reverse-digit relation for every finite generated block and the paper’s Method 1 inequalities that classify nontrivial seeds already on a cycle. These targets use the paper’s own claims in §§4.1, 4.3, and 4.5 rather than an arbitrary decomposition of the goal.

Significance

The result converts the orbit-length problem of a digit-and-borrow machine into a multiplicative-order calculation in a finite residue ring. A prime modulus and a primitive base produce a nontrivial cycle of length $m-1$ ; a nonprimitive base still has the exact order-of-base period. The seed classification separates states already on that cycle from states with an initial transient. These statements are what allow a proposed numerical parameter set to be assessed mathematically before the generator is used.

Marsaglia and Zaman proved these results in the cited paper. This mission asks for machine-checked Lean proofs of the statements, starting from an explicit finite-state update. The reusable output includes exact base- $b$ digit arithmetic, links between digit periods and multiplicative order, and methods for reasoning about the eventual cycles of finite-state digit generators. The present proposal consists of compiled statements and definitions; the theorem bodies are open proof targets.

Difficulty

Finiteness alone shows that every state eventually repeats, but it gives neither the bound of $r$ steps nor the exact cycle length. Likewise, observing that a generated digit block matches a prefix of some fraction does not by itself identify one period for the whole state orbit. The proof must keep track of the borrow bit and the direction in which the digit block is read. It must also show that a nontrivial seed does not collapse to one of the two fixed states. The source’s integer tableaux explain the arithmetic link, but turning their finite strings into a statement uniform over every seed and every block length is the main formalization challenge.

Formalization scope

Lean represents digits by Fin b, the borrow by Fin 2, and the row by a function on Fin r. Lean index zero is $x_1$ , so the digit used in the update, $x_{r+1-s}$ , has index $r-s$ . The update branches on an ordinary integer comparison before any natural-number subtraction can truncate a negative value. The modulus is a natural number, and $0<s<r$ with $b\ge2$ makes $b^r-b^s$ an exact subtraction. The $j$ th fractional digit is computed by an exact quotient and remainder; only $j\ge1$ has the mathematical meaning used in the theorems. The generated stream is one-based, and the first digit beyond the seed is $x_{r+1}$ .

The paper’s “after a few iterations” is pinned to its stated upper bound “at most $r$ .” Its “period” is the minimal positive state period of $f^r(z)$ , not a mere period divisor or the period of an arbitrarily selected digit window. “Appropriately chosen” parameters mean a prime $m$ for the goal and exclusion of the two named fixed seeds. The reverse-digit milestone permits the numerator $k$ to depend on the finite endpoint, as the tableau argument does. No seed is excluded from the at-most- $r$ milestone.

The discussion on pp. 473–474 prints the Method 1 seed inequalities in the opposite direction from the Method 1 listing on p. 472. The Lean seed-classification milestone uses the p. 472 directions, which agree with the step map on p. 466 and with direct finite checks. The §5 claim that every five-tuple except the $100$ patterns $xyxyx$ appears once in the special $b=10,r=5,s=2$ full cycle is left for a later extension. The other subtraction order, its modulus $b^r-b^s-1$ , and the paper’s large parameter certificates are outside this mission.

An encoding that merely asserts the existence of some period, allows an impossible seed hypothesis, or replaces the update by a different subtraction order would make the goal vacuous or change the result. The intended development needs Mathlib’s ZMod, multiplicative order, finite iterations, periodic points, and natural-number quotient and remainder. Contributions proving the numbered milestones, strengthening their arithmetic interfaces, or closing the goal are in scope.

Selected references

G. Marsaglia and A. Zaman, A new class of random number generators, The Annals of Applied Probability 1(3), 462–480 (1991). DOI: 10.1214/aoap/1177005878.

17 thms3 active usersReviewed

Completed

Linear Optimization Operations Research Theoretical Computer Science·Captain: mikedeng1

Approximation Algorithms for Scheduling Unrelated Parallel Machines 2: Enumerating Long Assignments and Rounding the LP Gives a (1 + ε)-Approximation for MakespanResearch Paper

Motivation

Scheduling independent jobs on unrelated parallel machines to minimize the makespan is one of the basic NP-hard problems of scheduling theory: each job has its own processing time on each machine, with no relation between machines, and the goal is to finish all jobs as early as possible. When the number of machines is part of the input, Lenstra, Shmoys and Tardos showed that no polynomial algorithm can come within a factor below 3/2 of the optimum unless P = NP. When the number of machines $m$ is a fixed constant, the picture is different: the problem admits a polynomial approximation scheme, a family of algorithms that reach any accuracy $1+\varepsilon$ .

Such a scheme was already known. Horowitz and Sahni (1976) gave a fully polynomial approximation scheme for fixed $m$ , but its space requirement grows like $(nm/\varepsilon)^m$ . The second application of the Rounding Theorem in the 1987 report of Lenstra, Shmoys and Tardos is a scheme whose space is polynomial in the input size, in $m$ , and in $\log(1/\varepsilon)$ . This mission formalizes the approximation guarantee of that scheme (Theorem 3 of the report).

Timeline:

1976. Horowitz and Sahni, a fully polynomial approximation scheme for a fixed number of unrelated machines, with exponential space in $m$ .
1985. Potts, a 2-approximation for unrelated machines whose running time is $m^{m-1}$ times a polynomial, based on LP rounding with enumeration.
1987. Lenstra, Shmoys and Tardos, the Rounding Theorem, a polynomial 2-approximation for arbitrary $m$ , and, for fixed $m$ , the scheme formalized here (FOCS 1987; journal version in Mathematical Programming 46, 1990).

Setting

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

Fix an integer deadline $d\ge0$ and an accuracy $\varepsilon>0$ . Assigning job $j$ to machine $i$ is long if $p_{ij}>\varepsilon d$ and short otherwise. A schedule of long assignments $L$ is a partial assignment of jobs to machines using only long assignments; its long load on machine $i$ is $t_i$ , and $L$ is admissible if $t_i\le d$ for every $i$ .

For a threshold $t$ and deadlines $d_1,\dots,d_m$ , the linear program (LP) of the Rounding Theorem has a variable $x_{ij}\ge0$ for every pair with $p_{ij}\le t$ , the constraints $\sum_i x_{ij}=1$ for each job, and $\sum_j p_{ij}x_{ij}\le d_i$ for each machine. The residual LP of $(d,L)$ is (LP) for the jobs left unassigned by $L$ , with $d_i=d-t_i$ and $t=\varepsilon d$ .

The procedure $A_\varepsilon$ , on input $d$ , tries every admissible $L$ ; if the residual LP is feasible it takes a vertex $\tilde x$ , rounds it to a 0-1 solution of the integer program (IP) of the Rounding Theorem, and combines the result with $L$ . It answers 'no' if no residual LP is feasible. A $\rho$ -relaxed decision procedure answers 'no' only when no schedule has makespan at most $d$ , and otherwise returns a schedule of makespan at most $\rho d$ . The binary search of Lemma 1 runs such a procedure on deadlines between $\lceil t/m\rceil$ and $t$ , where $t$ is the makespan of the greedy schedule, and returns the best schedule found.

Formalization targets

Goal: Theorem 3

For every $m\ge1$ , every positive integer matrix $P$ , every $\varepsilon>0$ , every LP solver $V$ , the procedure $A_\varepsilon$ run with $V$ exists, and the binary search driven by any such procedure returns a schedule $\sigma$ with

\mathrm{makespan}(\sigma)\le(1+\varepsilon)\,\mathrm{OPT}.

Milestones (§3, p. 6)

Every machine in an admissible $L$ carries fewer than $1/\varepsilon$ long assignments, and for $n,m\ge1$

\#\{L\text{ admissible}\}<(n+1)^{m/\varepsilon}.

If some schedule has makespan at most $d$ , its long part is admissible and its short part is a feasible solution of the residual LP.
If the short assignments take at most $d-t_i+\varepsilon d$ on machine $i$ , the combined schedule has load at most $(1+\varepsilon)d$ on every machine.
$A_\varepsilon$ exists for every LP solver and is a $(1+\varepsilon)$ -relaxed decision procedure.

Significance

Theorem 3 shows that for a fixed number of unrelated machines, the makespan can be approximated to any accuracy in polynomial time while keeping the memory polynomial in $\log(1/\varepsilon)$ . It is an early instance of the pattern "enumerate the large items, solve an LP for the small ones, round", which recurs in later approximation schemes for scheduling and packing. Together with the 2-approximation of the same paper (mission 1 of this series) and the 3/2 hardness bound (mission 3), it delimits what is achievable for unrelated machines.

The theorem is proved in the paper; none of it is known to have a machine-checked proof. Formalizing it requires a precise account of the enumeration of long assignments, the residual LP, and the binary search, and it exercises the Rounding Theorem, which this series poses in mission 1, outside its original setting (with a non-integral threshold $t=\varepsilon d$ ).

Difficulty

The arithmetic of the scheme is short; the content lies in the Rounding Theorem, which turns a vertex of the residual LP into a 0-1 schedule exceeding each deadline by at most the threshold. The obvious argument, rounding an arbitrary feasible LP solution, fails: a non-vertex solution may split many jobs across many machines, and rounding them can overload a machine by far more than $t$ . The bound depends on the structure of vertices of (LP), which an arbitrary feasible point does not have. A second difficulty is the count of milestone 1, which must be done with a real exponent $m/\varepsilon$ and a strict inequality.

Formalization scope

Machines are Fin m, jobs Fin n, processing times a matrix P : Matrix (Fin m) (Fin n) ℕ with all entries positive. Load, makespan and optimal schedules are those of the published MatousekLP.Scheduling.Schedule, applied to the real cast of P.
A vertex of an LP is a point of Set.extremePoints of its feasible region. Variables absent from the paper's (LP) are kept as matrix entries fixed to $0$ , which leaves the vertices unchanged.
The LP solver is a parameter (a vertex selector) and $A_\varepsilon$ is a predicate on procedures: each answer must extend an admissible schedule of long assignments, round the selected vertex within its support, and satisfy the (IP) load bound. The guarantee is proved for every such procedure. The output is thereby tied to what the algorithm computes, so the bound is not witnessed by an optimal schedule.
The binary search is a definition: greedy start, $l=\lceil t/m\rceil$ (the paper's $t/m$ rounded up because makespans are integers), $d=\lfloor(u+l)/2\rfloor$ , best stored schedule as output.
Not formalized: that $m$ is fixed, the polynomial running time, and the space bound polynomial in $m$ , $\log(1/\varepsilon)$ and the input size. The guarantee is stated for every $m\ge1$ . The count $(n+1)^{m/\varepsilon}$ of milestone 1, on which the running-time claim rests, is formalized, with the real power Real.rpow.
The constants are exact: $1+\varepsilon$ , $(n+1)^{m/\varepsilon}$ , $d-t_i+\varepsilon d$ . Milestone 1 needs $n\ge1$ and $m\ge1$ for strictness.
Theorem 1 (the Rounding Theorem) and Lemma 1 are milestones of mission 1 of this series and are not restated here.

Welcome contributions: a proof of the Rounding Theorem in the generality of real deadlines and thresholds, proofs of the counting bound, and lemmas on the binary search that are reusable for any relaxed decision procedure.

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; Theorem 3, p. 6). Journal version: Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
E. Horowitz, S. Sahni, Exact and approximate algorithms for scheduling nonidentical processors, Journal of the ACM 23 (1976) 317–327. https://doi.org/10.1145/321941.321951
C.N. Potts, Analysis of a linear programming heuristic for scheduling unrelated parallel machines, Discrete Applied Mathematics 10 (1985) 155–164. https://doi.org/10.1016/0166-218X(85)90009-5
D.S. Hochbaum, D.B. Shmoys, Using dual approximation algorithms for scheduling problems: theoretical and practical results, Journal of the ACM 34 (1987) 144–162. https://doi.org/10.1145/7531.7535

10 thms3 active usersReviewed

Completed

Graph Theory·Captain: mikedeng1

The Four-Colour Theorem: Birkhoff's Lemma (6.4) — Every Non-Empty Consistent Set of Edge-Colourings of a Ring of Length 5 Meeting ℰ Includes One of 𝒞ᵢ, 𝒟ᵢ, ℰResearch Paper

Motivation

The Four-Colour Theorem was proved by Appel and Haken (1976–77) and re-proved by Robertson, Sanders, Seymour and Thomas (RSST, 1997) with a simpler, fully computer-checkable argument. Both proofs rest on reducibility: a configuration is reducible when every 4-colouring of the ring around it can be modified, by Kempe-chain recolouring, into one that extends inside. RSST make this precise with a purely combinatorial notion, the consistent set of edge-colourings of a circuit (§3 of their paper), which captures exactly which boundary colourings Kempe interchanges can reach from one another.

The oldest results about consistent sets predate the computer proofs. G. D. Birkhoff (1913) analysed rings of length 4 and 5 and showed that the possible "Kempe-closed" sets of boundary colourings on such short rings are very restricted. RSST restate Birkhoff's analysis in their language as (6.3) (rings of length 4) and (6.4) (rings of length 5). These two lemmas power the short-circuit subroutine of their quadratic 4-colouring algorithm (6.5), which colours a triangulation across a separating circuit of length 4 or 5.

Timeline:

1879–1890. Kempe introduces chain interchanges; Heawood finds the gap in Kempe's argument.
1913. Birkhoff, The reducibility of maps, studies rings of small size and introduces reducibility.
1976–77. Appel and Haken prove the Four-Colour Theorem.
1997. Robertson, Sanders, Seymour and Thomas give a new proof and an $O(n^2)$ colouring algorithm; consistent sets and lemmas (6.3), (6.4) appear in §§3 and 6.
2005–08. Gonthier formalizes the Four-Colour Theorem in Coq, with a different encoding of Kempe closure (chromograms on hypermaps).

Setting

Let $R$ be a circuit of length $k$ : a cycle with edges $e_1, \dots, e_k$ in order, with no repeated vertices or edges. An edge-colouring of $R$ is a map $\kappa : E(R) \to \{-1, 0, 1\}$ .

A match is an unordered pair $\{e, f\}$ of distinct edges, and a signed match is a pair $(\{e,f\}, \mu)$ with $\mu = \pm 1$ . A signed matching is a set $M$ of signed matches such that for any two distinct members $(\{e,f\},\mu)$ , $(\{e',f'\},\mu')$ : the pairs $\{e,f\}$ and $\{e',f'\}$ are disjoint, and $e, f$ lie in the same component of $R$ with $e'$ and $f'$ deleted. Write $E(M)$ for the edges covered by $M$ .

For $\theta \in \{-1,0,1\}$ , the colouring $\kappa$ $\theta$ -fits $M$ when $E(M)$ is exactly the set of edges with $\kappa(e) \neq \theta$ , and for each $(\{e,f\},\mu) \in M$ , $\kappa(e) = \kappa(f)$ holds if and only if $\mu = 1$ . A set $\mathcal C$ of edge-colourings is consistent if for every $\kappa \in \mathcal C$ and every $\theta$ there is a signed matching $M$ that $\kappa$ $\theta$ -fits such that $\mathcal C$ contains every edge-colouring that $\theta$ -fits $M$ .

Two edge-colourings are equivalent if one is obtained from the other by a permutation $\lambda$ of $\{-1,0,1\}$ . On the circuit of length 5, $\mathcal A_{ij}$ ( $i \neq j$ ) is the equivalence class of the colouring that is $1$ on $e_i$ , $-1$ on $e_j$ and $0$ elsewhere. Then $\mathcal C_i = \mathcal A_{ij} \cup \mathcal A_{ik} \cup \mathcal A_{jk}$ , where $e_j, e_k$ are the two edges sharing an end with $e_i$ ; $\mathcal D_i = \mathcal A_{ac} \cup \mathcal A_{ad} \cup \mathcal A_{bc} \cup \mathcal A_{bd}$ , where $e_a, e_b, e_c, e_d$ are the other edges in order; and $\mathcal E = \mathcal A_{12} \cup \mathcal A_{23} \cup \mathcal A_{34} \cup \mathcal A_{45} \cup \mathcal A_{15}$ . In Lean these are A, C5, D5, E5, and Consistent.

Formalization targets

Goal: Birkhoff's lemma for rings of length 5, (6.4)

\mathcal C \text{ consistent},\ \mathcal C \neq \emptyset,\ \mathcal C \cap \mathcal E \neq \emptyset \;\Longrightarrow\; \exists i,\ \mathcal C_i \subseteq \mathcal C \ \ \text{or}\ \ \exists i,\ \mathcal D_i \subseteq \mathcal C \ \ \text{or}\ \ \mathcal E \subseteq \mathcal C.

Milestones

Every consistent set is a union of equivalence classes (§6, p. 25): $\kappa \in \mathcal C \Rightarrow [\kappa] \subseteq \mathcal C$ .
Claim (1) of the proof of (6.4): if $\mathcal A_{12} \subseteq \mathcal C$ then $\mathcal C$ includes one of $\mathcal A_{13}, \mathcal A_{15}$ and one of $\mathcal A_{23}, \mathcal A_{25}$ .
Claim (2): if $\mathcal A_{13} \subseteq \mathcal C$ then $\mathcal C$ includes one of $\mathcal A_{23}, \mathcal A_{35}$ .
The closure facts of §3, p. 8: $\emptyset$ is consistent, unions of two consistent sets are consistent, and every set $\mathcal S$ has a unique maximal consistent subset $\mathcal S'$ .

Companion: Birkhoff's lemma for rings of length 4, (6.3)

With $\mathcal C_0, \dots, \mathcal C_3$ the classes of $(0,0,0,0)$ , $(0,1,1,0)$ , $(0,1,0,1)$ , $(0,0,1,1)$ , every non-empty consistent set includes one of $\mathcal C_0 \cup \mathcal C_1$ , $\mathcal C_1 \cup \mathcal C_2$ , $\mathcal C_2 \cup \mathcal C_3$ , $\mathcal C_3 \cup \mathcal C_0$ .

Significance

The result. (6.3) and (6.4) say that on rings of length at most 5 the Kempe-closed families of boundary colourings are rigid: a non-empty consistent family always contains one of a short explicit list of families. This is what makes separating circuits of length 4 and 5 harmless in a minimal counterexample and in the RSST colouring algorithm: whatever colourings one side of the circuit admits, the other side can be made to agree after Kempe changes.

Formalizing it. The Four-Colour Theorem itself is machine-checked (Gonthier, Coq), but that proof uses a different combinatorial encoding; RSST's notion of a consistent set, their signed matchings, and Birkhoff's ring lemmas in their formulation have no machine-checked version. The Four-Colour Theorem as such is not part of this mission; it is posed separately on the platform as the open goal FourColor.four_color. This mission builds the self-contained §3 layer (consistency) that RSST's reducibility computations rest on, proves two of its basic structural facts, and proves the two Birkhoff lemmas the paper uses. The definitions are reusable for a later formalization of (3.1) (lifts of tri-colourings form a consistent set) and of D-reducibility.

Difficulty

The statements are about finite objects: on a 5-ring there are $3^5 = 243$ edge-colourings, and the signed matchings have at most two matches. The difficulty lies elsewhere. Consistency quantifies over every member of $\mathcal C$ , every $\theta$ and the existence of a signed matching together with a closure property, so a consistent set cannot be checked locally. The component condition on signed matchings is a statement about connectivity in a graph with two edges deleted, which must be connected to elementary arithmetic on the cycle before anything can be computed. An argument by brute force over all $2^{243}$ subsets is infeasible, so a proof has to pass through the structure of the classes $\mathcal A_{ij}$ . The paper's own proof also uses the dihedral symmetry of the 5-ring without stating it as a lemma; it is not a milestone.

Formalization scope

The circuit of length $k$ is SimpleGraph.cycleGraph k on Fin k; its edges are indexed by Fin k, edge $i$ being $\{i, i+1\}$ (mod $k$ ). The paper's $e_i$ is edge $i-1$ : $\mathcal A_{12}$ is A 0 1, $\mathcal A_{15}$ is A 0 4, $\mathcal A_{25}$ is A 1 4, $\mathcal A_{35}$ is A 2 4.
Colours are Mathlib's SignType; an edge-colouring is Fin k → SignType; $\mu \in$ ℤˣ; a match is a non-diagonal Sym2 (Fin k) of edge indices; a signed matching is a Set.
The component condition is encoded literally with deleteEdges and Reachable, for both orders of every distinct pair; both halves of "consistent" are kept; equivalence uses Equiv.Perm SignType.
C5 i uses edges $i \pm 1$ ; D5 i uses $(a,b,c,d) = (i+1, i+2, i+3, i+4)$ mod 5, the order along the path $R - e_i$ , which is the reading the paper's proof requires ( $\mathcal D_4 \supseteq \mathcal A_{25}, \mathcal A_{12}, \mathcal A_{13}, \mathcal A_{35}$ ).
General- $k$ statements assume $k \ge 3$ : circuits of length at most 2 have parallel edges and are not cycle graphs.
Ruled out: dropping the component condition (crossing pairs would become signed matchings), a one-sided "consistent" (every set would be consistent and (6.4) false), any use of the junk class A i i, and degenerate circuits.

All definitions are in one file, FourColourRSST.Ring.Setting. Proofs of any item are welcome, as are lemmas making consistency decidable on small rings and the symmetry of the 5-ring under rotations and reflections.

Selected references

N. Robertson, D. P. Sanders, P. Seymour, R. Thomas, The Four-Colour Theorem, J. Combin. Theory Ser. B 70 (1997), 2–44. https://doi.org/10.1006/jctb.1997.1750
G. D. Birkhoff, The reducibility of maps, Amer. J. Math. 35 (1913), 115–128. https://doi.org/10.2307/2370276
K. Appel, W. Haken, Every planar map is four colorable. Part I: Discharging, Illinois J. Math. 21 (1977), 429–490. https://doi.org/10.1215/ijm/1256049011
G. Gonthier, Formal proof — the Four-Color Theorem, Notices Amer. Math. Soc. 55 (2008), 1382–1393. https://www.ams.org/notices/200811/tx081101382p.pdf

6 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Application of the Branch and Bound Technique to Some Flow-Shop Scheduling Problems 3: Shifting and Scaling the Processing Times Changes Neither the Optimal Sequence nor the Branch-and-Bound PathResearch Paper

Motivation

Branch and bound was introduced for integer programming by Land and Doig (1960) and for the travelling salesman problem by Little, Murty, Sweeney and Karel (1963). Ignall and Schrage (1965) were among the first to apply it to machine scheduling. They give lower bounds for two permutation flow-shop problems: the makespan on three machines, and the mean completion time on two. Their Appendix then asks how the method depends on the units and the origin of the data. Its THEOREM says that changing the location and the scale of all processing times changes neither the optimal sequence nor the path the branch-and-bound procedure takes.

The statement matters for computational experiments of the kind the paper reports. Run times and node counts measured on one jobset carry over to every jobset obtained from it by a positive affine change of the processing times, so a test family need only vary the shape of the data, not its location and scale. It is also a correctness property of the procedure: a branch-and-bound method whose behaviour depended on the time unit would be suspect.

Setting

There are $n$ jobs, and every job visits the machines in the same order: $A$ , then $B$ (two-machine problem), or $A$ , $B$ , then $C$ (three-machine problem). Job $i$ has nonnegative processing times $a_i, b_i$ (and $c_i$ ). Following Johnson (1954), both problems are restricted to permutation schedules. A full sequence $\sigma$ lists the jobs in the order in which every machine processes them, and each operation starts as early as possible. The makespan of $\sigma$ is the time machine $C$ finishes its last job. The completion time $d_i$ of job $i$ is the time machine $B$ finishes it, and the two-machine objective is $\sum_i d_i$ , which is $n$ times the mean completion time.

A node $J_r$ is a partial sequence of $r$ distinct jobs, and $\bar J_r$ is the set of the $n-r$ jobs it has not scheduled. For three machines, $\mathrm{TIMEA}, \mathrm{TIMEB}, \mathrm{TIMEC}(J_r)$ are the times the machines finish $J_r$ , and the lower bound (p. 401) is

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

For two machines, $\hat T_r$ and $\hat S_r$ are the minima over orderings of $\bar J_r$ of two explicit sums $T_r$ , $S_r$ (pp. 405–406), and the lower bound is $LB(J_r)=\sum_{i\in J_r}d_i+\max(\hat T_r,\hat S_r)$ .

The branch-and-bound procedure (p. 402) keeps a list of nodes ranked by $LB$ , starting from the root alone. At each step it removes the first node and inserts each of its children $J_r\,j$ ranked into the list. On ties a new node goes before an old one (p. 403). It stops when the first node has scheduled $n-1$ jobs, which fixes the whole sequence. The list after $k$ steps is $\mathrm{run}_{LB}(k)$ .

Problems $P'$ (data $a'_i,b'_i,c'_i$ ) and $\tilde P$ are related by a change of location and scale when

\tilde a_i = H(a'_i+G),\qquad \tilde b_i=H(b'_i+G),\qquad \tilde c_i = H(c'_i+G),\qquad H,G>0.

Formalization targets

Goal: the Appendix THEOREM (p. 411)

For both the three-machine makespan problem and the two-machine sum-of-completion-times problem:

\sigma \text{ is optimal for } \tilde P \iff \sigma \text{ is optimal for } P', \qquad \mathrm{run}_{LB_{\tilde P}}(k)=\mathrm{run}_{LB_{P'}}(k)\ \text{ for all } k .

Milestones, in the order of the paper's proof

Adding $G$ to every processing time raises the completion time of the $r$ -th job on machine $M$ by $G(r+M-1)$ .
On two machines, $\sum_i d_i$ rises by $\tfrac12 Gn(n+3)$ for every sequence.
On two machines, $\hat T_r$ and $\hat S_r$ rise by $G[r(n-r)+\tfrac12(n-r)(n-r+1)+(n-r)]$ , $\sum_{J_r}d_i$ by $\tfrac12Gr(r+3)$ , and $LB(J_r)$ by $\tfrac12Gn(n+3)$ , for $1\le r\le n-1$ .
On three machines, every makespan and every $LB(J_r)$ with $1\le r\le n-1$ rises by $G(n+2)$ .
Multiplying all processing times by $H>0$ multiplies all these quantities by $H$ .
If $LB'=\varphi\circ LB$ on the nodes with $1\le r\le n-1$ , for a strictly increasing $\varphi$ , the two runs coincide at every step.

Significance

The THEOREM makes the method's behaviour a function of the shape of the data alone, not of its location or scale. This justifies normalizing test data, comparing running times across jobsets that differ by a change of units, and reporting results for one representative of each class. The proof also isolates a general principle: a deterministic best-first search depends on its bound only through the order the bound induces on the nodes it compares. Milestone 6 states that principle for the procedure of p. 402 with an arbitrary bound, so it applies to any other bound plugged into the same procedure.

As far as is known, no machine-checked version of this result or of the two lower bounds exists. The formalization needs the paper's procedure, with its tie rule, as an explicit deterministic function, and both lower bounds as functions of a node. The mission produces both, along with exact shift identities for every quantity the procedure uses.

Difficulty

The obvious argument is "adding $G$ adds a constant to everything", and it is not literally true. The constant depends on the position of a job and on the machine, so the identities must be computed term by term: maxima over machine-availability times commute with the shift only because both arguments move by the same amount, and that fails at the first job if processing times may be negative. The paper's own accounting contains a slip, the missing factor $G$ in $\tfrac12 r(r+3)$ . Its claim that "all lower bounds" of the three-machine problem rise by $G(n+2)$ is false at the root, where $\mathrm{TIMEB}=0$ does not move. The run equality therefore has to use the fact that the root is never compared with another node. The minima $\hat T_r$ , $\hat S_r$ range over all orderings of $\bar J_r$ , so their shift requires every ordering to move by the same amount. Finally, "the same path" has to be shown for the procedure's insertion with ties, step by step.

Formalization scope

Jobs are Fin n, numbered from $0$ . Processing times are real, and the shift statements and the goal assume them nonnegative, the paper's standing convention for durations. With negative times the goal is false (a three-job counterexample is recorded in the goal's statement). Scaling needs no sign condition.
The schedules of full sequences are Johnson's published as-soon-as-possible schedules (JohnsonFlowShop.ThreeStage.asapDone, JohnsonFlowShop.TwoStage.asapC2). Node attributes are computed by the same recursion on lists.
The two-machine objective is $\sum_i d_i$ instead of the mean; the two have the same minimizers.
$\hat T_r$ and $\hat S_r$ are minima over all orderings of $\bar J_r$ , not values at a sorted order.
Terminal nodes have depth $n-1$ . The procedure inserts children one at a time in increasing job index, each before every node of equal bound. Dominance discarding is not part of it.
Explicit readings. "The same sequence is optimal for both problems" means the sets of optimal sequences are equal, stated as an iff for every $\sigma$ . "Will follow the same path" means $\mathrm{run}(k)$ is equal for both problems at every $k$ . The paper's "all lower bounds" in the three-machine shift is restricted to nodes with $1\le r\le n-1$ . The hypotheses $H>0$ and $G>0$ are kept as stated.
Trivializations ruled out. A goal asserting only that some common optimal sequence exists, or only that the optimal values are related, would be weaker than the THEOREM. The goal states the iff and the equality of runs, with the procedure fixed independently of the data except through the bound.
The procedure, the node attributes and the lower bounds are also drafted in missions 1 and 2 of this series. Milestone 6 is reusable for any bound used with the same procedure. Proofs of any milestone are welcome. Generalizations, such as arbitrary real $G$ in the shift identities, are welcome as separate items.

Credit: Johnson (1954) for the reduction to permutation schedules and the published schedule definitions. No platform item treats flow-shop lower bounds or branch and bound over sequences. The nearest is the branch-and-bound mission BiconvexProg.BranchBound (Al-Khayyal and Falk), an unrelated algorithm for biconvex programs.

Selected references

E. Ignall, 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, A. G. Doig, An automatic method of solving discrete programming problems, Econometrica 28(3), 497–520, 1960. https://doi.org/10.2307/1910129
J. D. C. Little, K. G. Murty, D. W. Sweeney, C. Karel, An algorithm for the traveling salesman problem, Operations Research 11(6), 972–989, 1963. https://doi.org/10.1287/opre.11.6.972

15 thms3 active usersReviewed

Completed

Graph Theory Operations Research Optimization·Captain: mikedeng1

Sequencing a One State-Variable Machine: A Solvable Case of the Traveling Salesman Problem 2: For g = 0 ≤ f, the Tour ψ′ Minimizes the Largest Changeover CostResearch Paper

Motivation

A machine whose condition is described by one real number — the temperature of a furnace, the setting of a cutting knife — must process $N$ jobs in some order. Job $i$ must be started in state $A_i$ and leaves the machine in state $B_i$ ; moving the state between jobs costs money. Ordering the jobs so that the machine returns to its starting job after the last one is a traveling salesman problem whose distance matrix has a special structure. P. C. Gilmore and R. E. Gomory showed in 1964 (Oper. Res. 12(5), 655–679) that this special traveling salesman problem can be solved exactly with $O(N^2)$ operations, one of the first nontrivial polynomially solvable cases of the problem.

The same paper also treats a second objective: instead of the total changeover cost, minimize the largest single changeover cost of the cycle. This is the bottleneck traveling salesman problem, relevant whenever the binding constraint is the worst transition (a maximal temperature swing, a longest retooling) rather than the total. Without the tour constraint it is the bottleneck assignment problem solved by O. Gross (RAND, 1959). Gilmore and Gomory solve the bottleneck tour problem for the cost matrix of their model when only increases of the state cost anything. This mission formalizes that solution.

Timeline: Gross (1959) solves the bottleneck assignment problem; Gilmore and Gomory (1964) solve the sum and bottleneck traveling salesman problems for one state-variable costs; Gilmore, Lawler and Shmoys survey the well-solved special cases of the traveling salesman problem in The Traveling Salesman Problem (Wiley, 1985), where this case is a standard entry.

Setting

There are $N = n+1$ jobs. Job $i$ has a starting state $A_i\in\mathbb R$ and a final state $B_i\in\mathbb R$ , and the jobs are numbered so that $B_1\le B_2\le\dots\le B_N$ . Given two cost densities $f, g:\mathbb R\to\mathbb R$ , the cost of having job $j$ follow job $i$ is

c_{ij} = \int_{B_i}^{A_j} f(x)\,dx \ \text{ if } A_j\ge B_i,\qquad c_{ij} = \int_{A_j}^{B_i} g(x)\,dx \ \text{ if } B_i > A_j .

A permutation $\psi$ of the jobs means "job $\psi(i)$ follows job $i$ ". It is a tour if $\psi(s)\ne s$ for every nonempty proper subset $s$ of the jobs, i.e. if $\psi$ is a single cycle. The bottleneck cost of $\psi$ is

m(\psi) = \max_{1\le i\le N} c_{i\psi(i)} .

The bottleneck case of the paper is $g = 0$ and $f\ge 0$ : lowering the state is free, raising it costs $\int f$ .

A permutation $\varphi$ ranks the $A$ 's if $j>i$ implies $A_{\varphi(j)}\ge A_{\varphi(i)}$ . An interchange $\alpha_{ij}$ is the transposition of $i$ and $j$ ; $\psi\alpha_{ij}$ means "first apply $\alpha_{ij}$ , then $\psi$ ". The graph $G_\varphi$ has the jobs as nodes and an undirected arc $R_{i\varphi(i)}$ for each $i$ ; $R_{q,q+1}$ is the arc joining consecutive nodes $q$ and $q+1$ . A spanning tree of $G_\varphi$ is a set $T$ of arcs $R_{q,q+1}$ such that $G_\varphi\cup T$ is connected and no proper subset of $T$ connects $G_\varphi$ . In the bottleneck case the arc $R_{q,q+1}$ is given the cost $c_{q\varphi(q+1)}$ , and a minimum spanning tree minimizes the sum of these costs. If its arcs are $R_{j_1,j_1+1},\dots,R_{j_m,j_m+1}$ with $j_1<\dots<j_m$ , the paper's candidate tour is

\psi' = \varphi\,\alpha_{j_1 j_1+1}\,\alpha_{j_2 j_2+1}\cdots\alpha_{j_m j_m+1}.

Formalization targets

Goal: $\psi'$ solves the bottleneck traveling salesman problem

For $B$ sorted, $f\ge0$ locally integrable, $g=0$ , $\varphi$ ranking the $A$ 's and $T$ a minimum spanning tree as above,

\psi' \text{ is a tour}\quad\text{and}\quad m(\psi')\le m(\psi)\ \text{ for every tour } \psi .

The goal fixes no numerical constant. It asserts both that the construction produces a tour and that the tour is optimal, so it is a statement about the paper's algorithm, not only about the optimal value.

Milestones

Lemma 8 (p. 668): for a fixed $q$ , the number of $i$ with $i\le q<\varphi^{-1}\psi(i)$ equals the number of $j$ with $\varphi^{-1}\psi(j)\le q<j$ .
Lemma 7 (p. 668): for a tour $\psi$ , the graph $G_\psi^*$ — $G_\varphi$ plus the arcs $R_{q,q+1}$ selected by these two conditions — is connected.
Eq. (30) (p. 670): if $R_{q,q+1}$ is an arc of $G_\psi^*$ not in $G_\varphi$ , then $m(\psi)\ge c_{q\varphi(q+1)}$ .
$\varphi$ minimizes $m$ (p. 671): $m(\varphi)\le m(\psi)$ for every permutation $\psi$ .
The value of $m(\psi')$ (p. 671): $m(\psi')$ equals some $c_{j\varphi(j)}$ or the cost $c_{q\varphi(q+1)}$ of an arc of $T$ .
Theorem 6, corrected (p. 671): for a directed graph with nested out-neighbourhoods $\Gamma_1\subseteq\dots\subseteq\Gamma_N=\{1,\dots,N\}$ and $\varphi$ listing them as initial segments, a Hamiltonian circuit exists iff $\varphi(q)\in\Gamma_q$ for all $q$ and the graph $G'_\varphi$ is connected.

Significance

The result gives an exact solution of a bottleneck traveling salesman problem by one minimum spanning tree computation and a fixed sequence of transpositions. Since general bottleneck traveling salesman problems are NP-hard, cases with an exact algorithm are the reference points against which heuristics and approximation results are compared. Theorem 6, an application, characterizes Hamiltonicity for directed graphs whose out-neighbourhoods form a chain, a class on which the general Hamiltonian circuit problem becomes a connectivity test.

The result is proved in the paper; the mission formalizes the proof. To our knowledge none of it has a machine-checked proof. The formalization adds two things to the paper. First, the statements are made explicit: the order in which interchanges are applied, the reading of "spanning tree", the integrability of $f$ . Second, Theorem 6 as printed is false (see below), and the mission states and asks for a proof of the corrected version. Machine-checked statements of $G_\psi^*$ and Lemmas 7–8 are also the shared core of the companion mission on the minimal sum tour.

Difficulty

The obvious argument — every tour must "cross" each gap between consecutive components of $G_\varphi$ , so it pays at least the cheapest crossing — fails because the cost of a crossing is not intrinsic to the gap: a tour may cross between components using arcs that are not of the form $R_{q,q+1}$ , and $m$ looks at one arc at a time, not at a sum. The connection between an arbitrary tour and the spanning trees of $G_\varphi$ goes through the auxiliary graph $G_\psi^*$ and a counting argument (Lemma 8), and the sum-minimizing tree must be shown to be bottleneck-optimal as well. For the upper bound, the transpositions in $\psi'$ cascade along runs of consecutive tree arcs, so $\psi'(i)$ need not be $\varphi(i)$ or $\varphi(i+1)$ ; only the maximum $m(\psi')$ has that form, and showing it needs the monotonicity of $c_{ij}$ in $A_j$ and $B_i$ , which holds because $f\ge0$ and $g=0$ .

Formalization scope

Jobs are Fin (n + 1) (0-based; the paper's job $i$ is index $i-1$ ). $A, B : \text{Fin}(n+1)\to\mathbb R$ with Monotone B. The cost keeps the general two-density form (1); the bottleneck hypotheses are $f\ge0$ everywhere, $g$ identically $0$ , and $f$ locally integrable, so that every interval integral is genuine. Permutations are Equiv.Perm, and $\psi\alpha_{ij}$ is ψ * Equiv.swap i j. $m$ is a Finset.sup' over all jobs, including those that $\psi'$ leaves unchanged. The arc $R_{q,q+1}$ is indexed by q : Fin n.

Explicit readings of the paper's phrases:

"tour": $\psi(s)\ne s$ for every nonempty proper subset $s$ (the empty set is always fixed);
"a minimal set of additional arcs that connect": a connecting set of arcs $R_{q,q+1}$ none of whose proper subsets connects;
"minimum spanning tree … with these new costs": minimum sum of $c_{q\varphi(q+1)}$ over all such trees, not a bottleneck tree;
" $j_1,\dots,j_m$ in increasing order": the interchanges are applied to $\varphi$ in increasing index, lowest first;
" $\psi'$ minimizes $m(\psi')$ ": $\psi'$ is a tour and $m(\psi')\le m(\psi)$ for every tour $\psi$ ;
Theorem 6: the condition $\varphi(q)\in\Gamma_q$ for all $q$ is added, without which sufficiency fails (for $N=3$ , $\Gamma_1=\Gamma_2=\{3\}$ , $\Gamma_3=\{1,2,3\}$ , $\varphi=(3,1,2)$ , $G'_\varphi$ is connected but no Hamiltonian circuit exists); the existence of $\varphi$ is a hypothesis, not a claim.

Not formalized: the remark that the results hold for $f=0$ , $g\ge0$ ; the remark that $\psi'=\psi^*$ when $B_i\ge A_{\varphi(i)}$ ; the $O(N^2)$ operation count.

Trivializing formalizations are ruled out: with a Bochner integral and no integrability hypothesis every cost could collapse to $0$ and every claim would hold; dropping the tour conjunct of the goal would let $\varphi$ itself be "optimal"; and a maximum that ignored the unchanged arcs $c_{j\varphi(j)}$ would make the goal false.

The traveling salesman items already on the platform (metric and symmetric models with tours as visiting orders, e.g. MetricTSP, TSPHeuristics.Shared.TSPModel) describe a different model and are not used. A complete development needs permutation cycle structure (Mathlib's Equiv.Perm.SameCycle), connectivity of finite simple graphs, and interval integrals of nonnegative functions; the lemmas on $G_\psi^*$ and Lemma 8 are reusable for the sum objective. Proofs of any milestone are welcome independently.

Selected references

P. C. Gilmore and R. E. Gomory, Sequencing a one state-variable machine: a solvable case of the traveling salesman problem, Operations Research 12(5) (1964), 655–679. https://doi.org/10.1287/opre.12.5.655
O. Gross, The bottleneck assignment problem, RAND Corporation P-1630, 1959. https://www.rand.org/pubs/papers/P1630.html
P. C. Gilmore, E. L. Lawler and D. B. Shmoys, Well-solved special cases, in E. L. Lawler et al. (eds.), The Traveling Salesman Problem, Wiley, 1985, 87–143. ISBN 978-0-471-90413-7

9 thms3 active usersReviewed

Completed

Graph Theory Operations Research·Captain: mikedeng1

Sequencing Jobs to Minimize Total Weighted Completion Time Subject to Precedence Constraints 2: Near the Optimal Ratio, a Maximum-Weight Initial Set Is ρ-MaximalResearch Paper

Motivation

The single-machine sequencing problem with precedence constraints, written $1\mid\mathrm{prec}\mid\sum w_jC_j$ , asks for an order of $n$ jobs on one machine that respects a given acyclic digraph of precedences and minimizes the weighted sum of completion times. It is NP-hard in general (Lawler 1978; Lenstra and Rinnooy Kan 1978), and much of its structural theory goes through a decomposition due to Sidney (Sidney 1975): find an initial set of jobs of maximum weight-to-processing-time ratio, schedule it first, and recurse on the rest. Sidney's decomposition underlies the series-parallel algorithm of the same report, the 2-approximation algorithms for the general problem, and the vertex-cover view of Chudak–Hochbaum, Correa–Schulz and Ambühl–Mastrolilli.

The decomposition is only usable if a ratio-maximal initial set can be found efficiently. Section 7 of E. L. Lawler's report Sequencing jobs to minimize total weighted completion time subject to precedence constraints (IRIA-LABORIA Rapport de Recherche No. 205, December 1976; journal version in Annals of Discrete Mathematics 2, 1978) gives the polynomial algorithm: a binary search on the ratio, where each trial value is tested by one minimum-cut computation in an auxiliary network. This mission formalizes the correctness of that procedure.

Timeline.

1970: Rhys (Management Science 17) solves the selection problem, the bipartite case of a maximum-weight closed set, by minimum cut.
1975: Sidney introduces the decomposition into ratio-maximal initial sets.
1976: Lawler (this report) reduces the search for a ratio-maximal initial set to $O(\log n + \log w^* + \log p^*)$ minimum-cut computations.
1976: Picard (Management Science 22) treats the maximal closure of a general graph by the same network.

Setting

A finite set $N$ of $n=|N|$ jobs carries an acyclic digraph $G=(N,A)$ ; job $i$ must precede job $j$ when $G$ has a directed path from $i$ to $j$ . Job $j$ has an integer processing time $p_j\ge1$ and an integer weight $w_j$ of either sign.

An initial set of $N$ is a set $I\subseteq N$ that contains, with each of its jobs, every predecessor of that job. The ratio of a nonempty set is

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

and a nonempty initial set $I^*$ is ρ-maximal if $\rho(I^*)\ge\rho(I)$ for every nonempty initial set $I$ . Its ratio $\rho^*$ is the optimal ratio.

For a trial value $\rho$ , the trial weights are $\bar w_j=w_j-\rho p_j$ . A maximum-weight initial set for $\bar w$ is computed in the network $G^*$ : add a source $s$ and a sink $t$ , give the arc $(s,j)$ capacity $\max(0,-w_j)$ , the arc $(j,t)$ capacity $\max(0,w_j)$ , and every arc of $G$ capacity $+\infty$ . An $(s,t)$ cutset is a partition $(S,T)$ of the nodes with $s\in S$ , $t\in T$ , of capacity $c(S,T)=\sum_{i\in S}\sum_{j\in T}c_{ij}$ .

The integer data satisfy $-w^*\le w_j\le w^*$ and $1\le p_j\le p^*$ , and $\varepsilon=1/(np^*)^2$ .

Formalization targets

Goal: the last step of the binary search

If $\rho\le\rho^*\le\rho+\varepsilon$ , then every nonempty initial set $I$ of maximum trial weight,

\sum_{j\in I'}(w_j-\rho p_j)\le\sum_{j\in I}(w_j-\rho p_j)\quad\text{for all initial sets } I',

is ρ-maximal. This is the paper's sentence "At this point the smallest value in the interval is chosen for a trial value ρ. … In either case, the maximum weight initial set I which is determined is ρ-maximal" (pp. 16–17).

Milestones

Finite-capacity cutsets of $G^*$ correspond to initial sets $I=T-\{t\}$ (p. 14).
A finite cutset has capacity $\sum_{j\in N}\max(0,w_j)-\sum_{j\in I}w_j$ (p. 15).
A minimum cutset yields a maximum-weight initial set (p. 15).
Cases 1–3: a maximum-weight set of positive, negative or zero trial weight shows that $\rho$ is too small, too large, or optimal (pp. 15–16).
Every attainable ratio lies in $[-w^*,w^*]$ (p. 16).
Two distinct attainable ratios differ by at least $1/(np^*)^2$ (p. 16).

Significance

The goal is what makes Sidney's decomposition algorithmic: a ρ-maximal initial set can be found by a polynomial number of minimum-cut computations, with the bound $2\log_2 n+\log_2 w^*+2\log_2 p^*+1$ on the number of trial values. Ratio-maximal initial sets are the first step of every Sidney-decomposition-based algorithm for $1\mid\mathrm{prec}\mid\sum w_jC_j$ , and the cut network is the standard reduction of maximum-weight closure to minimum cut, used across open-pit mining, project selection and parametric optimization.

The results are classical and proved in the report. No machine-checked version of the closure–cut correspondence, the ratio-separation bound, or the binary-search correctness is known to exist in Lean or on Prove2Me. The mission produces a reusable formal account of initial sets, the network $G^*$ with infinite capacities, and the parametric test of a ratio.

Difficulty

Each step is short on paper; the difficulty is in the corners the paper does not discuss. The paper's "maximum weight initial set" ranges over all initial sets, and the empty set has weight $0$ . At $\rho=\rho^*$ the empty set is a maximizer and is not ρ-maximal, so the final step needs a nonempty maximizer; and Case 2, read literally over all initial sets, can never occur. The argument at the left end of the interval also needs the separation bound in the right direction: the printed display ends with " $<$ ", while the argument needs " $\ge$ ". Finally, initial sets are closed under predecessors along paths, while a cut only sees single arcs, so the correspondence between finite cuts and initial sets needs the arcs of $G$ to stay inside $N$ .

Formalization scope

Jobs are a Finset N in a type ι; the precedence digraph is a relation G with every arc inside N and no directed cycle, and "must precede" is Relation.TransGen G. Weights and processing times are real in the general statements and integers cast to reals in the integer-data statements. Lean evaluates $\rho(\emptyset)=0/0$ as $0$ ; ρ-maximality and every statement about attainable ratios therefore range over nonempty sets. Capacities take values in WithTop ℝ, with $+\infty=\top$ ; a pair of nodes that is not an arc of $G^*$ has capacity $0$ , and an infinite cut has capacity $\top$ . A cutset is given by its sink side $T\subseteq\{s,t\}\cup N$ .

Added hypotheses and corrected slips, all disclosed in the items:

the goal assumes the maximum-weight initial set $I$ is nonempty (the empty-set corner above);
Cases 2 and 3 maximize over nonempty initial sets;
the separation bound is stated with $\ge$ , against the printed " $<$ ";
the capacity display's first line, printed $\sum_{j\in S}c_{sj}$ , is read as $\sum_{j\in T}c_{sj}$ , as its second line shows;
the interval $[-w^*,w^*]$ and the separation bound are stated for every nonempty subset of $N$ , a slight generalisation.

A trivializing formalization is ruled out: the goal assumes neither Case 1 nor Case 3, nor the separation bound, nor anything about cuts; those appear only as milestones. The running-time statements of §7 and the binary search loop itself are out of scope.

A complete development needs finite sums over finsets, path closure of initial sets, and extended-real arithmetic in WithTop ℝ. The cut network with infinite capacities and the closure correspondence are reusable for any maximum-weight closure problem. Proofs of the milestones, and of the goal from Cases 1 and 3 with the separation bound, 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, 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
J. M. W. Rhys, A selection problem of shared fixed costs and network flows, Management Science 17 (1970) 200–207. https://doi.org/10.1287/mnsc.17.3.200
J.-C. Picard, Maximal closure of a graph and applications to combinatorial problems, Management Science 22 (1976) 1268–1272. https://doi.org/10.1287/mnsc.22.11.1268

11 thms3 active usersReviewed

Completed

Analysis Functional Analysis·Captain: mikedeng1

Quick Approximation to Matrices and Applications II: Every Square-Integrable f on [0,1]² Is a Sum of at Most 1/ε² Cut Functions plus an Error of Cut Norm at Most ε‖f‖₂Research Paper

Motivation

A large matrix, or a large graph, can be approximated in a weak but useful sense by a short sum of very simple pieces. Frieze and Kannan (Combinatorica 19 (1999) 175–220) proved that every real matrix is, up to an error small in the cut norm, a sum of at most $1/\epsilon^2$ cut matrices (constant on a combinatorial rectangle, zero elsewhere). This "weak regularity lemma" gives polynomial-time approximation schemes for dense instances of Max-Cut and other problems, with a number of pieces that is polynomial in $1/\epsilon$ , in contrast to the tower-type bounds of Szemerédi's regularity lemma.

Section 8 of the paper states the same decomposition for functions on the unit square, where the rows and columns of the matrix are replaced by the continuum $[0,1]$ . This continuous form became the weak regularity lemma for graphons (symmetric measurable functions $[0,1]^2\to[0,1]$ ) in the theory of dense graph limits developed by Lovász, Szegedy, Borgs, Chayes, Sós and Vesztergombi in the 2000s (Lovász–Szegedy 2006; Lovász, Large Networks and Graph Limits, 2012), where it is a standard step in proving compactness of the graphon space under the cut distance.

Setting

Let $[0,1]^2$ carry Lebesgue measure $dx\,dy$ . Let $f:[0,1]^2\to\mathbb R$ be Lebesgue measurable with

\|f\|_2^2=\int_{[0,1]^2}f(x,y)^2\,dx\,dy<\infty .

For measurable $S,T\subseteq[0,1]$ the rectangle integral is

f(S,T)=\int_{S\times T}f(x,y)\,dx\,dy,

and the cut norm is $\|f\|_C=\sup_{S,T}|f(S,T)|$ , the supremum over measurable $S,T$ . The measure of $S$ is written $|S|$ .

A cut function $\mathrm{CUT}(S,T,d)$ , for measurable $S,T\subseteq[0,1]$ and a real $d$ , is the function equal to $d$ on $S\times T$ and to $0$ elsewhere. Given cut functions $f_1,\dots,f_s$ , the error after $t$ of them is

w_t=f-(f_1+\dots+f_t),\qquad w_0=f .

In the Lean development these are rectInt f S T, l2Norm f, cutFun S T d and cutFunSum Ss Ts d in the namespace FriezeKannan.Continuum, on the type Sq = unitInterval × unitInterval.

Formalization targets

Goal: Theorem 12 (p. 217)

For every measurable $f$ with $\|f\|_2<\infty$ and every $\epsilon>0$ there exist cut functions $f_1,\dots,f_s$ with

s\le\frac1{\epsilon^2}\qquad\text{and}\qquad\|w_s\|_C\le\epsilon\|f\|_2. \tag{63}

The number of cut functions depends on $\epsilon$ alone, not on $f$ .

Milestones (the proof on p. 217)

Drop identity. For square-integrable $w$ , measurable $S,T$ with $|S||T|>0$ and $d=w(S,T)/(|S||T|)$ ,

\|w-\mathrm{CUT}(S,T,d)\|_2^2-\|w\|_2^2=\int_{S\times T}\big((w-d)^2-w^2\big)=-|S||T|d^2=-\frac{w(S,T)^2}{|S||T|}.

Drop bound. If $|w(S,T)|>\epsilon\|f\|_2$ , the same step lowers $\|w\|_2^2$ by at least $\epsilon^2\|f\|_2^2$ .
Inductive step. If $\|w_t\|_2^2\le(1-\epsilon^2t)\|f\|_2^2$ , then either (63) holds with $s=t$ , or one more cut function gives $\|w_{t+1}\|_2^2\le(1-\epsilon^2(t+1))\|f\|_2^2$ .

Significance

The result. Theorem 12 says that the space of square-integrable kernels is, in the cut norm, uniformly approximable by step functions of bounded complexity: $1/\epsilon^2$ rectangles suffice, whatever $f$ is. Refining the rectangles into a common partition gives a partition of $[0,1]$ into at most $4^{1/\epsilon^2}$ parts on which $f$ is close to a step function in cut norm, which is the weak regularity lemma for graphons. It is the ingredient behind compactness of graphon space, the approximation of graph parameters by sampling, and the equivalence of cut distance and left convergence in dense graph limit theory.

Formalizing it. The theorem is proved in the paper and in textbooks; this mission produces a machine-checked version. As far as the platform's catalog shows, no cut-norm decomposition of functions on $[0,1]^2$ is formalized there, and Mathlib has no graphons or cut norm. The definitions here (rectangle integrals, cut functions, the cut norm as a bound over measurable rectangles) are a reusable starting point for graph-limit results.

Difficulty

The paper's computations are short; the difficulty of a complete formalization is in the measure theory: the error $w_t$ must be shown square integrable at every stage (cut functions with measurable sets are bounded and measurable); integrability of $w_t$ and $w_t^2$ over $S\times T$ follows from square integrability on a probability space; the product measure of $S\times T$ is $|S||T|$ ; and the case $|S||T|=0$ must be excluded from the hypothesis $|w_t(S,T)|>\epsilon\|f\|_2$ rather than assumed. A naive attempt that bounds the cut norm by an $L^2$ approximation through step functions gives no bound on $s$ in terms of $\epsilon$ alone.

Formalization scope

$[0,1]$ is Mathlib's unitInterval with its Lebesgue measure, and $[0,1]^2$ is the product type unitInterval × unitInterval with the product measure. Sets $S,T$ are subsets of unitInterval, so no side condition $S\subseteq[0,1]$ appears.
"Lebesgue measurable with $\|f\|_2<\infty$ " is MemLp f 2, whose almost-everywhere strong measurability is measurability for the completed Lebesgue measure; no Borel Measurable f hypothesis is added. l2Norm f is the square root of $\int f^2$ ; it is the true $L^2$ norm under MemLp f 2, which every theorem about it assumes for the function whose norm is being lowered.
The cut norm is not defined as a supremum. A bound $\|w\|_C\le c$ is written $|w(S,T)|\le c$ for all measurable $S,T$ , which is the definition unfolded and avoids a real supremum of a possibly unbounded family. Every cut function and every test rectangle has measurable sides.
$|S|$ is (volume S).toReal, finite on $[0,1]$ .
Families of cut functions are indexed by Fin s; $s=0$ is the empty sum.
Added hypotheses, all disclosed in the items: $\epsilon>0$ in every theorem (the paper's implicit range of the error parameter, §2.3); $|S||T|>0$ in the drop identity (implicit on the page, where $d$ divides by $|S||T|$ ).
The width bound $s\le1/\epsilon^2$ is part of the goal. Without it the statement would follow from density of rectangle step functions in $L^2$ and would not be Theorem 12.

Contributions welcome: proofs of the three milestones and of the goal, and general lemmas on set integrals over measurable rectangles of unitInterval × unitInterval and on MemLp of finite sums of indicator functions, which are reusable beyond this mission.

Selected references

A. Frieze and R. Kannan, Quick approximation to matrices and applications, Combinatorica 19(2):175–220, 1999. https://doi.org/10.1007/s004930050052
L. Lovász and B. Szegedy, Limits of dense graph sequences, J. Combin. Theory Ser. B 96(6):933–957, 2006. https://doi.org/10.1016/j.jctb.2006.05.002
L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60, 2012. https://doi.org/10.1090/coll/060

5 thms3 active usersReviewed

Completed

Linear algebra Theoretical Computer Science·Captain: mikedeng1

Quick Approximation to Matrices and Applications I: Every Real Matrix Is a Sum of at Most 1/ε² Cut Matrices plus an Error W with |W(S,T)| ≤ ε√(|S||T|)‖A‖_FResearch Paper

Motivation

Many dense combinatorial optimization problems (Max-Cut, graph bisection, quadratic assignment on dense instances) have objective functions that are sums of matrix entries over rectangles $S\times T$ . If a matrix can be replaced by a simple surrogate that agrees with it on every rectangle up to a small error, such problems can be solved approximately on the surrogate. Frieze and Kannan's paper Quick approximation to matrices and applications (Combinatorica 19 (1999) 175–220) supplies this surrogate: a sum of a bounded number of cut matrices. Their decomposition is a "weak" form of Szemerédi's regularity lemma whose number of pieces grows only like $1/\varepsilon^2$ , against a tower-type bound for Szemerédi's lemma. It underlies constant-time sampling algorithms for dense instances, the theory of graph limits (the cut distance of Lovász and Szegedy), and the cut-norm approximation algorithm of Alon and Naor.

Timeline:

1978: Szemerédi's regularity lemma, with a number of parts of tower type in $1/\varepsilon$ .
1996: Frieze and Kannan announce the weak regularity lemma (FOCS 1996).
1999: the journal paper proves the matrix version, its algorithmic forms, and applications to Max-Cut, Max-SNP problems and pseudo-regular partitions.
2004–2006: Alon and Naor approximate the cut norm via Grothendieck's inequality; Lovász and Szegedy build graph limits on the cut distance.

Setting

Let $R$ and $C$ be finite sets, $|R|=m$ , $|C|=n$ , and let $A$ be a real $R\times C$ matrix. For $S\subseteq R$ , $T\subseteq C$ write

A(S,T)=\sum_{(i,j)\in S\times T}A(i,j).

The Frobenius norm is $\|A\|_F=\big(\sum_{i,j}A(i,j)^2\big)^{1/2}$ , and the cut norm is $\|A\|_C=\max_{S\subseteq R,\,T\subseteq C}|A(S,T)|$ .

For $S\subseteq R$ , $T\subseteq C$ and $d\in\mathbb R$ , the cut matrix $\mathrm{CUT}(S,T,d)$ has entry $d$ on $S\times T$ and $0$ elsewhere; it has rank at most one. A cut decomposition of width $s$ writes

A=D^{(1)}+\dots+D^{(s)}+W,\qquad D^{(t)}=\mathrm{CUT}(R_t,C_t,d_t),

with error matrix $W$ . In the Lean development these are blockSum, frobNorm, cutNorm, cutMatrix and cutSum in the namespace FriezeKannan.CutDecomp.

Formalization targets

Goal: Theorem 7 (p. 188)

For every real $R\times C$ matrix $A$ and every $\varepsilon>0$ there are $s\le1/\varepsilon^2$ cut matrices $D^{(t)}=\mathrm{CUT}(R_t,C_t,d_t)$ such that $W^{(s)}=A-(D^{(1)}+\dots+D^{(s)})$ satisfies

|W^{(s)}(S,T)|\le\varepsilon\sqrt{|S|\,|T|}\;\|A\|_F\qquad\forall S\subseteq R,\ T\subseteq C. \tag{17}

Milestones (the steps of the proof, p. 188)

With $d=W(S,T)/(|S||T|)$ for nonempty $S,T$ :

\|W-\mathrm{CUT}(S,T,d)\|_F^2-\|W\|_F^2=-|S|\,|T|\,d^2=-\frac{W(S,T)^2}{|S|\,|T|}.

If $|W(S,T)|>\varepsilon\sqrt{|S||T|}\,\|A\|_F$ , this drop is at most $-\varepsilon^2\|A\|_F^2$ .
If $\|W^{(t)}\|_F^2\le(1-\varepsilon^2t)\|A\|_F^2$ , then either $W^{(t)}$ satisfies (17), or one more cut matrix gives $\|W^{(t+1)}\|_F^2\le(1-\varepsilon^2(t+1))\|A\|_F^2$ .

Companion statements

The Remark after Theorem 7 (the case $m=1$ ): a real $n$ -vector $a$ is a weighted sum of at most $\varepsilon^{-2}$ 0-1 vectors plus an error $w$ with $|w(S)|\le\varepsilon\sqrt n\,|a|$ for all $S$ .
Inequality (1), p. 178: $\|M\|_C\le\sup_{x\ne0}\|Mx\|_1/\|x\|_\infty\le4\|M\|_C$ .
§2.3, p. 179: the symmetrised error $\bar W=(W+W^T)/2$ satisfies $\|\bar W\|_C\le\|W\|_C$ .

Significance

Theorem 7 says that the width needed to approximate a matrix on all rectangles, with error measured against $\sqrt{|S||T|}\|A\|_F$ , depends on $\varepsilon$ only, not on $m$ or $n$ . Since $|S||T|\le mn$ , it gives a cut decomposition with $\|W\|_C\le\varepsilon\sqrt{mn}\|A\|_F$ , the error of the paper's algorithmic Theorem 2. It is the existence statement behind the paper's constant-time approximation schemes for dense Max-Cut and Max-SNP problems and behind its pseudo-regular partitions of graphs (§5.1), and it is the matrix form of the weak regularity lemma used throughout the theory of dense graph limits.

The result is proved in the paper, by an elementary argument. Its formalization adds a machine-checked weak regularity lemma for real matrices with explicit constants, stated in a form (finite index types, block sums, cut matrices) that downstream developments in graph limits, property testing and approximation algorithms can import. To the best of the curators' knowledge it has no machine-checked proof; Mathlib contains Szemerédi's regularity lemma for graphs but not this matrix decomposition or the cut norm of matrices.

Difficulty

The obvious decomposition, one cut matrix per nonzero entry, achieves $W=0$ but has width $mn$ ; the content is that width $1/\varepsilon^2$ suffices uniformly in the dimensions. Bounding the error on a single rectangle is easy; bounding it on all $2^{m+n}$ rectangles at once, with an error that scales as $\sqrt{|S||T|}$ rather than as $\sqrt{mn}$ , is the point. The bound is also against the Frobenius norm of the original matrix $A$ , not of the current error, so the argument must track a single global quantity across all steps. In Lean, the main friction is bookkeeping: real casts of cardinalities inside square roots, the division by $|S||T|$ , and the identification of the squared Frobenius norm with a double sum.

Formalization scope

Index sets are arbitrary finite types R, C with decidable equality; subsets are Finsets, and $|S|$ is the cardinality cast to $\mathbb R$ . Empty $R$ or $C$ is allowed.
$\|A\|_F$ is the real square root of the sum of squares (frobNorm); Mathlib's scoped matrix norms are not used. The cut norm is a genuine maximum over the finite nonempty set of pairs of subsets.
A family of $s$ cut matrices is three functions on Fin s; $s=0$ is allowed (for $\varepsilon\ge1$ or $A=0$ no cut matrix is needed). No nonemptiness, disjointness or sign condition is imposed on $R_t$ , $C_t$ , $d_t$ .
Added hypotheses, each disclosed in the statement's Formalization Note: $\varepsilon>0$ (the paper's implicit range of the error parameter; $\varepsilon<1$ is not assumed); nonempty $S,T$ in milestone 1 (they make $d$ well defined); the strict inequality $>$ in milestone 2 (the negation of (17); the page prints $\ge$ ); a nonempty column set for inequality (1) (the supremum over $\mathbb R^n\setminus\{0\}$ needs $n\ge1$ ). Inequality (1) is stated without division, as the existence of a nonzero $x$ with $\|M\|_C\|x\|_\infty\le\|Mx\|_1$ together with $\|Mx\|_1\le4\|M\|_C\|x\|_\infty$ for all $x$ .
The width bound $s\le1/\varepsilon^2$ is the theorem; without it the statement is trivial (one cut matrix per entry gives $W=0$ ). A formalization that drops it, bounds the error by $\|W\|_F$ instead of $\|A\|_F$ , or uses $\sqrt{mn}$ in place of $\sqrt{|S||T|}$ proves a different theorem.
Reusable infrastructure: the identity $\|M\|_F^2=\sum_{i,j}M(i,j)^2$ , block sums of cut matrices and their sums, and the cut norm with its basic properties (transpose invariance, comparison with the $\infty\to1$ norm). Contributions of these as standalone lemmas, and of the milestones in the listed order, are welcome.

Selected references

A. Frieze and R. Kannan, Quick approximation to matrices and applications, Combinatorica 19(2) (1999) 175–220. https://doi.org/10.1007/s004930050052
A. Frieze and R. Kannan, The regularity lemma and approximation schemes for dense problems, Proc. 37th FOCS (1996) 12–20. https://doi.org/10.1109/SFCS.1996.548459
E. Szemerédi, Regular partitions of graphs, Problèmes combinatoires et théorie des graphes, Colloq. Internat. CNRS 260 (1978) 399–401.
N. Alon and A. Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35(4) (2006) 787–803. https://doi.org/10.1137/S0097539704441629
L. Lovász and B. Szegedy, Limits of dense graph sequences, J. Combin. Theory Ser. B 96(6) (2006) 933–957. https://doi.org/10.1016/j.jctb.2006.05.002

5 thms3 active usersReviewed

Graph Theory Operations Research·Captain: mikedeng1

An Introduction to Timetabling 1: Every Class–Teacher Requirement Matrix Has a Timetable over Any p Days with Every Daily Load and Pair Count Between ⌊r/p⌋ and ⌈r/p⌉Research Paper

Motivation

School and university timetabling is one of the oldest applications of combinatorial optimization. In his invited review An introduction to timetabling (European Journal of Operational Research, 1985), D. de Werra opens with the class–teacher model: classes meet teachers for a prescribed number of one-period lectures, and the lectures must be placed into periods or days so that no class and no teacher is overloaded. Every richer timetabling model of the review (preassignments, unavailabilities, course scheduling) is built on top of this one, and the review keeps returning to its graph-theoretic reading as an edge-colouring problem in a bipartite multigraph.

The model comes in three levels of demand. The daily problem asks for a clash-free timetable. The weekly problem asks for an assignment of lectures to days within daily load limits. The balanced weekly problem asks, in addition, that the load of every class and every teacher be spread as evenly as possible over the week, and that the lectures of each class–teacher pair be spread evenly too. The last one is the practical requirement that a teacher should not have all four lectures with one class on Monday.

Timeline (as cited in the review).

1916. D. König proves that a bipartite multigraph of maximum degree $\Delta$ can be edge-coloured with $\Delta$ colours. The review states it as Proposition 2.1, citing Berge's Graphes [1].
1975. D. de Werra, "A few remarks on chromatic scheduling" (reference [37] of the review), gives the balanced version: for every $p$ the edges of a bipartite multigraph can be $p$ -coloured so that every node and every bundle of parallel edges is balanced. This is Proposition 2.3.
1978. D. de Werra, "Some comments on a note about timetabling" (INFOR, reference [38]), gives the weekly version with daily load limits, Proposition 2.2.
1985. The review collects the three results in matrix form as problems CT1, CT2 and CT3 and sketches a network-flow construction for CT3, citing Krarup [19].

Setting

There are $m$ classes $c_1,\dots,c_m$ and $n$ teachers $t_1,\dots,t_n$ . The requirement matrix $R=(r_{ij})$ is an $m\times n$ matrix of nonnegative integers: $r_{ij}$ is the number of lectures class $c_i$ must have with teacher $t_j$ . Write $r_{i\cdot}=\sum_j r_{ij}$ for the total load of class $c_i$ and $r_{\cdot j}=\sum_i r_{ij}$ for that of teacher $t_j$ . For nonnegative integers $s$ and $p\ge1$ , $\lfloor s/p\rfloor$ and $\lceil s/p\rceil$ are the floor and ceiling of the rational $s/p$ .

A schedule over $p$ periods or days is an array $x=(x_{ijk})$ of nonnegative integers ( $i\le m$ , $j\le n$ , $k\le p$ ) that places every lecture exactly once:

\sum_{k=1}^p x_{ijk}=r_{ij}\quad\text{for all } i,j. \tag{1}

CT1 asks in addition that $x_{ijk}\in\{0,1\}$ and that $\sum_j x_{ijk}\le1$ , $\sum_i x_{ijk}\le1$ : no class and no teacher has two lectures in one period.
CT2, given positive integers $a_i$ , $b_j$ , asks that $\sum_j x_{ijk}\le a_i$ and $\sum_i x_{ijk}\le b_j$ on every day $k$ .
CT3 asks that on every day $k$

\Big\lfloor \tfrac{r_{i\cdot}}{p}\Big\rfloor\le\sum_j x_{ijk}\le\Big\lceil \tfrac{r_{i\cdot}}{p}\Big\rceil,\quad \Big\lfloor \tfrac{r_{\cdot j}}{p}\Big\rfloor\le\sum_i x_{ijk}\le\Big\lceil \tfrac{r_{\cdot j}}{p}\Big\rceil,\quad \Big\lfloor \tfrac{r_{ij}}{p}\Big\rfloor\le x_{ijk}\le\Big\lceil \tfrac{r_{ij}}{p}\Big\rceil. \tag{8–10}

In the Lean development these are IsCT1 R p x, IsCT2 R p a b x and IsCT3 R p x, with the floor and ceiling written lo s p and hi s p and the totals rowSum R i, colSum R j.

Formalization targets

Goal: Proposition 2.3

\forall\,R\in\mathbb N^{m\times n},\ \forall\,p\ge1:\quad \exists\,x,\ \ x \text{ solves CT3 for } R \text{ over } p \text{ days}.

The statement fixes no constant: it asserts that perfectly balanced weekly timetables always exist.

Milestones

One balanced day (flow sketch, p. 153): for $p\ge1$ there is a matrix $y$ satisfying the bounds (8), (9), (10) at once.
The remaining days stay balanced (same sketch): if $p\ge2$ and $\lfloor s/p\rfloor\le y\le\lceil s/p\rceil$ , then $\lfloor s/p\rfloor\le\lfloor (s-y)/(p-1)\rfloor$ and $\lceil (s-y)/(p-1)\rceil\le\lceil s/p\rceil$ .
Proposition 2.1 (König): CT1 is solvable iff $r_{\cdot j}\le p$ and $r_{i\cdot}\le p$ for all $i,j$ .
Proposition 2.2: CT2 is solvable iff $r_{\cdot j}\le p\,b_j$ and $r_{i\cdot}\le p\,a_i$ .
Minimum number of days: CT2 is solvable over $p$ days iff $p\ge\max\big(\max_j\lceil r_{\cdot j}/b_j\rceil,\max_i\lceil r_{i\cdot}/a_i\rceil\big)$ .
Figure 1: the printed timetable for $R=\begin{pmatrix}1&2&4\\3&0&2\end{pmatrix}$ , $p=3$ , solves CT3.

Significance

The result. Proposition 2.3 says that the balancing requirement costs nothing: whatever the requirement matrix, the week can be organised so that each class and each teacher has an essentially constant daily load and each class–teacher pair is spread evenly. It contains König's edge-colouring theorem (take $p$ at least the maximum degree, so every daily load is at most one) and the weekly Proposition 2.2 as special cases. Combined with Proposition 2.1 applied to each day, it reduces weekly timetabling to independent daily problems, which is the decomposition the review recommends ("one may start by solving the weekly problem … and then solve separately the resulting daily problems", p. 154). In graph language it is the existence of equitable edge colourings of bipartite multigraphs, a standard tool in scheduling and in the theory of edge colourings.

Formalizing it. All results of this mission are classical and proved in the literature; none of them is formalized on the platform. Mathlib contains Hall's marriage theorem but not König's edge-colouring theorem for bipartite multigraphs, and not balanced or equitable colourings. A complete development gives a machine-checked König edge-colouring theorem in matrix form, the matrix-rounding step with simultaneous row, column and entry bounds, and the balanced-colouring theorem itself.

Difficulty

Each family of constraints alone is easy: spreading a single number $r_{ij}$ evenly over $p$ days, or a single row total, is a matter of division with remainder. The difficulty is that one array must satisfy (1), (8), (9) and (10) simultaneously, so that the per-entry roundings must add up to correct roundings of every row total and every column total on every day. Rounding each entry independently breaks the row and column constraints, and greedy day-by-day choices can leave a remainder that no longer fits the bounds. The crux is integrality: the rational average $r_{ij}/p$ satisfies every bound on every day, but the problem asks for integers, and an integral one-day slice must round all entries, all row totals and all column totals consistently.

Formalization scope

Classes, teachers and days are Fin m, Fin n, Fin p; $R$ and $x$ are natural-number valued, which is the paper's " $x_{ijk}\ge0$ integer". Constraint (4) of CT1 is written $x_{ijk}\le1$ . Floors and ceilings are Nat.floor and Nat.ceil of the rational quotient. In (8) and (9) they are applied to the row and column totals, never summed entrywise. The minimum number of days uses Finset.sup, whose empty value is $0$ , and is stated as an equivalence ("solvable over $p$ days iff $p\ge p_{\min}$ ") rather than as an infimum.

Disclosed choices:

The goal and the one-day milestone assume $p\ge1$ ; the paper's "for any $p$ " means any number of days, and for $p=0$ Lean's division returns $0$ .
The remaining-days milestone assumes $p\ge2$ so that $p-1$ days remain.
Propositions 2.1, 2.2 and the minimum-days statement hold for every $p$ , including $p=0$ , and assume nothing more than the page: $a_i,b_j$ positive.
The edge-colouring and network-flow readings of the paper are stated in prose only; the formal statements are in matrix form, which is how the propositions are stated.

The formalization does not admit a trivial reading: CT3 requires all four constraint families at once, (1) is an equality, and the sanity checks show both that the Figure 1 data satisfy CT3 and that CT1 is not satisfiable for $R=(2)$ and $p=1$ .

Useful infrastructure, reusable beyond this mission: integral flows with lower bounds, or total unimodularity of bipartite incidence matrices; König's edge-colouring theorem for bipartite multigraphs; floor and ceiling arithmetic for natural-number quotients. Proofs of any milestone, alternative proofs of the goal, and a sorry-free proof of the Figure 1 instance are all welcome.

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
D. König, Über Graphen und ihre Anwendung auf Determinantentheorie und Mengenlehre, Mathematische Annalen 77 (1916) 453–465. https://doi.org/10.1007/BF01456961
C. Berge, Graphes, Gauthier-Villars, Paris, 1983 (reference [1] of the review).
D. de Werra, A few remarks on chromatic scheduling, in B. Roy (ed.), Combinatorial Programming: Methods and Applications, Reidel, Dordrecht, 1975, 337–342.
D. de Werra, Some comments on a note about timetabling, INFOR 16 (1978) 90–92.
J. Krarup, Chromatic optimisation: Limitations, objectives, uses, references, European Journal of Operational Research 11 (1982) 1–19.

8 thms3 active usersReviewed

Completed

Graph Theory Operations Research·Captain: mikedeng1

An Introduction to Timetabling 2: When Every Teacher Is Available in at Most Two Periods, Limited Backtracking Finds a Timetable or Correctly Reports That None ExistsResearch Paper

Motivation

School and university timetabling is one of the oldest applications of combinatorial optimization. In the class–teacher model, classes and teachers must be brought together for a prescribed number of lectures, each lecture occupies one period, and nobody can be in two places at once. With no further side constraints the model reduces to edge colouring of a bipartite multigraph and is solved exactly by König's theorem. Real instances, however, come with preassignments (a class and a teacher must meet at a fixed period) and unavailabilities (a teacher or a class cannot be scheduled at some periods). With these, deciding whether a daily timetable exists is NP-complete, as the paper records citing Even, Itai and Shamir (1976).

D. de Werra's invited review An introduction to timetabling (European Journal of Operational Research 19, 1985) surveys this landscape. In its §2.2 it isolates one restricted case that is easy: when every teacher is available during at most two periods, a limited backtracking method finds a timetable or proves that none exists (Proposition 2.4, attributed to [9], Even–Itai–Shamir). The Remark that follows recasts the procedure as a decision method for stable sets of half the vertices in graphs with a perfect matching, which is the 2-satisfiability problem in graph form.

Setting

There are $m$ classes $c_1,\dots,c_m$ , $n$ teachers $t_1,\dots,t_n$ and $p$ periods of one day. After removing the preassigned lectures, $\bar r_{ij}\in\mathbb N$ lectures of class $c_i$ with teacher $t_j$ remain; $\bar b_{ik}\in\{0,1\}$ is $1$ exactly when class $c_i$ is available and not preassigned at period $k$ ; $\bar c_{jk}\in\{0,1\}$ is $1$ exactly when teacher $t_j$ is available and not preassigned at period $k$ . A timetable (a solution of CT4) is a $0/1$ array $\bar x_{ijk}$ with

\sum_{k}\bar x_{ijk}=\bar r_{ij},\qquad \sum_{j}\bar x_{ijk}\le\bar b_{ik},\qquad \sum_{i}\bar x_{ijk}\le\bar c_{jk}.

A possible schedule of $t_j$ is the slice $y_{ik}=\bar x_{ijk}$ of a candidate array that satisfies the constraints involving $t_j$ alone. The conflict graph $G$ has one node per pair (teacher, possible schedule); two nodes are linked when they are different schedules of the same teacher or put the same class in the same period. When each teacher has exactly two schedules, they are written $x_j$ and $\bar x_j$ , and in Lean the nodes are (j, true) and (j, false) of Fin n × Bool.

The limited backtracking works on such a graph. The implications $\mathrm{cl}(S)$ of a set $S$ of chosen nodes form the least set containing $S$ such that whenever $u$ is in it and $u$ is linked to a node $w$ of another teacher, the other node of $w$ 's teacher is in it. A state is either $\mathrm{run}(A)$ , with $A$ the nodes fixed so far, or $\mathrm{fail}$ . From $\mathrm{run}(A)$ , for any teacher not yet fixed and any first choice $b$ of its node:

if $\mathrm{cl}(A\cup\{(j,b)\})$ is independent, the procedure moves there;
otherwise, if $\mathrm{cl}(A\cup\{(j,\lnot b)\})$ is independent, it moves there;
otherwise it fails.

Formalization targets

Goal: correctness of the limited backtracking

For every $n$ and every graph $G$ on $\mathrm{Fin}\,n\times\mathrm{Bool}$ in which $x_j$ and $\bar x_j$ are linked for all $j$ :

\begin{aligned} &\text{(1) the move relation is well founded from } \mathrm{run}(\emptyset);\\ &\text{(2) every reachable } \mathrm{run}(A) \text{ with an unfixed teacher has a move};\\ &\text{(3) a reachable } \mathrm{run}(A) \text{ with all teachers fixed has } A \text{ a set of } n \text{ pairwise non-adjacent nodes};\\ &\text{(4) if } \mathrm{fail} \text{ is reachable, } G \text{ has no set of } n \text{ pairwise non-adjacent nodes.} \end{aligned}

All four clauses range over every run of the nondeterministic procedure.

Milestones

A teacher available in at most $2$ periods has at most $2$ possible schedules.
CT4 has a solution iff its conflict graph has $n$ pairwise non-adjacent nodes.
The implications of chosen nodes lie inside every timetable that contains those nodes.
If $A$ is independent and closed under implications, $G$ has a timetable iff it has one containing $A$ .
In a graph $G=(X,E)$ with a perfect matching $M$ , a stable set has at most $|X|/2$ nodes, and one of exactly $|X|/2$ nodes contains one endpoint of every edge of $M$ .

Significance

Proposition 2.4 identifies a polynomial special case inside a scheduling problem that the paper cites as NP-complete in general (Even–Itai–Shamir [9]). The correctness of the procedure is what makes that special case tractable. Milestones 1 and 2 reduce the timetabling instance to a graph question, and the goal settles the graph question. Milestone 4 is the reason the method needs to undo only the last decision. It is the graph form of the autarky principle of 2-SAT solving: a closed, consistent partial assignment can always be kept. Milestone 5 extends the method from timetables to any graph with a perfect matching.

On the formal side, no machine-checked treatment of this reduction or of the backtracking argument exists on the platform; 2-SAT, unit propagation and autarky have no items there either. The statements are proved in the paper only in prose, and the propagation and autarky arguments are compressed into a few sentences. A formal proof makes the invariants explicit: what is closed, what is independent, and why a contradiction after a reversed decision is global.

Difficulty

Soundness of a successful run is an invariant argument. Soundness of failure is the hard part. The naive argument "both choices for $t_j$ lead to a contradiction, hence no timetable" is wrong in general backtracking, because an earlier decision might be at fault, and full backtracking would revisit it. The proof has to show that an earlier permanent decision never needs revisiting. This requires that the set of fixed nodes is closed under implications and independent, so that no unscheduled teacher is linked to it. This invariant must be maintained through both the keep and the reverse moves. Termination and progress are routine but must be stated: without them the correctness clauses hold for a procedure that never moves. On the CT4 side, the reduction must check that the class constraint $(13)$ with $\bar b_{ik}\in\{0,1\}$ splits exactly into per-teacher availability and pairwise disjointness of schedules.

Formalization scope

Data. $\bar r,\bar b,\bar c$ are taken as data; the preassignments that produce them are not modelled. Indices are Fin m, Fin n, Fin p; $0/1$ variables are Bool.
Schedules. The page's "each teacher has exactly 2 possible schedules" holds only after its normalisation. The milestone states the faithful bound $\le 2$ . The CT4-to-graph equivalence is stated for every instance, so its graph has $\sum_j\#\{\text{schedules of }t_j\}$ nodes rather than $2n$ .
Procedure. The implications are an inductive predicate with no iteration bound. A contradiction is a non-independent set of implications, checked against previously fixed nodes as well. The move relation is an inductive Step with one constructor for each of keep, reverse and fail, so the choice of teacher and of first schedule stays arbitrary.
Not formalized. The $O(n^2)$ running time of Proposition 2.4 and of the Remark has no machine model or constant on the page; termination stands in for it.
Ruled out. A goal with only clauses (3)–(4) would be satisfied by a relation with no moves, and a fixed choice rule would prove a weaker statement. The goal therefore includes termination and progress and quantifies over every run.
Needed infrastructure. Mathlib's SimpleGraph, IsIndepSet, IsNIndepSet, Subgraph.IsPerfectMatching, Relation.ReflTransGen and Acc. The autarky lemma (Milestone 4) and the propagation lemma (Milestone 3) are reusable for any 2-SAT-type development. Proofs of the milestones, and a bridge from the CT4 instance to the abstract graph on Fin n × Bool in the exactly-two-schedules case, are welcome.

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
S. Even, A. Itai, A. Shamir, On the complexity of timetable and multicommodity flow problems, SIAM Journal on Computing 5 (1976) 691–703. https://doi.org/10.1137/0205048
B. Aspvall, M. F. Plass, R. E. Tarjan, A linear-time algorithm for testing the truth of certain quantified boolean formulas, Information Processing Letters 8 (1979) 121–123. https://doi.org/10.1016/0020-0190(79)90002-4

8 thms3 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

On Cores and Indivisibility 2: Gale's Top Trading Cycles Give a Core Allocation Supported by Competitive PricesResearch Paper

Motivation

Markets for indivisible goods, in which each participant owns one unit and wants one unit (houses, kidneys in paired donation, dormitory rooms, school seats), cannot be analysed with the convexity assumptions of classical general equilibrium theory. Shapley and Scarf (1974) introduced the housing market to ask whether the two central solution concepts of exchange economies survive indivisibility: the core (allocations no coalition can improve upon by trading among itself) and competitive equilibrium (allocations supported by prices at which every trader optimizes within his budget). Their paper (doi:10.1016/0304-4068(74)90033-0) gives two proofs that the core is nonempty. The first (Section 4) shows that the associated game without side payments is balanced and invokes Scarf's theorem; that is the companion mission of this series. The second (Section 6) is a constructive argument the authors attribute to David Gale, the top trading cycles method, which also produces competitive prices. This mission formalizes the second.

Timeline.

1967: Scarf proves that balanced games without side payments have nonempty cores (doi:10.2307/1909383).
1974: Shapley and Scarf define the housing market, prove that it has a nonempty core by both arguments, and give Gale's top-trading-cycle construction with competitive prices, allowing indifferences.
1977: Roth and Postlewaite show that with strict preferences the competitive allocation is unique and is the unique allocation in the strong core (doi:10.1016/0304-4068(77)90004-0).
1982: Roth shows the top-trading-cycles mechanism is strategy-proof under strict preferences (doi:10.1016/0165-1765(82)90003-9).
2003: Abdulkadiroğlu and Sönmez adapt top trading cycles to school choice (doi:10.1257/000282803322157061).

Setting

A finite set $N$ of traders each brings one indivisible good; "item $j$ " is the good of trader $j$ . Preferences are a real matrix $A = (a_{ij})_{i,j\in N}$ : trader $i$ prefers item $j$ to item $k$ when $a_{ij} > a_{ik}$ and is indifferent when $a_{ij} = a_{ik}$ . Ties are allowed, and only comparisons matter.

An allocation is a bijection $\sigma : N\to N$ ; trader $i$ receives item $\sigma(i)$ . For a coalition $S$ , an $S$ -permutation $\tau$ reshuffles the items of $S$ among the members of $S$ . The allocation $\sigma$ is a core allocation if there is no nonempty $S$ and $S$ -permutation $\tau$ with $a_{i\tau(i)} > a_{i\sigma(i)}$ for every $i \in S$ .

Prices $\mathrm{price}: N \to \mathbb R$ are competitive for $\sigma$ if each trader $i$ , selling his own item for $\mathrm{price}(i)$ , can afford $\sigma(i)$ , i.e. $\mathrm{price}(\sigma(i)) \le \mathrm{price}(i)$ , and no item $k$ with $\mathrm{price}(k) \le \mathrm{price}(i)$ is better for him than $\sigma(i)$ .

For $R \subseteq N$ , a top trading cycle for $R$ is a nonempty $S \subseteq R$ whose members can be arranged in a cycle $i_1 \to i_2 \to \cdots \to i_s \to i_1$ so that each $i_r$ likes the good of $i_{r+1}$ at least as well as any other good in $R$ . A top-trading-cycle partition is

N = S^1 \cup S^2 \cup \cdots \cup S^p,

with $S^1$ a top trading cycle for $N$ and each $S^j$ a top trading cycle for $N - (S^1\cup\cdots\cup S^{j-1})$ . In Lean the partition carries stage : N → Fin p and the successor map next : N → N.

Formalization targets

Goal: Section 6, assertions (1) and (2), p. 114

For every market $A$ and every top-trading-cycle partition with successor map $\mathrm{next}$ , the allocation $i \mapsto \mathrm{next}(i)$ is a core allocation, and for every choice of prices

\pi^1 > \pi^2 > \cdots > \pi^p > 0

on the goods of $S^1,\dots,S^p$ it is competitive. The paper asserts that "a set of competitive prices exists"; its argument works for every such choice, and the goal states that.

Milestones (Section 6, p. 114)

Every nonempty $R\subseteq N$ has a top trading cycle.
A top-trading-cycle partition of $N$ exists (so the goal is not vacuous and every market has a competitive core allocation).
If $j$ is the first index with $S \cap S^j \ne \emptyset$ and $i \in S\cap S^j$ , then $a_{ik} \le a_{i\,\mathrm{next}(i)}$ for all $k \in S$ .
Under the prices $\pi^{\mathrm{stage}(k)}$ , the successor's item costs the same as one's own, and every affordable item lies in one's own cycle or a later one.

Example (Section 7, pp. 115–116)

For the matrix $\begin{pmatrix}0&1&2\\1&0&-1\\-1&1&0\end{pmatrix}$ the unique competitive payoff is $(2,1,1)$ at equal prices, while the allocation with payoff $(1,1,0)$ is a core allocation that is competitive at no prices.

Significance

The result gives the existence of a core allocation of every housing market by an explicit construction, and shows that this allocation is competitive, so the competitive solution is nonempty even though goods are indivisible and preferences may have ties. The Section 7 example shows that the inclusion of competitive allocations in the core is strict in general. Under strict preferences, the outcome of the construction is the basis of the matching-market literature: uniqueness of the strong core (Roth–Postlewaite), strategy-proofness (Roth), and the school-choice and kidney-exchange mechanisms built on top trading cycles.

The mathematics is classical and proved. The formalization adds a machine-checked statement of the weak-preference version with the paper's strict blocking notion and its price argument, which existing formal developments do not cover. The closest platform items are AGT.house_core_unique, the strict-preference refinement (Roth–Postlewaite: with strict preferences and weak blocking the core is exactly one allocation), and the school-choice items SchoolChoice.TTC.*. Neither is this statement: the first assumes strict total orders and a different blocking notion, under which the core can be empty once ties are allowed, and says nothing about prices; the second concerns another model with priorities.

Difficulty

Each step is short on paper; the work is in the bookkeeping. The cycle allocation must be shown to be a bijection of $N$ from the stage-by-stage cycle structure; the "chain of best-liked goods that eventually must come back to some earlier element" must be turned into a cycle whose members each get a best good in $R$ , with ties handled by a choice rather than by a unique top choice; and the first-stage argument must be carried out with the coalition's reshuffling restricted to its own goods. A tempting shortcut, assuming strict preferences or using a union of cycles at a stage, proves a different statement and is ruled out by the definitions.

Formalization scope

Traders form an arbitrary finite type N with decidable equality; no nonemptiness is assumed (the empty market has the empty partition). The matrix A : N → N → ℝ has no hypothesis, so ties are allowed.
Allocations are bijections σ : N → N rather than zero-one matrices. This loses nothing: a coalition in which all members are strictly better off gives each member exactly one item of the coalition (owning nothing is ranked below everything), and an allocation leaving a trader without an item is blocked by that trader alone.
Blocking is strict for every member of the coalition, as on p. 107; the weak notion (all weakly, one strictly better off) makes assertion (1) false with ties.
The paper gives no displayed definition of competitive prices. The Lean notion is: $\sigma$ is a bijection, $\mathrm{price}(\sigma(i)) \le \mathrm{price}(i)$ , and $\mathrm{price}(k)\le\mathrm{price}(i) \Rightarrow a_{ik}\le a_{i\sigma(i)}$ . This transcribes "can sell his own item for $\pi^j$ dollars", "cannot afford", and "his utility is maximized" (p. 114).
A top trading cycle is a single cycle of the successor map: nonempty, inside $R$ , closed under next, every member reaching every other by iterating next. A one-trader cycle with next i = i is allowed (footnote, p. 114).
Explicit readings of loose phrases: "it is evident" (milestone 1) is an existence statement; "the highest possible payoff available to him in $S$ " (milestone 3) is $a_{ik} \le a_{i\,\mathrm{next}(i)}$ for all $k\in S$ ; "cannot afford any items from $S^1,\dots,S^{j-1}$ " (milestone 4) is: price at most $\pi^j$ implies stage at least $j$ ; "a set of competitive prices exists" (goal) is strengthened to every strictly decreasing positive $\pi$ , as the proof gives.
Trivializing formalizations are ruled out: the partition is quantified over all choices and its existence is a milestone, cycles are required to be nonempty and single, and the budget clause is part of the price notion, so competitiveness does not reduce to "everyone gets a best good".
Contributions welcome: proofs of the milestones, a computable top-trading-cycle algorithm with a proof that it produces a partition, and a proof of the paper's remark that no other competitive prices exist up to ties.

Selected references

L. Shapley and H. Scarf, On cores and indivisibility, Journal of Mathematical Economics 1 (1974) 23–37. https://doi.org/10.1016/0304-4068(74)90033-0
H. Scarf, The core of an N person game, Econometrica 35 (1967) 50–69. https://doi.org/10.2307/1909383
A. E. Roth and A. Postlewaite, Weak versus strong domination in a market with indivisible goods, Journal of Mathematical Economics 4 (1977) 131–137. https://doi.org/10.1016/0304-4068(77)90004-0
A. E. Roth, Incentive compatibility in a market with indivisible goods, Economics Letters 9 (1982) 127–132. https://doi.org/10.1016/0165-1765(82)90003-9
A. Abdulkadiroğlu and T. Sönmez, School choice: a mechanism design approach, American Economic Review 93 (2003) 729–747. https://doi.org/10.1257/000282803322157061

8 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces VII: Bin Packing — P(|B_N − M| ≥ 1 + u) ≤ 8 exp(−u²/(64 N E X₁²))Textbook

Motivation

Bin packing asks for the minimum number of unit-capacity bins into which a list of items with sizes in $[0,1]$ can be packed. It is one of the basic NP-hard problems of combinatorial optimization and operations research, and its stochastic version, where the item sizes are random, has a large literature (Coffman and Lueker, Probabilistic Analysis of Packing and Partitioning Algorithms, 1991). A first question about the random optimum is how strongly it concentrates around its typical value.

A short history of that question, as Talagrand recounts it on p. 151 of the source:

Late 1980s. Martingale methods (Rhee–Talagrand; McDiarmid, On the method of bounded differences, 1989) give $P(|B_N - \mathbb E B_N| \ge t) \le 2\exp(-2t^2/N)$ for $N$ i.i.d. items. The exponent ignores the item sizes.
1994. Since $B_N$ behaves like $\sum_i X_i$ when the items are small, the right exponent should be of order $t^2/(N\operatorname{var} X_1)$ , or at least $t^2/(N\,\mathbb E X_1^2)$ . The second form was proved by W. Rhee (Inequalities for the Bin Packing Problem III, Optimization 29 (1994), 381–385) using non-trivial bin-packing theory.
1995. Talagrand (Publ. Math. IHÉS 81, Chapter 6) derives the $t^2/(N\,\mathbb E X_1^2)$ bound in a few lines from his convex hull distance inequality, using only trivial facts about bin packing.

This mission formalizes that chapter.

Setting

Let $\Omega = [0,1]$ and $N \ge 0$ . A point $x = (x_1,\dots,x_N) \in \Omega^N$ is a list of item sizes. A packing into $k$ bins is a map $\sigma : \{1,\dots,N\} \to \{1,\dots,k\}$ with $\sum_{i:\sigma(i)=j} x_i \le 1$ for every bin $j$ . The bin packing number $B_N(x)$ is the least $k$ for which a packing exists ( $N$ bins always suffice; $B_N = 0$ when $N = 0$ ).

Further notation, as in Lean (TalagrandConc.BinPacking):

$\|x\|_2 = (\sum_{i \le N} x_i^2)^{1/2}$ (l2Norm);
for real $a$ , the level set $A(a) = \{y \in \Omega^N : B_N(y) \le a\}$ (levelSet);
for $A \subseteq \Omega^N$ and $x \in \Omega^N$ , $U_A(x) = \{s \in \{0,1\}^N : \exists y \in A,\ s_i = 0 \Rightarrow x_i = y_i\}$ , its convex hull $V_A(x) \subseteq \mathbb R^N$ , and the convex hull distance $f_c(A,x)$ , the Euclidean distance from $0$ to $V_A(x)$ , valued in $[0,+\infty]$ (U, V, convexDist);
$\mu$ a probability measure on $[0,1]$ , $P = \mu^{\otimes N}$ the product probability on $[0,1]^N$ , whose coordinates $X_1,\dots,X_N$ are i.i.d. items with law $\mu$ , and $\mathbb E X_1^2 = \int \omega^2\,d\mu(\omega)$ (secondMoment);
$M$ is a median of $B_N$ if $P(B_N \le M) \ge 1/2$ and $P(B_N \ge M) \ge 1/2$ (IsMedian).

Formalization targets

Goal: Theorem 6.5 (p. 152)

For every median $M$ of $B_N$ and every $u$ with $0 \le u \le 8\sqrt2\,N\,\mathbb E X_1^2$ ,

P\big(|B_N(X_1,\dots,X_N) - M| \ge 1 + u\big) \le 8\exp\Big(-\frac{u^2}{64\,N\,\mathbb E X_1^2}\Big).

Milestones

Lemma 6.1 (p. 151): $B_N(x_1,\dots,x_N) \le 2\sum_{i\le N} x_i + 1$ .
Lemma 6.2, Eq. (6.2) (p. 151): for $a > 0$ and all $x$ , $B_N(x) \le a + 2\|x\|_2\, f_c(A(a),x) + 1$ .
Lemma 6.3, Eq. (6.3) (p. 152): $P(\|x\|_2 \ge 2\sqrt N(\mathbb E X_1^2)^{1/2}) \le \exp(-2N\,\mathbb E X_1^2)$ .
Proposition 6.4, Eq. (6.4) (p. 152): for all $t > 0$ , $a > 0$ ,

P(B_N \le a)\,P\big(B_N \ge a + 4t\sqrt N(\mathbb E X_1^2)^{1/2} + 1\big) \le e^{-t^2/4} + e^{-2N\,\mathbb E X_1^2}.

The goal keeps the paper's explicit constants $8$ , $64$ and $8\sqrt2$ .

Significance

The result. Theorem 6.5 shows that the random optimum $B_N$ fluctuates on the scale $\sqrt{N\,\mathbb E X_1^2}$ rather than $\sqrt N$ . For small items ( $\mathbb E X_1^2 \to 0$ ) this is much sharper than the martingale bound, and it is the scale of the fluctuations of $\sum_i X_i$ , which is a lower bound on $B_N$ . Chapter 6 is also the first application in Part II of the paper, and its scheme recurs in the later chapters: a deterministic lemma relating the functional to $f_c$ of a level set, a tail bound for an auxiliary factor, and Theorem 4.1.1 to finish.

Formalizing it. The result is proved (Talagrand 1995; Rhee 1994 by another route). No machine-checked proof is known to exist: the platform has no random bin packing statement and no general- $\Omega$ form of Talagrand's convex distance inequality. A complete development gives a checked concentration bound for an NP-hard combinatorial optimum, plus a bin-packing layer (the optimum as a minimum over assignments, Lemma 6.1, monotonicity in the item set) that other formalizations can reuse.

Difficulty

The obvious route is a bounded-differences argument: changing one item changes $B_N$ by at most one. That route yields only the exponent $t^2/N$ , because it cannot see that small items change little. Replacing the Hamming geometry by one weighted by item sizes is the point. The weights $x_i$ depend on the point $x$ itself, so no fixed weighted Hamming distance works. The convex hull distance $f_c$ controls every weighting at once, and the resulting factor $\|x\|_2$ is random and must be controlled separately (Lemma 6.3). In Lean, the further difficulty is the probabilistic input: Theorem 4.1.1 / Eq. (4.1.2) for a general (non-finite) $\Omega = [0,1]$ is not available, and the convex-hull minimax step (Lemma 4.1.2) behind Lemma 6.2 must be formalized too.

Formalization scope

$\Omega = [0,1]$ is Mathlib's unitInterval. Coordinates are Fin N (0-based). $P$ is Measure.pi (fun _ : Fin N => μ) for μ : Measure unitInterval with IsProbabilityMeasure μ. No density is assumed.
$B_N$ is sInf {k : ℕ | IsPacking x k}, an exact minimum over assignments Fin N → Fin k, not a heuristic such as First Fit. Zero-size items are allowed, as in the paper.
$f_c$ is an infimum in ℝ≥0∞ with the Euclidean norm written out ( $+\infty$ for an empty set; Mathlib's default norm on Fin N → ℝ is the sup norm). Lemma 6.2 is stated in ℝ≥0∞.
Probabilities are ℝ≥0∞-valued. Every event in the statements ( $\{B_N \le a\}$ , $\{\|x\|_2 \ge c\}$ ) is Borel. The paper's measurability convention matters only inside the proofs.
Theorem 6.5 makes the paper's implicit $u \ge 0$ explicit, and it is stated for every median, not for a chosen one. Lean's $u^2/0 = 0$ matters only in the degenerate case $N\,\mathbb E X_1^2 = 0$ , which forces $u = 0$ . There the bound is $8$ .
Not admissible: weakening the range of $u$ (the bound fails for large $u$ when $\mathbb E X_1^2$ is small), replacing $\mathbb E X_1^2$ by $1$ , or defining $B_N$ through a heuristic or a real-valued sInf.
Infrastructure needed: Talagrand's inequality (4.1.2) on a general product probability space (posed on the platform only in a finite-alphabet form) and Lemma 4.1.2. Both are welcome as separate contributions. A Chebyshev/exponential-moment bound gives Lemma 6.3.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205, Chapter 6, pp. 151–152. https://doi.org/10.1007/BF02699376
W. Rhee, Inequalities for the Bin Packing Problem III, Optimization 29 (1994), 381–385.
C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics 1989, LMS Lecture Note Series 141, Cambridge Univ. Press, 148–188. https://doi.org/10.1017/CBO9781107359949.008
E. G. Coffman Jr., G. S. Lueker, Probabilistic Analysis of Packing and Partitioning Algorithms, Wiley, 1991.

6 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

A Functional Equation and Its Application to Resource Allocation and Sequencing Problems 2: Under Precedence Constraints, All Deadlines Can Be Met iff They Are Met in Order of Modified DeadlinesResearch Paper

Motivation

A single machine must process $n$ jobs, each with a processing time and a deadline, and some jobs must be finished before others may start. The first question of any planner is whether the deadlines can be met at all. Without precedence constraints the answer is classical: Jackson's rule (J. R. Jackson, 1955, reported by W. E. Smith, 1956) says that all jobs can be completed on time if and only if they are completed on time when sequenced by earliest deadline first. Precedence constraints break this rule, because the earliest-deadline order may put a job before one of its required predecessors.

E. L. Lawler and J. M. Moore (Management Science 16 (1969) 77–84) repair the rule by replacing each deadline by a modified deadline that accounts for the deadlines of the job's successors. Their §2 Theorem says that a single sequence, the one in increasing order of modified deadlines, decides feasibility. They use it as the first step of their dynamic programming method for sequencing with deadlines and precedence constraints: because the sequence does not depend on processing times, the jobs to be scheduled on time can always be taken in this one fixed order.

Setting

There are $n$ jobs $1,\dots,n$ . Job $j$ has a processing time $a_j \ge 0$ and a deadline $d_j \in \mathbb R$ . A sequence $\sigma$ lists every job exactly once; the machine starts at time $0$ and processes the jobs in the order of $\sigma$ , one after another, without idle time. The completion time $C_j(\sigma)$ of job $j$ is the sum of the processing times of $j$ and of all jobs before it in $\sigma$ . Job $j$ is on time in $\sigma$ if $C_j(\sigma) \le d_j$ .

Precedence constraints are a partial order $\rho$ on the jobs (reflexive, antisymmetric, transitive). If $i\rho j$ and $i \ne j$ , job $i$ must precede job $j$ ; such a $j$ is a successor of $i$ , and every job counts as one of its own successors. A sequence is consistent with $\rho$ if no job appears before a job that must precede it. The jobs are numbered so that $i\rho j$ implies $i \le j$ .

For a number $\varepsilon$ the modified deadline of job $j$ is

\bar d_j = \min\{\, d_k \mid j\rho k \,\} + j\varepsilon ,

the earliest deadline among $j$ and its successors, plus a tie-breaking term. The paper takes $\varepsilon$ to be "a small number"; here that means $\varepsilon > 0$ and $n\varepsilon < d_l - d_k$ whenever $d_k < d_l$ .

Formalization targets

Goal: the §2 Theorem (p. 78)

Let $\sigma^*$ be the sequence in which $\bar d_j$ increases. Then

\Big(\exists\,\sigma \text{ consistent with } \rho:\ C_j(\sigma) \le d_j\ \ \forall j\Big)\iff C_j(\sigma^*) \le d_j\ \ \forall j .

Milestones (from §2 and the proof of the Theorem, p. 78)

For distinct jobs, $i\rho j \Rightarrow \bar d_i < \bar d_j$ .
The sequence $\sigma^*$ is consistent with $\rho$ (the "if" part of the Theorem).
If $\bar d_j < \bar d_i$ , then $j$ or some successor $k$ of $j$ has $d_k \le d_i$ .
In an on-time sequence consistent with $\rho$ , two adjacent jobs $i, j$ (in this order) with $\bar d_i > \bar d_j$ can be interchanged, and the result is again on time and consistent with $\rho$ .

Significance

The Theorem reduces a question over all $n!$ sequences consistent with $\rho$ to the evaluation of one sequence, and the sequence depends only on the deadlines and on $\rho$ , not on the processing times. This independence is what the paper's later sections rely on: it lets a subset-selection dynamic program (Eq. (1) of the paper) process jobs in a fixed order. Without precedence constraints ( $\rho$ the identity) the Theorem is Jackson's rule. The operational form, "always take next, from among the available jobs, a job which has a successor with the earliest possible deadline", is a list-scheduling rule of the same kind as the backward rule of Lawler (1973) for $1\mid prec\mid f_{\max}$ .

The result has been proved on paper since 1969. As far as is known it has no machine-checked proof. This mission produces a formal proof of the Theorem and of the exchange step behind it, stated on the same sequence and completion-time model as the platform's existing single-machine scheduling missions.

Difficulty

The obvious argument is the exchange argument for Jackson's rule: swap an adjacent pair that is out of order and check that nothing becomes late. Two things fail without care. First, the swap must not violate precedence; this is why the deadline of a job is replaced by the minimum over its successors. Second, after the swap, job $i$ completes when job $j$ used to complete, but $d_i$ need not be at least $d_j$ : one must find a successor of $j$ that is later in the sequence, on time, and due no later than $i$ . That step uses the smallness of $\varepsilon$ : with a large $\varepsilon$ the tie-breaking term outweighs a difference of deadlines, and the Theorem fails (three jobs without precedence, $a = (2,4,3)$ , $d = (7,9,8)$ , $\varepsilon = 3$ ). Finally, the exchange step must be turned into a terminating transformation of an arbitrary feasible sequence into $\sigma^*$ , a bubble-sort argument over lists.

Formalization scope

Jobs are Fin n, 0-based: the Lean job j is the paper's job $j+1$ , and the tie-break is $((j:\mathbb N)+1)\varepsilon$ . Processing times and deadlines are real.
Sequences and completion times are the published platform definitions MooreLateJobs.Shared.IsSchedule and MooreLateJobs.Shared.completionTime (a duplicate-free list of all jobs; start at time $0$ , no idle time). Idle time never helps meet a deadline, so this loses nothing. Consistency with $\rho$ is the published LawlerPrec.MinMax.IsFeasible.
The modified deadline minimizes over insert j {k | ρ j k}, which is nonempty; for the reflexive $\rho$ of the paper this is $\{k \mid j\rho k\}$ ("considering a job to be one of its own successors").
Explicit readings of the paper's phrases:
- " $\varepsilon$ is a small number": $\varepsilon > 0$ and $n\varepsilon < d_l - d_k$ whenever $d_k < d_l$ . A fixed $\varepsilon$ is quantified universally, not hidden under an existential.
- "the sequence obtained by ordering jobs according to increasing values of $\bar d_j$ ": any duplicate-free list of all jobs along which $\bar d_j$ strictly increases. Under the hypotheses the $\bar d_j$ are distinct, so exactly one such list exists.
- "iρj implies $\bar d_i < \bar d_j$ ": stated for $i \ne j$ , since $\rho$ is reflexive.
- The pair condition "a consecutive pair with $\bar d_i > \bar d_j$ " of milestone 3 is dropped, since the claim does not use it.
Added hypothesis: $a_j \ge 0$ . The paper uses it tacitly (" $j$ will remain on time since it will be earlier in the sequence") and the Theorem is false without it.
The milestones assume only what they use (for instance, milestone 1 needs transitivity, the numbering and $\varepsilon > 0$ ). The goal assumes the full partial order of the paper.
Trivializing formalizations ruled out: $\varepsilon = 0$ or an unconstrained $\varepsilon$ ; a minimum over a possibly empty set, which Lean would assign a junk value; completion times not tied to the order of the list; and dropping "consistent with the precedence constraints" from the left-hand side, which turns the Theorem into a false variant of Jackson's rule.
Not in scope: the "order of computational steps" remarks, §3 and the later sections (other missions of this series).

Related platform items: Jackson's rule for unrestricted jobs is already posed as MooreLateJobs.NumLate.jackson (Moore 1968) and is not re-posed here; Lawler's $1\mid prec\mid f_{\max}$ theorem is posed as LawlerPrec.MinMax.sequencing_theorem. Contributions welcome: general list-exchange lemmas (adjacent swaps, bubble-sort termination toward a sorted list) are reusable well beyond this mission.

Selected references

E. L. Lawler, J. M. Moore, A Functional Equation and Its Application to Resource Allocation and Sequencing Problems, Management Science 16(1) (1969) 77–84. https://doi.org/10.1287/mnsc.16.1.77
J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3 (1956) 59–66. https://doi.org/10.1002/nav.3800030106
E. L. Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5) (1973) 544–546. https://doi.org/10.1287/mnsc.19.5.544

8 thms3 active usersReviewed

Discrete Geometry Linear Optimization·Captain: mikedeng1

The d-Step Conjecture for Polyhedra of Dimension d < 6 1: The Bounded 5-Step Conjecture Holds, Every 5-Polytope with 10 Facets Has Diameter at Most 5, i.e. Δb(5, 10) = 5Research Paper

Motivation

The simplex method and every other edge-following linear programming algorithm moves from vertex to vertex of the feasible region along its edges. The number of steps such an algorithm needs in the worst case is at least the combinatorial diameter of the feasible polyhedron: the largest distance, counted in edges, between two of its vertices. Klee and Walkup introduced the two functions that measure this worst case, $\Delta(d,n)$ for polyhedra and $\Delta_b(d,n)$ for bounded polyhedra of dimension $d$ with $n$ facets, and wrote that $\Delta(d,n)$ "represents, in a sense, the number of iterations required to solve the 'worst' linear program of $n$ inequalities in $d$ variables using the 'best' edge-following algorithm" (Klee and Walkup 1967, p. 54).

The Hirsch conjecture, reported by Dantzig in 1963, asserted $\Delta(d,n)\le n-d$ . Its diagonal cases $\Delta(d,2d)\le d$ and $\Delta_b(d,2d)\le d$ are the general and the bounded $d$ -step conjectures.

Timeline.

1957–1963: W. M. Hirsch's conjecture, reported in Dantzig's Linear Programming and Extensions (1963, pp. 160, 168), with the claim that it holds for $m\le 4$ .
Before 1967: Klee determines $\Delta(3,n)=n-3$ and $\Delta_b(3,n)=\lfloor 2n/3\rfloor-1$ and settles $\Delta_b(d,n)$ for $n\le d+4$ (Canad. J. Math. 16 and the papers cited as [9], [12], [13] by Klee and Walkup, p. 55).
1967: Klee and Walkup (Acta Math. 117) prove $\Delta_b(5,10)=5$ , show that $\Delta_b(d,2d)\le d$ for all $d$ is equivalent to the bounded Hirsch conjecture, and disprove the unbounded conjecture with $\Delta(4,8)=5$ .
2012: Santos disproves the bounded Hirsch conjecture with a 43-dimensional polytope with 86 facets (Ann. Math. 176). The bounded $d$ -step conjecture therefore fails for some $d$ , and the smallest failing $d$ is unknown; it is at least 6.

Setting

A polyhedron in $\mathbb R^d$ is a nonempty set $P=\{x:\langle a_i,x\rangle\le b_i,\ i=1,\dots,n\}$ ; a polytope is a bounded polyhedron. $P$ is a $d$ -polyhedron with $n$ facets when it has nonempty interior and none of the $n$ inequalities is redundant; then the rows are in bijection with the facets, and row $i$ is tight at $v$ exactly when $v$ lies on the $i$ -th facet. The vertices of $P$ are its extreme points. Two vertices $u\ne v$ span an edge when the segment $[u,v]$ is an extreme subset of $P$ . A path of length $l$ is a sequence of $l$ edges $[x_0,x_1],\dots,[x_{l-1},x_l]$ , and $\delta_P(x,y)$ is the least length of a path from $x$ to $y$ . Then

\Delta_b(d,n)=\max\{\delta_P(x,y): P\text{ a }d\text{-polytope with }n\text{ facets},\ x,y\text{ vertices of }P\}.

$P$ is simple when every vertex lies on exactly $d$ facets. A face is $P$ itself or the intersection of $P$ with a supporting hyperplane, never $\emptyset$ ; its dimension is that of its affine hull. A $(k_1,\dots,k_r)$ -path from $x$ to $y$ is a sequence of faces $K_1,\dots,K_r$ with $x\in K_1$ , $y\in K_r$ , $\dim K_i=k_i$ and $K_i\cap K_{i+1}\ne\emptyset$ . A $d$ -dimensional Dantzig figure $(P,x,y)$ is a $d$ -polyhedron $P$ with $2d$ facets and two vertices $x,y$ such that exactly $d$ facets are incident to $x$ and the other $d$ to $y$ . A $d$ -polytope $Q$ has property A when it has between $2d$ and $2d+2$ facets and the following holds: if its facets are split into two classes $\mathfrak X,\mathfrak Y$ of at most $d+1$ facets each, and both sets $X$ , $Y$ of vertices all of whose facets lie in $\mathfrak X$ , respectively $\mathfrak Y$ , are nonempty, then some vertex of $X$ is joined to some vertex of $Y$ by a path of length at most $d$ .

Formalization targets

Goal: 4.3 THEOREM

\Delta_b(5,10)=5.

In two halves: every $5$ -polytope with $10$ facets satisfies $\delta_P(x,y)\le 5$ for all vertices $x,y$ , and some $5$ -polytope with $10$ facets has two vertices with $\delta_P(x,y)>4$ .

Milestones, in the order the proof uses them

2.8 THEOREM (bounded part): $\Delta_b(d,n)$ is attained by two vertices of a simple $d$ -polytope with $n$ facets, and for $n\ge 2d$ by two vertices on no common facet. For $n=2d$ this is a bounded simple Dantzig figure.
3.4 PROPOSITION (a): every simple Dantzig figure admits a $(k_1,1,k_3)$ -path for positive $k_1+1+k_3=d$ .
3.1 PROPOSITION: (a) facial paths in all $d$ -dimensional simple Dantzig figures, (b) facet-avoiding facial paths in simple $d$ -polytopes with $2d+1$ facets, and (c) facet-avoiding $(1,k_1,\dots,k_r)$ -paths in bounded $(d+1)$ -dimensional figures are equivalent.
3.4 PROPOSITION (b): every bounded simple Dantzig figure admits a $(1,k_2,1,k_4)$ -path for positive $1+k_2+1+k_4=d$ .
Remark after 3.4: adjacent terms of a facial path in a simple figure merge into their sum.
Remark after 3.4, p. 68: bounded simple Dantzig figures of dimension $d\ge 2$ admit $(1,d-2,1)$ -paths.
4.1 PROPOSITION: if the middle face $Q$ of a $(1,d-2,1)$ -path $([x,x'],Q,[y',y])$ has property A, then $\delta_P(x,y)\le d$ .
4.2 LEMMA: every simple $3$ -polytope with $6$ , $7$ or $8$ facets has property A.

Significance

The result. By the paper's reductions, $\Delta_b(d,2d)\le d$ for a given $d$ is equivalent to the bounded Hirsch bound $\Delta_b(d',d'+d)\le d$ for every $d'$ . So 4.3 gives $\Delta_b(d,n)\le n-d$ for all $n\le d+5$ , which is the column $n-d=5$ of the paper's Fig. 2. Since Santos's counterexample, the smallest $d$ with $\Delta_b(d,2d)>d$ is a well-defined open number. This theorem was the first to show it is at least $6$ ; later computer-assisted work treated further small cases, including the bounded $6$ -step case (Bremner and Schewe 2011). Santos's construction starts from exactly the reduction to Dantzig figures (the "strong $d$ -step theorem" for spindles) that this paper uses.

Formalizing it. The result has been proved since 1967; no machine-checked proof of $\Delta_b(5,10)=5$ exists. The platform has the Hirsch bound in dimension $\le 3$ (Hirsch.dimension_three_bound, Hirsch.klee_three_dimensional_bound), the Klee–Walkup wedge reduction at the level of inequality descriptions (Hirsch.balanced_hpoly_transfer), products (Hirsch.diamLE_prod) and Santos's counterexample. The mission adds the facial-path calculus of §3 and the property-A argument of §4. Both are reusable in any later formal treatment of small $d$ -step cases.

Difficulty

The obvious approach, a direct case analysis of $5$ -polytopes with $10$ facets, is out of reach: there are far too many combinatorial types, and nothing bounds the search. The paper first reduces to simple polytopes, and the reduction itself (2.8) rests on a perturbation lemma (2.6) whose proof is deferred to a separate paper by Walkup: simplicity must be gained without shrinking any distance. The facial-path results then pass between bounded and unbounded figures through truncation and the wedge (3.1), and a statement about all unbounded $d$ -dimensional figures is what yields one about bounded $(d+1)$ -dimensional ones. Finally the $(d-2)$ -face $Q$ must be shown to have property A. That property fails for some simple polytopes of classes $(4,10)$ and $(5,11)$ (p. 69), so 4.2 depends on the dimension being $3$ and on the facet count being at most $8$ . Its proof uses Euler's relation and Balinski's theorem that the graph of a $3$ -polytope is $3$ -connected (posed on the platform as Balinski61.Connectivity.disjoint_paths_between_vertices).

Formalization scope

Polyhedra are Hirsch.Hpoly a b with a : Fin n → EuclideanSpace ℝ (Fin d); edges and walks are Hirsch.Adj and Hirsch.Reach from the published Hirsch_model and Hirsch_walk. The conventions are:

" $d$ -polyhedron with $n$ facets" is a facet presentation: nonempty interior and no redundant row. The rows are exactly the facets; a statement over arbitrary inequality systems would count redundant rows as facets and is not the paper's.
$\delta_P(x,y)\le L$ is Hirsch.Reach P L x y, a walk of $L$ steps that may stand still. $\Delta_b(5,10)=5$ is an upper bound for every polytope plus a witness, never a supremum of reals. A version proving only the upper bound, or only the lower bound, is not the goal.
Simple means pointed with exactly $d$ tight rows at every vertex. On a facet presentation this is equivalent to the paper's "exactly $d$ edges at each vertex".
Faces are nonempty sets $\{x\in P:\langle a_i,x\rangle=b_i,\ i\in I\}$ , and dimension is the dimension of the affine span. A Dantzig figure has Fin (2 * d) rows.
Property A is defined for a bounded face $Q$ of dimension $m$ : its facets are the $(m-1)$ -faces of $P$ inside $Q$ , and the path runs in $Q$ . This keeps 4.1, where $Q$ is a $(d-2)$ -face of a polytope in $\mathbb R^d$ , and 4.2, where $Q=P$ , under one notion. Facet counts use Set.encard.
Explicit readings: 2.8's " $\Delta_b$ can be realized as the distance … of a simple polytope" is stated polytope by polytope ( $\delta_P(u,v)\le\delta_{P'}(x,y)$ ). Only the $\Delta_b$ sentences of 2.8 are stated. 3.4's joint hypothesis on $k_1,\dots,k_4$ is split by part. The merging remark carries the needed hypothesis $k_i+k_{i+1}\le d$ . The printed "3.5 implies" on p. 67 is read as 3.4.

The paper cites two inputs without proving them: Lemma 2.6 (Walkup's simple perturbation) and Balinski's theorem. A complete development needs face lattices of H-polyhedra, wedges and truncations, and the planar-graph arguments of 4.2. The face and facial-path layer is reusable for the companion mission on $\Delta(4,8)=5$ and for other diameter problems. Contributions are welcome at every milestone, including proofs of 2.6.

Selected references

V. Klee and D. W. Walkup, The d-step conjecture for polyhedra of dimension d < 6, Acta Mathematica 117 (1967), 53–78. https://doi.org/10.1007/BF02395040
G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963.
V. Klee, Diameters of polyhedral graphs, Canadian Journal of Mathematics 16 (1964), 602–614. https://doi.org/10.4153/CJM-1964-058-5
M. L. Balinski, On the graph structure of convex polyhedra in n-space, Pacific Journal of Mathematics 11 (1961), 431–434. https://doi.org/10.2140/pjm.1961.11.431
F. Santos, A counterexample to the Hirsch conjecture, Annals of Mathematics 176 (2012), 383–412. https://doi.org/10.4007/annals.2012.176.1.7
D. Bremner and L. Schewe, Edge-graph diameter bounds for convex polytopes with few facets, Experimental Mathematics 20 (2011), 229–237. https://doi.org/10.1080/10586458.2011.564966

12 thms3 active usersReviewed

Completed

Discrete Geometry Group Theory·Captain: mikedeng1

Some Polyhedra Related to Combinatorial Problems IV: In a Group All of Whose Elements Have Order 2, or All Order 3, the Irreducible Solutions of the Group Equation Are Exactly the VerticesResearch Paper

Motivation

Every pure integer program $\min\{c\cdot x : Ax = b,\ x \ge 0 \text{ integer}\}$ can be relaxed, by dropping the nonnegativity of the basic variables of an optimal linear-programming basis, to a problem over a finite Abelian group: find nonnegative integers $t(g)$ , one for each nonzero group element, with $\sum t(g)\cdot g = g_0$ . R. E. Gomory's 1969 paper Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2 (1969) 451–558) studies the convex hulls of the solutions of these group equations, the corner polyhedra, and the master polyhedron $P(\mathcal G, g_0)$ that contains all of them as faces. These polyhedra are the source of the group-theoretic approach to cutting planes: their faces are valid inequalities for every integer program with the same group, and their vertices are the candidate optimal solutions of the group relaxation.

The paper's first section shows that every vertex of such a polyhedron is an irreducible solution, and remarks (p. 460) that the converse fails in general: a typical group has many irreducible solutions that are not vertices. Section 3F identifies a family of groups where the two notions coincide, which is what makes the vertices of these polyhedra countable in closed form.

Setting

Let $\mathcal G$ be a finite Abelian group written additively, with zero $\bar 0$ , and $\mathcal G^+ = \mathcal G\setminus\{\bar 0\}$ . For $g_0 \in \mathcal G$ the group equation is

\sum_{g\in\mathcal G^+} t(g)\cdot g = g_0, \qquad t(g) \in \{0, 1, 2, \ldots\}.

The master polyhedron $P(\mathcal G, g_0)$ is the convex hull in $\mathbb R^{\mathcal G^+}$ of its nonnegative integer solutions (for $g_0 = \bar 0$ the solution $t = 0$ is excluded). A vertex is an extreme point of $P(\mathcal G, g_0)$ .

A nonnegative integer vector $t$ is irreducible if any two integer vectors $r, s$ with $0 \le r, s \le t$ and $\sum r(g)\cdot g = \sum s(g)\cdot g$ are equal. A finite set $S$ of group elements is independent if $\sum_{g\in S} s_g g = \bar 0$ with integers $s_g$ forces $s_g g = \bar 0$ for each $g$ .

The groups of §3F are those in which every nonzero element has order 2, the groups $\mathcal G_2, \mathcal G_{2,2}, \ldots$ , or every nonzero element has order 3, the groups $\mathcal G_3, \mathcal G_{3,3}, \ldots$ .

Formalization targets

Goal: THEOREM 23 (p. 505)

If every nonzero element of $\mathcal G$ has order $p$ , with $p = 2$ or $p = 3$ , and $g_0 \ne \bar 0$ , then for every nonnegative integer solution $t$ of the group equation

t \text{ irreducible} \iff t \in \operatorname{vert} P(\mathcal G, g_0),

and the support $\{g : t(g) > 0\}$ of such a vertex is an independent set.

Milestones

THEOREM 2 (p. 460), for $P(\mathcal G, g_0)$ with $g_0 \ne \bar 0$ : every vertex is an irreducible integer solution.
The LEMMA of p. 505: for $p \in \{2, 3\}$ , $p > t > 0$ and $p > s \ge 0$ there are $0 \le t', t'' \le t$ with $t' + s \equiv t'' \pmod p$ .
The support of an irreducible solution is independent (p. 506).
A solution vanishing off the support of an irreducible $t$ agrees with $t$ modulo $p$ and dominates it (p. 506, corrected).
An irreducible $t$ minimizes $\pi$ , the indicator of the complement of its support, every minimizer dominates $t$ , and $t$ is a vertex (p. 506, corrected).
The vertex characterization (p. 506): a nonzero $t$ is a vertex of some $P(\mathcal G, g_0)$ , $g_0 \ne \bar 0$ , iff its support is independent and $t(g) < p$ for all $g$ .

Significance

THEOREM 23 turns a polyhedral question into a combinatorial one for the elementary Abelian 2- and 3-groups: the vertices of $P(\mathcal G, g_0)$ are read off from independent subsets of the group and residues below $p$ . Gomory uses this on pp. 506–507 to count all vertices of all $P(\mathcal G_{s^n}, g_0)$ exactly and to derive their asymptotic number. It also marks the boundary of the general picture: groups with elements of other orders have irreducible solutions that are not vertices.

The result has been proved since 1969; no machine-checked proof exists. The mission produces a Lean statement and, once solved, a verified proof of the theorem together with the general fact that vertices of the master polyhedron are irreducible, a reusable layer for the other group-polyhedron results of the same paper. Two sentences of the printed proof (p. 506) are false as written (see Formalization scope); formalization records their corrected forms.

Difficulty

The direction "vertex $\Rightarrow$ irreducible" holds in every group and is a midpoint argument. The difficulty is the converse: showing that an irreducible solution cannot be written as a proper convex combination of other solutions, which are infinitely many and unbounded. The natural route, exhibiting a linear objective that $t$ uniquely minimizes, does not work with the objective printed on the page: solutions with the same support as $t$ but larger entries are tied with it. The argument must control those solutions through the arithmetic of residues modulo $p$ , and this is where the exponent 2 or 3 is used; the analogous residue statement fails for $p = 5$ .

Formalization scope

T-space vectors are functions on the subtype {g : G // g ≠ 0}; integer solutions are $\mathbb N$ -valued and cast to $\mathbb R$ ; vertices are Set.extremePoints ℝ of the convex hull of the cast solutions.
"All elements of $\mathcal G$ are of order 2 or all of order 3" is read as: there is $p \in \{2, 3\}$ with every nonzero element of order $p$ . Groups mixing orders 2 and 3 are excluded, as on the page.
$g_0 \ne \bar 0$ is a hypothesis of the whole of THEOREM 23 (the page attaches it to the second sentence only). At $g_0 = \bar 0$ the solution $t = 0$ is excluded (footnote p. 474) and every nonzero solution is reducible, so the first sentence would fail. THEOREM 2 is restated for $P(\mathcal G, g_0)$ , $g_0 \ne \bar 0$ , for the same reason.
"Independent" is the page's definition with integer coefficients; the gloss "part of a group basis" is not formalized.
The letter $T$ on pp. 505–506 is the support of $t$ , not the solution set.
The page's claim that $t$ is the only solution vanishing off its support, and the unique minimizer of $\pi$ , fail literally (in $\mathbb Z_2$ with $g_0 = 1$ , $t = (1)$ and $u = (3)$ ). Milestones 4 and 5 state the corrected conclusions; the goal theorem is unaffected.
The vertex characterization adds $t \ne 0$ , which the page leaves implicit.
Ruled out: stating the order hypothesis for all elements including $\bar 0$ (unsatisfiable, so the theorem would be vacuous), dropping $g_0 \ne \bar 0$ (false statement), or replacing the master polyhedron by a bounded truncation (a different polyhedron with extra vertices).
Needed: convex hulls of infinite sets of lattice points and their extreme points (Mathlib's convexHull, extremePoints_convexHull_subset), and finite sums in Abelian groups. Contributions welcome: any of the milestones, and a general lemma that a unique minimizer of a nonnegative linear function over the integer solutions is a vertex.

Selected references

R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra and Its Applications 2 (1969), 451–558. https://doi.org/10.1016/0024-3795(69)90017-2
R. E. Gomory, On the relation between integer and noninteger solutions to linear programs, Proc. Natl. Acad. Sci. USA 53 (1965), 260–265. https://doi.org/10.1073/pnas.53.2.260
R. E. Gomory and E. L. Johnson, Some continuous functions related to corner polyhedra, Mathematical Programming 3 (1972), 23–85. https://doi.org/10.1007/BF01584976

8 thms3 active usersReviewed

Completed

Graph Theory Operations Research Optimization·Captain: mikedeng1

Sequencing a One State-Variable Machine: A Solvable Case of the Traveling Salesman Problem 1: The Spanning-Tree Interchange Tour ψ* Is a Minimal Cost TourResearch Paper

Motivation

The traveling salesman problem is NP-hard in general, so special cost structures under which it can be solved exactly in polynomial time are of lasting interest in combinatorial optimization and scheduling. One of the earliest and most cited such cases comes from sequencing on a machine whose condition is described by a single real number: a furnace temperature, a knife setting, a fill level. Each job must start at a prescribed state and leaves the machine in another, and changing the state between consecutive jobs costs money or time. Finding the cheapest cyclic order of the jobs is a traveling salesman problem with asymmetric costs.

P. C. Gilmore and R. E. Gomory solved this problem exactly in 1964 (Oper. Res. 12(5), 655–679) with an algorithm of $O(N^2)$ simple steps. Their construction became the standard example of a solvable TSP case: it is the starting point of the survey literature on polynomially solvable TSPs (Gilmore, Lawler and Shmoys 1985; Burkard, Deineko, van Dal, van der Veen and Woeginger 1998), and it appears in the no-wait flow shop literature, where two-machine no-wait scheduling reduces to exactly this cost structure.

Setting

There are $N$ jobs $J_1,\dots,J_N$ . Job $i$ must be started when the state of the machine is $A_i$ and leaves the machine in state $B_i$ ; the jobs are numbered so that $j>i$ implies $B_j\ge B_i$ . Two cost densities $f,g:\mathbb R\to\mathbb R$ satisfy $f(x)+g(x)\ge0$ : raising the state through $x$ costs $f(x)$ per unit, lowering it costs $g(x)$ per unit. The changeover cost of having job $j$ follow job $i$ is

c_{ij}=\begin{cases}\int_{B_i}^{A_j}f(x)\,dx & \text{if } A_j\ge B_i,\\ \int_{A_j}^{B_i}g(x)\,dx & \text{if } B_i>A_j.\end{cases}

A permutation $\psi$ of the jobs assigns to each job $i$ its successor $\psi(i)$ and has cost $c(\psi)=\sum_i c_{i\psi(i)}$ . It is a tour if $\psi(s)\ne s$ for every nonempty proper subset $s$ of the jobs, i.e. if it is a single cycle through all jobs.

A permutation $\varphi$ ranks the $A$ if $j>i$ implies $A_{\varphi(j)}\ge A_{\varphi(i)}$ . The interchange $\alpha_{ij}$ swaps $i$ and $j$ ; applying it to $\psi$ gives $\psi\alpha_{ij}$ (first $\alpha_{ij}$ , then $\psi$ ), which exchanges the successors of $i$ and $j$ , at cost $c_\psi(\alpha_{ij})=c(\psi\alpha_{ij})-c(\psi)$ . The graph $G_\varphi$ links $i$ and $\varphi(i)$ for every $i$ ; a spanning tree of $G_\varphi$ is a minimal set of additional arcs $R_{ij}$ that makes it connected, with cost $\sum c_\varphi(\alpha_{ij})$ . Node $q$ is of type 1 if $B_q\le A_{\varphi(q)}$ and of type 2 otherwise.

Given a minimal cost spanning tree $\tau$ of $G_\varphi$ made of arcs $R_{q,q+1}$ , the tour $\psi^*$ is obtained from $\varphi$ by executing the interchanges $\alpha_{q,q+1}$ , $R_{q,q+1}\in\tau$ , first those of type 1 in decreasing order of $q$ , then those of type 2 in increasing order of $q$ .

Formalization targets

Goal: Theorem 5

\psi^*\ \text{is a tour, and}\quad c(\psi^*)\le c(\psi)\ \text{ for every tour }\psi.

This is the paper's main theorem. It fixes no constant and no special form of $f,g$ ; it asserts that the specific tour produced by the algorithm is optimal among all tours.

Milestones

In the order the proof uses them:

Theorem 1: $c(\varphi)=\min_\psi c(\psi)$ over all permutations.
Eq. (11): under $B_j\ge B_i$ , $A_{\psi(j)}\ge A_{\psi(i)}$ , the cost of $\alpha_{ij}$ is $\int_{[B_i,B_j]\cap[A_{\psi(i)},A_{\psi(j)}]}(f+g)$ .
Lemma 1: an interchange between two different cycles merges them.
Theorem 2: the interchanges of a spanning tree, in any order, turn $\psi$ into a tour.
Lemma 2: some minimal cost spanning tree of $G_\varphi$ uses only arcs $R_{i,i+1}$ .
Lemma 5: adjacent interchanges executed on $\varphi$ in the stated order have additive cost.
Theorem 3: $\psi^*$ is a tour of cost $c(\varphi)+c_\varphi(\tau)$ .
Theorem 4: $c(\psi)\ge c(\varphi)+c^*(\psi)$ for every permutation, with the underestimate $c^*$ of (17).
Lemma 7: for a tour $\psi$ the graph $G_\psi^*$ is connected.
Lemma 8: conditions (22a) and (22b) hold for equally many indices.
Eq. (28): $c^*(\psi)\ge c_\varphi(\tau)$ for every tour $\psi$ .

Off the goal's path: Theorem 7, a minimal tour for $(f,g)$ is minimal for $(f+g,0)$ .

Significance

The theorem shows that a traveling salesman problem whose costs come from a one-dimensional state is solved by three polynomial steps: sorting (an optimal assignment), a minimum spanning tree over $N-1$ candidate arcs, and a prescribed sequence of interchanges. It is the base case for a family of later results on solvable TSPs and for the two-machine no-wait flow shop, where it gives an exact polynomial algorithm.

The result has been proved since 1964. No machine-checked proof of it is known to exist. The proof in the paper argues largely from figures ("evident geometrically"), and its statement of Theorem 3 lists the interchanges in an order that contradicts its own proof: executed in the printed order, the paper's numerical example yields a tour of cost 39 instead of the optimum 34. A formal proof settles which order is correct and fills in the geometric steps. Partial contributions are useful: the permutation facts (Lemmas 1, 8 and Theorem 2) are independent of the cost model and reusable.

Difficulty

The obvious argument fails at two points. First, interchanges do not commute in cost: once one interchange is executed, the cost of the next one depends on the new successors, so the cost of $\psi^*$ is not simply $c(\varphi)$ plus the tree cost for an arbitrary execution order. Showing that the specific order of Lemma 5 avoids all interference requires tracking how type-1 and type-2 nodes behave as interchanges are applied. Second, optimality is not a local statement: an arbitrary tour is not reachable from $\varphi$ by tree interchanges, so the lower bound needs the separate underestimate $c^*$ and a counting argument relating every tour to a spanning tree of $G_\varphi$ . Neither step follows from general minimum spanning tree theory.

Formalization scope

Jobs are Fin (n + 1) ( $N=n+1\ge1$ ), so the paper's job $i$ is index $i-1$ ; the adjacent arc $R_{q,q+1}$ is indexed by q : Fin n and joins q.castSucc and q.succ. Permutations are Equiv.Perm (Fin (n + 1)), and $\psi\alpha_{ij}$ is ψ * Equiv.swap i j (Mathlib's composition, "first $\alpha_{ij}$ , then $\psi$ "). Costs are real; (1) uses oriented interval integrals and (17) set integrals.

Explicit readings of the paper's loose phrases:

"any integrable functions $f,g$ " is read as local integrability on $\mathbb R$ , with $f+g\ge0$ the only sign condition;
"proper subsets $s$ " in (4) are nonempty proper subsets;
"a minimal set of additional arcs that connect" is minimal under inclusion; "minimal cost spanning tree" is minimal in cost among spanning trees made of adjacent arcs (by Lemma 2 the same minimum as over all trees);
"minimal cost tour" means cost at most that of every tour, i.e. every permutation that is a single cycle;
"obtained by executing the $\alpha$ 's in a particular order" (Lemma 5) is the explicit order of its proof;
ties among the $A$ leave $\varphi$ non-unique; every statement holds for every ranking $\varphi$ .

The order of $\psi^*$ is that of the proof of Lemma 5 and of steps T2–T4 (p. 673), not the order printed in Theorem 3.

Trivializing formalizations are ruled out: the goal quantifies over all tours, not over permutations (that is Theorem 1) nor over tours reachable from $\varphi$ ; $\psi^*$ is constructed from $\varphi$ and $\tau$ , not taken as an arbitrary tour of the right cost; $\tau$ is both inclusion-minimal and cost-minimal; and the costs keep both branches of (1) with general densities, not $c_{ij}=|A_j-B_i|$ . The TSP items already on the platform concern symmetric or metric distances with tours as visiting orders, a different model, and are not reused.

Needed infrastructure: cycle structure of permutations under transpositions (Mathlib's Equiv.Perm.SameCycle), connectivity of finite simple graphs, interval integrals of locally integrable functions. Contributions to any milestone are welcome; the purely combinatorial ones (Lemmas 1, 8, Theorem 2, Lemma 7) are independent of the integrals.

Selected references

P. C. Gilmore and R. E. Gomory, Sequencing a one state-variable machine: a solvable case of the traveling salesman problem, Operations Research 12(5), 1964, 655–679. https://doi.org/10.1287/opre.12.5.655
P. C. Gilmore, E. L. Lawler and D. B. Shmoys, Well-solved special cases, in The Traveling Salesman Problem (Lawler, Lenstra, Rinnooy Kan, Shmoys, eds.), Wiley, 1985, 87–143. ISBN 978-0-471-90413-7
R. E. Burkard, V. G. Deineko, R. van Dal, J. A. A. van der Veen and G. J. Woeginger, Well-solvable special cases of the traveling salesman problem: a survey, SIAM Review 40(3), 1998, 496–546. https://doi.org/10.1137/S0036144596297514
J. B. Kruskal, On the shortest spanning subtree of a graph and the traveling salesman problem, Proc. AMS 7(1), 1956, 48–50. https://doi.org/10.1090/S0002-9939-1956-0078686-7

15 thms3 active usersReviewed

Completed

Computational Geometry Discrete Geometry Graph Theory·Captain: mikedeng1

A Combinatorial Theorem in Plane Geometry: Every n-Triangulation Can Be Partitioned into at Most ⌊n/3⌋ FansResearch Paper

Motivation

In a conversation reported by Chvátal, Victor Klee asked for the smallest number $f(n)$ such that every region bounded by a simple closed $n$ -gon is dominated by $f(n)$ points: every point of the region sees one of them along a segment inside the region. In the picturesque language that gave the problem its name, $f(n)$ is the number of guards needed to watch any art gallery with $n$ walls. A comb-shaped polygon (Figure 1 of the paper) shows $f(n) \ge \lfloor n/3 \rfloor$ .

V. Chvátal's three-page note (J. Combin. Theory Ser. B 18 (1975) 39–41) proves the matching upper bound by reducing it to a purely combinatorial statement about triangulated polygons: every such triangulation splits into at most $\lfloor n/3\rfloor$ fans, and a fan is watched by a single guard. The combinatorial theorem is the result this mission formalizes.

Timeline.

1973: Klee poses the question to Chvátal (the paper reports the conversation; the year is O'Rourke's).
1975: Chvátal proves $f(n) = \lfloor n/3\rfloor$ via the fan partition theorem, by induction on $n$ with a four-case analysis.
1978: S. Fisk gives the short proof by 3-colouring the vertices of the triangulation (J. Combin. Theory Ser. B 24 (1978) 374); the smallest colour class is a set of at most $\lfloor n/3\rfloor$ vertices meeting every triangle.
1987 onwards: J. O'Rourke's monograph Art Gallery Theorems and Algorithms (Oxford University Press, 1987) makes the theorem the starting point of a large literature on guarding problems.

Setting

An $n$ -triangulation (p. 39) is a planar graph $G$ with $n$ vertices such that one face is bounded by an $n$ -gon and every other face by a triangle. Its vertices are labelled $0, 1, \dots, n-1$ in their cyclic order around the $n$ -gon, and indices are taken mod $n$ ; the sides of the $n$ -gon are the pairs $\{a, a+1\}$ . Every other edge of $G$ is inner; it is a diagonal $\{a, b\}$ of the $n$ -gon. Two diagonals cross when their endpoints are distinct and alternate around the polygon.

Combinatorially, an $n$ -triangulation requires $n\ge 3$ and is the same thing as a set $D$ of diagonals that pairwise do not cross and is maximal with this property. Its triangles are the 3-element vertex sets all of whose pairs are edges of $G$ ; there are $n - 2$ of them, and they are the bounded faces.

Two triangles are adjacent when they share an edge. A set $F$ of triangles is dual-connected when any two of its members are joined by a chain of adjacent members; such an $F$ is a sub-polygon of $G$ , a $k$ -triangulation with $k = |F| + 2$ , whose inner edges are the edges shared by two of its triangles. Following the paper, a $k$ -triangulation is a fan if one of its vertices, the centre, meets all $k-3$ of its inner edges. A partition of $G$ into fans is a family of fans, pairwise disjoint as sets of triangles, covering all triangles of $G$ . Fans may share vertices and edges.

Formalization targets

Goal: Chvátal's theorem (p. 39)

For every $n \ge 3$ and every $n$ -triangulation $G$ there is a partition of $G$ into $m$ fans with

m \le \left\lfloor \frac{n}{3} \right\rfloor .

Milestones (the claims of the proof, pp. 40–41, in attack order)

Base case. Every $n$ -triangulation with $3 \le n \le 5$ is a fan.
Least span. For $n \ge 6$ , let $k$ be the least integer with $k \ge 4$ such that $G$ has an inner edge $\{j, j+k\}$ . Then $k \le 6$ .
The cut. An inner edge $\{j, j+k\}$ with $2 \le k \le n-2$ cuts $G$ into a $(k+1)$ -triangulation $G_1$ on $j, \dots, j+k$ and an $(n-k+1)$ -triangulation $G_2$ on $j+k, \dots, j$ , whose triangles together are those of $G$ .
The four cases. If $4 \le k \le 6$ and every inner edge $\{a,b\}$ of $G_1$ (relabelled $0,\dots,k$ , $a<b$ ) has $b - a \le 3$ , then $G_1$ is a fan or one of three explicit configurations (cases (2)–(4) of the paper), up to the mirror image $i \mapsto k - i$ .
Tightness. For every $n \ge 3$ some $n$ -triangulation admits no partition into fewer than $\lfloor n/3\rfloor$ fans:

\forall n\ge 3\ \exists G\ \forall P:\quad |P| \ge \lfloor n/3\rfloor .

The goal's only constant is the paper's $\lfloor n/3 \rfloor$ , which milestone 5 shows is best possible.

Significance

The result. The fan partition is a strengthening of the guard bound: the centres of the fans form a set of at most $\lfloor n/3\rfloor$ vertices meeting every triangle, but the partition also says that the triangles split into star-shaped pieces, each visible from one vertex. With the existence of triangulations of simple polygons it yields $f(n) \le \lfloor n/3 \rfloor$ , the art gallery theorem; with Figure 1 it gives $f(n) = \lfloor n/3\rfloor$ .

Formalizing it. The theorem has been proved since 1975, and the platform already has Fisk's consequence: ProofsInTheBook.Chapter36.chapter36 and chapter36_artgallery_combinatorial (Proofs from THE BOOK, Chapter 36) prove that an inductively built family of triangles has a hitting set of at most $n/3$ vertices, and ProofsInTheBook.PolygonGeometryDischarge.artGallery_strict_of_residue proves a geometric guard bound conditional on two assumed inputs. Neither states the fan partition, which is strictly stronger than a hitting set, and neither uses the cyclic labelling of a triangulated polygon. This mission asks for a machine-checked proof of Chvátal's own theorem and of the claims of his proof, on a reusable encoding of triangulated polygons (cyclic labels, non-crossing diagonals, triangles, cutting along a diagonal) that other results on polygon triangulations can build on.

Difficulty

The induction itself is short on paper; the work is in what the paper calls easy. Cutting $G$ along a diagonal and relabelling each piece cyclically must be shown to produce triangulations again, with the triangles split exactly between the two pieces; this is a statement about non-crossing chords that has no counterpart in Mathlib. The case analysis "it is easy to verify that we have one of the following four cases" is an enumeration of all triangulations of a 5-, 6- or 7-gon whose diagonals have span at most 3, and its exhaustiveness (including the mirror images of (2) and (4)) is precisely what the four inductive constructions rely on. The constructions then enlarge one fan of a smaller triangulation, so the induction must be carried out for partitions of arbitrary triangulations, with fans that share edges.

Formalization scope

Encoding of "planar graph". Mathlib has no planar embeddings. An $n$ -triangulation is encoded as the labelled $n$ -cycle on Fin n (vertex $i$ is the paper's $i+1$ ) plus a finset D : Finset (Sym2 (Fin n)) of diagonals that pairwise do not cross and is maximal. Maximality is binding: without it the empty set would "triangulate" every polygon and the goal would hold vacuously.
Triangles are the 3-element vertex sets whose pairs are all edges; in a triangulated polygon every 3-cycle bounds an inner face.
"Partitioned into fans" means a finset of fans, pairwise disjoint as sets of triangles, covering all triangles. A fan must be nonempty, dual-connected, and have a centre on all of its inner edges (edges shared by two of its triangles). Dropping dual-connectedness would turn the goal into Fisk's hitting-set bound; dropping the centre would let the whole triangulation be one "fan". Both clauses are stated.
"[n/3]" is the floor, n / 3 in ℕ. The goal assumes only $n \ge 3$ .
"The least $k \ge 4$ such that $G$ has an edge $(j, j+k)$ " is read over inner edges, with the minimality stated explicitly; read over all edges, a side of span $n-1$ would make the claim trivial for $n = 6, 7$ .
"Cuts $G$ into" is stated for every inner edge of span $2 \le k \le n-2$ (the paper's $4 \le k \le 6$ is a special case), as the pulled-back diagonal sets being triangulations and the triangles splitting between the pieces.
"Mirror image" is the relabelling $i \mapsto k - i$ of $G_1$ (Fin.rev); the four cases are an explicit disjunction on the diagonal set of $G_1$ . The minimality of $k$ enters as the hypothesis that inner edges of $G_1$ have span at most 3.
"Cannot be improved" is stated combinatorially, for the theorem itself; the paper argues it through Figure 1.
Not formalized: Klee's function $f(n)$ , Figure 1's lower bound and the corollary $f(n) \le \lfloor n/3\rfloor$ (p. 41). They need simple polygons in the plane, their interiors, visibility and the existence of triangulations, none of which is available unconditionally.

All definitions are in one file, ChvatalArtGallery.FanPartition.Triangulation; the triangle and cut machinery is reusable for any result on triangulated polygons. Proofs of the milestones, general lemmas on non-crossing diagonal sets (the count $|D| = n-3$ , existence of ears, the dual tree), and alternative proofs of the goal are all welcome.

Selected references

V. Chvátal, A combinatorial theorem in plane geometry, J. Combin. Theory Ser. B 18 (1975) 39–41. https://doi.org/10.1016/0095-8956(75)90061-1
S. Fisk, A short proof of Chvátal's watchman theorem, J. Combin. Theory Ser. B 24 (1978) 374. https://doi.org/10.1016/0095-8956(78)90059-X
J. O'Rourke, Art Gallery Theorems and Algorithms, Oxford University Press, 1987. https://www.science.smith.edu/~jorourke/books/ArtGalleryTheorems/
M. Aigner, G. M. Ziegler, Proofs from THE BOOK, Springer, Chapter "How to guard a museum". https://doi.org/10.1007/978-3-662-57265-8

7 thms3 active usersReviewed

Completed

Graph Theory Operations Research·Captain: mikedeng1

On Representatives of Subsets: Two Partitions into m Classes Have a Common System of Representatives When Any k Classes of One Meet at Least k Classes of the OtherResearch Paper

Motivation

Many assignment questions reduce to one combinatorial question: given finitely many sets, can one choose a different element from each? Workers are matched to jobs they are qualified for, rows of a matrix to columns with nonzero entries. The criterion for when this is possible is Hall's marriage theorem, first stated and proved by P. Hall in a five-page note in 1935 (DOI 10.1112/jlms/s1-10.37.26). It underlies bipartite matching, the integrality of the assignment polytope, the Birkhoff–von Neumann theorem on doubly stochastic matrices, and transversal theory in matroids.

Hall's note was written with a second question in view. In 1916 D. König proved, in the language of bipartite graphs, that if a set of $mn$ things is divided into $m$ classes of $n$ things in two ways, then one can choose $m$ things that represent every class of both divisions at once ("Über Graphen und ihre Anwendungen", Math. Annalen 77 (1916), 453). Van der Waerden (1927) and Sperner (1927) gave the set-theoretic form and a short proof. Hall's contribution was a criterion for a common system of representatives of two divisions in which the classes need not have equal sizes, obtained from the marriage theorem in two short steps.

Setting

Let $S$ be any set, finite or infinite, and let

T_1, T_2, \dots, T_m \tag{1}

be a finite system of subsets of $S$ . The sets $T_i$ may be infinite and need not be distinct; when one speaks of $k$ of the sets, $k$ indices are meant, so a repeated set is counted with multiplicity. A complete set of distinct representatives, or C.D.R., of (1) is a choice of pairwise distinct elements $a_1, \dots, a_m$ of $S$ with

a_i \in T_i \qquad (i = 1, \dots, m).

The system satisfies Hall's condition when any $k$ of the sets contain between them at least $k$ elements of $S$ , for $k = 1, \dots, m$ . The meet of all C.D.R.s, written $R$ , is the set of elements of $S$ that occur as a representative in every C.D.R. of (1).

A division of $S$ into classes is a family of pairwise disjoint sets $S_1, S_2, \dots$ whose union is $S$ . The paper writes $A \wedge B$ and $A \vee B$ for intersection and union; this mission writes $A \cap B$ and $A \cup B$ .

In Lean the system is T : ι → Set α over a finite index type, a C.D.R. is an injective a : ι → α with a i ∈ T i (IsCDR), Hall's condition is HallCondition, and the meet of all C.D.R.s is cdrMeet, all in the namespace HallReps.CDR.

Formalization targets

Goal: Theorem 3 (pp. 29–30)

Let $S$ be divided into $m$ classes in two ways, $S = S_1 \cup \dots \cup S_m = S_1' \cup \dots \cup S_m'$ , each a division into pairwise disjoint classes. If, for each $k$ , any $k$ of the classes $S_j'$ contain between them elements from at least $k$ of the classes $S_i$ , then for some permutation $\sigma$ of $\{1, \dots, m\}$ there are elements

a_i \in S_i \cap S'_{\sigma(i)} \qquad (i = 1, \dots, m).

The set $S$ and the classes may be infinite, and no class is assumed non-empty.

Milestones

Lemma (p. 27). If $a$ is a C.D.R. of (1) and $R$ is the meet of all C.D.R.s, the sets $T_i$ whose representative $a_i$ lies in $R$ contain between them exactly the elements of $R$ , and there are $|R|$ of them.
Induction step, p. 28. With (4) the system $T_1, \dots, T_{m-1}$ and $R^*$ the meet of its C.D.R.s: if $T_m \not\subseteq R^*$ , then (1) has a C.D.R.
Induction step, p. 29. If (4) has a C.D.R. and $T_m \subseteq R^*$ , then some $\rho + 1$ of the sets, including $T_m$ , have union exactly $R^*$ , where $\rho = |R^*|$ .
Theorem 1 (p. 27). Hall's condition is sufficient for a C.D.R. of (1).
Theorem 2 (p. 29). If $S$ is divided into any number of classes and any $k$ of the sets $T_i$ contain between them elements from at least $k$ classes, there are $a_i \in T_i$ lying in pairwise different classes.

A companion item states König's theorem (§1, p. 26), which the paper deduces from Theorem 3 on p. 30.

Significance

Theorem 3 gives a necessary and sufficient criterion for two partitions of a set into $m$ classes to admit a common system of representatives. Necessity is immediate, and the paper proves sufficiency. It contains König's theorem, and through it the statement that a regular bipartite multigraph has a perfect matching, as the case of equal class sizes. Hall remarks that R. Rado's generalization of König's theorem (1933) also follows. Theorem 2, the passage from "distinct elements" to "elements of distinct classes", is the form used for transversals of partitions and is the first instance of what later became the theory of common transversals and matroid intersection.

On the formal side, Hall's theorem for finite sets is in Mathlib as Finset.all_card_le_biUnion_card_iff_existsInjective' (in Mathlib/Combinatorics/Hall/Finite.lean), and the platform already has a proved equivalence for arbitrary sets with a finite index type (YogeshwaranDM.sdr_iff, included in this mission as a reference item) as well as finite bipartite-graph forms. For that reason Theorem 1 is a milestone and not the goal. What this mission adds is Hall's own proof structure, namely the meet of all C.D.R.s and the Lemma about it, which has not been formalized; Theorems 2 and 3 for divisions of a possibly infinite set; and König's theorem in its set-partition form. To our knowledge none of these statements has a machine-checked proof on the platform.

Difficulty

Theorem 3 does not follow from Theorem 1 applied to the classes $S_j'$ directly. Theorem 1 produces distinct elements, but the conclusion needs elements in distinct classes $S_i$ , and two distinct elements of $S_j'$ may lie in the same $S_i$ . The paper's route goes through Theorem 2, which allows any number of classes. That route needs Theorem 1 for systems whose sets can be infinite, because a single $T_i$ may meet infinitely many classes, so the finite-set version of Hall's theorem in Mathlib is not enough on its own. In Hall's own proof of Theorem 1, the work lies in the Lemma. It is an exchange statement about all C.D.R.s at once, whose object $R$ is defined by a universal quantifier over C.D.R.s, and it must be established over an arbitrary finite index type with possibly infinite sets.

Formalization scope

The ground set is a type α, with no finiteness or decidability assumed. The system (1) is T : ι → Set α with [Finite ι] (or Fin (m + 1) in the two induction steps, where the paper's $m$ is the Lean m + 1, its last set is T (Fin.last m), and (4) is fun i : Fin m => T i.castSucc).
Cardinalities of unions of the $T_i$ are Set.encard in ℕ∞, so an infinite union counts as infinite. Set.ncard is used only for subsets of Fin m, for the finite set $R^*$ (with its finiteness stated), and in König's theorem.
" $k$ of the sets" is a Finset ι of indices, so repeated sets count with multiplicity.
Divisions into classes are class maps: cls : α → κ in Theorem 2, with κ arbitrary, and p q : α → Fin m in Theorem 3 and König's theorem. A class map makes the classes cover $S$ and be pairwise disjoint by construction. Empty classes are allowed.
In Theorem 3 the permutation is existential and chosen together with the representatives. $a_i \in S_i \cap S'_{\sigma(i)}$ is p (a i) = i ∧ q (a i) = σ i.
Added or dropped hypotheses: the Lemma assumes a C.D.R. exists, as the page does (without one, cdrMeet is all of α). The first induction step omits the page's C.D.R. of (4), because its hypothesis already implies one. König's theorem adds $0 < n$ , which the page presumes and without which the statement is false.
The trivializing formalizations are ruled out. Typing the $T_i$ as Finset α would reduce Theorem 1 to Mathlib and lose the page's "It is not necessary that the sets $T_i$ shall be finite". Measuring unions by ncard would make Hall's condition fail exactly when a union is infinite. An infinite index type would make Theorem 1 and the Lemma false. None of these is used.
Useful contributions include proofs of the Lemma and of the induction steps, a proof of Theorem 1 either from them or from Mathlib's Hall theorem via a reduction to finite sets, and the reductions Theorem 1 → Theorem 2 → Theorem 3 → König.

Selected references

P. Hall, On representatives of subsets, J. London Math. Soc. 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26
D. König, Über Graphen und ihre Anwendungen auf Determinantentheorie und Mengenlehre, Math. Annalen 77 (1916), 453–465. https://doi.org/10.1007/BF01456961
B. L. van der Waerden, Ein Satz über Klasseneinteilungen von endlichen Mengen, Abh. Math. Sem. Hamburg 5 (1927), 185–188. https://doi.org/10.1007/BF02952519
R. Rado, Bemerkungen zur Kombinatorik im Anschluss an Untersuchungen von Herrn D. König, Sitzungsber. Berliner Math. Ges. 32 (1933), 60–75.
Mathlib, Mathlib/Combinatorics/Hall/Finite.lean and Mathlib/Combinatorics/Hall/Basic.lean. https://github.com/leanprover-community/mathlib4

8 thms3 active usersReviewed

Completed

Graph Theory·Captain: mikedeng1

The Intersection Graphs of Subtrees in Trees Are Exactly the Chordal Graphs: A Finite Graph Is a Subtree Graph If and Only If It Is ChordalResearch Paper

Motivation

Chordal graphs (graphs in which every long cycle has a shortcut edge) appear wherever a sparse symmetric structure has to be eliminated without creating new interactions: Gaussian elimination on sparse symmetric matrices (Rose 1970), acyclic database schemes, junction trees for probabilistic graphical models, and phylogenetic and scheduling problems. In all of these applications the useful object is not the graph itself but a tree representation of it: a tree on which every vertex of the graph is a connected piece, and adjacency is overlap.

The theorem of this mission says that such tree representations exist exactly for chordal graphs. It extends the theory of interval graphs (intersection graphs of intervals on a line, i.e. of subpaths of a path), whose characterization was asked by Hajós (1957) and given by Lekkerkerker–Boland (1962), Gilmore–Hoffman (1964) and Fulkerson–Gross (1965), from paths to arbitrary trees.

Timeline. Dirac (1961) proved that every chordal graph has a simplicial vertex, a vertex whose neighbourhood is a complete subgraph. Rose (1970) used this to recognize chordal graphs efficiently, and Gavril (1972) showed that a chordal graph has at most as many maximal cliques as vertices. Renz (1970) studied intersection graphs of arcs in trees. Gavril (1974), together with Buneman (1974) and Walter (1972/1978) independently, proved that the intersection graphs of subtrees of trees are exactly the chordal graphs, and gave an algorithm that builds such a representation.

Setting

All graphs are finite and simple: a graph $G$ has a finite vertex set $V$ and a symmetric irreflexive adjacency relation. A completely connected set is a set of pairwise adjacent vertices, and a clique is a maximal completely connected set. The set of cliques of $G$ is $\mu(G)$ , and $\mu_v(G) \subseteq \mu(G)$ is the set of cliques containing the vertex $v$ . For a vertex $v$ , $\Gamma v$ is the set of its neighbours; $v$ is simplicial if $\Gamma v$ is completely connected.

$G$ is chordal if every simple circuit $v_1, \dots, v_k, v_1$ with $k > 3$ vertices has a chord: an edge of $G$ joining two vertices of the circuit that are not consecutive on it.

A tree $T$ is a connected graph without simple circuits. A subtree of $T$ is a nonempty set of tree vertices that induces a connected subgraph of $T$ . A family $(\bar v)_{v \in V}$ of subtrees of $T$ represents $G$ if, for all distinct $u, v \in V$ ,

u \sim_G v \iff \bar u \cap \bar v \neq \varnothing.

$G$ is a subtree graph if it has such a representation on some tree, and a proper subtree graph if it has one in which no subtree is contained in another.

Formalization targets

Goal: Theorem 3 (p. 51)

G \text{ is a subtree graph} \iff G \text{ is chordal}

for every finite simple graph $G$ . The paper calls this "the main theorem of this paper".

Milestones

The three-point remark (p. 50): subtrees of a tree that each contain two of three given points have a common point.
Lemma 1 (p. 50): for every completely connected set $A$ of a subtree graph, $\bigcap_{v \in A} \bar v \neq \varnothing$ .
For two different cliques $A_1 \neq A_2$ , $\big(\bigcap_{v\in A_1}\bar v\big) \cap \big(\bigcap_{v \in A_2} \bar v\big) = \varnothing$ (p. 50).
Theorem 2 (p. 51): $G$ is a subtree graph if and only if there is a tree $T$ with vertex set $\mu(G)$ such that $T(\mu_v(G))$ is connected for every $v \in V$ (a clique tree).
Subtree graphs are chordal (proof of Theorem 3, p. 51).
Dirac–Rose (cited, p. 48): every nonempty finite chordal graph has a simplicial vertex.
For a simplicial vertex $v$ , $\{v\} \cup \Gamma v$ is a clique (p. 52).
Induced subgraphs of chordal graphs are chordal (p. 52).
Every finite chordal graph has a clique tree (pp. 51–52).

Companion statements (§3 and §1)

G \text{ subtree graph} \implies G \text{ proper subtree graph}, \qquad \text{subtree} \iff \text{proper subtree} \iff \text{chordal},

and, cited on p. 49, $|\mu(G)| \le |V|$ for a nonempty finite chordal graph.

Significance

The result. The theorem turns a forbidden-structure condition (no chordless cycle of length at least four) into a constructive geometric one (a tree model), and Theorem 2 makes the tree canonical: its vertices are the maximal cliques. Clique trees are the data structure behind junction-tree inference, multifrontal sparse Cholesky factorization, and dynamic programming over tree decompositions; the treewidth of a graph is defined through chordal supergraphs and their clique trees. The proper-subtree result of §3 shows a contrast with interval graphs, where proper interval graphs form a strictly smaller class.

Formalizing it. The theorem is classical and fully proved in the literature, but Mathlib has no notion of chordal graph, no Helly property for subtrees, no clique trees and no simplicial-vertex theorem. This mission produces those definitions together with the characterization, the Helly property for finite families of subtrees, the Dirac–Rose theorem under the cycle–chord definition, and closure of chordality under induced subgraphs. As far as is known, none of these results has a machine-checked proof in Lean under the cycle–chord definition.

Difficulty

The "only if" direction is short on paper but rests on tree facts that are not packaged in Mathlib: a connected vertex set of a tree contains the unique path between any two of its vertices, and three pairwise paths of a tree meet. The "if" direction must produce a tree on the set $\mu(G)$ of maximal cliques, and the maximal cliques of a graph are not stable under passing to induced subgraphs: a clique of a subgraph need not be a clique of $G$ , and two cliques of $G$ may restrict to the same set. Relating $\mu(G)$ to $\mu(G_1)$ for a smaller graph $G_1$ is the step where informal arguments are routinely loose, and it is where a formal proof spends most of its effort. The Dirac–Rose theorem is cited rather than proved in the paper and needs a separate development.

A tempting shortcut is to define chordality as the existence of a perfect elimination ordering. This builds the Dirac–Rose theorem into the definition and changes the theorem being proved; it is excluded here.

Formalization scope

Graphs are G : SimpleGraph V with [Fintype V] in the goal, Theorem 2, the clique-tree claim, Dirac–Rose and the clique count. Milestones whose claims hold for infinite graphs (Lemma 1 for finite $A$ , the three-point remark, the clique-disjointness claim, subtree ⇒ chordal, induced chordality, the simplicial clique, subtree ⇒ proper subtree) are stated without finiteness, which makes them stronger. $V$ may be empty in the goal and in Theorem 2; Dirac–Rose and the clique count assume $V$ nonempty, which they need.
Chordality is the cycle–chord definition: for every cycle walk c of length at least 4 there are vertices x, y on c with G.Adj x y and s(x, y) not an edge of c.
The paper's trees are topological and its subtrees connected closed portions that may end inside an edge. Here a tree is a combinatorial tree T : SimpleGraph β with T.IsTree (not necessarily finite), and a subtree is a vertex set s with (T.induce s).Connected; subdividing the topological tree at all end-points shows the class of subtree graphs is the same. The tree type lives in the same universe as V.
The representing family is indexed by V; adjacency is compared only for distinct vertices. A clique is Maximal G.IsClique s; $\mu(G)$ is the subtype of such sets.
Two trivializing formalizations are ruled out: chordality as a perfect elimination ordering, and representations by sets that need not be connected (with arbitrary sets every graph is an intersection graph, and the "only if" half would be false).
Needed infrastructure: paths and connected sets in trees, Helly's property for subtrees, maximal cliques and their behaviour under induced subgraphs, and simplicial vertices. The tree lemmas and the Dirac–Rose theorem are reusable well beyond this mission. Proofs of any milestone, alternative routes (for example via perfect elimination orderings proved equivalent to the cycle–chord definition), and the clique-count bound are all welcome.

Selected references

F. Gavril, Algorithms for minimum coloring, maximum clique, minimum covering by cliques, and maximum independent set of a chordal graph, SIAM J. Comput. 1 (1972) 180–187. https://doi.org/10.1137/0201013
F. Gavril, The intersection graphs of subtrees in trees are exactly the chordal graphs, J. Combin. Theory Ser. B 16 (1974) 47–56. https://doi.org/10.1016/0095-8956(74)90094-X
G. A. Dirac, On rigid circuit graphs, Abh. Math. Sem. Univ. Hamburg 25 (1961) 71–76. https://doi.org/10.1007/BF02992776
D. J. Rose, Triangulated graphs and the elimination process, J. Math. Anal. Appl. 32 (1970) 597–609. https://doi.org/10.1016/0022-247X(70)90282-9
P. Buneman, A characterisation of rigid circuit graphs, Discrete Math. 9 (1974) 205–212. https://doi.org/10.1016/0012-365X(74)90002-8
J. R. Walter, Representations of chordal graphs as subtrees of a tree, J. Graph Theory 2 (1978) 265–267. https://doi.org/10.1002/jgt.3190020311
D. R. Fulkerson and O. A. Gross, Incidence matrices and interval graphs, Pacific J. Math. 15 (1965) 835–855. https://doi.org/10.2140/pjm.1965.15.835

11 thms3 active usersReviewed

Operations Research Theoretical Computer Science·Captain: mikedeng1

One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties 1: Minimizing the Total Discrepancy from Preferred Times Is NP-CompleteResearch Paper

Motivation

Scheduling with earliness and tardiness penalties asks for schedules in which a job finishing early is as undesirable as a job finishing late. The model fits production planned for just-in-time delivery, where finished goods held before their due date cost money, and sequences of experiments tied to fixed external events. It departs from classical scheduling, in which finishing early is never penalized.

Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988) 330–348) study the symmetric version on one processor: each task has a preferred starting time, and the penalty is the absolute deviation from it. Their §2.1 settles the complexity of the most natural objective, the sum of these deviations, by proving it NP-complete. The result explains why the rest of their paper, and much of the later literature, turns to special cases that can be solved efficiently: a fixed task order, equal task lengths, or the maximum deviation instead of the sum.

A short history of the model:

Kanet (1981) minimized total absolute deviation from a common due date that is large enough not to constrain the schedule, by a sorting rule. The special case in the middle of §2.1 is the midtime version of this problem.
Garey, Tarjan and Wilfong (1988) proved the problem with arbitrary preferred times NP-complete (THEOREM 1, this mission), and gave an $O(N\log N)$ algorithm for a fixed task order.
Hall, Kubiak and Sethi (1991) proved that the common-due-date problem becomes NP-hard when the due date is restrictive. The reduction of THEOREM 1 already uses a common preferred midtime that is not large, together with one extra task that pins the right end.

Setting

There are $N$ tasks $T_1,\dots,T_N$ . Task $T_i$ has a length $l_i$ and a preferred midtime $M_i$ . A schedule $S$ assigns every task a starting time $s_i\ge0$ such that no two tasks overlap on the single processor: for $i\ne j$ , either $s_i+l_i\le s_j$ or $s_j+l_j\le s_i$ . Idle time is allowed. The actual midtime of $T_i$ is $m_i(S)=s_i+l_i/2$ , and the total discrepancy of $S$ is

\mathrm{cost}(S)=\sum_{i=1}^N |m_i(S)-M_i| .

The paper works with midtimes because the special case below is then symmetric. Preferred midtimes and preferred starting times $a_i$ are interchangeable through $a_i=M_i-l_i/2$ .

Total discrepancy (the decision problem). Given $N,k\in\mathbb Z^+$ and $M_i,l_i\in\mathbb Z^+$ , is there a schedule with $\mathrm{cost}(S)\le k$ ?

Even-odd partition. Given positive integers $x_1<x_2<\dots<x_{2n}$ , can they be split into two sets of equal sum so that each set contains exactly one of $x_{2i-1},x_{2i}$ for every $i$ ?

The special case. For tasks $T_0,\dots,T_{2n}$ with $0<l_0<l_1<\dots<l_{2n}$ and one common preferred midtime $M>\sum_i l_i$ , write $A(S)=\{T_i: m_i(S)<M\}$ and $B(S)=\{T_i:m_i(S)>M\}$ . A schedule is ordered if, on each side of $M$ , shorter tasks lie nearer to $M$ . The bracket $[A_n,\dots,A_1,T_0@M,B_1,\dots,B_n]$ is the schedule that puts $T_0$ at midtime $M$ and packs the listed tasks against it in the listed order.

Formalization targets

Goal: THEOREM 1

\text{Partition is NP-complete}\ \Longrightarrow\ \text{Total discrepancy is NP-complete.}

The hypothesis is the one result the paper imports (Garey and Johnson, 1979). The conclusion includes membership in NP and polynomial-time many-one reductions from every NP language, with Turing machines as the model of computation.

Milestones, in attack order

Even-odd partition is in NP; the instance $x_1=1$ , $x_{2i}=x_{2i-1}+y_i$ , $x_{2i+1}=x_{2i}+1$ built from a Partition instance $Y$ is a yes-instance if and only if $Y$ is; and LEMMA 1, even-odd partition is NP-complete.
The special case: a minimum cost schedule has no gaps and is ordered; LEMMA 2 (some $m_i(S)=M$ ), LEMMA 3 ( $|A(S)|=|B(S)|$ ), LEMMA 4 ( $m_0(S)=M$ ), LEMMA 5 (swapping $A_i$ and $B_i$ in a bracket keeps the cost), LEMMA 6 ( $\{A_i,B_i\}=\{T_{2i},T_{2i-1}\}$ in a minimum cost bracket), and the minimum cost

k=\sum_{i=1}^n(l_{2i}+l_{2i-1})\left(n-i+\tfrac12\right)+l_0\,n .

At the midtime $M=\frac12\sum_{i=0}^{2n}l_i$ used in the reduction, every schedule of $T_0,\dots,T_{2n}$ costs at least $k$ ; equality forces the ordered, gap-free form in item 2.
The reduction: the instance D with $l_0=x_1-1$ , $l_i=x_i$ , $l_{2n+1}=2$ , $M_j=M=\sum_{i\le 2n}l_i/2$ , $M_{2n+1}=2M+1$ has a schedule of cost at most $k$ if and only if $X$ has an even-odd partition. Total discrepancy is in NP.

Significance

THEOREM 1 is the hardness boundary for one-processor scheduling with symmetric earliness–tardiness penalties and arbitrary preferred times. It is the reason exact algorithms for this objective are enumerative, and the reason polynomial results are sought under extra structure, such as the fixed-order algorithm of the same paper. The special-case lemmas characterize every optimal schedule for a common, unrestrictive midtime, not just one of them: shortest task centered at $M$ , the $i$ -th pair of lengths in the $i$ -th positions on either side, either member on either side. This characterization holds independently of the reduction.

The result has been proved since 1988, and no machine-checked version of it is known to us. A formalization adds three things. First, the parts the paper calls "straightforward" or "a simple exercise", membership of both problems in NP. Second, the two places where the published argument is imprecise. The instance D has half-integer midtimes and threshold although the decision problem asks for integers, so a correct reduction must rescale. And the special-case lemmas are proved for a large midtime but applied with $M=\sum_i l_i/2$ , so they must be restated for every $M$ . Third, a reusable formal treatment of absolute-deviation scheduling objectives and of reductions between number problems written in binary.

Difficulty

The obvious argument fails at the step from the special case to the instance D. The lemmas on pp. 333–336 assume the common midtime is large, so that the constraint $s_i\ge0$ never binds. In D the midtime is $M=\sum_{i=0}^{2n}l_i/2$ , exactly half the total length, and the reduction works because the constraint binds. The tasks before $M$ must fit in $[0,M-l_0/2]$ , and the extra task $T_{2n+1}$ must sit at $[2M,2M+2]$ . Together these force the two sides to have equal total length. A proof that only cites the large- $M$ lemmas proves nothing about D. Conversely, dropping $s_i\ge 0$ makes the reduction false: put the shorter element of every pair after $M$ .

The other obstacle is the complexity bookkeeping. NP-completeness here means Turing machines, binary codes, and polynomial bounds, and a full proof must compute D from the code of $X$ , double the times to clear the half-integers, and certify membership in NP for a problem whose schedules have real starting times. The certificate cannot be the real starting times themselves.

Formalization scope

Everything is real-valued except the instance codes. Schedules have real starting times $s_i\ge0$ , and integer data are cast to $\mathbb R$ . Restricting to integer starting times would be a different problem and is not what is stated.
Nonnegative starting times are a standing assumption. The paper uses them ("scheduled between 0 and $M-l_0/2$ ", p. 336) without writing them into the model. Nonoverlap is "one task finishes before the other starts", the reading of "intersect only at their endpoints".
Tasks are indexed by Fin N from $0$ . In the special case $T_i$ is index $i$ , and the paper's $T_{2i-1},T_{2i}$ ( $1\le i\le n$ ) are the indices $2k+1,2k+2$ for $k=i-1$ .
Languages use the published CookPvsNP_defs (Cook's one-tape Turing machines, NP, NPComplete) and the published ProjSchedTW.Complexity.Encoding (four-letter alphabet and binary codes). This mission defines positivePartitionLang by restricting the imported equal-sum predicate to nonempty lists of positive integers, as on p. 333. Only codes of well-formed instances belong to the even-odd and total discrepancy languages.
The goal is not the combinatorial equivalence of milestone 4. It states NP-completeness, so it contains the polynomial-time computation of the reduction and membership in NP. Taking NPComplete evenOddLang as the hypothesis instead would drop LEMMA 1 and is not what is asked.
Running times of the algorithms of §2.2–§2.4 are out of scope for this mission, as are all results after §2.1.

Contributions welcome: proofs of any milestone, and reusable lemmas on Turing-machine computability of arithmetic on binary codes, which the two membership results and both reductions need.

Selected references

M. R. Garey, R. E. Tarjan, G. T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2):330–348, 1988. https://doi.org/10.1287/moor.13.2.330
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
J. J. Kanet, Minimizing the average deviation of job completion times about a common due date, Naval Research Logistics Quarterly 28(4):643–651, 1981. https://doi.org/10.1002/nav.3800280411
N. G. Hall, W. Kubiak, S. P. Sethi, Earliness–tardiness scheduling problems, II: Deviation of completion times about a restrictive common due date, Operations Research 39(5):847–856, 1991. https://doi.org/10.1287/opre.39.5.847
S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problems, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

19 thms3 active usersReviewed

Completed

Graph Theory Operations Research·Captain: mikedeng1

Matching, Euler Tours and the Chinese Postman IV: Every Connected, Even, Symmetric Mixed Graph Has an Euler TourResearch Paper

Motivation

A postman, a snowplough or a street sweeper must traverse every street of a district and return to the depot. When some streets are one-way, the street network is a mixed graph: some edges are directed and must be traversed in a prescribed direction, the others are undirected and may be traversed either way. The first question about such a route is whether a closed route exists that traverses every street exactly once, an Euler tour of the mixed graph. When one exists, it is an optimal postman route; when none exists, the postman problem asks which streets to repeat.

J. Edmonds and E.L. Johnson treat this question in §6 of Matching, Euler tours and the Chinese postman (Mathematical Programming 5, 1973), the paper that solved the undirected Chinese postman problem by matching. Section 6 gives an algorithm that finds an Euler tour in any mixed graph that is connected, of even degree and symmetric, and §7 uses it for the mixed postman problem.

Timeline.

1736: Euler's condition for undirected graphs (even degrees, connectivity).
1951: T. van Aardenne-Ehrenfest and N.G. de Bruijn enumerate the Euler tours of a symmetric directed graph through spanning arborescences ("circuits and trees in oriented linear graphs"). Edmonds and Johnson cite this as the source of their arborescence rule.
1962: L.R. Ford and D.R. Fulkerson (Flows in Networks, §II.7) characterize, by a flow argument, when a mixed graph has an Euler tour without assuming symmetry.
1973: Edmonds and Johnson give the combined orientation and Rule algorithm of §6 for connected, even, symmetric mixed graphs, and the existence criterion of §7 for mixed postman tours.
1976: C.H. Papadimitriou shows the mixed postman problem NP-hard, so the polynomial-time picture of §6 does not extend to its optimization version.

Setting

A mixed graph $G$ has a finite set $N$ of nodes and a finite set $E$ of edges. Each edge $e$ meets two distinct nodes; several edges may meet the same pair of nodes. Some edges are directed: an edge directed away from node $i$ toward node $j$ must be traversed from $i$ to $j$ . In Lean an edge has a tail, a head (distinct) and a Boolean directed; for an undirected edge the order of the two ends carries no meaning.

The degree of a node is the total number of edges, regardless of direction, meeting it. $G$ is even if every degree is even.
$\operatorname{out}(n)$ and $\operatorname{in}(n)$ count the directed edges directed away from and toward $n$ . $G$ is symmetric if $\operatorname{out}(n)=\operatorname{in}(n)$ for every node $n$ .
$G$ is connected if it is connected when the directions on the edges are ignored.
A mixed walk is a sequence $(n_1,e_1,n_2,\dots,e_l,n_{l+1})$ in which each directed $e_i$ goes from its tail $n_i$ to its head $n_{i+1}$ and each undirected $e_i$ meets $n_i$ and $n_{i+1}$ . It is a tour if $n_{l+1}=n_1$ , an Euler tour if it contains every edge exactly once, and a postman tour if it contains every edge at least once.
An arborescence with root $r$ is a tree $T$ of directed edges in which every node $n\neq r$ of $T$ has precisely one edge of $T$ directed away from $n$ . Following those edges from any node of $T$ leads to $r$ . It is spanning if it contains every node.

Formalization targets

Goal: the mixed Euler tour theorem (§6, pp. 115–118)

If $G$ is connected, even and symmetric, then for every node $r$

\exists\ (r=n_1,e_1,\dots,e_l,n_{l+1}=r)\ \text{a mixed Euler tour of } G .

Milestones

Cut balance (p. 116). If $G$ is symmetric, every node set $S$ has as many directed edges leaving it as entering it.
Maximal arborescences span (pp. 115–116). Suppose the directed edges form a symmetric, connected spanning subgraph. Then an arborescence of directed edges to which no directed edge entering it from outside can be added contains every node.
The Rule (pp. 116–117). Suppose the directed edges form a symmetric connected spanning subgraph and the undirected edges have even degree. Fix a spanning arborescence with root $r$ and order the directed edges leaving each node $n\neq r$ so that the arborescence edge comes last. Then the following traversal from $r$ is an Euler tour: leave by the next unused undirected edge if there is one, otherwise by the next unused directed edge.
The assignment outcome (p. 118). If $G$ is connected, even and symmetric, directions can be assigned to some undirected edges so that the result is symmetric, its directed edges form a connected spanning subgraph, and the unassigned edges have even degree.
Mixed postman criterion (§7, p. 120). A connected mixed graph has a postman tour if and only if no nonempty proper node set $S$ has every boundary edge directed away from $S$ .

Significance

The goal contains two classical theorems as special cases. With every edge undirected it is Euler's theorem for connected even multigraphs. With every edge directed it is the theorem that a connected balanced digraph is Eulerian. The milestones connect the two cases: an orientation reduces the mixed case to one the Rule can handle. The Rule itself is the van Aardenne-Ehrenfest–de Bruijn construction, which underlies the BEST theorem counting Euler tours. Milestone 5 decides whether the mixed postman problem has any feasible solution. The mixed postman problem is the standard model for routing on one-way street networks.

All results here are proved in the paper, so none is open. No Lean proof of any of them in this form is known. Mathlib's Eulerian walks are for simple graphs; it has no multigraph or mixed-graph Euler theorem, no directed Euler theorem and no arborescence-based traversal. The mission produces these, together with a reusable vocabulary of mixed multigraphs, walks that respect directions, and arborescences given by parent edges.

Difficulty

The obvious approach to the goal is to forget the directions and apply Euler's theorem. This fails because the tour it produces may traverse a directed edge backwards. Orienting all undirected edges at once also fails: an arbitrary orientation of the undirected edges need not keep every node balanced.

The difficult part of the Rule is showing that the greedy traversal does not get stuck before using every edge. It cannot stop at a node other than $r$ because of the degree conditions. The hard step is showing that no edge is left unused when it stops at $r$ . The answer depends on the ordering condition: without the arborescence edge last at every node, the Rule can return to $r$ with edges still unused. The assignment step needs an invariant: the orientation must keep every node symmetric while it extends a spanning structure of directed edges.

Formalization scope

Graphs. Nodes and edges are finite types (Fintype V, Fintype E). Parallel edges are allowed, including a directed and an undirected edge on the same pair. Loops are excluded (tail e ≠ head e), following the paper's standing setting of §2 (p. 91: edges meet two different nodes). Edges are a type, not a relation on nodes, so parallel edges stay distinct in every walk.
Hypotheses as on p. 115. "Even" counts all edges, directed or undirected. "Symmetric" counts only directed edges. "Connected" ignores directions. Strong connectivity is not assumed. "Symmetric" does not mean that every node has even in-degree, and an Euler tour of the underlying undirected multigraph does not satisfy the goal: the tour must traverse each directed edge from its tail to its head.
Walks are a node list and an edge list of length one less. The one-node walk is allowed, so the graph with one node and no edges satisfies the goal.
Arborescences are given by an optional edge $a_n$ at each node, with an edge required for each non-root node of $W$ ; following those edges leads to $r$ . A maximal arborescence is one where no directed edge enters $W$ from outside. The optional choice represents the root-only arborescence when the graph has no edges.
The Rule is computed by a fuel-bounded traversal (at most $|E|$ steps) that keeps a global list of used edges. Its conclusion is that the computed sequences form a mixed Euler tour from $r$ .
The assignment is an existential statement over a second mixed graph $G'$ on the same edges, with the same unordered ends and every directed edge kept. The paper's algorithm (Steps 0–3) is not formalized.
Postman criterion. "Proper subset" means nonempty and proper. Connectivity is assumed, as throughout §7, and the node set is nonempty (with no nodes there is no tour, while the criterion holds vacuously).
Not formalized. The §7 evenness argument (p. 122) and the min-cost flow formulations are outside the scope.

Contributions are welcome at every level: proofs of the milestones, a direct proof of the goal, and general lemmas about mixed multigraph walks.

Selected references

J. Edmonds and E.L. Johnson, Matching, Euler tours and the Chinese postman, Mathematical Programming 5 (1973) 88–124. https://doi.org/10.1007/BF01580113
T. van Aardenne-Ehrenfest and N.G. de Bruijn, Circuits and trees in oriented linear graphs, Simon Stevin 28 (1951) 203–217.
L.R. Ford and D.R. Fulkerson, Flows in Networks, Princeton University Press, 1962.
C.H. Papadimitriou, On the complexity of edge traversing, Journal of the ACM 23 (1976) 544–554. https://doi.org/10.1145/321958.321974

7 thms3 active usersReviewed

Missions

3SUM in O(n^1.999074) Time on a Word RAMOpen Problem

Concentration of Measure and Isoperimetric Inequalities in Product Spaces XI: The Random Assignment Problem — Fluctuations of the Optimal Cost of Order (log N)²/(√N log log N)Textbook

Motivation

Setting

Formalization targets

Goal: Theorem 10.5

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Concentration of Measure and Isoperimetric Inequalities in Product Spaces VIII: The Longest Increasing Subsequence — Gaussian Concentration of L_N around Its Median MTextbook

Why the longest increasing subsequence

Setting

Formalization targets

Goal: Theorem 7.1.2 (p. 153)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Concentration of Measure and Isoperimetric Inequalities in Product Spaces II: The Two-Point Space — an N-Free Exponential Bound for the One-Sided Hamming Distance under a Second MeasureTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 2.3.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

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

Motivation

Setting

Formalization targets

Exact cycle period

Supporting results

Significance

Difficulty

Formalization scope

Selected references

Approximation Algorithms for Scheduling Unrelated Parallel Machines 2: Enumerating Long Assignments and Rounding the LP Gives a (1 + ε)-Approximation for MakespanResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3

Milestones (§3, p. 6)

Significance

Difficulty

Formalization scope

Selected references

The Four-Colour Theorem: Birkhoff's Lemma (6.4) — Every Non-Empty Consistent Set of Edge-Colourings of a Ring of Length 5 Meeting ℰ Includes One of 𝒞ᵢ, 𝒟ᵢ, ℰResearch Paper

Motivation

Setting

Formalization targets

Goal: Birkhoff's lemma for rings of length 5, (6.4)

Milestones

Companion: Birkhoff's lemma for rings of length 4, (6.3)

Significance

Difficulty

Formalization scope

Selected references

Application of the Branch and Bound Technique to Some Flow-Shop Scheduling Problems 3: Shifting and Scaling the Processing Times Changes Neither the Optimal Sequence nor the Branch-and-Bound PathResearch Paper

Motivation

Setting

Formalization targets

Goal: the Appendix THEOREM (p. 411)

Milestones, in the order of the paper's proof

Significance

Difficulty

Formalization scope

Selected references

Sequencing a One State-Variable Machine: A Solvable Case of the Traveling Salesman Problem 2: For g = 0 ≤ f, the Tour ψ′ Minimizes the Largest Changeover CostResearch Paper

Motivation

Setting

Formalization targets

Goal: ψ′\psi'ψ′ solves the bottleneck traveling salesman problem

Milestones

Goal: $\psi'$ solves the bottleneck traveling salesman problem