Guaranteed delivery: classification proofs
Read the exact-count overview, download the paper and sources, or inspect the Lean coverage. This proof text and the PDF are generated from the same arXiv-prepared manuscript by Angel Ivanov Raychev and Alexandra Ignatova. The manuscript has not been submitted.
The exact-count classification is complete. The sparse upper proofs use a common source/sink induction, and the main construction uses pair codes that reach the dense endpoint directly. The contents group the arguments by mathematical topic. Retained theorem labels preserve existing cross-references; a result that follows from a later theorem is identified as a consequence. Ordinary proofs, finite computational premises and partial Lean coverage are distinguished throughout.
The four-regime formula covers every order from twelve, and the complete tables through eleven vertices cover every smaller host and budget. The finite sparse-budget completion supplies the exact arrow-only values through twenty-one and the smaller-host exceptions, with explicit attainers.
The current main theorem gives M(n,m) = n(n − 1) − m for every n ≥ 12 and 2n ≤ m ≤ n(n − 3). The complete main-interval proof joins a bounded staged certificate bridge to periodic sparse constructions, circles and the generalized hub composition. The six-offset circles and reduced hub interface have ordinary parameterized proofs. Earlier constructions retain their original domains and stronger time or optional-subset guarantees.
The common local-strategy theorem proves when a finite arena simulates ring play and how safe transfers reach a delivery entry. The guide-attachment lemma separates safe entry from the finite routing interface. The 21-module formal coverage includes eventual-winning completeness, the unrestricted vertex bound, the dense zero band, an exact mixed-score example and abstract guide entry. Concrete local arenas, hub codes and the full classification remain outside Lean.
The evidence and replay guide connects the current results to their computational checks and distinguishes those checks from dated research history.
For every feasible vertex and arc count, the classification gives the exact value of M(n,m) and explicit adjacency rules, a specified attaining composition with parameters determined from (n,m), or a certified listed finite graph. The construction inventory checks these recipes separately from numerical coverage. Conditional and probabilistic theorems retain their full statements and any stronger routing or optional-subset guarantees; alternative exact-count constructions do not automatically inherit those properties.
The delivery-time companion preserves the separate, parked time-optimization questions. Routing and two-move arguments needed for the count constructions remain here.
Results and scope
Introduction
A messenger has just obtained a message at a station of a directed network. A pursuer occupies another station, and both positions are visible. They move alternately, the messenger first, using one directed connection or waiting. The messenger wants to deliver to a designated recipient before interception. Receipt completes the task immediately, even if the pursuer is at : the pursuer can intercept the messenger but cannot disable the recipient.
A direct connection makes delivery immediate. We study the additional communication supported by the network: source–recipient pairs without a direct connection for which delivery is nevertheless guaranteed against every allowed initial pursuer position and policy. Write for their number.
We determine for every admissible pair of integers and , and give explicit adjacency rules or a specified composition procedure attaining each value, with parameters determined from and a proof of guaranteed delivery for its counted pairs. The vertex-only and arc-only maxima follow by taking the corresponding maxima:
Isolated vertices are allowed. Removing them preserves , so the arc-only maximum is finite: a graph with arcs has at most nonisolated vertices. Our constructions prescribe adjacency or composition directly from ; finite exceptions are specified by certified lists of arcs. The results also include separate probabilistic and deterministic derandomization statements. Time bounds establish termination and, in several families, stronger guarantees. Optimization of delivery time is a separate problem, discussed in the companion.
The original problem and a layered subset construction arose in Alexandra Ignatova’s 2023 project, mentored by Angel Raychev. A public 2023 abstract records that provenance (Ignatova 2023); the retained manuscript is dated February 2024 (Ignatova 2024). Ignatova and Raychev had already established the upper bound and investigated two-in/two-out-regular constructions. This account reconstructs that bound, distinguishes the original construction from its corrected analysis, and supplies new attaining families among the September 2026 extensions. The present account completes the joint extremal classification with explicit attaining constructions.
Relation to pursuit games and reachability
Destination-based pursuit has a classical antecedent in the cat-and-mouse game. Chandra and Stockmeyer’s work on alternation introduced a directed version (Chandra and Stockmeyer 1976). Huq gives proofs of P-completeness for directed and undirected variants and explicitly compares their rules (Huq 2015). In Huq’s formulation the cat moves first, repeated positions give a draw, and players traverse edges rather than wait. The earlier variant allows waiting, has the mouse move first, and forbids the cat from occupying the hole. Here the pursuer may occupy the recipient: receipt still wins immediately. We quantify over every permitted initial pursuer position and count guaranteed ordered pairs, rather than decide the winner of one prescribed initial position. We do not transfer a complexity classification between these rule sets.
The traditional Cops and Robbers game studies capture or indefinite evasion; see Bonato and Nowakowski (Bonato and Nowakowski 2011). Delivery requires reaching a specified vertex, so an evasion strategy or a usual cop-win characterization alone does not resolve our question. Once the recipient is fixed, the present game is a finite reachability game on positions of both players and the turn. Its attractor and rank-certificate arguments are standard finite-game methods (Berwanger 2009). Our extremal question concerns their simultaneous consequences for all source–recipient pairs and all graphs with prescribed vertex and arc counts.
The difficulty is not a shortage of paths alone. An additional arc can provide a route to the messenger while also enabling an interception by the pursuer. Accordingly, neither nor the validity of an attaining construction is monotone under arbitrary addition of arcs. We address this by proving strategies against a larger permitted pursuer graph while restricting the messenger to a compulsory subgraph. Every graph between those two graphs then inherits the same guarantee. The separating set viewpoint also connects the two-move constructions to earlier work on separating systems and oriented diameter-two graphs (Bollobás and Scott 2006); the directed safety condition remains an additional requirement in the present game.
Proof roadmap
The complete formula and finite tables appear first. Source/sink deletion and live-row/live-column counting provide the sparse upper bounds, while counting failed pairs in the missing-arc graph gives the dense staircase. Periodic local strategies attain the sparse endpoints; robust circles and hub/guide constructions cover the intervening budgets. Missing-arc cores and functional attachments attain the dense band. Finally, degree-profile reductions and complete finite exclusions establish the exceptional small values. The verification section specifies which steps have ordinary proofs, which use finite computation, and which have Lean verification.
Results and proof boundaries
Complete classification. For every and , we determine and supply an explicit attaining graph. The combined formula below covers every order ; the complete finite tables cover orders one through eleven. Ordinary parameterized constructions cover the infinite ranges. Certified listed graphs cover the genuine finite exceptions.
The classification has two ingredients:
- A formula at every order from twelve. Put for . The small-budget table specifies these 24 constants. For larger budgets, the sparse parity formulas, missing-pair main interval, final dense staircase, and zero range determine every value. The sparse graph is padded with isolates; the other cases use the stated circle, stage, hub, code, and dense-block recipes. The main formula starts sharply at twelve because ; the dense staircase starts sharply at eleven. The full main interval has no uniform two-move deadline.
- Complete small-host values. The finite sparse-budget theorem settles the global values at twelve through twenty-one arrows. Source/sink deletion, live-row and live-column capacities, and complete joint-degree exclusions resolve the exceptional smaller hosts. The finite tables give every remaining value, with literal adjacency and full winning/losing certificates. In particular, , , , , and . From twelve onward, .
Both parts include constructions with parameters fixed by . Separate reproducibility checks verify the numerical coverage and the availability of direct adjacency, prescribed composition, or a saved finite graph for each case. These checks supplement the coverage and strategy proofs; numerical equality alone is not an explicit construction.
The complete mathematical classification uses ordinary proofs and finite computer-assisted proofs. Independent reviews check the finite domain reductions, pruning, and the actual alternating game; their precise replay scopes are stated with the evidence. The Lean development formalizes selected structural implications and examples, not this entire classification.
The proof uses a shared source/sink deletion and positive-support induction for the sparse upper bounds, separated pair codes for a shorter main-interval construction, and a functional attachment identity for dense graphs. The following construction and support results retain their full parameter ranges and stronger guarantees:
- Protected routing (Theorem 54). For a specified routing set of size , put and . If , exactly incident arrows can be chosen deterministically so that every assignment of exterior arrows preserves universal two-move delivery. This gives every exact budget and subsumes the former full-vertex conditioning theorem, including its random-sampling guarantee.
- Sparse support (Theorems 56–57). With arrows, , a graph outside the -vertex two-regular shape has . With arrows, , a graph with reduces to a -vertex induced core with at least the same score, or to three specified -vertex degree families. A stronger original-graph reduction shows that, for , a graph with arrows and already has exactly nonisolated vertices, allowing arbitrary degrees in that core. These quantitative statements retain the regular equality information and do not assume that deleting arrows preserves strategies.
- Direct dense construction (Theorem 58). Its two-move endpoint works at every . Its arbitrary-subset bridge covers at every . Two explicit residue constructions enlarge the dense envelope to missing arrows, preserving two-move delivery and every optional subset. Its first-step two-move domain is , and its original full-band domain is . Combining its blocks with root-colored cycles extends the full-band two-move domain to . Arbitrary-duration block addition and the fixed attachments give the uniform staircase from order eleven; safe-root exclusions and literal graphs determine every smaller dense-band case. The smaller-order delivery bounds remain separate.
- Antichain composition (Theorem 59). Incomparable hub subsets attach outside vertices to a fixed two-part core, preserving two-move delivery under every choice of outside arrows. The generalized theorem includes separated two-element codes: for and they give every budget from through . Their overlap with circles covers for every . The supplied larger and mixed codes retain their independent ranges; the two-move sparsity consequence is retained in the companion.
- Support concentration (Theorem 60). With , the nonisolated support has at most vertices; all but arrows lie in a core of size between and . This controls near-extremizers below the earlier exact-support cutoffs without asserting that deleting the exceptional arrows preserves delivery.
The general arguments have ordinary mathematical proofs, with the main-interval finite bridge additionally using complete independently replayed state certificates. The accompanying Lean development verifies actual-game semantics, selected bounds and exact cells, finite certificate interfaces, and strategy implications for routing and envelope constructions. The dense staircase counting inequalities and existence of attaining blocks remain ordinary proofs. Its precise formal coverage is stated below; the complete classification is not a Lean theorem.
The combined joint maximum
The sparse constructions can be placed inside a larger network by adding isolated vertices. This observation joins the arc-budget extrema to the two dense regimes and gives a single eventual formula.
Corollary 47 (complete joint classification). Let and . Put equal to the following listed value:
| 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 1 | 1 | 2 | 2 | 4 | 5 | 6 | 8 |
| 12 | 13 | 14 | 15 | 16 | 17 | 18 | 19 | 20 | 21 | 22 | 23 | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 9 | 11 | 13 | 15 | 19 | 28 | 33 | 40 | 53 | 60 | 79 | 83 |
Then Every value has an explicit attaining construction. For , the complete tables in the finite-values section supply every admissible value and its certified listed graph or specified composition.
The two formulas at agree. For even , the first formula also holds for every on every host order .
Proof. For , use the complete small-budget theorem and its listed witnesses. The finite sparse-budget theorem supplies ; its largest least attaining host is twelve. Thus every through21 is attained at every by adding isolates.
The explicit eleven-vertex, 22-arrow extremizer and its matching arc-only bound give after adding isolates. Theorem 53 gives on every host of order at least twelve.
For even , Theorem 40 constructs an attaining -vertex graph. If , add isolated vertices. This does not change : pairs between components have no delivery path; a pursuer starting at an added isolate stays there and cannot obstruct an existing delivery strategy. The arc-only upper bound supplies the matching upper bound for the joint problem.
For odd , Corollary 45.1 constructs an attaining graph on vertices. When , its support has at most vertices. Add isolates and apply the odd arc-only upper bound. This gives .
The complete main-interval theorem supplies the third case from order twelve, preserving Theorem 44 and all its earlier constructions. The complete-band corollary in the root-colored cycle section supplies the fourth from order eleven. Four moves suffice for that whole dense band; its stronger two-move corollary applies from order sixteen. Finally Theorem 13 gives zero above . The ranges cover every stated integer budget. The finite-values section and its complete source-pinned registry cover all smaller orders.
At order eleven the three initial values are For , the saved finite stages give . The displayed staircase and zero branches then cover all remaining budgets. Thus every , has an exact value and an explicit attaining graph. The special order-eleven values are proved in the small-order section; they are not obtained by extending the sparse parity formula below its hypotheses.
The two parts together determine every admissible integer pair, including the small host exceptions. Stronger optional-subset and delivery-time conclusions remain attached to the construction theorems that prove them; the classification does not transfer those properties to every other attainer of the same value.
Complete values and explicit constructions
Every admissible pair , is determined, with an explicit attaining graph. Corollary 47 gives the full formula for ; the complete finite tables cover . No numerical or explicit-construction gap remains within the stated objective.
The numerical and construction obligations were checked separately. The independent closure in research/finish-ledger-review.json preserves every previous exact value and closes all 101 former representatives. All 493,924 admissible cells in the retained audit box through order 114 have matching bounds. This finite check is supplemented by the ordinary parameterized construction proofs and host reductions; it is not used to infer an infinite theorem merely from finite success.
For budgets , the least attaining host orders are Adding isolates gives every larger host at each corresponding budget. The remaining smaller-host values are explicitly tabulated. Above those budgets, the established sparse, main, dense, and zero constructions cover the infinite ranges. The exact 23-arrow value 83 first fits at order 12.
The separate construction audit finds a concrete adjacency rule, prescribed composition, or certified listed graph for every value. It needs no generic graph search or orientation derandomization to instantiate an attainer. Fixed stages retain every-optional-subset guarantees inside their own envelopes; other constructions retain their separately proved delivery bounds. Those stronger properties are not inferred for unrelated graphs of the same score.
Finite upper proofs combine ordinary degree and source/sink arguments with complete residual graph enumerations. Their reviews distinguish full independent game replay from a second full graph enumeration and from sampled pruning tests. The exact dependencies are in the evidence guide and approved registry. The new concrete classification is not fully instantiated in Lean.
Delivery-time optimization, classification of all maximizing graphs, and a structural characterization of all guaranteed pairs remain outside this paper’s scope. Further simplification and fuller formalization do not represent unknown values or absent explicit attainers.
Complete tables through eleven vertices
These tables and interval rules determine for every admissible pair with . An em dash means , so no such loopless graph exists. At every order, for ; this rule covers any final budgets omitted below.
Orders one through seven
The three blocks list budgets zero through thirty-five. Together with the zero-tail rule, they cover every admissible budget at these orders.
| 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 1 | 0 | — | — | — | — | — | — | — | — | — | — | — |
| 2 | 0 | 0 | 0 | — | — | — | — | — | — | — | — | — |
| 3 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | — | — | — | — | — |
| 4 | 0 | 0 | 0 | 0 | 1 | 1 | 2 | 1 | 1 | 0 | 0 | 0 |
| 5 | 0 | 0 | 0 | 0 | 1 | 1 | 2 | 2 | 4 | 3 | 3 | 3 |
| 6 | 0 | 0 | 0 | 0 | 1 | 1 | 2 | 2 | 4 | 5 | 6 | 7 |
| 7 | 0 | 0 | 0 | 0 | 1 | 1 | 2 | 2 | 4 | 5 | 6 | 8 |
| 12 | 13 | 14 | 15 | 16 | 17 | 18 | 19 | 20 | 21 | 22 | 23 | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 1 | — | — | — | — | — | — | — | — | — | — | — | — |
| 2 | — | — | — | — | — | — | — | — | — | — | — | — |
| 3 | — | — | — | — | — | — | — | — | — | — | — | — |
| 4 | 0 | — | — | — | — | — | — | — | — | — | — | — |
| 5 | 2 | 2 | 2 | 1 | 0 | 0 | 0 | 0 | 0 | — | — | — |
| 6 | 7 | 6 | 7 | 6 | 6 | 6 | 6 | 4 | 4 | 4 | 4 | 3 |
| 7 | 9 | 10 | 10 | 11 | 12 | 12 | 14 | 15 | 18 | 21 | 14 | 12 |
| 24 | 25 | 26 | 27 | 28 | 29 | 30 | 31 | 32 | 33 | 34 | 35 | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 1 | — | — | — | — | — | — | — | — | — | — | — | — |
| 2 | — | — | — | — | — | — | — | — | — | — | — | — |
| 3 | — | — | — | — | — | — | — | — | — | — | — | — |
| 4 | — | — | — | — | — | — | — | — | — | — | — | — |
| 5 | — | — | — | — | — | — | — | — | — | — | — | — |
| 6 | 2 | 0 | 0 | 0 | 0 | 0 | 0 | — | — | — | — | — |
| 7 | 12 | 11 | 10 | 10 | 9 | 8 | 8 | 7 | 6 | 5 | 4 | 2 |
Orders eight through eleven: the low budgets
The next two blocks list budgets zero through twenty-three. Budget twenty-four appears with the interval data immediately afterward.
| 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 8 | 0 | 0 | 0 | 0 | 1 | 1 | 2 | 2 | 4 | 5 | 6 | 8 |
| 9 | 0 | 0 | 0 | 0 | 1 | 1 | 2 | 2 | 4 | 5 | 6 | 8 |
| 10 | 0 | 0 | 0 | 0 | 1 | 1 | 2 | 2 | 4 | 5 | 6 | 8 |
| 11 | 0 | 0 | 0 | 0 | 1 | 1 | 2 | 2 | 4 | 5 | 6 | 8 |
| 12 | 13 | 14 | 15 | 16 | 17 | 18 | 19 | 20 | 21 | 22 | 23 | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 8 | 9 | 11 | 13 | 15 | 19 | 19 | 21 | 22 | 24 | 25 | 28 | 29 |
| 9 | 9 | 11 | 13 | 15 | 19 | 24 | 33 | 35 | 37 | 39 | 40 | 44 |
| 10 | 9 | 11 | 13 | 15 | 19 | 28 | 33 | 38 | 53 | 56 | 60 | 61 |
| 11 | 9 | 11 | 13 | 15 | 19 | 28 | 33 | 40 | 53 | 58 | 79 | 78 |
| Interval of budgets | Value on that interval | ||
|---|---|---|---|
| 8 | 32 | ||
| 9 | 48 | ||
| 10 | 61 | ||
| 11 | 79 |
The remaining eight-vertex middle budgets
| 35 | 36 | 37 | 38 | 39 | 40 | |
|---|---|---|---|---|---|---|
| 8 | 19 | 18 | 16 | 15 | 14 | 12 |
The small dense tails
Put . The entries below give ; the preceding intervals already include at orders nine and ten, and the eight-vertex endpoint appears above.
| 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | |
|---|---|---|---|---|---|---|---|---|---|---|
| 8 | 11 | 10 | 9 | 8 | 7 | 6 | 4 | 3 | 0 | 0 |
| 9 | 14 | 12 | 11 | 10 | 9 | 8 | 6 | 5 | 3 | 0 |
| 10 | 16 | 15 | 14 | 12 | 11 | 10 | 8 | 7 | 5 | 4 |
At order eleven the uniform staircase applies throughout the remaining nonzero tail. For and ,
For , the value is zero.
The uniform classification from twelve vertices
Every entry of the small-arrow table below has an explicit attainer on at most twelve vertices. Consequently it equals for every at that budget, as well as the unrestricted-host maximum .
| 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 1 | 1 | 2 | 2 | 4 | 5 | 6 | 8 |
| 12 | 13 | 14 | 15 | 16 | 17 | 18 | 19 | 20 | 21 | 22 | 23 | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 9 | 11 | 13 | 15 | 19 | 28 | 33 | 40 | 53 | 60 | 79 | 83 |
For and , put , and, in the dense band, . Then
The sparse formulas have fitting even- and odd-budget cores: in the even case and in the odd case. The complete main-interval theorem and the staircase theorem from order eleven cover the next two bands. The small-arrow attainers extend by isolated vertices. Conversely, removing isolated vertices leaves at most vertices when , so the finite ledger and isolate invariance also establish the unrestricted-host upper bounds in the small-arrow table. At every graph has value zero.
Provenance and attainment
The values are generated from the complete classification ledger, publication/classification-coverage.json, by src/finite_value_tables.py, using an independent affine-segment decoder. The generator refuses unresolved cells, checks that the displayed tables and intervals cover all 451 admissible cells through order eleven, and checks the uniform formulas against every stored order from twelve onward. It also requires a fresh explicit-construction audit, research/explicit-construction-coverage.json, with zero known-value construction gaps. These paths identify files in the downloadable research-source archive.
The infinite statement uses the ordinary sparse constructions in paper/sparse-all-orders.md, the complete main interval in paper/main-interval-complete.md, the dense staircase in paper/dense-third.md, and the zero regime. The finite exclusions retain their individual source reviews and complete literal winning/losing rank checks in the small-case registry, research/small-case-results.json. This table readback adds no graph search and makes no new Lean claim.
Game and structural bounds
The game and its elementary structure
Let be a finite loopless digraph. Opposite arcs are allowed. A legal move from goes to or to an outgoing neighbor; write Fix and . If , receipt has already occurred. Otherwise the messenger moves first. On its turn it chooses . If , delivery wins immediately. If and , it is captured. Otherwise the pursuer chooses ; equality is capture. The process repeats. Infinite play without delivery is a messenger loss.
Let mean that, for every initial , there exists a messenger strategy guaranteeing delivery against every pursuer strategy. The messenger observes ; its strategy may depend on it. Then If counts all guaranteed pairs including the diagonal, then exactly
The terminal rule matters. In the directed diamond , , the messenger chooses the intermediate vertex not occupied by the pursuer and delivers on its next turn. But reaching a vertex that would be safe as a recipient does not justify using it as an intermediate stop. The pursuer gets an intervening move before the message can be forwarded again.
Camping obstructions
Lemma 1 (source domination). If and , there is no guaranteed indirect pair with source .
Proof. The pursuer starts at and waits while the messenger waits. Every nonterminal departure from is either an immediate collision or is captured on the following pursuer turn. Waiting forever is not delivery.
Lemma 2 (predecessor domination). Put . If , an indirect guaranteed source for must equal .
Proof. For any other source the pursuer may start at . Every indirect delivery must first enter , where the pursuer can capture before the next messenger turn.
In particular, a source counted by has outdegree at least two, and a recipient counted by has indegree at least two. An indegree-one recipient is blocked by its unique predecessor. In an undirected network, interpreted as two opposite arcs per edge, the pursuer can start at and catch the messenger upon its first arrival at a neighbor of . Thus for every such network.
The two degree conditions are necessary, not sufficient. Neither the absence of a one-vertex directed separator nor the existence of two internally disjoint routes characterizes this game. Adding to the diamond destroys its only indirect guarantee, although both routes remain. Consequently is not monotone under adding arcs.
Lemma 3 (two-move criterion). For an indirect pair , put . Delivery is guaranteed within two messenger moves exactly when
Proof. Choose an intermediate vertex of , survive every pursuer response, and deliver. Conversely, any successful two-move indirect delivery must use such an intermediate. Waiting on the first move cannot reach a nonadjacent recipient on the second.
Components, zero minima, and the vertex bound
Removing isolated vertices preserves . More generally, There are no cross-component routes; a pursuer in the other component cannot interfere with a route in the messenger’s component.
Proposition 4. At every admissible the minimum of is zero.
Proof. For , list all nonloop arcs row by row and retain the first . There are full outgoing rows, at most one partial row, and empty rows. Full rows have only direct recipients; empty rows cannot move. If a full row exists, its vertex blocks every indirect attempt from the partial row by Lemma 1. Otherwise successors of the partial row have no outgoing arcs, so no indirect route exists. The empty and one-vertex cases are immediate.
Theorem 5 (original upper bound). For every ,
Proof. A recipient of indegree zero or one has no indirect guaranteed sources. A recipient of indegree has at most , after excluding itself and its direct predecessors. Sum over recipients.
For , equality forces every recipient to have indegree two and every missing pair to be guaranteed. Every source must then have outdegree at least two; the degree sum forces outdegree exactly two. Conversely, a two-in/two-out-regular graph with every pair guaranteed attains equality. Thus attaining the vertex bound is exactly a sparse universal-delivery construction problem.
Sharp arc-budget upper bounds
The source/sink and positive-support lemma below bounds an actual source/sink graph by preceding arc budgets and a positive-degree graph by its eligible rectangle. Its ordinary induction proves the following bounds and equality shapes before deriving the stronger support results. The induction starts from the elementary results through six arrows; it uses no finite extremum as a premise.
Theorem 6. If and , then
Theorem 7. If and , then
Proof of Theorems 6 and 7. Apply the ordinary sparse parity proposition, whose proof is the increasing-budget induction (56.2)–(56.6).
Theorem 8. For , equality in Theorem 6 holds exactly when deleting isolated vertices leaves a two-in/two-out-regular graph on vertices with every pair guaranteed.
Theorem 9. For , equality in Theorem 7 holds exactly when the nonisolated support has vertices; one vertex has outdegree one and indegree two; a different vertex has indegree one and outdegree two; every other degree is two; is absent; and every missing pair from an outdegree-two source to an indegree-two recipient is guaranteed.
Proof of Theorems 8 and 9. The same parity proposition proves the equality shapes. In even support the number of missing pairs is . In the odd absent-arrow family the eligible count is ; every other shape has a strictly smaller upper bound. The stated guarantees therefore characterize equality.
Adding the absent in Theorem 9 gives a two-regular digraph. It does not follow that the completed graph is universally winning.
A common upper-bound argument for sparse graphs
The same source/sink deletion and positive-degree count prove the sharp arc bounds, their equality shapes, and the quantitative support reductions. All graphs are simple and loopless; opposite arrows are allowed. An induced subgraph retains every arrow between its vertices.
Put , , , , , and . Camping excludes every counted pair outside . Direct and diagonal pairs are disjoint, so
Deletion and positive support
Lemma (source/sink and positive-support bounds). Write . An actual source of outgoing degree , or an actual sink of incoming degree , satisfies On a fixed support of order , the added term may also be replaced by . Consequently every graph with a nonisolated source or sink obeys If every indegree and outdegree is positive, then Here .
Proof. An old-source messenger cannot enter a deleted source. A messenger delivering to an old recipient cannot enter a deleted sink and subsequently leave it. Restrict the cop to the remaining graph: every counted pair with both endpoints surviving therefore remains a guarantee there. Only the deleted source row or sink column can add pairs.
Every live recipient column needs two predecessors of positive indegree. An indegree-zero predecessor cannot be reached after the initial position, and starting there would make the pair direct. If there is only one usable predecessor, a cop may camp there. Separately, every live source row needs two nonsink successors: a cop camps at a sole nonsink successor, while every alternative departure traps the messenger at a sink. Thus the deleted source’s arrows supply none of the first capacity, and the deleted sink’s arrows supply none of the second. At most columns or rows can contribute. For the deleted row or column is empty; simply counts its nonadjacent distinct pairs.
Adding a fresh sink with one incoming arrow preserves . An old winning strategy works while the cop stays in the old graph; if the cop enters or starts at the sink, it is trapped and any old route to the recipient suffices. Old losing pairs retain a cop strategy confined to the old graph, and the new sink contributes no indirect row or column. Hence is nondecreasing, which gives (56.3). This is a budget comparison, not arbitrary arrow deletion.
For positive degrees, the vertices outside each active set have the corresponding degree one. This gives and where counts arrows from ’s complement to ’s complement. Subtract this lower bound and from the eligible rectangle. The two deletion arguments used the original arrow directions throughout; no graph-reversal assumption is needed.
Arithmetic lemma. In positive support the following bounds hold: For the odd support reduction, the first odd bound remains valid at , and at a coordinate below gives . For , positive support at seven arrows has .
Proof. In (56.4), increasing either coordinate when the other is at least two cannot decrease the expression: its product increases by at least two, while the two positive-part subtractions increase by at most two. At the fixed supports, substitute the largest permitted coordinates. Coordinates zero or one give and are bounded separately. For , infeasible small coordinates can be discarded using and its incoming counterpart. At , is impossible and the nonmaximal-coordinate bound at is one. At , the corresponding bounds at are one and four. These are the only small fixed-support cases outside the uniform substitution.
For the large-support cases put . Then and If both coordinates are at least two, their maximum is bounded by ; otherwise . Moreover , so is nondecreasing for . The values at are immediate. Since in both large-support cases, substitution at gives (56.5); its value also dominates in the stated domains. At , the possibilities give the separate bound three.
Ordinary induction for the parity bounds
Proposition (sparse parity bounds and equality). For every , Even equality forces a two-in/two-out-regular nonisolated support of order , with every missing pair guaranteed. Odd equality forces support , with distinct vertices of respective degree pairs , every other degree two, absent, and every eligible missing pair guaranteed. These conditions also suffice.
Proof. The elementary ordinary results through six arrows give . Applying (56.3)–(56.4) successively gives These small integer maxima require only , , and (56.4); they enumerate no graphs. Thus the seeds at ten and eleven arrows are ordinary and do not use their sharper finite values.
Induct in the arrow budget. At , (56.3) gives . Positive support has fewer than missing pairs; is bounded by (56.5). At , the missing-pair bound is , and a coordinate below gives the smaller first bound in (56.5). Hence equality requires , which forces every degree two, and all its missing pairs to win.
At , the deletion bound is at most Positive has at most missing pairs, and is bounded by (56.5). At , a coordinate below again gives a strict bound. For , the degree sums force exactly one degree-one vertex on each side. If these coincide, ; otherwise . Since , the eligible count is in the first case and in the second. Here is precisely the possible arrow from the low-outdegree vertex to the low-indegree vertex. This proves the bound and equality statement. The seed cases have the same strict support and deletion comparisons.
A gap before another even support shape can compete
Theorem 56 (even sparse stability). Let and let have exactly arcs. At least one of the following holds:
- Deleting isolated vertices leaves a graph on exactly vertices, with indegree and outdegree two at every vertex.
- .
Proof. Put . The parity induction and (56.3) bound every source/sink graph by . In positive support, has at most missing pairs. At , every nonregular shape has ; at , (56.5) gives . Only the stated regular support remains.
Thus forces that shape; it does not itself assert universal delivery. The same dichotomy holds at using the finite value . It fails at : the six-vertex, eight-arrow witness has . The theorem for is entirely ordinary.
Corollary 56.1. For , For example the retained finite core bounds give , , , and . These weaker consequences are superseded numerically by the finite-budget classification, but retain their separate support interpretation.
Three odd exception families and an induced core
Theorem 57 (odd sparse support reduction). Let , let have arcs, and suppose . Then at least one holds:
- has an induced -vertex subgraph with . Either is two-in/two-out regular with arcs, or it has arcs, one outgoing degree three and one incoming degree three, and all other corresponding degrees two. The exceptional vertices may coincide.
- Removing isolates leaves vertices, with distinct vertices of degree pairs and all other degrees two. The two possibilities absent or present are separate families.
- Removing isolates leaves vertices, with one vertex of indegree and outdegree one and all other degrees two.
Proof. Put . A source/sink of other degree at least two gives for . At the ordinary seeds give respectively and . Thus only other degree one is possible. Delete such a vertex. Its row or column contributes zero, so the remaining graph has arcs and score at least . For , Theorem 56 applies because : deleting its isolates leaves a regular -vertex induced core with at least the original score. It remains induced in , proving case 1. For , degree-one deletion is impossible since , , , respectively, are below .
Otherwise all degrees are positive. The missing-pair count excludes , and (56.5) excludes (including its seven-arrow case). At , a coordinate below gives , so and the one-excess degree pattern in case 1 follows. At , a coordinate below gives . Thus , and the degree-one vertices either differ or coincide, giving cases 2 and 3. These exhaust the graph itself, without reversing arrows or contracting routing vertices.
For , the elementary values make the conditional statement vacuous.
Corollary 57.1 (odd bound and equality shape). For , , with equality exactly in the absent-arrow distinct-exception family when every eligible missing pair is guaranteed.
Proof. This is the already proved parity proposition. Equivalently, the families in Theorem 57 have respectively at most , , , , and eligible missing pairs. Only the absent-arrow family can attain the bound.
The arithmetic checker and its separate audit record verify the finite substitutions and inequality instances used here. They supplement these ordinary proofs; they neither enumerate graphs nor supply a new Lean proof.
Quantitative concentration near the sparse optimum
The exact support alternatives in Theorems 56 and 57 apply above specific cutoffs. The following estimate continues below those cutoffs. It says that losing only a linear number of pairs from the leading quadratic bound forces only a bounded number of exceptional vertices and arrows. It makes no claim that deleting those exceptions preserves a delivery strategy.
Theorem 60. Let have arrows and . Put If and count the source rows and recipient columns containing at least one guaranteed indirect pair, then Define . The induced core satisfies The graph has at most nonisolated vertices, and at most arrows have an endpoint outside .
Proof. Only vertices in can supply nonzero indirect source rows, and only vertices in can supply nonzero recipient columns. These are the usual camping obstructions at degree zero or one. In particular .
At most arrows end outside , so at least vertices of have indegree zero. They emit at least arrows. Let be the total excess indegree above two inside . At most arrows end outside , and vertices of indegree at least three have total indegree at most , since for . Thus at most of the arrows can avoid indegree-two recipients. At least distinct indegree-two recipients have an indegree-zero predecessor.
Each such recipient has a zero indirect column. An indirect source cannot reach the indegree-zero predecessor and must approach through the other predecessor, where the pursuer can wait. Therefore The identity uses and the common parity of .
For the row bound, use the original arrow directions. At least members of are sinks. Their incoming arrows force outdegree-two predecessors except for at most arrows, by the same surplus count. An outdegree-two source with a sink successor has zero indirect row: the pursuer camps at the other successor. Repeating the count gives . This is not an appeal to symmetry under reversing the pursuit game. The displayed minimum bounds and follow.
Put . Since and , arithmetic–geometric mean gives . The row and column estimates also imply so . Its upper bound is immediate.
Every nonisolated vertex outside contributes at least one to its incoming plus outgoing degree. Outgoing degrees outside total at most , and incoming degrees outside total at most . There are therefore at most such vertices. The nonisolated support is at most Finally, the number of arrows with tail outside is at most , and the analogous incoming count is at most . Counting an arrow twice can only increase this estimate. The number of arrows outside the induced core is thus at most This proves all assertions.
For example, if and with , then . Thus the support has at most vertices and all but arrows lie inside a core of at most vertices. The constants above are explicit but are not asserted to be optimal. Theorems 56 and 57 retain their sharper conclusions in their stated ranges. In particular, this concentration estimate does not supply the game restriction that is proved under the more specific hypotheses of Theorem 57.
The argument was independently reviewed and checked against both game solvers on all 4,165 labelled loopless digraphs through four vertices and 181 additional graphs. The ordinary proof, finite tests, and exact integer comparisons are recorded in research/routing-defect-phase2-support.md and its two verification receipts. This theorem is not presently formalized in Lean.
A bounded host for every remaining small budget
The refined outside-vertex counts in the small sparse section make a stronger finite reduction possible. This is a reduction of the whole extremal problem, not a claim that an arbitrary induced core preserves a strategy.
Corollary 60.1. For , define by Then, for every admissible host order, An explicit graph attaining the value on vertices supplies an explicit attainer on every larger host by adding isolated vertices.
Proof. The saved lower scores at these ten budgets are, respectively, They are attained on respectively vertices. The 19-arrow witness is the disjoint union of the nine-vertex, 18-arrow graph and a single directed arrow. Every listed support is at most .
Apply the refined necessary integer-profile bounds to a graph scoring strictly more than the listed lower score. Complete enumeration of the integer parameters, independently implemented in two ways, bounds its nonisolated support by This enumerates degree counts, not graphs. Every actual graph has one of the enumerated tuples; a surviving tuple need not be realizable.
Only the 20-arrow bound needs a further observation. Its sole possible 13-vertex tuple has a nine-vertex core in which every vertex has indegree and outdegree two, together with two one-arrow sources and two one-arrow sinks. The eligible source–recipient rectangle has at most 56 pairs. An arrow from an outside source into the core kills a whole indirect recipient column: a core source can reach at most the other predecessor, where the pursuer waits. An arrow from the core to an outside sink kills the corresponding source row. Each such row or column contains at least six eligible pairs, leaving at most 50 guarantees. If neither interaction occurs, the core has 18 arrows and the outside arrows form a separate zero-count component. Then . Neither case can beat 53, so every improvement has support at most twelve at budget twenty. The twenty-arrow host-compression proposition in the small sparse section then replaces its only surviving twelve-vertex form by an eleven-vertex graph of the same score, using a fresh sink. This gives ; it does not claim that every improving graph already has support eleven.
For , take any -vertex graph. If its score is no greater than the saved lower score, the saved witness already matches or improves it on at most vertices. Otherwise delete only its isolated vertices, using the proved support bound, using the compression at budget twenty when needed, and pad to if necessary. This proves ; adding isolates proves the reverse inequality. For the assertion is an identity.
The exact arithmetic, literal lower witnesses and independent replays are indexed in research/small-case-results.json. Together with the complete joint coverage from order eleven, this confines every remaining unknown numerical value to a host of order at most eighteen. The separate recipe audit is still required: a numerical reduction alone would not prove that an infinite known-value domain has explicit constructions.
Sparse attaining constructions
Sparse constructions with a linear deficit
A safe branching principle
Lemma 10. Suppose distinct vertices have closed move sets intersecting in at most one vertex. If a vertex has two distinct outgoing neighbors that each guarantee delivery to , then guarantees delivery to .
Proof. For every pursuer position , one of the two successors lies outside . Move there. It survives every intervening pursuer response, after which its guaranteed strategy applies. If the chosen vertex is , delivery is already terminal. This is a finite concatenation of actual strategies.
Theorem 11. Let , , , and . The digraph on with outgoing steps has every pair guaranteed. It has arcs and
Proof. The positive differences in are all distinct. Since , no positive difference coincides modulo with a negative one. Distinct closed move sets therefore intersect in at most one vertex.
Translate the recipient to zero. Vertices are already delivered or have direct arcs to it. Vertex is guaranteed via its neighbors . Thus all four vertices are guaranteed for . If is guaranteed, apply Lemma 10 in the following order:
| New source | Two guaranteed successors |
|---|---|
This proves . Iterating at most times covers every vertex because is coprime to . The induction is finite; it supplies terminating strategies, not merely perpetual evasion. Finally subtract the diagonal pairs and arcs from .
The choice proves the theorem for every not divisible by seven. Adding an isolated vertex gives a linear-deficit construction for the remaining large sizes as well. The next elementary lemma removes that padding and improves the constant.
Lemma 12. For every , there is an odd integer with and .
The proof and its explicit choices are included in the construction appendix below. Taking gives, for every , These estimates motivate the sharper endpoint result: Theorem 40 subsequently proves equality in the upper bound for every .
Local strategies on cyclic graphs
The following lemmas separate the finite strategy certificates from the ordinary simulation and composition arguments used by the sparse families.
Lemma (local simulation). Represent actual delivery-game states by states of a local alternating arena, preserving the player to move. A local winning strategy applies to the actual game if:
- Its selected messenger moves lift to legal actual moves with the prescribed represented successors.
- Every actual pursuer response has a permitted local image, and nonterminal collisions are preserved.
- Local delivery success means actual receipt; local safe handoff means a noncollision messenger turn after the pursuer response, satisfying the next module’s source requirements.
Its messenger-move bound is preserved. Encountering the actual recipient inside a handoff module instead ends play immediately, before collision.
Proof. The first two conditions represent every actual play following the strategy by a legal local play; the third identifies its success. Termination follows from the certified nonnegative ranks. Both conventions used below suffice: strict descent at each nonterminal half-move, or strict descent at messenger moves and nonincrease at pursuer responses. The latter strictly decreases rank each round. Rank zero requires the stated success; nonterminal collision states cannot be winning. In particular, a handoff is not complete until the pursuer reply has been survived.
Lemma (window projection). Represent a pursuer exactly in columns of a ring of circumference , and otherwise by . Confine the messenger to , where . Suppose actual pursuer jumps have absolute column displacement at most , and the local arena includes their represented moves, sends exits to , and allows to wait or enter any existing vertex in either boundary’s layers. If every actual pursuer move projects legally and no collision is concealed. Selected messenger moves must separately lift legally.
Proof. Represented columns are distinct. A wrapped jump between their opposite ends would need displacement at least . Outside moves project to waiting at or entry into a permitted boundary layer; other moves are literal or exits. Every messenger position lies in the exact pursuer window, so collisions are detected.
For a single periodically repeated defect, include all changed outgoing tails, deleted vertices and exceptional source or recipient positions in its relative support . A window meets only anchors in . Hence allows at most one periodic copy to affect the window. Certifying those anchors and the unchanged arena supplies a module at every center, subject to the move inclusions above. Several nearby defects instead require a proved covering list of local crops.
Theorem (cyclic strategy composition). Fix a recipient and an orientation of its columns. Delivery-entry columns form a consecutive block of length . From every eligible state outside this block, suppose a simulated transfer uses at most messenger moves and ends at a safe handoff advancing by some step in , with . From every eligible entry state, suppose simulated delivery uses at most moves. Modules cover all noncollision pursuer starts, and transfers preserve messenger eligibility. Then delivery takes at most messenger moves.
Proof. Outside the entry block, use the forward distance to its first column as potential; it is at most . A transfer either decreases it or enters the block, since a step of size at most cannot skip the whole block. Thus at most phases suffice. Each handoff preserves turn, eligibility and a pursuer position covered by the next module. Recenter between modules, then deliver. Earlier receipt only shortens play, and summing the local bounds gives the estimate.
Unit transfers therefore need at most phases for one entry column and for two adjacent entries. Progress of one or two likewise reaches two adjacent entries within phases; it need not reach one specified column. Eligibility can exclude particular messenger types or vertices, as in the odd construction.
For optional arrows, restrict the messenger to compulsory moves and give the local pursuer every optional move: every intermediate graph then satisfies the simulation inclusions. Omitting an external defect is sound only if the selected messenger moves remain legal and all actual pursuer responses remain represented. The following chapters check these construction-specific facts and retain every finite certificate premise.
An infinite family attaining the sparse bounds
The five-type graph used in the dense construction also attains the sparse vertex and arc-budget bounds. This requires a different strategy: its messenger may need to travel around a substantial part of the ring. The proof combines fixed local certificates with a simulation valid at every sufficiently large circumference, followed by six finite base cases.
For clarity, define the sparse graph again. Its vertices are The first outgoing arc follows the cycle The second outgoing arc is specified by Both arc maps are permutations, are loopless, and have distinct images at every vertex when . Hence has vertices and arcs, with indegree and outdegree two everywhere. Waiting is an additional legal action, as throughout the paper.
Theorem 21 (uniform sparse attainment). For every integer , every source–recipient pair in is guaranteed. Consequently For , a sufficient delivery time is messenger moves. The theorem is computer-assisted: its finite ingredients are the two local objectives specified below and the six rings .
The stronger local arena
Unwrap the column coordinate to the integers, retaining the same two arc rules. Confine the messenger to columns , disallowing moves out of this interval. Represent the pursuer by its exact vertex in columns , together with an exterior state . Thus there are 35 messenger positions and 46 pursuer positions.
Within its nine-column window the pursuer has all its usual moves and its wait; a move leaving the window goes to . From it may wait or enter any vertex of either boundary column or . This grants more freedom than a particular physical pursuer outside the window. The messenger and can never coincide.
The objectives are safe handoff in column zero and immediate delivery to , with the distinct stopping rules of local simulation. The certificates use strict half-move rank descent, seeding handoff only at noncollision messenger turns and receipt before collision.
The checked finite bounds are:
| Local objective | Initial column | Initial noncollision states | Maximum messenger moves |
|---|---|---|---|
| Safe transfer to column zero | 1 | 225 | 8 |
| Delivery to | 2 | 225 | 24 |
| Delivery to | 2 | 225 | 16 |
| Delivery to | 2 | 225 | 16 |
| Delivery to | 2 | 225 | 17 |
| Delivery to | 2 | 225 | 18 |
Each row covers all five source types and all 46 pursuer states other than the source itself. In particular, it includes an initially exterior pursuer. Only the bounds 8 and 24 are needed below; optimality of these local times is not claimed as a separate result.
Projection to a ring
Apply the window-projection lemma with , , and circumference . Both arrow rules lift literally, so every selected messenger move is legal. The local-simulation lemma therefore transfers both objectives to every translated window. At the boundary columns have wraparound adjacencies, which is why smaller rings retain separate finite certificates.
Composition and termination
Proof of Theorem 21. Relative to a recipient in column zero, transfers move one column backward and delivery starts in column two. All source types are eligible. Cyclic strategy composition with , and gives the bound messenger moves.
For , the explicit finite-ring certificates verify every source and pursuer position for each of the five recipient types in column zero. Translating columns gives every recipient. These six checks, together with the uniform argument for , establish universality for all .
Finally, a universal graph with vertices and arcs has The vertex upper bound and the even arc-budget upper bound both equal this number. Hence both asserted extremal equalities follow.
Certificate reproduction and scope. The file research/five-type-certificates.json contains the fixed local arena, ranks, and chosen messenger moves, generated and directly checked by src/five_type_certificate.py. The independent implementation src/five_type_local_verify.py constructs the explicit alternating-state graph from the arc rules and checks every winning rank condition, as well as closure of the losing region. Its full ranks and selected moves are saved in research/five-type-independent-local-certificates.json, together with the implementation hash. Both implementations agree on the six local bounds above. The six finite bases are stored in research/five-type-small-ring-certificates.json, including complete arc lists, messenger-move layers, and explicit alternating-state rank certificates for the five representative recipient types. The script src/five_type_small_certificates.py reproduces those checks using both game solvers and verifies every certificate transition. The ordinary projection and composition proof explains why these finite arrays certify infinitely many rings. This theorem is not currently claimed as a Lean formalization.
Corollary 22 (sharp arc-budget leading term). As , More explicitly, for every ,
Proof. Set and , so . Take together with disjoint one-way arcs. Each added component has no indirect guaranteed pair, and additivity over components preserves . This graph has exactly arcs and The upper bound follows because there are at most possible sources and at most that many possible recipients of indirect guaranteed pairs. Thus the quadratic coefficient is sharp for arbitrary arc counts, not only the progression .
Theorem 40 proves exact vertex maxima at every order from twelve and exact even arc maxima from 24 arcs; Corollary 45.1 proves exact odd arc maxima from 25 arcs. The padding argument above is retained as a direct proof of the leading term. The remaining small exceptions are stated in the current result summary.
Sparse endpoint attainment at every order from twelve
A second periodic construction admits controlled removal of vertices. Unlike a finite modification checked at one circumference, the removal is certified in a fixed local game that applies at every translated position. Separating the removals then provides all residue classes of the vertex count.
Theorem 40 (with finite certificates). For every integer , there is an explicit two-in/two-out-regular universally winning digraph on vertices. Consequently Every source–recipient pair in the construction can be guaranteed within messenger moves.
Proof. First construct a uniform family for . Begin with columns, indexed modulo , containing vertices of types . One permutation follows the Hamilton cycle The other permutation has arcs Choose columns whose consecutive cyclic gaps are at least three. At each , remove and smooth its path separately in the two permutations: All remaining arcs stay unchanged. The resulting graph has vertices. Smoothing preserves each permutation’s bijectivity. There are no loops or coincident outgoing arcs: the modified first-permutation arc leaves type three for type five, while its other arc ends at type zero; the modified second-permutation arc leaves type one for type two two columns ahead, while its first-permutation arc ends at type two in the same column. Thus the graph remains simple and two-in/two-out regular.
We establish a uniform strategy when . Around an arbitrary reference column zero, restrict the messenger to columns and represent the pursuer in columns , together with a state for all outside positions. Retain both players’ waits and graph arcs. Messenger moves leaving its window are disallowed; pursuer moves leaving its window lead to . From allow waiting and entry at any existing vertex in columns .
The removals inside the represented pursuer window form a subset of with consecutive gaps at least three. There are exactly 189 such subsets. For every one of these patterns, the following finite local claims have complete rank certificates:
| Objective | Initial messenger column | Maximum messenger moves |
|---|---|---|
| Reach column zero safely at the start of a messenger turn | ||
| Deliver to any specified existing vertex in column zero |
Each claim covers every existing initial messenger type and every noncolliding initial pursuer position, including . Safe-transfer goals are seeded only at messenger turns, after the preceding pursuer response. Delivery goals instead use immediate receipt before collision. There are 1,287 certificates: seven objectives for each of the 189 patterns, with delivery to omitted in the 36 patterns where that vertex is removed. An independent explicit alternating-state implementation verifies all 560,885 required initial states and all 10,271,740 states of these finite games, including winning rank descent and losing-region closure.
The window-projection lemma applies with , , and . It remains to check that selecting a crop neither removes an actual pursuer move nor supplies an illegal messenger move.
A removal outside the represented window does not change any represented-to-represented arc. The only change to an outward arc occurs when removing redirects to ; both heads represent . Outside-to-inside changes are already included among its permitted boundary entries. At the messenger boundary, any analogous changed outgoing arc still leaves the allowed messenger window. The local model therefore depends only on the removals inside the pursuer window. Their consecutive gaps are at least three, so it always has one of the 189 certified patterns.
All existing messenger types are covered by each certified crop. Transfers advance one column, and delivery starts two columns before the recipient. Cyclic strategy composition with , and therefore gives This proves universal winning for every permitted set .
Finally, given , put and . Then and . Choose when , and take empty when . The displayed gaps are three, and the wraparound gap is at least . The graph has exactly vertices and arcs. Universal winning gives , and the vertex and even arc-budget upper bounds give the three stated equalities for .
The complete primary certificates and their direct checker are research/sparse-composition-multi-certificates.json.gz and src/sparse_composition_multi_certificate.py. The independently written verifier uses direct arc formulas and an explicit alternating graph: src/six_type_independent_spacing.py, with full ranks in research/six-type-independent-spacing-3-certificates.json.gz and a summary in research/six-type-independent-spacing-3-summary.json. The graph definition, spacing argument and simulation are ordinary proofs; the two bounded local claims depend on the finite certificates. No Lean formalization of this theorem is asserted.
For completeness, the finite range is supplied by 73 explicit graphs. Each graph has distinct nonloop arcs and both incoming and outgoing degrees two. Two independent exact game algorithms agree, and every actual-game rank obligation is checked for every recipient and every allowed initial pursuer. The finite witnesses also satisfy the displayed delivery-time bound. Their arc lists are in research/sparse-finite-bridge-witnesses.json, the complete ranks in research/sparse-finite-bridge-certificates.jsonl.gz, and the verification receipt in research/sparse-finite-bridge-verification.json. The unified generator src/sparse_finite_bridge_construct.py returns the corresponding finite witness below 85 and the uniform construction above it. This proves the remaining finite cases of the theorem.
Together with the complete small-order tables, this settles the vertex maximum at every order. The separate Theorem 45 addresses the odd arc-budget bound. Both its finite bridge and uniform local certificates remain outside the current Lean coverage.
The odd endpoint and completion of its degree defect
The odd arc-budget equality theorem prescribes a particularly small defect: on vertices there is one vertex of outdegree one, a different vertex of indegree one, all other indicated degrees are two, and the arc is absent. The candidate extremal value is The equality theorem reduces attainment to guaranteeing every missing pair whose source differs from and whose recipient differs from . It does not make arbitrary deletion from, or completion to, a two-regular graph preserve the relevant guarantees.
Two necessary structural properties
Lemma. Every odd-extremal graph with the preceding degree pattern is strongly connected. Moreover, for each vertex , the graph with deleted has a directed path from every to every .
Proof. Each such ordered pair with is either a direct arc or a guaranteed missing pair. Against a pursuer initially at and waiting there, any successful delivery path avoids internally. Since its endpoints differ from , it gives the asserted path in the deleted graph.
To prove strong connectivity without deleting a vertex, all vertices different from already reach all vertices different from . The unique predecessor of is different from , because is absent. Thus all vertices other than reach by first reaching . The unique successor of differs from , and reaches every vertex by first going to .
These are necessary conditions, not substitutes for the full game: the pursuer can move, so ordinary connectivity and stationary separators do not establish an attaining strategy.
Completing an odd extremizer can fail
Proposition (finite certified example). There is a graph on 19 vertices with 37 arcs attaining such that adding the unique degree-completing arc yields a two-in/two-out graph which is not universally winning. Its completed indirect count is 276, whereas a universally winning two-regular graph on 19 vertices would have 304.
The example has vertex set and the following outgoing neighbors:
| Vertex | Outgoing neighbors | Vertex | Outgoing neighbors |
|---|---|---|---|
| 0 | 5, 12 | 10 | 2, 17 |
| 1 | 15, 10 | 11 | 1, 6 |
| 2 | 7, 0 | 12 | 3, 8 |
| 3 | 1, 18 | 13 | 4, 5 |
| 4 | 15 | 14 | 4, 12 |
| 5 | 11, 9 | 15 | 0, 16 |
| 6 | 8, 13 | 16 | 7, 9 |
| 7 | 13, 17 | 17 | 14, 11 |
| 8 | 10, 16 | 18 | 2, 6 |
| 9 | 3, 14 |
Its exceptional vertices are and . The finite actual-game certificate verifies every guarantee required by odd equality and the count 272. The upper bound follows from Theorem 7 with .
There is also a short ordinary obstruction after adding . Fix recipient zero and start the messenger at 1, the pursuer at 4. Define The following four classes of messenger-turn states form a pursuer trap: They contain the initial state and exclude every state where the messenger has reached zero. The pursuer acts as follows, in terms of the messenger’s new vertex :
| Current pursuer | Response |
|---|---|
| 4 | If , move to 18. If or , capture at . Otherwise wait at 4. |
| 18 | If , capture there. If , move to 6. If , wait. |
| 6 | If or , move to 13. If , wait. |
| 13 | If , move to 4, capturing if . Otherwise wait at 13. |
An immediate collision with the current pursuer already loses. Direct inspection of the outgoing-neighbor table shows that every other possible move either permits the stated capture or returns to one of the four trap classes. Waiting is included. Since infinite play without receipt loses, the messenger cannot deliver to zero. This explicitly identifies how the new arc helps the pursuer: the transition from cop position 4 to 18 after the messenger moves from 1 to 10 was unavailable before completion.
src/odd_endpoint_completion.py contains the fixed graph and runs both independent game solvers, checking every winning rank and every losing closure obligation. research/odd-endpoint-completion-certificate.json stores the complete finite certificates for the original and completed graphs. The ordinary trap proves nonuniversality without computation; the original graph’s attainment and the completed count 276 use the verified finite certificates. This example is not presently embedded in Lean. The subsequent construction settles the odd endpoint at every sufficiently large budget.
A useful degree-preserving search operation
Given a two-in/two-out graph, split one vertex into vertices . Assign one old incoming and one old outgoing arc to each new vertex, then add . This adds one vertex and one arc, giving exactly the odd equality degree pattern: has indegree one and outdegree two, while has indegree two and outdegree one. The forbidden opposite arc is absent because the original graph was loopless.
This operation supplies a structured family to investigate, but it is not a preservation theorem. A split of the 20-vertex five-type graph attains , while all twenty canonical splits of its 30-vertex member fail to attain the corresponding odd bound. Likewise, changing the two horizontal lane speeds to three produces attaining single-arc deletions at 40 and 50 vertices but failures at neighboring and larger orders. These counterchecks prevent promoting isolated success to a uniform construction. A different six-type family supplies the following uniform positive result.
Every sufficiently large odd budget
Theorem 45 (the odd endpoint). For every integer , Equivalently, for every odd , An explicit attaining graph has vertices. Every pair required for attainment has a delivery strategy using at most messenger moves. The construction and its composition proof are ordinary finite arguments; the bounded local strategy lemmas are supplied by independently verified finite certificates.
Proof. Put and , so . The sufficient circumference for each residue is given below. We first describe a graph on the surviving vertices of . Its two initial permutations are Use the following four choices of , whose entries are in type order :
| Pattern | ||
|---|---|---|
For a set of deleted vertices, smooth each permutation separately: from a surviving vertex, follow that permutation until first reaching another surviving vertex, and use the resulting arc. Finally delete one specified arc of the smoothed graph. The complete choices are:
| Pattern | Tail of deleted arc | Which arc | Direction | |
|---|---|---|---|---|
| 0 | ||||
| 1 | ||||
| 2 | ||||
| 3 | ||||
| 4 | ||||
| 5 |
The corresponding deleted vertex sets are:
- : .
- : .
- : .
- : .
- : .
- : .
Write for the head of the final deleted arc. Every type cycle of each displayed has a nonzero total displacement with no greater than its length . Its cyclic lift has length , whereas is a cycle of length . At most five vertices are removed, so no permutation cycle disappears. The smoothing operation therefore preserves the permutation property on surviving vertices. Inspection of these six fixed patterns shows that the two smoothed images at each surviving vertex are distinct, are not the vertex itself, and change the column by at most two. The changes to outgoing arcs are confined to tails in columns ; removed vertices lie in columns . These are finite checks on the displayed tables, independent of . The sufficient circumferences are at least 15, so reduction modulo introduces neither a coincidence nor a loop. Thus the final graph has vertices, arcs, precisely one outdegree-one vertex , precisely one indegree-one vertex , and all other corresponding degrees two. Moreover and is absent.
Use the retained local certificates with messenger radius , pursuer radius , and an outside state . Both players may wait; messenger moves leaving its window are forbidden. A pursuer leaving its window goes to , which permits waiting and entry into its boundary layers. Let contain every changed outgoing tail, deleted vertex and degree-exception vertex. The exact parameters are:
| Sufficient | Transfer | Delivery | |||||
|---|---|---|---|---|---|---|---|
| 0 | 4 | 6 | 2 | 15 | 14 | 26 | |
| 1 | 4 | 6 | 1 | 15 | 9 | 22 | |
| 2 | 4 | 6 | 2 | 15 | 17 | 26 | |
| 3 | 5 | 7 | 2 | 17 | 34 | 23 | |
| 4 | 5 | 7 | 2 | 17 | 28 | 27 | |
| 5 | 5 | 7 | 2 | 18 | 9 | 26 |
The table’s support is obtained without a search: trace each removed vertex backwards in each permutation to its first surviving predecessor, and include the final deleted arc and its two endpoints. Outside those tails, outgoing arcs are unchanged. All actual column jumps are at most ; in residue zero the allowed entry depth two is conservative.
For every represented defect translation, safe transfer goes from column to column zero on a noncolliding messenger turn, excluding at both endpoints. Delivery goes from column to every surviving recipient of column zero other than , again excluding initial source . In residue five, transfer may instead end in column zero or , and delivery starts in column 2 or 3. Receipt is terminal before collision. The table lists the maximum certified messenger moves.
The frozen independent archives contain all 847 local objectives: 97 for residue zero and 750 for the nonempty patches. The direct replay checks all 470,026 required initial states, 8,417,696 alternating states, and 24,787,015 legal-transition obligations, including losing closure. For residue zero the anchors are ; for the others they are , always with an additional unchanged arena. These are finite local lemmas, not tests extrapolated over ring lengths.
The window-projection lemma and its single-defect condition require The relevant anchor interval lies within the certified anchors in every table row. On represented outgoing tails the selected one-patch arena agrees with the smoothed arrow formulas; other incoming effects are covered by the permitted exterior entries. If no patch is relevant, the unchanged arena applies. Thus local simulation holds at every center. The displayed circumferences satisfy both inequalities and cover every ; the last excluded residue representative is .
Fix a source other than and a recipient other than . Eligibility means that the messenger avoids at module starts and handoffs; every certified transfer preserves it. For , transfers advance one column in the displayed direction , and delivery starts in the single column two steps before the recipient. Cyclic strategy composition uses at most transfers. For , transfers advance one or two columns leftward, and the delivery entries are the two adjacent columns 2 and 3 relative to the recipient. The same theorem, with maximum progress two and entry-block length two, uses at most transfers. In particular, the uniform bound stated above remains valid.
Every missing pair with source different from and recipient different from is therefore guaranteed. Their number is . The odd arc-budget upper bound proves equality.
When , the same argument gives the sharper bound for all , retaining the original congruence-family theorem. The generator is src/odd_endpoint_all_residues.py; the unchanged proof archives are research/six-type-independent-odd-certificates.json.gz and research/six-type-independent-odd-residues-certificates.json.gz. src/odd_projection_threshold_check.py --check replays their full ranks, checks exact defect support and the projection inequalities, and compares its result with research/odd-projection-threshold-audit.json. The original generation receipts retain their historical threshold 145 and source hashes; no frozen certificate was regenerated or repinned. The original primary certificates are retained as additional evidence. This theorem has not been formalized in Lean.
Corollary 45.1 (the odd endpoint from 25 arcs). For every , Consequently the exact odd arc-only extremum is
Proof. Theorem 45 covers . For every one of the remaining 85 integers , the supplementary data give a fixed simple graph with arcs, one outdegree-one vertex , one different indegree-one vertex , all other corresponding degrees two, and absent. The displayed six-type residue families supply most of these graphs. Deleting one arc from independently verified finite two-regular examples supplies the remaining orders from 19 upward. Six further fixed witnesses cover orders 13 through 18.
For every recipient other than , the finite certificates specify an integer rank for every explicit messenger-turn and pursuer-turn state. Terminal receipt has rank zero, nonterminal collision has rank , and every other nonnegative messenger rank has a legal successor of smaller nonnegative rank. Every legal successor of a nonnegative pursuer rank has smaller nonnegative rank. The direct checker verifies these conditions against the original graph, together with the entire complementary losing closure. Every initial messenger state whose source differs from and whose pursuer position differs from the source has nonnegative rank. Strict rank descent therefore forces finite delivery from each required state against every pursuer policy. This proves all required guarantees for each listed graph.
The retained full archive, which also covers the now unnecessary orders 98 through 144, contains 10,236 recipient objectives and 215,967,810 explicit alternating states. The same degree count as in Theorem 45 then gives guaranteed missing pairs. The arc-only upper bound applies to all support sizes, and hence also to the fixed support size . This proves both equalities.
The 126 graphs at orders 19 through 144 are in research/odd-endpoint-finite-bridge-graphs.json. Their complete ranks are in the streamable archive research/odd-endpoint-finite-bridge-certificates.jsonl.gz, with source hashes and a full numerical summary in research/odd-endpoint-finite-bridge-verification.json. The producer src/odd_endpoint_finite_certify.cpp uses an explicit alternating-game attractor. The separate direct verifier src/odd_endpoint_finite_verify.py checks the original legal moves; it does not rerun or trust the producer’s queue logic. Its accelerated array checks have an equivalent standard-library scalar mode. Scalar replay of all objectives at orders 19 through 24 also passes, and the earlier two independent game algorithms agree with selected saved certificates at orders 19, 28 and 144. The complete direct rank checks, rather than these additional sample comparisons, prove the finite bridge. The six smaller witnesses are fully checked by both original game algorithms and the direct transition verifier in src/odd_endpoint_small_verify.py; their complete proof data and summary are research/odd-endpoint-small-certificates.json.gz and research/odd-endpoint-small-verification.json. These finite certificates have not yet been imported into Lean.
Proposition (small odd exceptions; exhaustive finite check). For , the general odd upper bound is not attained: In particular, .
Proof. Equality in the upper bound would, by the equality characterization, have precisely nonisolated vertices, one outdegree-one vertex , one distinct indegree-one vertex , all other corresponding degrees two, and absent. Add this missing arc. The resulting two-in/two-out digraph is a bipartite two-regular graph when its sources and recipients are represented in separate parts. Each of its bipartite cycles has even length, so alternating edge colors decompose it into two permutation factors . Choose to contain and label .
Up to relabeling fixing these two vertices, the -cycle through zero is for one . Its other cycles are represented by an integer partition of into parts at least two. For each such choice, enumerating all permutations with covers every candidate graph; remove before applying any game test.
Two necessary obstructions safely prune this enumeration. Once the outgoing neighborhood of an eligible source is complete, if some has and there is an eligible missing recipient for , the pursuer can wait at and capture the first nonwaiting messenger move. Once the incoming neighborhood of an eligible recipient is complete, if and there is an eligible source outside , waiting at until the messenger first enters likewise permits capture. In a partial assignment the cop’s outgoing row may be incomplete: coverage already present persists under later additions. The source or recipient neighborhood used in the inclusion is always complete. The code checks explicitly that the required eligible missing partner exists.
All remaining completed graphs are evaluated by the exact finite reachability game, with receipt priority and finite termination. Enumeration finishes at every and finds no attaining graph. Its counts are:
| Distinguished cycle partitions | Partial nodes | Completed graphs surviving local obstructions | |
|---|---|---|---|
| 7 | 7 | 756 | 0 |
| 8 | 11 | 6,338 | 21 |
| 9 | 15 | 59,375 | 2,092 |
| 10 | 22 | 800,507 | 64,992 |
| 11 | 30 | 10,079,292 | 767,210 |
| 12 | 42 | 164,276,910 | 16,902,091 |
These finite exclusions and the equality characterization prove the claimed strict bounds.
The complete enumerator is src/odd_endpoint_exhaustive.cpp; its finished receipts are research/odd-endpoint-small-exhaustive.json and research/odd-endpoint-n12-exhaustive.json. A known attaining 13-vertex graph passes every partial pruning test as a positive control. The independent review research/odd-endpoint-twelve-independent-audit.md checks the permutation coverage, both pruning arguments, and the final game semantics. It is an independent source and proof audit, not a separately implemented repetition of the enumeration. Neither this result nor the preceding odd endpoint certificates currently has Lean coverage. The proposition does not determine the exact small odd maxima.
The general support reduction in Theorem 57 and the exact finite exclusions in Theorem 53 supersede the earlier bespoke 23-arc reductions and intermediate bounds. Their original arguments and receipts are preserved in research/history/manuscript-superseded-arguments-2026-09-13.md. The following eleven-vertex core lemma underlies the retained small-order exclusions.
Lemma (eleven-vertex cores). Every graph on 11 vertices with 22 or 23 arcs satisfies .
Proof. A vertex of outdegree at most one leaves at most ten contributing source rows, each of size at most eight, giving . A low-indegree vertex gives the same column bound. We may therefore assume minimum indegree and outdegree two. At 22 arcs all degrees equal two. At 23 arcs exactly one vertex has outdegree three and exactly one has indegree three.
If a source camping obstruction occurs, at least eight missing pairs fail at 22 arcs, and at least seven fail at 23 arcs. If a recipient camping obstruction occurs at with pursuer position , every source outside fails. This gives at least seven failed pairs at 22 arcs and at least six at 23 arcs. The total numbers of missing pairs are 88 and 87, respectively, so every graph with one of these obstructions has .
It remains to enumerate the graphs with neither obstruction. The 22-arc case uses the two-permutation decomposition already described. For 23 arcs, the bipartite graph still has a perfect matching: a set of source vertices emits at least edges, whereas a set of possible heads can receive at most . Thus , which implies a perfect matching by the augmenting-path criterion. Its removal leaves residual degree one at every source except the unique degree-three source, where two choices remain; recipient capacities are analogous.
Fix the matching permutation to each cycle partition with no singleton. Its cycle rotations and permutations of equal-length cycles allow the degree-three source to be placed at one representative vertex for each distinct cycle length. Enumerate all positions of the degree-three recipient, then every residual row subject to the prescribed column capacities. This covers every graph in question. Only complete source rows or recipient columns are used in camping prunes; a partial cop row suffices because any coverage already present persists under later additions.
The complete 22-arc enumeration has 120,302 graphs surviving these prunes, with maximum . The complete 23-arc enumeration has 792,080 such graphs, with maximum . Both use the exact finite game recurrence and were freshly recompiled and replayed with all counts and witnesses matching. Thus the graphs surviving the prunes also have , proving the lemma.
The source and mathematical audit, including the matching argument, symmetry reduction and rollback checks, is research/odd-endpoint-eleven-enumeration-audit.md. The enumerators are src/small_exceptional_regular_max.cpp and src/small_exceptional_one_excess.cpp; matching replay receipts and hashes are indexed by research/odd-endpoint-eleven-enumeration-audit.json. The saved maximizing witnesses additionally pass both original game solvers and all direct rank checks. This is independent review and re-execution of the same enumeration sources, rather than a second independently implemented enumeration.
Theorem 53 combines the exact value , the shared source/sink and positive-support bounds, and the three finite exceptional-family exclusions to prove . Its verified twelve-vertex witness also proves for every after adding isolates.
A packed sparse construction with optional arcs
Deleting a short, specified cluster of vertices from the six-type family allows an explicit sparse construction at every order at least 115. Near each deletion, only seven optional arrows must be suppressed. The local strategies allow both of two adjacent columns as entries for final delivery.
Theorem 52 (with finite local certificates). Let , put and . For every integer there is an explicit universally winning digraph with vertices and arcs. Consequently The construction has compulsory arcs and exactly optional arcs; every subset of the optional arcs works. Its range includes every , and every delivery takes at most messenger moves.
Proof. We specify the graph, prove the exact arc count, describe the finite strategy certificates and their complete scope, and lift those strategies to every order in the theorem.
The base graph and the seven exclusions
Begin with the six-type graph on . Write for . The first permutation is the Hamilton cycle and the second permutation has arrows Delete in the canonical columns with when . Reconnect each permutation through each deleted vertex. The changed arrows are There are exactly vertices and base arcs. Both indegree and outdegree remain two. The displayed formulas, , and the gaps of at least three between deleted columns show that the two outgoing arrows at each surviving vertex are distinct and nonloop. In particular the smoothed type 1 arrow has head of type 2 two columns ahead, distinct from its type 2 head in the same column.
The available optional arrow types are Omit arrows whose source was deleted. In addition, for each , omit precisely the following seven arrows, where a quadruple denotes : All column indices in this definition are modulo . These optional arcs are distinct nonloop arcs outside the base graph, and their target types are 0, 1, or 5, so their targets always survive.
Originally there are optional arrows. Each deletion removes the two arrows with its absent type 4 source and the seven further arrows in . None of the seven has the deleted source. The source-column sets for different holes are disjoint, including across the cyclic gap, so these losses do not overlap. Thus the optional count is exactly . Moreover because and . The full envelope has arcs and contains every budget through .
The finite local strategy statements
Unwrap a window around a prospective destination column, now called zero. Retain messenger columns and cop columns . Messenger exits are disallowed. A cop exit enters an outside state ; from the cop may wait or reenter any existing vertex in columns .
For a local deletion crop , construct the smoothed base arrows literally. The messenger uses only these base arrows, together with waiting. The cop receives all surviving optional arrows, except the seven relative exclusions for each hole in , as well as its base arrows and waiting. The finite certificates prove the following statements for every crop that can arise from the canonical construction:
- From every existing vertex in column , the messenger can reach column zero within nine messenger moves and hand off a messenger-turn state in which it is distinct from the cop.
- From every existing vertex in column , the messenger can deliver to any specified existing vertex in column zero within 39 messenger moves.
- From every existing vertex in column , the corresponding delivery bound is 38 messenger moves.
Each assertion quantifies over every cop position other than the source, including . Receipt is terminal before capture; safe transfer instead requires surviving the cop reply before the handoff.
Here the finite evidence consists of complete ranks and messenger policies, not just successful simulations. There are 101 crops and 696 objectives: 101 safe-transfer objectives and 595 specified-target delivery objectives. Every delivery objective checks both entry columns. Ranks use the round convention of local simulation: the selected messenger move decreases rank, every cop reply is safe and nonincreasing, and zero messenger ranks have the required terminal condition. These checked obligations prove the stated local bounds.
Why those crops cover every
Enumerate , , and every choice of center. Cropping the canonical hole sets to gives exactly 101 distinct sets. For any , the gap from the last hole back to the first is at least A 17-column crop has span 16, so it cannot contain holes from both sides of this gap. Its holes form a contiguous portion of one arithmetic progression of step three, containing at most five terms. Every such cropped progression already occurs in the enumeration, by taking the appropriate number of holes and translating the center. No new local pattern can therefore occur at larger .
This is a statement about the specified canonical cluster. It does not assert that arbitrary deletion sets with minimum spacing three admit these local strategies.
Projection of every actual cop move
Smoothed base arrows have column jumps at most two and optional arrows at most three. Thus the window-projection lemma applies with , , and . The preceding crop-coverage argument supplies a certified arena at every center. Its remaining move inclusions require the following check on omitted holes.
Omitting holes outside the crop is conservative. A hole immediately to the right may change a represented boundary arrow from an outside head to another outside head; both project to . No other omitted hole changes a represented-to-represented base arrow. An omitted hole to the left can suppress optional arrows through its relative exclusions; the cropped arena instead permits these extra cop moves. Messenger moves inside are modeled literally. Consequently the projection neither grants the messenger an illegal move nor removes an actual cop response, and it preserves collisions and both terminal conditions.
The certificates grant the cop every permitted optional arrow at once, while the messenger uses only compulsory arrows. They therefore remain valid after selecting any subset of the optional arrows.
Global delivery and the time bound
For a recipient in column , the delivery entries form a consecutive block of length two. Every existing source type is covered, and safe transfer advances one column. Cyclic strategy composition with , , and bounds the total messenger moves by Hence every missing ordered pair is guaranteed. The universal missing-pair upper bound gives , as claimed.
Certificate boundary and reproducibility. The complete finite ranks and policies are saved in research/dense-phase2-sparse-two-entry-certificates.json.gz. The checker src/dense_phase2_sparse_two_entries.py --check reconstructs every arena, checks exact coverage of the 101 crops and 696 objectives, and directly verifies every supplied rank, policy, and required entry state. The reconstruction spells out all six smoothed source-type maps; the independent generator uses explicit messenger-turn and cop-turn states with an AND/OR priority queue, rather than the earlier collapsed-round solver. The summary is research/dense-phase2-sparse-two-entry-check.json. Literal global graph and exact optional-count checks are recorded in research/dense-phase2-sparse-global-map.json.
The smaller messenger window does not establish all the new column entry statements. Enlarging it to is part of this proof, and the failed smaller-window checks are retained in the research log. The earlier broad exclusion buffers and their projection proofs remain research history; they are unnecessary for the theorem above. Negative certificate ranks make no assertion of global impossibility or optimal delivery time. The graph construction, crop coverage, projection, and global composition are ordinary proofs using finite rank certificates; this theorem is not presently formalized in Lean.
Finite cyclic supplement below order 115
The same adjacency recipe gives a further computer-assisted exact interval at orders where the brackets here denote all integers in the displayed range. For every , put and . Every budget has the explicit graph above, and every subset of its optional arrows is universally winning. These 47 finite envelopes have delivery bounds at most 72 messenger moves. In particular, at the full interval is 228 through 380, with bound 66, and it includes the low-budget interval 229 through 341.
Proof and finite evidence. Retain the full cyclic vertex set for both players; no window or exterior-state abstraction is used. Give the messenger only the two compulsory permutations and waiting, while giving the cop all compulsory and optional arrows and waiting. For each recipient, the saved policy assigns to every nonterminal noncollision messenger state a compulsory move. It either reaches the recipient immediately, or every cop response is noncollision and strictly decreases the nonnegative messenger rank. Induction on that rank proves finite delivery. The policy remains legal in every graph between the compulsory graph and its full optional envelope, and all possible cop replies remain covered.
When there are no holes, simultaneous one-column rotation is an automorphism of both the compulsory and optional arrow sets, so six representative targets suffice. This identity is checked on both complete arrow sets. Otherwise every literal recipient is certified. All source/cop positions are checked for every representative target. The optional count is the same displayed count as above; the finite records separately check distinctness, absence of loops, and the complete compulsory and optional lists. Taking the appropriate lexicographic prefix gives each intermediate integer budget.
The 47 finite canonical certificates are contained in the single bundle research/sparse-interface-third-certificates.zip, indexed by research/sparse-interface-third-proof-registry.json. The producer reconstructs and smooths the two permutation cycles. The checker src/sparse-interface-third-independent.py imports no project graph builder or solver: it instead reconstructs each source-type arrow literally and directly checks the rank after the messenger’s chosen move against every actual cop reply. Its receipt is research/sparse-interface-third-independent.json. Together these are a finite proof of the displayed domain, not an extrapolation to smaller or larger uncertified rings. Theorem 52 still supplies the ordinary infinite continuation. Neither this supplement nor its finite graph generation is presently formalized in Lean.
The order 109 capacity repair. At (), additionally permit Both were among the seven suppressed relative arrows near the hole at column zero. These two fixed additions extend the optional count from 107 to 109 and therefore the exact budget interval from 218–325 to 218–327, reaching . The same full cyclic rank argument was independently replayed for every one of the 109 recipients, retaining the messenger’s compulsory arrows and giving the cop the entire enlarged optional set. Its maximum rank is 72. The bundle contains this 48th certificate under the variant name repair109; it is a specific finite extension, not a claim that these two arrows may be restored at arbitrary orders. Together with the preceding supplement, this gives every for all .
A consecutive interval above the two-regular endpoint
The five-type construction can tolerate a controlled set of additional arcs. The proof gives the pursuer every additional move while restricting the messenger to the original moves. This verifies all intermediate graphs at once, without assuming that winning is monotone under adding arcs.
Theorem 36 (with finite local certificates). Let with . For every integer there is an explicit graph with vertices and arcs satisfying Every pair can be guaranteed within messenger moves.
Proof. Use the five-type graph of Theorem 21 on vertices , where is modulo and . Its two outgoing arcs are There are arcs. Add any chosen subset of the further arcs They are distinct from the original arcs and from each other, so every integer budget in the stated interval is obtained.
We verify the stronger asymmetric game in which the messenger may use only and waiting, while the pursuer may also use all additional arcs. Construct the same local arena as in Theorem 21: messenger columns , pursuer columns , and a pursuer state representing the outside. The messenger is constrained to its local columns. The pursuer may leave into , wait there, and re-enter at any vertex in either boundary column or . Within its columns it has the two original arcs and the additional arc above whenever its type is zero.
Two independently implemented finite attractor computations verify the following objectives against every legal initial pursuer state, including :
| Objective | Initial messenger column | Maximum messenger moves |
|---|---|---|
| Reach column zero safely at the beginning of a messenger turn | 1 | 8 |
| Deliver to | 2 | 26 |
| Deliver to | 2 | 19 |
| Deliver to | 2 | 17 |
| Deliver to | 2 | 17 |
| Deliver to | 2 | 18 |
Each row covers all five messenger types and all 45 legal pursuer positions per type: 225 required initial states. The complete ranks verify every selected move and every pursuer response, with the distinct handoff and receipt rules of local simulation.
The window-projection lemma applies with , , and . The messenger uses only original arrows and the local pursuer receives every optional arrow, so local simulation applies to every chosen subset. Cyclic strategy composition, with backward unit transfers and delivery entry column two, gives at most Thus every pair is guaranteed, and all missing pairs are counted. The missing-pair upper bound proves equality.
The primary generator and full ranks are src/five_type_sparse_interval.py and research/five-type-sparse-interval-certificates.json. The independent explicit alternating-state implementation is src/five_type_augmented_verify.py, with its full certificate in research/five-type-augmented-independent-certificates.json. The ring projection and concatenation are ordinary proofs; the bounded local facts depend on these finite certificates. This theorem is not presently formalized in Lean, and it makes no claim for the small rings or for budgets beyond .
Theorem 37 (with finite local certificates). Let with . At every integer budget , there is an explicit graph attaining Every pair can be guaranteed within messenger moves.
Proof. Keep the original five-type graph, and add any subset of the arcs They are pairwise distinct and are not original arcs. It suffices to win with the messenger restricted to the original graph and the pursuer allowed all the additional arcs.
Use messenger columns , pursuer columns , and the outside state . Give the represented pursuer its original and added moves; moves leaving the interval enter . From permit waiting and re-entry at every vertex in the six columns . Independent synchronous and explicit alternating-state certificates verify safe transfer from column one to zero in at most eight moves, and delivery from column two to the five recipient types at zero in at most moves. Each objective covers all 325 legal initial states: five messenger types and 65 pursuer positions per type. The transfer ends on a safe messenger turn, and delivery has immediate terminal priority, exactly as in Theorem 36.
Now the window-projection parameters are , , , requiring . This is the gap condition, not merely distinctness of represented columns. The original messenger moves lift literally and all optional pursuer moves are covered. Cyclic strategy composition with backward unit transfers, delivery entry column two, and gives . Local simulation applies to every optional subset, so all pairs are guaranteed at each of the integer budgets. Counting missing pairs proves equality.
The full primary ranks are research/five-type-full-sparse-interval-certificates.json, generated by src/five_type_sparse_interval.py. The independent 4620-state implementation and certificate are src/five_type_long_augmented_verify.py and research/five-type-long-augmented-independent-certificates.json. The statement is a uniform theorem with a finite local proof ingredient, not an extrapolation from tested circumferences. No new Lean coverage is claimed. For orders divisible by five with , Theorems 34 and 37 combine into a consecutive explicit interval starting at and reaching order .
Explicit attainment at every budget in a sparse interval
The circulant construction gives an exact joint extremum, not only a lower bound on the vertex maximum: for every , Theorem 11 and Lemma 12 already show that . The next result fills consecutive budgets above . Its proof controls the extra pursuer moves; arbitrary additions of arcs would not justify that conclusion.
Theorem 34. For every , Moreover, if and then at every integer budget there is an explicit graph attaining In particular, this holds throughout for every . More generally the explicit interval reaches arc counts of order .
Proof. Say that a set has distinct nonzero differences when implies . For such a set, two distinct translates and intersect in at most one point: two intersections would give two representations of the nonzero difference .
Choose as in Lemma 12 and put . The set has distinct nonzero differences by the proof of Theorem 11. The base graph has steps . For any larger set with distinct nonzero differences, let have the nonzero steps in ; we will keep throughout. Every graph satisfying has distinct closed move sets intersecting in at most one vertex, because .
The proof of Theorem 11 therefore works inside every such . To make this preservation explicit, fix the recipient zero. Its direct predecessors and zero are guaranteed, and is guaranteed using the two successors . If is guaranteed, the following four applications of Lemma 10 establish :
| New source | Two guaranteed successors |
|---|---|
All displayed moves belong to . Coprimality of and makes finitely many repetitions cover all sources. The same argument with all coordinates shifted applies to every recipient, even when itself is not translation invariant. Thus every intermediate graph is universally winning.
It remains to enlarge . Suppose and its nonzero differences are distinct. To adjoin , exclude the following residues:
- The members of itself.
- Residues with and . These exclude every equality between an old nonzero difference and either sign of a new difference. There are at most such residues.
- Solutions of with . These exclude an equality between the two signs of new differences. There are unordered pairs with repetition, and each congruence has at most two solutions, hence at most excluded residues.
Within each sign the new differences are already distinct. The three exclusions are therefore sufficient, and together rule out at most residues. Whenever , at least one admissible residue remains; choose the smallest representative. Under the theorem’s hypothesis this process continues from size four to size .
The resulting has arcs and contains the arcs of . For a prescribed integer in the interval, add exactly of the remaining arcs in lexicographic order. The intermediate graph is universally winning by the preservation argument, so all missing pairs are guaranteed. This matches the elementary upper bound.
For the hypothesis is . Taking the largest admissible gives of order , and therefore an upper interval endpoint of order . The endpoint only needs the original construction, with no extension.
This is a deterministic construction at each stated integer budget. The underlying delivery argument may require many moves; it is not a two-move theorem. Its ordinary proof is independent of the finite tests in src/sidon_main_interval.py, and no new Lean coverage is asserted. It provides an initial consecutive part of Raychev’s full-density interval. The stronger constructions and exact-budget argument in Theorems 38–48 subsequently cover the entire interval at every sufficiently large order.
An explicit algebraic family at intermediate density
Theorem 35. Let be a prime. For every integer there is an explicit graph attaining In particular, the interval extends to at orders . For primes , Theorem 34 extends its lower endpoint to .
Proof. Put , and let be the directed graph with all nonzero moves in . Let be its four-move subgraph with parameters These are distinct and nonzero when . We prove universal delivery in every graph satisfying , including graphs without translation symmetry.
Every closed outgoing neighborhood in is a subset of the corresponding translate of . Distinct translates of intersect in at most one point. Indeed, a nonzero difference determines uniquely: if the first coordinate is nonzero, it determines their difference and sum, and division by two is valid; if the first coordinate is zero, the entire difference is zero. Thus every nonzero difference has at most one ordered representation.
This intersection property gives the following safe-branching rule. Fix a recipient. If two distinct outgoing neighbors of a vertex are already universally winning positions for that recipient, the vertex is universally winning as well. Against an initial cop at another vertex, at most one of the two successors lies in the cop’s closed outgoing neighborhood. Move to the other, survive the cop’s response, and use its winning strategy. The rule concerns the actual game, including the intervening pursuer move.
We first use recipient and only moves of the uniform core . Put and define The vertices are initially winning, by immediate receipt or a direct final move. The remaining vertex has winning successors , so all of is winning.
If every vertex of is winning, so is every vertex of . Apply the safe-branching rule in the following order; each row lists the new vertex and two already winning successors: The corresponding pairs of moves are , respectively. They are distinct allowed moves.
Repeated propagation makes the entire line winning: the nonzero vector has additive order , so integer multiples cover all the displayed scalars.
Use the fourth core move . We have while because . If every vertex of a coset is winning, then every vertex of has two distinct winning successors, obtained by adding and . The safe-branching rule therefore fills that entire coset as well. Iterating gives all cosets , which are the distinct cosets because . Thus every vertex is winning.
The same proof shifted by the recipient uses only moves of and the global closed-neighborhood intersection bound. It applies to every recipient even if the extra arcs of are not translation invariant. Hence every intermediate graph is universally winning.
The core has arcs, and has arcs. Add the remaining arcs one at a time in any fixed order until the prescribed integer budget is reached. All missing nonloop pairs are guaranteed, attaining the elementary upper bound. Finally, when we have , so Theorem 34 covers the adjacent interval .
The proof is finite and constructive: initializing a quartet takes at most two messenger moves, and each quartet propagation increases a bound by at most four. At most such propagations and further coset steps therefore give the uniform, unoptimized bound messenger moves.
The prime hypothesis is intentional. In an extension field, repeated addition only covers scalars from its prime subfield, so this four-move propagation does not justify the same conclusion for arbitrary prime powers. The construction is checked at by src/parabola_cayley.py; it verifies the full-parabola intersection condition, the four-move core’s complete safe-branching closure, and the core/upper-graph inclusions for all 827 consecutive integer budgets in these examples. At , both full game solvers and their rank certificates independently verify every recipient. These finite checks supplement the ordinary proof and are recorded in research/parabola-cayley-checks.json. No new Lean formalization is claimed.
Protected routing and the main interval
Protecting the moves used by the strategy
The distinct-difference condition in Theorem 34 is stronger than the delivery strategy needs. Its branching steps only compare pairs of the three original outgoing moves. Preserving those comparisons permits a much larger set of additional moves.
Theorem 38. For every and every integer there is an explicit graph attaining The strategy uses only three outgoing moves per vertex; the remaining arcs may be added individually up to the stated budget.
Proof. Choose using Lemma 12, put , and set The proof of Theorem 11 shows that has distinct nonzero differences. In particular, each of the six ordered differences has just its original ordered representation in . We only preserve uniqueness for these six differences.
Starting from , adjoin any residue outside No new ordered pair involving the adjoined residue has a difference in , because . Thus the six protected differences retain their original unique representations. When , at most residues are excluded. If , then , so the extension remains possible. Choosing the smallest available representative constructs a set of size at least . For , the initial set already has that size.
Let be the uniform three-move graph with steps in , and let have all nonzero steps in . Consider any graph For a source vertex and distinct core moves , no different cop vertex can have both and in its closed outgoing neighborhood. Indeed, that neighborhood is contained in . If both successors belonged to it, their corresponding elements would satisfy . Protected uniqueness forces and therefore , a contradiction.
Consequently, whenever two successors obtained using core moves are universally winning for a fixed recipient, their source is universally winning: at least one of those successors is inaccessible to the initial cop and survives its response. This argument does not assert that arbitrary pairs of actual outgoing successors have the same property.
The entire proof of Theorem 11 uses exactly these protected pairs. For recipient zero, the direct predecessors are winning, and uses the core moves . If is winning, the four steps establishing use the move pairs respectively, in the order given in Theorem 34. Hence that quartet propagates in . Since , its successive translates cover every source. Shifting the proof by the recipient covers every target, regardless of whether the added arcs are translation invariant.
Thus every graph between and is universally winning. The first has arcs and the latter has at least . Add the extra arcs in lexicographic order until the prescribed integer budget is reached. All missing pairs are guaranteed, meeting the elementary upper bound.
The improvement from order to order comes from preserving only the distinctions actually used by the strategy. Other differences may repeat many times. The graph may also have larger closed-neighborhood intersections; the proof protects its particular pairs of core successors instead of imposing a global intersection bound.
For example, at the construction gives core moves and the envelope . Its protected differences are , each still uniquely represented. The unprotected difference occurs twice, as . Thus this envelope genuinely fails the full distinct-difference condition, yet every intermediate graph with is universally winning.
Corollary 39. There is an absolute such that, for every and every integer we have For every sufficiently large multiple of five , the same formula holds at every integer budget .
Proof. The upper endpoint in Theorem 38 satisfies Since , this endpoint eventually exceeds , the lower endpoint in Corollary 26. The two integer intervals overlap. Theorem 38 covers the lower one and Corollary 26 covers all remaining budgets through , including its dense end via Theorem 20, now a consequence of the direct dense envelopes in Theorems 48 and 58. Taking a common sufficiently large threshold establishes the first statement.
For multiples of five, Theorem 37 supplies every budget from through once . Combining the intervals proves the second statement.
The later Theorems 44 and 59 replace this eventual overlap by a fully explicit construction for every , including the sparse range. Theorem 38 retains its smaller-order domain, arbitrary-subset guarantee, and protected-difference strategy. The probabilistic overlap in Corollary 39 is included only as a consequence of its underlying constructions.
The generator src/main_interval_resume.py checks protected differences at eight orders from 25 through 1000. It checks every protected source-pair/cop triple at the seven listed orders through 200, and verifies 24 selected recipient games with both independent solvers and the explicit rank-certificate checker. Those tests include intermediate graphs lacking translation symmetry. The receipt research/main-interval-resume-checks.json records their exact scope; the parameterized proof above is independent of these finite checks.
Protected routing sets at every exact budget
The random construction can be strengthened by reserving a small set of routing vertices. Only arrows incident with that set are used to certify delivery. All arrows outside the set can then be chosen freely, including adversarially, without invalidating any certified route.
Theorem 54 (protected routing). Let , let be a specified set of vertices, and put Choose an integer and write . If there is a deterministic algorithm, polynomial in , choosing exactly arrows with at least one endpoint in such that every assignment of the arrows between vertices outside guarantees every source–recipient pair within two messenger moves. In particular, at every integer budget an explicit algorithm attains .
Separately, for every real , without condition (R) or an integer exact-budget requirement, independently including each of the incident arrows with probability fails to give such a robust routing set with probability at most Thus the theorem includes both the deterministic exact-budget and the random-construction conclusions.
Proof. Fix and an initial pursuer position . Each certifies a safe two-move route when The three variables are distinct, even when . All are incident with . For different candidates the sets of three variables are disjoint: an equality between an incoming-to-candidate variable and an outgoing-from-candidate variable would force a candidate to equal one of , which is excluded.
There are at least candidates, each with probability of success. There are exactly legal triples. The union bound proves the random assertion. If counts bad triples, it also gives under (R).
Let be the number of chosen incident arrows. Then and is a mode. Since , Chebyshev’s inequality gives . Here , so this interval contains at most integers. Modal maximality implies Therefore .
For completeness, the conditional-expectation algorithm remains exact when restricted to these variables. After a partial assignment, let be the number of undecided incident arrows and the number of additional present arrows required. The total number of completions is . For a fixed legal triple, each candidate contributes a factor if its witness pattern is already contradicted; otherwise its factor is , where variables remain undecided and of them require presence. Multiply these factors, multiply by for unused variables, and extract the coefficient of . This counts exactly the completions in which the triple is bad. Summing over triples gives an integer with initial .
For either decision on the next arrow, child counts satisfy and . Hence some feasible child retains . At the end and . There are decisions and triples per decision, with polynomial-size polynomial products and -bit counts. Straightforward exact integer arithmetic is therefore polynomial in .
For every legal triple a selected candidate differs from the pursuer and both endpoints. Moving to it is safe, and the pursuer cannot reach it on its response. The messenger then reaches the recipient; receipt precedes collision. No outside- arrow appears in these conditions, so the same strategies work for every assignment of those arrows. There are of them. Choosing any prescribed number proves the entire displayed exact-budget interval.
Setting gives and the former exact-budget density theorem at every original order and budget, with its polynomial algorithm and two-move guarantee. A smaller routing set adds genuine robustness and extends the low-density range; it does not merely combine old intervals.
An explicit interval from oriented routing pairs
The separate two-move sparsity question and its bounds are in the delivery-time companion. The exact-budget routing constructions remain here.
Orientation specialization. Fix a routing set of size , and let . If there is a deterministic polynomial construction using exactly incident arrows that preserves universal two-move delivery under every choice of exterior arrows. Thus all budgets from to work. A sharper sufficient condition is
To prove this, independently orient each unordered pair touching , with its two directions equally likely. The incident count is exactly for every outcome. For distinct , a candidate is a safe intermediary when , , and , with probability . The last orientation excludes . Different candidates use independent orientation variables. When , only two variables are needed and the probability is . Counting the two kinds of triples gives the sharper displayed failure bound; the coarser one also follows. Exterior arrows occur in none of these tests.
For exact derandomization, fix orientations in sequence. For a given triple and candidate with free relevant variables, there are bad completions if a fixed variable already prevents the witness, and otherwise. Multiply over candidates, whose variable sets are disjoint, and account for irrelevant free variables. Summing these integer counts over triples gives the total number of bad completions, with multiplicity. Initially it is smaller than the number of all completions. At each decision choose a branch preserving that strict inequality; the two child counts sum to their parent counts. At the end there is one completion and zero failures. There are polynomially many operations on integers of polynomial bit length. This specialization replaces coefficient extraction by products, while the full density and sampling assertions of Theorem 54 remain available.
Corollary 55. Set Whenever , every integer budget admits universal two-move delivery by a deterministic polynomial algorithm, with arbitrary exterior-arrow subsets as in Theorem 54. For every , this extends to every integer budget
Proof of the constructions. Use the orientation specialization. Since for , It gives the exact robust interval .
For , At , makes the left side of the second inequality less than , while its right side equals . The difference increases thereafter because . The elementary inequality follows, for example, from .
Consequently . The existing dense constructions supply every missing budget from through for , in two moves (Theorems 48 and 58). Their interval overlaps , proving the claimed extension through .
Verification boundary. The proofs above are ordinary mathematical arguments. The restricted exact-count implementation and its independent finite checks are recorded in research/routing-unification-checks.json; the independent proof review is research/routing-independent-audit.md. No large instance of the polynomial conditional-expectation algorithm is claimed. ProtectedRouting.lean verifies preservation of safe routing witnesses under arbitrary exterior-arrow changes and their implication for actual terminating delivery. The probability estimates and counting algorithm remain ordinary proofs.
Composition through incomparable hub sets
The construction below reduces a delivery problem on an arbitrarily large outside set to a family of subsets of a small core. The subsets specify which hubs an outside vertex cannot reach. Incomparability makes one outside vertex’s inaccessible hubs available to another vertex. A two-part core handles the remaining configurations, including recipients inside the core. This produces an entire robust interval of exact budgets.
Theorem 59 (antichain composition). Let . Take two sets of hubs , indexed modulo . Their missing arrows are all other distinct hub pairs are arrows. For each of outside vertices , choose a set of hubs subject to these conditions:
- , and lies entirely in one of the two hub parts;
- a set in the part contains no two indices differing by ; a set in the part contains no adjacent indices;
- a two-element code contains no pair at either cyclic difference or ;
- the sets form an antichain: no one contains another.
Include every hub-to-outside arrow, and include for precisely the hubs . Every subset of the arrows between distinct outside vertices may then be included. Every resulting graph has universal delivery within two messenger moves.
Writing and , this gives every exact budget At the upper endpoint the number of missing arrows is . The assertion holds for every optional subset, not merely a specially chosen subset of each size.
Proof. Let denote the missing graph inside the hubs. For a missing pair and a pursuer at , we seek a hub with arrows , with and no arrow . The messenger can move to , survive every pursuer response, and then reach . The case is included.
First suppose all three vertices are hubs. For a missing hub pair, the set contains two points and two lines. If , the line indices are and the point indices are either or . A point pursuer has its entire missing row in only when it is ; a line pursuer’s point pair has difference two and cannot fit inside the adjacent point pair. If , the point indices are and the line indices are either or . The same argument with the two parts exchanged applies. Thus contains a hub outside , which is the desired intermediary.
Now consider the other nondirect configurations.
Both endpoints outside. If the pursuer is outside, choose , which exists by incomparability. It is reachable from , inaccessible from , and reaches . If the pursuer is a hub, its missing row consists of an adjacent line pair or a point pair of difference two. The restrictions on prevent that entire row from lying in . A remaining member works.
Source outside, recipient a hub. Missingness means . For an outside pursuer whose code lies in the same part, choose ; that part is a clique, so . For an outside pursuer using the other part, is disjoint from . Its code cannot fit inside : a larger code has at least three members, and a pair code has neither of that row’s possible differences, one and two. Thus a member reaches . For a hub pursuer whose missing row lies in the part containing , the code restriction leaves a member outside , and the clique supplies the last arrow. For the other hub pursuer part, both missing neighbors are reachable from . Their adjacent or difference-two pair cannot equal the opposite kind of pair , so at least one reaches .
Both endpoints hubs, pursuer outside. The set above contains only two members in either part, with cyclic difference one or two. A larger code cannot fit in that part, and a pair code excludes both differences. Hence contains an intermediary.
A hub source reaches an outside recipient directly. All intermediaries used in the proof are hubs, so optional arrows between outside vertices cannot invalidate a witness. Counting the compulsory and optional arrows gives the stated interval.
Corollary (separated pair codes). For , there are permitted pair codes. For , put . Every budget has an explicit attainer with two-move delivery and every optional subset.
Proof. Each hub index has partners after excluding itself and differences . The two parts supply pairs. Distinct pairs form an antichain. List the point pairs, then line pairs, lexicographically, and take the first . Theorem 59 with gives base and terminal missing count . Take the desired optional prefix in ordered-endpoint order. The original codes of size at least three, and the core, remain unchanged.
The main interval above three arrows per vertex
Theorem (pair-code overlap). Every and has an explicit attaining graph.
Proof. Choose the least with . Then and the pair corollary supplies . Theorem 38 supplies , with . The five-offset circle with admissible reaches at least , starting at . The following direct parameter rules make the intervals meet.
For , take unless , then . The lower cap exceeds on () and (): check each left endpoint and the increasing quadratic difference. At 79 its exact cap is . The cases are ; their lower cap exceeds , first by 2 at 84 and by at 91, then increasingly.
For , choose the first coprime in . Failure requires and either 3 or 5 to divide , forcing . All circle hypotheses hold. The cap is at least . Here , and minimality gives . The cap minus increases from ; twice its value there, with , is
For , Theorem 38 alone reaches . Subtracting from gives . At and it is respectively and , and increases through both ranges. For , minimality gives , so . All choices use arithmetic and optional prefixes, with no graph search.
src/main_interval_pair_codes.py implements the direct rules; src/main_interval_pair_codes_check.py independently reconstructs witnesses and coverage. Its receipt is research/main-interval-pair-code-checks.json. The all-order proof is ordinary; the checks are not a new Lean instantiation. The former classification-overlap proof is preserved in research/history/before-slimming-core-code-composition.md. The following independent stronger construction results remain part of the paper.
Retained larger and mixed codes
Equal-weight codes at every core parity. For a cycle of length , write , put if or , and otherwise put This counts its independent -sets: for , distinguish a selected vertex and distribute the unselected vertices among the nonempty gaps. Dividing by the choices of distinguished selected vertex gives , the same expression.
For every and , the total number of permitted size- codes in the two hub parts is Indeed, the forbidden graph in the line part is a -cycle. For odd , multiplication by two identifies this cycle with the forbidden difference-two graph in the point part. For even , the even and odd indices instead form two disjoint cycles of length . Choosing indices in one and in the other gives the displayed convolution. The two parts have disjoint hub labels, so their counts add. All distinct size- codes are incomparable.
Consequently every supplies the explicit interval in Theorem 59, with List independent sets by taking increasing indices with at least one unselected index between consecutive selections and across the cyclic boundary. For even cores, list the two component choices in increasing order of and then in lexicographic order within each component. List line codes first, then point codes, and take the first . This gives a concrete rule from without pursuit-game search. It includes all previous odd-core ranges. The implementation and independent counting and asymmetric witness checks are src/core_code_all_parities.py and src/core_code_all_parities_check.py; the original odd-core implementation and its earlier receipts remain available unchanged.
For example, , giving for . The fixed mixed list at order 105 contains 85 incomparable codes of total weight 268, giving every budget . At order 116 the saved list has two size-five and 92 size-four codes, weight 378, giving : the two larger codes exclude at most ten of the 110 available size-four codes. The literal lists and independent witnesses remain in research/core-code-third-mixed-105.json and research/routing-defect-phase2-mixed-code-checks.json. These families retain two-move delivery and every optional subset. Their stronger two-move sparsity consequences remain in the delivery-time companion.
Retained wider protected circles
Here we use the protected differences of Theorem 38 without changing its strategy. Let be an allowed odd step, , and Put and No difference between two members of belongs to : within a run it has magnitude at most , while between runs, including the cyclic gap, the shortest gap is at least . For any translate , remove all members of and then adjoin . Every protected difference still has exactly its original representation. Thus the result is an allowed envelope in Theorem 38. The excluded set has at most 19 elements, by expanding the four translates of the six differences. Averaging over gives an envelope of size at least One may then apply the greedy extension from Theorem 38. In particular the old guarantee is preserved. Searching the translations is explicit and takes polynomial time.
The literal protected sets at orders remain in research/core-code-third-circle-envelopes.json, supplying every budget . At order 117, the explicit envelope with has 38 members and exactly one representation of each protected difference, retaining . Its independent check and the order-116 mixed codes remain in research/routing-defect-phase2-mixed-code-checks.json. Original implementations and receipts remain unchanged. RobustTwoMove.lean proves the semantic implication from supplied witnesses, not the combinatorial construction or the complete classification.
Routing through a layer of guides
A small hub-and-guide interface can serve arbitrarily many additional vertices. The following attachment lemma separates its delivery proof from the antichain argument that enters it. This gives the three- and five-move constructions below without repeating their pursuer cases.
Lemma (guide attachment). Let be a set of hubs with internal arrows, and let be disjoint guide vertices. Guide reaches precisely the hubs outside its omitted set , and no other guide. Put . Include all arrows from to the guides and no other hub-to-guide arrows. Choose .
Attach bulk vertices. Every hub in reaches every bulk vertex; each bulk vertex reaches and its assigned guide set . These are all compulsory arrows. The distinct sets have size at least two and form an antichain. Put . The optional arrows are all guide-to-bulk arrows, all distinct bulk-to-bulk arrows, the arrows from a fixed to every bulk vertex, and the arrows from each bulk vertex to . Assume:
- Every hub in has a missing hub successor in ; the successor must differ from the hub itself.
- From every hub or guide, delivery takes at most moves using only hubs as nonterminal intermediaries and compulsory final arrows. This interface strategy remains valid against a bulk pursuer allowed every hub in , every guide, and every bulk vertex.
Then every optional subset gives universal delivery within moves. Its exact-budget interval is where The interface hypothesis is finite: a recipient outside is represented by a terminal outlet reached from , and a bulk pursuer by its permitted hub set and unrestricted guide access. Hub moves do not distinguish other bulk vertices. Receipt at the actual recipient is always terminal, even if that vertex is occupied by the pursuer.
Proof. Let the messenger start at a bulk vertex . If the pursuer is a hub in , the first hypothesis supplies a safe compulsory move into . A hub outside reaches no guide, so any assigned guide is safe against it. Against a guide pursuer choose an assigned guide other than the pursuer, possible because . Against another bulk pursuer , choose a guide in ; incomparability makes this difference nonempty, and no optional arrow enters a guide from a bulk vertex. Each chosen vertex lies in the interface and outside the pursuer’s closed neighborhood in the full envelope. After the cop reply the interface strategy therefore applies. If the chosen vertex is the recipient, receipt has already ended play. Interface sources need no entry move. This proves the time bound against the full envelope and hence for every optional subset.
Count the hub arrows, outlet arrows, guide-to-hub arrows, and bulk arrows to obtain . The four disjoint optional classes have sizes , , , and . Taking an ordered-endpoint prefix attains every stated integer budget.
Theorem (three-move layered construction). Choose integers and , and put . There is a direct construction attaining for every It guarantees delivery within three messenger moves. Every subset of the specified optional arrows is permitted. For pairs of guides, , the compulsory budget is .
Construction and proof. Take fourteen hubs , indexed modulo seven, with missing arrows All other distinct hub pairs are arrows, giving . Use the first omitted guide codes in the ordered list Set , , and Assign the bulk vertices the first distinct -subsets of the guides in lexicographic order. The guide attachment lemma prescribes all arrows. In particular, only guide-to-bulk and distinct bulk-to-bulk arrows are optional; take their first ordered endpoints for the exact budget.
The displayed guide codes satisfy Theorem 59. Thus hub and guide sources deliver within two moves against hub and guide pursuers, using only hub intermediaries. To check a bulk pursuer, put For a missing hub pair , its danger set has only two points and two lines, so it cannot contain . A hub in the difference is a safe intermediary. A hub source reaches any outside recipient directly. For a guide source, the opposite part from its omitted code contains three reachable safe hubs in . All reach an outside recipient. A missing hub recipient lies in the code’s own part, so at most two fail to reach it. This proves the two-move interface hypothesis. Finally, ’s point triple contains no difference-two pair and its line triple contains no adjacent pair, so meets every hub missing row. The lemma applies with , and , giving exactly the stated count and three-move bound. Every missing pair delivers, so the missing-pair upper bound is attained.
For example, gives every budget 1268 through 2888 at order 60; gives 1749 through 5324 at order 80. The larger- formulas remain valid when more bulk vertices are needed. The direct implementation is src/main_interval_layered.py; its checks replay the two-move interface and safe-entry obligations against the full optional envelope. They supplement the ordinary all-parameter proof.
A smaller core with antipodal guide codes
Theorem (twelve-hub guide construction). Choose , , and put . Every exact budget has a direct attaining construction with delivery within three messenger moves. Every optional subset is valid.
Construction and proof. Use the same hub missing-arrow formula modulo six, giving and . Use the first guide codes in Set , , and Again assign the first lexicographic -subsets of guides and use the attachment lemma’s adjacency and optional-prefix rule.
All guide codes satisfy generalized Theorem 59, including its separated pair condition. Its hub-intermediary proof supplies the interface against hub and guide pursuers. Against a bulk pursuer, a missing hub pair has a safe intermediary in : its line triple cannot fit in the danger set’s two lines. For a point-code guide source, all three safe lines are reachable, and at most two fail to reach a missing hub recipient, which is a point. For a line-code guide, the two safe points are reachable. A missing hub recipient is a line, whose missing predecessors are adjacent points; they cannot contain the antipodal pair . Either choice of opposite part also reaches every outside recipient. Hub sources reach outside recipients directly. This proves the two-move interface.
The safe point pair has difference three and the safe line triple has no adjacent pair, so meets every hub missing row. The attachment lemma now uses , , and , giving and the claimed optional count.
For pair guide codes the base is . At this gives 701 through 1268. Taking gives At orders 50 and 60 the intervals are respectively 942 through 2052 and 1162 through 3042. These are all-parameter consequences of the ordinary proof, not extrapolations from numerical games.
lean/GuideAttachment.lean formalizes antichain safe entry followed by a supplied interface strategy. The concrete hub sets, interface witnesses, code counts and adjacency instantiations remain ordinary proofs and independently checked construction data, not claimed Lean coverage.
Circle constructions with three-way escape
The following construction gives the messenger several alternative moves. No pursuer at a different vertex can cover all alternatives. A finite propagation argument then makes every source winning for every recipient. The construction tolerates every subset of its optional arrows.
Theorem (half-density circles and a wraparound gap). Let , , , and . In , take the compulsory offsets One may use either of the following closed offset sets, whose representatives are in :
- If , take
- At any order satisfying the hypotheses, take
In both formulas the deletion applies to the whole preceding union. Include all arrows for , and an arbitrary subset of the arrows for . Every resulting graph has universal delivery and hence attains For an exact budget, include the first optional arrows in increasing lexicographic order of their ordered endpoints.
The first version has . For the second version, put , write with , and put Then . These are explicit adjacency and counting rules, with no graph search.
Proof. All five compulsory offsets are distinct and nonzero. They belong to either envelope: , and none equals the deleted offset. The offset zero is allowed for waiting but is not counted as an arrow. The cardinalities follow by counting the residue classes and the one exceptional offset .
We first prove a local escape property. Relative to a messenger at zero, the following sets of alternative moves cannot all be reached in one move (including waiting) by any pursuer at :
For a full modulo-four envelope, suppose the pursuer reaches . A pursuer congruent to one modulo four cannot do so. A pursuer congruent to zero must be zero, because is the only envelope element congruent to three. A pursuer congruent to two reaches no zero-class point and at most one one-class point. A pursuer congruent to three reaches no one-class point. Each displayed triple contains together with either a zero-class and a one-class point, or two distinct one-class points. This proves their escape property. For the pair , the only remaining possible pursuer is . Reaching would require the deleted offset , a contradiction.
The second envelope has a gap of consecutive absent offsets at the end of its representative interval. Every displayed alternative set has diameter at most . If, after subtracting a pursuer position, its representatives wrapped around zero, their extreme representatives would differ by at least . They cannot both lie in . Thus any putative covering uses a common integer lift of the entire alternative set. The same residue argument applies to that lift. Its only exceptional pursuer is the integer zero, which represents the excluded modular pursuer zero. The pair argument again requires a deleted offset. This proves the local escape property for every order in the second version.
Fix recipient zero. Call a vertex winning when it guarantees eventual delivery from every distinct pursuer position. The recipient and all direct compulsory predecessors are winning. Whenever the compulsory successors of a vertex contain one of the displayed alternative sets of already winning vertices, that vertex is winning too: choose a successor outside the pursuer’s full closed envelope. After the pursuer response, the positions remain distinct and the winning successor strategy applies. Each use of this rule increases a finite delivery rank, so the conclusion is delivery in finite time, not merely indefinite evasion.
Let . The pattern is winning: three of its vertices are direct compulsory predecessors; its remaining vertex uses offsets to reach predecessors . Given , make the following four additions in order:
- uses , reaching ;
- uses , reaching ;
- uses , reaching ;
- uses , reaching .
Every successor belongs to the original pattern or an earlier addition. The resulting set contains . Since , repeated shifts by visit every residue. Modular coincidences only identify vertices already known to be winning; they do not invalidate this finite induction. Translating this proof gives every recipient. All moves of the messenger are compulsory, and the pursuer has throughout been allowed the entire envelope. Consequently the assertion holds for every optional subset, including nonsymmetric ones. The arc count and the missing-pair upper bound give the stated value of .
Parameters at every order divisible by four. The full-envelope version applies to every divisible by four. If , choose . Otherwise write with odd : choose when , and when . The relevant gcd divides eight or sixteen and is odd, so is one. The remaining inequalities follow directly. Thus the complete direct interval in that subfamily is
For other orders, take the smallest admissible , or choose among the finitely many arithmetic candidates to maximize the explicit envelope count. This parameter calculation is separate from graph or strategy search. In particular applies whenever and , regardless of the parity of . The second family therefore bridges the old divisibility restriction while losing only a bounded number of offsets when is fixed.
Relation to the earlier eight-move construction. The previous construction had the additional compulsory offsets and removed both and , under the stronger assumption . Its compulsory graph contains the present one and its envelope is contained in the present envelope. Thus the present theorem preserves every old optional-subset guarantee while lowering the compulsory budget from to and restoring one allowed offset. In particular the earlier interval at , , remains valid.
The direct implementation is src/main_interval_half_density.py. Finite structural replays are recorded separately from this ordinary parameterized proof. No Lean formalization is claimed here.
The main interval above three arrows per vertex
The circle and guide constructions reduce the order needed for the broad main interval. The distinction between its first linear segment and its remaining budgets is now explicit.
Theorem (expanded main interval). There are explicit attaining constructions with throughout both of the following domains:
- Every and .
- Every and .
The thresholds are sufficient, not claimed necessary. Every construction comes with a concrete adjacency rule and arithmetic parameter selection; no new graph search or derandomization is required for a given . The individual families retain their optional-subset and delivery-time guarantees. The combined statement imposes no uniform two-move deadline.
Proof. For , the previous complete main-interval theorem already applies. It remains to cover the finite range . Here we combine the following proved intervals, taking only parameters satisfying their stated arithmetic hypotheses:
- The protected three-jump circle, from through , reaches at least .
- The new five-jump circle reaches , using a full modulo-four envelope or its guarded version as appropriate.
- The twelve- and fourteen-hub guide constructions provide their displayed exact intervals, with and enough distinct guide subsets.
- The equal-weight antichain construction of Theorem 59 provides its explicit interval at each admissible core size and code weight.
- The earlier dense envelopes finish at , starting no later than .
The finite parameter certificate research/main-interval-expanded-checks.json lists a covering chain at every order . Each chain starts at , or at for orders 104 and 105, and adjacent integer intervals meet without a missing budget. All parameters are integers checked against the preceding formulas. The two smaller starting budgets use the already certified canonical sparse envelopes: order 104 covers 208 through 316, and order 105 covers 210 through 327. Both reach .
This is a finite certificate of parameters and inequalities for proved families, rather than a collection of unverified game outcomes. The selector enumerates only the displayed arithmetic parameters, takes a covering family in a fixed order, and selects the prescribed number of optional arrows. The direct constructor src/main_interval_expanded.py implements this rule. Its separate check constructs graphs at the ends and middle of each selected interval and checks their exact arrow counts. The original constructor is used unchanged above order 105. This proves both assertions.
For example, at order 60 the new circle covers 300 through 1740 and the twelve-hub guide family covers 1162 through 3042. The preceding sparse, protected-circle and dense constructions cover the two ends of the main interval. Their overlap fills every budget from 120 through 3420.
Combining the second domain with the previously proved sparse and dense formulas strengthens Corollary 47 to every and . Budgets 12 through 21 remain a separate small-support problem. At orders below 104, the remaining gap inventory distinguishes from the uncovered main budgets at orders at most 42. Neither the new domain nor a successful finite construction implies attainment at an unlisted pair.
The ordinary circle and guide proofs have independent local and actual-game rank checks. RobustLayers.lean proves that supplied strictly decreasing base/envelope source ranks imply actual delivery, and that safe entry into a routing region adds one move. The modular identities, guide-code premises, parameter coverage and extremal counting conclusions remain ordinary proofs; they are not claimed to have been formalized by that semantic lemma.
Exact-budget consequences of protected routing
The full-vertex random and deterministic constructions are specializations of the protected-routing theorem. Their common counting proof is Theorem 54.
Theorem 43. Put and . Under the hypotheses of Theorem 25, there is a deterministic algorithm, polynomial in , constructing an -vertex, exactly -arc graph in which every pair is guaranteed within two messenger moves.
Proof. Set , , and in Theorem 54. The condition implies the required condition because for . The restricted completion counts become exactly the full-vertex counts.
The algorithm’s polynomial bound does not imply a small practical runtime. src/exact_budget_derandomize.py retains the earlier full-vertex implementation and small exhaustive checks; src/routing_unification.py generalizes those counts to a specified routing set. Neither receipt claims execution on a large asymptotic instance.
An explicit threshold for the entire main interval
Theorem 44. For every integer and every integer an explicit polynomial-time construction produces a graph with exactly vertices and arcs in which every pair is guaranteed. Consequently throughout this interval.
Proof. First let . The finite cyclic supplement to Theorem 52 covers every budget , using the two specified restored optional arrows at order 109. The literal protected-circle envelopes at these nine orders have maximum budget at least . With and code weight three, Theorem 59 supplies 100 codes, more than the required , and its interval is Its upper endpoint overlaps the two-move dense bridge . Thus the sparse, circle, code and dense intervals cover every budget at these nine orders. The explicit circle lists are recorded in research/core-code-third-circle-envelopes.json for 106 through 111 and in research/core-code-circle-overlap-screen.json for 112 through 114. Their six protected differences and all integer overlaps are independently checked in research/sparse-interface-third-cross-lane-review.json. The executable adjacency recipe is src/main_interval_composed.py. Its finite extension is checked against the sparse certificate graphs, the circle conditions and the full code/dense witness conditions in research/main-interval-composed-third-checks.json; the earlier outputs at the listed regression orders are unchanged.
For , Theorem 52 covers . The separated-pair overlap theorem following Theorem 59 covers at every , hence at each remaining order. Together these two intervals cover every stated budget. Each construction lists its base arrows and optional arrows; include the prescribed number of optional arrows in lexicographic order. All relevant lists can be constructed in polynomial time. The missing-pair bound gives the reverse inequality.
The sufficient order threshold 106 is not asserted to be optimal. This proof is entirely by explicit combinatorial constructions and finite local strategy certificates. At , the sparse part retains its move bound; its finite 106–114 supplement uses at most 72 moves. These are bounds for the sparse part; there is no uniform two-move assertion for the entire interval. The protected-routing theorem remains independently useful because it allows a specified routing set and a variable incident density, with an explicit random success probability and exact-budget derandomization.
Six-offset circles and finite changes of the compulsory moves
The five-offset circle uses a protected pair of escape moves. Its envelope therefore cannot exceed half density: two translates of that envelope have at most one common point. Adding a sixth compulsory move replaces the pair by a triple. The same four-position pattern still propagates, but the permitted graph may now contain substantially more arrows.
Theorem (three escape triples). Work in and choose with . Require the offsets to be six distinct nonzero residues. Let contain . Suppose that, for every nonzero residue , none of is contained in . Include every arrow whose difference belongs to and any subset of the other arrows whose nonzero difference belongs to . Every resulting graph has universal delivery. Consequently this is an explicit attaining construction at every exact budget
Proof. Fix recipient zero and call a source winning when delivery is guaranteed from every distinct pursuer position. A winning set of vertices supports an additional source whenever all its successors from one of the three displayed triples are already winning. The escape condition selects one successor outside the pursuer’s full closed envelope. After every pursuer response, the messenger remains uncaptured and uses the successor strategy. Every such addition has a finite strictly decreasing strategy rank when followed during play.
Put . Every member of is a direct compulsory predecessor of zero; the new offset supplies its previously missing member. From a winning , add the following four sources in order:
- uses , reaching ;
- uses , reaching ;
- uses , reaching ;
- uses , reaching .
This yields . Coprimality makes its successive translates cover every vertex. All additions use previously established finite ranks, even when some modular vertices coincide. Translating the argument establishes every recipient. The messenger uses only compulsory arrows and the pursuer may use the full envelope throughout; therefore every optional subset is covered, including nonsymmetric subsets. Add the first optional arrows in lexicographic order of ordered endpoints to obtain the exact budget. All missing pairs are winning, proving equality in the missing-pair upper bound.
Two periodic recipes. The escape hypotheses admit direct residue rules.
If , , , , and , take There are no deleted offsets. This gives and the whole interval . The parameter rule from the five-offset theorem provides such an at every , .
To check escape, a pursuer of residue one cannot reach . A pursuer of residue zero reaches only when it is zero. A pursuer of residue two reaches no zero-class point and at most one one-class point; a pursuer of residue three reaches no one-class point. Every required triple contains and either a zero-class and a one-class point or two distinct one-class points. None can be covered.
If , , , , and , take The three deleted offsets are distinct, lie in the periodic part, and avoid . Thus , giving For every odd multiple of five with , one may simply take . The rule also applies to all other displayed arithmetic parameters, with no graph search.
For the escape check, the periodic residue set is three consecutive residues modulo five, whereas the residues of each required triple are not three consecutive residues. A covering translate must therefore use the exceptional envelope point . For this leaves possible pursuers ; for they are ; and for they are . Ignore the forbidden pursuer zero. For , would require , whose residue is absent, and requires the deleted . For , requires the absent-residue offset and requires the deleted . For , requires the absent-residue offset , and requires the deleted . These exhaust the possible covers.
Finite circle envelopes. The literal offsets in research/six-circle-recipes.json supply the theorem’s escape premises at every order from 16 through 42. They are finite construction data; constructing a graph reads those data and performs no optimization. The direct checker separately verifies every translated triple against every nonzero pursuer position.
At some small orders, the fixed three-triple test stops short of the next construction. One can instead enlarge the envelope and make some newly available offsets compulsory. The messenger can then use the new arrows to counter the pursuer’s new moves. These finitely many promoted envelopes carry a different certificate: a literal nonnegative source-rank vector for recipient zero. It has , and every other source either has a direct compulsory arrow to zero or, against each distinct pursuer, has a compulsory successor of smaller rank outside the pursuer’s closed envelope. The usual finite-rank induction proves actual delivery. For recipient , use ; the checker also replays every target explicitly. This applies to all optional subsets and does not infer intermediate-budget success merely from successful endpoints.
For example, at order 24 the six-offset envelope is covering . Add offset three to the envelope and take every nonzero offset in the enlarged envelope except offset one as compulsory. The resulting family has the rank vector The only optional arrows in this second envelope have difference one. Thus every budget between 144 and 312 is covered by a direct finite recipe.
In the same way, the six-offset and promoted envelopes together provide every for orders 19 through 27, where The supplied source ranks, rather than the three-triple theorem, justify the promoted portions. This is a finite certificate boundary, not an assertion that an optimization result proves an infinite family.
The direct constructor is src/main_interval_six_circle.py. Its check replays the escape clauses or supplied ranks, the four propagation identities, exact arc counts, and every recipient for the promoted rows. research/six-circle-checks.json records the executable checks. The ordinary parameterized proofs and finite certificates are not claimed to have been instantiated in Lean.
A smaller incoming and outgoing hub interface
The guide attachment lemma also permits fewer hub arrows at both ends. Only its fixed interface proof changes: it now needs four moves, followed by the same single safe-entry move from a bulk vertex.
Theorem (reduced twelve-hub interface). Let . Assign the bulk vertices any distinct guide subsets which have size at least two and form an antichain. Put and . There is an explicit attaining construction at every budget Every subset of the specified optional arrows is permitted, and delivery takes at most five messenger moves. In particular, distinct size- codes give whenever and .
Construction. Label the hubs and , with indices modulo six. Their missing arrows are all other distinct hub pairs are arrows. Use the first guide codes The parameters of the guide attachment lemma are Thus precisely reaches every guide compulsorily, each guide reaches the hubs outside its code, and bulk vertex reaches . The optional arrows are all guide-to-bulk and distinct bulk-to-bulk arrows, all arrows from to bulk vertices, and all arrows from a bulk vertex to . In particular a bulk pursuer may reach nine hubs, whereas the messenger needs only four.
For equal-size codes, take the first lexicographic -subsets. For an exact budget, take the first optional arrows in ordered-endpoint order. These are direct finite listing rules with no game search.
Proof. We verify the attachment lemma’s interface hypothesis with , allowing a bulk pursuer every guide and every hub outside . A hub move is safe against hub exactly when it belongs to the missing row , against a guide when it belongs to that guide’s code, and against a bulk pursuer whenever it belongs to . All nonterminal intermediaries below are hubs.
For a hub recipient, Theorem 59 supplies the two-move proof against hub and guide pursuers; removing hub-to-outside arrows cannot affect its hub witnesses. Against a bulk pursuer, a missing hub pair’s danger set has only two points, so it misses a member of . For a point-code guide source, a missing recipient is a point; at least one of ’s three points lies outside its two-element code and reaches the recipient through the point clique. For a line-code guide, all three safe points are reachable, and at most two fail to reach a line recipient. Thus all interface sources reach every hub recipient within two moves.
For an outside recipient, the hubs in reach it directly. The following table specifies the further source-rank layers and their reachable, already winning hub sets, using the numeric hub labels.
| New sources | Delivery bound | Reachable already winning hubs |
|---|---|---|
| 2 | ||
| 2 | ||
| 3 | ||
| 3 | ||
| Point-code guide with code | 3 | |
| Remaining guide with code | 4 |
Each displayed set meets the missing row of every hub pursuer other than the source, every other guide code, and . These are exactly the safe-intermediary tests, with a source’s own pursuer position excluded. We verify the tests explicitly. In the first two rows, the four point members meet every difference-two pair; the listed lines meet every adjacent pair except the source’s own missing row. Both rows meet the first guide triple in or , respectively, the second in , all three point codes, and the two retained line-pair codes. They meet in .
In the next two rows the only omitted lines form the antipodal pair , so every adjacent line pair is met. Their point members meet every difference-two pair except the source’s own row. Directly reading the seven codes shows that both sets meet each; they meet in and in , respectively. For a point-code guide, removing its antipodal point pair leaves a point in every difference-two pair. The four retained lines meet every adjacent pair and every line code; the other point codes are disjoint from its own. At least one member of remains. Finally for a remaining guide meets every hub missing row because contains neither an adjacent line pair nor a difference-two point pair. It meets every other guide code by incomparability, and contains all of , since is a line code. This verifies the table.
Every safe hub has smaller delivery rank, independently of the cop’s reply. Rank induction proves the four-move interface, including against the allowed bulk pursuer. Optional hub-to-bulk arrows do not change any missing hub row. Finally meets exactly the eight hub missing rows indexed by ; the four exceptions are . This is the attachment lemma’s remaining hypothesis.
Apply that lemma with , , , , , , , and . It gives the compulsory count the optional count and the five-move bound. Every missing pair therefore delivers, attaining the missing-pair upper bound throughout the interval.
For pair codes the base is . At the interval is ; at it is . These cover, respectively, the earlier outstanding budgets 326 through 339 and 352 through 375. The optional-subset guarantee and five-move bound preserve the earlier family’s stronger three-move claim as a separate result.
The eighth code is deliberately absent: it misses the first two safe-intermediary sets. This is an obstruction to that interface, not to every eight-guide construction or to the game. The direct constructor is src/main_interval_reduced_hubs.py. Its checks replay the fixed hub ranks, safe-entry premises, full-capacity equal-weight families, a mixed antichain and the two targeted intervals. The generic attachment lemma has a separate Lean proof; these concrete instantiations remain ordinary proofs supplemented by the stated checks.
The complete main interval from order twelve
Theorem (main interval). For every integer and every , There is an explicit attaining graph at every pair. Its construction uses arithmetic families and fixed finite arrow lists; it performs no game search or derandomization. Finite lists cover a bounded bridge; the circle and separated-pair constructions cover all budgets above from order 79. The finite-values section treats smaller orders and the other budget ranges.
Stages with changing compulsory arrows
Let be two graphs on the same vertices. For each recipient suppose that every nonterminal, noncollision position has a legal compulsory messenger move , and either , or and every legal cop reply in satisfies Here is a nonnegative integer rank on the noncollision positions. Receipt takes precedence over collision at , as throughout this paper. Induction on this rank proves delivery in every graph . The messenger uses only , while the cop is allowed all of .
One may now replace between successive budget intervals. In particular, if and each pair has such a certificate, every budget from through is supplied. Earlier additions are available to the messenger in subsequent stages. No strategy is required to survive all final cop arrows using only the original sparse base. Every optional subset within each certified stage works; no arbitrary-subset assertion across different stages is inferred.
The same observation works when discovering graphs by deleting arrows from a dense example. Read the resulting list backwards. Discovery direction is irrelevant to the proof: every saved certificate is for a literal lower base and upper envelope, with all intervening budgets obtained by prefixes.
Finite bridge and explicit recipe
The construction data in research/sparse-staged-records.json specify a base arrow list, an ordered list of additional arrows, and certified prefix intervals. At budget , take exactly the first arrows in that list. A stored stage containing supplies the delivery proof. The selected base need not be the same graph as a previously known construction at an overlapping endpoint; each interval has its own complete certificate.
The finite certificates check both positions, waits, receipt before collision, and strict descent after every legal cop reply. Only their stated intervals are used: a stored arrow list can extend beyond its certified stages, and those extra prefixes are not inferred to work. Combine these domains.
- For , use the finite stages, protected and five/six-offset circles, layered and reduced hub interfaces, and separated pair codes. The existing literal dense envelopes at orders 13 and 14 supply the remaining budgets and , respectively. The independent integer-interval check covers this entire finite range. No general larger-code capacity theorem or dense connector is needed by this cover.
- For , the pair-code overlap theorem covers every budget from . The retained sparse stages and certified sparse envelopes cover through , including the repaired order-109 envelope.
- For , Theorem 52 covers through , and the pair-code overlap theorem covers the remainder through .
src/main_interval_complete.py selects these intervals and constructs their adjacency. src/main_interval_pair_codes_check.py independently reconstructs the finite interval union from formulas and saved stage endpoints, and checks actual constructor outputs. The current source-pinned receipts are research/main-interval-pair-code-checks.json and research/main-interval-pair-complete-checks.json. Earlier constructors, certificate files, stronger guarantees, and historical receipts remain intact.
Since every resulting missing nonloop pair is guaranteed, each graph has , matching the elementary missing-pair upper bound. This proves the theorem. The finite bridge is computer-assisted; the circle and pair-code overlap have ordinary proofs. The sparse infinite family retains its stated finite local certificate ingredient.
Formal verification and possible simplifications
lean/StagedEnvelopes.lean proves the generic asymmetric rank-envelope implication for every intermediate graph and actual play against arbitrary legal history-dependent cop policies. It does not instantiate the large finite lists, their computed ranks, the periodic parameter rules, or the complete classification in Lean. Those parts retain the ordinary and independently replayed computer-assisted proof boundaries just described.
A single repeatable small attachment rule remains a possible simplification, not a missing step in this finite-bridge theorem. Two fixed attachments transported whole budget families from order 25 to 26 and 26 to 27. Reusing only the newest vertex’s ports subsequently creates a recipient whose predecessors one cop can cover. That obstruction rules out the proposed repeated tip attachment; it does not obstruct the explicit constructions above. The private extension research is retained separately from the main theorem.
Dense constructions and the final staircase
The dense boundary
Theorem 13. For , and for every admissible .
Proof. If is indirect guaranteed, row misses . By Lemma 1, every other row must miss an arc into . Thus every row misses at least one nonloop arc, and .
Now suppose . If , the upper bound is immediate. Otherwise the preceding argument shows that every row misses exactly one arc; write for its endpoint. Necessarily . A possible indirect pair is . Lemma 1 says These conditions suffice: for initial pursuer , choose the intermediate . It is different from , is inaccessible on the pursuer’s next move, and has an arc to . This is a two-move guarantee.
Pairs satisfying (2) have disjoint source and target vertices. If there are pairs, the remaining vertices contain a cycle of the loopless functional graph of and therefore number at least two. Hence . For attainment use pairs in the missing-arc graph, send every to , put , and send any remaining vertex to . Take all nonloop arcs except these missing arcs.
Theorem 14. A noncomplete graph with every pair guaranteed has at most arcs.
Proof. Such a graph has an indirect pair. No row can be complete: its vertex would block every indirect source other than itself and have no indirect target of its own. If a row missed only , then . Vertex also has an indirect recipient, contradicting Lemma 1. Every row therefore misses at least two arcs.
The next section gives a uniform construction attaining this density on an infinite set of orders. Its proof is independent of the sparse-game certificate for the complementary graph proved later.
A periodic family with three-move delivery
Let , , and write vertices as , with modulo and . Put and Let have arcs , and let be its loopless directed complement. Both maps are permutations, without fixed points or coincident images at a vertex; thus has arcs.
Theorem 15. Every pair in is guaranteed within three messenger moves. Consequently for every .
Proof. For a missing pair and initial pursuer , a safe two-move intermediate is any member of Its exclusion from ensures the two required arcs in , while its membership in the displayed pair makes it inaccessible to the pursuer’s next move.
Translate the source by a multiple of five so that . A failure requires , since . The complete local calculation is:
| , with , | |||
|---|---|---|---|
| 0 | 1 | ||
| 0 | 5 | ||
| 1 | 2 | ||
| 1 | |||
| 2 | 3 | ||
| 2 | |||
| 3 | 4 | ||
| 3 | |||
| 4 | 5 | ||
| 4 |
The only candidate with is . Every difference being tested has absolute value at most 19, so no extra equality appears modulo any . In that exceptional state move from 4 to 0. This is legal and safe: the pursuer at has no arc to 0. Afterwards the pair is covered by the nonexceptional second row for every surviving pursuer position, and delivery takes at most two more moves.
Direct missing graphs unify the dense constructions
The following direct constructions replace the high-girth existence arguments for the numerical dense results. Its proof examines the possible safe intermediaries directly, so no girth hypothesis is needed. The parameterized families have ordinary proofs; a few small orders use explicitly listed finite constructions and independently checked witnesses. All strategies here take at most two messenger moves. Write and .
For a missing-arc graph , a missing pair has a safe intermediary against pursuer precisely when We call the union in this expression the danger set. It contains both endpoints. A vertex outside it supplies both required messenger arcs, while being a missing outgoing neighbor of the pursuer makes it safe.
There is also a robust version. Suppose are missing graphs, and for every arc of and every , Then every intermediate missing graph guarantees all pairs in two moves: retain the witness from , while the danger set only shrinks. In particular, optional arcs can be chosen individually and in arbitrary order.
Theorem 58 (a unified dense construction). There are deterministic polynomial constructions with the following properties.
- At every , a graph with arcs has all missing pairs guaranteed within two moves. Thus .
- At every , one compulsory set of missing arcs and a list of optional missing arcs satisfy (R). Hence every integer attains , with two-move delivery.
- At every , the entire final dense band is exact: Every counted pair in an attaining construction delivers within two moves. The first step already holds at every .
- For , , put A compulsory set of missing arcs extends to an envelope with missing arcs satisfying (R). For , , the same assertion holds with Thus every integer has , where for and for . Every optional subset works, and every missing pair delivers within two moves.
These statements determine every missing budget at every , and every at every . The value is the displayed staircase for and for . The new cap strictly exceeds the cap of Theorem 48 throughout their common domain , preserving its time and arbitrary-subset guarantees; part 2 also covers all of its smaller orders. From onward, .
The two-type core
Use vertices , with modulo , and the compulsory arcs There are exactly two incoming and two outgoing arcs at every vertex. The two types are disjoint, so no loop occurs. For , all pairs in the directed complement are guaranteed in two moves.
To see this, translate the source index to zero. A pursuer is blocked precisely when the line part of the danger set contains both . A pursuer is blocked precisely when its point part contains both . Thus line indices are tested for adjacency, and point indices for a difference of two. The four possible missing pairs have the following point and line danger sets:
- For : point indices , line indices .
- For : point indices , line indices .
- For : point indices , line indices .
- For : point indices , line indices .
For , the only blocked pursuer in each case is the source itself, which is not a legal initial position. This gives every even order .
For odd order , introduce a vertex . Replace the arcs and by Each degree is still two. We verify the two-move property directly. For an old missing pair and a pursuer other than , its old witnesses are unchanged: the danger set only gains the new vertex and may lose old vertices. The pursuer at has missing neighbors , which cannot both occur in any of the four old line danger sets, whose only nonzero differences are one or two.
A pursuer at , , can use unless the source is the other modified point or the recipient is or . In those cases is safe. Explicitly, for source with its remaining old recipient is and the line danger set is . For old recipient , the remaining source is and the line danger set is . None contains when and .
For a new pair , the danger set has point indices and the single line index , in addition to . Neither an adjacent line pair nor a point pair of difference two fits; the other modified point pursuer also retains its different line neighbor. For a new pair , the line indices are and the point index is , in addition to . Again all legal pursuers have a safe neighbor.
The remaining order has the following explicit missing rows:
Every incoming and outgoing degree is two. For each source, its two recipients in the displayed order give the following two danger sets:
Inspection of the eleven rows shows that each danger set contains only its source’s row. Every legal pursuer therefore has a safe missing neighbor. This finite set-containment argument proves the eleven-vertex case and completes part 1. The accompanying certificate also lists all 220 pair/pursuer witnesses explicitly.
An envelope with one optional arc per vertex
For even order , retain (B) as and add the optional arcs For , condition (R) holds for the full envelope . There are six types of missing pairs. Their point and line danger indices are respectively:
- : and ;
- : and ;
- : and ;
- : and ;
- : and ;
- : and .
Test line adjacency and point differences of two as before. The only blocked compulsory pair belongs to the source. All index differences tested have absolute value at most eight; introduces no additional modular adjacency or difference of two. Thus (R) holds.
For odd order , with or , use a different placement of the new vertex : replace and by paths through . Retain every optional arc in (E), and add the single optional arc . The compulsory graph has arcs and the full envelope arcs. We check (R).
For an old pair, every unmodified old pursuer retains its old safe witness because the only new danger vertex is . The compulsory neighbors of the pursuer at are . No translated line danger set in the six-case list contains both: their integer differences have absolute value at most six, while seven is not congruent to any such nonzero difference modulo the stated .
The remaining old pursuers are , , with compulsory neighbors . If is in the danger set and the source differs from , only the following cases arise:
- The source is the other modified point . Its retained old targets are and . The respective line danger sets are and .
- The recipient is , . The remaining old sources are and . Their line danger sets are and .
- The recipient is . Its old sources are , and their line danger sets are contained in .
None contains in its applicable case, for or . Thus the remaining compulsory neighbor is safe.
It remains to check the new missing pairs. In the following lists, the danger set also contains :
- For , , the point indices are and the only line index is .
- For , the point indices are and the line indices are .
- For , the point indices are and the line indices are .
The point sets contain no pair of difference two and the line sets no adjacent pair at the stated moduli. For example, the largest relevant point difference is 13, so it cannot become two when ; modulo 14 it becomes , which is also harmless. The line differences have absolute value at most eleven, so they introduce no modular adjacency. A modified point pursuer, when legal, retains a line neighbor or outside its danger set; the pursuer at is either the source or sees only one of its two line neighbors in that set. This proves (R) at the stated odd orders.
Four explicit repairs fill the remaining odd orders. On vertices, subdivide and through as above, retain the optional arcs (E), and add . Make the following substitutions in the optional list; every index is modulo :
- At , use , replacing by and by .
- At , use , replacing by .
- At , use , replacing by .
- At , use , replacing by .
In each case the compulsory set has arcs and the optional list has distinct additional arcs. These are finite constructions: research/dense-phase2-certificates.json supplies, for every full-envelope pair and every legal pursuer, a compulsory neighbor outside its danger set. The direct checker src/dense_phase2_certificates.py verifies each listed witness using literal legal-move sets; an independent check is recorded in research/dense-phase2-independent-root-check.json. The certificate proves (R), so it covers every optional subset rather than just the chosen total counts. Together with the parameterized families, this establishes the bridge at every .
Six smaller envelopes
For , use the compulsory core (B), or its odd modification (O). Identify , , and, in odd order, , where . The following ordered pairs are optional missing arcs:
Each list contains exactly distinct arcs outside the compulsory set of arcs. For every missing pair in the full envelope and legal initial pursuer, the archived certificate explicitly supplies with and . These are precisely the obligations in (R). The archives are research/routing-defect-phase2-dense-tiny-checks.json for orders and research/routing-defect-phase2-dense-small-checks.json for ; at order 18 the archived full envelope is larger, so the displayed subset inherits its witnesses.
Separate literal readback programs, importing neither the producer nor its graph helpers, check every stored witness and its complete pair/pursuer coverage. Their receipts are research/routing-defect-phase2-dense-tiny-independent.json and research/routing-defect-phase2-dense-small-independent.json. In addition, SmallDenseEnvelopes.lean checks all six row lists, the base and envelope arrow counts, and every required safe witness by kernel reduction. The robust-envelope semantic theorem then proves actual two-move delivery for every intermediate graph, against arbitrary legal pursuer choices. This verifies every optional subset, not just a single graph at . Together with the preceding families, it completes part 2 for every .
Quadratic envelopes from a shared danger-set calculation
The interval can be enlarged while keeping just two compulsory missing neighbors per pursuer. In a core with indices modulo , use and optional arcs for and for . Translate the source index to zero. The six full-envelope danger sets have the following point and line index parts:
Condition (R) asks whether the line part contains an adjacent pair, or the point part contains a compulsory pair of difference , belonging to a pursuer other than the source. This single calculation will establish both caps in part 4.
A residue-five family at every order from 30
Write , where and , and put . Take and Add vertices with compulsory missing rows There are no missing arcs from the core to these vertices. Permit every directed nonloop arc between added vertices as an additional optional missing arc.
First consider only old sources and pursuers. The multiples-of-five sets in (T) contain neither adjacent indices nor indices of difference two. In the four compulsory-pair rows of (T), a compulsory cop row can be contained only when it is the source’s own row. For , the line set acquires an additional adjacent pair only at ; values and merely duplicate the source row. Only is a multiple of five, and it is excluded from . For , the apparent extra difference-two pair at is just the existing pair . Thus old legal pursuers always have a witness. These modular statements hold because and .
An added cop has point/line index difference three. For an optional pair, the point danger has the source’s residue, while its line residues differ by ; difference three is absent. For an optional pair, the line danger has one residue and the point residues differ from it by , again excluding the row. The four compulsory cases in (T) give the same exclusion except possibly or . Their actual line-minus-point difference is , which cannot equal three modulo . Hence added cops also retain witnesses.
For a new source targeting , the old danger parts are The first lies in one residue class. The second has pairwise differences , none congruent to modulo . Neither old row type is blocked. An added row from would require to be a multiple of five and one of , forcing , the excluded source. For recipient , the old point danger is , whose differences cannot be ; the old line danger has one residue class. An added cop would require to be a multiple of five, again forcing .
Finally, an optional pair has old danger exactly . It contains neither an old row nor a distinct new row. Incoming arrows from added vertices only add new vertices to other danger sets, whereas every compulsory row lies in the old core. They cannot spoil any witness. This proves (R).
There are compulsory missing arcs, optional core arcs, and optional added arcs. Their total is exactly .
A parity family with quarter-density cap
Write , , , and put . Take . Let consist of all nonzero even residues except , and let consist of all nonzero even residues except . For each add a vertex with compulsory row and again permit all nonloop missing arcs between added vertices, with none from old vertices to new ones.
Both forbidden row differences in (T) are odd: one for a point cop, three for a line cop. Since contain only even indices, testing the exceptional even/odd pairs in each row of (T) gives the following possible offsets for a blocked old cop other than the source:
- : in , or in ;
- : in , or in ;
- : ;
- : in , or in ;
- : in , or in ;
- : .
All these offsets are excluded. Coincidences that merely reproduce the source row do not block another cop: adjacent pairs and pairs of difference three have unique source indices when .
An added cop has a point pair of difference five. In the same six point-danger sets, such a pair would require respectively offsets in ; in ; no possibility in the all-even third case; in ; in ; or in . Every exception is excluded, so added cops are safe against old pairs.
For a new source targeting , its old point danger is and its old line danger is . The latter is not adjacent. A difference-three point pair would require or , excluded from . For recipient , the point danger is the same test requires the excluded offsets . Its line danger again has difference three. A distinct added row could be contained only if or modulo : one parity occurs just once in the point danger. The first is the source and the others are impossible for and .
For a new-to-new pair, the old danger is the source’s difference-five point pair, containing no old row and no distinct added row. As before, new danger vertices belong to no compulsory row. This proves (R).
The eight exclusions in and seven in are distinct because , so and . There are compulsory missing arcs and optional ones, totaling . Part 4 follows by selecting any desired number of optional arcs.
Comparison and proof boundary
The improvement retains the old small-order domains. For , Also Since , this strictly exceeds the cap of Theorem 48. For , the difference from is at least and At its values are , and each increases with . Thus this family also strictly exceeds the old cap at every .
The twenty residue classes modulo show for every . Indeed it holds at , and if , the difference increases on replacing by by For the old orders , that cap is exactly , already covered by part 2. Thus the present envelopes subsume its entire numerical statement, preserving the time, algorithm, and arbitrary-subset conclusions at every old order. No earlier domain is lost.
The two cap formulas have ordinary proofs above. The independent review research/dense-phase2-uniform-independent-audit.md checks their modular exceptions and counts. The primary receipts research/dense-phase2-uniform-envelope.json and research/dense-phase2-quarter-envelope.json additionally check bounded full-envelope games; those samples are not used to infer the formulas.
The first forced loss at every order from 16
Use an even core of order , or its odd modification (O) of order . Add four vertices and missing arcs In the even case choose . In the odd case choose . The four attachments are distinct; each branch pair has index difference three, hence neither one nor two modulo .
For an old missing pair, old pursuers retain their old safe neighbors, since the danger set only gains or . A pursuer at uses . A pursuer at can use or : no old recipient receives both branches. The pursuers at have point pairs of difference three, which cannot fit into the old point danger pairs of difference one or two. In the odd core there is also the point danger set for a pair ending at ; neither chosen branch is that pair. The other new old-core pairs have at most one point in their danger set.
For a new pair with source or and recipient an attachment , ordinary point pursuers have adjacent line neighbors while the old incoming line pair of has difference two. Ordinary line pursuers have point-neighbor difference two while the branch pair has difference three. In the odd core, the modified point pursuers use , and the pursuer at has line neighbors of difference three, which cannot both lie in the incoming pair of difference two. The opposite branch is disjoint, can use that opposite branch, and can use . Thus these four pairs win. The pair also wins: no missing neighbor enters , and every other pursuer has two missing neighbors, at least one outside .
Exactly the pairs fail. A pursuer at has closed move set in the delivery graph and blocks every nonterminal departure from . All other initial pursuers have safe neighbors for those pairs. The construction has missing arcs, so pairs count. This proves the first-step assertion for all .
Functional roots and the rest of the staircase
Use the spare functional vertex when the order is odd. On vertices put , retain the missing chains and the cycle , and, for odd , put the remaining vertex . The set of vertices with no missing incoming arc is Consequently .
Add vertices, each with a distinct two-element missing-neighbor set in . This is possible whenever It guarantees exactly counted pairs. Against a functional pursuer, its unique missing neighbor is outside and outside the added vertices, so it is safe for every added source and its two recipients. Against another added pursuer, choose a member of its two-element set outside the source’s set. Any two distinct roots are joined in the delivery graph. The original pairs also survive: an added pursuer has a root neighbor different from , and that root has a direct delivery arc to . This argument includes the extra root . Theorem 27 gives the matching upper bound.
Now fix and , and put . The first step is already proved. For and , join the functional -vertex graph to the direct -vertex core; Lemma 28 preserves guarantees. If remains, then , so (F) holds because Finally is the functional endpoint in Theorem 13. Since this proves part 3. More precisely, the same formula holds whenever and either the core condition or (F) applies, including smaller orders than 20; the endpoint holds at every .
All recipes consist of modular arc lists and elementary subset choices, and therefore take polynomial time. The receipt research/dense-unified-core-checks.json records bounded complete two-move and robustness checks from src/dense_unified_core.py. The parameterized proofs above do not depend on those finite tests. The explicitly isolated eleven-vertex core and small optional envelopes have the finite proofs and certificates described above. The infinite families and their general existence proofs remain ordinary arguments. The finite eleven-vertex core and the six small envelopes have Lean coverage in ElevenVertexDense.lean and SmallDenseEnvelopes.lean, as detailed in the formal verification section.
Functional interfaces in the final dense band
All graphs in this section are missing-arrow graphs; the delivery graph is their loopless directed complement. Put and . The functional graph on vertices has , chains for , and a spare when is odd. Its roots have missing indegree zero and ; exactly its pairs are guaranteed.
Theorem (root-colored attachment). The exact value has a direct attaining construction in the following domains:
- ; or and or even; or , with two-move delivery;
- and arbitrary , with three-move delivery.
Construction and proof. For use the functional graph. For give the new vertex two distinct roots as its missing neighbors. For , put a missing cycle on the new vertices, with successor , and add for a proper root coloring . Two alternating roots suffice for even ; an odd cycle uses a third root at its last vertex. Each new row has two missing neighbors.
Fix a new missing pair, from to either or . An old pursuer has a unique missing neighbor in the old nonroots, which is a safe intermediary to either recipient. A new pursuer with different root color uses . If the colors agree, use : injectivity gives , and proper coloring ensures its delivery arrow to . It also has an arrow to , since a missing arrow there would force , contradicting the equal colors. For an old counted pair , a new pursuer uses ; the source reaches every new vertex and each new vertex reaches the old nonroot . The case instead uses a root different from the functional source. These intermediaries prove every claimed two-move guarantee.
Only odd with two roots remains. Use an alternating cycle on vertices and a singleton whose missing neighbors are the two roots. A cycle-source pair against pursuer uses the other root; an old counted pair uses a root different from its source. Thus all these pairs retain their two-move guarantees. From to a root, an old pursuer again supplies its unique nonroot missing neighbor. Against a cycle pursuer , move safely to and either deliver directly or invoke its already proved two-move strategy. This takes at most three moves.
The graph has missing arrows and guarantees, matching Theorem 27. The existing fixed-graph certificates check the same constructions; the displayed argument proves their unbounded domains.
Corollary (the two-move band). For every and , the staircase value has an attaining construction with two-move delivery.
Proof. The first step uses the four-vertex attachment of Theorem 58. For , the remaining core has vertices, so functional-block addition to the direct core applies. For use the preceding colored attachment. The case is functional.
Exact addition across missing-arrow blocks
Lemma (arbitrary-duration missing-block addition). Let be a disjoint union of loopless directed graphs , every vertex of which has positive outgoing degree. Let be the loopless complement of on its own vertex set, and let be the loopless complement of . Then More precisely, a missing pair inside block is guaranteed in if and only if it is guaranteed in . If its original guarantee uses at most messenger moves, at most moves suffice in .
Proof. Every arrow between distinct blocks is present in , so all missing pairs lie within one block. Fix such a pair in block .
Suppose first it is guaranteed in . If the pursuer starts outside block , choose one of its missing neighbors in its own block. The source has a delivery arrow to , the pursuer cannot reach in its reply, and has a delivery arrow to . Two moves suffice. Otherwise follow the original within-block strategy while the pursuer remains in block . If the pursuer first leaves that block after a nonterminal messenger move, apply the same two-move escape argument from the messenger’s present vertex. A play in which the pursuer stays inside follows the original winning strategy. If the strategy has a bound , any departure occurs after at most messenger moves, giving at most moves in total. All waits are included in these strategies. The chosen is not the pursuer’s current vertex, since has no loops, so waiting cannot invalidate its safety.
Conversely, suppose the pair is not guaranteed in . Choose a permitted initial pursuer position and its avoiding strategy in that finite reachability game. Keep the pursuer inside the block and follow that strategy. If the messenger also stays inside, it cannot guarantee receipt. If it first leaves, its new vertex is outside the recipient’s block, so receipt has not occurred, and the pursuer immediately captures it using the complete cross-block arrow. Thus an outside excursion cannot turn an internal losing pair into a winning one. This proves the equivalence and summing over missing pairs proves the identity.
The two-move version of the original block lemma retains its sharper two-move time conclusion. The present lemma removes that hypothesis for the count identity; it does not assert that every copied strategy continues to use two moves.
Proposition (a nine-vertex core). There is an explicit graph with , and . Label vertices and take all nonloop delivery arrows except the following missing-neighbor rows: Every missing pair is guaranteed within three messenger moves. Four of the eighteen pairs need more than two moves under the exact two-move criterion. The literal graph is a permitted finite exception: it is verified by two independent actual-game solvers and a full replay of all alternating-state rank certificates, in research/dense-third-core-compose-certificates.json. The missing-pair upper bound proves .
One additional missing arrow supplies every first step
Lemma (enlarged direct cores). At every order there is an explicit missing graph with arrows whose complement guarantees all of them. Three messenger moves suffice for ; the retained nine-core uses four.
Proof. For even , use the two-type core (B) of Theorem 58 and add . Only pairs leaving , entering , and the new pair can lose an old safe intermediary. For the new pair the point and line danger indices are and . For , the latter contains only the source’s adjacent pair . The affected old pairs have just one additional blocked state: where the entries are source, recipient and pursuer. Move safely to , whose missing pair to still has its universal two-move guarantee. This proves the assertion for .
For odd , use (O) and add the same . For the only additional blocked states and safe first moves are Both resulting pairs retain their universal two-move guarantees. Indeed the new pair has line danger indices , point indices , and vertex . No ordinary cop row fits; the modified row fits only when . The old pair to has point danger and the old pair to has point danger , giving exactly the two states displayed. Pairs entering introduce no others for .
The small moduli have the following complete exceptional-state lists; each safe first move leads to a universally two-move pair:
| Core | Source, recipient, pursuer | Safe first move |
|---|---|---|
| even | ; | ; |
| even | ; | ; |
| odd | ; | ; |
| odd | ; ; | ; ; |
For the eleven-core listed in Theorem 58, add missing arrow . The five affected danger sets, for pairs , are respectively Each contains only its source’s missing row. Thus every missing pair still wins in two moves. Finally, the nine-core above with added is the retained finite all-delivery witness with 19 missing arrows in research/small-dense-anchor-certificates.json.
The modular danger-set proof establishes the unbounded families. src/dense_functional_transfer_check.py independently checks their exceptional states and safe moves, the five literal eleven-core sets, and both exact game algorithms on the fixed small graphs. The receipt research/dense-functional-transfer-audit.json records the checks; no new Lean instantiation is asserted.
Corollary (the first dense step). For every ,
Proof. Adjoin a disjoint missing two-cycle to the enlarged core of order . Missing-block addition preserves all core guarantees; there are missing arrows, meeting Theorem 27. Four moves suffice for by the lemma; the retained full certificate gives the same bound at . The earlier two-move construction remains available for . The retained finite attachments at additionally retain their three-move bounds; their full ranks are in research/dense-third-core-compose-certificates.json.
Equality in the second dense step
Proposition (the second step reduces exactly to a smaller dense core). Let and put . Then In particular, An attaining graph at the left-hand endpoint must have a missing graph consisting of a two-cycle disjoint from a -vertex missing core whose outdegree is exactly two everywhere and whose complement guarantees all missing pairs. No missing-indegree-two condition or two-move assumption is imposed on this core.
Proof. Suppose the first maximum is attained at . There are missing arrows, so the failed-pair count is . The proof of Theorem 27 applies because . In its notation, every missing outdegree is positive, the number of vertices with missing outdegree one satisfies , and . Therefore . The total degree sum then forces all other missing outdegrees to be two.
Write for the two degree-one vertices and for their unique missing-neighbor map. If , the stronger inequality in that proof gives which is impossible. Thus , and looplessness forces the two-cycle on . Its two missing pairs already fail, as both vertices lie in .
Every missing pair with source outside must consequently be guaranteed. If such a source has a missing arrow to , let be the other cycle vertex. The pursuer at has closed delivery neighborhood . The messenger at cannot move to , so every legal move, including waiting, is intercepted unless it is immediate receipt; a missing recipient cannot be reached immediately. Hence the entire missing source row of fails, a contradiction. All missing arrows from outside therefore stay outside .
The missing graph is the disjoint union of the two-cycle and a -vertex outdegree-two graph. Exact missing-block addition gives , because the complement of the two-cycle has no indirect guarantees. This yields the right-hand equality.
Conversely, a graph attaining guarantees every missing pair. Its missing graph has positive outgoing degree at every vertex; otherwise the corresponding universal pursuer neighborhood would force . Adjoin a disjoint missing two-cycle. Exact addition preserves guarantees, matching the staircase bound. The maximum inequality follows because any larger integer than must equal the staircase upper bound , and the equivalence then forces the smaller-core maximum to have that value.
The already completed finite joint tables give and . Hence two of the gaps at that stage had stricter upper bounds than the eventual staircase: These immediate bounds inherit the existing exhaustive finite table proofs. The complete small-core checks below strengthen them and also exclude second-step equality at orders nine and ten. Their completeness, rather than a failed bounded construction search, supplies the exclusion.
A safely reached root and the staircase from order eleven
A rooted missing core consists of vertices and one additional root , with missing rows for . In its restricted delivery game, surviving pursuer positions are in . Receipt at the actual recipient remains immediate. For a recipient in , a messenger move to is useful only when for the current pursuer : otherwise the pursuer can capture there. After a safe arrival the root delivers directly to the recipient on the next move. Restricting surviving pursuer positions does not remove this capture at an unsafe root arrival.
Lemma (designation and exact functional replacement). Designating any vertex of an all-delivery missing core as and forgetting its own row yields an all-delivery rooted interface. More generally, let every core row contain a missing neighbor in . Attach any loopless functional missing graph at , with no missing arrow in entering , and no other cross missing arrows. Then where the rooted count includes missing pairs whose recipient is .
Proof. Designation follows the old strategy until receipt or safe arrival at ; in the latter case the strengthened root row delivers next. Receipt when is the actual recipient is immediate, even if the pursuer is there.
For a core pair, an pursuer’s unique missing neighbor lies in . It is safely reachable from any core position and directly delivers to every core recipient and to . Thus a rooted winning strategy extends whenever the pursuer leaves . A losing pursuer can remain in , capturing every messenger excursion into ; visits to obey precisely the rooted safe-arrival rule. Hence the core guarantees are exactly preserved.
For an pair the missing recipient differs from . Against a core pursuer choose its missing neighbor in , which is safely reachable from and directly delivers to that recipient. This also handles a pursuer leaving during an internal winning strategy. Conversely, a losing pursuer can remain in and capture every excursion into . Thus the guarantees are also exactly preserved. All waits and terminal receipt are included.
For a functional missing map , its pair is guaranteed exactly when has missing indegree zero and has missing indegree one. Otherwise a predecessor of , or a second predecessor of , camps and blocks every nonterminal move. If both conditions hold, is a safe intermediary against every . This proves the functional count used by the attachment lemma directly.
Proposition (rooted cores). An all-delivery rooted interface with two missing neighbors per core vertex exists at every core order . At , with root 7, its rows are Its rooted guarantee has the retained finite actual-game proof in research/small-dense-rooted-certificates.json and research/small-dense-rooted-deletion-certificates.json. At , designate vertex 8 of the nine-core as root; at designate a vertex of the direct core on vertices. Every row has an internal missing neighbor, so exact functional replacement applies. In particular, the seven-core with gives the retained small value . The audit checks both positive and negative transfer masks on fixed interfaces; the lemma itself is an ordinary proof.
Corollary (the complete staircase from order eleven). For every and , Four messenger moves suffice; at every the earlier uniform two-move construction remains available.
Proof. The first step was proved above. For adjoin a disjoint missing two-cycle to the ordinary core on vertices. For , use the rooted core on vertices and attach the functional -vertex graph, choosing one of its roots as . The exact replacement identity gives . For use the root-colored cycle and singleton construction, including . Every count meets Theorem 27. The fixed rooted seven-core and nine-core certificates retain their four-move attached bounds; larger designated cores have two-move strategies before replacement and need at most three afterwards.
Strict small values in the second through fourth steps
Theorem. The following are exact values, with literal attaining graphs: In particular the uniform staircase threshold eleven is sharp: , the staircase value at that cell.
The ordinary seven- and eight-vertex endpoint cores needed below admit complete small normal forms. In an all-delivery two-out missing core, the two members of any row have disjoint missing rows and no missing arrow between them. Otherwise source or predecessor camping loses a missing pair. Normalize . If either neighbor points back to 0, the other rows can be labeled and ; otherwise they can be labeled and . These exhaust the possibilities, without imposing any missing-indegree condition. Complete enumeration of all remaining rows has no survivors at either order. The independent chronological replay uses 227 and 4,307 prefixes respectively, recorded in research/small-dense-endpoint-independent-checks.json. This is the finite endpoint exclusion used here, not an assumption about two-move delivery strategies.
Here are the finite and ordinary components of the proof. Write , , , , and . Positive implies everywhere; hence . From the degree-one proof, . Put , , , and let count vertices in whose image has exactly one preimage in . Its stronger bounds are Every row with source in is killed. An outside row pointing into is killed as well by the corresponding degree-one pursuer.
At , equality in the staircase would require , forcing . The functional graph on is therefore . Its three killed rows exhaust the losses, and all other rows avoid . Equality is equivalent to an all-delivery safe-root two-out core on vertices.
At , equality again means . For the same functional path leaves a rooted core on vertices with one degree-three row and all other degrees two. For , the case is excluded. The case would force : the two vertices outside would need distinct unique images, but the vertex of must also map to the outside image, a contradiction. Thus , and is a three-cycle or a two-cycle with one incoming tail. All three pairs fail, leaving a rooted two-out core on vertices (with unused root in the three-cycle case).
Complete safe-root enumeration excludes two-out cores of orders 3 through 6 and one-degree-three cores of orders 3 through 6. The source test is for distinct core vertices: it kills row . The predecessor test requires a cop row contained in the core whose neighbors’ completed rows have a common missing recipient. A cop row using the root is not pruned by this latter test. There is no missing-indegree restriction. Two-out rows using the root have normalized initial rows and either or . Rows without root use the two ordinary depth-two forms. A unique degree-three row is normalized to or . Every other loopless row is enumerated.
The two-out families have 4, 14, 72, 1,168 prefix nodes at orders 3, 4, 5, 6; only the last has static leaves, six in total. The one-degree-three families have 4, 74, 1,442, 29,852 nodes, with twelve static leaves at order 6 only. All eighteen leaves fail in the full actual game after functional attachment; both winning and losing ranks are checked. These complete finite exclusions prove the strict third- and fourth-step upper bounds in the table. The seven-core attachment supplies its exceptional entry at order 10.
For , the earlier equivalence and complete ordinary seven/eight-core exclusions first rule out at orders 7 through 10. At order 10 this gives the claimed upper bound 15. At orders 7, 8, 9 suppose . Then . The case leaves the four-vertex functional path and a rooted core of order with excess 2: one degree-four row or two degree-three rows. All six profiles at orders 3, 4, 5 have zero static leaves in complete all-row enumeration. Their prefix counts are 1, 3, 8, 69, 396, 4,211. The case leaves a rooted core of order with one degree-three row, already excluded.
When , all other degrees are two. A closed two-cycle forces every outside row to avoid it, since an additional killed row would give four losses. Exact missing-block addition then bounds by the ordinary core values at orders 5, 6, 7, all below . Otherwise the only shape with at most three losses is , with degrees 1, 1, 2. The rows at exhaust the losses. Put . The degree-one pursuer at kills every missing column into ; , or the additional pair would fail. Every remaining good row avoids , except . If , removing these four special vertices leaves an ordinary universal two-out core of order , impossible by the small tables. Otherwise it leaves a rooted two-out core of order , root . The order-two case is immediately source-camped; the other two are among the complete exclusions above. This proves and the strict upper at orders 7, 8, 9.
For the lower bounds at , take a missing two-cycle and two free roots , . Attach the alternating colored cycle and, when necessary, singleton on vertices 4 onward, using roots 2, 3. All four functional pairs fail, while the previous routing proof guarantees all new pairs in at most three moves. This attains . At , orders 7, 8, 9, add missing arrow to those respective graphs. At , add also , , or respectively. For order 10, , add missing arrow to the seven-core three-vertex attachment. These finite modifications have full game certificates, without any assertion that arbitrary additions preserve their guarantees.
The independent finite review covers every normalized case and degree profile above, plus all eighteen negative attached graphs, in research/small-case-rooted-independent-review.json. The literal positive graphs and ranks are in research/small-dense-two-root-certificates.json and research/small-dense-second-step-certificates.json. The ordinary reduction and finite game checks are distinct from the generic Lean results retained elsewhere in the paper.
The remaining first steps
Theorem. The first dense-step values at orders seven through ten are Together with the preceding results, this determines every dense cell in the original unresolved list. Together with the existing complete tables through order 6 and the constructions for , every admissible cell of the final dense band is exact and has an explicit attaining graph. The eventual staircase is exact throughout the final band at every order at least eleven.
Proof of the upper bounds. The seven-vertex value comes from the independently replayed complete finite table. At the other orders put and . The staircase bound gives . As above, and .
Suppose first that . If , the degree-one image count forces a disjoint missing two-cycle and an ordinary universal core on vertices with missing arrows. At , the six-vertex maximum excludes this; at , the exact value excludes it. At , it would be a universal core. Such a core has no missing degree zero or one, so one degree is three and the other seven are two. Normalize the unique degree-three row to . Complete enumeration of every other loopless degree-two row, using the two camping predicates, has no survivors. The primary search visits 3,322 prefixes; the independent chronological replay visits 189,190 prefixes.
If , all other degrees are two. Write the unique degree-one row as and put . The two pairs from exhaust the losses. Every missing column into fails under the pursuer at , and every other nonfunctional row pointing to would be killed. Thus all other good rows avoid . If , removing and the other member of leaves an ordinary universal two-out core of order , excluded by the small-order results. Otherwise removing leaves a safely rooted two-out core of order , root , among the complete exclusions above. Therefore at orders 8, 9, 10, giving respective upper bounds 12, 14, 16.
At order 8 it remains to exclude . Here . For , the four-vertex functional path leaves a rooted four-core with total excess 3. Its degree profiles are , , and . Complete all-row enumeration gives no static leaves; degree 5 is an empty row domain. For , the closed functional triple leaves a rooted five-core with excess 2, namely the one-degree-four or two-degree-three profiles already excluded above.
For , the other degrees are two except for one degree-three row. A closed two-cycle would reduce the score to a six-vertex core and is excluded by . Otherwise only with is compatible with three losses; a higher degree at , two distinct outside images, or a common outside image gives at least four. The earlier reduction with leaves either an ordinary four-core with all degrees at least two, impossible by its known maximum, or a rooted three-core with all degrees two and at most one degree-three row. Both rooted profiles were excluded.
For , normalize . Up to relabeling, or , and all other rows have degree two. Complete enumeration of all such rows has no completion with at most three distinct forced losses. The two searches use different row orders: the primary combined count is 578 prefixes; the independent counts are 12,160 and 9,934. To avoid double counting, each source stores the set of its marked missing recipients. A source-camping witness marks its entire row. A predecessor-camping witness at marks the shared missing recipient column, except for initial source , where that cop placement is excluded. The size of the union, not the sum of witness counts, is the pruning bound. Every pruned prefix therefore forces at least four different lost pairs in every completion. This completes the upper bound 11 at order 8.
Literal lower bounds. The following missing rows, listed in source order, give the four attaining graphs: Each string denotes the set of its digit labels; all labels are single digits in this table. The order-nine graph is the three-vertex attachment of a rooted six-core with two degree-three rows; its root is 6. The literal full graphs have respective exact counts 8, 11, 14, 16 and delivery bounds 3, 3, 5, 4 from both game solvers and full rank replay. These finite bounds retain the four-move staircase guarantee from order 11 and the uniform two-move guarantee from 16.
The constructor is src/small_dense_first_step.py, with fixed game records in research/small-dense-first-step-certificates.json. The independent upper-bound replay is research/small-case-first-step-independent-review.json; the literal game replay is research/small-case-first-step-literal-review.json. These are ordinary reductions and finite certificate proofs, with no claim that the new small classification has been formalized in Lean.
Missing-graph criteria and the dense endpoint
The following criterion applies to arbitrary missing graphs. The numerical constructions are now supplied by the stronger direct Theorem 58.
Lemma 18 (high-girth complement). Let be an orientation of a finite simple undirected graph of girth at least six. Suppose every vertex has outdegree at least two in . Let contain exactly the nonloop arcs absent from . Then every source–recipient pair in is guaranteed within two messenger moves.
Proof. Diagonal and direct pairs need no argument. For a missing pair of , the arc belongs to . Set Both and belong to . In the underlying undirected graph, the vertices of form an induced double star: its centers are , the other outneighbors of are leaves at , and the other predecessors of are leaves at . The two sets of leaves are disjoint, since an overlap would make a triangle. An additional edge inside would make a triangle or quadrilateral. Thus the distance between any two vertices in this induced tree is at most three.
Fix an initial pursuer vertex . If , two neighbors of in would form an undirected cycle of length at most five, so has at most one outgoing -neighbor in . The same bound holds when : a leaf at has its only incident edge in the tree directed toward it; a leaf at has only its edge toward ; and all tree edges incident with point into .
Since has at least two outgoing -neighbors, choose Then , and and are arcs of . Also and is absent from . The messenger moves to , survives every pursuer response, and delivers to on its next turn.
The lemma only requires a lower bound on outgoing degrees. In particular, edges can later be added to the underlying graph and oriented arbitrarily, provided its girth remains at least six.
Theorem 19 (the densest noncomplete all-delivery networks). At every , An attaining graph guarantees every pair within two messenger moves.
Proof. Use the direct two-type missing graph, with its odd-order subdivision when needed, and the explicit eleven-vertex core, in Theorem 58. It has exactly missing arcs and a two-move guarantee for every pair. The missing-pair upper bound proves equality.
The density is maximal for a noncomplete all-delivery graph by Theorem 14. The earlier high-girth construction at orders is no longer needed for this numerical theorem. Lemma 18 remains useful as a criterion for arbitrary missing graphs; its structural hypothesis is stronger than the condition needed by the direct construction.
Theorem 20 (a retained dense parameterization). Fix integers and , and put Every integer satisfies with a deterministic two-move attaining construction. An empty interval makes no assertion.
Proof. A nonempty interval forces . For , the displayed polynomial gives . Hence The robust bridge of Theorem 58 and the protected envelope of Theorem 48 cover every missing budget from to the latter endpoint. Their constructions have two-move delivery.
This parameterization is a consequence of the stronger dense envelope, retained for references to its explicit -dependent bound. It introduces no additional graph search, girth-growth certificate, or separate construction family.
Attainment across densities and losses near completeness
Angel Raychev proposed that, for every sufficiently large , the missing-pair bound should be attained at every integer budget Theorem 44 proves this conjecture at every using the explicit constructions of Theorems 38, 52, 58, and 59. This section gives the separate exact-budget probability argument and the dense counting and composition principles. Raychev also proposed separating existence from explicit constructions and studying how domination destroys missing pairs as the graph approaches completeness. These distinctions motivate the statements below; their proofs were developed in the September 2026 follow-up investigation.
Write and . Thus is the number of missing nonloop arcs, and always .
An exact-budget existence theorem
Theorem 25. Let , let be an integer, and put . If then some graph with exactly vertices and arcs guarantees every source–recipient pair within two messenger moves. In particular,
Proof. Apply Theorem 54 with the routing set equal to the entire vertex set: , , and . Since , the displayed hypothesis implies its condition. Theorem 54 supplies an exactly -arc graph with a safe two-move intermediary for every legal source–recipient–pursuer triple, proving the assertion.
This is an exact integer-budget existence theorem, rather than a statement about an expected number of arcs. It also gives a finite randomized search: sample graphs with exactly arcs and check the safe-intermediate condition. No practical running-time bound near the threshold is asserted.
Corollary 26. There is an absolute such that, for every and every integer budget we have . Attainment can always be achieved with delivery in at most two moves.
Proof. Let and . For , we have . If , the lower bound on gives and therefore If and , then , giving Theorem 25 covers both cases.
For the remaining dense budgets use Theorem 20 with For all sufficiently large its hypotheses hold, and its upper endpoint satisfies Since grows as a positive constant times , this endpoint eventually exceeds . Theorem 20 supplies every integer missing-arc count from to , and the probabilistic range supplies the rest. The intervals overlap, so no admissible integer budget is omitted. Both proofs give two-move delivery.
The absolute threshold is not optimized or asserted to be moderate. In particular, this corollary does not establish the full interval at . The general sparse interval between and order remains outside its conclusion.
A growing loss in the final dense band
Let be the loopless directed complement of , and write . The number counts missing pairs that fail to guarantee delivery.
Theorem 27. For and every admissible integer , Equivalently, writing , we have
Proof. If , the conclusion holds: the right-hand side is increasing with and at equals . Assume henceforth that .
Every is positive. Otherwise a vertex with can intercept every nonterminal departure from any other source, while its own source row has no missing pair. Put Since , we have . For let be its unique missing neighbor; thus . Set
Every source loses all of its missing pairs. To see this, choose with . The pursuer’s closed outgoing neighborhood in is . It can wait at while the messenger waits at and intercept every nonterminal departure. An indirect recipient cannot be reached by a direct departure.
A second obstruction applies when two distinct vertices have the same image . The missing pair loses against a pursuer starting at , whose closed outgoing neighborhood contains every possible nonterminal intermediate vertex.
Let be the set of for which has exactly one preimage in , and put . Every missing edge with tail in loses by one of the two obstructions. The killed rows in have at least two missing edges each, with tails outside . These losses are disjoint, so
If , then because , and because its members have distinct images in . Consequently If , the function maps into itself without fixed points. Its finite functional graph has a directed cycle of length at least two. Every cycle vertex belongs to and already has a preimage in , so it cannot also be the image of a member of : that member is outside and would give a second preimage. Thus , as well as . It follows that Using proves the bound.
Thus the forced loss increases as as the arc budget moves one, two, three, four, five, six, and further steps above . At the other endpoint, , the bound agrees with Theorem 13.
Combining two-move constructions
Lemma 28. Suppose a missing-edge graph is a disjoint union of graphs , each with positive outgoing degree at every vertex. Let be the complement on its own block. If an indirect pair in can be guaranteed within two messenger moves, then it remains guaranteed in the complement of the entire .
Proof. Let the source and recipient lie in block . If the initial pursuer also lies there, the original two-move strategy chooses an intermediate vertex outside its closed outgoing neighborhood. The same is true in . The pursuer may respond by moving outside the block, but this cannot prevent receipt on the messenger’s next move.
If the pursuer starts at in another block, choose any outgoing -neighbor of in that block. The arcs and are present in because they cross blocks, whereas is absent. Also . This gives the required safe two-move delivery.
The lemma concerns two-move strategies. No preservation theorem for arbitrary longer strategies under this join is assumed.
Theorem 29. Let and . If , then An explicit polynomial construction attains this value with every counted pair delivered within two messenger moves.
Proof. Use the functional missing graph on vertices, with guaranteed pairs. On the other vertices use the direct missing core in Theorem 58, which has guaranteed missing pairs. Both blocks have positive missing outdegree, so Lemma 28 preserves all guarantees in the complement of their disjoint union. There are missing arcs, and Theorem 27 gives optimality.
This includes the former range and the separate 26-vertex block, without any finite girth-growth dependency. In missing-budget notation the range is .
A restriction on permutation constructions
Proposition 30. Suppose the two outgoing neighbors of each vertex are and , where are commuting permutations, both images differ from , and . Then . In fact all indirect guarantees are decided by a two-move criterion.
Proof. Fix a recipient and put . Commutation gives The predecessor camping lemma excludes every indirect source except possibly : a pursuer starting at can intercept the messenger when it first reaches a predecessor of . Thus each recipient contributes at most one pair.
When , the pair is missing because neither predecessor of a loopless recipient equals that recipient. This pair is guaranteed exactly when no has . Necessity is the same camping lemma. For sufficiency, from each legal initial pursuer position choose . The messenger moves from to this safe predecessor and then delivers.
The bound is sharp: on , take arcs and . For recipient zero the predecessors are , and the only closed outgoing neighborhood containing both is that of . The criterion gives ; translation gives exactly the seven pairs . Since for , commuting permutations cannot supply a universal vertex-extremal graph in that range. Noncommutation is necessary, not asserted sufficient.
An extension that fills the small dense offsets
Proposition 31. Let , , and . If then a deterministic polynomial construction attains with a two-move strategy for every counted pair.
Proof. The functional construction has guaranteed pairs. Its vertices with no missing incoming arc are the branch sources, together with the spare vertex when is odd. There are exactly such roots. Give each added vertex a different two-element missing-neighbor set among these roots. The functional-root argument in Theorem 58 proves all new missing pairs and preserves the original pairs in two moves. The identity and Theorem 27 prove equality.
This strengthens the former bound when is odd and preserves it when is even. In particular, all the earlier , cases remain covered.
Theorem 58 supplies the common direct construction and complete proof. The ordinary counting bound, the arbitrary-block composition lemma, and the commuting-permutation restriction remain independent structural results. No new Lean formalization is asserted here.
Exact final dense band
Theorem 32. For every , A deterministic attaining graph guarantees all but two of its missing pairs within two messenger moves.
Proof. Use the four-vertex attachment to a direct two-type core in Theorem 58. The graph has missing arcs. Exactly the two missing pairs leaving the attachment’s vertex are blocked by a pursuer at ; every other missing pair has a safe two-move intermediary. Theorem 27 gives the matching upper bound.
Corollary 33 (the complete final dense band). For every and every integer , Equivalently, for every integer , There is a deterministic polynomial attaining construction at every such budget, with a two-move strategy for every counted pair.
Proof. Theorem 27 gives the upper bound. The first step is Theorem 32. For , put . If , Theorem 29 applies. Every remaining positive is at most nine, so and Proposition 31 applies. Finally is the functional endpoint of Theorem 13.
Together with Theorem 19 at and Theorem 13 above , this determines the joint maximum for every and . At the boundary the value is ; the next step has value ; the staircase then reaches before becoming zero. The proof does not assert that 20 is the smallest possible whole-band threshold.
The core and attachment formulas and their complete ordinary proofs are given together in Theorem 58. The eleven-vertex core is listed explicitly and independently checked; its two-move guarantee is also formalized in Lean. The general composition and attaining-existence statements remain ordinary proofs.
A quadratic dense interval from three safe intermediaries
The sparse missing graph need not retain large girth while its density increases. Three designated outgoing missing arcs per vertex suffice, provided certain differences between their endpoints stay protected. The resulting construction covers a quadratic interval of missing-arc counts by a direct modular rule.
Theorem 48. For every integer , put At every integer missing-arc count , an explicit graph attains Every source–recipient pair in the construction is guaranteed within two messenger moves. Arbitrary intermediate subsets of the specified optional missing arcs are permitted.
Proof. Work in , and put We shall construct a set containing , not containing zero, with the following properties:
- Each difference in has exactly its original ordered representation between two members of , and no other ordered representation between members of .
- No difference between two members of belongs to .
For , these properties hold for : its six ordered nonzero differences are precisely the six distinct members of , and none belongs to .
Whenever , adjoin any residue outside The exclusion of preserves all protected representations, and the exclusion of preserves the second property; both difference sets are symmetric. At most residues are excluded. If , this quantity is strictly less than , so the process continues. Starting with three members, it produces ; choosing the smallest permissible representative makes the rule deterministic.
Let be any loopless digraph satisfying Let be its directed complement. We prove all missing pairs of have safe two-move intermediaries, using only the three designated missing neighbors of each initial pursuer position.
Fix a missing pair and initial pursuer position . Translate so , and write and . The three candidates are the members of . A candidate is suitable if it lies outside Indeed, this ensures both messenger arcs are present in , while the candidate is a missing outgoing neighbor of and therefore cannot be reached on the pursuer’s response.
At most one candidate belongs to . Otherwise, for distinct , the difference of is the protected difference . Its unique representation forces and , contrary to .
At most two candidates belong to . If the candidates with steps belong there, the two elements of have protected difference . Its unique representation is , so If the third candidate, with step , also belonged to , the same argument applied to would give , a contradiction.
If all three candidates were blocked, the remaining candidate would have to belong to , while the other two are in . Setting , the displayed equality gives As runs over and are the other two steps, this difference is respectively . Each belongs to , contradicting the second property of . Hence a suitable candidate exists.
The suitable candidate differs from because . It differs from both endpoints: and . Thus the messenger first moves to it, survives every response, and then reaches ; receipt precedes any subsequent interception. This argument uses only the envelope containments, so no translation symmetry of the chosen intermediate is needed.
The compulsory missing graph has arcs and the full envelope has arcs. Adding any chosen number of optional missing arcs gives each integer in this interval, with all missing pairs guaranteed. The missing-pair upper bound proves equality.
Theorem 58 now subsumes this entire numerical range, including the orders 19 through 21, while preserving two-move delivery and every optional subset. The proof above is retained as a distinct sufficient condition on arbitrary protected difference sets. The main numerical catalogue therefore no longer counts this as an additional dense interval.
The executable construction and bounded checks are in src/dense_protected_envelope.py; their exact finite scope is recorded in research/dense-protected-envelope-checks.json. The ordinary theorem is independent of those finite pursuit-game checks. No new Lean coverage is asserted.
Finite extrema
Completion of the finite sparse budgets
The ordinary source/sink and positive-support lemma supplies one common reduction. We use the exact smaller budgets in increasing order, followed by the complete finite exclusions listed below. The game and counted pairs are unchanged: messenger first, waiting allowed, receipt before capture, and distinct nonadjacent source–recipient pairs.
Theorem (finite sparse-budget values). The budgets twelve through twenty-one have the following global maxima and least attaining host orders:
| 12 | 13 | 14 | 15 | 16 | 17 | 18 | 19 | 20 | 21 | |
|---|---|---|---|---|---|---|---|---|---|---|
| 9 | 11 | 13 | 15 | 19 | 28 | 33 | 40 | 53 | 60 | |
| Least host | 7 | 8 | 8 | 8 | 8 | 10 | 9 | 11 | 10 | 12 |
For every , . The exceptional smaller-host values are
The finite domains, in budget order
Write , for (56.3), and for the positive-support bound (56.4). The exact values through eleven arrows are already established. At each following budget, use only the preceding exact values.
Budgets twelve through sixteen. In a strict counterexample to the displayed value, a degree-one source or sink is impossible because is smaller. A source or sink of other degree at least three has score at most at the five respective budgets, again at or below the displayed target. Thus every nonisolated source or sink has other degree exactly two. Every nonisolated vertex has total degree at least two, so the support has order at most . This directly justifies the comparison hosts 12 and 13 for their complete exclusions: a smaller support is padded with isolates. No final least-attaining-host value is used to prove either comparison.
For budgets fourteen through sixteen, the deleted degree-two row or column must be live, because otherwise deletion gives the smaller value . A source-to-sink arrow would contradict its required two nonsink successors or two positive-indegree predecessors. These observations also hold at twelve and thirteen, although their full-host exclusions already cover the permitted graphs.
For completeness, the simultaneous live capacities used by the retained enumerators follow from the same lemma. Let be the total outgoing degree of all indegree-zero vertices and the total incoming degree of all sinks. If are the numbers of live rows and columns, then With active sets of sizes and overlap , the count for actual live rows and columns gives Routes through nonlive vertices remain available; this counts pairs, not an induced game on live vertices.
The complete twelve- and thirteen-arrow exclusions have respectively 65 and 88 outgoing-degree profiles. The fourteen- through sixteen-arrow packages cover all permitted positive and degree-two-zero profiles on supports nine through , together with the reviewed eight-vertex bounds 13,15,19. The retained seven-vertex bounds at those budgets are 10,11,12. Consequently every support is covered. The literal attainers give equality, allowing the induction to continue.
Budgets seventeen through twenty-one. Once the preceding exact values are known, every graph with an actual source or sink is bounded as follows:
| 17 | 18 | 19 | 20 | 21 | |
|---|---|---|---|---|---|
| 22 | 28 | 36 | 42 | 53 |
All are strictly below the global target. For positive support, (56.4) leaves the following finite domains; support cannot exceed .
| Supports requiring finite exclusions | Larger-support arithmetic bound | |
|---|---|---|
| 17 | 9,10 | for |
| 18 | 9,10,11 | for |
| 19 | 9,10,11 | for |
| 20 | 10,11 | for |
| 21 | 10,11 | at , and for |
At seventeen arrows, the retained eight-vertex value 19 excludes every smaller host by isolate padding. At eighteen use . At nineteen, twenty and twenty-one, the missing-pair bounds on the respective smaller supports are 37,52,51. These are independent of the global values being proved.
The seventeen- and eighteen-arrow joint-degree exclusions therefore give the claimed maxima and . At nineteen arrows the complete positive-support exclusions give 35,38,40 on orders 9,10,11. The general source/sink bound 36 suffices at ten and eleven. At nine vertices it sharpens to 25: degree-one deletion gives , degree two gives , and degree at least three gives . An isolate leaves the retained value . Thus the fixed-host claims also cover every graph.
At twenty arrows, the positive ten-vertex possibilities above 53 are the regular family, the two directional single-transfer families, and eleven joint-degree multisets comprising double transfers or a transfer in both directions. The existing regular and directional bounds are 53; the complete eleven-profile exclusion supplies the same bound for the remainder. On eleven vertices, exceeding 53 requires : there are two degree-one vertices in each direction and all other degrees two. The complete two-defect exclusion retains all overlaps of the low sets and gives 53. This finishes the global bound without the historical nineteen-arrow upper 53 or the comparison-host argument.
At twenty-one arrows, the ten-vertex exclusions bound the one-excess family and the twelve remaining joint-degree multisets by 56. All other positive degree counts have cap at most 54. At eleven vertices, the one-low-in/one-low-out family has upper 56; the remaining cases above 58 have or and are included in the complete eleven-profile exclusion with upper 58. The five profiles in that inventory already have cap 57. The source/sink bound 53 applies on both hosts, so their literal values 56 and 58 are exact. The twelve-vertex literal attains the arithmetic upper 60. No separate nineteen-arrow upper 49 is needed.
Every lower bound is a saved literal graph with complete winning ranks and a closed losing region independently checked. Adding isolates preserves its score. Least attainment at seven and eight follows from and . The displayed smaller-host values handle budgets 17,19,21; at eighteen use , and at twenty a nine-vertex graph has only52 missing pairs. This proves all assertions.
The next endpoints use exactly the same reduction: at twenty-two arrows, , positive supports at least twelve have cap 74, and supports at most ten have at most 68 missing pairs. Only order eleven remains. At twenty-three, , positive supports at least thirteen have cap 76, and supports at most ten have at most 67 missing pairs. The twenty-two- and twenty-three-arrow sections complete those residual families, in that order.
What a complete finite exclusion establishes
Each producer lists every permitted degree profile. Joint profiles assign incoming degrees to sorted outgoing degrees, sorting only within equal-outdegree classes. Zero entries are retained whenever the ordinary reduction permits them. Adjacency rows are assigned completely. Future vertices may be permuted only when their prescribed degree pairs and already fixed incoming prefixes agree; these permutations fix every completed row. Choosing every possible cardinality and a prefix in each such class retains a representative of every completion. Earlier vertices remain individual choices, loops are forbidden, and opposite arrows are independent. Matching-based families retain their separately proved complete factorization and normalization.
Pruning subtracts permanent losses as a union. Source camping requires a different initial cop; predecessor camping retains the source-equals-cop exception. A column loss applied to an unfinished row uses a full column, so a future direct arrow cannot be subtracted twice. Guarded-path tests grant the messenger every individually possible future arrow and keep only fixed cop arrows, permitting the initial escape and terminal receipt. Failure in this easier game is permanent. Every surviving leaf is evaluated in the actual alternating game. Early exit uses the current count plus every unprocessed eligible pair as an upper bound. An incumbent rises only after a literal larger score is evaluated; earlier prunes remain valid under the larger final bound. Complete traversal therefore excludes every score above that bound.
Evidence and computational boundary
The following records, under research/, specify the exact completed families, source hashes, literal graphs, and independent reviews. Counts refer to residual families; inherited finite results retain their original evidence.
- Budgets 12–13.
endpoint40_tiny_live_review.jsonsupplies complete 65- and 88-profile exclusions, independently counted inventories, and independent checks on 6,651 graphs, 44,376 prefixes and 662,312 specific camping states. It does not claim a second full graph traversal. - Budgets 14–16.
finish_budget_manifest.jsonandfinish-budget-ordinary-review.jsonsupply complete prescribed-degree residual families, with 118,547 leaf games independently replayed, together with the reviewed eight-vertex bounds. - Budgets 17–18.
finish_eighteen_review_manifest.jsonandfinish_eighteen_review_seventeen.jsonsupply exact joint-profile set comparisons, with 73,472 package leaf games and 26,662 stronger seventeen-arrow leaf games independently replayed. - Budget 19.
sparse_finish_nineteen_exact_manifest.jsonandfinish_nineteen_review_manifest.jsonsupply 153 complete joint profiles and 291,301 independently replayed leaf games; the literal host values are 35, 38 and 40. - Budget 20.
finish-sparse-review.jsonsupplies independent coverage and game review of the new residual families, with 19,286 leaf games. Inherited regular and directional-transfer bounds are explicitly identified. - Budget 21.
sparse_finish_twentyone_manifest.jsonandfinish-twentyone-review.jsonsupply complete matching and joint-degree families, independent alternating-game leaf replays and permanent-loss checks; the literal host values are 56, 58 and 60.
The independent game replays use a separately written alternating-state attractor. For literal attainers, finite winning ranks and all losing-closure conditions are checked. Except where a record explicitly supplies a second generator, replay reuses the independently reviewed producer traversal. These are ordinary finite proofs with auditable computational premises; they do not claim new concrete Lean certificates.
The eight-vertex row is now completely classified: the sparse, lower-main and upper-main receipts are endpoint40_n8_sparse_receipt.json, endpoint40_n8_low_receipt.json, and endpoint40_n8_high_receipt.json, with the separate high-budget review in finish-n8-review.json; retained formulas and literal completions cover the intervening and dense ranges. Together with the other completed nine- and ten-vertex families, these close every finite exception. The final main-cell values are , , , , and . The complete finite tables identify their matching graph records; the approved small-case registry pins their separate exclusions and independent reviews.
Exact extrema with at most seven arcs
Proposition 23. Allowing arbitrarily many vertices, including isolated vertices,
Proof. Write , , , , and . Every counted pair belongs to , excludes the diagonal, and excludes arcs. Consequently For completeness, the second inequality follows by counting the arcs leaving and those entering : their respective totals are at least and , and their union has at most arcs.
A counted pair requires two arcs leaving and two entering . These four arcs are distinct because is absent. Thus when .
We will use two elementary camping observations. If , , and , then no indirect pair ending at is guaranteed. Indeed, let be its other predecessor. An indirect source is neither nor . A pursuer starting at can wait there: the messenger cannot reach , and cannot enter without being captured before reaching . Dually, if , , and , then no indirect pair starting at is guaranteed. A pursuer waits at the other successor of ; the messenger’s only alternative departure reaches a sink different from the indirect recipient.
Suppose first that or . Then . If either is zero there is nothing to count, and if both are one the bound is immediate. When , (23.1) gives . When and , two counted pairs would have the same source and distinct recipients. The source’s two outgoing arcs are then disjoint from the at least four arcs entering those recipients, which would require . The case follows by the same count with sources and recipients interchanged: at least four arcs leave the two counted sources, and the recipient’s two incoming arcs are disjoint from them. Hence .
Now let , so that . If , three counted pairs would require two outgoing arcs from their common source and six disjoint arcs entering their three recipients; this is impossible. Thus . The same argument applies when ; cases with a zero coordinate are again immediate. If , (23.1) gives .
Consider . Every arc ends in , and every vertex of has indegree exactly two. If , then and (23.1) gives . Otherwise choose . It has indegree zero and at least two distinct successors in . The first camping observation eliminates both corresponding recipient columns. At most one column remains, containing at most the two sources in . Thus .
For , every arc starts in and every vertex of has outdegree exactly two. If , the same count gives zero. Otherwise a vertex has outdegree zero and at least two predecessors in . The second camping observation eliminates their two source rows, leaving at most one row and two recipients. Again .
Finally, if , all six arcs go from to , and all relevant indegrees and outdegrees equal two. If , (23.1) gives . Otherwise a vertex of has indegree zero and eliminates two recipient columns by the first camping observation. The remaining column has two distinct predecessors in , so at most one of the three sources can contribute an indirect pair. This completes the upper bounds in all cases.
For the lower bounds, the four-arc diamond guarantees the indirect pair : the messenger chooses the branch not occupied by the pursuer and delivers on the next move. Adding a disjoint arc gives the five-arc example. The six-arc graph guarantees both and . If the pursuer starts on one branch, choose the other; if it starts at either sink, choose either branch. In each case it cannot reach the selected branch on its next move, and receipt then occurs on the messenger’s second move. Hence , as required.
These arguments establish the arc-only maximum over every finite vertex set; no restriction on the number of nonisolated vertices is used.
Proposition 24 (with a finite exhaustive computation). We have
Proof. First consider a weakly connected digraph with at most seven arcs and at least seven vertices. Forget the directions but retain one undirected edge for each arc, so that opposite arcs become parallel edges. The resulting connected multigraph has at most as many edges as vertices. It is therefore a tree or has exactly one cycle; a parallel pair is allowed as a cycle of length two.
In a tree, any reachable indirect source–recipient pair has an internal vertex separating its endpoints. A pursuer can start and wait there, preventing delivery. Thus no indirect pair is guaranteed. In the unicyclic case, a pair with either endpoint outside the unique cycle likewise has an internal separating vertex, unless its endpoints are adjacent in the underlying graph. For adjacent endpoints off the cycle, a directed route exists only if their connecting arc has the required direction, making the pair direct. Thus every counted pair must have both endpoints on the cycle.
There are exactly two simple undirected paths along that cycle between two distinct cycle vertices. If only one is a directed path from the source to the recipient, it is either a direct arc or has an internal vertex where the pursuer can wait. If neither is directed, the recipient is unreachable. Excursions into attached trees cannot bypass an internal cycle vertex. Consequently a counted pair requires both cycle paths to be directed from its source to its recipient. This forces the cycle’s unique divergence at that source and unique convergence at that recipient; every other cycle vertex has one entering and one leaving cycle edge. A fixed orientation can therefore support at most one such ordered pair. A cycle of length two consists of opposite arcs and supports no indirect pair. We have proved that every weakly connected digraph with at most seven arcs and at least seven vertices has .
For a general digraph with seven arcs, distinct weak components contribute additively to . Each component with a positive contribution uses at least four arcs by Proposition 23, so at most one component contributes. If that component uses at most six arcs, Proposition 23 bounds its contribution by two. If it uses seven arcs and has at least seven vertices, the preceding argument bounds its contribution by one. In the only remaining case it has at most six vertices. Adding isolated vertices to make six does not change its indirect guarantee count, and the complete six-vertex enumeration gives a maximum of two at seven arcs.
This last finite assertion is the computational dependency of the proposition. It is reproduced by src/enumerate_small_n6.cpp; the result is recorded with complete: true in research/solver-enumeration-n6.json. The enumeration covers every six-vertex digraph up to the degree-ordering reduction described in the computational section; the witness is also checked by the separate explicit-turn solver. The structural reduction above is what extends that finite calculation to unrestricted vertex counts.
Finally, add one disjoint arc to the six-arc, two-recipient construction in Proposition 23. This preserves its two guarantees and supplies seven arcs, proving the matching lower bound.
Theorem 49 below settles the next four budgets, eight through eleven.
Exact arc maxima from eight through eleven
The six-vertex table supplies useful lower bounds, but does not itself settle an arc budget when the number of vertices is unrestricted. At eleven arcs the distinction is essential: seven vertices attain eight guarantees, exceeding the six-vertex maximum of seven.
Theorem 49 (with finite exhaustive certificates). Over all finite vertex sets,
Proof of the support reduction. Indirect guarantees add over weak components. Every component with a positive contribution has at least four arcs. At these budgets there can be at most two positive components. If there are two, each has at most seven arcs; Propositions 23 and 24 give a combined maximum of at most three. This cannot improve any of the displayed lower bounds.
There is therefore only one relevant positive component. We argue in increasing order of the budget . If this component has fewer than arcs, the already established smaller-budget maximum bounds its contribution by the displayed value at . If it uses all arcs and has at least vertices, the tree-or-unicyclic argument in Proposition 24 gives at most one indirect guarantee. That argument only needs a connected underlying multigraph with at most as many edges as vertices, so applies unchanged at the present budgets.
In the remaining case the component has at most vertices. Pad it with isolates to exactly vertices; its arc count and indirect count do not change. Hence each upper bound reduces to the following one finite counterexample test:
| Arc budget | Host order | Excluded threshold for |
|---|---|---|
| 8 | 7 | 5 |
| 9 | 8 | 6 |
| 10 | 9 | 7 |
| 11 | 10 | 9 |
Complete finite upper checks. Both enumerators list all prescribed outdegree profiles with total in sorted order and then all loopless outgoing rows. As in the canonical reduction of Theorem 46, future vertices with equal prescribed degree and equal incoming pattern from completed rows can be permuted while leaving every completed row unchanged. Choosing the new row’s neighbors as a prefix of each such contiguous cell retains a representative of every graph. The second implementation instead uses descending degrees and suffixes. Both reduction arguments fix the current vertex and all completed vertices.
The source and predecessor camping conditions of Theorem 46 supply necessary local rejections. A completed degree-two source that points to a prescribed sink also contributes zero, by the earlier sink obstruction. Otherwise a source of degree contributes at most . A target of current indegree contributes at most , or zero if its indegree cannot reach two.
One additional numerical bound makes these sparse checks short. Let contain all sources not yet excluded, and put . Every member of has prescribed outdegree at least two. If the eventual number of indegree-at-least-two targets is , the same degree-incidence count as (1) gives To bound at a partial assignment, let be the number of arcs still to be assigned. A target currently of indegree needs at least of these arcs to reach indegree two. Discard targets with too few remaining possible predecessors, and select as many of the others as possible using the smallest such costs first, with total cost at most . The resulting is an upper bound: each remaining arc enters only one target. Maximizing the displayed bound over is therefore a safe partial rejection. No sufficiency is assumed for these degree or camping tests.
Every remaining complete graph is evaluated by the original finite reachability game. The primary implementation uses synchronous messenger-position masks; the independent implementation uses an explicit alternating-state queue attractor. Both start with terminal receipt states and compute the least winning region, including waiting and all pursuer responses. They reject every candidate at every one of the four thresholds. The exact enumeration counts are supplied in the reproduction receipt; both runs report complete enumeration rather than termination at their time limit. This proves the four upper bounds.
Lower witnesses. The witnesses at eight, nine and ten arcs are the graphs in the six-vertex table. The eleven-arc witness has seven vertices and the following outgoing neighborhoods:
| Vertex | Outgoing neighbors |
|---|---|
| 0 | 1 |
| 1 | 0 |
| 2 | 3 |
| 3 | 4, 5 |
| 4 | 0, 2 |
| 5 | 3, 6 |
| 6 | 1, 2 |
Its guaranteed indirect pairs are Both independent game solvers check each of the four lower witnesses, and the saved explicit ranks satisfy every legal-move obligation. They attain the upper bounds and complete the proof.
The complete reproduction command is python3 src/small_arcs_resume.py. Its two exhaustive sources are src/small_arcs_sparse_primary.cpp and src/small_arcs_sparse_independent.cpp; the receipt, source hashes, complete enumeration summaries and all four lower rank certificates are in research/small-arcs-resume-verification.json. The final full reproduction took about eighteen seconds. These are finite computer-assisted proofs with an ordinary all-order support reduction; they have not yet been formalized in Lean.
Small vertex orders
The smallest order attaining the vertex bound is twelve. This statement is about attaining the bound, not about the first noncomplete network in which all pairs are guaranteed: the latter already occurs at seven vertices.
Theorem 46 (with finite exhaustive certificates). The seven-, eight-, and eleven-vertex maxima are In addition, and . The intermediate vertex bounds proved here at orders nine through eleven are:
| Lower bound for | Upper bound for | |
|---|---|---|
| 9 | 48 | 53 |
| 10 | 62 | 69 |
| 11 | 85 | 85 |
There is no universally winning two-in/two-out regular digraph on any of vertices. Together with the previous exact results through six vertices and Theorem 40, this implies that twelve is the smallest order for which .
Proof of the lower bounds. The finite witnesses at orders seven through ten have respectively arcs and guarantee every pair. Their complete graph and winning-strategy certificates are provided in research/small-exceptional-general-certificates.json, with the improved nine-vertex witness in research/root-small-structured-9-certificate.json. The earlier eleven-vertex witness with 26 arrows remains in research/small-exceptional-structured-11-certificate.json. A new 25-arrow witness improves its count from 84 to 85; its outgoing rows are Two independent attractor algorithms agree; each stored alternating-state rank satisfies all messenger-choice and universal pursuer-response obligations. Thus gives respectively. The new literal witnesses are consolidated in research/small-case-results.json and independently replayed by src/small_case_certificate_review.py. For concreteness, the seven-vertex witness is the following graph, whose guarantees require at most four messenger moves:
| Vertex | Outgoing neighbors |
|---|---|
| 0 | 1, 3, 6 |
| 1 | 0, 4, 6 |
| 2 | 0, 5, 6 |
| 3 | 1, 2, 5 |
| 4 | 0, 2, 3 |
| 5 | 1, 3, 4 |
| 6 | 2, 4, 5 |
Seven-vertex upper bound. If a graph has at most thirteen arcs, the arc-only bounds give ; it suffices here to use monotonicity of (pad by disjoint one-way arcs) and . A graph with at least twenty-one arcs has at most missing pairs. It remains to exclude for .
We describe the finite reduction and every rejection rule. Write , and . A counted pair necessarily satisfies
- , , and ;
- for every ;
- for every .
The degree conditions are the one-neighbor camping obstructions. For condition 2, a pursuer waiting at captures the messenger after its first departure from . For condition 3, it waits at and captures the messenger upon the first entry into a predecessor of , before the next messenger move can deliver. Indefinite waiting by the messenger also fails to deliver. These arguments respect receipt priority because an indirect source is not itself a predecessor of its recipient.
Let be the number of pairs satisfying these three conditions. Then . A source contributes at most four pairs, so requires at least six sources of outdegree at least two. Every graph can be relabeled in nondecreasing outdegree order, allowing only the first row to have degree below two. We enumerate every loopless outgoing row mask in that order, with total degree between fourteen and twenty. This includes every possible graph, with harmless repetitions. At a partial assignment, the following bounds allow safe pruning:
- A completed row of degree contributes at most , or zero if a known completed row already violates condition 2. Each remaining row contributes at most , where is the smallest outdegree still allowed by the ordering.
- A target currently of indegree contributes at most . Its contribution is zero if the remaining rows cannot raise its indegree to two.
- The total arc count must remain extendible to the interval .
No omitted edge can repair a rejected completed source: the covering closed neighborhood only grows. The incoming-degree bounds likewise use upper estimates on all possible completions. At every surviving complete graph we count directly. The exhaustive enumeration has recursion nodes and complete leaves before an optional indegree tie normalization. None has . A separate implementation uses boolean adjacency, descending outdegree order, and no indegree tie normalization; it completes nodes and the same leaves, again with no survivor. This proves in the remaining arc range. The lower witness proves equality.
Eight-vertex upper bound. At most fifteen arcs give ; at least twenty-four arcs leave at most thirty-two missing pairs. To exclude , it therefore suffices to examine . Each source contributes at most five pairs, so at least seven sources must have outdegree at least two. The same camping conditions and partial bounds used above apply with eight vertices.
For this slightly larger search we also remove labeling redundancy. Fix a nondecreasing outdegree sequence. After the outgoing rows numbered less than have been chosen, partition the unassigned vertices into cells with equal prescribed outdegree and identical adjacency from all completed rows. Vertices in such a cell may be permuted without changing any completed row or degree requirement. Therefore, when choosing row , its neighbors among the future vertices of each cell may be required to form a prefix of that cell. This loses no graph: permute within each cell to put the neighbors first, fixing row and all previous vertices, and continue recursively. The new cells are obtained by splitting the old cells, so their contiguity is preserved. The analogous suffix rule and reversed degree order are equally complete.
The primary search completes all degree sequences, with recursion nodes and complete leaves. Only leaves satisfy the necessary pair bound . Exact least-attractor evaluation rejects all of them; the largest actual among these survivors is seventeen. Thus no graph has , proving . The ordinary canonicalization and every pruning rule were independently audited; as an additional small positive check, every labeled loopless four-vertex graph was canonicalized in both prefix and suffix conventions and its relabeling and prefix conditions checked. Independent complete suffix enumeration and the explicit alternating-state game provide a second finite verification: its completed intervals and cover all degree profiles. They visit nodes and complete leaves, with static survivors, all rejected. The differing counts reflect the opposite degree order and suffix convention, which choose a different redundant collection of representatives. Both implementations give the same zero-survivor conclusion.
Eleven vertices and twenty-three arrows. We prove . If vertices have outdegree at least two, the other vertices emit at most arrows and cannot be indirect sources. The eligible rows therefore contain at most missing pairs. This is at most 78 for . The incoming argument is identical: an indirect recipient requires at least two predecessors. Consequently, a graph with at least 79 guarantees must have all indegrees and outdegrees at least two. There is exactly one outdegree-three vertex and one indegree-three vertex , which may coincide; all other degrees are two.
The bipartite arrow graph has a perfect matching. Indeed, a source set emits at least arrows, whereas fewer than recipient columns have total capacity at most . This contradicts a failure of Hall’s condition. The matching is a fixed-point-free permutation. Up to simultaneous relabeling there are fourteen possible cycle partitions of eleven into parts at least two. Rotating cycles and swapping cycles of equal length places at the first vertex of one cycle of each distinct length. Allowing all eleven positions for retains every relation between the exceptional vertices and gives 330 patterns in total. The remaining arrows have outgoing degree one except two at and incoming capacity one except two at . Enumerating all residual rows, avoiding loops and matching arrows, covers the entire class. The two residual neighbors at are chosen in increasing order.
During this enumeration, source and predecessor camping identify permanent losing pairs, retaining the exception when the initial source equals the camping vertex. No camping class is excluded in advance. A partial cop row contains only arrows that persist; a predecessor set is used only when its prescribed capacity is full. The permanent losing pairs are copied separately at each recursion depth. A row contributes at most the smaller of its final missing-pair count and the number of targets not already direct, diagonal, or permanently losing.
The guarded-path bound uses every still-possible messenger arrow and only fixed cop arrows. It permits the first move to escape the cop’s closed neighborhood and the final move to deliver anywhere; only interior positions must avoid that neighborhood. Thus a failed optimistic route certifies a losing pair in every completion. Surviving graphs receive exact recipient least-attractor evaluation. Solved recipient counts plus the remaining potentially winning pairs form an upper bound, so the game calculation may stop once this is at most 78.
The complete ranges of cycle partitions – and – visit 121,790,823 nodes and reach 1,152,430 exact game decisions. Every decision rejects a score of at least 79. The recorded value is an early rejection sentinel, not a graph score. The source, complete receipts, and independent ordinary audit are respectively src/small_sparse_one_excess.cpp, research/small-sparse-one-excess11-partitions1-6.json, research/small-sparse-one-excess11-partitions7-14.json, and research/small-plateau-one-excess-review.md. The independently rank-verified literal 78 witness is included in research/small-case-results.json, proving equality.
Eleven vertices and twenty-four arrows. We prove . The certified attaining graph has outgoing rows Suppose a graph at this budget has . If exactly ten source rows have outdegree at least two, at least 23 arrows start in those rows, so they contribute at most pairs. At most nine eligible rows give at most . The incoming-degree count is identical. Thus every indegree and outdegree is at least two. The total surplus above two is two on each side, so the outgoing degree profiles are and , and no degree exceeds four.
There are 86 missing pairs, permitting at most six failures. Source camping would make an entire row fail. To lose at most six pairs that source would need outdegree four. It then uses all outgoing surplus, while every other cop has a closed neighborhood of size three and cannot cover its four successors. Hence source camping is impossible.
First suppose there is no predecessor camping either. The preceding canonical row method, in descending degree order, enumerates both degree profiles. Incoming feasibility requires enough unassigned tails to reach indegree two and to escape every completed cop neighborhood covering a current predecessor set. If no single tail escapes them all, at least two new predecessors are required; summing these lower bounds over recipients cannot exceed 24. At a complete graph, each counted pair must also have a route to a predecessor of its recipient through vertices outside every stationary cop’s closed neighborhood. The final arrow into the recipient is exempt from this avoidance requirement, so receipt priority is respected. This gives a necessary pair-count filter before exact game evaluation.
The complete target-80 run visits 186,865,392 nodes, 2,805,991 complete camping-free graphs, and 371,060 guarded-path survivors. Its largest actual count is 79. Every pruned branch has a proved upper below 80. The frozen receipt is research/small-loss-n11-m24-camping-free-80.json.
If predecessor camping occurs at with cop , at least missing pairs fail. Thus is three or four, and no other column may be camped. For degree four there are three cases: , , or . In each case has outdegree four, and its outgoing set is respectively , , or . All other degrees are two. For degree three, the exceptional cop-source pair must be indirect, so . The cop has outdegree three or four. In the latter case its extra neighbor can be normalized to one outside vertex, and the second indegree-three vertex has ten possible labels. In the former case the second outdegree-three vertex has three symmetry types: , a predecessor of , or an outside vertex. Retaining all ten possible labels of the second indegree-three vertex gives another 30 configurations. Together with the three degree-four cases, this is configurations.
Exact incoming caps, the prescribed predecessor set at , and colored prefix cells preserve all these cases. The colors retain degrees, recipient status, and predecessor membership. Source camping and camping at every other column remain forbidden. A complete enumeration of all 43 configurations visits 113,000,606 nodes, 603,453 leaves, and 66,362 guarded-path survivors; its largest evaluated count is 73, and no graph reaches 80. This proves , matching the witness. The source and complete receipt are src/small_loss_camped_profiles.cpp and research/small-loss-n11-m24-camped80.json; the ordinary completeness audit is research/small-plateau-camped80-review.md.
At most 21 arrows give by the retained arc bounds. At budgets 22 and 23 the bounds are respectively 79 and 78. We have just proved the value 79 at budget 24. At least 25 arrows leave at most 85 missing pairs. The universal 25-arrow witness therefore proves .
Nonattainment at orders eight through eleven. By the vertex equality criterion, an attaining graph would be universally winning and have indegree and outdegree exactly two everywhere. Any such directed graph is the union of two arc-disjoint permutation factors. Indeed, its bipartite tail/head incidence graph is two-regular, so alternating the edges around each even cycle gives the two perfect matchings. Both permutations are fixed-point-free. Up to simultaneous relabeling, the first permutation may be put in canonical cycle form for each partition of having no part one; enumerate every second permutation avoiding both the diagonal and the first permutation’s arcs.
The source and predecessor camping conditions above reject a branch as soon as a completed two-element neighborhood is covered by a known closed outgoing neighborhood. For the predecessor condition, at least sources are indirect, so a covering vertex can be avoided as the initial source. Every remaining complete graph is evaluated by the finite least-attractor algorithm. The exhaustive counts are:
| Cycle partitions | Recursion nodes | Locally admissible complete graphs | Universally winning graphs | |
|---|---|---|---|---|
| 7 | 4 | 142 | 0 | 0 |
| 8 | 7 | 1,446 | 0 | 0 |
| 9 | 8 | 10,996 | 535 | 0 |
| 10 | 12 | 231,676 | 35,610 | 0 |
| 11 | 14 | 2,177,946 | 120,302 | 0 |
An independent implementation reverses the permutation assignment order. Its local tests forbid directed transitive triangles, two distinct length-two walks with the same ordered endpoints, and duplicate completed outgoing pairs; these are precisely the same camping obstructions in adjacency-matrix form. It then uses an explicit alternating-state AND/OR queue attractor instead of the primary synchronous bitmask iteration. Both complete enumerations give exactly the displayed counts. As a positive control, a known universal twelve-vertex graph passes every incremental pruning test and the game check of the primary enumeration. Hence equality is impossible at these orders, which lowers the integer upper bound by one.
The seven-vertex example also gives the first noncomplete universally winning graph. At orders at most three, the previously established zero maximum excludes any missing guaranteed pair. At orders four through six, the density bound for a noncomplete universal graph would require and hence , contradicting the exact maxima .
Proposition (complete seven-vertex joint table). Every arrow budget at order seven is determined:
| 0 | 0 | 15 | 11 | 30 | 8 |
| 1 | 0 | 16 | 12 | 31 | 7 |
| 2 | 0 | 17 | 12 | 32 | 6 |
| 3 | 0 | 18 | 14 | 33 | 5 |
| 4 | 1 | 19 | 15 | 34 | 4 |
| 5 | 1 | 20 | 18 | 35 | 2 |
| 6 | 2 | 21 | 21 | 36 | 0 |
| 7 | 2 | 22 | 14 | 37 | 0 |
| 8 | 4 | 23 | 12 | 38 | 0 |
| 9 | 5 | 24 | 12 | 39 | 0 |
| 10 | 6 | 25 | 11 | 40 | 0 |
| 11 | 8 | 26 | 10 | 41 | 0 |
| 12 | 9 | 27 | 10 | 42 | 0 |
| 13 | 10 | 28 | 9 | ||
| 14 | 10 | 29 | 8 |
Proof. The previously established small-arrow bounds and witnesses give budgets zero through eleven. The universal 21-arrow graph gives the central value 21, and the dense results give budgets 33 through 42. The twenty other budgets are certified by complete independent descending-degree, suffix-cell enumeration, using the normalization already proved above and an explicit alternating-state game solver.
For completeness, the additional sparse pruning bound is as follows. If rows and columns contain winning indirect pairs, they include at least diagonal coincidences and at least direct arrows between them. These exclusions are disjoint, giving Partial assignments overestimate the possible live rows using the permanent source-camping obstructions. For each potential live column, the cost of reaching indegree two is . The remaining arrow budget bounds how many of the cheapest columns can become live. Maximizing the displayed inequality over both dimensions below these caps is therefore a valid upper bound. Fixed source and column capacity sums give further necessary bounds. Every surviving complete graph is checked by the explicit game attractor with receipt priority and waiting.
The independent runs cover every degree profile at every one of the twenty budgets, visiting 193,302,277 nodes. None reaches one above the displayed value. They reproduce all eighteen completed primary exclusions and also finish the two cases ; in particular, the sharp values there are 14 and 12. Literal attaining graphs have complete winning and losing rank certificates independently replayed by src/small_case_certificate_review.py. The upper receipts and ordinary audit are research/small-case-n7-independent.json and research/small-case-n7-independent-review.md; the consolidated records are in research/small-case-results.json.
Proposition (further fixed-host values). In particular, ; no unrestricted equality at budget thirteen is asserted.
Proof. The seven-vertex 12-arrow witness embeds by isolates at orders eight and nine. At order eight and budget thirteen, the graph with rows has eleven guarantees. Its 1,024 alternating-state rank obligations are checked directly. Complete fixed-host exclusions of scores 10, 10, and 12 at , , and cover respectively 55, 61, and 52 degree profiles. They use the descending-degree, suffix-cell method and the two-dimensional incidence bound proved above. The source differs from the independently audited seven-vertex implementation only in comments, array capacity, and the host-order guard. The ordinary coverage review and literal rank replay are recorded by src/small_case_tiny_review.py in research/small-case-tiny-review.json. This is independent source review, not a second complete negative enumeration at these host orders.
For there are seventeen missing arrows. To exceed fourteen guarantees, at most two missing pairs could fail. A zero missing row makes every indirect pair fail. If missing rows have degree one, their degree-one loss bound forces . When , the two functional rows must form a two-cycle; the other rows avoid that cycle and would give a universal six-vertex core with fifteen missing pairs, contradicting . When , its unique image row already accounts for two failures. The remaining rows avoid its forced bad targets. Restriction gives either an impossible universal five-vertex core or a four-vertex core with one safe root. The latter has one of the four degree profiles , , , or , all excluded by the reviewed rooted certificates. The root is useful only if the current cop cannot capture there; root arrival is not declared unconditional success.
With no degree-one row, the missing degrees are . Normalize the degree-three source and its neighbors, then enumerate every remaining missing row. A union of permanent source and recipient camping losses rejects only prefixes with at least three forced failures. The complete search has 46,344 prefixes and 3,168 surviving leaves. An independent orbit reconstruction covers every leaf using 22 fixed representatives; all 22,528 negative-state rank obligations are checked. Their largest score is thirteen, while discarded graphs have score at most fourteen. Thus the upper bound is fourteen, met by the separately rank-verified literal graph in research/small-case-results.json. The complete degree reduction, corrected root semantics, source audit, and full leaf-orbit review are in research/small-sparse-eight39-review.md/json, checked by src/small_sparse_eight39_review.py. This review does not claim a second traversal of the full search tree or a Lean proof of its enumeration.
Proposition (complete finite intervals). The missing-pair upper bound is attained at every budget in each of the following intervals:
Proof. Saved staged envelopes cover at order eight, at order nine, at order ten, and at order eleven. At each stage the messenger uses only arrows of a fixed base graph , while the rank obligations permit every cop move in the larger envelope . Hence the same decreasing ranks prove delivery for every graph , including every optional subset and every intermediate arrow budget. The ranks depend on both positions and are checked at every recipient and initial cop position. The order-nine stages obtained from the two ends overlap; no inference from winning endpoints is used. The previously certified dense endpoints supply , , and . All resulting counts equal the missing-pair upper bound. The consolidated literal recipes and certificates are indexed in research/small-case-results.json; src/small_case_stage_review.py independently replays the interval obligations.
Verification boundary. These are finite computer-assisted proofs, with ordinary completeness and pruning arguments; they are not presently Lean formalizations. The seven-vertex vertex-maximum exclusion needs no game solver after the static camping reduction; its complete joint table also uses explicit game evaluation. The lower witnesses have saved rank certificates checked directly. Every remaining degree-two graph and every eight-vertex static survivor is evaluated by the exact game algorithms in the independent exhaustive runs; full per-graph ranks for those negative enumerations are not stored. The vertex maxima at orders nine and ten remain open. The eleven-vertex maximum is exact, but this does not determine every joint budget below 25. Absence of a two-regular universal graph alone does not determine the vertex maximum.
Primary sources are src/small_exceptional_n7_exact.cpp and src/small_exceptional_regular.cpp; independent sources are src/small_exceptional_n7_independent.cpp and src/small_exceptional_independent.cpp. The eight-vertex sources are src/small_exceptional_canonical.cpp and src/small_exceptional_canonical_independent.cpp; the independent ordinary audit is research/small-eight-canonical-independent-audit.md. The reproduction receipt is research/small-exceptional-verification.json and the research record is research/small-exceptional-progress.md.
Stronger support bounds and the last small even endpoint
The shared deletion and positive-support argument also preserves the stronger support results. Complete finite regular-core exclusions then supply the remaining twenty-two-arrow case. The exact smaller budgets are proved in the finite sparse-budget section before they are used here.
Two stronger support consequences
Proposition (strict improvement of the even support cutoff). For , a graph with arrows either has a two-in/two-out-regular nonisolated support of order , or
Proof. Positive supports are covered by (56.5) and the missing-pair count. For an actual source or sink of other degree one, deletion gives . Other degree at least three gives For degree two, write for the deleted graph. The general cap is . A score above must attain this integer cap, so and the deleted row or column contributes . The even equality statement makes a regular -vertex core plus isolates. A live deleted row needs two nonsink successors; a live deleted column needs two positive-indegree predecessors. Both neighbors must therefore be in that core. The two direct pairs leave at most possible additions, a contradiction.
Proposition (original-graph support reduction). For , a graph with arrows and has exactly nonisolated vertices, whose degrees need not all be two. Consequently
Proof. Positive supports other than are excluded by (56.5) and the missing-pair count. Source/sink degrees one or at least three give the same bounds as above, both below . For other degree two, Theorem 56 at parameter forces to have a regular -vertex core plus isolates. The deleted row or column must be live, since otherwise . Its two neighbors therefore lie in the core, as in the preceding proof. Adjoining the deleted vertex gives exactly nonisolated vertices in the original graph.
At twenty-two arrows, any graph beating74 already fits on eleven vertices. These implications concern the original graph, not a claim that arbitrary arrow deletion or contraction preserves delivery. Their earlier numerical consequences and follow using ; the finite-budget theorem gives the sharper exact values 13 and 19.
Regular cores and their finite exclusions
Lemma (two-row loss). In an -vertex two-in/two-out-regular graph, a source camping obstruction forces at least missing pairs to fail.
Proof. Suppose and . If , the two outgoing pairs are equal, and both rows are zero. Otherwise write . The arrow makes , so row and column are both zero by camping. Their intersection is the direct pair , so their missing pairs are disjoint.
Without source camping, every predecessor-camping cop is outside the recipient’s predecessor set. Otherwise, if and , the row is covered by the closed neighborhood of , a source obstruction. Two cops camping the same recipient would have identical outgoing pairs and likewise create source camping. Thus distinct predecessor-camping pairs have distinct recipients, and two such pairs destroy at least missing pairs.
The complete retained finite exclusions for zero or exactly one such pair give the following bounds. All degrees in this table are two.
| Maximum with no camping | Maximum with exactly one predecessor-camping pair | Bound with at least two pairs | Resulting bound | |
|---|---|---|---|---|
| 9 | 30 | 24 | 44 | 44 |
| 10 | 38 | 45 | 58 | 58 |
| 11 | 66 | 71 | 74 | 74 |
Source camping gives the smaller bound . This proves, in particular, the retained eleven-vertex regular-core upper 74. The exactly-one-pair enumerations evaluate 1,567,20,658,484,471 leaves at the three orders, without time or target termination. The eleven-vertex run covers all 14 derangement cycle types of one permutation factor, with 7,016,903 partial nodes; an independent scalar solver agrees on482 selected leaves, including every successive maximizing witness. The source and coverage review and replay are retained in research/sparse-third-audit.md and research/sparse-third-enumeration.json. They are complete source-reviewed exclusions, not second full graph enumerations or Lean proofs.
A further complete ten-vertex regular enumeration sharpens58 to53. It covers 12 first-factor cycle types,5,652,419 partial nodes and 289,163 actual-game evaluations. The retained literal attains53. The factorization, coverage and threshold-dependent camping review is research/small-plateau-regular-family-review.md. The separate incoming and outgoing single-transfer families on ten vertices also have upper 53, with complete receipts research/small-sparse-transfer-in10-threshold53.json and research/small-sparse-transfer-out10-threshold53.json. These three family results are premises of the finite twenty-arrow proof, independent of its conclusion.
For reference, the more restrictive eligible-camping-free directional transfer families retain their sharper finite maxima:
| Order | One outgoing degree1 and one outgoing degree3 | One incoming degree1 and one incoming degree3 |
|---|---|---|
| 9 | 13 | 29 |
| 10 | 32 | 50 |
All other corresponding degrees, and every degree in the opposite direction, are two. Hall’s condition follows directly from these degree patterns: source sets emit at least arrows against recipient capacity two, or at least against capacity at most . A perfect matching can therefore be normalized by cycle type; the high-degree vertex uses one representative of each distinct cycle length and the low-degree vertex is unrestricted. Incoming and outgoing families are evaluated separately. The complete scopes and audits remain in the sparse-third-transfer-* evidence. None of the directional statements assumes graph-reversal invariance.
Exact attainment at twenty-two arrows
Theorem (the twenty-two-arrow maximum). For every ,
Proof. The preceding exact budgets give . Positive support at least twelve has bound 74 from (56.4); support at most ten has at most 68 missing pairs. At support eleven, a coordinate below eleven gives with all smaller coordinates bounded as in the arithmetic lemma. If , every degree is two and the retained regular-core upper 74 applies. This proves the global upper 79 without either stronger support proposition being a premise.
For attainment, take vertices with outgoing pairs Every outdegree is two; vertex 0 has indegree three, vertex 3 indegree one, and all other indegrees two. The saved full certificate verifies 79 guaranteed indirect pairs. Both independent solvers agree, and the literal verifier checks every winning and losing condition at all 2,662 alternating states across the eleven recipients. The adjacency and ranks are in research/sparse-third-one-transfer-in-certificate.json. Adding isolates supplies every larger host.
The lower bound uses this literal graph, not completeness of its discovery search. The upper uses the ordinary kernel and the retained regular-core exclusions. No new concrete Lean certificate is claimed.
Additional outside-vertex bounds
Lemma (outside-vertex refinement). Put Let be the nonisolated vertices outside , and write Then , , and . The nonisolated support is . If count the source rows and recipient columns containing at least one guaranteed indirect pair, then Moreover, and
Proof. Every vertex of has indegree and outdegree at most one, with positive sum, proving the elementary constraints and support count. Let . Exactly arrows end outside , of which exactly end in . Thus exactly vertices of have indegree zero; they emit at least twice that many arrows. The indegree-zero vertices in each emit one further arrow. At most of these arrows end outside , and recipients of indegree at least three receive at most arrows in total. Consequently at least selected arrows enter indegree-two recipients. Dividing by their capacity two gives that many distinct zero columns after taking the ceiling. Such a recipient has an inaccessible predecessor; a cop waits at its other predecessor. The cop-source exception is a direct pair and is not counted. Rearranging, using the common parity of , gives the displayed column bound.
For the row bound, use sinks in the original directions. If , exactly members of are sinks, and further sinks in each receive one arrow. At most of these incoming arrows can avoid outdegree-two predecessors. Thus at least arrows come from degree-two sources with a sink successor. Each such source has a zero indirect row, since the cop waits at its other successor. Dividing by two and rearranging proves the row bound; no reversal invariance of the game is used.
Total outdegree outside is at most , and total indegree outside is at most . Subtracting both from bounds the arrows in from below. Its diagonal pairs are disjoint from these arrows, giving the first pair bound. The live row and column sets intersect in at least vertices. Their total outgoing and incoming degrees are at least and , forcing at least direct pairs in their rectangle. Removing these arrows and diagonals gives the second bound.
Dropping the outside-vertex subtractions also gives the simpler bounds The full integer constraints imply that a 20-arrow graph with has at most 13 nonisolated vertices, and an 18-arrow graph with has at most 15. The independent replay retains respectively 22 and 67 triples , not that many graphs or degree sequences. Its source and complete arithmetic receipt are research/small-case-support-review-2026-09-13.py and the adjacent JSON. These support bounds do not assert that deleting exceptional vertices preserves a strategy.
Consequences for the earlier small-budget comparisons
The exact finite-budget theorem gives and . It therefore preserves the earlier intermediate conclusions , , and without their former separate optimization arguments. The regular and directional family exclusions used in the final proof were stated independently above.
Proposition (comparison host for twenty arrows). For every , Every twenty-arrow graph has an explicit eleven-vertex twenty-arrow comparison graph with at least as many guarantees.
Proof. Pad the retained ten-vertex score 53 literal with one isolate. The finite-budget theorem bounds every original graph by 53. Further isolate padding proves the assertion for every larger host.
The historical stronger task of modifying a hypothetical larger-support improvement remains documented in research/small-sparse-twenty-host-compression.md and its independent review. It is no longer a dependency of the exact classification. Its frozen evidence and the earlier intermediate exclusions are preserved unchanged.
The exact 23-arc endpoint
The shared deletion and positive-support bounds reduce the twenty-three-arrow endpoint to the same three finite families as the odd support theorem.
Theorem 53 (with finite exhaustive checks). Moreover, for every .
Proof. The retained twelve-vertex literal has 83 guaranteed indirect pairs. For the upper bound, the preceding exact budgets give Thus a graph with has positive indegree and outdegree after isolates are removed. Support at most ten has at most 67 missing pairs; support at least thirteen has at most 76 by (56.4). The retained eleven-vertex value excludes that order.
At support twelve, , and a coordinate at most ten gives Consequently . Degree sums force one degree-one vertex in each direction and every other corresponding degree two. The two exceptional vertices are either distinct, with their connecting arrow absent or present, or coincide. Their eligible missing-pair counts are respectively 90,89,89. This proves the full finite domain directly; neither Theorem 57 nor a historical eleven-vertex upper 81 is required for this endpoint.
We exhaust these families using their two-permutation descriptions. For the first, add the missing exceptional arc ; for the second add another copy of the existing arc; for the third add a dummy loop at the common exceptional vertex. The resulting bipartite incidence multigraph is two-regular and decomposes into two perfect matchings. This follows directly by alternating the edges of each even cycle, including a doubled-edge cycle. Regard the matchings as permutations , placing the added arc in .
Label the exceptional source 0 and, when distinct, the exceptional recipient 1. Up to relabeling, enumerate the cycle of containing the added arc and the unordered cycle lengths of its remaining vertices. In the common-exception case, fixes 0. Every other cycle has length at least two. Then enumerate every admissible permutation , allowing only the prescribed doubled exceptional arc in the second family, and delete the added arc before any game calculation. This covers every graph in the three families.
Partial assignments may be discarded when a stationary pursuer covers the completed outgoing neighbors of a contributing source, or the completed predecessors of a contributing recipient. A source obstruction destroys at least eight eligible pairs. A recipient obstruction destroys at least seven, after omitting a possible source coinciding with the pursuer. Since there are at most 90 eligible pairs, all discarded graphs satisfy . Testing coverage with a partially assigned pursuer neighborhood is also safe: that neighborhood can only grow.
Every completed graph surviving these obstructions is evaluated by the exact least reachability fixed point. Evaluation may stop at a leaf once its remaining possible score falls below 84. The three finished enumerations give the following counts; none has .
| Exceptional configuration | Permutation cases | Partial nodes | Completed graphs surviving camping |
|---|---|---|---|
| Distinct, arc absent | 42 | 164,276,910 | 16,902,091 |
| Distinct, arc present | 42 | 13,448,216 | 1,125,588 |
| Common vertex | 14 | 49,814,092 | 3,558,672 |
This excludes every proposed counterexample and proves . The verified witness gives equality. Adding isolates preserves its guaranteed indirect pairs, proving the fixed-order assertion for every .
Reproducibility and proof boundary. The new source src/odd_endpoint_near23_threshold.cpp is a separately saved, parameterized copy of the earlier enumerator; it accepts cutoffs at least 84. The coverage, game calculation, and pruning are unchanged. The complete receipts are research/odd-endpoint-threshold84-absent.json, research/odd-endpoint-threshold84-present.json, and research/odd-endpoint-threshold84-same.json. Their cutoff, completion flags, exact counts, source hash, and dependencies are consolidated in research/odd-endpoint-threshold84-summary.json. The unchanged dependency on the eleven-vertex enumeration is audited in research/odd-endpoint-eleven-enumeration-audit.md. The source/sink and positive-support argument above supplies the current all-host reduction. Its arithmetic is checked separately by src/sparse_upper_kernel_check.py. The earlier specialized 23-arc reduction and the unchanged cutoff-84 pruning are recorded in research/odd-endpoint-threshold84-ordinary-audit.md. A separate software audit of the coverage, pruning, and evaluation is research/odd-endpoint-threshold84-independent-audit.md. It also compares 37 leaf-game and early-exit cases across all three families with an explicit alternating-state solver, including full rank and losing-closure checks; the receipt is research/odd-endpoint-threshold84-independent-tests.json. The lower-bound certificate is research/odd-endpoint-m23-lower-certificate.json.gz, checked by two independently implemented game solvers and every saved rank obligation. The exhaustive upper-bound computation is reviewed at the source and mathematical level; it is not a separately implemented second enumeration or a Lean proof.
Verification and scope boundary
Exact computation and formal verification
For a fixed recipient , let be the set of initial pursuer positions from which delivery can be forced in at most messenger moves. Start with and otherwise. Set and update The recurrence includes waits and excludes all nonterminal collisions. Its least fixed point enforces eventual delivery. A separate implementation builds the explicit alternating graph of states and computes its reachability attractor. This is standard finite reachability-game machinery (Berwanger 2009), rather than a new general algorithm for graph games.
The certificate checker independently verifies decreasing ranks on the selected messenger moves and on every pursuer response. Outside the winning region it verifies closure under every messenger move and at least one pursuer response. Thus a negative answer comes with an avoidance strategy, not simply failure of a search. Standard adjacency-list attractor analysis gives an all-recipient time bound ; that bound describes the standard implementation, not a claimed running-time bound for the simpler synchronous reference solver.
Certified finite extrema
Complete enumeration gives
| 1 | 2 | 3 | 4 | 5 | 6 | |
|---|---|---|---|---|---|---|
| 0 | 0 | 0 | 2 | 4 | 7 |
For every labeled digraph was enumerated. For , sorting the vertex labels by degree reduces the search while retaining at least one representative of every isomorphism class; valid degree bounds prune only candidates unable to improve the current maximum. This certifies extrema, not labeled distributions. Every attaining graph is independently checked by the explicit alternating solver. The complete joint tables, enumeration code, and receipts accompany the paper.
The complete finite sparse endpoint bridge covers every order , joining the uniform family from order 85 in Theorem 40. The sharper projection in Theorem 45 and Corollary 45.1 starts the odd family at support order 98, so its required finite bridge is . The full earlier archive through order 144 remains available unchanged. The graph lists, local ranks, projection proof and direct verification receipts are cited with those results. Theorem 46 supplies the original small-order bounds; the completed finite classification gives .
One clean 12-vertex example is a Cayley digraph of , with right multiplication by two suitable 3-cycles. Its actual graph and all-recipient finite-rank certificate are included. The Lean theorem checks the explicit 12-vertex graph directly, so correctness does not depend on trusting the group-label interpretation or the search that discovered it.
Lean coverage
The formal artifact has 21 modules using Lean 4.33.1 and its standard library. The game permits both players to wait and gives receipt priority over collision. SemanticCompleteness.lean proves that finite winning trees are equivalent to one fixed legal messenger policy succeeding against every permitted initial pursuer and every legal history-dependent pursuer policy. Eventual success is defined without an a priori move bound; the converse derives a finite bound. Thus the formal score agrees with the actual finite game’s guarantees.
The development defines that score and an exact-maximum specification, proves the missing-pair bound and the unrestricted vertex bound for , and derives the dense zero band when directly from the graph and game. The checked 12-vertex, 24-arrow attainer and vertex bound prove . A second literal graph has 11 vertices, 88 arrows and 22 guaranteed indirect pairs, all delivered within two moves. Six literal base/envelope pairs at orders sixteen through twenty-one have kernel-checked arrow counts and two-move witnesses for every intermediate graph.
ExactScoreCertificates.lean combines partial winning ranks with closed losing regions: each accepted missing pair covers every legal initial pursuer, and each rejected pair has a checked losing start. Its literal four-vertex, six-arrow example has six missing pairs, exactly two guaranteed. This proves that graph’s exact score, not its extremality. A separate finite-cover interface checks a complete pilot covering all 64 loopless three-vertex graphs; the larger enumeration completeness arguments remain external proofs.
The strategy modules prove safe branching, camping obstructions, protected witness preservation under exterior-arrow changes, robust two-move envelopes, source-rank and position-dependent staged envelopes, and safe guide entry followed by a supplied interface strategy. Concrete guide codes, local ring arenas and projections, and the full numerical overlap remain external premises. Dense-counting results prove staircase arithmetic from explicit cardinality hypotheses and complementary-block two-move delivery; the staircase graph-to-counting bridge and existence of its attaining blocks remain ordinary arguments.
The remaining sparse bounds, dense staircase, arithmetic existence lemmas, infinite construction parameters, probabilistic existence results and large finite exclusions are not fully formalized. The coverage map lists exact theorem names and source hashes. The complete classification remains an ordinary and computer-assisted theorem with partial Lean coverage.
Further consequences and open problems
The random statement in Theorem 54, specialized to the full vertex set, implies that for every fixed density the random loopless digraph guarantees all pairs with probability tending to one. Its failure probability is at most Consequently Indeed, the loss from the missing-pair count is at most times the indicator of failure; the probability decays exponentially. This expectation conclusion is separate from the theorem’s exact-budget conditioning and deterministic construction.
The exact-count and explicit-construction objective is complete. Corollary 47, the finite sparse-budget theorem, and the complete small-host tables cover every admissible pair. Maximizing that joint answer gives and ; those projections are consequences rather than substitutes for the joint table.
Further simplification of the finite constructions and proofs remains possible. It is not an unresolved value or missing attaining graph. Classification of all extremizing graph shapes, a structural characterization of all guaranteed pairs, and exact optimization of delivery time lie outside this paper’s boundary. The existing timing results and remaining timing questions are preserved in the delivery-time companion. The ordinary and finite proofs establish the classification. The accompanying formal development has the more limited coverage specified above.
A finite construction at one circumference does not prove a uniform family. Here the finite bridge is complete on a bounded range and the retained ordinary constructions supply the infinite tail. A repeatable marked vertex-extension rule remains a possible simplification, not an unproved premise of the main-interval theorem.
A correct future proof must retain enough information about both players. Simple distance-to-recipient potentials fail: some states at a fixed small distance from the recipient require detours whose length grows with the graph. Nor does safe indefinite motion imply delivery. The finite witnesses and failed conjectures are preserved to make those distinctions reproducible.
Appendix: provenance and retained formulations
Correcting the original layered construction
The original graph remains a useful construction, but its printed count is not correct. We give its exact count and separate safe intermediate movement from terminal delivery.
Let , , and choose a family containing one of each complementary pair of -subsets of , with every coordinate occurring in exactly members. Such a family exists precisely when positive is not a power of two; a proof follows below.
There are row vertices for , and coordinate vertices for . The only arcs are
- when ;
- when , and when ;
- when ;
- when , and when .
The order is . The four directed layers are , , , .
Theorem 16. For the balanced original family, At , the 44-vertex graph has exactly 764 indirect guaranteed pairs, rather than the draft’s claimed lower bound of 1252.
Proof. The rows form an antichain. The literal columns, indicating membership or nonmembership of each coordinate, also form an antichain, with size . They cannot coincide: equality on the selected rows would remain true on their complements and hence on every -subset, which is impossible for distinct literals. Every vertex has at least two successors.
From any noncollision state the messenger can safely advance one layer. If both players are in the same layer, use incomparable outgoing neighborhoods to choose a successor inaccessible to the pursuer. If the pursuer is in the next layer, avoid its occupied vertex; it has no within-layer arc. In the other two cases it cannot reach the next layer in one move. This includes waiting responses.
From to a specified there is a two-move guarantee. Against a pursuer , choose a coordinate in , then choose its primed or unprimed intermediate according to membership in . Against a pursuer in the intermediate layer, choose another coordinate of ; the other layers cannot interfere. The reverse direction is identical. Safely advancing to the appropriate row layer first therefore gives delivery to any row recipient in at most five moves. There are such recipients, each with indirect sources.
For target or , its predecessor set is exactly . Lemma 2 excludes every indirect source except . That exceptional source wins in two moves: literal-column incomparability handles a pursuer in its own layer, and the other layer cases are as above. Thus and both count. Symmetrically and count, and no other indirect sources do. These give exactly further pairs.
The correction preserves the original leading estimate along its constructed orders. The new circulant family supplies the stronger linear-deficit result at every sufficiently large order. The original construction’s regular incidence design and the later extremal construction are distinct contributions.
Balanced complementary halves
Lemma 17. For positive , the -subsets of can be partitioned into two coordinate-balanced families with complementary subsets in opposite families if and only if is not a power of two.
Proof. Put . Each coordinate occurs in subsets, so balance requires . The factorial valuation formula gives where is the number of ones in the binary expansion. Thus divisibility by four is equivalent to not being a power of two.
For sufficiency, distinguish coordinate and cyclically rotate the other coordinates. Subsets containing correspond to binary circular words with ones and zeros. Every orbit has length : a proper repetition would have a repetition count dividing both consecutive integers. The number of orbits is even, since is odd and .
Choose half of those orbits. In the first family put their subsets, and put the complements of the subsets in the unchosen orbits. Exactly one of each complementary pair is selected. The distinguished coordinate occurs times. Rotation invariance gives a common incidence count for every other coordinate; counting all incidences yields so . The other family is balanced as well.
This proof replaces the draft’s incorrect stronger divisibility assertion , which already fails at .
Construction appendix: choosing the circulant parameter
Proof of Lemma 12. If , choose ; any common divisor with divides two and is odd. If , choose ; the same argument uses four. If , use .
It remains to handle . Write with odd and . If , take : it divides and is at most . If and , use .
If and , take . The number is not divisible by seven, since powers of two modulo seven are . The case and is impossible. Finally, if and , then is even. Use . Divisibility of by eleven would imply , whereas even powers have residues .
All choices are odd and smaller than . Their smallest possible lower estimate is , valid for .
The sparse interval as a consequence of the stronger envelope
Theorem 41. For every integer and every , an explicit universally winning graph exists, with delivery within messenger moves and arbitrary subsets of its prescribed optional arrows.
Proof. Theorem 52 gives the stronger assertion from , through a larger exact budget endpoint, with the better time bound .
The earlier construction separated deletions by seventeen columns and forbade optional arrows within sixteen columns of a deletion. Its separate finite strategy certificates remain available. The new theorem replaces that numerical result and its overlap role; the old proof is retained in research/sparse-budget-earlier-proof.md for reproducibility.
Corollary 42. There is an absolute such that for every and ,
Proof. Theorem 44 now permits the explicit choice , with combinatorial attaining constructions throughout.
A robust dense bridge
Theorem 50. For every and every integer , there is a deterministic -vertex graph with exactly missing arcs in which every pair is guaranteed within two messenger moves. Consequently
At each allowed order, one compulsory set of missing arcs and a list of optional missing arcs suffice: every subset of the optional list preserves two-move delivery. The construction takes polynomial time.
Proof. This is the robust envelope in Theorem 58. Its parameterized modular families and four odd repairs cover every order from 22; six further explicit optional lists cover . The ordinary danger-set arguments and the finite witnesses retain a compulsory safe intermediary against every pursuer, so any optional subset is permitted. Selecting optional arcs gives the exact prescribed count.
Theorem 58 further enlarges this same robust dense interval to at every , where is its explicit cap and from the parity construction. The statement here is its uniform initial interval, with its earlier label retained for references. Theorem 58 gives the common constructions and proofs. The earlier projective-incidence decomposition is no longer a separate premise or a separate numerical result. The generic high-girth criterion of Lemma 18 remains available for other graphs.
The full-vertex specialization
Proposition 51. Put and , where . If there is a deterministic algorithm, polynomial in , constructing an -vertex graph with exactly arcs in which every pair is guaranteed within two messenger moves.
Proof. Take , , and in Theorem 54. The condition forces . That theorem proves the stronger statement with a specified routing set, exact incident budget, arbitrary exterior arrows, and a random-sampling probability bound.
The former full-vertex conditioning argument and its overlap are retained in the research history. The counting proof now appears once in Theorem 54, and Theorem 44 gives the improved overlap.
Provenance and assistance
Alexandra Ignatova formulated the original problem and developed the layered construction in her 2023 project under Angel Raychev’s mentorship, recorded in the retained February 2024 manuscript. Their earlier work includes the upper bound and the investigation of two-in/two-out-regular graphs. These results and this research direction are not claimed as new in the present paper.
The September 2026 development, directed by Angel Raychev, repairs the balancing and strategy arguments, corrects the original layered count, and establishes the additional extremal bounds, attaining constructions, finite computational proofs and formal results reported here. Astra 6, operating through the Codex harness, made substantial contributions to mathematical exploration and deductions, counterexample searches, proof writing, programming, independent implementation and proof checks, and Lean development. This assistance extended beyond language editing. The paper distinguishes ordinary proofs, externally checked computational proofs, and kernel-checked Lean results. The named human authors are responsible for the submitted account; tool-assisted checks do not constitute external peer review.