Motivation

The weak pentagon problem asks for a five-label structure on the edges of every triangle-free cubic graph. Although its wording resembles proper edge coloring, properness is not part of the conjecture. Instead, each individual color class must meet enough odd cycles that deleting that class leaves a bipartite spanning graph. The problem connects odd-cycle transversals, cut structure, and homomorphisms to a fixed sixteen-vertex graph.

Robert Šámal recorded the conjecture on the Open Problem Garden in 2007. DeVos and Šámal proved that sufficiently high-girth subcubic graphs map to the Clebsch graph, with an explicit girth threshold in their theorem; that does not cover all triangle-free cubic graphs. The mission separates the general existence question from two exact reformulations that can be verified independently.

Setting

Let $G$ be a finite simple triangle-free cubic graph. A five-edge coloring here is any symmetric assignment

It need not be proper or surjective. For a color $i$, delete all edges with label $i$ while retaining every vertex. The coloring is a weak-pentagon coloring when each of the five resulting spanning graphs is bipartite.

Equivalently, each color class is an odd-cycle edge transversal: it meets the edge set of every simple odd cycle. The cycles are not required to be induced. This last distinction matters because an odd cycle may have a chord in the original graph and still survive in a deleted-edge spanning subgraph.

A second representation uses the sixteen four-bit vectors. Two vectors are adjacent when their Hamming distance is three or four. This graph is a model of the Clebsch graph. A graph homomorphism sends every edge of $G$ to an adjacent pair in this target.

Formalization targets

Weak pentagon conjecture

The root target is

No condition is imposed on adjacent edges receiving different labels.

Odd-cycle equivalence

For every fixed graph and fixed five-edge labeling,

This theorem is graph-general: triangle-freeness and cubicity delimit the root but are not needed for the equivalence.

Sixteen-vertex homomorphism formulation

For every finite simple graph $G$,

where $H_{16}$ has vertex set $\{0,1\}^4$ and edges at Hamming distance three or four. The statement concerns existence of some coloring and some homomorphism; it does not preserve an arbitrarily prescribed coloring.

Significance

The root theorem would establish a uniform parity decomposition for all triangle-free cubic graphs. The transversal form makes every odd cycle use all five colors. The homomorphism form replaces edge labels and five separate bipartitions by one bounded vertex certificate, allowing structural and computational methods to share an exact target.

Formalization prevents several nearby but inequivalent conjectures from being conflated. A weak-pentagon coloring can be improper. Checking only induced odd cycles of the original graph is insufficient. Mapping to a five-cycle is stronger and fails even for familiar positive examples. The explicit four-bit model also avoids relying on the name “Clebsch graph” without fixing its adjacency convention.

Difficulty

The equivalences reorganize the problem but do not create the required object. Five odd-cycle transversals must be pairwise compatible as color fibers; finding one small transversal is not enough. Local deletion and gluing methods must preserve existence of a whole homomorphism, not one chosen boundary assignment.

High-girth results leave finitely many short-cycle configurations only when the girth hypothesis is present. Triangle-free graphs may still contain overlapping five- and seven-cycles, and naive local recoloring can repair one odd cycle while breaking another color complement. Minimum-counterexample arguments also require care because deleting vertices preserves subcubicity but not cubicity.

Formalization scope

Colors are Fin 5. The coloring stores a symmetric value on ordered endpoint pairs, with nonedge values ignored. Cubic means every neighbor set has extended cardinality exactly three. A simple odd cycle is a cyclic list of at least three distinct vertices of odd length; it need not be induced. Bipartiteness is witnessed by a Boolean side assignment after one color is deleted.

The sixteen-vertex relation is defined directly on four-bit functions by Hamming distance, so its cardinality and adjacency are not hidden behind an imported graph name. The repository's transversal proof, normalization, and local homomorphism studies are candidate_only; the mission publishes their clean statements as proof obligations. Contributions may close either equivalence, formalize known high-girth results, prove restricted graph classes, or attack the root. A finite benchmark or a failure of one extension strategy is not a counterexample to the conjecture.

Selected references

• R. Šámal, Weak pentagon problem, Open Problem Garden, 2007. https://www.openproblemgarden.org/op/weak_pentagon_problem
• M. DeVos and R. Šámal, High-girth cubic graphs are homomorphic to the Clebsch graph, Journal of Graph Theory 66 (2011), 241–259. https://arxiv.org/abs/math/0602580
• P. Kolman, B. Lidický, and J.-S. Sereni, On Minimum Fair Odd Cycle Transversal, 2010. https://kam.mff.cuni.cz/kamserie/clanky/2010/s956.pdf
• Open Problem Garden / UnsolvedMath, OPG-434. https://www.unsolvedmath.com/problems/OPG-434

Motivation

The dichromatic number of a digraph is the directed analogue of chromatic number: vertices of one color may be adjacent, but each color class must induce an acyclic digraph. The Two Color Conjecture asks whether every orientation of a planar graph has dichromatic number at most two. It is a natural directed-coloring counterpart to planar graph coloring, with the key difference that forbidden monochromatic objects are directed cycles rather than undirected edges.

Critical-digraph theory gives general degree restrictions on minimal counterexamples, and Li and Mohar proved two-colorability under the additional hypothesis that the directed girth is at least four. The unrestricted planar-orientation problem permits directed triangles, so that theorem is a genuine partial result rather than a solution. The project candidate develops the elementary least-order-counterexample consequences needed before any planar structural argument.

Setting

Let $G$ be a finite simple planar graph. An orientation $D$ assigns exactly one direction to every edge of $G$, with no loops, parallel arcs, or pair of opposite arcs. For $X\subseteq V(D)$, the induced digraph $D[X]$ retains every arc whose two endpoints lie in $X$.

A two-coloring is a map

It is valid when both induced digraphs $D[c^{-1}(0)]$ and $D[c^{-1}(1)]$ contain no directed cycle. The color classes need not be independent and either color may be unused.

Planarity belongs to the underlying undirected graph. Lean represents it by an injective straight-line embedding with noncrossing nonincident edges. Directed reachability is reflexive, so a singleton orientation is strongly connected under the usual length-zero convention, although it is also acyclic and hence cannot be a counterexample.

Formalization targets

Two Color Conjecture

The goal is

Disconnected graphs and empty color classes are included.

Least-order counterexample structure

A supporting theorem states that every counterexample of minimum vertex order is nonempty and strongly connected, and its underlying graph has minimum degree at least three:

The minimum is taken over the full class of finite planar orientations, not over one embedding or an arc-minimal subclass.

Semidegree candidate

A stronger open milestone asks whether every vertex of such a least-order counterexample has at least two incoming and at least two outgoing neighbors. This is recorded separately because it is stronger than the degree-three conclusion and its repository proof remains candidate_only.

Significance

The root theorem would establish a universal two-color bound for planar orientations while allowing directed triangles and arbitrary local degree. A counterexample would demonstrate a sharp obstruction specific to directed cycles, not visible to ordinary planar coloring.

The formalized minimal-counterexample package is reusable regardless of the ultimate answer. Strong connectivity permits arguments inside one component, while the degree and semidegree restrictions narrow discharging configurations and finite searches. Encoding the full induced color classes prevents an invalid shortcut in which only a selected acyclic spanning subdigraph is checked.

Difficulty

Deleting a low-degree vertex is safe only if a valid coloring of the smaller graph can be extended without creating a monochromatic directed cycle through the restored vertex. For a chosen color, obstruction depends on both an incoming and an outgoing neighbor of that color together with a directed return path in the old color class. Merely seeing same-colored in- and out-neighbors is not sufficient.

Strongly connected components can be colored separately because their condensation is acyclic, but that observation only reduces a minimal counterexample to one component. Planarity alone does not eliminate directed triangles or the return paths that block both colors. Results assuming directed girth at least four therefore leave the central case untouched.

Formalization scope

A directed graph is a binary relation, coupled to a SimpleGraph by an orientation predicate that requires exactly one direction on every edge and forbids arcs on nonedges. A directed cycle is a cyclic list of at least three distinct vertices. A color class is acyclic when no such list lies entirely in that class. Strong connectivity is nonempty mutual reflexive-transitive reachability.

The least-order predicate quantifies over every smaller finite planar orientation in the same universe. It does not assert that a counterexample exists. Consequently, its structural theorems may be true vacuously if the root conjecture is true; the read-back must expose that conditional form.

Repository arguments, finite tables, and transport receipts are not machine-checked proofs. Contributions may formalize component gluing, exact vertex-extension criteria, degree or semidegree restrictions, planar reducible configurations, or the root. Any stronger minimum-degree claim must remain distinct from the admitted degree-three target until proved.

Selected references

• Open Problem Garden / UnsolvedMath, OPG-169: The Two Color Conjecture. https://www.unsolvedmath.com/problems/OPG-169
• B. Mohar, Eigenvalues and colorings of digraphs, Linear Algebra and its Applications, 2010. https://www.sfu.ca/~mohar/Reprints/Inprint/BM09_LAA09_Mohar_EigenvaluesandColorings.pdf
• Z. Li and B. Mohar, Planar digraphs of digirth four are 2-colourable, Journal of Combinatorial Theory, Series B, 2017. https://arxiv.org/abs/1606.06114

Motivation

Circular coloring refines ordinary vertex coloring by placing colors on a cycle and measuring separation modulo the palette size. It records information that an ordinary chromatic-number bound can lose, and it interacts sharply with planarity, forbidden short cycles, and degree constraints. OPG-401 asks for a specific bound at the intersection of those themes: whether triangle-free planar graphs of maximum degree three always admit a circular coloring of ratio $20/7$.

The question appears on Xuding Zhu's open-problem page and in the Open Problem Garden record. Nearby theorems on fractional coloring do not settle it: fractional chromatic number and circular chromatic number are distinct parameters, so the known fractional bounds for subcubic triangle-free graphs cannot simply be substituted for a circular-coloring proof. Work on circular recoloring likewise studies connectivity between colorings that already exist and does not supply the missing universal existence theorem.

Setting

For integers $p\ge 2q>0$, a $(p,q)$-coloring of a finite simple graph $G$ is a map

such that the shortest cyclic distance between $\varphi(u)$ and $\varphi(v)$ is at least $q$ for every edge $uv$. Equivalently, using representatives in $\{0,\ldots,p-1\}$, the modular difference lies between $q$ and $p-q$, inclusive. The circular chromatic number is the infimum of the ratios $p/q$ for which such a coloring exists.

The root domain consists of all finite simple graphs that are planar, triangle-free, and subcubic. Disconnected and empty graphs are included. Planarity is represented by an injective straight-line drawing with no vertex in the interior of an edge and no intersection between nonincident edges. For finite simple graphs this is the standard straight-line form of planarity.

Formalization targets

Root question

The central target is

This is exactly the claim $\chi_c(G)\le 20/7$ in a form suitable for finite Lean data.

Local extension table

A reusable finite milestone freezes the local palette arithmetic. For $a\in\mathbb Z_{20}$, let $A(a)$ be the colors at cyclic distance at least seven from $a$. For all $a,b$,

This includes equal colors, antipodal colors, tied symmetries, and all twenty residues. It is the exact obstruction encountered when extending a coloring over a deleted degree-two vertex while preserving every old color. The repository artifact supporting this formulation is only candidate_only; the mission publishes the statement as an open formal target rather than claiming it as proved.

Significance

A proof of the root theorem would give the requested sharp circular-coloring guarantee uniformly over a broad planar graph class. It would also separate the circular problem from nearby fractional results by constructing the stronger cyclic palette assignment itself. A counterexample, if one exists, would have to survive the combined restrictions of planarity, triangle-freeness, and maximum degree three, and would identify a genuine boundary for local extension methods.

Formalization adds two concrete assets. First, the cyclic-distance convention is fixed once, avoiding common errors involving directed residues, unrestricted integer lifts, or truncated subtraction. Second, graph reductions can be checked against a precise preservation obligation: deleting a vertex does not help unless the chosen coloring of the smaller graph has compatible boundary colors. The mission therefore welcomes both global structural arguments and verified finite boundary classifications, but finite enumeration alone is not accepted as a proof for arbitrary graph order.

Difficulty

The obvious induction on vertices fails at degree two. A coloring of $G-v$ need not extend over $v$: if its two neighbors receive colors at cyclic distance at least seven, their two allowed sets can be disjoint. The local table characterizes this failure exactly but does not guarantee that a different coloring of $G-v$ has favorable boundary values. Recoloring, reducible configurations, and planar discharging must therefore interact without silently assuming universal extension or connectivity of the recoloring graph.

A second source of difficulty is parameter confusion. Bounds for fractional colorings do not automatically yield $(20,7)$-colorings, and a theorem about mixing existing circular colorings does not prove existence. Any proposed bridge must be stated and verified explicitly.

Formalization scope

Lean represents colors by Fin 20 and uses the minimum of the two directed modular differences as cyclic distance. Edge compatibility includes both the lower bound $7$ and the formal upper bound $13$. Triangle-freeness is literal absence of three mutually cyclic adjacent vertices, and subcubic means every neighbor set has extended cardinality at most three.

The definition bundle contains no theorem and no sorry. Draft theorem items contain exactly one := by sorry. The local candidate computations and GitHub transport records are provenance, not evidence that either theorem is proved. A complete contribution may formalize the finite palette table, a faithful reducible configuration, a recoloring lemma with all quantifiers exposed, or the root theorem. Every claimed universal reduction must retain finiteness, simplicity, planarity, triangle-freeness, and the degree bound.

Selected references

• X. Zhu, Circular chromatic number of triangle-free planar graphs with maximum degree three, open-problem page. https://www.math.nsysu.edu.tw/~zhu/open-problems/chic-k3free-planar.htm
• Open Problem Garden, OPG-401. https://www.unsolvedmath.com/problems/OPG-401
• X. Zhu, The fractional version of Hedetniemi's conjecture is true, European Journal of Combinatorics, 2011. https://doi.org/10.1016/j.ejc.2011.03.004
• Z. Dvořák, J.-S. Sereni, and J. Volec, Subcubic triangle-free graphs have fractional chromatic number at most 14/5, Journal of the London Mathematical Society, 2014. https://arxiv.org/abs/1301.5296

Motivation

A star edge coloring is a proper edge coloring with an additional local restriction: no path or cycle of four edges may use only two colors. It sits between ordinary proper edge coloring and strong edge coloring. The problem is local enough to admit finite obstruction searches, but global enough that independently valid local colorings may fail to fit together.

Dvořák, Mohar, and Šámal proved in 2013 that every subcubic multigraph has a star edge coloring with seven colors and conjectured that six always suffice. The Open Problem Garden records the simple-graph version as OPG-37271. The value six would be best possible because the complete bipartite graph $K_{3,3}$ has star chromatic index six.

Subsequent work has proved the six-color bound under additional hypotheses. Lei, Shi, and Song proved it for subcubic multigraphs with maximum average degree less than $5/2$ and obtained a five-color result below $24/11$. Casselgren, Granholm, and Raspaud proved the conjecture for cubic Halin graphs and several bipartite families. These results leave the unrestricted finite subcubic case as the target of this mission.

Setting

Let $G$ be a finite simple undirected graph. An edge coloring assigns to each unordered edge of $G$ one color from a finite palette. It is proper if two distinct edges incident with the same vertex always have different colors.

A simple path of four edges has five pairwise distinct vertices $v_0,v_1,v_2,v_3,v_4$ and consecutive edges $v_0v_1,v_1v_2,v_2v_3,v_3v_4$. It is bichromatic in a proper coloring exactly when the first and third edges have the same color and the second and fourth edges have the same color. The path need not be induced: additional chords do not remove it. A four-cycle has four pairwise distinct vertices and is bichromatic under the analogous alternating equalities, including the closing edge.

A coloring is a star edge coloring when it is proper and contains neither type of bichromatic four-edge configuration. The star chromatic index $\chi'_s(G)$ is the least palette size admitting such a coloring. A graph is subcubic when every vertex has at most three neighbors.

Formalization targets

Goal — the six-color conjecture

The main target is the exact OPG-37271 assertion for finite simple graphs:

In the Lean statement, this is expressed directly as the existence of a coloring by Fin 6; no separate minimization operator is needed.

Known upper bound

The first literature milestone is the established seven-color theorem:

Formalizing this result provides a checked baseline and infrastructure that a six-color argument can reuse.

Sharpness at $K_{3,3}$

The second literature milestone records both sides of the exact value

Thus the mission cannot be completed by weakening the goal to a larger universal constant.

Significance

A proof would determine the universal star chromatic-index bound for graphs of maximum degree three and would match the known lower-bound example $K_{3,3}$. A counterexample, if one exists, would separate six from the established seven-color bound and identify the first genuinely seven-chromatic subcubic graph.

The formalization contributes a reusable definition of star edge coloring on Mathlib finite simple graphs. In particular, it fixes several conventions that are easy to blur in informal or computational work: forbidden paths have four edges rather than four vertices; they are simple but need not be induced; four-cycles are checked separately; and properness is not inferred merely from the absence of an alternating four-edge pattern. These definitions can support certified bounded searches, verified coloring certificates, and later formalizations of sparse or planar special cases.

The current research repository contains candidate-only local extension criteria and finite certificates. They may motivate future milestones, but they are not treated here as proofs of the conjecture, as admitted evidence, or as replacements for the literature milestones.

Difficulty

A direct greedy coloring argument can fail at a newly inserted edge because a color may be forbidden either by an adjacent edge or by a bichromatic four-edge path created several incidences away. Deleting a low-degree vertex and coloring the remaining graph therefore does not guarantee that the old coloring extends without recoloring. Explicit small configurations already witness failure of this zero-recoloring strategy while remaining globally six-colorable.

The known seven-color proof has one extra color available to break such interactions. Reaching six requires coordinating local recolorings or extracting stronger structure from a minimal counterexample. Finite searches can test configurations and produce certificates, but bounded verification alone cannot establish the universal quantifier over all finite graphs.

Formalization scope

The mission uses SimpleGraph with an arbitrary finite vertex type. Edges are unordered edge-set elements, and palettes are the labeled finite types Fin k. The graph need not be connected, cubic, planar, or nonempty; isolated vertices and the empty graph are included. “Subcubic” means degree at most three, not degree exactly three.

A forbidden path is represented by five pairwise distinct vertices and four consecutive adjacencies. It is not required to be induced. A forbidden cycle is represented separately by four pairwise distinct vertices and four cyclic adjacencies. Under the properness hypothesis, equality of opposite edge colors is precisely the bichromatic alternating pattern.

A complete development should supply the known seven-color theorem, certify the exact value for $K_{3,3}$, and then address the six-color goal. Contributions formalizing faithful special cases or reusable extension lemmas are welcome, but sampled graph families and successful SAT searches remain finite evidence unless converted into a general Lean proof.

Selected references

• Z. Dvořák, B. Mohar, and R. Šámal, Star chromatic index, Journal of Graph Theory 72 (2013), 313–326. arXiv:1011.3376
• H. Lei, Y. Shi, and Z.-X. Song, Star chromatic index of subcubic multigraphs, Journal of Graph Theory 88 (2018), 566–576. arXiv:1701.04105
• C. J. Casselgren, J. B. Granholm, and A. Raspaud, On star edge colorings of bipartite and subcubic graphs, Discrete Applied Mathematics 298 (2021), 21–33. arXiv:1912.02467
• Open Problem Garden, Star chromatic index of subcubic graphs, OPG-37271. Problem page
• Vibe Mathing candidate repository, OPG-37271 star chromatic index of subcubic graphs, candidate-only artifacts at commit ddc49c1978a196490702150bb75264793a658457. Repository

That the prime numbers, thinning out as they climb yet never quite vanishing, should nonetheless contain arithmetic progressions of every finite length is one of the most celebrated discoveries of twenty-first-century mathematics. Ben Green and Terence Tao proved it in 2004 (published in the Annals of Mathematics in 2008), resolving a question whose roots reach back to Lagrange and Waring around 1770 and which had crystallized in the Erdős–Turán conjecture. The primes have density zero, so Szemerédi's theorem — which guarantees long progressions only in positive-density sets — does not apply directly; the genius of the proof was a transference principle extending Szemerédi's theorem to sets sitting densely inside a 'pseudorandom' host, built from the sieve ideas of Goldston, Pintz, and Yıldırım. The result was a centerpiece of the citation for Tao's 2006 Fields Medal and opened a whole industry, including the Tao–Ziegler extension to polynomial progressions. Unusually for a headline problem, this theorem is already proved — which makes it an ideal flagship formalization mission: a deep, decomposable argument whose pieces, from Szemerédi's theorem to the transference principle, the community can rebuild and verify in Lean.

Motivation

Vertex connectivity measures how robust a network is against the failure of nodes. It can be measured in two ways that look different. One way counts the fewest nodes whose removal disconnects the network. The other counts the routes between two nodes that share no intermediate node. Whitney's theorem (1932) says that the two measures agree for every pair of nodes. It is the vertex form of Menger's theorem, and it underlies reliability analysis of communication and transportation networks, the design of fault-tolerant routing, and much of structural graph theory.

M. L. Balinski's 1961 paper On the graph structure of convex polyhedra in n-space proves that the graph of a bounded full-dimensional polyhedron in $n$-space is $n$-tuply connected (the subject of Mission I of this series). It then invokes Whitney's theorem to conclude that any two vertices of such a polyhedron are joined by $n$ disjoint paths. Balinski gives a short new proof of Whitney's theorem through the max-flow min-cut theorem of Ford and Fulkerson and of Dantzig and Fulkerson. That makes the theorem a consequence of linear programming duality. This mission formalizes that part of the paper: the network vocabulary, the max-flow min-cut theorem with capacities on both points and lines, the integrality of maximum flows, and Whitney's theorem itself.

Timeline.

• 1927: Menger states the disjoint-paths theorem for separating sets.
• 1932: Whitney proves the characterization of $n$-connected graphs by $n$ disjoint paths between every pair of points.
• 1956: Ford and Fulkerson and Dantzig and Fulkerson prove the max-flow min-cut theorem.
• 1961: Balinski derives Whitney's theorem from it with a unit-capacity network.

Setting

A graph $G$ consists of a finite set $V$ of points and a set of lines, each line being a pair of distinct points. A path from $p_s$ to $p_k$ is a sequence of lines $(p_1,p_2),(p_2,p_3),\dots,(p_m,p_{m+1})$ with $p_1 = p_s$, $p_{m+1} = p_k$ and $m \ge 1$. Paths are disjoint if they have no point in common except possibly their first and last points.

$G$ is $n$-tuply connected if it has at least $n+1$ points and, for every set $X$ of fewer than $n$ points, the graph $G - X$ remaining after deleting $X$ is connected. $G$ has $n$ disjoint paths from $p_s$ to $p_k$ if there are $n$ pairwise distinct paths from $p_s$ to $p_k$, none of which repeats a point, and no two of which share a point other than $p_s$ and $p_k$.

A network is a connected graph with a capacity $c(x) \ge 0$ on every point and $c(e) \ge 0$ on every line, and with a distinguished source $p_s$ and sink $p_k$. A flow assigns a number $f(C) \ge 0$ to every path $C$ from $p_s$ to $p_k$, such that for every point $x$ and every line $e$

Its value is $\operatorname{val}(f) = \sum_C f(C)$. A disconnecting set is a pair $(X,F)$ of points and lines that meets every walk from $p_s$ to $p_k$. Its value is $\sum_{x\in X} c(x) + \sum_{e \in F} c(e)$.

The unit network of the proof has capacity $1$ on every point except $p_s$ and $p_k$, and capacity $n+1$ on every line except the line $p_sp_k$ (if present), which has capacity $1$. In Lean these are IsNTuplyConnected, HasNDisjointPaths, IsFlow, flowValue, IsDisconnecting, cutValue, unitCapV and unitCapE, all in the namespace Balinski61.Whitney.

Formalization targets

Goal: Whitney's theorem (p. 434)

For a finite graph $G$ with at least two points and any $n \ge 0$:

Both directions are part of the goal.

Milestones, in the order of the proof

1. Max-flow min-cut (p. 433). In every network there is a number $M$ that is the value of some flow and of some disconnecting set, with every flow of value at most $M$ and every disconnecting set of value at least $M$.
2. Integrality (p. 434). If all capacities are integers, some maximum flow has only integer path flows.
3. Min-cut in the unit network (p. 434). If $G$ is $n$-tuply connected and $p_s \ne p_k$, every disconnecting set of the unit network has value at least $n$.
4. Paths from unit flows (p. 434). An integral flow of value at least $n$ in the unit network yields $n$ disjoint paths from $p_s$ to $p_k$.
5. Sufficiency (p. 434). If every pair of distinct points is joined by $n$ disjoint paths, $G$ is $n$-tuply connected.

Significance

Whitney's theorem turns a statement about all small deletion sets into the existence of explicit, verifiable path systems, and back again. In applications it certifies connectivity by exhibiting paths, and it certifies that connectivity is no larger by exhibiting a separating set. It is the base of the theory of $k$-connected graphs: ear decompositions, the fan lemma, and the structure of minimally $k$-connected graphs all use it. Inside this paper it supplies the COROLLARY that any two vertices of a bounded full-dimensional polyhedron in $n$-space are joined by $n$ disjoint edge paths.

None of these results is formalized for vertex connectivity at this Mathlib revision. Mathlib has edge connectivity and connected components but no vertex Menger theorem. The Prove2Me library has max-flow min-cut statements for arc capacities only and integrality results for basic solutions of network LPs, but no flow model with capacities on points. A completed development gives a reusable vertex-capacitated max-flow min-cut theorem for undirected graphs and the first machine-checked Whitney theorem in this library. The results are classical and proved; the remaining work is the formalization.

Difficulty

The sufficiency direction is elementary. The necessity direction needs a global object (a flow, or a family of paths) to exist from purely local hypotheses about deletions. The obvious induction on $n$, which deletes a point and applies the hypothesis to a smaller graph, does not keep the path systems disjoint. In Balinski's route the weight falls on max-flow min-cut and integrality for path flows with capacities on points, neither of which exists in the library. A second difficulty sits in a case the paper's proof skips: a disconnecting set of the unit network may use the line $p_sp_k$ (capacity $1$) together with up to $n-2$ points, and the deletion hypothesis of $n$-tuple connectedness speaks only about points.

Formalization scope

Graphs are Mathlib SimpleGraphs on a Fintype with decidable equality and adjacency. Paths are walks with IsPath. A flow is a real function on the finite type G.Path ps pk of simple paths; "through a point" and "through a line" mean membership in the walk's support and edge list. Capacities are functions V → ℝ and Sym2 V → ℝ. Nonnegativity, connectivity of $G$ and $p_s \ne p_k$ are hypotheses of the network theorems.

The following readings of loose phrases are explicit in the statements:

• "dropping out $n-1$ or fewer points" is $|X| < n$;
• "$n$ disjoint paths" means $n$ pairwise distinct simple paths. The printed path syntax permits repeated vertices; in a graph with lines $p_s a$, $p_s b$, and $p_s p_k$, the distinct walks $p_s,a,p_s,p_k$ and $p_s,b,p_s,p_k$ share only their endpoints even though the graph is not $2$-tuply connected. The theorem therefore uses its conventional simple-path reading;
• path flows live on simple paths (merging and shortcutting changes no maximum value);
• the paper leaves the capacities of $p_s$ and $p_k$ in the unit network unassigned, and here they are $n+1$;
• "the condition is sufficient is obvious" is the full statement that $n$-tuple connectedness follows;
• the hypothesis $|V| \ge 2$ is added to the goal and to sufficiency, because the paper's "any pair of points" presupposes it and the equivalence fails for a one-point graph.

The max-flow min-cut milestone states that the maximum and the minimum are attained. A statement that only bounds some flow by every cut is satisfied by the zero flow. A connectivity notion without the $n+1$ point count would make every complete graph $n$-connected for all $n$. Both trivializations are excluded.

Contributions welcome: a vertex-capacitated augmenting-path or LP-duality proof of max-flow min-cut for path flows, integrality by an augmenting-path argument, the unit-network lemmas, and direct combinatorial proofs of Whitney's theorem that bypass flows.

Selected references

• M. L. Balinski, On the graph structure of convex polyhedra in n-space, Pacific J. Math. 11 (1961), 431–434. https://doi.org/10.2140/pjm.1961.11.431
• H. Whitney, Congruent graphs and the connectivity of graphs, Amer. J. Math. 54 (1932), 150–168. https://doi.org/10.2307/2371086
• L. R. Ford, Jr. and D. R. Fulkerson, Maximal flow through a network, Canadian J. Math. 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
• G. B. Dantzig and D. R. Fulkerson, On the max-flow min-cut theorem of networks, in Linear Inequalities and Related Systems, Ann. of Math. Stud. 38, Princeton Univ. Press, 1956, 215–221. https://doi.org/10.1515/9781400881987
• K. Menger, Zur allgemeinen Kurventheorie, Fund. Math. 10 (1927), 96–115. https://doi.org/10.4064/fm-10-1-96-115

Motivation

In binary classification the VC dimension decides PAC learnability: a class of $\{0,1\}$-valued functions is learnable from finitely many examples exactly when its VC dimension is finite. Multiclass classification, where a predictor outputs one of many labels, arises whenever the label set is large: language models choosing a next token, image recognition over open vocabularies, structured prediction. For finitely many labels the Natarajan dimension plays the role of the VC dimension (Natarajan 1989; Ben-David, Cesa-Bianchi, Haussler and Long 1995). Whether it still characterizes learnability when the label set is infinite stayed open for three decades.

Brukhim, Carmon, Dinur, Moran and Yehudayoff (arXiv:2203.01550, FOCS 2022) settled both directions. Their Theorem A shows that the DS dimension of Daniely and Shalev-Shwartz (COLT 2014, PMLR 35) characterizes multiclass PAC learnability for every label set. Their Theorem 2, the goal of this mission, shows that the Natarajan dimension does not: there is a class whose Natarajan dimension is $1$ and whose DS dimension is infinite.

Timeline:

• 1989: Natarajan introduces his dimension and proves it gives sample-complexity bounds when the label set is finite.
• 1995: Ben-David, Cesa-Bianchi, Haussler and Long show that, for finite label sets, every "reasonable" extension of the VC dimension characterizes learnability.
• 2003: Januszkiewicz and Świątkowski construct, for every dimension, finite simplicial complexes without empty squares from coset complexes of finite groups (Comment. Math. Helv. 78(3), 555–583); the multiclass paper uses this construction for its separation.
• 2014: Daniely and Shalev-Shwartz introduce the DS dimension, prove that finite DS dimension is necessary for learnability, and ask whether it is sufficient.
• 2022: Brukhim et al. prove that finite DS dimension is sufficient and that the Natarajan dimension fails to characterize learnability for infinite label sets.

Setting

A concept class is a set $\mathcal H \subseteq \mathcal Y^{\mathcal X}$ of functions from a domain $\mathcal X$ to a label set $\mathcal Y$, with no finiteness assumption on either. For a sequence $S = (x_1, \dots, x_n) \in \mathcal X^n$, the projection $\mathcal H|_S \subseteq \mathcal Y^n$ is the set of words $(h(x_1), \dots, h(x_n))$, $h \in \mathcal H$.

• $S$ is N-shattered if there are $f, g : [n] \to \mathcal Y$ with $f(i) \ne g(i)$ for every $i$ and $\mathcal H|_S \supseteq \{f(1), g(1)\} \times \dots \times \{f(n), g(n)\}$: the projection contains a copy of the Boolean cube. The Natarajan dimension $d_N(\mathcal H)$ is the largest $n$ for which some $S \in \mathcal X^n$ is N-shattered, or $\infty$.
• A pseudo-cube of dimension $d$ is a non-empty, finite $B \subseteq \mathcal Y^d$ in which every word $h$ has, for every coordinate $i$, an $i$-neighbour: a word $g \in B$ with $g(i) \ne h(i)$ and $g(j) = h(j)$ for $j \ne i$. $S$ is DS-shattered if $\mathcal H|_S$ contains an $n$-dimensional pseudo-cube, and the DS dimension $d_{DS}(\mathcal H)$ is the largest such $n$, or $\infty$.

Every Boolean cube is a pseudo-cube, so $d_N \le d_{DS}$. The hexagon $\{12, 32, 34, 54, 56, 16\} \subseteq \{1,\dots,6\}^2$ is a 2-dimensional pseudo-cube that contains no Boolean square.

The milestones pass through simplicial complexes: downward-closed families of finite sets. A complex is good if it is finite, pure, has a proper coloring $r$ of its vertices with $\dim(C)+1$ colors, and satisfies replacement (every vertex of every face can be exchanged for a new vertex). A good complex $C$ with coloring $r$ defines the class $B(C, r)$ of its top faces, each written as the word listing its vertices by color. A square is a 4-cycle of distinct vertices in the 1-skeleton; it is empty if neither diagonal is an edge. The coset complex $C_F(H_1, \dots, H_d)$ of subgroups of a group $F$ has the cosets $gH_i$ as vertices and the sets of cosets with a common point as faces.

Formalization targets

Goal: Theorem 2 (p. 4)

Milestones

1. Theorem 45 (p. 30; Januszkiewicz–Świątkowski): for every $d > 1$ a finite group $F$ and subgroups $H_1, \dots, H_d$ with $(\bigcap_{j\ne i} H_j) \setminus H_i \ne \emptyset$ for all $i$, whose coset complex has no empty squares.
2. Proposition 46 (p. 31): such a coset complex has dimension $d - 1$, is good and has no empty squares.
3. Proposition 42 (p. 28): a $d$-dimensional good complex with a proper coloring $r$ yields the $(d+1)$-dimensional pseudo-cube $B(C, r)$; conversely every pseudo-cube yields a good complex $C(B)$.
4. Proposition 43 (p. 29): $d_N(B(C,r)) \ge 2$ iff $C$ has a square $v_0 v_1 v_2 v_3$ with $r(v_0) = r(v_2)$ and $r(v_1) = r(v_3)$.
5. Corollary 44 (p. 29): a good complex without empty squares gives $d_N(B(C, r)) \le 1$ for every proper coloring.
6. Proof of Theorem 2 (p. 32): for every $d \ge 1$, a $d$-dimensional pseudo-cube with Natarajan dimension exactly $1$.

Significance

Theorem 2 shows that the classical generalization of the VC dimension to many labels is the wrong invariant once the label set is infinite: a class can contain no Boolean square at all and still be unlearnable, because it contains pseudo-cubes of every dimension. Combined with the necessity of finite DS dimension, it gives a class that is not PAC learnable although its Natarajan dimension is $1$, and it identifies pseudo-cubes, not Boolean cubes, as the relevant combinatorial obstruction. It also links learning theory to a problem studied in geometric group theory, finite "flag-no-square" complexes.

The paper's proof is complete modulo Theorem 45, which it imports from Januszkiewicz–Świątkowski 2003. None of these results is formalized. A formalization would give machine-checked versions of the dictionary between concept classes and properly colored complexes (Propositions 42–44), of the coset-complex translation (Proposition 46), and of the final disjoint-union argument; Theorem 45 itself, which rests on Coxeter-group and topological arguments, is a separate and substantial formalization target.

Difficulty

Infinite complexes that are pure, properly colored, satisfy replacement and have no empty squares are easy to build: grow a tree of faces indefinitely. The definition of a pseudo-cube demands finiteness, and the difficulty is entirely there: one must "fold" such an infinite object into a finite one without creating an empty square. The obvious finite candidate, the group $(\mathbb Z/2)^d$ with its coordinate subgroups, produces the Boolean cube, whose complex is full of empty squares. Theorem 45 is the input that resolves this, and it is far beyond the rest of the argument.

Formalization scope

All declarations live in the namespace MulticlassDS.NatGap.

• Concept classes are Set (X → Y) with arbitrary types; $[n]$ is Fin n (0-based), and shattering is defined for sequences Fin n → X, as in the paper.
• Both dimensions are ℕ∞-valued suprema, so "infinite DS dimension" is dsDim H = ⊤. An ℕ-valued supremum would silently return $0$ on an unbounded family and would trivialize the goal.
• The goal requires the Natarajan dimension to be exactly $1$; an upper bound alone holds for any class with at most one element.
• Pseudo-cubes are required to be finite (Definition 5). Without finiteness, the tree classes of Example 8 would already have infinite "DS dimension".
• Complexes are Set (Finset V). The dimension is the predicate HasDim C d, not a natural-number subtraction, and colors are Fin (d + 1).
• Replacement is stated with a new vertex $u \notin f$. The page writes "$u \ne v$", but read literally that allows $u \in f$, which makes the condition hold by downward closure and makes Proposition 42 false; the proofs of Propositions 42 and 46 use a new vertex.
• Coset-complex vertices are left cosets as subsets of the group, not pairs (index, coset).
• Proposition 46 states dimension $d - 1$ under $d > 1$, where the subtraction is exact; the converse of Proposition 42 is indexed by $d + 1$ and $d$ to avoid it.
• The proof-of-Theorem-2 milestone says "for every $d$"; it is posed for $d \ge 1$, because at $d = 0$ the only pseudo-cube has Natarajan dimension $0$.

Welcome contributions: proofs of Propositions 42–44 and 46 and of the goal from the milestones, which need only finite combinatorics and elementary group theory; and, separately, a formalization of the Januszkiewicz–Świątkowski construction behind Theorem 45. The definitions of pseudo-cubes, the DS dimension and good complexes are reusable by the companion mission on sample compression and by any later work on multiclass learnability.

Selected references

• N. Brukhim, D. Carmon, I. Dinur, S. Moran, A. Yehudayoff, A Characterization of Multiclass Learnability, arXiv:2203.01550v1, 2022 (FOCS 2022). https://arxiv.org/abs/2203.01550
• T. Januszkiewicz, J. Świątkowski, Hyperbolic Coxeter groups of large dimension, Comment. Math. Helv. 78(3) (2003), 555–583 (reference [Januszkiewicz and Świątkowski 2003] of arXiv:2203.01550v1, p. 33).
• A. Daniely, S. Shalev-Shwartz, Optimal learners for multiclass problems, COLT 2014, PMLR 35, 287–316. https://proceedings.mlr.press/v35/
• B. K. Natarajan, On learning sets and functions, Machine Learning 4 (1989), 67–97. https://doi.org/10.1007/BF00114804
• S. Ben-David, N. Cesa-Bianchi, D. Haussler, P. M. Long, Characterizations of learnability for classes of {0,…,n}-valued functions, J. Comput. Syst. Sci. 50(1) (1995), 74–86. https://doi.org/10.1006/jcss.1995.1008

Motivation

In multiclass classification a learner sees examples $(x, y)$ with $x$ in a domain $\mathcal X$ and a label $y$ in a set $\mathcal Y$, and must predict labels of new points. When $\mathcal Y$ is finite, the Natarajan dimension characterizes PAC learnability, extending the role of the VC dimension in binary classification (Natarajan 1989; Ben-David, Cesa-Bianchi, Haussler, Long 1995). Label sets in practice are often unbounded: structured prediction, ranking, and language modelling all predict from very large or infinite label spaces. For infinite $\mathcal Y$ the Natarajan dimension fails to characterize learnability, and the question of which combinatorial parameter does was left open by Daniely and Shalev-Shwartz.

Timeline:

• 1989–1995. Natarajan, then Ben-David et al. and Haussler–Long: for finite $\mathcal Y$, learnability is equivalent to finite Natarajan dimension, with sample complexity depending on $\log|\mathcal Y|$.
• 2011–2015. Daniely, Sabato, Ben-David and Shalev-Shwartz show that ERM can fail for multiclass problems with many labels. Daniely and Shalev-Shwartz (COLT 2014) introduce the DS dimension, prove that finite DS dimension is necessary for learnability, and ask whether it is sufficient.
• 2022. Brukhim, Carmon, Dinur, Moran, Yehudayoff prove sufficiency, so the DS dimension characterizes multiclass PAC learnability, and show that the Natarajan dimension does not.

Setting

A concept class is a set $\mathcal H\subseteq\mathcal Y^{\mathcal X}$ of functions. For a sequence $S=(x_1,\dots,x_n)$ the projection $\mathcal H|_S\subseteq\mathcal Y^n$ is the set of label words $(h(x_1),\dots,h(x_n))$, $h\in\mathcal H$. A finite non-empty set $B\subseteq\mathcal Y^d$ is a pseudo-cube if every $h\in B$ has, in every coordinate $i$, a neighbour $g\in B$ that differs from $h$ exactly in coordinate $i$. The sequence $S$ is DS-shattered if $\mathcal H|_S$ contains an $n$-dimensional pseudo-cube, and the DS dimension $d_{DS}(\mathcal H)$ is the maximum length of a DS-shattered sequence. The Natarajan dimension $d_N(\mathcal H)\le d_{DS}(\mathcal H)$ is the same with Boolean cubes $\prod_i\{f(i),g(i)\}$, $f(i)\ne g(i)$, in place of pseudo-cubes.

A sample $S\in(\mathcal X\times\mathcal Y)^n$ is $\mathcal H$-realizable if some $h\in\mathcal H$ is consistent with it. An $n\to r$ sample compression scheme for $\mathcal H$ (Littlestone and Warmuth 1986) is a single reconstruction function $\rho:(\mathcal X\times\mathcal Y)^r\to\mathcal Y^{\mathcal X}$ such that every realizable sample of size $n$ contains $r$ of its examples $S'$ with $\rho(S')$ consistent with the whole sample. Logarithms are base $2$ throughout.

Formalization targets

Goal: Theorem 36 (p. 22)

For $\mathcal H$ with $d_{DS}(\mathcal H)=d_{DS}<\infty$ and $d_N(\mathcal H)=d_N$, and all integers $n,t>0$, there is an $n\to r$ sample compression scheme, $r\le n$, with

Milestones

The scheme combines two components, each with its own chain of results:

• List learning from the DS dimension. Lemma 13 (orientations of out-degree $\le d$ on $\mathcal Y^{d+1}$), Claim 16 (the one-inclusion algorithm is right on some leave-one-out example), Fact 14 (leave-one-out symmetrization), Proposition 32 (a list PAC learner with list size $\binom{d+t}{t}$ and success probability $\frac{t+1}{d+t+1}$), Lemma 39 (an $n\to r_1$ list compression scheme with $r_1\le\frac{d_{DS}+t+1}{t+1}(d_{DS}+t)\log(2n)$ and menu size $\le\binom{d_{DS}+t+1}{t+1}\log(2n)$).
• Learning from a menu via shifting. Claim 22, Corollary 23, Claim 26, Proposition 27 ($\operatorname{avd}\le4d_E$), Corollary 28, Lemma 29 ($d_E\le5d_N\log p$), Lemma 17 (orientations of out-degree $\le20d_N\log p$ on $[p]^n$), Proposition 34 (error $\le20d_N\log(p)/n$ given a $p$-menu), Lemma 40 (an $n\to r_2$ compression scheme given a $p$-menu with $r_2\le10^3d_N\log(p)\log(2n)$).

Significance

Theorem 36 is the algorithmic heart of the characterization: by the standard "compression implies generalization" argument it gives PAC learnability of every class of finite DS dimension, with sample complexity $\tilde O(d_{DS}^{3/2}/\epsilon)$ in the realizable case ($t=\lceil d_{DS}^{1/2}\rceil$), and with the agnostic case following by known reductions. It also exhibits sample compression schemes of size polylogarithmic in $n$ for multiclass classes with infinitely many labels, in contrast to the constant-size schemes known for finite VC classes.

The result is proved in the paper; none of it is formalized. The formalization would produce a machine-checked theory of one-inclusion graphs and their orientations, multiclass shifting, the exponential dimension, list learning, and sample compression schemes for arbitrary label sets. These objects recur throughout learning theory (one-inclusion graphs in optimal PAC learning, shifting in VC theory), so the infrastructure is reusable beyond this mission.

Difficulty

The natural first idea, running empirical risk minimization or bounding the Natarajan dimension, fails: classes with Natarajan dimension $1$ and infinitely many labels can be unlearnable, and ERM can fail even for learnable classes. The DS dimension gives only a weak guarantee: by Claim 16, among $d+1$ leave-one-out runs, one is correct. Turning this into a learner requires a list learner whose menus are still of unbounded total size, and then learning with a menu of size $p$, where the obstacle is controlling one-inclusion graph orientations over $[p]^n$ by the Natarajan dimension. Multiclass shifting does not preserve the average degree (Example 20), so the binary argument breaks down, and a new potential ($\operatorname{avd}'$) and a new dimension ($d_E$) are needed. Lemma 13 for infinite classes needs a compactness argument.

Formalization scope

Lean conventions:

• A class is H : Set (X → Y) with arbitrary types X, Y; sequences and samples are functions on Fin n ($[n]$ is 0-based).
• The DS, Natarajan and exponential dimensions are suprema in ℕ∞, so unbounded families give ⊤; hypotheses are written dsDim H = dDS with dDS : ℕ. A pseudo-cube is required to be finite.
• Logarithms are Real.logb 2. Menu sizes use Set.encard.
• A compression scheme is a reconstruction function fixed before the sample (∃ ρ, ∀ S, ∃ S'); a subsample may repeat and reorder examples. Theorem 36 states $r\le n$ explicitly.
• Orientations of the one-inclusion graph of $V\subseteq\mathcal Y^m$ are maps sending a direction $i$ and a vertex $v$ to the head of the edge of direction $i$ through $v$; the out-degree of $v$ counts directions whose head is not $v$.
• Classes over $[p]$ use labels Fin p; the shifting condition $1\le g(i)\le|e_f|$ becomes $g(i)<|e_f|$.
• The one-inclusion algorithm (Algorithms 1 and 3) is parametrized by a permutation-equivariant choice of minimal orientations, the reading under which the paper's leave-one-out proofs are valid; statements about the algorithm hold for every such choice. Its default output on non-realizable input requires a non-empty label set, assumed in Claim 16 and Propositions 32 and 34. Lemma 40 assumes a non-empty label set because it is false for $\mathcal X\ne\emptyset=\mathcal Y$.
• Distributions are discrete (PMF), and i.i.d. probabilities are sums over $\mathcal Z^m$. The measure-theoretic generality of the paper is not attempted.

A trivial formalization is ruled out by these choices. Placing the reconstruction function after the sample would let it output the consistent hypothesis. A dimension in ℕ defined by sSup would be $0$ for infinite dimension. Pseudo-cubes without finiteness would change the dimension (Example 8).

Contributions welcome: proofs of any milestone, in particular the shifting results of §3 (self-contained combinatorics on finite classes), Fact 14 (pure discrete probability), and Lemma 13; general-purpose lemmas about one-inclusion graphs, orientations and sample compression schemes are reusable by other learning-theory missions.

Selected references

• N. Brukhim, D. Carmon, I. Dinur, S. Moran, A. Yehudayoff, A Characterization of Multiclass Learnability, FOCS 2022; arXiv:2203.01550v1 (2022). https://arxiv.org/abs/2203.01550
• A. Daniely, S. Shalev-Shwartz, Optimal Learners for Multiclass Problems, COLT 2014. https://arxiv.org/abs/1405.2690
• N. Littlestone, M. Warmuth, Relating Data Compression and Learnability, unpublished technical report, University of California, Santa Cruz, 1986 (no stable link).
• D. Haussler, N. Littlestone, M. Warmuth, Predicting {0,1}-Functions on Randomly Drawn Points, Information and Computation 115(2), 1994. https://doi.org/10.1006/inco.1994.1097
• D. Haussler, P. M. Long, A Generalization of Sauer's Lemma, Journal of Combinatorial Theory, Series A 71(2), 1995. https://doi.org/10.1016/0097-3165(95)90006-3
• S. Ben-David, N. Cesa-Bianchi, D. Haussler, P. M. Long, Characterizations of Learnability for Classes of {0,…,n}-Valued Functions, JCSS 50(1), 1995. https://doi.org/10.1006/jcss.1995.1008
• B. K. Natarajan, On Learning Sets and Functions, Machine Learning 4, 1989. https://doi.org/10.1007/BF00114804

Motivation

The problem $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ asks for a single-machine sequence of jobs, respecting precedence constraints, that minimizes the weighted sum of completion times. It has been known to be strongly NP-hard since Lawler (1978) and Lenstra and Rinnooy Kan (1978), several different 2-approximation algorithms are known, and closing the approximability gap is listed by Schuurman and Woeginger (1999) as one of ten outstanding open problems in scheduling theory. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) give the first inapproximability result for this problem: under a widely believed complexity assumption it has no polynomial-time approximation scheme (PTAS). The bridge to that result is a quantitative link, Lemma 9.1, between the optimal value of a special bipartite scheduling instance and the maximum edge biclique of a bipartite graph, a problem whose hardness of approximation was established by Ambühl, Mastrolilli and Svensson (FOCS 2007). This mission formalizes that link.

Setting

A schedule of a finite job set is a sequence $\sigma$ listing every job once; the machine processes the jobs in that order from time $0$ without idle time or pre-emption. Job $j$ has a processing time $p_j$ and a weight $w_j$; its completion time $C_j$ is the sum of the processing times of the jobs up to and including $j$, and the value of $\sigma$ is $\mathrm{val}(\sigma)=\sum_j w_jC_j$. Precedence constraints are a relation $P$ on jobs: $(i,j)\in P$ with $i\ne j$ means job $i$ must be completed before job $j$ starts. A schedule respecting all of them is feasible, and a feasible schedule $\sigma^*$ of least value is optimal.

Let $G=(U,V,E)$ be an $n$-by-$n$ bipartite graph: $|U|=|V|=n$ and $E\subseteq U\times V$. An edge biclique is a pair $A\subseteq U$, $B\subseteq V$ with $A\times B\subseteq E$, of value $|A|\cdot|B|$; the maximum edge biclique problem (Definition 9.1) asks for one of largest value. The bipartite scheduling instance $S_G$ has jobs $U\cup V$ and precedence constraints

so $u\in U$ must precede $v\in V$ exactly when $(u,v)$ is not an edge. Jobs of $U$ have $p=1$, $w=0$; jobs of $V$ have $p=0$, $w=1$. Thus $\mathrm{val}(\sigma)=\sum_{v\in V}C_v$, where $C_v$ is the number of $U$-jobs scheduled before $v$. For $i\ge1$, $\sigma(i)$ denotes the number of $V$-jobs scheduled before $i$ jobs of $U$ have been scheduled.

In the Lean development these are weightedCompletion, IsOptimalSchedule, IsEdgeBiclique, maxBicliqueValue, precSG, procSG, weightSG, valSG, IsOptimalSG and vBefore in the namespace SingleMachinePrec.Biclique.

Formalization targets

Goal: Lemma 9.1 (p. 666)

If a maximum edge biclique of $G$ has value $an^2$ with $a\in(0,1]$, then $S_G$ has an optimal schedule and every optimal schedule $\sigma^*$ satisfies

Milestones (proof of Lemma 9.1, §9, p. 666)

1. For every edge biclique $(A,B)$, a schedule in the block order $U\setminus A\to B\to A\to V\setminus B$ exists, and every such schedule is feasible with

2. For every schedule, $\sigma(n+1)=n$ and

3. For every feasible schedule and $i=1,\dots,n$,

Significance

Lemma 9.1 shows that the optimal value of $S_G$ determines the maximum edge biclique of $G$ up to a factor of order $\ln(1/a)$ in the "area above the work line" $n^2-\mathrm{val}(\sigma^*)$. Combined with the hardness of approximating maximum edge biclique (Theorem 9.1, cited from Ambühl, Mastrolilli and Svensson 2007) it yields Theorem 9.2: $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ has no PTAS unless SAT can be decided by a probabilistic algorithm in time $2^{N^\epsilon}$ for every $\epsilon>0$. It also makes precise the two-dimensional Gantt chart picture of Eastman, Even and Isaacs (1964) and of Goemans and Williamson (2000), in which every point on the work line of a schedule defines an edge biclique.

The lemma is proved in the paper; it is not formalized anywhere to our knowledge. A formal proof certifies the combinatorial core of the no-PTAS result independently of the complexity-theoretic layer, and its definitions (the bipartite instance $S_G$, edge bicliques, the profile $\sigma(i)$) are reusable for the gap inequality behind Theorem 9.2.

Difficulty

The upper bound is a direct computation on one explicit schedule. The lower bound is a statement about every feasible schedule, of which there are exponentially many, and it must hold with the explicit constant $2$ and the factor $\ln(1/a)$ for every $a\in(0,1]$. The printed argument splits the sum at $i=(1-a)n$ and uses $\lfloor an\rfloor$, treating $an$ as an integer; for general $a$ (for example $n=3$, value $2$, $an=2/3$) the split point is not an integer, so the printed estimate does not apply verbatim and the constant $2$ has to be re-checked for non-integral $an$. On the formal side, the value identity requires relating completion times in a list to counting $U$-jobs before each $V$-job, with ties among zero-length jobs.