Guaranteed delivery: paper and sources

The research archive contains current proof evidence alongside dated research history, including superseded arguments and failed approaches. Start with its current evidence guide to identify the files used by the completed classification. Only the specified complete exclusions and verified certificates are proof premises.

• Research sources and local certificates: the current evidence guide, proofs, Python and C++ programs, check records, and dated research history.
• Full finite strategy certificates: the six larger frozen certificate files for the sparse constructions and finite bridges. These are required for a full replay; extract both archives into the same directory.

Evidence guide: guaranteed indirect delivery

The mathematical classification is complete: every admissible pair (n,m) has an exact value M(n,m) and an explicit attaining adjacency or specified composition with parameters determined from the pair. This guide maps those claims to ordinary proofs, finite evidence and replay tools; it is not a new verification, build or deployment receipt. Start with the manuscript’s paper/joint-classification-resume.md, paper/finite-completion.md and paper/finite-values.md, then the canonical ledger and recipe audit below. Historical notes retain their earlier thresholds and status language.

The companion evidence-index.json gives machine-readable paths, command arguments, scope and historical classifications. Paths below are relative to the extracted research archive root; preserve that directory structure. Extract finite-strategy-certificates.zip into the same root for its six larger finite certificate files, including the even/odd bridge ranks, three six-type families and the six-type budget certificates. The guide is maintained at publication/EVIDENCE_GUIDE.md in the repository and may be placed at the download archive root.

What each kind of evidence establishes

An ordinary proof establishes the construction, coverage, projection and all-order argument stated in the manuscript. A finite certificate supplies explicit ranks, policies or safe intermediaries for its finite obligations. A checker examines those obligations. A receipt records a particular run and its stated scope. A successful bounded test does not replace an infinite proof; a source hash is an identity check, not a proof of correctness.

The Lean development formalizes selected game statements and finite examples. The current21-module receipt includes an exact-maximum specification, the general vertex upper bound, the dense zero range, the exact cell M(12,24)=108, a complete64graph three-vertex exclusion pilot, guide safe-entry composition, and an exact-score checker with a mixed winning/losing four-vertex example. Finite winning trees are now proved equivalent to one fixed messenger policy that succeeds against every legal history-dependent cop, including every initial cop position. The full extremal classification remains outside Lean. Built artifacts and successful deployment are separate from mathematical verification: consult the download release.json and the maintained repository’s publication/deployment receipts for the exact release being inspected. This guide does not certify a build or deployment; those claims require their separate current receipts.

Numerical coverage and explicit constructions

research/CLASSIFICATION_SCOPE.md states the completion condition, and research/CLASSIFICATION_GAPS.md records the final zero-gap boundary. publication/classification-coverage.json records each value and its source, including isolate lifting. Its audit box contains 493,924 admissible cells, all exact, with zero unresolved canonical representatives. Ordinary domain and host-reduction proofs extend this finite audit to all admissible pairs. python3 src/classification_coverage.py --check recomputes and expands the ledger without graph searches.

research/finish-ledger-review.json independently replays the final closure from the frozen 101-gap baseline. It preserves all 492,834 previously exact audit cells and verifies 1,090 newly exact cells; all 101 former representatives are numerically settled. research/endpoint40_finite_value_tables_audit.json separately checks the displayed finite tables and uniform formulas against the whole ledger. These arithmetic audits do not reprove the underlying ordinary theorems or finite exclusions.

research/EXPLICIT_CONSTRUCTIONS.md separately audits the explicit-construction requirement. It records direct family domains, fixed finite parameters and graphs, and the distinct conditional-expectation results. research/explicit-construction-coverage.json matches the complete ledger and has zero recipe gaps. python3 src/audit_explicit_constructions.py --check repeats that source-pinned audit without orientation derandomization or new graph searches. This checks actual recipes and certified finite exceptions; numerical closure alone would not establish the stronger completion claim.

Earlier coverage reviews retain their original hashes and domains. The final numerical and recipe receipts identify the incorporated sources; older receipts are not rewritten as if they had already reviewed the new results. The index lists each intentional historical source-pin exception by exact receipt field, old digest and current digest. Any additional mismatch still fails the publication audit.

The retained 71-guarantee witness in research/classification-fixed-witnesses.json remains valid historical lower evidence. The new eleven-vertex, 22-arrow graph has 79 guarantees and matches a separately proved global upper bound. Its complete strategy certificate is research/sparse-third-one-transfer-in-certificate.json. The regular one-diamond enumeration has now received an explicit coverage/game audit; this does not turn every earlier bounded search into an exhaustive proof. See the small-budget entry below for the exact dependencies.

Main classification: proofs and supporting evidence

The uniform main-interval theorem gives every n>=12, 2n<=m<=n(n-3), with value n(n-1)-m. paper/main-interval-complete.md combines the bounded finite bridge with the retained infinite constructions. src/main_interval_complete.py returns the explicit adjacency; its finite plans and boundary constructions are recorded in research/main-interval-complete-checks.json. The finite completion chapter supplies every smaller exceptional cell and every remaining sparse budget. Together they give the complete joint classification, with no numerical or construction gaps.

Every budget from 22 onward is exact with explicit attainers at every order from eleven. The order-eleven boundary values at budgets 22, 23 and 24 are 79, 78 and 79; its budgets 25 through 88 attain every missing pair. The entire seven-vertex table and every final dense-band cell are complete. The staircase has sharp threshold eleven and attaining graphs within four moves throughout that range; the earlier two-move theorem from order sixteen remains intact. The smaller graph at (9,55) has its separate five-move bound.

Complete finite exceptions and their evidence

The single small_case_completion entry in evidence-index.json links the final proof chapter, finite tables, result registry, approved bounds, reviews and replay commands. research/small-case-results.json separates literal graphs, certified stage intervals, approved upper bounds and host cutoffs. src/classification_small_cases.py reads those fixed inputs to supply adjacency and coverage; it performs no discovery search. Every exact finite value has both an attainer and a matching independently approved upper argument. The detailed files remain inside the existing research download rather than becoming separate public downloads.

• Registry and approvals. src/small_case_results.py consolidates saved graphs and checked stage inputs. src/small_case_bound_registry.py maintains the separately reviewed proof list in research/small-case-approved-bounds.json. These producers write registries; changing a proof dependency requires its own review, not merely a new hash. They are not read-only packaging checks. The small-case registry producer is historical: in a disposable copy restore research/history/before-slimming-odd-endpoint-resume.md to paper/odd-endpoint-resume.md and research/history/before-arxiv-preparation-small-orders-resume.md to paper/small-orders-resume.md before running it. It validates those original approved proof bytes and may write a bundle before rejecting a mismatched source; do not run it on the maintained checkout.
• Literal game and stage certificates. research/small-case-fixed-certificates.json stores adjacency and complete winning/losing ranks. src/small_case_certificate_review.py checks every actual alternating-state obligation without importing a game solver. The two stage catalogues are research/small-plateau-staged-records.json and research/small-plateau-small-stage-records.json, with their respective -certificates.zip bundles. src/small_case_stage_review.py independently checks every allowed intermediate graph through the supplied base/envelope ranks. These ZIPs stay inside the existing research download; no additional public download entry point is needed.
• Complete exclusions and ordinary reductions. The earlier order-seven, rooted, first-step, order-eleven and dense reviews remain in the same entry with their original scopes. The final (8,40) value is 12, supported by two complete endpoint enumerations and full literal replay. The new eight-vertex row, small sparse budgets and remaining nine-/ten-vertex cells have their separately pinned reviews in research/finish-case-approved-bounds.json.
• Sparse budgets and host frontiers. The final sparse global values at budgets 12 through 21 are respectively 9,11,13,15,19,28,33,40,53,60. research/finish_budget_manifest.json, the separate seventeen-, eighteen- and nineteen-arrow reviews, and the twenty-/twenty-one-arrow reviews retain the exact source/sink reductions and complete residual families. Their fixed-host exceptions and attaining hosts are displayed in paper/finite-values.md. Isolates lift the specified attainers to larger hosts.
• Final integration. research/finish-ledger-review.json checks that all new finite inputs close the frozen 101-gap ledger while preserving every old exact value. The independent recipe audit checks the resulting explicit constructions. These two final audits are separate from the individual mathematical reviews.

The final ordinary synthesis is paper/finite-completion.md, retaining the earlier proofs in paper/small-orders-resume.md, paper/sparse-third.md, paper/support-concentration.md and paper/dense-third.md. All rank checks retain receipt before collision and every legal pursuer reply. Some earlier endpoint cases have a second independent graph enumeration. Later reviews retain the source-reviewed enumeration and independently solve every reached leaf; sampled guarded-prune tests are counted separately. Neither an incomplete search nor an omitted family is upper evidence. These are ordinary and external computer-assisted proofs, not new Lean instantiations of the complete tables or full classification.

Five named frozen manifests authorize eight scientific run/replay .log files in the research archive. Their exact paths and hashes are checked by src/audit_publication_artifacts.py; arbitrary compiler, TeX and operational logs remain excluded. The new independent game header is included with all other .hpp, .cpp and .py sources. This packaging policy changes no mathematical receipt. The two evidence archives retain all original paths and file bytes. To keep each download below the hosting limit, larger plain research receipts use ZIP BZIP2 compression, and six intact gzip certificate files are grouped in the finite archive. The named partition and compression policy are recorded in the index and checked against every extracted SHA256. Systems whose ZIP utility lacks BZIP2 support can use Python’s standard library:

python3 -m zipfile -e research-sources.zip extracted-evidence
python3 -m zipfile -e finite-strategy-certificates.zip extracted-evidence

For a literal replay, use an extracted working copy and run python3 src/small_case_certificate_review.py research/small-case-fixed-certificates.json --out research/small-case-independent-review.json. It reads the fixed graphs and writes a fresh receipt. python3 src/small_case_stage_review.py similarly reads the two saved ZIPs and replaces only its stage-review receipt. The JSON index distinguishes these replays from complete finite re-enumeration and registry regeneration. Preparing this guide did not execute those commands or replace any receipt.

Retained main-interval and family evidence

The new ordinary construction proofs are paper/main-interval-six-circle.md and paper/main-interval-reduced-hubs.md. research/main-interval-fifth-ordinary-review.json records independent ordinary-proof review, literal reconstruction, and full-envelope rank checks. The periodic circle recipes and reduced hub interface are ordinary parameterized results; the supplied promoted circles retain their separate finite source-rank certificates.

research/sparse-staged-records.json specifies literal arrow lists and certified budget stages; research/sparse-staged-certificates.zip stores ranks on recipient and both player positions, with policies. The independent checker src/sparse_staged_replay.cpp checks the actual lower base, upper envelope, waits, both collision checks and every cop reply. research/sparse-staged-independent-review.json additionally records its stated independent Python replay and explicit alternating-state comparisons; its recorded snapshot and selected finite scope must not be silently broadened. Constructing a graph with src/sparse_staged.py reads fixed records and does not regenerate ranks or run discovery.

The canonical complete saved-stage replay is python3 src/check_sparse_staged.py. It checks all 638 frozen stages without running discovery or replacing records. research/sparse-staged-release-replay.json records the current full replay. The historical producer src/sparse_staged.py --certify selects cells from the pre-fifth coverage ledger: do not run it against the current ledger, which already marks these cells exact. It could replace the catalogue with an empty one. Graph construction and the read-only replay do not use this producer.

The preceding 43/104 checkpoint remains supported by paper/main-interval-half-density.md, paper/main-interval-layered.md and paper/main-interval-new-overlap.md. Its independent reconstruction checked 145 envelopes, 1,238 recipients and 4,416,069 rank obligations; its arithmetic review checked 63 chains at 43..105 and 42,130 newly exact cells. Those receipts (research/main-interval-new-independent-checks.json and research/main-interval-fourth-review.json) retain their original source pins and scope. The older theorem below likewise retains its original evidence and stronger component properties.

lean/RobustLayers.lean proves the generic source-rank and safe-entry implications. lean/StagedEnvelopes.lean proves the more general position-dependent asymmetric rank implication for every intermediate graph and actual play. The concrete large finite ranks, periodic parameters, hub codes and complete interval overlap are not instantiated in Lean. Compilation of these generic modules does not discharge those premises.

1. Main interval, Theorem 44: every n≥106 and 2n≤m≤n(n−3), with M(n,m)=n(n−1)−m.

   Proof. paper/exact-budget-derandomization.md; full overlap argument in paper/core-code-composition.md.

   Evidence and replay. research/routing-defect-phase2-code-overlap-checks.json, research/routing-defect-phase2-mixed-code-checks.json, and research/main-interval-composed-checks.json; construction checker src/main_interval_composed.py. The finite extension106..114 uses research/main-interval-composed-third-checks.json and src/main_interval_composed_third_check.py --check; the original receipt remains the115+ implementation checkpoint. Depends on the sparse, protected-circle, all-parity antichain and dense proofs. The whole interval is not a two-move claim.

2. Sparse envelope, Theorem 52: n=6k−r≥115, 0≤r≤5; every 2n≤m≤20k−11r, arbitrary optional subsets, time 9k+21.

   Proof. paper/sparse-packed-holes.md; research/dense-phase2-sparse-two-entry-proof.md.

   Evidence and replay. research/dense-phase2-sparse-two-entry-certificates.json.gz and matching -check.json; checker src/dense_phase2_sparse_two_entries.py. Independent collapsed-solver readback: research/composition-budget-phase2-two-entry-root-check.json. All 101 canonical crops/696 objectives are covered; arbitrary gap-three hole sets are not claimed. The separate finite supplement covers47 canonical circumferences below115 and the109repair. Its48 literal asymmetric certificates are consolidated in research/sparse-interface-third-certificates.zip, indexed by research/sparse-interface-third-proof-registry.json; src/sparse-interface-third-independent.py reconstructs adjacency and checks the full ranks independently. This is finite evidence, not an additional infinite projection theorem.

3. Even endpoint, Theorem 40: M_V(k)=M_E(2k)=M(k,2k)=k(k−3) for k≥12; time 9ceil(k/6)+18.

   Proof. paper/sparse-all-orders.md.

   Evidence and replay. research/sparse-finite-bridge-witnesses.json, sparse-finite-bridge-certificates.jsonl.gz, and sparse-finite-bridge-verification.json cover 12..84. sparse-composition-multi-certificates.json.gz and the independent six-type-independent-spacing-3-certificates.json.gz support the uniform family from 85.

4. Odd endpoint, Theorem 45/Corollary 45.1: M_E(2k+1)=k(k−3)+2 for k≥12.

   Proof. paper/odd-endpoint-resume.md.

   Evidence and replay. research/odd-endpoint-small-certificates.json.gz covers support 13..18; odd-endpoint-finite-bridge-certificates.jsonl.gz covers 19..144. Uniform local evidence: odd-endpoint-all-residues-certificates.json.gz, odd-endpoint-uniform-certificates.json.gz, and independently generated six-type-independent-odd* ranks/receipts. The uniform time 34ceil(n/6)+27 applies to support n≥145, not automatically to the smaller bridge. The period-six family’s faster 14q+12 bound remains separate.

5. Retained small even-budget bounds and exact twenty-two-arrow attainment: M_E(14)≤22, M_E(16)≤32, M_E(18)≤44, M_E(20)≤58, and M_E(22)=M(n,22)=79 for every n≥11. The finite completion above sharpens the four smaller global values to 13,19,33,53 respectively. The earlier support theorems, witnesses and upper proofs remain valid with their original scopes.

   Proof. paper/sparse-third.md proves two nested support thresholds for every k≥7: I>k²−5k+8 forces exactly k nonisolated vertices; I>k²−4k+2 forces two incoming and two outgoing arrows at every such vertex. The first threshold uses the repaired outer-diamond/core argument, with the failed shortcut retained in the research log.

   Evidence and replay. research/sparse-third-audit.md, research/sparse-third-source-audit.json, and research/dense-third-independent-sparse-review.md record the ordinary and finite reviews. research/sparse-third-transfer-commands.json gives the complete enumeration commands and hashes. The exact 22-arrow lower bound uses one explicit graph, both game solvers and every one of its 2,662 rank conditions. It does not depend on completeness of the new graph search. The 18- and 20-arrow upper bounds do depend on the reviewed finite degree-family reductions and complete enumerations, with arrow directions treated separately.

   Explicit lower witnesses. research/sparse-third-fixed-lower-certificates.json freezes graphs with counts 30, 50 and 79 at (9,18), (10,20) and (11,22). Isolates supply every larger host order. python3 src/sparse_third_replay.py reads these records, checks all 6,120 literal winning/losing rank conditions and recounts the guarantees without searching or solving fresh games. No new Lean verification is claimed.

6. Exact 23 arcs, Theorem 53: M_E(23)=83 and M(n,23)=83 for n≥12.

   Proof. paper/odd-endpoint-twenty-three-exact.md; reductions in paper/sparse-stability.md and the eleven-core lemma in paper/odd-endpoint-resume.md.

   Evidence and replay. research/odd-endpoint-threshold84-{absent,present,same}.json, their -summary.json, and odd-endpoint-eleven-enumeration-audit.{md,json}. Lower witness: odd-endpoint-m23-lower-certificate.json.gz. The independent leaf-game test checks 37 examples and saved hashes; it does not rerun the exhaustive exclusion.

7. Retained dense constructions and the order-thirteen band theorem: all n≥13 and 1≤r≤n have the exact staircase value at m=n(n−3)+r, with explicit constructions requiring at most four moves. The whole band has a two-move construction at n≥16. Theorem 58 retains its endpoint, robust bridge and H5/H4 envelopes. The new small-case entry above extends the staircase threshold to eleven and completes the smaller dense values; this earlier result retains its own evidence and guarantees.

   Proof. paper/dense-unified-core.md retains the original families. paper/dense-third.md supplies the root-colored cycle and singleton attachments, exact addition across disjoint missing-arrow blocks, the finite nine-core and three first-step attachments, and the exact reduction of the second dense step to a smaller core. The previous uniform proof and ordinary independent audit remain valid.

   Evidence and replay. The previous dense-phase2, odd-envelope and tiny/small receipts remain valid; lean/SmallDenseEnvelopes.lean retains its six 16..21 examples. The new evidence is in research/dense-third-root-cycle-{checks,certificates}.json, dense-third-core-compose-{checks,certificates}.json, dense-third-first-step-{checks,certificates}.json, and dense-third-r2-reduction-checks.json. The nine-core and the three first-step graphs are explicit finite exceptions checked by both game solvers and complete rank replay. The unbounded attachment, block-addition and equality-reduction statements are ordinary proofs. No additional Lean scope is claimed; two-, three- and four-move guarantees are distinguished.

8. Antichain composition, Theorem 59: exact A..A+q(q−1), A=2k(2k−3)+4kq−W, for every outside-arrow subset.

   Proof. paper/core-code-composition.md; research/routing-defect-phase2-code-composition.md.

   Evidence and replay. src/core_code_composition.py, research/core-code-composition-checks.json, and the code-overlap/mixed-code records. The code-size, forbidden-difference and incomparability hypotheses matter. The specialized two-move sparsity consequence is preserved in the separate delivery-time companion; it is not a remaining objective of the classification paper.

9. Support concentration, Theorem 60: eta=m−2sqrt(I), core size in [m/2−3eta,m/2], support≤m/2+4eta, outside arcs≤12eta.

   Proof. paper/support-concentration.md; research/routing-defect-phase2-support.md.

   Evidence and replay. research/routing-defect-phase2-support-checks.json and routing-defect-phase2-support-exhaustive-checks.json: both original solvers on 181 examples plus all 4,165 labelled graphs through order four. These support the ordinary proof; they do not establish that deleting outside arcs preserves I.

Parked delivery-time companion

The separate page and PDF preserve the universal two-move threshold, its proved bounds, and the unfinished fast sparse construction. The main paper still contains the safe-routing machinery and termination bounds needed to prove its attaining constructions. The companion depends on the main classification proofs, not conversely. Its future objective M_{≤T}(n,m) counts guaranteed missing pairs subject to a deadline; it differs from minimizing the worst delivery time among count-maximizing graphs.

1. Universal two-move threshold: q2(n)=Theta(n log n), with the stated lower bound and constructive upper constant 5.3555763082.

   Proof. paper/delivery-time-companion.md, using the protected-routing and antichain constructions in paper/routing-unification.md and paper/core-code-composition.md. This does not settle the exact threshold or all larger budgets.

2. Partial fast result: eight recipient types deliver within 32D+64 on qualifying quotients.

   Proof. research/composition-interface-terminal-checkpoint.md; composition-interface-terminal-independent-audit.md.

   Evidence and replay. research/composition-interface-terminal-checkpoint-certificates.json.gz, production receipt and later composition-interface-terminal-independent-audit.json; checker src/routing_defect_phase2_terminal_audit.py. Requires connected simple four-regular quotients of girth≥133 and inverse-generator directed diameter D. Types 2/7 remain open; no universal logarithmic-time family is claimed.

Shared formal verification

1. Lean: twenty-one modules, Lean 4.33.1 and Std.

   Proof. lean/README.md.

   Evidence and replay. lean/check.py, embedded .lean data, and lean/verification.json. Covers actual game semantics, selected structural implications, the 12-vertex sparse and 11-vertex dense examples, six small robust envelopes, and the generic position-dependent staged-envelope implication. The semantic equivalence, vertex upper bound and dense zero theorem are unconditional. Concrete staged tables and the complete extremal classification are not fully instantiated in Lean.

The JSON index expands abbreviated filenames in these entries into complete path lists.

Saved-certificate replay

Run these commands from the extracted research root. The arguments were checked against the actual script entry points; they were not executed to prepare this guide.

python3 src/dense_phase2_sparse_two_entries.py --check
python3 src/sparse_composition_multi_certificate.py --check
python3 src/sparse_finite_bridge_verify.py --check
python3 src/odd_endpoint_finite_verify.py --check

The last two need the separate finite-strategy archive. The odd checker uses NumPy when available; append --scalar for the same complete check using only the standard library. These four --check commands read saved certificates without replacing them.

The following also check saved data, but write fresh receipts. Use an extracted working copy to preserve the downloaded receipts:

python3 src/routing_defect_phase2_dense_tiny_verify.py
python3 src/routing_defect_phase2_dense_small_verify.py
python3 src/routing_defect_phase2_terminal_audit.py
python3 lean/check.py

Lean also creates compiled .olean files and replaces lean/verification.json. Install Lean 4.33.1 on PATH, or supply the supported --lean /path/to/lean option. The standalone Lean archive is enough for this replay; the finite-certificate generator is unnecessary.

New fixed-construction checks

The small sparse literal replay above is read-only and does not solve fresh games. The following dense --check commands are also read-only, but the first three reconstruct their fixed graphs and recompute the two game solvers before comparing saved bytes:

python3 src/sparse_third_replay.py
python3 src/dense_third_root_cycles.py --check
python3 src/dense_third_core_compose.py --check
python3 src/dense_third_first_step.py --check
python3 src/dense_third_r2_reduction.py --check

The final command reads the already proved five- and six-vertex numerical premises; it does not rerun those exhaustive enumerations. The sparse arithmetic/counting attack python3 src/sparse_third_checks.py writes a fresh arithmetic receipt. The C++ enumeration commands are preserved separately in research/sparse-third-transfer-commands.json; they are not required to verify the explicit 79-guarantee lower witness.

Recalculation and regeneration

python3 src/main_interval_composed.py --check reconstructs selected boundary graphs and checks the finite parameter coverage. It prints a result unless --out is supplied. This is a bounded construction check, not a replay of the full all-order game proof.

Other programs may solve games or regenerate evidence even when their names contain “verify.” In particular, src/odd_endpoint_small_verify.py solves the six fixed graphs at 13..18 and replaces their certificate/receipt; src/core_code_composition.py and the two routing_defect_phase2_support* programs recompute bounded tests and replace receipts. Their precise commands and write targets are in the JSON index.

src/odd_endpoint_threshold84_independent_test.py needs a C++17 compiler named c++. It runs bounded leaf-game tests and checks existing exclusion hashes; it does not repeat the exhaustive search. Earlier odd-bridge generation also assumes binaries at /tmp/odd_endpoint_finite_check and /tmp/odd_endpoint_finite_certify. Their C++ sources are included, but the binaries are not. The saved --check path does not require them.

Historical evidence and changed source pins

Original receipts and hashes are retained. A historical status below does not mean that a theorem is false. The JSON index lists the exact expected historical hash mismatches; any additional mismatch or further source change needs a new classification. All current Lean source hashes remain required, without an exception.

• research/dense-phase2-uniform-independent-audit.json pins the earlier paper/dense-protected-envelope.md used for comparison. It is not a hash check of the current manuscript. The uniform proof and ordinary audit text remain relevant; current statements are in paper/dense-unified-core.md.
• research/routing-defect-phase2-dense-tiny-checks.json pins an earlier producer dependency src/dense_unified_core.py. Its literal witness data remains current evidence. The independent tiny checker validates that data directly, and lean/SmallDenseEnvelopes.lean proves the six 16..21 cases. Preserve the file and its original producer hash.
• research/six-type-packed-holes-independent-review.{md,json} reviews the former n≥1075/time 9ceil(n/6)+26 theorem. Current Theorem 52 uses the two-entry certificate and proof listed above.
• research/website-local-verification.json records an older 788-formula website check without a timestamp or artifact hash. It is historical UI evidence, not the current release receipt. The PDF, visual-review, build and deployment receipts have separate purposes.
• research/result-catalogue-audit.md analyzes an earlier 74-page checkpoint; research/solver-checkpoint.json records the initial solver/five-type stage. research/sparse-composition-resume.md retains a former “current strongest” n≥85 heading, although its uniform construction remains part of the n≥12 theorem.

Use the manuscript and handoff for current domains. Keep failed windows/crops, the nonuniversal cover, the odd-completion counterexample, and unsuccessful terminal-type repairs: they explain why stronger-looking shortcuts are not claimed. Failed searches imply only their recorded scope.

Website and manuscript dependencies

The research archives are not a standalone website checkout. src/check_web_solver.py needs the website TypeScript solver, explorer graphs, Node and esbuild in .site-worktree. The publication builder additionally needs the publishing Python packages (pypandoc_binary/pypandoc, Matplotlib and pypdf), LaTeX, and the website’s KaTeX/Node dependencies. Consult the current builder for executable configuration.

Use manuscript-source.zip for the standalone classification manuscript and figures. Use delivery-time-source.zip for the separate companion. Both source archives are recompiled independently before release. The shared research archive preserves the full project history and dependencies of both documents; it is not a claim that every archived investigation remains active. The research package also includes the paper figures generated by src/build_figures.py; this does not supply the complete website checkout and its dependencies. The optional lean/generate_finite_certificate.py also needs src/game_solver.py and research/solver-two-regular-hillclimb.json from the research archive.

A source guide cannot certify what is live. Public release.json supplies download identities; research/publication-build.json and research/website-deployment.json in the maintained repository distinguish build from verified public readback. Those mutable release records may be excluded from the research archive to avoid circular or stale metadata.

Current all-parity code and protected-set additions

The counting proof in paper/core-code-composition.md now includes odd and even core sizes. The constructor src/core_code_all_parities.py lists the permitted independent sets directly. src/core_code_all_parities_check.py --check independently compares the counting formula with cycle-polynomial recurrence and literal subsets, and verifies full asymmetric two-move witnesses for its recorded examples. The same receipt includes the fixed mixed105 code list. research/core-code-third-circle-envelopes.json stores literal protected sets at100..111; src/core_code_third_circles.py --check checks the six protected differences and exact prefix budgets. Their discovery searches are separate historical evidence and are not required to instantiate the saved recipes.

Current regression commands

Run python3 src/main_interval_complete.py --check to replay the current finite interval plans and exact adjacency boundaries without overwriting a receipt. The current saved result is research/main-interval-pair-complete-checks.json; the older research/main-interval-complete-checks.json retains its historical source pins. python3 src/main_interval_six_circle.py --check and python3 src/main_interval_reduced_hubs.py --check replay their concrete premises. python3 research/main-interval-fifth-ordinary-review.py independently reconstructs and checks the earlier circle and hub families. The staged record and bundle identify the exact finite ranks; their independent replay tools check fixed evidence rather than rediscovering graphs.

The September18 proof simplification has four separately scoped checks. python3 src/sparse_upper_kernel_check.py --check verifies the arithmetic consequences of the shared deletion/support induction, retaining the finite exclusions as explicit premises. python3 src/main_interval_pair_codes_check.py --check independently reconstructs pair witnesses, finite interval coverage and actual constructor outputs. python3 src/dense_functional_transfer_check.py --check checks the functional attachment identity and exceptional dense graphs. python3 src/odd_projection_threshold_check.py --check replays the frozen local rank certificates and checks the sharper residue projection inequalities. These are checks of supplied constructions and proof obligations, not new extremal graph searches or full Lean proofs. Their receipts are indexed under proof_simplification_20260918.

The earlier main_interval_expanded.py, main_interval_fourth_review.py, main_interval_new_independent.py and sparse_third_coverage_review.py receipts retain their earlier checkpoint scopes and source identities. A review requiring old ledger bytes must be run against those bytes, not presented as a review of the new ledger. The current coverage and recipe audits are python3 src/classification_coverage.py --check and python3 src/audit_explicit_constructions.py --check.

The retained main_interval_fourth_review.py command checks the fourth-pass historical gap counts, not the completed ledger. It is not a current release validation command. Use the source-pinned classification and explicit-construction checks for the current zero-gap state.