Graph Theory

Motivation

Edge-colored tournaments combine a complete orientation with a finite palette. They are a natural setting for comparing local multicolor obstructions with global directed reachability. The question attributed to Sands, Sauer, and Woodrow asks whether three colors force one of two outcomes: a directed triangle whose three arcs all have different colors, or a single vertex that can reach every target along a monochromatic directed path.

The problem was recorded by the Open Problem Garden in 2008. A minimum-counterexample reduction was later restated by Georgakopoulos and Sprüssel in their study of three-colored tournaments. The available project computation excludes counterexamples through eleven vertices, but that package is explicitly candidate_only: it is bounded search evidence, not a proof of the unrestricted theorem.

Setting

A tournament is an orientation of a finite complete simple graph. For each pair of distinct vertices $u,v$, exactly one of $u\to v$ and $v\to u$ is present. Every directed arc receives one of three labeled colors.

A rainbow directed triangle is a cyclically oriented triangle

$$a\to b\to c\to a$$

whose three arc colors are pairwise distinct. A transitive three-vertex subtournament is not a directed triangle and is therefore not forbidden merely because its three arcs have different colors.

A vertex $s$ is a monochromatic source when, for every vertex $t$, there is some color $k$ and a directed $s$-to-$t$ path all of whose arcs have color $k$. The chosen color may depend on $t$; the theorem does not demand one common color for all targets. Length-zero reachability handles $t=s$.

The formal domain is nonempty finite tournaments. This nonemptiness convention is stated explicitly because an empty vertex type has neither a rainbow triangle nor a candidate source and would trivialize the negation of the intended question.

Formalization targets

Root theorem

For every nonempty finite tournament $T$ with a three-coloring of its arcs,

$$T\text{ has a rainbow directed triangle} \quad\lor\quad \exists s\in V(T)\ \forall t\in V(T),\ \text{$s$ reaches $t$ monochromatically}.$$

No compatibility is required between the colors of paths to different targets, and unused palette colors are permitted.

Finite order milestone

The first milestone freezes the exact bounded claim supported by the replay package:

$$1\le |V(T)|\le 11\text{ and no rainbow directed triangle} \quad\Longrightarrow\quad T\text{ has a monochromatic source}.$$

The statement includes all tournaments and all three-color arc assignments at those orders, not only one symmetry representative. The repository's observations report exhaustive search after a minimum-counterexample reduction, but the Lean theorem remains open until it has an accepted proof.

Significance

The root theorem would turn a local forbidden configuration into a global reachability certificate. Such a result clarifies how orientation and edge color interact: ordinary Gallai decompositions for undirected colored complete graphs cannot be imported unchanged, because the hypothesis forbids only rainbow cyclic triangles and allows rainbow transitive triples.

The formal development creates reusable definitions for colored directed reachability and exposes the direction of every relation. This matters in minimum-counterexample arguments, where an auxiliary arc $u\to_F v$ may encode that $v$ cannot reach $u$; reversing that convention invalidates the cycle reduction. A verified finite milestone would also provide a regression target for SAT, SMT, or exhaustive encodings without elevating their raw output to a universal theorem.

Difficulty

The classical Gallai theorem is not directly applicable. It assumes an undirected complete graph with no rainbow triangle of any orientation, whereas this problem permits a transitive triple with three distinct colors. A proposed partition must therefore control both arc colors and directions between parts.

The minimum-counterexample route yields a useful spanning cycle in an auxiliary nonreachability digraph. It does not itself bound the size of a counterexample. The order-eleven computation terminates because its domain is finite, but no induction from eleven to arbitrary order follows. A proof must add a structural theorem that survives all orientations and allows monochromatic paths of arbitrary length rather than treating reachability bits as independent physical arcs.

Formalization scope

Lean represents the tournament as a binary relation D with looplessness and exactly one orientation on each unordered pair. The coloring is a total function on ordered pairs, but only values on actual arcs are semantically used. Monochromatic reachability is the reflexive transitive closure of arcs of one fixed color. The root and finite theorem quantify over every nonempty finite vertex type.

The finite replay, its solver versions, hashes, and no-witness observations remain external candidate evidence. They do not close the milestone without a checkable certificate or a proof accepted by the platform. Contributions may formalize the minimum-counterexample cycle lemma, build an independently checked finite certificate, isolate a directed decomposition theorem, or prove the root. No contribution may replace a directed rainbow triangle by an undirected one, require the same path color for every target, or assume heredity of failure for arbitrary induced subtournaments.

Selected references

• Open Problem Garden, Monochromatic reachability versus rainbow triangles, posted 2008. https://www.openproblemgarden.org/op/monochromatic_reachability_vs_rainbow_triangles
• B. Sands, N. Sauer, and R. Woodrow, On monochromatic paths in edge-coloured digraphs, Journal of Combinatorial Theory, Series B 33 (1982), 271–275.
• A. Georgakopoulos and P. Sprüssel, On 3-coloured tournaments, 2009. https://arxiv.org/abs/0904.1967
• A. Trygub, Full Characterization of Color Degree Sequences in Complete Graphs Without Tricolored Triangles, 2023. https://arxiv.org/abs/2304.14579

Why network information has a cost

Choosing a small group of people to start an intervention can have a much larger effect when their contacts pass it on. In many applications the contacts themselves are expensive to learn: a survey worker can ask about a person's neighbors, or a crawler can request one adjacency-list entry, but neither necessarily has a complete network. Eckles, Esfandiari, Mossel and Rahimian study influence maximization with this information cost included. Their paper asks whether a near-greedy spread guarantee can be obtained while limiting the number of edge queries made to the network. An edge query reveals one indexed neighbor of one vertex. The bound matters when the graph is large and acquiring its edges is a material part of the work, rather than a free preprocessing step.

Graph, spread, and sketches

The independent cascade model starts with a finite undirected simple graph $G=(V,E)$ and a common probability $p\in[0,1]$. Each edge is independently active with probability $p$. Given a seed set $S\subseteq V$, a vertex adopts when an active-edge path joins it to a seed; a seed adopts by a path of length zero. Write $\phi(v,S)$ for the probability that $v$ adopts. The influence function is the expected number of adopters,

$$\Gamma(S)=\sum_{v\in V}\phi(v,S),\qquad \mathrm{OPT}=\max_{S\subseteq V,\ |S|=k}\Gamma(S).$$

The problem is to choose exactly $k$ seeds. Here $n=|V|$ and $1\le k\le n$. These definitions follow Section 2, Definitions 1–2, of the source paper.

The paper's PROBE procedure samples an initial vertex set $V_\rho$ and produces $T$ partial graphs. It explores outward through neighbor queries, retaining each candidate edge with probability $p$. Exploration from a vertex stops once its revealed component reaches a threshold $\tau$. A query is charged even when its answer points to a vertex already explored and the answer is discarded. From these partial graphs, the paper defines an influence estimate $\Gamma^{(T)}_{\rho,\tau}$. Its SEED procedure applies randomized greedy selection to that estimate. Algorithm 4 fixes the parameters, runs PROBE, then runs SEED. The estimator and procedures are specified in Sections 3.1–3.4 of the paper.

Formalization targets

The goal is the explicit Algorithm 4 form of Theorem 7. For $0<\epsilon'\le1$ and $n\ge(30/\epsilon')^2$, let $\Lambda^*$ be the output seed set and $q$ the number of PROBE edge queries. With $\epsilon=\epsilon'/7$ and $\delta=2\log n$, the targets are

$$\mathbb E[\Gamma(\Lambda^*)]\ge(1-1/e)\mathrm{OPT}-\epsilon'n, \qquad \mathbb E[q]\le Q^{n,k}_{\epsilon,\delta}+6T^{n,k}_{\epsilon,\delta}.$$

The first inequality is Theorem 7's spread claim; the second is the explicit query inequality (30) in its Appendix B.12 proof. The theorem also states asymptotic query and run-time classes. This mission states the explicit query bound and does not give a machine-level running-time semantics. Theorem 7 and Appendix B.12 identify both formulas.

The milestones record the approximation-transfer lemma, the two concentration claims for initial sampling and probing, the coverage structure of the truncated sketch, the randomized-greedy guarantee, Theorem 5's high-probability query bound, and the worst-case query bound used to pass to expectation. The statement of each is tied to its source page.

What the result supplies

The spread inequality makes the cost of incomplete graph information explicit: the output's expected spread is within an additive $\epsilon'n$ of the standard $1-1/e$ factor times the complete-information optimum. The query inequality specifies the expected amount of network information Algorithm 4 requests, using the paper's constants $Q$ and $T$. This puts a concrete price on obtaining a seed set without reading the whole graph. The paper gives the corresponding asymptotic discussion and simulations; neither simulations nor a running-time model is part of the target here.

Formalizing this result requires reusable definitions of finite set-function maxima and submodularity, a finite independent-cascade spread model, and an exact account of a random graph-exploration algorithm. The model separates the graph's random active edges from the algorithm's random probes and from SEED's random candidate sets. The resulting definitions can support later statements about graph sampling, coverage functions, and influence maximization. The target is a known paper claim that has been stated in Lean with open proofs; the proposal does not assert that these proof obligations have already been discharged by a machine checker.

Where the difficulty lies

One cannot simply apply a greedy approximation theorem to $\Gamma$: Algorithm 4 chooses seeds using a random, truncated sketch, while its guarantee concerns the original cascade spread. The random initial set, the repeated probe copies, and the threshold each change the objective being optimized. The required probability bounds must hold across all size-$k$ seed sets, not only a fixed one. Query accounting also has to charge revealed neighbors that do not enter the sketch. Those are the reasons the proposition is stronger than a routine monotone-submodular maximization statement; the distinct claims appear in Lemmas 1–3, Theorem 5, and Appendix B.12 of the paper.

Formalization scope

Lean uses $V=\operatorname{Fin}(n)$, a finite undirected SimpleGraph, real-valued probabilities and objectives, and natural logarithms. Cascade probabilities are finite weighted sums over retained edge sets. PROBE randomness is represented by finite permutations and Bernoulli coins; probabilities and expectations are finite weighted sums. A single PROBE realization returns both its sketch edges and its count of step-10 queries. The untruncated sketch uses threshold $n+1$. SEED draws a uniform subset of the remaining vertices at each round and chooses a maximum marginal gain, with least-index tie breaking. These choices make the algorithm in the theorem a defined object, so its expected query count cannot be made zero by treating the entire graph as free input.

Three boundary conventions make Algorithm 4 total. When $\rho>1$, its initial sample size is $\min(\lceil n\rho\rceil,n)$. PROBE's inner loop ends when the selected neighbor indices are exhausted. SEED uses the ceiling of its nonintegral subset size, capped at the number of unselected vertices. The proof targets for Lemmas 2–3 and Theorem 5 explicitly use $n\ge5$ and $\delta\ge2\log n$; Lemma 1 includes $\alpha\ge0$. Lemma 3 also states the inherited initial-sample size and sampling-rate conditions. These refinements are identified in the item descriptions and audit notes. The formulas for $\rho$, $T$, $\tau$, $E$, $C$, and $Q$ retain the constants of equations (5)–(7) of the paper.

The foundational definitions, exact theorem statements, and proofs of the listed milestones are within scope. Results about directed graphs, other diffusion models, and empirical network simulations are separate from this target.

Selected references

• D. Eckles, H. Esfandiari, E. Mossel, and M. A. Rahimian, Seeding with Costly Network Information, Operations Research, 2022; arXiv:1905.04325v5.

Motivation

Directed network design asks which connections can be bought under a limited budget when traffic follows the directions of arcs. In directed tree orienteering, the reward comes from vertices reached by a rooted directed tree. The submodular version allows the reward of a new vertex to depend on which vertices have already been reached. This captures diminishing returns, including coverage rewards, while preserving a single cost constraint. Ghuge and Nagarajan use this problem to obtain results for directed Steiner tree and other directed network design problems; the connection is explained in their introduction and applications.

The target here is the paper's main algorithmic theorem. Its distinguishing claim combines an approximation ratio that improves with the optimal solution size and a quasi-polynomial bound on the algorithm's work. Both parts matter: an approximation statement about an unspecified algorithm would leave the computational content of the result open. The paper develops recursive greedy search, a value-guided budget search, and a version that groups several recursion levels. The main theorem reports the combined guarantee.

Setting

An instance has a finite vertex set $V$ of size $n$, a root $r^*\in V$, a nonnegative integral cost $c(u,v)$ for every directed arc, and a budget $B\ge0$. A rooted arborescence is a set of directed arcs in which each selected non-root vertex has one incoming arc and every selected vertex is reachable from $r^*$. Its cost is the sum of its arc costs. The complete directed graph is used because the source reduces to that representation; loops have no role.

A value oracle supplies $f(S)$ for every vertex set $S\subseteq V$. The reward is monotone: enlarging a set cannot lower its value. It is submodular: $f(S\cup T)+f(S\cap T)\le f(S)+f(T)$. In this mission, values are natural numbers and satisfy $f(S)\le n^a$ for a fixed exponent $a$. This makes the integer thresholds used in the binary-search version explicit. The reward of an edge set $T$ is evaluated on $V(T)$, which includes the root. For an already selected set $X$, the marginal reward is $f_X(T)=f(V(T)\cup X)-f(X)$.

The algorithm also receives a responsibility set $Y$, a budget, and a depth $i$. A successful output must reach every vertex in $Y$ and respect the budget. A compatible comparison arborescence has the same root, responsibility and budget conditions, together with the depth's vertex cap. The paper's $k$ counts vertices in a comparison solution, including its root. The target assumes $3\le k\le n$ so its double logarithm is positive.

Formalization targets

The main target is Theorem 1.1, p. 1. For every $\varepsilon>0$ and polynomial reward exponent $a$, one constant $C>0$ works for every eligible instance. The specified grouped recursive greedy algorithm returns a feasible solution $T$ such that every feasible rooted arborescence $A$ with at most $k$ vertices obeys

$$f(V(A))\le C\frac{\log k}{\log\log k}f(V(T)), \qquad \operatorname{steps}(T)\le\bigl(n\log_2(B+2)\bigr)^{C(\log k)^{1+\varepsilon}}.$$

The milestone statements are the rooted separator Fact 2.2 in the corrected edge-count form, the $1/i$ guarantee for basic recursive greedy in Lemma 2.5, the same guarantee with binary-search budget guesses in Lemma 2.8, and the grouped recursion guarantee in Lemma 2.10. Their original wording and page locations accompany the individual milestones. These statements isolate the size reduction and the three approximation regimes on which the target depends.

Significance

The theorem supplies a directed, budget-constrained optimization guarantee for a class of rewards broader than additive vertex prizes. If an optimal solution has $k$ vertices, the approximation factor grows as $\log k/\log\log k$, while the reported work grows quasi-polynomially in the input parameters. The paper applies the result to directed tree orienteering and derives consequences for directed Steiner tree and other network design settings. The mission concentrates on the submodular tree orienteering theorem itself, so those later reductions remain separate statements in the source.

This is a known paper result, not an open conjecture. The formalization work is to state and eventually prove the theorem for an explicit algorithm and a concrete step counter. A machine-checked proof would also settle the paper's boundary cases in a representation that subsequent results can import: reachability in directed edge sets, compatible subproblems, and value-threshold budget search. The statements here are draft targets; a successful Lean build checks that they are well formed, not that the advertised bounds have already been proved.

Difficulty

A recursion that guesses a separator and divides responsibilities must coordinate the two subcalls: the second uses vertices already found by the first, and its remaining budget depends on the first guess. A direct transcription of the printed pseudocode can return an empty edge set despite unmet responsibilities. It also omits zero as a left-subtree budget even though the paper permits zero-cost arcs. Either issue can break feasibility or the approximation claim on small instances. The grouped version must preserve the approximation bound when its depth counts several levels at once. In particular, its depth-one call must handle every compatible tree with at most $(3/2)^s$ non-root vertices. Its binary searches and grouped-base candidates must be included in the runtime accounting. A value-only guarantee does not establish the theorem's time bound.

Formalization scope

Vertices are Fin n; arcs are ordered pairs and algorithms return an optional finite arc set with a natural-number step count. none represents infeasibility. The output's reachability, cost and responsibilities are asserted separately because a union of recursive outputs need not itself have the unique-parent property of an arborescence. The target also requires a rooted arborescence contained in that output on the same vertex set. Marginal rewards use real subtraction, avoiding truncated natural-number subtraction. The paper's submodularity predicate is reused from the published NonmonotoneSubmod.Shared.Submodular definition.

The concrete algorithm searches budgets from zero through the remaining budget and carries infeasibility through subcalls. Its grouped depth-one call examines all feasible arborescences up to the source's $(3/2)^s$ cap. Binary search records every recursive probe, and the step count records each candidate value evaluation and each grouped-base edge tuple. The logarithmic base uses $B+2$, making the statement meaningful for budgets zero and one. No triangle inequality is assumed: the source invokes metric completion without loss of generality, while these statements work directly with the complete cost table. These choices, along with the corrected rooted interpretation of Fact 2.2, are recorded in the moderation notes.

The target names this algorithm and its recorded steps; an existence claim about some algorithm would miss its computational assertion. Useful contributions include the separator theorem, the three approximation lemmas, and reusable properties of the budget search, reachability and step counter. The source's length-constrained and deadline extensions, and its later application reductions, are outside this mission.

Selected references

• R. Ghuge and V. Nagarajan, Quasi-Polynomial Algorithms for Submodular Tree Orienteering and Other Directed Network Design Problems, arXiv:1812.01768v2, 2019; journal version in Mathematics of Operations Research, 2022. Preprint.