Combinatorics

Why this question matters

In a strategic game, each player evaluates a change in their own strategy using that player's own payoff. These incentives need not point in a common direction. A potential game is a case in which one real-valued function records every player's payoff change under a unilateral deviation. This common function lets questions about incentives be expressed as questions about one object on the space of strategy profiles. Monderer and Shapley's 1996 paper introduced several kinds of potential and gave a local characterization of the exact kind. The characterization is the subject of this mission.

The local test matters because the defining condition appears to require finding an unknown potential on the entire profile space. Theorem 2.8 says that a condition on four-step cycles already determines whether such a function exists, even when individual strategy sets are infinite. The paper compares this characterization with the familiar idea that a conservative field has zero integral around closed curves; here the “integral” is a finite sum of payoff changes along unilateral deviations (Monderer and Shapley, pp. 130–131).

Games, deviations, and path sums

Let $N$ be a finite set of players. For each player $i\in N$, let $Y^i$ be a strategy set, and let $Y=\prod_{i\in N}Y^i$ be the set of pure strategy profiles. The payoff of player $i$ is a function $u^i:Y\to\mathbb R$. If $y\in Y$, the notation $(y^{-i},x)$ means the profile obtained by replacing only player $i$'s strategy with $x\in Y^i$. The strategy sets themselves are not required to be finite in this section of the paper (p. 127).

An exact potential is a function $P:Y\to\mathbb R$ such that, for every $i$, every opponents' profile $y^{-i}$, and every $x,z\in Y^i$,

$$u^i(y^{-i},x)-u^i(y^{-i},z) =P(y^{-i},x)-P(y^{-i},z).$$

A game admitting such a function is an exact potential game. The paper uses the shorter term “potential game” for this class when the adjective is clear (pp. 127–128, equation (2.2)).

A path $\gamma=(y_0,\ldots,y_L)$ is a sequence in which each step changes exactly one player's strategy to a different value. Write $i_k$ for the unique player who moves from $y_{k-1}$ to $y_k$. The path sum of the payoff vector $u$ is

$$I(\gamma,u)=\sum_{k=1}^{L} \bigl(u^{i_k}(y_k)-u^{i_k}(y_{k-1})\bigr).$$

The path is closed when $y_0=y_L$. It is simple closed when, in addition, the vertices $y_0,\ldots,y_{L-1}$ are pairwise distinct. Its length is $L$, the number of steps and the number of vertices before the final return. These definitions follow pp. 128, 130–131.

Formalization targets

Theorem 2.8: four equivalent conditions

For a game with finitely many players, Theorem 2.8 asserts the equivalence of all four claims:

$$\begin{aligned} &\Gamma\text{ has an exact potential};\\ &I(\gamma,u)=0\quad\text{for every finite closed path }\gamma;\\ &I(\gamma,u)=0\quad\text{for every finite simple closed path }\gamma;\\ &I(\gamma,u)=0\quad\text{for every simple closed path }\gamma\text{ of length }4. \end{aligned}$$

The last condition is a local criterion, but the goal keeps the full four-way equivalence of the published theorem, p. 131. The milestone list follows five claims in its Appendix A proof: vanishing path sums from a potential, path independence, construction of a potential from vanishing closed-path sums, the local exchange of two different players' moves, and the reduction from all closed paths to length-four simple cycles (pp. 138–139).

Related results in the same development

Corollary 2.9 expresses the length-four test directly as a zero sum of payoff changes around four corners obtained by varying two players' strategies. Lemma 2.7 says that two exact potentials for the same game differ by one additive constant. Both are included as supporting statements from the same definition layer, although they are not milestones in the attack path for Theorem 2.8 (pp. 130–131).

What the result provides

Theorem 2.8 turns existence of a global function into a test on local cycles. Corollary 2.9 makes those cycles visible in payoff tables: fixing all but two players, the alternating sum around each two-player rectangle must vanish. For finite strategy sets this gives a direct finite collection of conditions; for infinite strategy sets the theorem remains a mathematical characterization without claiming a finite algorithm (Monderer and Shapley, p. 131).

The original paper proves these statements. The formalization work is to represent games, paths, path sums, and the four-way equivalence in Lean, then supply machine-checked proofs. The present mission contains compiled statements with open proofs. Its definition modules are also reusable for the paper's other results about potentials, improvement paths, and congestion games.

Where the proof is difficult

The challenging direction is that zero sums on simple length-four cycles force zero sums on every closed path. A closed path may repeat vertices and may involve more than two players. A direct appeal to the local condition does not cover such a path. The Appendix A argument uses changes to a path's sequence of deviators, and its informal treatment of adjacent moves by the same player leaves a boundary case: the two moves can cancel, so replacing them by one move would create a null step, which the definition of a path excludes. A formal proof must account for this case while preserving the paper's exact statement (pp. 138–139).

Formalization scope

Lean represents the finite player set by a finite type $\iota$ and a profile by a dependent function $y:\prod_{i:\iota}Y^i$. Strategy sets $Y^i$ remain arbitrary types. The operation $(y^{-i},x)$ is a one-coordinate update. A finite path stores $L+1$ vertices and its deviator at each of the $L$ steps; the step condition determines that deviator uniquely. Closed paths of length zero are allowed and have sum zero. The paper prints $n$, the number of players, as the upper limit of the path sum on p. 130, although its summands are indexed by path steps. The Lean definition sums over all $L$ steps, as the surrounding definition and later equations require.

The four-cycle hypothesis quantifies only over simple closed paths of exactly four genuine steps. It is not replaced by all four-step walks or by cycles with null or simultaneous deviations. The goal retains all four clauses rather than only its shortest equivalence. Corollary 2.9 explicitly requires the two varying players to be distinct; this is implicit in the paper's four-corner construction. No finite-strategy assumption is imposed on Theorem 2.8, Corollary 2.9, or Lemma 2.7.

The development needs ordinary finite sums, dependent functions, coordinate updates, and finite-indexed paths. Its path and potential definitions are intended as an interface for later work. Contributions proving any of the five source-backed milestones, the goal, or the two related statements are within scope.

Selected references

• Dov Monderer and Lloyd S. Shapley, Potential Games, Games and Economic Behavior 14 (1996), 124–143. DOI: 10.1006/game.1996.0044.

Motivation

A job shop is the basic model of a factory floor in which every job follows its own route through the machines. Minimizing the time at which the last job is finished (the finish time, or makespan) is one of the central problems of deterministic scheduling theory, and the question of which special cases admit efficient algorithms has organized much of the field since the 1950s.

For two machines the picture is sharp. Jackson (1956) showed that a two-machine job shop in which every job has at most two operations is solved by a simple rule extending Johnson's flow-shop algorithm (Jackson, Naval Research Logistics Quarterly 3, 1956; Conway, Maxwell and Miller, Theory of Scheduling, 1967, p. 105). Once a single job may have three operations, the non-preemptive problem becomes NP-complete: Lenstra, Rinnooy Kan and Brucker showed this for $n-1$ jobs with one nonzero task each and one job with three (Annals of Discrete Mathematics 1, 1977; a 1975 Mathematisch Centrum report is the paper's reference [1]). Gonzalez and Sahni (Operations Research 26(1), 1978) extended this boundary to preemptive schedules, in which a task may be interrupted and resumed later: even then the two-machine problem is NP-complete, already when only two jobs have three nonzero tasks. This mission formalizes that reduction, Lemma 5 together with Corollary 2 of their paper.

Timeline:

• 1956: Jackson, two-machine job shop with at most two operations per job, solved in $O(n\log n)$.
• 1975/1977: Lenstra, Rinnooy Kan and Brucker, the non-preemptive two-machine job shop NP-complete with $n-1$ one-task jobs and one three-task job.
• 1976: Garey, Johnson and Sethi, the non-preemptive two-machine job shop NP-complete even when problem size is measured by the sum of the task lengths (Mathematics of Operations Research 1, 1976).
• 1978: Gonzalez and Sahni, the preemptive two-machine job shop NP-complete (Lemmas 5 and 6), and the non-preemptive case again by the same reduction (Corollary 2).

Setting

A job shop has processors $P_1, \dots, P_m$ and jobs $1, \dots, n$. Job $i$ is a finite sequence of tasks; task $j$ of job $i$ must be processed on a given processor $k$ for $t_{k,i,j} \ge 0$ time units, and for every job, task $j \ge 2$ can begin only after task $j-1$ has been completed. Schedules start at time $0$. A preemptive schedule assigns to every task a finite set of time intervals $[s, f)$ on its processor, of total length $t_{k,i,j}$, such that intervals on the same processor do not overlap and every interval of task $j$ begins after task $j-1$ of the same job is completed. A non-preemptive schedule processes each task in a single interval. If $f_i(S)$ is the time at which job $i$ is completed, the finish time is $\mathrm{FT}(S) = \max_i f_i(S)$.

PARTITION: a multiset $\{a_1, \dots, a_n\}$ of nonnegative integers has a partition if some index set $u$ satisfies $\sum_{i \in u} a_i = \tfrac12 \sum_{i=1}^n a_i$.

From $a_1, \dots, a_n$, with $T = \sum_i a_i$, the paper builds the two-processor job shop $\mathrm{JS}$ with $n+2$ jobs:

• job $i \le n$: tasks $(P_2, a_i)$, $(P_1, a_i)$;
• job $n+1$: tasks $(P_1, T/2)$, $(P_2, T/2)$, $(P_1, 3T)$;
• job $n+2$: tasks $(P_2, 3T)$, $(P_1, T/2)$, $(P_2, T/2)$.

Each processor carries load exactly $5T$. In Lean, the instance is JS a : JobShopLTAS.Core.Instance 2 (n + 2), a schedule is S : Schedule (JS a) (a finite set of pieces), and the predicates are S.IsPreemptive, S.IsNonPreemptive and S.FinishedBy (5 * T a).

Formalization targets

Goal: Lemma 5 and Corollary 2

For every $n$ and every $a : \mathrm{Fin}\,n \to \mathbb N$,

$$\bigl(\exists\, S \text{ preemptive},\ \mathrm{FT}(S) \le 5T\bigr) \iff \mathrm{Partition}(a) \quad\text{and}\quad \bigl(\exists\, S \text{ non-preemptive},\ \mathrm{FT}(S) \le 5T\bigr) \iff \mathrm{Partition}(a).$$

Milestones

1. Lemma 5(a): a partition yields a non-preemptive schedule of finish time exactly $5T$ (the paper's Figure 3).
2. Observations (i)–(ii) in the proof of Lemma 5(b): in any preemptive schedule with $\mathrm{FT} \le 5T$, task $t_{2,n+1,2}$ is completed by $2T$ and $t_{2,n+2,1}$ by $4T$; no part of $t_{1,n+1,3}$ runs before $T$ and no part of $t_{1,n+2,2}$ before $3T$.
3. Lemma 5(b): without a partition, every preemptive schedule has $\mathrm{FT} > 5T$.
4. Lemma 5: the preemptive equivalence.
5. Corollary 2: the non-preemptive equivalence.

Significance

The result places the boundary of tractability for two-machine job shops exactly: at most two operations per job is solvable in $O(n\log n)$, while two jobs with three operations make the problem NP-complete, and allowing preemption does not help. The same instance serves both schedule types, because its optimum is $5T$ in either model exactly when a partition exists.

The theorem is classical and fully proved on paper; no machine-checked proof is known to exist. Formalizing it requires a precise model of preemptive schedules, which the paper treats informally, and makes explicit an argument (the "no idle time" step of Lemma 5(b)) that the paper compresses into a few sentences. The schedule model built here is shared with the other job-shop missions of this series.

Difficulty

Direction (a) is a concrete schedule and is bookkeeping. Direction (b) is the substance. The tempting argument "each processor has load $5T$, so a schedule of finish time $5T$ has no idle time, hence some set of short jobs fills exactly $[0, T/2]$ on $P_2$" is incomplete for preemptive schedules: the short jobs may be split into many pieces spread over the whole horizon, and $U$, the set of short jobs that touch $P_1$ during $[0, T]$, is defined by pieces rather than by whole tasks. Making the counting argument rigorous requires measuring idle time on each processor across arbitrary finite unions of intervals and tying the amount of processing done on $P_1$ before $T$ to the completed first tasks on $P_2$.

Formalization scope

• Processing times are real numbers; the PARTITION data are natural numbers cast to $\mathbb R$; $T$ is the real sum. Processors are Fin 2 with $P_1 = 0$, $P_2 = 1$; jobs and tasks are 0-based, so the paper's job $n+1$ is job n and job $n+2$ is job n + 1.
• Job-shop data reuse the published JobShopLTAS.Core.Instance. Schedules are finite sets of pieces (task, start, end) with positive length, following the paper's footnote 1 (p. 40). A task of length zero has no pieces and is completed when its predecessor is; it never blocks a processor.
• A non-preemptive schedule is a preemptive one with at most one piece per task. "Finish time $\le \tau$" is ∀ j, S.jobFinish j ≤ τ; "finish time $> 5T$" is the existence of a job finishing after $5T$; "finish time $5T$" in Lemma 5(a) is $\le 5T$ together with a job finishing at exactly $5T$.
• Complexity wording not formalized. "Partition $\alpha$ preemptive JOFT" and "Partition $\alpha$ nonpreemptive JOFT" (polynomial reducibility), "NP-complete", and Lemma 6 ("JOFT is in NP") are not stated. What is stated is the equivalence that the paper's proofs establish for the instance they construct, with the explicit constant $\tau = 5T$.
• The PARTITION condition is written $2\sum_{i\in u} a_i = \sum_i a_i$ in $\mathbb N$, avoiding truncated division.
• A trivializing formalization is ruled out: the schedule notion requires every task to receive its full processing time, so the empty schedule is feasible only when $T = 0$ (and then the empty index set is a partition), and the finish-time bound is over every job, so no statement holds by an unattained supremum or a default value.
• Welcome contributions: a proof of Lemma 5(a) by an explicit piece schedule; infrastructure for measuring busy and idle time of a processor in a finite piece schedule, reusable for Lemma 7 (mission 4) and the preemptive flow-shop missions; the proof of Lemma 5(b).

Selected references

• T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
• J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• M. R. Garey, D. S. Johnson, R. Sethi, Complexity of Flow Shop and Job Shop Scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117
• J. R. Jackson, An Extension of Johnson's Results on Job Lot Scheduling, Naval Research Logistics Quarterly 3(3), 201–203, 1956. https://doi.org/10.1002/nav.3800030307
• R. W. Conway, W. L. Maxwell, L. W. Miller, Theory of Scheduling, Addison-Wesley, 1967.

Motivation

A multicommodity flow problem asks to route many source–sink demands through one capacitated network at the same time. Its min-cut (sparsest cut) is the smallest ratio, over all cuts, of the capacity crossing the cut to the demand separated by it. Routing is always limited by every cut, so the max-flow never exceeds the min-cut. For a single commodity the two are equal (Ford–Fulkerson); for many commodities they are not, and the size of the gap governs a large family of approximation algorithms for graph partitioning, layout and routing problems.

Leighton and Rao (J. ACM 46 (1999), extended abstract FOCS 1988) proved that for uniform problems, where every pair of nodes demands one unit, the gap is at most $O(\log n)$ (their Theorem 2). This mission formalizes the other half: Section 2.1 of the paper, A bad example, which shows that the $\log n$ is necessary. On a 3-regular expander graph the max-flow is a $\Theta(\log n)$ factor smaller than the min-cut, so Theorem 2 cannot be improved beyond the constant.

Timeline. Ford and Fulkerson (1956) and Elias–Feinstein–Shannon (1956): single-commodity max-flow equals min-cut. Hu (1963): equality for two commodities. Leighton and Rao (1988, journal 1999): uniform and product problems have an $O(\log n)$ gap, and expanders show it is tight. Klein, Agrawal, Ravi and Rao (1990) and later Linial–London–Rabinovich (Combinatorica 1995) and Aumann–Rabani (1998): an $O(\log k)$ gap for general demands with $k$ commodities, tight by the same expander example.

Setting

Let $V$ be a finite set of $n$ nodes. A network assigns a capacity $C(u,v)\ge0$ to every pair, symmetric and zero on the diagonal. For $U\subseteq V$ with complement $\bar U$, the cut capacity $C(U,\bar U)$ is the total capacity of the pairs with one end in $U$ and the other in $\bar U$.

In the uniform multicommodity flow problem (UMFP) every pair of distinct nodes is a commodity with unit demand. Its max-flow $f$ is the largest fraction such that $f$ units of every commodity can be routed simultaneously without exceeding any capacity (concurrent flow). Its min-cut is

$$\mathcal S=\min_{\emptyset\ne U\subsetneq V}\frac{C(U,\bar U)}{|U|\,|\bar U|}.$$

Section 2.1 takes a 3-regular $n$-node graph $G$ with unit edge capacities, so that $C(U,\bar U)=|\langle U,\bar U\rangle|$ is the number of edges between $U$ and $\bar U$, and assumes that $G$ is a $c$-edge-expander:

$$|\langle U,\bar U\rangle|\ \ge\ c\,\min\{|U|,|\bar U|\}\qquad\text{for all }U\subseteq V,$$

for a constant $c>0$. Families of such graphs exist for a sufficiently small $c$ (Margulis 1973; a random 3-regular graph has the property with high probability). Throughout, $\log$ is $\log_2$.

Formalization targets

Goal: the gap on an expander

For a 3-regular $c$-edge-expander with unit capacities and $n\ge 8$,

$$f\ \le\ \frac{6\,\mathcal S}{c\,\bigl(\lfloor\log n\rfloor-2\bigr)} .$$

This is the final display of §2.1 (pp. 794–795), with the floor that the argument actually supports (see Formalization scope). It leaves the expander family unspecified: it holds for every graph with the two properties.

Milestones, in the order the argument uses them

1. $\mathcal S\ge c/(n-1)$ for the expander (p. 794).
2. In a 3-regular graph, at most $n/2$ nodes lie within distance $\lfloor\log n\rfloor-3$ of any node.
3. Hence at least half of the source–sink pairs are at distance at least $\lfloor\log n\rfloor-2$.
4. A uniform flow of fraction $f$ uses capacity at least $\tfrac12\binom n2 f(\lfloor\log n\rfloor-2)$, and the total capacity is $3n/2$.
5. Hence $f\le 3n/\bigl(\binom n2(\lfloor\log n\rfloor-2)\bigr)=6/\bigl((n-1)(\lfloor\log n\rfloor-2)\bigr)$.

Companions: Theorem 1

Theorem 1 (p. 795) states that for any $n$ there is an $n$-node UMFP with $f\le O(\mathcal S/\log n)$. It is stated twice: conditionally on a family of 3-regular $c$-expanders (the form §2.1 proves), and unconditionally, with one constant $K$ for all $n\ge2$.

Significance

The result shows that the $O(\log n)$ max-flow min-cut gap of Leighton and Rao's Theorem 2 is tight up to the constant, and, through the same example, that the $O(\log k)$ bound for general demands is tight. Every approximation algorithm that rounds a multicommodity flow, or its dual, to a cut loses a $\Theta(\log n)$ factor in the worst case for this reason; improving on it, as Arora, Rao and Vazirani did (J. ACM 2009) with an $O(\sqrt{\log n})$ approximation for sparsest cut, requires a stronger relaxation than the flow LP.

The result is classical and proved. To our knowledge it has no machine-checked proof. Formalizing it requires the concurrent-flow LP, the uniform sparsest cut, graph distance balls in bounded-degree graphs and a counting argument that converts path lengths into capacity usage; each of these is reusable. The unconditional Theorem 1 additionally needs the existence of bounded-degree expanders on every number of nodes, which is a substantial formalization project in its own right.

Difficulty

The min-cut bound and the ball bound are elementary. The central step is milestone 4: turning "the shortest path of a commodity has at least $\ell$ edges" into "the commodity uses at least $f\ell$ units of capacity". In an arc-flow formulation a commodity is a conservation-respecting function on arcs, not a set of paths, so the step needs either a path decomposition of each commodity's flow or a weak-duality argument with unit edge lengths. The obvious attempt, summing the conservation equations directly, gives only the net flow across one cut and loses the factor $\ell$.

The unconditional Theorem 1 is hard for a different reason: the paper cites the existence of 3-regular expanders and does not prove it, and the theorem asks for every $n$, including odd $n$, where no 3-regular graph exists.

Formalization scope

Nodes are a Fintype $V$ with decidable equality and $n=|V|$. A network is a symmetric nonnegative real capacity function with zero diagonal; the unit-capacity network of a simple graph $G$ has $C(u,v)=1$ on edges and $0$ elsewhere. Commodities are ordered pairs $(s,t)$, $s\ne t$, each with demand $\tfrac12$ (the paper's footnote 2), so each unordered pair carries one unit; a flow is a nonnegative arc flow per commodity, and both directions of an edge share its capacity. The max-flow is the supremum of feasible fractions. The min-cut ranges over nonempty proper $U$ only: at $U=\emptyset$ or $V$ the ratio is $0/0$, which Lean reads as $0$ and which would make $\mathcal S=0$.

Conventions and added hypotheses:

• The floor. The page writes $\log n-2$. Its argument shows that far pairs have distance at least $\lfloor\log n\rfloor-2$, which differs from $\log n-2$ for non-integer $\log n$. The goal and milestones state $\lfloor\log n\rfloor-2$ (Nat.log 2 n), a different constant in the same $\Theta(\log n)$.
• $n\ge 8$ makes $\lfloor\log n\rfloor-2\ge1$, so the bound divides by a positive number.
• Graph distance is the extended distance, $\infty$ between components, never Lean's junk value $0$.
• Regularity is SimpleGraph.IsRegularOfDegree 3.
• Theorem 1 requires the network to be connected (the paper's standing assumption, p. 789); a disconnected network has $f=\mathcal S=0$ and would make the statement empty. Its constant is quantified before $n$.
• Polynomial-time claims are not formalized.

The hypotheses of the goal are satisfiable: the 3-cube $Q_3$ ($n=8$) is 3-regular and a $1$-edge-expander. Contributions welcome: the arc-flow path-length lemma, the ball bound for bounded-degree graphs, and an existence theorem for 3-regular expanders.

Selected references

• T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46(6):787–832, 1999. https://doi.org/10.1145/331524.331526
• G. A. Margulis, Explicit constructions of concentrators, Problems of Information Transmission 9(4):325–332, 1973.
• N. Linial, E. London and Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2):215–245, 1995. https://doi.org/10.1007/BF01200757
• S. Arora, S. Rao and U. Vazirani, Expander flows, geometric embeddings and graph partitioning, J. ACM 56(2):5, 2009. https://doi.org/10.1145/1502793.1502794

Motivation

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Proposition 3.1

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

Milestones

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

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

Selected references

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

Motivation

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

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

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

Setting

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

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

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

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

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

Formalization targets

Goal: the construction computes the power sum

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

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

Milestone 1 (Proved, referenced): the THEOREM

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

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

Milestone 2: footnote 2

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

Companion: footnote 3

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

The coalition payoff set is

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

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

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

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

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

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

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

Formalization targets

The goal is the paper's Section 4 theorem:

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

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

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

Setting

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

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

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

Formalization targets

Goal: Theorem 2 (p. 35)

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

Selected references

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

Motivation

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

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

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

Timeline.

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

Setting

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

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

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

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

Formalization targets

Goal: Theorem 3' (p. 49)

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 5.1

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

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

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

Stronger: Proposition 5.2

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

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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