← All papers
First page of Guaranteed indirect delivery in directed networks: The joint extremal function and explicit attaining constructions

Guaranteed indirect delivery in directed networks: The joint extremal function and explicit attaining constructions

Angel Ivanov Raychev

math.CO Oct 29, 2026 · v1
A Lean 4 development verifies the extremal formula for n≥12, m≥24, construction scores, game semantics, and finite certificate checkers.
A messenger and a pursuer move alternately on a finite loopless directed graph, with complete information and waiting permitted. The messenger moves first and wins upon reaching a designated recipient, before interception there. We determine the maximum number $M(n,m)$ of ordered nonadjacent source–recipient pairs for which delivery is guaranteed against every initial pursuer position, among graphs with $n$ vertices and $m$ arcs. We give the exact value and an explicit attaining graph for every admissible pair $(n,m)$. For $n\ge12$, a piecewise formula describes sparse growth, the interval $2n\le m\le n(n-3)$ in which every missing pair can be guaranteed, a dense staircase, and the zero range above $n(n-2)$. Complete finite tables cover smaller orders. The proofs combine degree and support bounds, local strategy composition, protected routing, and constructions in the missing-arc graph. Finite exceptional cases use explicit strategy certificates and complete computational exclusions. Reproducible programs and certificates accompany the paper; a Lean development verifies the complete formula for $n\ge12$ and $m\ge24$, the claimed scores of prescribed constructions at every admissible pair, and further finite upper bounds. Its remaining obligations are stated separately.

In a messenger–pursuer game on finite loopless digraphs, the task is to determine M(n,m): the maximum number of nonadjacent source–recipient pairs with guaranteed delivery against every initial pursuer position, over graphs with n vertices and m arcs.

Upper bounds come from degree and support arguments and domination lemmas. Attaining graphs are built from circulant digraphs with protected step differences, local strategy composition, and constructions in the missing-arc graph. Small cases are settled by certified exhaustive computation using reachability-game solvers and certificate checkers. A Lean 4 development formalizes the game semantics, the checker theorems, concrete certificates, and the complete formula for n≥12 and m≥24.

The exact value of M(n,m) and an explicit attaining graph are given for every admissible (n,m). For n≥12 the formula is piecewise: sparse growth, the interval 2n≤m≤n(n−3) where every missing pair can be guaranteed, a dense staircase, and zero above n(n−2). Complete finite tables cover smaller orders, and the parts not yet formalized in Lean are listed separately.

m12131415161718192021
M_E(m)9111315192833405360
Least host h78888109111012
Finite sparse-budget global maxima M_E(m) and least attaining host orders