Combinatorics

Why bi-Cayley graphs over abelian groups matter

A Cayley graph turns multiplication in a group into adjacency between vertices. Every Cayley graph is vertex transitive: multiplying every vertex by the same group element moves any chosen vertex to any other. A bi-Cayley graph starts with two copies of a group and permits edges both within and between the copies. Its built-in group action is transitive on each copy, but it need not exchange them. This makes bi-Cayley graphs a setting for distinguishing edge, vertex, and arc transitivity. Conder, Zhou, Feng and Zhang study these distinctions and their consequences for graph constructions in Edge-transitive bi-Cayley graphs.

For abelian groups, the paper proves a strong restriction: once a connected bi-Cayley graph is edge transitive, it is also vertex transitive. Its half-arc-transitive examples face additional local restrictions, including a minimum valency of six. The paper exhibits a graph of valency six in Example 4.3, so the numerical bound is attained in its class. The result separates these graphs from semisymmetric graphs, which are edge transitive but not vertex transitive. The claims and example appear in Proposition 1.3 and §4.

Graphs, actions, and terminology

Let $H$ be a finite group and let $R,L,S$ be subsets of $H$. Require $R=R^{-1}$, $L=L^{-1}$, $1\notin R\cup L$, and $|R|=|L|$. The graph $\Gamma=\operatorname{BiCay}(H,R,L,S)$ has vertices $H_0\cup H_1$, two labelled copies of $H$. For $h\in H$, an element $x\in R$ gives an edge from $h_0$ to $(xh)_0$; an element $y\in L$ gives an edge from $h_1$ to $(yh)_1$; and an element $z\in S$ gives an edge from $h_0$ to $(zh)_1$. The inverse closure of $R$ and $L$ makes the within-copy edges undirected. Excluding $1$ from those two sets excludes loops. This is the construction on p. 1.

Every $g\in H$ acts by right multiplication $R(g):h_i\mapsto(hg)_i$. The subgroup $R(H)$ of graph automorphisms has two vertex orbits, $H_0$ and $H_1$. Its normaliser in $\operatorname{Aut}(\Gamma)$ is useful for describing further symmetries. For a group automorphism $\alpha$ and group elements $g,x,y$, the paper defines permutations $\sigma_{\alpha,g}$, which preserve the two copies, and $\delta_{\alpha,x,y}$, which exchange them. Their precise edge-preservation conditions are the sets $F$ and $I$ of equation (2.2). The mission includes those definitions and the relevant part of the normaliser characterization, Proposition 2.2.

A graph is vertex transitive if its full automorphism group can move any vertex to any other, and edge transitive if it can move any undirected edge to any other. Arc transitivity asks the same for ordered adjacent pairs. A graph is half-arc-transitive when it is vertex and edge transitive but not arc transitive. A semisymmetric graph has constant valency, is edge transitive, and is not vertex transitive. These are the paper's definitions on p. 4. Valency means the actual number of neighbours of a vertex.

Formalization targets

The central target is the corrected reading of Proposition 1.3: for connected $\Gamma$ over an abelian $H$,

$$\Gamma\text{ edge transitive}\implies\Gamma\text{ vertex transitive},$$

and, if $\Gamma$ is half-arc-transitive,

$$R\cup L\ne\varnothing,\quad (\forall x\in R\cup L)\ \operatorname{ord}(x)\ne2, \quad |R|=|L|\text{ is even},\quad |S|>2,\quad \deg_{\Gamma}(v)\ge6\quad(v\in V(\Gamma)).$$

The attack path records the normaliser characterization in Proposition 2.2, both parts of Proposition 4.1, its explicit bipartition step, and Proposition 4.2. The companion Corollary 4.4 expresses the absence of connected semisymmetric examples over abelian groups.

What the result establishes

The vertex-transitivity conclusion collapses one apparent possibility in the symmetry classification: an edge-transitive bi-Cayley graph over an abelian group cannot be semisymmetric. For half-arc-transitive graphs, the theorem rules out involutions in the within-copy connection sets, forces even set sizes, and excludes valencies below six. Example 4.3 supplies an attained bound, with $H=C_{28}$ and valency six. These are concrete restrictions on any later classification or construction in this family; they follow from §4.

The mathematical results are proved in the cited paper. The mission asks for machine-checked Lean proofs of their statements and for a reusable finite bi-Cayley graph interface. The setting includes the right regular action, its normaliser, the two families of candidate automorphisms, and the transitivity predicates. The proof obligations are open in this local proposal; a successful development would make the abelian argument and its underlying graph-action lemmas available for later formalizations of bi-Cayley graphs.

The main obstacle

The right multiplication action gives only two known vertex orbits, one for each copy of $H$. Edge transitivity alone does not name an automorphism that swaps them. Inversion is an automorphism of an abelian group, but its induced copy-swapping permutation preserves graph edges directly only in the relevant bipartite case $R=L=\varnothing$. The paper must account for edge-transitive graphs whose connection sets initially allow edges inside the copies. For the valency bound, the absence of arc transitivity restricts how a vertex stabiliser can permute its neighbours; degree counting without those orbit constraints cannot yield $|S|>2$. These are the points at which a proof must use the full automorphism action rather than just the visible right regular subgroup.

Formalization scope

Lean uses the vertex type $H\sqcup H$, with Sum.inl h for $h_0$ and Sum.inr h for $h_1$. The group and graph are finite; the graph is simple and undirected by construction, and every theorem assumes it is connected. The finite sets $R,L,S$ retain the conditions $R=R^{-1}$, $L=L^{-1}$, $1\notin R\cup L$, and $|R|=|L|$. The graph's degree, rather than a separately defined cardinality formula, represents valency. “Involution” means an element of order exactly two. All graph-level transitivity predicates quantify over the full automorphism group; the normaliser appears only in the separate Proposition 2.2 milestone. The paper's exponent notation for group automorphisms is rendered as function application, while $R(g)$ remains right multiplication.

The printed first sentence of Proposition 1.3 says every connected bi-Cayley graph over an abelian group is vertex transitive. That sentence is false: the connected generalized Petersen graph $GP(7,2)$ is a bi-Cayley graph over $C_7$ and is not vertex transitive. Proposition 4.1(b), which the paper uses to establish Proposition 1.3, includes the missing edge-transitivity condition. The Lean goal states that corrected condition explicitly. It does not add an assumption to the half-arc-transitive clause, since half-arc-transitivity already entails edge transitivity. Proposition 4.2 prints two clauses labelled “(a)”; they are treated as distinct clauses while its quotation retains the printed labels.

The definition of the graph keeps $R$ and $L$ inverse closed as data; no graph constructor silently symmetrises arbitrary sets. Transitivity is taken over actual edges or arcs, and the degree bound is checked at every vertex. Contributions to the graph-action lemmas, the normaliser result, Proposition 4.1, and the vertex-stabiliser analysis behind Proposition 4.2 are all within scope. The Cayley-graph isomorphism in Proposition 2.2(b) is outside this mission's stated milestone because it is not used by the target.

Selected references

• M. Conder, J.-X. Zhou, Y.-Q. Feng, and M.-M. Zhang, Edge-transitive bi-Cayley graphs, Journal of Combinatorial Theory, Series B, 2020; arXiv:1606.04625v1; DOI:10.1016/j.jctb.2020.05.006.

Motivation

The associahedron $\mathrm{Ass}_n$ is the $n$-dimensional simple polytope whose faces correspond to the sets of pairwise non-crossing diagonals of a convex $(n+3)$-gon, ordered by reverse inclusion: its vertices are the triangulations of the polygon and its facets are the diagonals. It appears in homotopy theory (Stasheff), in the theory of cluster algebras of type $A$, and as the secondary polytope of a convex polygon. Many explicit realizations are known, and a natural question is which of them are genuinely different.

Ceballos, Santos and Ziegler (arXiv:1109.5544, Combinatorica 2014) compare realizations up to normal isomorphism: two polytopes are normally isomorphic if some linear isomorphism of the ambient spaces sends every cone of one normal fan to a cone of the other (their Definition 2.1). This notion ignores the right-hand sides of the defining inequalities and keeps only the linear structure of the facet normals, which is what the classical constructions fix.

One family of realizations is due to Hohlweg and Lange (arXiv:math/0510614, Discrete Comput. Geom. 2007): one associahedron $\mathrm{Ass}^I_n(\sigma)$ for every sign sequence $\sigma \in \{+,-\}^{n-1}$. The constant sequence gives Loday's associahedron (arXiv:math/0212126), and the alternating sequence gives, up to normal isomorphism, the Chapoton–Fomin–Zelevinsky associahedron (arXiv:math/0202004). This mission formalizes the classification of the Hohlweg–Lange family up to normal isomorphism, Theorem 4.9 of Ceballos–Santos–Ziegler.

Setting

Fix $n \ge 0$. The vertices of a convex $(n+3)$-gon are its positions $0, \dots, n+2$ in counterclockwise order. A diagonal joins two distinct non-adjacent positions; two diagonals cross when their endpoints are distinct and alternate around the boundary. The dihedral symmetries are the $2(n+3)$ maps $i \mapsto r + i$ and $i \mapsto r - i$ modulo $n+3$.

For $\sigma \in \{+,-\}^{n-1}$, the sign word $\widetilde\sigma = \{+,-,\sigma,-,+\}$ assigns signs to the labels $0, 1, \dots, n+2$. The polygon $P_{n+3}(\sigma)$ places the labels from left to right, positive ones above a horizontal line and negative ones below; going counterclockwise, it visits the negative labels in increasing order and then the positive labels in decreasing order. For a diagonal $ij$ with labels $i < j$, the set $R_{ij}(\sigma)$ consists of the labels strictly below the diagonal, and $S_{ij}(\sigma) \subseteq [n+1] = \{1,\dots,n+1\}$ is obtained from it by replacing $0$ by $i$ and $n+2$ by $j$. The facet of $\mathrm{Ass}^I_n(\sigma)$ for the diagonal $\delta$ has normal vector $e_{S_\delta(\sigma)}$, the characteristic vector of $S_\delta(\sigma)$ taken modulo $e_{[n+1]} = (1, \dots, 1)$. In coordinates this is the vector

$$v_\delta(\sigma) = \big(\mathbf 1[k \in S_\delta(\sigma)] - \mathbf 1[n+1 \in S_\delta(\sigma)]\big)_{k = 1, \dots, n} \in \mathbb R^n .$$

The normal fan of $\mathrm{Ass}^I_n(\sigma)$ is the collection of cones $\mathbb R_{\ge 0}\{v_\delta(\sigma) : \delta \in D\}$, one for each set $D$ of pairwise non-crossing diagonals. Two facets are parallel when their normals are negative multiples of each other. The reflection of $\sigma$ is $-\sigma$ (all signs flipped), and its reversal $\sigma^t$ is $\sigma$ read backwards.

Formalization targets

Goal: Theorem 4.9

For all $\sigma_1, \sigma_2 \in \{+,-\}^{n-1}$,

$$\mathrm{Ass}^I_n(\sigma_1) \text{ and } \mathrm{Ass}^I_n(\sigma_2) \text{ are normally isomorphic} \iff \sigma_2 \in \{\sigma_1, -\sigma_1, \sigma_1^t, -\sigma_1^t\}.$$

Both directions are content.

Milestones

1. Lemma 2.2. Every bijection of the diagonals that preserves crossing is induced by a dihedral symmetry; for $n \ge 2$, that symmetry is unique.
2. The fan-isomorphism step. A linear isomorphism of the two normal fans induces a crossing-preserving bijection of the diagonals that maps parallel pairs to parallel pairs.
3. Proposition 4.7. $\mathrm{Ass}^I_n(\sigma)$ has exactly $n$ pairs of parallel facets, with normals $e_{[j]}$ and $e_{\overline{[j]}}$. They are the diagonals of explicit quadrilaterals $\{i, j, j+1, k\}$.
4. The four diagonals. The diagonals crossing at least one member of every parallel pair are those joining $\{0,1\}$ to $\{n+1, n+2\}$.
5. Rigidity. A dihedral symmetry mapping the parallel pairs of $P_{n+3}(\sigma_1)$ onto those of $P_{n+3}(\sigma_2)$ forces $\sigma_2 \in \{\sigma_1, -\sigma_1, \sigma_1^t, -\sigma_1^t\}$.
6. Reflection. $\mathrm{Ass}^I_n(\sigma) \cong \mathrm{Ass}^I_n(-\sigma)$, with $\{S_\delta(-\sigma)\} = \{[n+1] \setminus S_\delta(\sigma)\}$.
7. Reversal. $\mathrm{Ass}^I_n(\sigma) \cong \mathrm{Ass}^I_n(\sigma^t)$, with $\{S_\delta(\sigma^t)\} = \{\tau(S_\delta(\sigma))\}$ for $\tau(i) = n + 2 - i$.

Significance

The theorem gives an exact count. The number of normally non-isomorphic Hohlweg–Lange associahedra equals the number of sign sequences of length $n-1$ up to reflection and reversal, which is $2^{n-3} + 2^{\lfloor (n-3)/2 \rfloor}$ for $n \ge 3$ (OEIS A005418). Together with Hohlweg–Lange's identification of the constant and alternating sequences, it shows that Loday's associahedron and the Chapoton–Fomin–Zelevinsky associahedron are not normally isomorphic for $n \ge 3$. It is one of the two classifications on which the paper's main result (Theorem 6.1, that the Hohlweg–Lange and Santos families meet only in the Chapoton–Fomin–Zelevinsky associahedron) rests.

Bergeron, Hohlweg, Lange and Thomas (Isometry classes of generalized associahedra, Sém. Lothar. Combin. 61A, 2009) classified the same family up to isometry of normal fans and obtained the same classes. As Remark 4.10 of the paper explains, that classification does not imply this one, because a normal isomorphism need not be an isometry. Combining the two gives Proposition 4.11, that normal isomorphism and isometry coincide for this family.

Theorem 4.9 is proved in the paper; no machine-checked version is known. A formalization would supply the first formal treatment of the crossing graph of polygon diagonals and its automorphisms (Lemma 2.2), of the Hohlweg–Lange normal vectors, and of linear isomorphisms of simplicial fans given by rays on diagonals.

Difficulty

The "if" direction needs two explicit linear isomorphisms. Their action on the sets $S_\delta$ is not diagonal by diagonal: $P_{n+3}(\sigma)$ and $P_{n+3}(-\sigma)$ have different boundary edges, so the matching of diagonals goes through a mirror image and through the sign swaps of Remark 4.2. One must show that this matching preserves the cone structure, not just the set of normals.

The "only if" direction cannot compare the two polygons by label, since $P_{n+3}(\sigma_1)$ and $P_{n+3}(\sigma_2)$ order their labels differently around the boundary. A linear isomorphism of fans first has to be turned into a combinatorial object. Linearity has to be used twice: it maps rays to rays and preserves cones, which yields a crossing-preserving bijection, and it preserves opposite pairs of normals. Lemma 2.2 then reduces that bijection to one of $2n+6$ dihedral symmetries. The remaining step is a case analysis showing that a symmetry preserving the parallel pairs, and the four distinguished diagonals they determine, is a reflection or reversal of $\widetilde\sigma$. Comparing the multisets of normal vectors alone is not enough: every $\sigma$ gives exactly $n$ parallel pairs with the same normals $\pm e_{[j]}$.

Formalization scope

• Polygon conventions. Polygon vertices are Fin (n + 3), diagonals are Sym2 (Fin (n + 3)), and crossing, diagonal and triangulation come from the published definition ChvatalArtGallery.FanPartition.Triangulation, used as a reference item. Signs are Bool, and $\sigma$ is a function Fin (n - 1) → Bool. Positions and labels are kept apart: hlLabel n σ p is the label at position p.
• Fan-level encoding. All statements are about normal fans, not polytopes. The normal fan of $\mathrm{Ass}^I_n(\sigma)$ is encoded as the fan of the vectors $v_\delta(\sigma)$, with one cone per set of pairwise non-crossing diagonals. That this is its normal fan is Hohlweg–Lange's theorem (Proposition 4.3 of the paper, [17, Prop. 1.3]), assumed by the encoding and not proved. The projection modulo $e_{[n+1]}$ is $x \mapsto (x_k - x_{n+1})_{k \le n}$; linear-isomorphism classes do not depend on this choice.
• Normal isomorphism. This is Definition 2.1 read literally: a LinearEquiv that sends every cone of the first fan to a cone of the second.
• Corrected statements. Three printed slips are corrected:
  • In the four-diagonal claim, only those of the four label pairs that are diagonals count. For constant $\sigma$ one of them is a polygon edge.
  • The complement in milestone 6 is taken in $[n+1]$, where the page prints $[n]$.
  • The reversal in milestone 7 is $\tau(i) = n+2-i$, where the page prints $n+1-i$.
• Dimension threshold. Lemma 2.2 applies $n \ge 2$ only to uniqueness, exactly as the page does; existence holds also for $n=0,1$.
• Ruled-out trivializations. The isomorphism must be linear, since a homeomorphism or a bijection of cones would identify every pair. Cones are nonnegative spans of the actual vectors $v_\delta(\sigma)$, not index sets. Symmetries of the polygon are the $2(n+3)$ dihedral maps, not arbitrary permutations of the vertices.
• What to build. Lemma 2.2 and the fan-isomorphism step are reusable for every classification of associahedra by normal fans, including the Santos family in the companion missions. Contributions to Lemma 2.2 and to the simplicial-fan step are particularly welcome.

Selected references

• C. Ceballos, F. Santos, G. M. Ziegler, Many non-equivalent realizations of the associahedron, Combinatorica 34 (2014); arXiv:1109.5544v2. https://arxiv.org/abs/1109.5544
• C. Hohlweg, C. E. M. C. Lange, Realizations of the associahedron and cyclohedron, Discrete Comput. Geom. 37 (2007). https://arxiv.org/abs/math/0510614
• J.-L. Loday, Realization of the Stasheff polytope, Arch. Math. 83 (2004). https://arxiv.org/abs/math/0212126
• F. Chapoton, S. Fomin, A. Zelevinsky, Polytopal realizations of generalized associahedra, Canad. Math. Bull. 45 (2002). https://arxiv.org/abs/math/0202004
• N. Bergeron, C. Hohlweg, C. Lange, H. Thomas, Isometry classes of generalized associahedra, Sém. Lothar. Combin. 61A (2009).

Motivation

When indivisible goods are shared among people, comparing each person's bundle with another person's bundle is only one way to judge fairness. A second test asks whether a group could repartition the goods it collectively received so that one of its members would reliably obtain more. Groupwise maximin share (GMMS) makes this test for every subgroup. It strengthens the ordinary maximin-share benchmark, which tests only the grand coalition and all goods. Chaudhury, Kavitha, Mehlhorn and Sgouritsa use this distinction to study a complete allocation obtained from their almost envy-free allocation: goods initially left unassigned are given to one unenvied agent. Their Theorem 16 proves that the resulting allocation gives every agent at least four sevenths of her groupwise maximin share under additive valuations. Chaudhury et al., pp. 4–5, 15–16.

The paper first constructs a partial EFX allocation whose unallocated goods have bounded value to every agent. Its Section 3 then assumes additive valuations and derives maximin-share and GMMS guarantees. This mission addresses the GMMS consequence of that construction. The existence of the starting allocation is the subject of the first mission in this series; the present theorem specifies what happens when its pool is donated. Chaudhury et al., Theorems 8 and 16.

Setting

Let $N$ be a finite set of agents and $M$ a finite set of indivisible goods. Each agent $i$ has a valuation $v_i(S)$ for a bundle $S\subseteq M$. Here valuations are nonnegative and additive: $v_i(S)$ is the sum of the values of the individual goods in $S$. A partial allocation $X=(X_i)_{i\in N}$ gives pairwise disjoint bundles to the agents. The remaining goods form its pool, $P=M\setminus\bigcup_{i\in N}X_i$. An allocation is complete when its pool is empty. These are the paper's allocation conventions. Chaudhury et al., pp. 3–4.

An allocation is envy-free up to any good (EFX) if, after any single good $g$ is removed from agent $j$'s bundle, agent $i$ values that remainder no more than her own bundle: $v_i(X_j\setminus\{g\})\le v_i(X_i)$ for all $i,j$ and $g\in X_j$. The envy graph has a directed edge $i\to j$ when $i$ values $j$'s bundle more than her own. A source is a vertex with no incoming edge, so nobody envies that agent. Chaudhury et al., pp. 3, 8.

For a set $S$ and a positive number $k$ of parts, $\operatorname{MMS}_i(k,S)$ is the largest worst-part value agent $i$ can secure by partitioning $S$ into $k$ bundles. A complete allocation $Y$ is $\alpha$-GMMS when each agent meets an $\alpha$ fraction of this benchmark for every subgroup containing her:

$$v_i(Y_i)\ge\alpha\operatorname{MMS}_i\!\left(|N'|,\bigcup_{j\in N'}Y_j\right) \qquad(N'\subseteq N,\ i\in N').$$

The benchmark uses only goods allocated to that subgroup. The paper states it both as a complete-allocation property in its introduction and in Definition 15. Chaudhury et al., pp. 5, 15.

Formalization targets

The donated allocation

Assume $X$ is partial and EFX, every agent satisfies $v_i(P)\le v_i(X_i)$, and $s$ is a source of its envy graph. Define $Y_s=X_s\cup P$ and $Y_j=X_j$ for $j\ne s$. The goal states that $Y$ is complete, that donation does not lower any agent's own value, and that

$$v_i(Y_i)\ge\frac47\operatorname{MMS}_i\!\left(|N'|,\bigcup_{j\in N'}Y_j\right) \qquad(N'\subseteq N,\ i\in N').$$

This is the GMMS bullet of Theorem 16 applied to the particular allocation the authors define immediately before it. The paper obtains a suitable $X$ from Lemma 12, which has the relevant properties of Theorem 8. Chaudhury et al., pp. 11–12, 14–16.

Intermediate results

The milestones are Proposition 13, the reduction step in Theorem 16's proof, and all three parts of Lemma 17. Proposition 13 compares maximin shares after deleting agents and at most as many goods. Lemma 17 bounds the value of each bad good, the donated bundle, and the other good bundles. They retain the constants $2$ and $3/2$ used in the paper. Chaudhury et al., pp. 14, 16–17.

Significance

The result turns an almost envy-free partial allocation into a complete allocation with a guarantee for every coalition. A plain maximin-share statement would only compare each agent with a partition of all goods among all agents; here every subgroup and its allocated goods count. The distinction matters even when an ordinary maximin-share bound is easy to meet because there are fewer goods than agents. Chaudhury et al., p. 5.

The paper proves Theorem 16 mathematically. The remaining work for this mission is a machine-checked proof of its stated GMMS consequence and its supporting results. Its definitions of partial allocation, pool, finite maximin share and groupwise guarantee can also serve later formalizations of fair division. The Nash-social-welfare half-guarantee in the printed theorem depends on the starting allocation from Lemma 12; this mission records only the value preservation under donation. Chaudhury et al., pp. 14, 16.

Difficulty

Giving all leftover goods to one agent makes the allocation complete, but it can change how another agent values that enlarged bundle and how a subgroup's benchmark is calculated. EFX alone compares bundles after deleting one good; GMMS compares an agent with every repartition of a subgroup's goods. The difficulty is to control those repartitions while keeping the exact $4/7$ constant. Merely applying an ordinary maximin-share bound to the grand coalition does not establish the required subgroup inequalities. Chaudhury et al., pp. 15–17.

Formalization scope

Agents and goods are represented by Fin n and Fin m; Lean numbers agents from zero, and the paper's “agent 1” is an explicit source $s$. Bundles are finite sets. Valuations are real-valued but include nonnegativity alongside additivity, representing the paper's codomain $\mathbb R_{\ge0}$. The pool is computed from $X$, and the donated allocation is a function of $X$ and $s$. No independent pool or arbitrary completed allocation is allowed. Completeness is a conclusion. The maximin share is a finite maximum of finite minima over labelled partitions, which may have empty parts. Every use has a positive part count; in the GMMS definition this follows from $i\in N'$. Cardinality is converted to real numbers before fractions are formed. These choices exclude zero-part maximin shares and integer division. Chaudhury et al., pp. 3–5, 15–16.

The theorem is conditional on the EFX and pool-value properties of the source allocation, rather than repeating its existence proof. It states the conclusion for every such allocation and every source. The paper's half-optimal-Nash-social-welfare bullet is outside this mission because it invokes the separate black-box starting allocation of Lemma 12. Contributions toward finite-partition comparisons, EFX value bounds, and the groupwise estimate are welcome. Chaudhury et al., pp. 14–17.

Selected references

• B. R. Chaudhury, T. Kavitha, K. Mehlhorn and A. Sgouritsa, A Little Charity Guarantees Almost Envy-Freeness, SIAM Journal on Computing, 2021. Formalization source: arXiv:1907.04596v3.

Motivation

An associahedron of dimension $n$ is a simple polytope whose nonempty faces correspond, reversing inclusion, to the sets of pairwise non-crossing diagonals of a convex $(n+3)$-gon: its vertices are the triangulations of the polygon and its facets are the diagonals. Associahedra appear in the combinatorics of parenthesizations (Tamari, Stasheff), in the theory of cluster algebras of type $A$, where the Chapoton–Fomin–Zelevinsky construction realizes the cluster complex as the normal fan of a polytope, and in the study of secondary polytopes (Gelfand–Kapranov–Zelevinsky).

Many different polytopes realize the associahedron. Ceballos, Santos and Ziegler (arXiv:1109.5544v2) compare them up to normal isomorphism, a linear isomorphism of normal fans. One of the families they study, the "type II" family, is a construction of Santos presented at a conference in 2004 and first published in that paper (§5, pp. 18–23). It produces one associahedron for every triangulation $T_0$ of the $(n+3)$-gon, the seed triangulation, and contains the Chapoton–Fomin–Zelevinsky associahedron as the case of the snake seed. This mission formalizes the statement that the construction works for every seed: Theorems 5.1 and 5.2 of the paper.

Setting

Let $n \ge 0$ and $N = n+3$, and number the vertices of a convex $N$-gon $0, 1, \dots, N-1$ counterclockwise. A diagonal joins two non-adjacent vertices; two diagonals cross when their endpoints are distinct and alternate around the boundary; a triangulation is a maximal set of pairwise non-crossing diagonals, and has $n$ elements. Two triangulations differ by a flip when $T_1 \setminus T_2 = \{v_1\}$ and $T_2 \setminus T_1 = \{v_2\}$.

Fix a triangulation $T_0$ and let $V = \mathbb R^{T_0}$, with basis vectors $\alpha_\delta$, $\delta \in T_0$. Santos' vectors (p. 19) are

$$v_{pq} = -\alpha_\delta \ \text{ if } pq = \delta \in T_0, \qquad v_{pq} = \sum_{\delta \in T_0,\ pq \text{ crosses } \delta} \alpha_\delta \ \text{ if } pq \notin T_0.$$

For a set $D$ of diagonals, $\mathbb R_{\ge 0} D$ is the cone spanned by the vectors $v_e$, $e \in D$. The fan $\mathcal F_{T_0}$ is the collection of the cones $\mathbb R_{\ge 0} D$ for all non-crossing sets $D$, the empty set giving $\{0\}$.

The cones $\mathbb R_{\ge 0}T$ of the triangulations form a complete simplicial fan when the vectors of each triangulation are linearly independent, every vector of $V$ lies in one of these cones, and any two of them meet in the cone of their common diagonals.

For a polytope $P \subseteq \mathbb R^{T_0}$ and $x \in P$, the exterior normal cone is $N_P(x) = \{c : \langle c, y\rangle \le \langle c, x\rangle \text{ for all } y \in P\}$, where $\langle c, y\rangle = \sum_\delta c_\delta y_\delta$. The normal fan of $P$ is the set of all $N_P(x)$, $x \in P$, one cone for each nonempty face (p. 5).

Formalization targets

Goal: Theorems 5.1 and 5.2 (p. 19)

For every triangulation $T_0$ of the $(n+3)$-gon,

$$\{\mathbb R_{\ge0} T : T \text{ a triangulation}\} \text{ is a complete simplicial fan in } V, \quad\text{and}\quad \mathcal F_{T_0} = \{N_P(x) : x \in P\} \text{ for some polytope } P.$$

A polytope with normal fan $\mathcal F_{T_0}$ is an $n$-dimensional associahedron. The goal fixes no weights and no right-hand sides: it asserts only that some polytope has this normal fan.

Milestones

1. Theorem 5.1 (p. 19): the cones of the triangulations form a complete simplicial fan.
2. Assertion (1) of §5.1 (p. 20): $\mathbb R_{\ge 0}T_0$ is the closed negative orthant, a simplicial cone, and the only cone of $\mathcal F_{T_0}$ meeting the open negative orthant.
3. Lemma 5.3 (p. 20), with assertion (2): if $T_1, T_2$ differ by a flip removing $v_1$ and inserting $v_2$, the vectors of $T_1 \cup T_2$ have a linear dependence with nonzero coefficients of the same sign at $v_1$ and $v_2$.
4. Lemma 5.4 (p. 22): a complete simplicial fan of this kind is the normal fan of a polytope if and only if there are weights $\omega > 0$ on the generators such that $\sum_v \lambda(v)\omega(v) > 0$ for the dependence $\lambda$ of every pair of adjacent maximal cones, signed positively on the two flipped generators.
5. The inequality of p. 23: $g_{ij} = (j-i)(n+3+i-j)$ satisfies $g_{ik} + g_{jl} > \max\{g_{ij} + g_{kl}, g_{il} + g_{jk}\}$ for $1 \le i < j < k < l \le n+3$.
6. The weights of pp. 22–23: for all sufficiently small $\varepsilon > 0$, $\omega_{ij} = 2$ on $T_0$ and $\omega_{ij} = 1 + \varepsilon g_{ij}$ off $T_0$ satisfy the condition of Lemma 5.4.

Significance

Theorems 5.1 and 5.2 are what make Santos' family a family of associahedra at all. Every later statement of the paper about type II, including the classification up to normal isomorphism (Corollary 5.7: seeds agreeing up to rotation and reflection) and the identification of the Chapoton–Fomin–Zelevinsky associahedron as the only realization of both types (Theorem 6.1), compares the fans $\mathcal F_{T_0}$, and the word "associahedron" in them rests on these two theorems. The construction yields Catalan-many fans with facet normals in $\{0, \pm 1\}$-coordinates, and modulo rotations and reflections they are pairwise non-isomorphic.

The theorems are proved in the paper; to the best of a search of the Prove2Me catalogue, nothing about normal fans of polytopes, complete simplicial fans or associahedra has been formalized there, and Mathlib at the pinned revision has no notion of fan. The formalization would provide a machine-checked polytopality criterion for complete simplicial fans (Lemma 5.4), an explicit flip analysis of Santos' vectors (Lemma 5.3), and a polytopal realization of the associahedron for every seed.

Difficulty

Theorem 5.1 is not a direct computation. Linear independence of each triangulation and a sign condition for each flip do not by themselves make a fan; the paper combines them with assertion (1), a region covered by exactly one cone, and appeals to a covering criterion for vector configurations (De Loera–Rambau–Santos, Triangulations, Cor. 4.5.20, properties (ICoP) and (IPP)). A solver will likely need to formalize that criterion, or an equivalent argument that a pseudo-manifold of simplicial cones with these properties covers the space exactly once.

Lemma 5.3 requires a case analysis of how the seed triangulation meets the quadrilateral of a flip; the paper distinguishes four configurations, each with its own dependence (equations (4)–(7), p. 21), and showing that the four are exhaustive is itself a combinatorial statement about triangulations. Lemma 5.4 requires constructing a polytope from weights and identifying all of its normal cones, including the lower-dimensional ones, with the cones of the fan. Finally, the uniform constant $\varepsilon_0$ has to work for all flips at once; for the dependence (4) the unperturbed weights ($2$ on $T_0$, $1$ elsewhere) give exactly zero, so a perturbation is unavoidable and must not spoil the other cases.

Formalization scope

Vertices of the polygon are Fin (n + 3), chords are Sym2 (Fin (n + 3)), and diagonals, crossing and triangulations are reused from the published definition ChvatalArtGallery.FanPartition.Triangulation. The space $V$ is {d // d ∈ T₀} → ℝ, coordinate $d$ being the coefficient of $\alpha_d$. Cones are nonnegative hulls (PointedCone.hull ℝ). The fan contains every face, including $\{0\}$.

"Normal fan of a polytope" is encoded as: $P$ is the convex hull of a finite set, and the set of cones equals $\{N_P(x) : x \in P\}$ with exterior normal cones, functionals identified with vectors by the coordinate pairing. Because $\{0\}$ is a cone of $\mathcal F_{T_0}$, the polytope must be full-dimensional; a point, a lower-dimensional polytope, or "some polytope whose facet normals are the rays" does not satisfy the goal. The inner-normal convention would give the fan $-\mathcal F_{T_0}$, which is a different statement. The polytope is specified only through its normal fan, as in the paper.

Lemma 5.4 is stated for fans whose rays are indexed by the diagonals and whose maximal cones are the triangulations, the case in which the paper uses it; adjacent maximal cones are flip pairs. Lemma 5.3 requires the two coefficients to be strictly positive, as assertion (2) does, so the zero dependence is excluded. The ε of milestone 6 is quantified as $\exists \varepsilon_0 > 0\ \forall \varepsilon \in (0, \varepsilon_0)$. The weight $g$ is computed on 0-based positions as $(b-a)(n+3+a-b)$ for $a < b$, which equals the paper's 1-based $g_{ij}$.

A complete development needs basic fan theory (simplicial cones, a covering criterion), the polar construction behind Lemma 5.4, and the flip case analysis. The first two are reusable beyond this mission, for any polytopality argument on simplicial fans. Contributions of general lemmas on simplicial cones and on normal cones of polytopes are welcome.

Selected references

• C. Ceballos, F. Santos, G. M. Ziegler, Many non-equivalent realizations of the associahedron, Combinatorica 34 (2014); arXiv:1109.5544v2. https://arxiv.org/abs/1109.5544 — DOI 10.1007/s00493-014-2959-9
• J. A. De Loera, J. Rambau, F. Santos, Triangulations: Structures for Algorithms and Applications, Springer, 2010. https://doi.org/10.1007/978-3-642-12971-1
• F. Chapoton, S. Fomin, A. Zelevinsky, Polytopal realizations of generalized associahedra, Canad. Math. Bull. 45 (2002). https://arxiv.org/abs/math/0202004
• G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995. https://doi.org/10.1007/978-1-4613-8431-1

Motivation

An associahedron is a polytope whose faces encode ways to dissect a convex polygon without crossing diagonals. Its vertices represent triangulations. Associahedra occur in geometric combinatorics because the same combinatorial object admits many geometric realizations. Ceballos, Santos and Ziegler ask when two such realizations have the same normal fan up to a linear change of coordinates. This question distinguishes geometric constructions that have identical face lattices but different arrangements of facet normals. Their Santos family is indexed by seed triangulations, so its classification asks exactly how much of a seed can be recovered from its fan. Ceballos, Santos and Ziegler, §5.3.

Santos' construction was presented at a conference in 2004 and first appeared in print in this paper. The paper proves that the number of normal-isomorphism classes in this family is the number of polygon triangulations modulo rotations and reflections. It also explains a useful limit of the result: the set of normal vectors alone determines only the abstract dual tree of the seed triangulation, while the fan retains the further information needed for classification. Ceballos, Santos and Ziegler, §5 and Proposition 5.8.

Setting

Take a convex polygon with $N=n+3$ vertices in cyclic order and label its positions $0,\ldots,N-1$. A diagonal joins two nonadjacent vertices. A triangulation $T$ is a maximal collection of diagonals with no crossings. Each triangulation has $n$ diagonals. A flip removes one diagonal shared by two triangles and inserts the other diagonal of their quadrilateral.

Choose a seed triangulation $T_0$. Let $V_{T_0}=\mathbb R^{T_0}$, with a coordinate $\alpha_d$ for each seed diagonal $d$. Santos assigns a vector to every polygon diagonal $e$:

$$v_e(T_0)= \begin{cases} -\alpha_e,&e\in T_0,\\ \displaystyle\sum_{d\in T_0:\,e\text{ crosses }d}\alpha_d,&e\notin T_0. \end{cases}$$

For each noncrossing set $D$ of diagonals, take the cone spanned by the vectors $v_e(T_0)$, $e\in D$, with nonnegative real coefficients. The collection of these cones is the fan $F(T_0)$. The paper proves that it is complete and is the normal fan of an associahedron. This mission uses that explicit fan as the meaning of $\mathrm{Ass}^{II}_n(T_0)$, following the paper's own convention in §5.3. Ceballos, Santos and Ziegler, pp. 19, 23, Theorems 5.1–5.2.

Two fans are normally isomorphic here when an invertible real linear map sends every cone of the first to a cone of the second. A dihedral symmetry is a rotation or a reflection of the cyclically ordered polygon. It acts on a triangulation by relabelling both endpoints of each diagonal. Write $T_1\sim_D T_2$ when such a symmetry sends $T_1$ to $T_2$.

Formalization targets

Classification of Santos associahedra

For every $n\ge 0$ and triangulations $T_1,T_2$ of the $(n+3)$-gon, the goal is Corollary 5.7:

$$F(T_1)\cong_{\mathrm{lin}}F(T_2) \quad\Longleftrightarrow\quad T_1\sim_D T_2.$$

The left side compares all cones of the two fans through a linear isomorphism. The right side permits only the $2(n+3)$ rotations and reflections of the polygon. It makes no choice of an ordering for the diagonals within either seed.

Intermediate source results

The milestone list follows the paper's argument: the polygon symmetry theorem for the associahedron's face lattice (Lemma 2.2); the induced crossing and parallelism preserving bijection of diagonals; the description and count of parallel facet pairs for Santos fans (Proposition 5.5); the injectivity of $T\mapsto B_T$, where $B_T$ contains a seed and all single-flip insertions (Lemma 5.6); and invariance under rotations and reflections. Ceballos, Santos and Ziegler, pp. 6, 23–24.

Significance

The classification says precisely which apparent choices of seed triangulation are redundant. In particular, different dihedral orbits produce different normal-fan geometries even though all the resulting polytopes have the associahedron's face lattice. Parallel facet pairs supply an intrinsic geometric trace of the seed: they correspond to each seed diagonal and its flip. Lemma 5.6 then separates distinct seeds from their collections of these pairs. Ceballos, Santos and Ziegler, Proposition 5.5, Lemma 5.6 and Corollary 5.7.

The result is proved in the paper. The formalization work is to give a machine-checked account of its fan model and classification, including the polygon combinatorics and the linear-algebraic implications of a fan isomorphism. The supplied statements are proof targets, with sorry at theorem bodies; a complete Lean proof of the classification is not yet claimed. The explicit diagonal and crossing representation and the seed-indexed vector construction can also be reused to formalize the paper's fan and polytopality theorems.

Difficulty

A face-lattice isomorphism alone does not identify the seed: every associahedron in the family has the same face lattice. A first attempt to compare only the vectors also loses information. Proposition 5.8 shows that two different seed triangulations with isomorphic dual trees can yield linearly equivalent vector sets. The full fan records which vectors span cones together. The central task is to recover a crossing-preserving map of diagonals from a linear map of fans, then use the opposite directions of facet normals to recover $B_T$. Ceballos, Santos and Ziegler, pp. 23–24, Propositions 5.5 and 5.8.

Formalization scope

Lean represents polygon positions by Fin (n + 3) and unordered diagonals by Sym2; crossings and triangulations come from the published Chvátal triangulation definition. The ambient real vector space for a seed is the function space on the subtype of its actual diagonals. This makes the basis intrinsic to $T$. A cone is the nonnegative real hull of the Santos vectors attached to a noncrossing diagonal set. NormallyIsomorphic demands a real linear equivalence of these ambient spaces. The classifying symmetry is explicitly $i\mapsto r+i$ or $i\mapsto r-i$ modulo $n+3$.

No premise asserts the classification, and the fan is built from the paper's vectors rather than from a chosen list of abstract cones. Arbitrary permutations of diagonals, nonlinear maps, and an abstractly isomorphic dual tree do not satisfy the target's symmetry condition. The goal and the diagonal-action clause of Lemma 2.2 cover every $n$; the separate group-order clause in Lemma 2.2 applies for $n\ge2$. Lemma 5.6 carries the printed bound $n\ge2$. The triangular and quadrilateral cases are included in the goal and require their own boundary treatment in a proof. Contributions on crossing preservation, ray distinctness, linear independence of maximal cones, single-flip combinatorics, and dihedral equivariance are welcome.

Selected references

• C. Ceballos, F. Santos and G. M. Ziegler, Many non-equivalent realizations of the associahedron, Combinatorica 34 (2014), 513–551; preprint arXiv:1109.5544v2 (2013). arXiv, DOI.

Fair division of indivisible goods

A set of $n$ agents must share a set $M$ of $m$ indivisible goods, each agent valuing bundles of goods by her own valuation. Two fairness notions dominate the literature. Envy-freeness up to any good (EFX), introduced by Caragiannis, Kurokawa, Moulin, Procaccia, Shah and Wang (EC 2016), asks that no agent prefer another's bundle once any single good is removed from it. The maximin share (MMS), proposed by Budish (JPE 2011), asks that every agent receive at least what she could secure by splitting the goods into $n$ bundles herself and taking the worst one.

Neither notion is known to be achievable in full. Whether complete EFX allocations always exist is open in general. Complete MMS allocations need not exist: Procaccia and Wang (EC 2014) gave a counterexample with three agents, and the best known approximation factors for additive valuations are $3/4-\varepsilon$ (Ghodsi et al., EC 2018) and $3/4$ (Garg and Taki, arXiv:1903.00029). Amanatidis, Birmpas and Markakis (IJCAI 2018) showed that every complete EFX allocation is a $4/7$-MMS allocation.

Caragiannis, Gravin and Huang (EC 2019) showed that EFX can be achieved if some goods are left unallocated, with no bound on how many. Chaudhury, Kavitha, Mehlhorn and Sgouritsa (arXiv:1907.04596, SODA 2020, SIAM J. Comput. 2021) relax completeness instead: some goods may be "donated to charity". Their Theorem 8 produces an EFX partial allocation in which nobody envies the donated set and the donated set has fewer goods than there are unenvied agents. This mission formalizes their Theorem 14: such an allocation also gives every agent a maximin-share guarantee that improves as more goods are donated.

Setting

Agents are $N=[n]$ and goods are $M$, $|M|=m$. Agent $i$ has a valuation $v_i:2^M\to\mathbb{R}_{\ge 0}$, assumed additive: $v_i(S)=\sum_{g\in S}v_i(\{g\})$ for every $S\subseteq M$.

A (partial) allocation $X=\langle X_1,\dots,X_n\rangle$ gives agent $i$ the bundle $X_i\subseteq M$, the bundles being pairwise disjoint. The pool of unallocated goods is $P=M\setminus\bigcup_i X_i$, and $k=|P|$.

• $X$ is EFX if $v_i(X_i)\ge v_i(X_j\setminus\{g\})$ for all agents $i,j$ and every $g\in X_j$.
• The envy graph $G_X$ has the agents as vertices and an edge $i\to j$ exactly when $v_i(X_i)<v_i(X_j)$. A source is a vertex of indegree zero: an agent nobody envies.
• The maximin share of agent $i$ over $k'\ge1$ bundles of a set $S$ of goods is

$$\mathrm{MMS}_i(k',S)=\max_{(S_1,\dots,S_{k'})}\ \min_{1\le j\le k'} v_i(S_j),$$

the maximum over partitions of $S$ into $k'$ possibly empty bundles. Agent $i$'s maximin share in the instance is $\mathrm{MMS}_i(n,M)$.

The three conditions of Theorem 8 on $(X,P)$ are:

1. $X$ is EFX;
2. $v_i(X_i)\ge v_i(P)$ for every agent $i$;
3. $|P|$ is less than the number of sources of $G_X$; in particular $|P|<n$.

Formalization targets

Goal: Theorem 14 (MMS bullet)

For every allocation $X$ with pool $P$ satisfying conditions 1–3, and every agent $i$,

$$v_i(X_i)\ \ge\ \frac{\mathrm{MMS}_i(n,M)}{2-\frac{k}{n}},\qquad k=|P|.$$

The factor ranges from $\tfrac12$ when $P=\emptyset$ to $(1+\tfrac1n)^{-1}$ when $|P|=n-1$.

Milestones

1. Proposition 13 (quoted by the paper from Garg, McGlaughlin and Taki, SOSA 2019): for $N'\subseteq N$ and $M'\subseteq M$ with $|N\setminus N'|\ge|M\setminus M'|$ and $i\in N'$,

$$\mathrm{MMS}_i(|N'|,M')\ \ge\ \mathrm{MMS}_i(|N|,M).$$

2. MMS is at most the proportional share: $\mathrm{MMS}_i(k',S)\le v_i(S)/k'$ for additive valuations and $k'\ge1$.
3. The EFX half-bound: if $X$ is EFX and $|X_j|\ge2$, then $v_i(X_i)\ge(1-1/|X_j|)\,v_i(X_j)\ge\tfrac12 v_i(X_j)$.
4. The counting step (summing inequalities (1)–(3) of the proof): with $N'$ the sources of $G_X$, agent $i$ and all agents holding at least two goods, $n'=|N'|$ and $M'=\bigcup_{j\in N'}X_j$,

$$(2n'-k)\,v_i(X_i)\ \ge\ v_i(M'\cup P).$$

Significance

Theorem 14 shows that leaving goods unallocated is not merely a cost: under conditions 1–3, each donated good buys a quantitative improvement of every agent's maximin-share guarantee, interpolating between the factor $\tfrac12$ the bound gives when the pool is empty and a factor tending to $1$ when nearly $n$ goods are donated. Together with Theorem 8 it shows that a single allocation can be simultaneously EFX, envy-free towards the charity, small in its charity, and approximately MMS. The same reduction (Proposition 13 applied to a carefully chosen sub-instance) is the template for the paper's $4/7$-groupwise-maximin-share result, Theorem 16, formalized in mission III of this series.

The result is proved in the paper; no machine-checked proof of it, of Proposition 13, or of the existence of EFX allocations with bounded charity is known to exist. The mission produces a formal maximin-share definition on arbitrary subsets of goods with an arbitrary number of bundles, a formal proof of the monotonicity of the maximin share under removal of agents and goods (Proposition 13, which the paper quotes without proof), and the guarantee itself. Combined with mission I of this series (Theorem 8), it yields the printed existence statement.

Difficulty

The guarantee compares an agent's own bundle with a benchmark defined over all partitions of all goods, while EFX and the source condition speak only about the allocation at hand. The obvious attempt, summing $v_i(X_i)\ge\tfrac12 v_i(X_j)$ over all agents and adding the pool, gives only a factor near $\tfrac12$ and ignores the pool's size. Agents holding a single good are the obstruction: EFX gives no bound on the value of their bundles relative to $v_i(X_i)$, and the benchmark $\mathrm{MMS}_i(n,M)$ is defined on the full instance, which contains them. Proposition 13, the comparison of maximin shares across instances, is a combinatorial statement about all partitions of the original instance and requires nonnegativity of the valuations: with a good of negative value it fails.

Formalization scope

Agents are Fin n (0-based) and goods Fin m; the set $M$ is the whole of Fin m. Valuations are functions Fin n → Finset (Fin m) → ℝ; additivity is the sum formula together with nonnegativity, which is the paper's codomain $\mathbb{R}_{\ge0}$. An allocation is a family of pairwise disjoint finsets and the pool is always computed as the complement of their union, never taken as a free parameter. Sources are agents of indegree zero in the envy graph (nobody envies them), not agents who envy nobody. The maximin share $\mathrm{MMS}(k',S)$ is a supremum over labellings Fin m → Fin k' restricted to $S$ of the minimum bundle value; it is used only with $k'\ge1$, which every statement has in its hypotheses or derives from them (in the goal, condition 3 forces $n\ge1$). Every cardinality is cast to $\mathbb{R}$ before division or subtraction, and $2-k/n>1$ under condition 3, so no division by zero occurs.

The goal is posed as an implication for every allocation satisfying conditions 1–3, rather than as the paper's "there exists an allocation"; the paper's proof of the MMS bullet uses only those three conditions, and existence is Theorem 8. The Nash-social-welfare bullet of Theorem 14 is not posed: it depends on Lemma 12, which takes the allocation of an earlier paper as a black box. The goal cannot be trivialized by a free pool, by overlapping bundles, by zero agents (condition 3 excludes them), by a junk maximin share over zero bundles, or by natural-number division; the statement keeps all three conditions, each of which is needed.

Contributions welcome: a library-quality maximin-share API for additive valuations (attainment of the maximum, monotonicity, the proportional bound), which is reusable for other MMS results; proofs of the milestones; and the final assembly.

Selected references

• B. R. Chaudhury, T. Kavitha, K. Mehlhorn, A. Sgouritsa, A Little Charity Guarantees Almost Envy-Freeness, SIAM J. Comput. 50(4), 2021; cited from arXiv:1907.04596v3. https://arxiv.org/abs/1907.04596
• E. Budish, The Combinatorial Assignment Problem: Approximate Competitive Equilibrium from Equal Incomes, J. Political Economy 119(6), 2011. https://doi.org/10.1086/664613
• I. Caragiannis, D. Kurokawa, H. Moulin, A. D. Procaccia, N. Shah, J. Wang, The Unreasonable Fairness of Maximum Nash Welfare, EC 2016. https://doi.org/10.1145/2940716.2940726
• A. D. Procaccia, J. Wang, Fair Enough: Guaranteeing Approximate Maximin Shares, EC 2014. https://doi.org/10.1145/2600057.2602835
• M. Ghodsi, M. HajiAghayi, M. Seddighin, S. Seddighin, H. Yami, Fair Allocation of Indivisible Goods: Improvements and Generalizations, EC 2018. https://doi.org/10.1145/3219166.3219238
• J. Garg, S. Taki, An Improved Approximation Algorithm for Maximin Shares, CoRR abs/1903.00029, 2019. https://arxiv.org/abs/1903.00029
• J. Garg, P. McGlaughlin, S. Taki, Approximating Maximin Share Allocations, SOSA 2019. https://doi.org/10.4230/OASIcs.SOSA.2019.20
• I. Caragiannis, N. Gravin, X. Huang, Envy-Freeness up to Any Item with High Nash Welfare: The Virtue of Donating Items, EC 2019. https://doi.org/10.1145/3328526.3329574
• G. Amanatidis, G. Birmpas, E. Markakis, Comparing Approximate Relaxations of Envy-Freeness, IJCAI 2018. https://doi.org/10.24963/ijcai.2018/7

Motivation

An associahedron is a polytope whose vertices represent triangulations of a convex polygon and whose edges represent flips between triangulations. The same combinatorial polytope can be realized in different vector spaces with different facet directions. This matters when a construction uses the geometry of the realization, rather than only its face lattice: a linear change of coordinates can preserve its normal fan, while a general combinatorial relabelling need not. Ceballos, Santos and Ziegler compare three constructions and use parallel facets to distinguish them.

Two of those constructions form large families. Hohlweg–Lange choose a word of signs; Santos chooses a triangulation as a seed. Both yield associahedra, and both include the Chapoton–Fomin–Zelevinsky (CFZ) realization. The paper proves that CFZ is their only shared normal-isomorphism class. Its Theorem 6.1 is the target here; the result was announced as Theorem 1.1 in the introduction. Source, pp. 4 and 28.

Setting

Fix $n\ge0$ and a convex polygon with $n+3$ cyclically ordered vertices. A diagonal joins two nonadjacent vertices. Two diagonals cross when their endpoints alternate around the boundary. A triangulation is a maximal collection of pairwise noncrossing diagonals. Every triangulation has $n$ diagonals, and replacing one diagonal with the other diagonal of the quadrilateral it borders is a flip. The faces of an associahedron correspond to noncrossing sets of diagonals, while its vertices correspond to triangulations. Source, pp. 5 and 18–19.

A normal fan records the outward normal directions of all faces of a polytope and the cones they span. Two complete fans are linearly isomorphic when a real linear equivalence sends every cone of the first to a cone of the second. Polytopes are normally isomorphic when their normal fans are linearly isomorphic. This is Definition 2.1 of the paper; the comparison is geometric because it requires a linear map. Source, p. 5.

For the Hohlweg–Lange family, choose a sign word $\sigma\in\{+,-\}^{n-1}$ and extend it to $\widetilde\sigma=(+,-,\sigma,-,+)$ on the labels $0,\ldots,n+2$. The negative labels, in increasing order, form one boundary chain; the positive labels, in decreasing order, form the other. For a diagonal with endpoint labels $i<j$, let $R_{ij}(\sigma)$ contain the labels strictly below it. Form $S_{ij}(\sigma)$ by replacing $0$ with $i$ and $n+2$ with $j$ if those labels occur in $R_{ij}(\sigma)$. The characteristic vector of $S_{ij}(\sigma)$, considered modulo the all-ones vector, gives its facet normal. Source, pp. 14–16, Definition 4.1.

For the Santos family, choose a seed triangulation $T_0$ and use one basis vector $\alpha_d$ for each seed diagonal $d$. The normal assigned to a diagonal $e$ is $-\alpha_e$ when $e\in T_0$. Otherwise it is the sum of $\alpha_d$ over seed diagonals crossing $e$. The cones spanned by compatible diagonal vectors give the fan. The distinguished snake seed joins alternating polygon positions $1,n+2,2,n+1,3,\ldots$; this seed gives the CFZ fan. Source, pp. 13 and 18–19.

Formalization targets

The only shared class

Let $F^I_n(\sigma)$ and $F^{II}_n(T)$ be the two normal fans, and let $S_n$ be the fixed snake. If $T$ is a triangulation, the target says

$$F^I_n(\sigma)\cong_{\mathrm{lin}}F^{II}_n(T) \quad\Longrightarrow\quad T=g(S_n)\text{ for some rotation or reflection }g,$$

and it also asserts that $F^I_n(+,-,+,-,\ldots)\cong_{\mathrm{lin}}F^{II}_n(S_n)$. Together these are the uniqueness and existence parts of Theorem 6.1. The result covers dimensions zero and one as well as higher dimensions; Lemma 2.2 uses $n\ge2$ only for its second sentence, the uniqueness of the inducing symmetry. Source, pp. 6, 16 and 28–29.

Supporting targets

The milestone list follows the paper's stated intermediate results: polygon symmetries of the associahedron, the parallel-facet pairs in each family, and the three properties of triangles in the seed that force the snake. Proposition 4.4 supplies the alternating-sign realization used for existence. The parallel-pair targets retain the source's exact count of $n$ pairs, through their characterization by the $n$ seed flips or the $n$ labelled quadrilaterals. Source, pp. 6, 16–17, 23 and 28–29.

Significance

Theorem 6.1 gives a complete answer to a comparison question that face-lattice data alone cannot settle: every member of either family has the same associahedral combinatorics, but almost no cross-family pair has linearly equivalent normal fans. It identifies the exceptional class without fixing coordinates for either construction. The characterization of parallel facets also gives a concrete invariant for later comparisons among associahedron realizations. Source, pp. 23 and 27–28.

The paper proves the result mathematically. A complete Lean development would add machine-checked definitions of the two ray systems and a proof of the classification, including the geometric step that a linear fan isomorphism induces a compatible correspondence of facet rays. The polygon triangulation and crossing definitions are already available as a published reusable component; proofs about fans and the two constructions are the remaining work.

Difficulty

An isomorphism of abstract face lattices gives too little information: it exists between all associahedra of the same dimension. The useful comparison must control a linear map on the actual normal vectors. The first obstacle is proving that such a map preserves the rays and therefore preserves which facets are parallel. Then the two explicit descriptions of parallel pairs must be reconciled, and the resulting sign restriction on a triangulation must force alternating turns of its dual path. Showing only that the dual tree is a path is insufficient; path triangulations can make consecutive turns on the same side. Source, pp. 17, 23 and 28–29.

Formalization scope

Vertices are Fin (n+3) in counterclockwise positions, with zero-based indexing; Hohlweg–Lange signs apply to labels carried by those positions. Diagonals are unordered pairs. The imported Chvátal triangulation definition gives boundary edges, crossings, maximal noncrossing sets, and their triangles. A cone is the nonnegative span of the vectors assigned to a noncrossing set. The type I vectors are represented in $\mathbb R^n$ using quotient coordinates $x_k-x_{n+1}$; type II vectors are functions on the seed diagonals. Hohlweg–Lange Proposition 4.3, cited in the paper, identifies the maximal cones of the type I normal fan with triangulations. Source, pp. 15–16.

Normal isomorphism uses a real linear equivalence, dihedral symmetry uses only rotations and reflections of the polygon, and the snake is the explicit alternating triangulation. The cones use the actual facet vectors. These commitments exclude a mere bijection of index sets, an arbitrary permutation of vertices, and a path triangulation with nonalternating turns. The condition $n\ge2$ appears only where the page has it, in the second sentence of Lemma 2.2 (uniqueness of the inducing symmetry); facet-normal comparisons quantify only over diagonals, exactly the facets represented in the paper. Reusable contributions include combinatorial flip lemmas, linear independence of triangulation rays, and general results about linear maps of simplicial fans.

Selected references

• César Ceballos, Francisco Santos, and Günter M. Ziegler, Many non-equivalent realizations of the associahedron, Combinatorica 34 (2014), 513–551. arXiv:1109.5544v2.

Motivation

Allocating indivisible goods fairly is difficult because a single good can change how an agent compares two bundles. Exact envy-freeness can be impossible (one good, two agents), so the field works with relaxations. Envy-freeness up to any good (EFX) requires each agent to prefer her own bundle to every other agent's bundle after any one good of that other bundle is removed. Whether EFX allocations of all goods always exist is open; the question motivates weakening the requirement that every good be assigned, and asking how little must be left over. Chaudhury, Kavitha, Mehlhorn and Sgouritsa show that leaving a small, unenvied set of goods unallocated (donated to "charity") suffices for every normalized monotone valuation profile (arXiv:1907.04596v3, Theorem 8, pp. 11–12).

Timeline (as recounted on pp. 2–3 of the source):

• 2004: Lipton, Markakis, Mossel and Saberi introduce the envy-graph and cycle-elimination technique and compute allocations now called EF1 (DOI 10.1145/988772.988792).
• 2016: Caragiannis, Kurokawa, Moulin, Procaccia, Shah and Wang define EFX (DOI 10.1145/2940716.2940726).
• 2018: Plaut and Roughgarden prove EFX allocations of all goods exist for two agents, or for any number of agents with identical valuations (arXiv:1707.04769).
• 2019: Caragiannis, Gravin and Huang introduce EFX with charity: a partial EFX allocation in which each agent gets at least half her value in a Nash-optimal allocation, with no bound on the number or value of donated goods (arXiv:1902.04319).
• 2020: Chaudhury, Garg and Mehlhorn prove existence of complete EFX allocations for three agents with additive valuations (arXiv:2002.05119).
• 2020/2021: the present paper bounds the charity: fewer goods than unenvied agents, and no agent envies the donated set. Its SODA 2020 version assumed gross-substitute valuations; the journal version (arXiv v3) needs only normalized monotone valuations (p. 8, §1.4).

The two bounds matter separately. The empty allocation is EFX and donates everything; a cardinality bound alone still lets the donated goods carry most of an agent's value; the value bound alone allows almost all goods to be donated. The paper's later maximin-share and groupwise-maximin-share guarantees (Theorems 14 and 16, treated in the next missions of this series) are derived from exactly the allocation produced here.

Setting

There are $n\ge1$ agents, indexed by $N=\{1,\ldots,n\}$ in the paper, and a finite set $M$ of $m$ indivisible goods. Agent $i$ has a valuation $v_i:2^M\to\mathbb R_{\ge0}$. It is normalized if $v_i(\varnothing)=0$ and monotone if $S\subseteq T$ implies $v_i(S)\le v_i(T)$. No additivity, submodularity or substitutes condition is assumed. These are the general valuations of §1.1.1, p. 3, and §2 of the source.

A partial allocation $X=(X_i)_{i\in N}$ consists of pairwise disjoint bundles $X_i\subseteq M$. Its pool is the goods not assigned to anyone,

$$P(X)=M\setminus\bigcup_{i\in N}X_i.$$

The allocation is EFX when

$$v_i(X_j\setminus\{g\})\le v_i(X_i) \qquad\text{for all }i,j\in N\text{ and every }g\in X_j.$$

The paper calls allocations partial by default (p. 3, footnote 5). The envy graph $G_X$ has the agents as vertices and an edge $i\to j$ when $v_i(X_i)<v_i(X_j)$. A source is a vertex with no incoming edge. Its reachability component $C(s)$ includes $s$ itself. The social welfare of $X$ is $\phi(X)=\sum_i v_i(X_i)$. These notions are introduced on pp. 8–9 of the source.

For a set $S$ of goods, an envied set is one some agent values more than her own bundle. An inclusion-wise minimal envied subset $Z$ is envied, but no strict subset of $Z$ is envied by anyone. An agent who envies such a $Z$ is a most envious agent of $S$; the paper allows ties. The three update rules U0, U1 and U2 use these sets to change an allocation while maintaining EFX (Definition 3 and Algorithm 2, p. 9).

Formalization targets

The goal is the allocation guarantee of Theorem 8:

$$\exists X\text{ partial}:\quad X\text{ is EFX},\qquad v_i(P(X))\le v_i(X_i)\ (i\in N),\qquad |P(X)|<|\operatorname{sources}(G_X)|\le n.$$

Both the stronger source-count bound and its consequence $|P(X)|<n$ are stated. The theorem asserts existence for every normalized, monotone valuation profile, including nonadditive profiles. It does not require the returned envy graph to be acyclic; acyclicity is an invariant used during construction, rather than an additional advertised property of the final allocation.

The attack path consists of the paper's numbered Lemmas 2, 4, 5, 6 and 7. Lemma 2 concerns removal of envy cycles; its Lean form keeps the page's conditional "if $X$ is EFX then $X'$ is EFX" and the unconditional strict welfare increase. Lemma 4 records what U0 does and what its failure implies. Lemma 5 records U1's welfare and EFX guarantees. Lemma 6 supplies the finite source, good and agent data required for U2. Lemma 7 states U2's welfare and EFX guarantees. Their source wording and page locations appear in the milestone list; the Lean statements include the exact allocation updates where those lemmas rely on them.

Significance

The theorem guarantees a partial EFX allocation even for general monotone valuations, while limiting the unallocated pool more tightly than the number of agents: its size is below the number of unenvied agents. Every agent also values that entire pool no more than her own bundle. These two bounds distinguish the allocation from a merely EFX partial allocation. They provide the starting point for the paper's later statements on approximate maximin shares under additive valuations (Theorems 14 and 16).

The mathematical result is proved in the paper. The mission asks for a machine-checked proof of its allocation guarantee and of the supporting lemmas, with a reusable Lean account of finite partial allocations, the unallocated pool, envy graphs, minimal envied subsets and the update rules. Such definitions are useful for other fair-division questions involving unallocated indivisible goods.

Difficulty

EFX must hold after the allocation is changed, for every agent pair and for removal of every good from the other agent's new bundle. Simply giving a pool good to an agent may violate that condition, even though it makes the pool smaller. Conversely, replacing a bundle with an envied subset can improve welfare while returning goods to the pool. The source-count bound depends on controlling both kinds of progress. Rule U2 adds a further complication: its bundle moves follow envy paths, so an overlap between selected paths would make the new allocation ambiguous. These are the points at which the straightforward approach of distributing the remaining goods one at a time stops working.

Formalization scope

Lean represents agents by Fin n, goods by Fin m, bundles by finite sets of goods, and valuations by real-valued functions on bundles. The paper's one-based subscripts become zero-based Lean indices. Nonnegative values need no separate hypothesis: normalization and monotonicity imply them. The hypothesis $n>0$ is explicit because the paper presumes agents and the strict bound $|P|<n$ is false when $n=0$. The pool is computed as the complement of the union of pairwise disjoint assigned bundles. It is never a free set. EFX ranges over every pair $i,j$, including $i=j$, and every good of $X_j$.

The minimal-envied-subset definition checks every strict subset against every agent. The most envious agent is a relation, allowing the paper's arbitrary tie choice. Reachability includes a path of length zero. U2's new allocation is calculated from its paths and chosen subsets. Lemma 6 includes Algorithm 1's acyclic-graph invariant and the ordering property established in its proof. It replaces the printed threshold $|P|\ge n$ with $|P|\ge|\operatorname{sources}(G_X)|$, the exact number of fresh goods its construction needs and the threshold used by the goal. Lemma 7 takes that ordering property to make path assignments unambiguous.

The printed U2 pool expression in Algorithm 2, line 13, is malformed; the formal statement uses the pool of the constructed allocation and the corrected union of leftover goods. Theorem 8's final sentence also asserts an $nmV/\Delta$ iteration bound. This mission poses the allocation conclusions, while a future run-level formalization would be needed to state and check the iteration count. The paper's preceding count of U1/U2 steps and successive U0 steps does not by itself imply the printed number. Definitions and the numbered lemma statements are welcome contributions; a purported proof that uses a free empty pool, overlapping bundles, zero agents or an arbitrary replacement allocation would not establish this target.

Selected references

• B. R. Chaudhury, T. Kavitha, K. Mehlhorn and A. Sgouritsa, A Little Charity Guarantees Almost Envy-Freeness, arXiv:1907.04596v3, 2020; published in SIAM Journal on Computing, 2021. Pinned preprint.
• R. J. Lipton, E. Markakis, E. Mossel and A. Saberi, On approximately fair allocations of indivisible goods, ACM EC 2004. https://doi.org/10.1145/988772.988792
• I. Caragiannis, D. Kurokawa, H. Moulin, A. D. Procaccia, N. Shah and J. Wang, The unreasonable fairness of maximum Nash welfare, ACM EC 2016. https://doi.org/10.1145/2940716.2940726
• B. Plaut and T. Roughgarden, Almost envy-freeness with general valuations, SODA 2018. https://arxiv.org/abs/1707.04769
• I. Caragiannis, N. Gravin and X. Huang, Envy-freeness up to any item with high Nash welfare: the virtue of donating items, ACM EC 2019. https://arxiv.org/abs/1902.04319
• B. R. Chaudhury, J. Garg and K. Mehlhorn, EFX exists for three agents, ACM EC 2020. https://arxiv.org/abs/2002.05119

Why excluded minors matter here

Many graph classes are defined by excluding a fixed graph as a minor. A minor can be formed by deleting vertices, deleting edges, and contracting edges. Planar graphs, for example, exclude $K_5$ as a minor. Édouard Bonnet, Eun Jung Kim, Stéphan Thomassé, and Rémi Watrigant proved that every class excluding a fixed clique minor has bounded twin-width, a graph parameter that controls how much adjacency information is lost while vertices are successively combined. Their result connects a classical graph-minor restriction with the contraction parameter used in their first-order model-checking framework. The explicit bound is very large, but it establishes that the width depends only on the excluded clique size, rather than on the graph's number of vertices. Bonnet et al., Twin-width I, Theorem 6.3.

Graphs, contractions, and matrix orders

Let $G$ be a finite simple graph. A partition of its vertices is a collection of nonempty, disjoint parts covering all vertices. Two distinct parts are homogeneous if every vertex pair across them is adjacent, or every such pair is nonadjacent. Otherwise the pair of parts is marked red. A $d$-partition has at most $d$ red neighbours at every part. A contraction sequence begins with singleton parts, merges two parts at each step, and finishes with at most one part. The statement $\operatorname{tww}(G)\le d$ says that such a sequence exists with every intermediate partition a $d$-partition. This partition formulation is equivalent to the paper's original description in terms of trigraph contractions. Bonnet et al., pp. 3:11–3:12, 3:32.

Write $K_t$ for the complete graph on $t$ vertices. The graph $G$ is $K_t$-minor free when $K_t$ cannot be obtained from $G$ by the minor operations above. The Lean statement uses a branch-set formulation: a minor model consists of disjoint, nonempty, connected vertex sets, with a connecting edge for each edge of the minor. Bonnet et al., p. 3:9.

An ordering $\sigma$ of the vertices gives a Boolean adjacency matrix $A_\sigma(G)$, with entry $1$ at an edge and $0$ otherwise. A division cuts its rows and columns into nonempty consecutive intervals. A zone is mixed if it is neither constant down its columns nor constant across its rows. A $k$-mixed minor is a division with $k$ row intervals and $k$ column intervals in which every zone is mixed; a $k$-grid minor requires a $1$ in every zone. A matrix is $k$-mixed free or $k$-grid free if the corresponding minor does not exist. A mixed Boolean zone always contains a $1$, so grid freeness implies mixed freeness. Bonnet et al., pp. 3:18–3:19.

The order used in the proof is a depth-first search (DFS). A discovery order $v_1,\dots,v_n$ lists the vertices; at each time the active vertex is the lastly discovered vertex that still has an undiscovered neighbour, and the next vertex is a neighbour of the active vertex, which becomes its parent in the DFS tree $\mathcal T$. The Lex-DFS breaks ties: among the connected components of the undiscovered vertices that meet the active vertex's neighbourhood, it enters one whose word (the $0/1$ vector recording which discovered vertices have a neighbour in the component) is lexicographically largest. The proof also uses minimal subtrees of $\mathcal T$: the union of the tree paths between the vertices of a set. Bonnet et al., pp. 3:26–3:27.

Formalization targets

The main target is the explicit excluded-clique-minor bound. With

$$c_k=\frac83(k+1)^2 2^{4k},\qquad g(t)=2(2^{4t+1}+2)^2,\qquad f(t)=4c_{g(t)}2^{4c_{g(t)}+2},$$

the goal says

$$K_t\not\preceq G\quad\Longrightarrow\quad \operatorname{tww}(G)\le f(t).$$

The $+2$ in $g(t)$ follows the value defined and used in the proof of Theorem 6.3 on p. 3:26; the printed theorem statement has $+1$. The formal target uses the proof-supported bound and records the printed statement verbatim in its provenance. It does not assert the paper's asymptotic triple-exponential notation as a separate theorem. Bonnet et al., pp. 3:26–3:29.

The milestones follow the proof in order:

1. twin-width is the maximum over connected components;
2. a Lex-DFS exists from any vertex of a connected graph;
3. Lemma 6.4: in any DFS, the vertices $a_{i,j}$ of the proof lie on one branch of $\mathcal T$;
4. Lemma 6.5: the enhancements $B^*_j$ avoid the paths $A'_i$, except the last ones;
5. $|V(H)|\le\alpha(H)\omega(H)$ for intersection graphs of subtrees of a tree;
6. the Helly property for subtrees of a tree;
7. Lemma 6.6: each component of $\mathcal T[v]-\{v\}$ meets at most two enhancements of the clique;
8. for a connected $K_t$-minor-free graph, the adjacency matrix in any Lex-DFS order is $g(t)$-grid free;
9. grid free implies mixed free for $0/1$ matrices;
10. the graph form of Theorem 5.8 with the explicit constant applied on p. 3:29.

The Helly theorem is a reference to an existing open platform statement rather than a duplicate draft. Bonnet et al., pp. 3:22–3:29.

What the bound supplies

The theorem supplies a uniform contraction-width bound for every fixed excluded clique minor. In particular, the paper applies it to planar graphs through exclusion of $K_5$. Its numerical value is far from small; the article remarks that the planar specialization has billions of digits. Without the result, excluding a clique minor alone would not yield the particular twin-width certificate required for those applications. Bonnet et al., p. 3:29.

The mathematical result is proved in the cited paper. This mission asks for machine-checked statements and, eventually, proofs of its graph and matrix claims. The reusable output includes a precise partition model of graph twin-width, interval-division models of mixed and grid minors, and a graph statement that converts a mixed-free adjacency order into a contraction-width bound. No machine-checked proof of these new target items is claimed here.

The main obstruction

A dense pattern of nonzero matrix zones does not directly give a graph minor. A matrix zone merely contains an edge somewhere between two vertex blocks. Those blocks need not induce connected subgraphs, and contracting them as if they were connected would use operations unavailable to graph minors. The proof also needs a vertex order with strong enough structure to control how the relevant connected sets overlap. These are the points that separate the grid-free milestone from a direct application of the matrix grid theorem. Bonnet et al., pp. 3:26–3:29.

The conversion from a mixed-free adjacency matrix to graph twin-width has a second issue: matrix twin-width permits separate row and column contractions, while a graph contraction merges one vertex partition and must keep the two matrix axes synchronized. Theorem 5.8 addresses the graph case. The milestone uses the explicit constant that the paper applies at the end of Theorem 6.3, while the printed Theorem 5.8 states an asymptotic bound. Bonnet et al., pp. 3:22–3:23, 3:29.

Formalization scope

Graphs are finite simple graphs, and twin-width and the number of division parts are natural numbers. The real constants $c_k$ and $f(t)$ are compared with natural-number twin-width through $\lfloor f(t)\rfloor$; the explicit value is positive. Vertex orders are equivalences with $\operatorname{Fin}(n)$. Matrix divisions use strictly increasing cut points, so every part is a nonempty consecutive interval. The adjacency matrix has a zero diagonal because simple graphs have no loops. The graph-minor predicate and the subtree representation come from existing published definitions with the same conventions; graph twin-width and the matrix objects are local draft definitions shared across this mission. Bonnet et al., pp. 3:9, 3:12, 3:17–3:19.

The grid-free milestone holds for every Lex-DFS order, as in the paper, and the existence of such an order is a separate milestone. Lemmas 6.4–6.6 are stated in the proof's context: a DFS, and vertices $a_{i,j}$, $b_{i,j}$ and blocks $B_j$ with exactly the order and adjacency properties the page uses. Lemma 6.5 is posed for every block except the last. As printed it also covers the last block $B_{g(t)/2}$, and for that block it can fail. A five-vertex example satisfies every hypothesis of the lemma and violates the printed conclusion; it is checked in Lean in the sanity file, and the formal item records the change. The theorem's bound is uniform over all finite graphs on the excluded-minor hypothesis. A twin-width definition using an unrestricted real infimum, a sequence that skips directly to one part, red degree counted over homogeneous pairs, or a grid minor over arbitrary noninterval partitions would change the claim. Components and empty graphs use the endpoint conventions stated above. The $k\ge1$ hypothesis in the graph conversion milestone rules out the degenerate zero-division case.

Contributions toward the core grid-free order claim, the symmetric contraction bridge, the component theorem, and the reusable minor and division lemmas are within scope. The running-time claims elsewhere in the paper and the pointer construction and the two $K_{t,t}$-minor constructions inside the proof of Theorem 6.3 are not separate milestones: they are unnumbered and their statements need the pointers. They remain part of the grid-free milestone.

Selected references

• É. Bonnet, E. J. Kim, S. Thomassé, and R. Watrigant, Twin-width I: Tractable FO Model Checking, Journal of the ACM 69(1), Article 3, 2021. DOI:10.1145/3486655.
• A. Marcus and G. Tardos, Excluded permutation matrices and the Stanley–Wilf conjecture, Journal of Combinatorial Theory, Series A 107(1), 153–160, 2004. DOI:10.1016/j.jcta.2004.04.002.
• F. Gavril, The intersection graphs of subtrees in trees are exactly the chordal graphs, Journal of Combinatorial Theory, Series B 16(1), 47–56, 1974. DOI:10.1016/0095-8956(74)90094-X.

Motivation

Many scheduling decisions are not owned by a single decision maker. A machine shared by two departments, a production line serving two customers, or a computing resource shared by two users must process the jobs of two agents, each of which judges a schedule by its own criterion. Agnetis, Mirchandani, Pacciarelli and Pacifici introduced this model in Scheduling Problems with Two Competing Agents (Operations Research, 2004, doi:10.1287/opre.1030.0092), and it became the starting point of the literature on multi-agent scheduling (surveyed in Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal, Multiagent Scheduling, Springer, 2014, doi:10.1007/978-3-642-41880-8).

When neither agent can impose its criterion on the other, the natural object to compute is the set of compromises that cannot be improved for one agent without hurting the other: the Pareto frontier. Section 11 of the paper asks how large that frontier can be for each pair of criteria it studies, because the size of the frontier decides whether it can be listed in polynomial time. This mission formalizes the answer for one agent minimizing its total completion time against the other agent's maximum cost.

Setting

Agent $A$ owns jobs $J^A_1,\dots,J^A_{n_A}$ and agent $B$ owns jobs $J^B_1,\dots,J^B_{n_B}$, with $n_B\ge 1$. Every job $J_j$ has a positive processing time $p_j$, is available at time $0$, and is processed without interruption on a single machine that handles one job at a time. Since both criteria below are nondecreasing in completion times, a schedule $\sigma$ is a sequence of all $n_A+n_B$ jobs processed in that order from time $0$ without idle time, and $C_j(\sigma)$ denotes the completion time of $J_j$.

• Agent $A$ wants to minimize its total completion time $\sum_{h=1}^{n_A} C^A_h(\sigma)$.
• Each $B$-job has a nondecreasing cost function $f^B_k$ of its completion time, and agent $B$ wants to minimize its maximum cost $f^B_{\max}(\sigma)=\max_k f^B_k(C^B_k(\sigma))$.

A schedule $\sigma$ is nondominated if no schedule $\bar\sigma$ has $\sum C^A_h(\bar\sigma)\le\sum C^A_h(\sigma)$ and $f^B_{\max}(\bar\sigma)\le f^B_{\max}(\sigma)$ with at least one inequality strict. Its nondominated pair is $\bigl(\sum C^A_h(\sigma),f^B_{\max}(\sigma)\bigr)$. The constrained problem $1\|\sum C^A_i : f^B_{\max}\le Q$ asks for a schedule with $f^B_k(C^B_k)\le Q$ for every $B$-job that minimizes $\sum C^A_h$ among such schedules; such a schedule is optimal for the bound $Q$.

The $A$-jobs of a schedule follow the SPT order when they appear by nondecreasing processing time, equal lengths in index order. A $B$-job overtakes an $A$-job when it moves from after it to before it.

Formalization targets

Goal: Theorem 11.6, corrected

$$\bigl|\{(\textstyle\sum C^A_h(\sigma),\,f^B_{\max}(\sigma)) : \sigma\ \text{nondominated}\}\bigr|\ \le\ n_A\,n_B+1.$$

The paper prints the bound $n_An_B$. That bound is false: with one job per agent, unit processing times and $f^B(t)=t$, the schedules $AB$ and $BA$ give the two nondominated pairs $(1,2)$ and $(2,1)$. The corrected bound $n_An_B+1$ is the one the printed argument supports.

Milestones

1. Lemma 5.4 (p. 234): if no $B$-job can complete last within the bound, every optimal schedule ends with a longest $A$-job. This is the reason the $A$-jobs of optimal schedules are in SPT order.
2. Lemma 11.4 (p. 240): for $Q'<Q$ and optimal schedules $\sigma,\sigma'$ for $Q$ and $Q'$ whose $A$-jobs follow the SPT order, $C_j(\sigma')\ge C_j(\sigma)$ for every $A$-job $j$.
3. Lemma 11.5 (p. 240): under the same hypotheses, if a $B$-job precedes an $A$-job in $\sigma$, it precedes it also in $\sigma'$.

Significance

A frontier of size at most $n_An_B+1$ means that the scheme the paper calls PP, which solves the constrained problem for a decreasing sequence of bounds, lists every nondominated pair with polynomially many calls to a polynomial algorithm (Theorem 5.5 of the paper). The contrast with the other criteria of §11 is the point: for two total-completion-time agents the paper exhibits an exponential frontier (Example 11.7). The bound therefore separates criteria whose compromises can be negotiated over an explicit list from those where they cannot.

Formalizing it adds three things. First, the printed statements need corrections: the bound is off by one, and Lemmas 11.4 and 11.5 are false when identical $A$-jobs may be ordered differently in the two schedules. A machine-checked version fixes the exact hypotheses. Second, the monotonicity of overtakes (Lemma 11.5) is a reusable structural fact about parametric scheduling under a tightening constraint. Third, no part of this paper or of two-agent scheduling has been machine-checked before, to our knowledge; the published sequence model the mission builds on comes from the formalization of Moore's 1968 algorithm.

Difficulty

The obvious argument counts overtakes: as the bound decreases, each $B$-job overtakes each $A$-job at most once, so consecutive frontier points differ by at least one new overtake. The step that does not go through as printed is "at most once". Optimal schedules for a given bound are not unique, and two optimal schedules can disagree on the order of identical $A$-jobs and on the position of a $B$-job between them. Then an "overtake" can be undone between two bounds without any change in the objectives. The counting is valid only for a consistently chosen family of schedules, and turning the comparison of optimal schedules for two different bounds into a strict improvement needs an exchange argument with careful bookkeeping of which jobs shift. A second, smaller gap is the base case: the first schedule of the chain carries no overtake and must be counted separately.

Formalization scope

Jobs are Fin nA ⊕ Fin nB, 0-based, and a schedule is a duplicate-free list of all jobs; completion times come from the published definition MooreLateJobs.Shared.completionTime (Moore 1968 series), referenced rather than redefined. Processing times are real and strictly positive, the paper's standing convention, which the exchange arguments use. The bound $Q$ is real; the paper's integer $Q$ is a special case. Feasibility for the bound is stated job by job. The maximum cost $f^B_{\max}$ is a finite maximum and requires $n_B\ge 1$.

Explicit readings of the paper's phrases:

• "Nondominated schedules" in Theorem 11.6 is read as nondominated pairs, one schedule per pair, as §11 defines the set it enumerates. Counting schedules would count swaps of identical jobs separately.
• The count is Set.encard of a set of real pairs, so the goal asserts finiteness as well as the bound; it is not a Set.ncard, which would be $0$ on an infinite set.
• "The $A$-jobs are always SPT ordered" (p. 240) is read as the SPT order with ties broken by index, imposed as a hypothesis on both schedules in Lemmas 11.4 and 11.5. Without a fixed tie-break both lemmas are false.
• Lemma 5.4 is restated with $n_A\ge 1$, since an empty schedule has no last job. It is also a milestone of mission 3 of this series and is restated here identically because draft items cannot import each other.

Nothing in the statements is trivial by construction. The goal is about every instance with positive data, its hypotheses are satisfiable, and the counterexample to the printed bound is checked in Lean. The milestones' SPT hypotheses are met by some optimal schedule of every feasible instance, so they are not vacuous. Running times, including the polynomiality of PP and the choice of the decrement $\epsilon$ in Figure 4, are not formalized.

A complete development needs exchange lemmas for single-machine sequences (moving a job, swapping two adjacent jobs, and their effect on completion times), the existence of SPT-ordered optimal schedules, and a chain-counting argument for nested sets of overtakes. The exchange lemmas are reusable for any single-machine sequencing mission. Contributions of any of these, and of a proof of the corrected bound that avoids the scheme PP, are welcome.

Selected references

• A. Agnetis, P. B. Mirchandani, D. Pacciarelli, A. Pacifici, Scheduling Problems with Two Competing Agents, Operations Research 52(2), 229–242, 2004. https://doi.org/10.1287/opre.1030.0092
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1), 102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• A. Agnetis, J.-C. Billaut, S. Gawiejnowicz, D. Pacciarelli, A. Soukhal, Multiagent Scheduling: Models and Algorithms, Springer, 2014. https://doi.org/10.1007/978-3-642-41880-8