TC10 LEAN PROJECT

The unchanged MainStatement is proved by TC10.Runtime.MainGenerator.main.
TC10.Runtime.FixedGenerator.specification supplies a named finite machine and
constants shared by fields in every universe. PaperContract.main expands the
full target, including strict domains, rank bounds, encoding and actual runtime.

From this directory:
  lake exe cache get
  python3 -B scripts/verify.py

The production project contains 366 Lean files (365 modules plus TC10.lean).
UniversalLowerBounds proves the height-zero list and finite-field naming
obstructions. BranchingPrograms proves the exact affine-tree budget and
universal operational hitting corollary. The original generator and main
theorem are unchanged; the audit includes the new results.
The exact statement and proof navigation are in EXACT_STATEMENT.txt and
PROOF_MAP.txt. Current verification evidence is in validation/verification.json;
contract.json pins the unchanged proposition, encoding and current manuscript.

The clean submission distribution contains the two PDFs and their standalone
LaTeX sources, this Lean project, and a reproduction guide. Its root README.txt
supplies full installation instructions and the tested-platform limitations.
The verifier's --package-only mode is for that extracted distribution; ordinary
workspace verification uses the current source and installed dependencies.

CITATION
Michael Schroeder, Universal Rank Tests for Noncommutative Rational Formulas
(2026). Reserved DOI: 10.5281/zenodo.23453468.
https://doi.org/10.5281/zenodo.23453468
The DOI identifies the work and its companion materials. The Zenodo record
is reserved and unpublished; the DOI becomes active on publication. The
submission package includes a BibTeX entry in its root CITATION.bib.
