UNIVERSAL RANK TESTS FOR NONCOMMUTATIVE RATIONAL FORMULAS
Michael Schroeder | Independent Researcher | 18 October 2026
Final submission package: paper, formal supplement and complete Lean proof

DOI AND CITATION
Reserved DOI: 10.5281/zenodo.23453468
https://doi.org/10.5281/zenodo.23453468
This identifier is reserved for the work and its companion materials. The
Zenodo record remains unpublished; the DOI becomes active on publication.
CITATION.bib supplies a BibTeX entry. zenodo-reservation.json records the
reservation; its draft URL requires access to the owner's Zenodo account.

START HERE
  paper/main.pdf                 Main paper, 22 pages including references.
  paper/supplement.pdf           Formal supplement, 24 pages.
  paper/main.tex                 Standalone main source; original layout retained.
  paper/supplement.tex           Standalone supplement source.
  REVIEWER_GUIDE.txt             Claim, trust boundaries and navigation.
  PUBLICATION_AUDIT.txt          Final findings, corrections and scope.
  CHANGES.txt                    Final assembly summary and explicit deferrals.
  formal/tc10/PROOF_MAP.txt       Every numbered result mapped to declarations.
  formal/tc10/EXACT_STATEMENT.txt Readable verbatim formal contract/predicates.
  formal/tc10/                   Complete proof, pinned dependencies and checks.
  SHA256SUMS                    Hash of every other distributed file.

REPRODUCE
Install Python 3.10 or newer, Git, curl and Lean's elan manager:
  https://github.com/leanprover/elan#installation
The project pins Lean 4.34.1 and every dependency revision. From this package:

  cd formal/tc10
  lake exe cache get
  python3 -B scripts/verify.py

Keep lake-manifest.json. The full verifier checks the manifest, unchanged
main theorem/encoding, all production sources, third-party attribution,
installed dependency revisions, import coverage and proof-placeholder
exclusions. It builds the library, audits the transitive axioms of all 8,679
local declarations, checks 85 navigation declarations and six universe-free
witnesses, and runs 8,047 arithmetic regressions. It also checks all 31
supplement excerpts, quotient/curve diagnostics at q=2,3, 13 audit-parser
regressions, 8 excerpt-checker regressions and 289 characteristic-two
integration checks. Any failed command is fatal.
New logs go to validation/local-run/, preserving supplied verification evidence.
No API keys, AI service or private arithmetic oracle are required.

Fast integrity check, without Lean or network access:
  python3 -B scripts/verify.py --package-only

Files plus installed dependency sources, without a new proof check:
  python3 -B scripts/verify.py --preflight

These fast modes explicitly do not claim to have checked the proof. Checksums
establish consistency of an unmodified review copy, not a digital signature.

QUICK DIAGNOSTICS (from formal/tc10)
  python3 -B scripts/check_supplement.py
  python3 -B scripts/test_supplement.py
  python3 -B scripts/test_verify.py
  python3 -B scripts/diagnostics.py
  python3 -B scripts/characteristic_two_example.py
  python3 -B scripts/parameters.py 2 10 1 0
  python3 -B scripts/parameters.py 0 10 1 0

The supplement checker matches source slices and mechanically escaped Unicode
symbols against their Lean files. It is not a separate proof checker.
The arithmetic diagnostics check star quotients and companion curves for q=2,3
over F_65537 and a 3x3 skew-symmetric pencil with an invertible size-2 evaluation.
The characteristic-two example enumerates 256 raw pairs at D=2, retains 36
unit pairs, decodes the exact n=2 dictionary, and checks strict evaluation
and 882-bit serialization. Its representative identities and 32-bit sample
encoding are checked in Lean. It is not universal-core generation or a TM run.
The calculator takes p n s h and prints the selected dimension and pre-filter
list bound. Positive p is promised prime; this is not a primality test. These
scripts are independent diagnostics, not the verified full generator. Dense
outputs are enormous even at s=1; no claim of practical efficiency is made.

RESOURCES AND PLATFORMS
A recorded fresh local-source build on macOS arm64 completed 3,631 Lake jobs
in 429.19 seconds with third-party dependency caches present. Fresh-build peak
RAM was unavailable. See validation/fresh-source-build.json and its log.
The unchanged Lean sources also have a recorded isolated rebuild without
prior TC10 build artifacts; see validation/publication-source-build.json
and publication-source-build.log. That record predates these editorial
changes. The complete reviewer command is rerun against the current paper. Its wall times,
cache scope, warnings and OS-reported maximum child-process RSS are in
validation/verification.json. That RSS is not aggregate simultaneous memory;
no minimum RAM specification is inferred. Installation also needs download
time and several GB of disk space; actual resources depend on host/parallelism.

Initial setup accesses elan.lean-lang.org, github.com and release/content
redirects, releases.lean-lang.org, and cache.mathlib.org. The pinned mathlib
source also documents lakecache.blob.core.windows.net. Once these exact
dependencies and toolchain are available, proof checks can run offline.

.github/workflows/verify.yml supplies a manually triggered Linux x86-64 replay
and retains verification/resource logs if run separately. Linux verification
is excluded from this revision at the author's request; it was not executed.
The DOI has been reserved. Zenodo publication and public deposit remain
deferred; no files were uploaded and no journal submission was made by this
revision.

PAPERS
Both PDFs were visually inspected page by page and compiled with the desktop
compiler and Tectonic. The main source enforces the agreed 22-page limit. Recompile in
a separate copy (PDF metadata and checksums may change):
  tectonic paper/main.tex
  tectonic paper/supplement.tex
The supplement uses standard mathematical fonts for Unicode Lean symbols;
it does not require a host-specific font or external source file to typeset.

CURRENT AND HISTORICAL EVIDENCE
validation/verification.json records this assembly. validation/references-changes.json
records the citation edits and unchanged mathematical inputs; reference-audit.json
records the primary sources, checked passages and publication metadata.
doi-changes.json records the preceding DOI integration.
Older revision and build records are retained as explicitly historical audit
evidence; their paper hashes do not describe this final version.

CONTENTS AND LICENSING
There are 366 production Lean files: TC10.lean and 365 modules. Two additional
Lean scripts check arithmetic and declaration names. The 53 original upstream
reference Lean files are not imported; their notices, Apache 2.0 license and
recorded hashes are retained. See formal/tc10/THIRD_PARTY_NOTICES.txt and
TC10/Runtime/PROVENANCE.txt. Dependencies retain their own licenses. No new
license is assigned here to the paper or original contributions. Working
notes, historical manuscripts, build caches, binaries, temporary renders and
private machine paths are excluded.
