Guaranteed delivery: delivery-time companion

Scope and proof boundaries

The main manuscript asks for the exact number of guaranteed indirect deliveries at every vertex and arrow budget. This companion preserves a different set of questions: how many arrows suffice for universal delivery within two messenger moves, and how quickly sparse strategies can deliver. It is a research checkpoint, not a completed classification or a publication-ready paper.

The game is unchanged. Both players see their positions, may wait or follow an outgoing arrow, and the messenger moves first. Receipt wins immediately before collision; other collisions lose, and infinite evasion is not delivery. Time counts messenger moves. A guarantee quantifies over every initial pursuer position other than the source and every legal history-dependent pursuer policy.

The numbered results cited here belong to the main count manuscript: Theorem 54 proves protected routing, Corollary 55 gives an exact-budget interval, and Theorem 59 proves antichain composition. Those count-relevant constructions and their natural delivery bounds remain in the main manuscript. This companion contains the extracted time-constrained consequences and the independently audited, explicitly partial fast-composition checkpoint.

Future deadline questions: definitions only

For an integer $T\ge0$, let $I_{\le T}(G)$ count missing nonloop ordered pairs $(s,t)$ for which, for every initial pursuer position $c\ne s$, there is a messenger strategy delivering within $T$ messenger moves against every legal pursuer policy. The strategy may depend on the observed initial $c$. The associated extremal function is $$M_{\le T}(n,m)=\max_{|V(G)|=n,\ |E(G)|=m}I_{\le T}(G).$$ For a fixed admissible $n\ge1$ and $0\le m\le n(n-1)$, define $$T_*(n,m)=\min\{T\ge0:M_{\le T}(n,m)=M(n,m)\}.$$ Thus $T_*$ asks for the smallest uniform deadline at which some graph attains the unrestricted optimum. It does not require one graph to be optimal at every deadline. When the unrestricted maximum is zero, this convention gives $T_*=0$.

These are definitions for possible further work; no classification of either function is claimed here. All deadlines are guarantees against arbitrary pursuer play, not expected delivery times or success probabilities. The probability estimates in the routing construction concern random choices of the graph, not a probability distribution on the game’s players.

The scale of the first universal two-move budget

Let $q_2(n)$ be the smallest number of arrows in a graph on $n$ vertices for which every source–recipient pair is guaranteed within two messenger moves. This differs from minimizing delivery time among extremizers that guarantee only some of their missing pairs, as in $T_*$.

The first feasible budget $q_2(n)$ also differs from an interval onset. To make the latter precise, for $n\ge10$ put $L=n(n-1)$, $B=n(n-3)$, and Define $\rho_2(n)$ as the least integer $a\in\{0,\ldots,B\}$ such that every integer budget $a\le m\le B$ admits universal two-move delivery. The endpoint construction in Theorem 58 ensures this set is nonempty. The condition concerns every budget in the interval, whereas $q_2$ asks only for the first feasible budget; no equality between these two quantities is claimed. The interval stops at $B$ because Theorem 14 excludes noncomplete universal-delivery graphs above $B$. The complete graph at $m=L$ is a separate trivial case.

Two-move consequence of Corollary 55. For every $n\ge2$, $$q_2(n)\ge\left\lceil\frac n2(\log_2n-1)\right\rceil.$$ Moreover, $q_2(n)=\Theta(n\log n)$ as $n\to\infty$. This statement and the lower-bound proof below were formerly included in Corollary 55 of the combined manuscript; its exact-budget construction remains in the main count paper.

Proof of the upper order bound. Corollary 55 supplies a universally two-move graph with exactly $$A_n=\frac{b_n(2n-b_n-1)}2,\qquad b_n=\lceil24\log n+4\rceil,$$ arrows whenever $b_n\le n$. This condition holds for all sufficiently large $n$, and $A_n\le nb_n=O(n\log n)$. Therefore $q_2(n)=O(n\log n)$. The following lower bound gives the matching order. $\square$

Proof of the lower bound. For every vertex $u$, form the disjoint sets $$S_u=\{u\}\cup N^-(u),\qquad T_u=N^+(u)\setminus N^-(u).$$ For each unordered reciprocal pair add its two singleton endpoints as another pair of disjoint sets. These pairs separate every two vertices. A one-way arrow $s\to t$ is separated by $(S_s,T_s)$, and a reciprocal pair has its singleton separator. If neither arrow exists, start the pursuer at $t$. A two-move guarantee forces a route $s\to u\to t$ with $t\not\to u$: waiting first would leave the missing pair undelivered in the one remaining move. Thus $s\in S_u$ and $t\in T_u$.

If there are $z$ reciprocal unordered pairs, the first $n$ separators have total membership $n+2m-2z$ and the singleton separators add $2z$, giving $n+2m$ in total.

Hansel’s separating-system inequality states that this total is at least $n\log_2n$; see (Bollobás and Scott 2006, Lemma 1). Its short proof is included here. Independently delete one uniformly chosen side of every separator. At most one vertex survives. A vertex appearing in $d_v$ separators survives with probability $2^{-d_v}$, so $\sum_v2^{-d_v}\le1$. Convexity gives $n2^{-(\sum_vd_v)/n}\le1$, hence $\sum_vd_v\ge n\log_2n$. Applying this inequality proves $n+2m\ge n\log_2n$ and the integer lower bound. $\square$

The lower-bound ingredient is classical; the conversion from the delivery game to this separating system uses the present timing convention, including a pursuer initially at the recipient. The antichain construction in the next section improves the constructive asymptotic constant. The order-of-growth result does not identify an optimal constant or assert that $\rho_2(n)=q_2(n)$.

Antichain two-move sparsity

For the equal-weight codes of Theorem 59, put $$C(k,r)=\frac{k}{k-r}\binom{k-r}{r}.$$ For odd $k\ge7$ and $3\le r\le\lfloor k/2\rfloor$, its two hub parts supply $2C(k,r)$ codes. With $q=n-2k\le2C(k,r)$, the exact base budget is $$A=(4k-r)n-2k(2k+3-r).$$ The count proof and the assertion that every outside-arrow subset preserves two-move delivery remain with Theorem 59. The following consequence and its parameter calculation are extracted from that theorem’s former continuation.

Two-move sparsity. These codes sharpen the constructive side of the preceding order bound to $$q_2(n)\le\left(\frac{26\log2}{\log(3125/108)}+o(1)\right)n\log_2n =(5.3555763082\ldots+o(1))n\log_2n.$$ For an exact parameter rule at every $n\ge30$, choose the least even $d\ge2$ with $2C(7d+1,2d)\ge n$, and put $k=7d+1$, $r=2d$. The core fits: when $d=2$ it has 30 vertices; when $d\ge4$, minimality gives $$n>2C(7d-13,2d-4)\ge2\binom{5(d-2)}{2(d-2)} \ge5(d-2)(5(d-2)-1)\ge14d+2.$$ The binomial inequality uses unimodality and $2\le2(d-2)\le5(d-2)/2$. The exact base budget is $$A=(26d+4)n-2(7d+1)(12d+5).$$ The modal probability of a binomial distribution with $5d$ trials and success probability $2/5$ is attained at $2d$ and is at least $1/(5d+1)$. Consequently $$C(7d+1,2d)\ge\binom{5d}{2d}\ge\frac{(3125/108)^d}{5d+1}.$$ This proves $d\le\log n/\log(3125/108)+O(\log\log n)$ and the displayed upper bound. Since $k=O(\log n)$, even listing all hub subsets and retaining valid codes is a polynomial algorithm. The separating-system lower bound above still applies; the leading constant of $q_2(n)$ remains open.

Partial fast sparse composition

The following is the retained 13 September 2026 checkpoint. Its conditional eight-recipient-type theorem has independently replayed finite certificates and an ordinary finite-quotient projection proof. It does not establish universal delivery, an all-order attaining construction, or a new exact value of $M(n,m)$. The final two recipient types remain open.

Let $X$ be a finite set with permutations $a,b$. The undirected edges $\{x,xa\},\{x,xb\}$ must form a connected simple four-regular graph; thus $xa,xa^{-1},xb,xb^{-1}$ are four distinct neighbors at every $x$. The positive eight-type theorem below assumes girth at least 133. Let $D$ be the directed diameter using $a^{-1},b^{-1}$. The earlier six-exclusion navigation result only needs girth at least nine, but that weaker hypothesis is not substituted into the eight-type delivery theorem.

The graph rules are from research/composition-interface-navigation.md. The remaining checkpoint is extracted from research/composition-interface-terminal-checkpoint.md; its proof and literal transition replay are reviewed in research/composition-interface-terminal-independent-audit.md.

Construct ten vertices $(x,0),\ldots,(x,9)$ over each $x$. There are two outgoing arcs, called $A$ and $B$, at every vertex. The first permutation is

$$\begin{aligned} 0_x&\to6_x\to2_x\to3_x\to9_x\to5_{xb},\\ 5_x&\to1_x\to7_x\to8_x\to4_x\to0_{xa}. \end{aligned}$$

The second permutation is

$$\begin{aligned} 0_x&\to0_{xa},&1_x&\to2_{xa^{-1}},&2_x&\to4_{xa^{-1}},\\ 3_x&\to3_{xa^{-1}},&4_x&\to1_{xa^{-1}},\\ 5_x&\to5_{xb},&6_x&\to7_{xb^{-1}},&7_x&\to9_{xb^{-1}},\\ 8_x&\to8_{xb^{-1}},&9_x&\to6_{xb^{-1}}. \end{aligned}$$

Both arc rules are permutations, and their destinations are distinct at every vertex. The graph is loopless, two-in/two-out regular, with $10|X|$ vertices and $20|X|$ arcs.

One common interface

Write $(i;w,j)$ for messenger type $i$ at cell $x$ and cop type $j$ at cell $xw$. In addition to collisions, exclude precisely these twelve joint states:

$$\begin{aligned} &(3;e,5),\ (3;e,9),\ (3;b,7),\ (3;b^{-1},5),\ (3;b^{-1},9),\ (4;e,0),\\ &(8;e,0),\ (8;e,4),\ (8;a,2),\ (8;a^{-1},0),\ (8;a^{-1},4),\ (9;e,5). \end{aligned}$$

Call the remaining uncaught messenger-turn states $J$. The finite certificates verify both of the following.

1. Every initial uncaught state reaches $J$ safely in at most two messenger moves. The cell may change during normalization.
2. From $J$ at cell $x$, either prescribed cell $xa^{-1}$ or $xb^{-1}$ is safely reachable within 32 messenger moves, ending in $J$ after the final cop response.

The twelve exclusions are the union of the nine-exception interface previously used for recipient type 0 and its lane mirror. This avoids assuming that the earlier eight-exception interface was contained in the type-0 interface: it was not. The common interface is contained in every successful terminal module’s input condition.

Exact terminal modules

Each statement starts in $J$ at cell $x$, with arbitrary cop position. Arrival at the recipient ends the game immediately, before a cop response.

• Type 0 at $xa$: at most 39 moves. The messenger window has radius 2, the cop window radius 3, and the cop exterior retains only its type.
• Type 1 at $xa^{-1}$: at most 62 moves. Both windows have radius 3; exterior cop states retain their type and the first two letters of their reduced quotient word.
• Type 3 at $xa^{-2}$: at most 35 moves. Both windows have radius 3; the cop exterior retains only its type.
• Type 4 at $xa^{-1}$: at most 38 moves. Both windows have radius 3; the exterior again retains its type and first two reduced letters.
• Interchange $a\leftrightarrow b$ in the parameterized rule scheme and add 5 to every type modulo 10. The rules and $J$ have this exact symmetry for every pair of permutations; no automorphism of a fixed quotient interchanging $a,b$ is required. It gives, respectively, types 5 at $xb$, 6 at $xb^{-1}$, 8 at $xb^{-2}$, and 9 at $xb^{-1}$, with the same bounds.

Types 2 and 7 remain unresolved. They are not obtained from these modules by treating a successful receipt at a predecessor as safe intermediate arrival: receipt permits a final collision, while an intermediate step must survive the cop response.

Why branch provenance matters

The old exterior symbol allowed a cop that left one branch of the free quotient tree to enter another branch immediately. Retaining the first two reduced letters removes some of these artificial jumps.

In the branch-aware finite arena, a cop outside the radius-three window has descriptor $(\Omega_p,i)$, where $p$ is one of the twelve reduced words of length two and $i$ is its type. It may wait or make either type change while retaining $p$. For an arc labelled $g$, it may enter a represented cell $z$ exactly when the prior cell $zg^{-1}$ lies outside the radius-three ball and has prefix $p$. There are 530 messenger positions and 650 cop positions. This is an overapproximation of the game on the infinite free quotient tree.

For type 4, the original six-exception interface had exactly one failing start in this arena: messenger 3 and cop 5 in the anchor cell. Excluding that state and its lane mirror produced the eight-exception interface; both 32-move navigation modules survived, and normalization took at most two moves. The final twelve-exception interface also handles the separate type-0 input conditions.

Audited finite-quotient projection, with an explicit girth bound

The following ordinary argument and its finite certificates have passed the independent audit cited above.

For a branch-aware terminal module lasting at most $T$ moves, let

$$R=3,\qquad L=R+T.$$

Assume the undirected quotient ball of radius $L$ about the anchor is an induced tree. Girth at least $2L+3$ is a sufficient conservative condition. A cop initially farther than $L$ cannot enter the represented radius-$R$ window before the module ends. It can be assigned any exterior prefix, with its true type, and mapped to exterior transitions throughout.

Otherwise, use the cop’s unique word in this tree. At time $t$, call it relevant if its distance from the anchor is at most $R+T-t$. While it is relevant, all relevant moves lie in the induced radius-$L$ tree. Thus its exterior prefix cannot change without passing through the represented ball. If it becomes irrelevant, no remaining play can bring it into that ball before the deadline; retain its last exterior prefix and its actual type. If irrelevance first occurs on an outward step from the represented ball, initialize that frozen prefix from the departure edge. This defines a causal projection and does not assume knowledge of the cop’s future choices. Every possible collision with the messenger is inside the represented ball and is preserved.

The largest terminal bound is $T=62$, so girth at least 133 suffices simultaneously for these branch-aware modules. It also implies the girth-nine condition for the ordinary navigation and other terminal modules.

Eight-type delivery theorem (computer-assisted, independently audited). On every finite quotient satisfying the connected simple four-regular hypothesis above and having girth at least 133, let $D$ be its directed diameter using $a^{-1},b^{-1}$. Every recipient of types

$$\{0,1,3,4,5,6,8,9\}$$

is reachable from every source and every uncaught initial cop position in at most $32D+64$ messenger moves. Normalize, navigate to the appropriate anchor, and invoke its terminal module. For example, recipient $0_y$ uses anchor $ya^{-1}$, while $1_y,4_y$ use $ya$ and $3_y$ uses $ya^2$. This is a statement about eight recipient types, not universal delivery or a new exact value of $M(n,m)$.

Final gap and a real infinite-tree obstruction

For recipient $2_x$, the predecessors are $6_x$ and $1_{xa}$. A cop camping at $0_x$ controls $6_x$ and $0_{xa}$. In the infinite free quotient tree, every passage from the $x$-side of the edge $x\!-\!xa$ into the $xa$-side has head $0_{xa}$. Thus a messenger starting at $1_x$ cannot safely reach either recipient predecessor. The state belongs to $J$.

This rules out a terminal theorem from all of $J$ at the recipient’s own cell on the infinite lift, regardless of the window radius. A finite quotient can bypass that cut through a long outside route. The remaining composition problem is therefore to retain enough information about that final approach, or to change the gadget.

A useful next interface fact survives: the 32-move negative-$a$ module can finish specifically in types $\{1,2,3,4\}$, and the negative-$b$ module in $\{6,7,8,9\}$, while retaining the eight-exception interface. This last-generator information was tested but is not included as a separately replayed claim in the current terminal certificate archive.

Files and proof boundary

• src/composition_interface_terminal_checkpoint.py generates the seven full finite proofs: two navigation modules, normalization, and four terminal modules. It directly checks a legal messenger action and all cop responses for every new winning state.
• research/composition-interface-terminal-checkpoint-certificates.json.gz contains their arenas and all layers.
• research/composition-interface-terminal-checkpoint-verification.json records counts, source hashes, and the archive hash.
• research/composition-interface-development.md records successful reductions, failed alternatives, and the finite/infinite distinction.

The original direct replay shares its arena producer. The subsequent independent audit reconstructed the literal ordinary and branch-aware transitions, checked all seven complete layer certificates and their exact seed/input conditions, verified lane symmetry, and reviewed the quotient projection. Its files are research/composition-interface-terminal-independent-audit.md and research/composition-interface-terminal-independent-audit.json. The immutable production archive retains its original pre-audit status text; the later independent audit supersedes that status. Earlier exploratory JSON files are diagnostics, not replacements for these full certificates.

Provenance and further questions

Alexandra Ignatova’s original problem and layered construction arose in her 2023 project under Angel Raychev’s mentorship, with a retained February 2024 manuscript. Their original upper bound and two-in/two-out research direction are credited in the main paper. The September 2026 extensions and this companion’s proofs and computational work were developed with Astra 6 through the Codex harness. The main manuscript’s approved authors are Angel Ivanov Raychev and Alexandra Ignatova, in that order. This separate timing companion remains a research checkpoint; no arXiv submission is claimed.

The exact leading constant of $q_2(n)$, the interval onset $\rho_2(n)$, and universal fast delivery for the ten-type construction remain open. No new deadline-constrained extremal classification is asserted here. The infinite-tree obstruction is not a proof of failure for finite quotients. None of these open questions is required to complete the main manuscript’s exact-count objective.

The probability and separating-system arguments, cycle-code counts, and quotient projection are ordinary proofs. The fast modules additionally depend on finite rank certificates and their independent replay. No full Lean proof of these general time results is claimed. Bibliographic citations use paper/references.bib; source and receipt paths are relative to the repository root.

References