Guaranteed delivery: Lean verification

At the 25 October 2026, 10:22 UTC development checkpoint, Lean also proves $M(7,15)=11$ for every loopless seven-vertex graph with fifteen arrows. All 266 numerical positive-degree families, the complete catalogue, the actual source/sink reduction and an exact score-eleven graph are joined in a 9,060-module accepted closure. The final theorem has no numerical or normalization premise. An independent audit rechecked the complete source, object, compiler, dependency and provenance fingerprints.

At the 25 October 2026, 08:04 UTC development checkpoint, Lean proves the unrestricted maximum $M(7,14)=10$. The upper bound includes every loopless seven-vertex graph with fourteen arrows, including sources, sinks and isolates. It combines 154 positive and 417 zero-side degree families, complete coverage of the 571 hard joint degree profiles, and actual-graph normalization. A verified graph with exact score ten attains the bound.

At the 25 October 2026, 06:40 UTC development checkpoint, all 80 hard positive degree families of the fifteen-arrow, eight-vertex component, their complete catalogue membership, and the normalized support-eight assembly are accepted. The normalization assumes every vertex has total degree at least two and is positive in both directions or has total degree two. This proves the stated component upper bound of fifteen; the unrestricted fifteen-arrow theorem remains unfinished. Separately, an independent route to the sharp twenty-arrow bound has prior-free weak bounds of 36, 44 and 53 at budgets 16, 18 and 19, and three of its sixteen target-family exclusions accepted; thirteen remain. Those weaker bounds do not close the sharp earlier budgets.

The statements and outstanding obligations in this section describe that release. The current development's stronger domains and remaining obligations are listed above.

Exact maxima and explicit constructions already verified

1. The uniform sparse construction from support order 85. For every $n\ge k\ge85$, Lean proves $M(n,2k)=k(k-3)$. The literal six-type cyclic graph, its local projection, all 552 strategy objectives in 81 covered patterns, global strategy composition, exact counts, and isolate padding are connected. Supports 12–18, 50, 55, 65, 70, 75 and 80 also follow from the finite main endpoints below. The remaining even bridge is stated explicitly at the end of this page. SixTypeConstruction.
2. Uniform odd sparse maxima from support order 98. For every $n\ge s\ge98$, Lean proves $M(n,2s-1)=(s-1)(s-4)+2$. All 124 local patterns and 847 objectives, actual cyclic geometry, every cop reply, global safe transfer and exact counts are supplied. The same catalogue also covers supports 88, 89, 90, 94, 95 and 96. Six retained graphs cover supports 13–18. All pad to every larger host. Uniform construction, earlier residue cases, and small supports.
3. The complete main interval at every order from 115. For every $n\ge115$ and $2n\le m\le n(n-3)$, Lean proves $M(n,m)=n(n-1)-m$ with explicit attaining graphs. All 101 local patterns and 696 objectives, actual optional cop replies, safe-transfer composition, exact counts and prescribed optional-prefix budgets are supplied. The lower construction also retains its larger envelope endpoint. LowBandConstruction.
4. The upper main interval at every order from 25. Every $3n\le m\le n(n-3)$ attains all missing pairs. Counted circle, hub and separated-code recipes have prescribed parameters and proved overlaps. At orders 19, 20, 21, 22, 23 and 24 the same assembly respectively covers budgets 95–304, 100–340, 126–378, 110–418, 115–460 and 120–504. MainUpperInterval. The separate pair-code family retains two-move delivery for every optional subset.
5. Complete main intervals at every order 12–18. Thirty saved rank envelopes supply order twelve, and 145 further stages cover orders thirteen through eighteen, with a pair-code endpoint. Each stage checks all initial cop positions, waiting, optional cop arrows and exact arrow counts. MainTwelve and MainSmallClassification. Their endpoints also give the even sparse maxima on supports 12–18, padded to every larger host.
6. Ten further complete main intervals and two short intervals. The five-type constructions prove the entire main interval at orders 65, 70, 75, 80, 85, 90, 95, 100, 105 and 110. The short charts cover budgets 100–110 at order 50 and 110–121 at order 55. Each has an exact optional-prefix recipe. Their endpoints give even sparse maxima on all twelve supports and every larger host. The proof transports common-envelope symmetries without assuming that a selected optional graph is symmetric. FiveTypeClassification.
7. The complete dense range for every $n\ge11$. For $n(n-3)\le m\le n(n-1)$, Lean proves the exact maximum and a concrete attaining graph. At $m=n(n-3)$ the value is $2n$; for $r=m-n(n-3)$ with $1\le r\le n$, it is $2n-r-\lceil r/2\rceil-1$; above $n(n-2)$ it is zero. Arbitrary-graph upper bounds, root and core constructions, exact counts and every threshold case are supplied. DenseSharpClassification.
8. The adjacent band for every $n \ge 16$. For $n(n - 4) \le m \le n(n - 3)$, the maximum equals the number of missing pairs, $n(n - 1) - m$. Explicit even and odd formulas and finite repairs cover every order in this domain. Every optional subset works within two moves; taking the first required optional arrows gives the exact budget. Together with the preceding result, this verifies every budget $m \ge n(n - 4)$ when $n \ge 16$. DenseEnvelopeClassification.
9. The functional endpoint at every $n \ge 2$. The exact value at $m = n(n - 2)$ is $\lfloor (n - 2)/2\rfloor$. The proof characterizes all successful missing pairs in complements of fixed-point-free functions and supplies a literal paired-root attainer. FunctionalEndpoint.
10. The zero range at every order. More than $n(n - 2)$ arrows force zero indirect guarantees. The first $m$ nonloop ordered pairs give a counted attainer at every admissible budget in that range. DenseZero.
11. The twenty-four-arrow maximum on every host from twelve. Lean proves $M(n,24) = 108$ for all $n \ge 12$, combining a checked twelve-vertex witness, the general sparse upper bound and exact isolate padding. SparseAttainment.
12. Prescribed five-offset circles. When $n \ge 16$ is divisible by four, every budget $5n \le m \le n(n/2 - 1)$ attains all missing pairs. The parameter is prescribed from $n$; modular escape, coprime orbit coverage, actual delivery and exact optional-prefix counts are proved. A separate guarded family has a closed arithmetic endpoint under its displayed parameter conditions. CircleParameters and CircleGuardedConstruction.
13. Protected circles at every $n \ge 25$. Every budget $3n \le m \le n(\lceil n/7\rceil - 1)$ attains all missing pairs. A proved arithmetic parameter selection and a specified greedy offset procedure supply the graph; Lean proves preservation of protected differences, the envelope size, delivery and exact budget. ProtectedParameters.

Complete small budgets and small host tables

The unrestricted sharp upper bounds at budgets 0–10 are 0, 0, 0, 0, 1, 1, 2, 2, 4, 5 and 6. Matching graphs are proved at every admissible host for 0–3, from host four for 4–6, from five for 7–8, and from six for 9–10. Sources, sinks and isolates are included. Complete degree-profile and row-choice coverage accompanies every finite exclusion. The ten-arrow theorem completes this chain.

Every admissible budget at every order at most five is classified, with explicit attainers. The four-vertex proof covers all loopless adjacency choices. The five-vertex proof combines actual source/sink deletion, a complete positive-degree catalogue and seven retained witnesses. Orders zero to three, order four, and order five.

General bounds and finite exclusions

VertexBound proves $I(G) \le n(n - 3)$ for every loopless graph with $n \ge 3$. SparseParity proves the unrestricted budget bounds $I(G) \le k(k - 3)$ for $2k$ arrows and $I(G) \le k(k - 3) + 2$ for $2k + 1$ arrows, for every $k \ge 5$. Support counting, deletion, strategy preservation and induction are discharged; the small auxiliary induction bounds are not the sharp finite table.

The complete nine-vertex strictness proof establishes $I(G) \le 53$ for every loopless nine-vertex graph. It includes degree rigidity, matching factorization, canonical permutation cycles and all eight complete exclusion trees. This strictness result alone does not prove all nine-vertex maxima. Further checked interfaces support optimistic partial-game pruning and symmetry reductions; additional exclusion families still require complete concrete certificates.

The sharp regular-nine exclusion proves exact maximum $30$ among all loopless nine-vertex graphs with two incoming and two outgoing arrows at each vertex. Factorization, normalization, all eight first-factor cycle types, complete exclusion trees and an explicit attainer are included. This restricted-family maximum does not establish the unrestricted eighteen-arrow value of 33.

Signed winning and losing certificates verify the exact scores 8, 9, 11, 13, 15, 19, 28, 33, 40, 53, 60, 79 and 83 of retained graphs at budgets 11–23, respectively. All their supports have at most twelve vertices; each graph pads to every larger host. These are lower witnesses, and do not by themselves prove an upper bound over all competing graphs. The witness and padding assembly states every support and score. Earlier literal witnesses remain available.

The sharp fourteen-arrow positive-support exclusion proves score at most thirteen whenever the nonisolated support has at least nine vertices and every supported vertex has positive incoming and outgoing degree. Arbitrary isolates are allowed. The nine-vertex proof covers all eleven normalized joint profiles and 160,718 proof-DAG nodes; the ten-vertex proof and larger-support counting complete the stated range. Smaller supports and sources/sinks remain separate obligations for the unrestricted fourteen-arrow maximum.

The actual game and the trust boundary

Both players may wait; the messenger moves first and receipt precedes collision. SemanticCompleteness proves equivalence between finite winning trees and one fixed messenger policy that eventually delivers against every permitted initial cop and every legal history-dependent cop policy. No time bound is assumed in the actual-play definition.

Padding preserves scores exactly when adding isolates or sinks with at most one predecessor, including cops starting at or entering the new sink. LocalArena proves projection and sequential composition for separate messenger/cop state spaces. A safe transfer includes the cop reply before the next stage; only terminal receipt waives collision at the recipient. Concrete geometry and certificate premises remain visible until instantiated.

All finite checks use Lean kernel reduction. No external solver assertion, custom axiom, proof hole or native proof is accepted. Reported axioms are confined to Lean's standard propext, Classical.choice and Quot.sound. Certificate producers are untrusted and unnecessary for replaying the literal distributed sources.

Obligations outstanding at that earlier snapshot

1. Even sparse supports 19–84, excluding 50, 55, 65, 70, 75 and 80. Odd sparse supports 19–97, excluding 88, 89, 90, 94, 95 and 96. Each missing support case represents all larger hosts through padding.
2. Main-interval budgets 38–94 at order 19, 40–99 at 20, 42–125 at 21, 44–109 at 22, 46–114 at 23 and 48–119 at 24; 111–149 at order 50; 122–164 at 55; and $2n\le m<3n$ at all other orders 25–114 except the ten completed orders 65, 70, 75, 80, 85, 90, 95, 100, 105 and 110.
3. Unrestricted sharp upper exclusions for budgets 11–23 and complete joint tables at orders 6–11. The exact dense range at every order from eleven is already verified.
4. One quantified theorem and explicit constructor for every admissible $(n,m)$, with all finite dependencies discharged.

Download the Lean sources, install the pinned toolchain and run python3 check.py inside the extracted lean folder. It rebuilds every distributed module one module at a time, with two Lean workers and rejects source changes during replay. The theorem and replay guide gives precise statements. The research archive contains the dependency-ordered roadmap; the evidence guide separately describes the ordinary and external computational proofs.