Guaranteed indirect delivery in directed networks: The joint extremal function and explicit attaining constructions
Angel Ivanov Raychev
math.CO
Oct 29, 2026 · v1
TL;DR
A Lean 4 development verifies the extremal formula for n≥12, m≥24, construction scores, game semantics, and finite certificate checkers.
Abstract
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.
Problem
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.
Approach
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.
Results
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.
| m | 12 | 13 | 14 | 15 | 16 | 17 | 18 | 19 | 20 | 21 |
|---|
| M_E(m) | 9 | 11 | 13 | 15 | 19 | 28 | 33 | 40 | 53 | 60 |
| Least host h | 7 | 8 | 8 | 8 | 8 | 10 | 9 | 11 | 10 | 12 |
Finite sparse-budget global maxima M_E(m) and least attaining host orders