Guaranteed delivery: Lean verification
Exact-count overview · Classification proofs · Paper and evidence · Delivery-time companion
The artifact uses Lean 4.33.1 with Std only. All 21 modules passed their recorded build. The receipt identifies the toolchain, source hashes, compiler output, and logical axioms.
| Module | What it proves |
|---|---|
| DeliveryGame | The alternating game with waiting and terminal receipt; finite winning certificates imply actual delivery against arbitrary legal history-dependent pursuer choices. See the game definition and certificate argument. |
| FiniteGame | Partial winning regions with decreasing ranks imply actual delivery. Closed losing regions exclude finite winning strategies. Guaranteed requires a finite winning strategy for every permitted initial pursuer position. |
| SemanticCompleteness | On finite graphs, guaranteed finite winning trees are equivalent to one fixed legal messenger policy delivering against every permitted initial pursuer and every legal history-dependent pursuer policy. Eventual delivery assumes no prior move bound; the proof derives a common finite bound and constructs a losing-region cop when no winning tree exists. |
| Extremal | A general score counts guaranteed missing pairs. IsMaximum requires both an unrestricted upper bound and an attaining graph with the prescribed arrow count; the score is bounded by the number of missing pairs. |
| SafeBranching | Two safe successors yield a winning source under the stated neighborhood-overlap condition, including the intervening pursuer turn. Ordinary proof. |
| CampingObstruction | Predecessor domination prevents indirect guarantees; consequences for undirected graphs and unique predecessors. Ordinary proof. |
| VertexBound | The unrestricted vertex bound: every loopless graph has score at most n(n − 3) for n ≥ 3, and zero below three. The proof derives two distinct outgoing neighbors for every contributing source and counts its excluded pairs. |
| DenseZero | The dense zero band: every loopless graph with more than n(n − 2) arrows has score zero. A guaranteed indirect pair forces a missing nonloop arrow in every row; the module proves the resulting arrow and missing-pair counts directly. It proves M(n,m) = 0 throughout this admissible range, with an explicit attaining graph formed from the first m nonloop ordered pairs and a proved exact arrow count. |
| TwelveVertexCertificate | An explicit 12-vertex, 24-arc network guarantees every pair and has exactly 108 indirect guaranteed pairs. Construction and certificate context. |
| ExtremalExamples | The exact maximum IsMaximum 12 24 108, combining the general vertex bound with the checked attainer. It also connects the eleven-vertex dense graph to the general score and proves its score is 22. |
| DenseCounting | The staircase arithmetic from explicit cardinality hypotheses, the attaining count identity, and complementary-block two-move delivery in the actual game. See the counting argument and block construction. |
| ProtectedRouting | Changing arrows outside a routing set preserves its safe witnesses and delivery within two moves against every legal history-dependent pursuer. Existence of those witnesses is an explicit hypothesis. Ordinary proof and existence argument. |
| RobustTwoMove | Supplied base/envelope witnesses imply actual two-move delivery for every graph between the base and envelope; direct pairs need no intermediary. |
| RobustLayers | Supplied source ranks that decrease along safe base moves imply actual delivery for every graph between the base and envelope. Safe entry into an already winning routing region adds one messenger move, including the pursuer response. The circle arithmetic and guide-code hypotheses are supplied premises, not proved by this module. Ordinary construction proof. |
| GuideAttachment | The four pursuer cases for safe entry into a hub-and-guide interface, followed by its supplied delivery strategy, work for every optional subset. Concrete neighborhood, antichain and interface hypotheses remain explicit premises; hub lists and arrow counts are not instantiated. Ordinary attachment lemma. |
| StagedEnvelopes | Supplied ranks depending on messenger and pursuer positions certify every graph between a compulsory base and a larger envelope. The strategy delivers against every legal history-dependent pursuer. The concrete finite stages and their computed ranks remain external premises. Ordinary bridge and finite construction evidence. |
| ElevenVertexDense | The explicit 11-vertex dense graph has 88 arrows and 22 guaranteed indirect pairs, with safe witnesses, counts, and actual delivery checked in Lean. Construction and ordinary proof. |
| SmallDenseEnvelopes | All six published base/envelope pairs at orders 16 through 21: row lists, exact arrow counts, safe witnesses, and actual two-move delivery for every intermediate graph. Published envelopes and proof. |
| ExactScoreCertificates | Winning ranks and closed losing regions classify every missing pair and prove the exact score. A literal four-vertex, six-arrow graph has two guaranteed and four losing missing pairs, with all certificate obligations and counts checked by the kernel. Its extremality is not asserted; the generic maximum theorem requires a separately proved upper bound. |
| ExclusionCertificates | A finite-cover upper-bound schema with an explicit completeness premise. Its concrete pilot covers all 64 loopless three-vertex graphs and checks a zero-score obstruction for each. It does not formalize the larger external enumerations. |
| Audit | Reports the logical axioms used by the principal theorems. |
The literal finite-graph certificates are checked by kernel reduction, not by trusting an external solver or native computation. The strategy interpretation accounts for every legal pursuer response and proves termination. The main semantic theorems use Lean's standard propext, Classical.choice, and Quot.sound; the literal arrow and missing-pair counts in TwelveVertexCertificate and ElevenVertexDense use no axioms.
SemanticCompleteness.guaranteed_iff_actual connects the formal score to the actual game: one messenger policy works against every legal initial pursuer and every legal history-dependent pursuer policy. This is an equivalence, including the converse from eventual delivery to finite winning trees.
What remains outside Lean
The exact-count classification and explicit-construction inventory are complete, while Lean coverage remains partial. The construction inventory identifies concrete adjacency rules, specified compositions with parameters determined from (n,m), and certified listed finite graphs for every resource pair. Their construction and optimality proofs are not all formalized.
The graph-to-cardinality argument for the dense staircase, existence of attaining blocks, the general arc-budget bounds, the arithmetic parameter lemma, infinite constructions, probabilistic existence proofs, the original construction's corrected count, and the larger exhaustive enumeration completeness arguments remain outside Lean. The general vertex bound and dense zero band are formalized, and the three-vertex pilot proves its own complete graph coverage. The mixed four-vertex example proves an exact graph score. These results do not formalize the remaining classification.
The shared local simulation and cyclic composition theorem remains an ordinary proof. The five-type and six-type infinite families, the all-order sparse theorem and the odd constructions apply it to independently checked finite local certificates; those concrete arenas and projections are not Lean instances.
The complete main-interval theorem from order 12 remains outside Lean as a concrete classification theorem. Its staged finite bridge has independently replayed state certificates, while the six-offset periodic circles, reduced twelve-hub interface and retained infinite constructions have ordinary proofs. StagedEnvelopes formalizes the implication from supplied position-dependent ranks; RobustLayers and GuideAttachment prove safe entry and strategy composition from their stated premises. These modules do not instantiate the large finite records, verify the circle parameters and concrete hub codes, or prove the complete numerical overlap.
The complete joint tables through eleven vertices, the finite sparse-budget completion, the small staged intervals, the source/sink and degree-profile reductions, and the complete final band with sharp staircase threshold eleven remain outside Lean as concrete theorems. Their proofs combine ordinary arguments, complete finite exclusions, independent game checks and full winning/losing ranks. The approved research/small-case-results.json registry records their separate dependencies. An independent game replay using reviewed enumeration code is distinguished from a separately implemented graph enumeration; neither is presented as a Lean proof of the classification.
The finite cyclic envelope supplement, the two restored optional arrows at order 109, the 22-arrow extremizer, root-colored cycles and arbitrary-duration block addition retain their existing ordinary and external finite proof boundaries. Four moves suffice for the full dense band from order eleven; the smaller graph at nine stations and 55 arrows has a separate five-move certificate. The uniform two-move corollary from order sixteen also remains an ordinary proof. DenseCounting exposes its cardinality hypotheses; it does not assume the full graph theorem under another name.
Download the Lean archive, install the pinned toolchain, and run python3 check.py. The coverage and replay guide explains the exact theorem statements and trust boundary. The separate computational evidence guide identifies the external checks used by the ordinary proofs.