U20 SUBMISSION COMPENDIUM - VERSION 1.0 - 3 OCTOBER 2026

CURRENT DOCUMENTS
  output/pdf/u20_submission_1.0/U20_Paper.pdf
  output/pdf/u20_submission_1.0/U20_Technical_Supplement.pdf
  publication/u20_paper_draft/main.tex
  publication/u20_paper_draft/supplement.tex

The main paper retains the U21-style 11-point amsart format. Figure 2 belongs
before Section 5; its ordering is checked in the rendered PDF. The documents
have no visible package-version or draft labels. Package versioning belongs
to this inventory and the verification records.

DEPOSIT AND CITATION
Version 1 DOI: 10.5281/zenodo.23095173
The paper, supplement and this compendium are prepared for the same Zenodo
deposit. The paper's companion citation identifies the immutable Lean archive
included here and uses that DOI. The DOI has been reserved in a saved Zenodo
draft; files have not yet been uploaded and the deposit is not published.
The reservation record is publication/u20_paper_draft/verification/zenodo_reservation.json.
Prepared record fields are in publication/u20_submission_compendium/paper-deposit-metadata.json;
their current abstract still needs to be synchronized to the Zenodo draft.
The document and software licenses below are applied to this package; the
prepared license metadata still needs to be synchronized to the Zenodo draft.
Repository upload and publication are separate actions.
The existing U21 DOI resolves publicly and supplies files;
publication/u20_paper_draft/verification/public-artifact-check.json records
the unauthenticated checks.
No venue-specific page limit, anonymity or submission declaration is implied.

LICENSES
Copyright (c) 2026 Michael Schroeder.
The paper and technical supplement, including their LaTeX source and original
figures, are licensed under Creative Commons Attribution 4.0 International
(SPDX: CC-BY-4.0). The Lean and Python code and associated software documentation
and verification data are licensed under the MIT License (SPDX: MIT).
These are separate scopes, not a choice of two licenses for every file.
LICENSE.txt identifies the scope, including the unchanged frozen archive.
LICENSES/ contains both full license texts; LICENSE_SCOPE.json records the
scope and the frozen archive checksum. Third-party rights and notices remain
unchanged. When redistributing the standalone formal archive, accompany it
with LICENSE.txt and LICENSES/MIT.txt so that its license travels with it.

VERIFY THE PACKAGE FIRST
  python3 verify_bundle.py

This checks every payload hash, the complete frozen companion, the current
source/PDF/log bindings, and both file-byte and portable tape-content hashes.
BUNDLE_MANIFEST.json is the current package manifest; RELEASE_MANIFEST.json
identifies the original formal companion. Neither is a digital signature or
an independent mathematical proof.
Untracked .pyc/.pyo files inside __pycache__ are ignored. Missing, unexpected
and changed payload files are named explicitly. A successful reproduction run
may rewrite recorded JSON/logs; those changes correctly fail a check of the
original delivered bytes. Use a fresh extraction for that integrity check.

WHAT WAS REMOVED
PACKAGE_CLEANUP.json lists each excluded file and its reason. The package
contains one current paper and supplement, their source, current verification
records, concrete data and the complete formal companion. Superseded paper
editions, duplicate manuscript PDFs, obsolete editorial audits, AI-specific
review prompts and the separate U21 publication package have been removed.
The historical bibliographic source-inspection record is retained without
its separate review manuscript. Original workspace archives are preserved
outside this package. Historical archive names in cleanup records identify
comparisons, not required package dependencies.

The immutable formal companion is kept intact, including original audit logs
and the research/U21 files needed by its reproducibility checks. Its original
ZIP is also retained because the clean-build script verifies and extracts it.
No compiled Lean caches, native binaries or third-party PDFs are included.

PROOF AND DATA ENTRY POINTS
  utm20_lean/U20/Machine.lean
  utm20_lean/U20/FinalTheorem.lean
  utm20_lean/PROOF_MAP.md
  publication/u20_paper_draft/verification/ProofInterfaces.lean
  publication/u20_paper_draft/verification/CompactReferenceChecks.lean
  publication/u20_paper_draft/verification/ReadabilityChecks.lean
  publication/u20_paper_draft/verification/reference-benchmark.json
  publication/u20_paper_draft/verification/reference-*-macro-replay.json
  publication/u20_paper_draft/verification/reference-*-terminal.json.gz

CURRENT VERIFICATION
The immutable formal archive passed a cache-free build on 2 October 2026.
The entire 360-file exported library was rebuilt and its full transitive
dependency audit passed. The current eight paper-facing Lean files passed
against that clean build. The source verifier also checked the literal table,
the 2,999-transition complete fixture, two million-step reference prefixes,
compact arithmetic, both full compressed macro replays and readback, and the
small literal differential controls. Current logs are beside the paper.

The 191 semantic mutation controls and three forbidden-proof controls remain
preserved original-release evidence; they were not repeated for this submission
preparation. No claim of a newly repeated mutation suite is made.

REPRODUCE
Prerequisites: Python 3.10+ and leanprover/lean4:v4.32.2 available through lake.
No external Lean packages are required. Work in a disposable extraction because
reproduction replaces generated evidence files.

From publication/u20_paper_draft/:
  python3 verification/clean_rebuild.py

Read verification/clean-build-location.json for the fresh project path, then:
  python3 verify_paper.py --formal-dir /path/to/fresh/utm20_lean

Source-only checks are the default. --source-only explicitly selects the same
mode; --build additionally creates and checks PDFs.

For just the independent checks:
  python3 verification/verify_readability.py
  python3 verification/verify_macro_replay.py
  python3 verification/reference_macro_replay.py

The paper README gives native bank regeneration and PDF build instructions.
The source/proof checks do not require TeX. The PDF build uses Tectonic 0.17.0;
PDF validation uses pypdf. All figures are embedded vector TikZ.

SCOPE OF THE RESULT
The reference route proves finite-input universality, halting equivalence,
original-source readback, O_T((t+1)(n+t+1)^2) target time and
O_T((t+1)(n+t+1)) retained space. Constants fix the source table and can be
astronomically large. The paper's linear streaming-encoding argument is
separate from Lean evaluator costs and uniform source-table compilation.

The two complete large executions are compressed queue replays with exact
calculated target costs and functional decoding of saved physical tapes.
They are not complete instruction-by-instruction target or five-tape reader
runs. Neither reaches an autonomous periodic refresh epoch. Historical priority,
global instruction-count minimality and practical speed superiority are outside
the claim. The main manuscript and supplement state these boundaries explicitly.
