FINAL SUBMISSION CHECK -- 18 OCTOBER 2026

DOCUMENTS
The main paper is 22 pages and the formal supplement 24 pages. Both have
standalone LaTeX sources. The reference audit corrects the Fortin-Reutenauer
pinpoint, documents Table 1 height reduction, verifies publication metadata,
sorts and standardizes all 23 references, and pins the two checked quotations.
Changed pages were visually inspected; unchanged page renders match their
preceding inspection. Compiler and PDF/source records are in
formal/tc10/validation/visual-audit.json and supplement-visual-audit.json.

MATHEMATICS AND FORMAL CORRESPONDENCE
All 18 numbered statements, mathematical proof arguments, 366 production
Lean files, nine reviewer scripts, 31 source excerpts and dependency pins are
preserved. The full reviewer command checks the exact distributed sources,
compiles the project, audits 8,679 declarations and 22 named theorems, checks
85 navigation declarations and six fixed witnesses, and runs 8,047 arithmetic
regressions plus parser, excerpt and characteristic-two diagnostics. Only
propext, Classical.choice and Quot.sound are allowed. No new axiom is added.
See REVIEWER_GUIDE.txt for the precise formalization scope: the abstract
free-field identification and the paper's general-tree strengthening are
not claimed as separately formalized Lean results.

REPRODUCIBILITY
validation/verification.json records the current full verifier on macOS arm64
with reusable compiled artifacts. The historical isolated-build record covers
byte-identical Lean sources and reviewer scripts and is not a new rebuild of
this editorial revision. All package files are checksummed; the completed ZIP
is tested after fresh extraction. Dependencies and toolchain are pinned; their
caches and binaries are not distributed. Third-party license notices remain.

STATUS
The package is prepared for external mathematical review and submission.
These are internal build, correspondence and artifact checks, not independent
peer-review certification. DOI 10.5281/zenodo.23453468 is reserved; the Zenodo
record is unpublished and public deposit remains deferred. Linux verification
is excluded and has not been run. No public upload, journal submission or new
license assignment is performed.
