REVIEWER GUIDE

The target is Theorem 2.1. The generator precedes all target coefficients and
fields. One list member respects every original inverse gate and attains each
family member's maximum normalized rank. The actual dimension is independent
of variable count and height. Bit bounds count full dense printing and actual
finite-machine transitions. The characteristic is binary encoded; n,s,h unary.

READ THE FORMAL SUPPLEMENT
  S1: all 18 numbered results, proof-route limits and dependency structure.
  S2: complete parameter glossary and first-use locations.
  S3: explicit common-denominator heights and dense rational encoding bound.
  S4: exact semantic predicates, encoding, MainStatement, fixed witnesses,
      and the expanded contract with independent field universes.
  S5: lower bounds, branching programs, literature pinpoints, exact literal
      dictionary sizes, and the bounded characteristic-two integration example.
  S6: reproduction, provenance, measurements and publication state.

AUTHORITATIVE LEAN FILES (relative to formal/tc10)
  TC10/MainTheorem.lean: MainStatement, Structured and SimultaneousRanks.
  TC10/Encoding.lean: literal encodings, Tape.right_0 and OutputsWithin.
  TC10/Runtime/FixedGenerator.lean: named witnesses shared across universes.
  TC10/PaperContract.lean: expanded target and universe-transfer proofs.
  TC10/Audit.lean: computed declarations and the transitive trust audit.
PROOF_MAP.txt maps every numbered result to its source declarations. The
navigation script checks 85 declarations, including height/serialization,
branching-program, exact-size and characteristic-two example results.
EXACT_STATEMENT.txt preserves verbatim source for readers without Lean.

CORRESPONDENCE LIMITS
The exact logarithmic dictionary follows finite cyclic/triangular witnesses,
with a unit rank witness before transferring to literal trees. It does not
assume a free-field extension or identify arbitrary-input domains.
The paper's quantum-plane division proof and Lean's Hahn-series construction
give the same needed rank mechanism through different presentations.
Lean checks the star overlap case used by the generator; the paper's general
tree version is not separately formalized. The affine-rank corollary identifies
operational rank with abstract free-field rank using cited classical theorems;
that identification is explicitly outside this formalization. No claim is made
that the paper's asymptotic raw-height expression is definitionally equal to
every (sometimes looser) internal Lean integer certificate.

The fixed machine is selected from a proved compilation certificate using
standard Classical.choice. There is no assumed arithmetic or runtime oracle.
Admissibility is individual; a common witness is proved. Extensions are explicit
embeddings, size is one total family budget, and every original inverse gate
is retained. On halting only the tape from the head rightward is prescribed;
the left cells are unconstrained. Two nonblank bit symbols give lossless output.

CONTINUITY AND TRUST
The reference audit corrects citation locators and publication metadata, sorts
all 23 references, and explains the height reduction behind the comparison
table. The main paper remains 22 pages and the supplement 24. All 18 numbered
statements, proof arguments, 366 production Lean files, nine reviewer scripts,
generator parameters, dependency pins and literal encoding are unchanged.
The Fortin-Reutenauer proof citation now points only to Section 2, Corollary 1.
See validation/references-changes.json and reference-audit.json under formal/tc10/.
DOI 10.5281/zenodo.23453468 remains reserved and unpublished.
Historical revision records are retained as provenance, not represented as current hashes.
The full verifier checks the source inventory and all 31 displayed source
slices, then invokes Lean and computes transitive axioms. The only allowed
axioms are propext, Classical.choice and Quot.sound. Finite regressions and
Python diagnostics supplement kernel checking; they do not replace it.

validation/verification.json records the current full reviewer command.
validation/visual-audit.json and supplement-visual-audit.json record PDF/source
hashes and page-by-page inspection. The separate historical fresh-build log
states its measurement limits. Nonfatal linter warnings and heartbeat budgets
remain and are not extra axioms. No independent human referee certification,
successful Linux CI run, DOI deposit or venue-policy approval is claimed.
