PAPER / LEAN DECLARATION MAP
All source paths below are relative to formal/tc10/.

Coverage: every numbered definition, theorem, lemma, proposition and corollary.
The paper includes complete mathematical arguments except for standard cited
results and the compiler/low-level arithmetic implementation, which is proved
in Lean. Proof-route and scope differences are explicitly identified below.
No row asserts that a declaration name alone establishes correspondence.
Read the cited definitions and theorem signatures.

Definition 2.1: Strict admissibility and operational rank [def:rank]
Definitions and attained-rank equivalence. Lean states a matching integer upper bound and witness instead of defining a rational supremum.
  TC10.ExprMatrix.Admissible — TC10/MatrixSemantics.lean
  TC10.UpperRank — TC10/MatrixSemantics.lean
  TC10.Attains — TC10/MatrixSemantics.lean
  TC10.intrinsicRank — TC10/StructuralRank.lean
  TC10.structural_rank — TC10/StructuralRank.lean

Theorem 2.1: Universal polynomial matrix tests over every characteristic [thm:paperMain]
Unconditional, unchanged main contract. FixedGenerator strengthens its presentation: all six named witnesses have no universe parameters. PaperContract expands strict evaluation and permits three independent field universes. The finite machine is obtained by proved compilation, not an assumed runtime oracle.
  TC10.MainStatement — TC10/MainTheorem.lean
  TC10.Runtime.MainGenerator.main — TC10/Runtime/MainGenerator.lean
  TC10.Runtime.FixedGenerator.specification — TC10/Runtime/FixedGenerator.lean
  TC10.PaperContract.main — TC10/PaperContract.lean

Corollary 2.2: Scalar rational identity testing [cor:paperRIT]
Consequence of the main theorem. The checked scalar lemma has the simultaneous-rank conclusion as a hypothesis; the main theorem discharges it.
  TC10.scalar_corollary — TC10/ScalarCorollary.lean

Corollary 2.3: Universal affine-rank tests [cor:affine]
The paper gives the size accounting and identifies operational rank with noncommutative free-field rank using IQS Theorem 1.5 (a rank-attaining blow-up over a sufficiently large field) and Lemma 5.3 (field-extension invariance). Allowing extensions avoids the small-field regularity obstruction. This abstract-free-field identification is NOT newly formalized here. Lean proves the all-characteristic operational statement applied to expression matrices; the cited interpretation is an ordinary mathematical corollary.
  TC10.SimultaneousRanks — TC10/MainTheorem.lean
  TC10.Runtime.FixedGenerator.specification — TC10/Runtime/FixedGenerator.lean

Proposition 2.4: List lower bounds [prop:lower]
Exactly the total-size and coefficient-extension quantifiers of SimultaneousRanks.
The eigenvalue-cover proof gives L >= floor(s/3)+1 at every height.
The four-leaf pair matrix gives n <= p^(D*D*L) for s>=4.
Neither proof assumes invertible or mutually conjugate coordinates.
  TC10.UniversalLowerBounds.list_length — TC10/UniversalLowerBounds.lean
  TC10.UniversalLowerBounds.naming_bound — TC10/UniversalLowerBounds.lean
  TC10.UniversalLowerBounds.signatures_injective — TC10/UniversalLowerBounds.lean

Lemma 3.1: Division lift [lem:lift]
The paper supplies the quantum-plane/localization proof; Lean uses an explicit Hahn-series division algebra with a matrix representation. Both give strict lift, rank monotonicity and divisibility by the block dimension. The representation construction is substantially more detailed in Lean.
  TC10.QuantumMatrices.fourier_reconstruction — TC10/QuantumMatrices.lean
  TC10.QuantumLift.expression_rank_lift — TC10/QuantumWitness.lean
  TC10.PermittedLift.expression_rank_lift — TC10/PermittedLift.lean
  TC10.DivisionRank.block_dimension_dvd_rank — TC10/DivisionRank.lean

Lemma 3.2: Permitted scalar witnesses [lem:scalarwitness]
Complete induction in the paper; permitted direct sums and the division lift are checked. The Lean induction states both domain and nonzero-to-unit witnesses.
  TC10.domain_and_unit_witnesses — TC10/DomainInduction.lean
  TC10.permitted_domain_witness — TC10/DomainInduction.lean
  TC10.permitted_unit_witness — TC10/DomainInduction.lean

Lemma 3.3: Simultaneous strict conditions [lem:generic]
The paper uses explicit rational numerators/domain polynomials. Lean proves the equivalent generic-matrix specialization via local rings; repetition/direct sums enforce common dimensions. There is no assumed common witness.
  TC10.GenericEvaluation.strict_lift — TC10/GenericEvaluation.lean
  TC10.GenericEvaluation.rank_lift — TC10/GenericEvaluation.lean
  TC10.simultaneous_generic_rank — TC10/SimultaneousRank.lean

Theorem 3.4: Simultaneous division witnesses [thm:structural]
Paper and Lean give integral optimal rank and simultaneous minor witnesses. Finite maxima/least integer upper bounds avoid a proper-class supremum in Lean.
  TC10.structural_rank — TC10/StructuralRank.lean
  TC10.simultaneous_rank_with_minors — TC10/SimultaneousWitness.lean

Proposition 3.5: Weighted certificates [prop:certificates]
The paper gives the realization and gate/domain induction; Lean checks the exact certificate orders and sums, including original strict inverse obligations.
  TC10.Formula.inverseNodes_iff_defined — TC10/AffineCertificateBounds.lean
  TC10.Formula.certificates_weight_budget — TC10/AffineCertificateBounds.lean
  TC10.family_certificates_bounded_order — TC10/FamilyCertificates.lean

Lemma 4.1: Support separation [lem:names]
Paper follows the implemented prime-field weighted selector. The abstract WideNames construction uses a different finite name field; the executed PrimeNames results supply the same palette and sharper saved-log bound. This distinction matters for exact list counts.
  TC10.Runtime.PrimeNames.length_bound — TC10/Runtime/PrimeNames.lean
  TC10.Runtime.PrimeNames.functions_separate — TC10/Runtime/PrimeNames.lean
  TC10.Runtime.PrimeNames.construct_poly — TC10/Runtime/PrimeNames.lean

Lemma 4.2: An honest logarithmic dictionary [lem:code]
The written proof follows the checked finite-matrix relative-cyclic and triangular dictionary route, preserving every inverse gate. The final transfer explicitly uses a unit rank witness; TC10.UnitSubstitution.honest_transfer implements the transfer using generic unit inputs and strict evaluation certificates. Equality of group values alone is not assumed to identify domains at arbitrary inputs. No free-field embedding is used.
  TC10.RelativeCyclicCoding.honest — TC10/RelativeCyclicCoding.lean
  TC10.TriangularDictionary.relative — TC10/TriangularDictionary.lean
  TC10.TriangularDictionary.term_value_path — TC10/TriangularPaths.lean
  TC10.ShortHonesty.honest_dictionary — TC10/ShortHonesty.lean
  TC10.ConjugateCoding.code_size_exact — TC10/ExactCodeSize.lean
  TC10.ShortWords.leaf_size_exact — TC10/ExactCodeSize.lean
  TC10.ShortWords.size_le_exact_cost — TC10/ExactCodeSize.lean
Exact literal size is 5|w|+5, with no cancellation; generator constants remain unchanged.

Lemma 5.1: Overlap on a tree [lem:overlap]
The paper proves the general tree inequality. Lean verifies the star specialization actually used by the generator. The general-tree strengthening is not separately formalized; the main theorem needs only the checked star case.
  TC10.StarOverlap.row_bound — TC10/StarOverlap.lean
  TC10.StarOverlap.overlap — TC10/StarOverlap.lean

Lemma 5.2: Full-window folded multiplicity [lem:folded]
Full extended-window multiplicities and joint node distinctness are explicit in both arguments. The bound is an integer dimension inequality, not division inside the coefficient field.
  TC10.FoldedDeterminant.full_window_bound — TC10/FullWindow.lean
  TC10.FoldedDeterminant.spaced_full_window_bound — TC10/FullWindow.lean

Proposition 5.3: Constant rank gap [prop:quotient]
The paper uses the star tree and full-kernel projection, with padding. SquareQuotient proves the design over every coefficient extension; BoundedQuotientDesign and the executed quotient modules supply effective arithmetic.
  TC10.SquareQuotient.geometric_design — TC10/SquareQuotient.lean
  TC10.SquareQuotient.rank_and_threshold — TC10/SquareQuotient.lean
  TC10.BoundedQuotientDesign.rank_of_full_kernel — TC10/BoundedQuotientDesign.lean

Lemma 6.1: Direct central-curve realization [lem:curve]
Written simultaneous conjugacy and monomial action are expanded. Lean separately checks the even-order sign, determinant identity, central polynomial nonvanishing and degree bound.
  TC10.CompanionCurve.determinant — TC10/CompanionCurve.lean
  TC10.CompanionCurve.reduced_determinant — TC10/CompanionCurve.lean
  TC10.DeterminantCurve.nonzero — TC10/DeterminantCurve.lean
  TC10.DeterminantCurve.degree_bound — TC10/DeterminantCurve.lean

Proposition 6.2: Simultaneous sampling over every coefficient field [prop:sampling]
The union bound over components and certificates is checked, as is regular-representation descent. Distinct scalar samples remain distinct in each geometric component.
  TC10.SampledDescent.sample_then_descend — TC10/SampledDescent.lean
  TC10.CompanionSampling.pencil_sample — TC10/CompanionSampling.lean

Lemma 7.1: Stagewise rational heights [lem:heights]
The paper gives stagewise asymptotic estimates. Lean contains explicit (usually looser) integer bounds for quotient entries, lifted/decoded words, canonical rational encodings and executed intermediates. The particular O-expression H_raw is a written estimate, not a definition identifying every internal Lean bound.
  TC10.BoundedQuotientDesign.rational_square_bits — TC10/BoundedQuotientDesign.lean
  TC10.LiftedCodeHeight.code_entry_bits — TC10/LiftedCodeHeight.lean
  TC10.RationalWordHeight.normalized_height — TC10/RationalWordHeight.lean
  TC10.RationalWordHeight.code_height_bound — TC10/RationalWordHeight.lean
  TC10.Runtime.RationalGenerator.data_poly — TC10/Runtime/RationalGenerator.lean

Machine and implementation details beyond the numbered mathematical results:
  TC10/Encoding.lean: OutputsWithin, encodeInput, encodeOutput and tapeBit.
  TC10/Runtime/LiteralGenerator.lean: compile (actual finite-machine transitions).
  TC10/Runtime/FixedGenerator.lean: specification and six universe-free witnesses.
  TC10/PaperContract.lean: tape_word_injective and universe-transfer lemmas.
  TC10/Runtime/{BinaryGenerator,OddPrimeGenerator,RationalGenerator}.lean:
    output theorems and Poly proofs assembled in Runtime/MainGenerator.lean.
  TC10/Runtime/SmallFieldStep.lean: doubled-degree rebuilt field, NOT a quadratic
    tower representation. Full new-field enumeration is bounded by (eW+2)^2.
  TC10/Runtime/PROVENANCE.txt: adapted upstream compiler/arithmetic modules.

The accompanying scripts/paper_declarations.lean rechecks every declaration
named in the numbered-result entries. The dependency-wide axiom audit covers
all production TC10 modules. It does not formalize the external literature.
Full source of the target and its foundational predicates is reproduced in
EXACT_STATEMENT.txt; the original .lean files remain the authoritative sources.

Supplement S5: Branching-program corollary and explicit size conversion.
  TC10.BranchingPrograms.Program: affine-labelled DAG in topological order.
  TC10.BranchingPrograms.value: finite sum of adjacency powers, in path order.
  TC10.BranchingPrograms.Nonzero: a nonzero matrix evaluation over an extension.
  TC10.BranchingPrograms.paths_inverse: I-A has its finite path sum as inverse.
  TC10.BranchingPrograms.border_value_unit_iff: border/output unit equivalence.
  TC10.BranchingPrograms.affineMatrix_size: exact N^2(4n+1) literal-tree budget.
  TC10.BranchingPrograms.hitting: operational nonzero iff an invertible listed value.
All are in TC10/BranchingPrograms.lean. The main theorem discharges the
SimultaneousRanks hypothesis of hitting. Formula expansion is used only for
existence of a unit witness; its size does not enter the test-list budget.
No identification with an abstract free-algebra representation is asserted by
this operational corollary; no arbitrary rational-circuit extension is claimed.

SUPPLEMENTAL FINITE INTEGRATION EXAMPLE
TC10/CharacteristicTwoExample.lean checks the nonidentity homogeneous
normalization, actual n=2 dictionary, decoded pair, strict target evaluation,
cancelled inverse failure and exact literal sample encoding.
scripts/characteristic_two_example.py independently enumerates 256 raw pairs,
retains 36 unit pairs and checks 289 finite properties, including 882-bit
serialization and malformed-input rejection. This diagnostic neither executes
the universal core nor claims a new universal hitting set or machine runtime.

FINAL EXAMPLE CORRESPONDENCE CHECKS
TC10/CharacteristicTwoAudit.lean reuses the unchanged example and exact size
lemma. It proves the actual substituted-tree evaluation, its strict domain
pullback at the displayed unit pair, its exact 84 nodes and height two,
the 20-node leaf, structured sample output, rank two of its value, scalar
undefinedness over every characteristic-two field, and the exact displayed
32-bit output string. The finite 36-entry Python diagnostic is not presented
as a formal universal-core or Turing-machine execution.
