Michael Schroeder · Preprint · Version 1.0 · 18 October 2026 · ORCID 0009-0004-3249-0195

Universal Rank Tests for Noncommutative Rational Formulas

DOI: 10.5281/zenodo.23453468

Abstract

Testing noncommutative rational expressions requires preserving the domains of their inverse operations while detecting their algebraic rank. We construct universal matrix evaluation lists that achieve both over every field, extending polynomial rational testing constructions over ℚ to arbitrary coefficient fields.

For n variables, total tree size s, and inversion height h, the list depends only on these bounds and the characteristic. Every family of individually admissible rational expression matrices within these bounds has a common evaluation in the list at which every original inverse is defined and every matrix attains its maximum normalized rank. All evaluation entries lie in the prime subfield.

In characteristic two, the matrix dimension is O(s2 log3(s+2)), and the list length is O((h+1)s8 log6(s+2) log(n+2)). In every other characteristic, the corresponding bounds are O(s4 log4(s+2)) and O((h+1)s10 log7(s+2) log(n+2)). Thus matrix dimension is independent of the number of variables and inversion height, while list length depends only logarithmically on the number of variables. The construction yields coefficient-independent, nonadaptive tests for affine noncommutative rank over every field.

One deterministic Turing machine constructs the complete densely encoded lists in polynomial time, with the characteristic supplied in binary. We prove the main theorem, including serialization and the machine’s runtime bound, in Lean.

Paper and Supplement

The paper presents the universal construction, its bounds and applications to rational identity testing and affine noncommutative rank. The supplement records the exact formal statement, proof correspondence, encoding, runtime guarantees and limits of the formalization.

Lean Proofs and Verification Materials

The complete release includes both PDFs and their LaTeX sources, all 366 production Lean files, pinned dependency revisions, proof-correspondence documentation, verification scripts, recorded audits and integrity checksums. Working files and build caches are excluded.

Start with README.txt and REVIEWER_GUIDE.txt in the archive. Reproduction requires Python 3.10 or newer, Git, curl and Lean’s elan manager; the project pins Lean 4.34.1 and every dependency revision. From formal/tc10, run lake exe cache get, followed by python3 -B scripts/verify.py. Use a fresh extraction and retain lake-manifest.json.

For a fast integrity and contract check without Lean or network access, run python3 -B scripts/verify.py --package-only from the same directory. This mode does not check the proof. The full verifier builds the library, audits declaration dependencies and runs the supplied regression checks.

Citation and file integrity

Schroeder, Michael. Universal Rank Tests for Noncommutative Rational Formulas. Version 1.0, Zenodo, 2026. DOI: 10.5281/zenodo.23453468. Download the BibTeX citation.

The paper, supplement and ZIP on this site are byte-identical to the published Zenodo files. Download the SHA-256 checksums. The archive contains its own manifests and verification records.

The unchanged archive preserves preparation-time references to a reserved DOI, an unpublished record and no licence yet assigned. Version 1.0 was published on 18 October 2026; the published record specifies the licence for this release.

The Result and Its Formalization

The evaluation list is chosen before the targets and their coefficients are known. Within the prescribed total tree size and inversion-height bounds, every family whose members are individually defined somewhere has a common listed evaluation preserving every inverse and attaining every member’s maximum normalized rank. Rank is normalized by the size of the substituted matrices, and its maximum ranges over all dimensions and coefficient-field extensions.

Lean verifies the main theorem’s strict evaluation semantics, rank and domain guarantees, list construction, dense serialization and polynomial Turing-machine runtime. The characteristic-two construction has sharper dimension and list-length bounds. The supplement distinguishes the checked theorem from the separate written general-tree strengthening and the cited classical identification with abstract free-field rank.

The recorded audit rebuilt all 366 local Lean files on macOS arm64 and checked 8,679 declarations using only the standard Lean foundations propext, Classical.choice and Quot.sound. Linux verification has not been performed. The construction provides polynomial complexity guarantees; its explicit dense outputs remain enormous even for small parameters, and no practical full-generator run is claimed.

Licences

Except for material carrying a separate licence notice, Michael Schroeder’s original contributions in this deposit are released under Creative Commons Attribution 4.0 International (CC BY 4.0). Third-party material retains its existing licences, including Apache License 2.0 for the OpenAI reference sources and identified adaptations. See formal/tc10/THIRD_PARTY_NOTICES.txt, the source-file headers, and the included licence and provenance files.

Acknowledgments

The preparation of this manuscript and its computational companion benefited from assistance by AI systems developed by OpenAI and Anthropic. Responsibility for the mathematical claims, implementation, and presentation rests with the author.