a(6) = 872

The paper (PDF) · The paper (source) · The claim, exactly · Every known gap · The audit matrix · Errata · Audit & provenance report · Priority & literature

A computer-assisted proof that the minimal superpermutation on six symbols has length 872.

The upper bound a(6) <= 872 is Robin Houston's 2014 witness and is an input to this work. This package proves the lower bound a(6) >= 872, closing the interval 868 <= a(6) <= 872 that had stood since 2019. (On the same day as this release, Hunter and Raudvere announced a Lean-formalized a(6) >= 869 and a(7) >= 5888 — see [HR26] in the paper's references; it does not conflict with this work and independently machine-certifies two of the four lengths excluded here.)

Status, in three sentences

The statement "some six-symbol superpermutation has length at most 871" is reduced, by proved and elementary steps, to the emptiness of a finite partition of 209 cells, and every cell has a recorded verdict of zero. The reduction is a theorem; the partition is machine-checked as a partition, not merely as a total. The end-to-end certification is conditional: it rests on the conformance obligations stated in GAPS.md, and we publish the evidence tier those obligations imply rather than a friendlier number.

Verify it in fifteen seconds

python3 verify/verify_all.py --tier 1

Stock Python 3.9, no dependencies, no downloads. Nine checks recompute the arithmetic backbone from scratch: the interval-macro table, the partition maxima, both unconditional filters, the confinement identities, beta <= s - 1, and the closed forms for the last cells. Everything else rests on this; if it fails, stop and open an issue.

python3 verify/verify_all.py --tier 2      # minutes; every ledger checker that runs offline
python3 verify/fetch_archives.py           # ~540 MB from the Zenodo deposit, hash-checked
python3 verify/verify_all.py --tier 3      # ~1 hour; every shipped archive verifier

Be precise about what tier 3 buys: each archive's verifier is the producing implementation checking its own frozen logs. A pass proves hash-binding and internal consistency, not an independent replay. AUDIT.md records which cells an outside party has actually replayed.

Read next, in this order

1. CLAIM.md — the precise statement, what is proved here, and what is assumed.
2. GAPS.md — every known gap, with blast radius and closure path. Written to make disbelieving us easy; if you find a gap not listed there, that is a defect in the file as much as in the proof.
3. AUDIT.md — the per-cell evidence matrix, generated from the ledger and never hand-edited.
4. ERRATA.md — every claim made and withdrawn during this work, with impact.
5. paper/a6_872.md — the proof.

How to attack this result

The three questions worth asking first, in order:

1. Is the partition complete? The cells are generated by the confinement theorem, and verify_d4_priced.py checks that the classes partition the enumerated universe — not merely that counts agree. 209 = 8 + 26 + 60 + 115 across delta = 1..4.
2. What discharges the conformance obligations? GAPS.md states which are discharged and which are open. The open ones are exactly the direction in which a proof by exhaustion fails silently.
3. What did adversaries find? Two independent adversarial audits attacked the result. Both signed the parts they examined; both corrected claims of ours, and every correction is on record. Their reproducers ship in audits/ and run under tier 2.

A finding that weakens the result is worth more to us than one that confirms it. Open an issue; we would rather hear it now than after journal submission.

Contents

A bare clone contains everything checkable without bulk data: the ledger, the checkers, the derivation record, the audit matrix, and the adversarial reproducers. The 21 release archives and large producer outputs live in the Zenodo deposit; archives/BULK_MANIFEST.json is the generated, hash-bound inventory, and ledger.py validate fails if any row references a path that is neither present nor listed there.

Licensing: LICENSE-CODE and LICENSE-DATA. Citation: CITATION.cff.