Arithmetic source provenance
============================

Upstream: https://github.com/openai/math
Revision: fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb
License: Apache-2.0; the full license is at reference/openai/LICENSE.
Original sources and their recorded hashes remain in reference/openai/.

Scope note: the paragraphs below describe each module's own responsibility.
They do not list outstanding gaps. MainGenerator proves the complete generator;
FixedGenerator exposes its universe-independent machine and constants.

StackWords, BinaryAddition, BinaryMultiply, BinarySubtract, BinaryDivision,
and BinaryGcd adapt the identically named upstream RationalHitting modules.
WordRecords adapts the first namespace block of DenseRecords.lean, through
eval_unpackRecord. Namespace changes reuse TC10.StackLanguage and its actual
compiler; imports are narrowed to the local dependencies and Nat.Size.
No theorem is accepted merely because it was present upstream: all adapted
sources are rechecked by the pinned Lean kernel and included in TC10.Audit.

ModReduction.lean is the new integration. It supplies the explicit ten-stack
program, its complete execution proof, and a fixed Fin4 TM0 with a quartic
bound in the two input bit lengths. It proves only modular reduction.
It does not supply the full hitting-list generator.

Additional adapted computational infrastructure
----------------------------------------------
CleanMultiply takes BinaryBinomial.lean through eval_multiplyClean, before
factorMul. SignedDifference takes the third SignedBinary.lean namespace block
(wordValue_complement through eval_signedDifference). The factorial, binomial,
array-write, power-loop, and rational-encoding blocks are not imported.
Procedures, ProcedurePairs, ProcedureControl, Feasibility, Tabulation,
ListProcedures, SignedArithmetic and DenseDeterminant adapt the corresponding
upstream modules. Procedures imports WordRecords and CleanMultiply rather
than the unneeded upstream rational-encoding chain. SignedArithmetic imports
the narrowed SignedDifference. DeterminantAlgorithm adapts Determinant.lean,
with direct mathlib Bird determinant imports; the Vector.get/ofFn bridge is
made explicit for the pinned toolchain. ListOperations takes only the generic
list-flattening block of MatrixComputation.lean.

CompileProcedure, PivotComputation, PivotCompression and ComplementQuotient
are new integrations/proofs. They certify the actual finite-TM quotient
calculation from a supplied rectangular matrix and pivot lists. They do not
select the pivots or implement the full hitting-list generator. All runtime
encodings are explicit and are not identified with the main theorem encoding.

Further original integrations/proofs
-----------------------------------
PivotExtension, PivotSelection, PivotSelectionTime, SelectedQuotient and
QuotientMachine implement and verify pivot search and its complete quotient
composition. BoundedQuotientDesign now uses the computed quotient.
ModProcedure connects the existing concrete binary remainder program to the
compositional Procedure/Poly interface. CharacteristicPivot,
CharacteristicPivotTime and CharacteristicQuotient extend the algorithm to
integer representatives in characteristic p, with p=0 included. Their fixed
machine and polynomial transition count precede every binary characteristic
and input matrix. The kernel, row count, literal output and entry-height
specifications are proved. None of these modules supplies short-code honesty,
finite-extension arithmetic, or the complete hitting-list generator.

Finite-extension arithmetic integrations
---------------------------------------
ModularMatrix, ModularMatrixSemantics, BitAccess, BinaryMatrixPower,
BinaryMatrixCorrectness, FiniteExtensionArithmetic, FiniteExtensionMachine,
FiniteExtensionEquality and PrimeMatrixInverse are original integrations
and proofs. They use the previously checked integer arithmetic, determinant,
Procedure composition and finite-TM compiler. Regular-representation field
laws and finite-field powering facts come from the pinned mathlib.
The raw-bit length/head/tail programs have complete Eval proofs. Matrix
powering is binary and has an intermediate-size invariant; caching is proved
extensionally equal to the original matrices. No executable field/basis oracle
is used. These supply arithmetic operations, not the complete generator,
field/basis construction or short-code honesty.

Canonical presentations and exhaustive field construction
--------------------------------------------------------
MonicPresentation, CompanionConstruction, PolynomialMatrix,
PowerBasisCoordinates, PowerBasisArithmetic, ListSearch, MatrixZero,
FieldTest, ResidueGrid, FieldConstruction, UnaryParameters and
BinaryFieldConstruction are original integrations/proofs. Algebraic quotient,
power-basis, finite-field existence and primitive-element existence facts
come from the pinned mathlib. Noncomputable choices are used only to prove
that the finite search contains a successful candidate, never as operations
of the implemented search. The constructor has a proved runtime polynomial
in an explicit unary cardinality budget. For the manuscript's binary stage,
that budget and every parameter are computed from unary q, giving one fixed
polynomial-time TM for field construction. This does not supply short-code
honesty, the large-characteristic etale construction, or the complete
hitting-list generator. All new modules enter the transitive axiom audit.

Large-characteristic etale construction
--------------------------------------
BoundedOrder, BoundedOrderSearch, OddCyclotomic, EtalePowerBasis,
EtaleRealization, LargePrimeRawSampling, LargePrimeHomogeneousHitting,
LargePrimeAffineHitting and LargePrimeConstruction are original integrations
and proofs in this project. The generic power-basis/realization and sampling
proofs generalize the checked local rational construction; polynomial root
counting and finite multiplicative order use the pinned mathlib. The literal
bounded-order search, quotient coefficients, companion and sample list have
one fixed finite TM with polynomial dependence on bitlen(p). Every geometric
component is accounted for in the semantic hitting proof, without factoring
the quotient. The full quotient/lift/list runtime composition and short-code
honesty remain unproved. All these modules enter the transitive axiom audit.

Relative strict coding and executable short-code postprocessing
--------------------------------------------------------------
UnitSubstitution and RelativeCyclicCoding are original proofs using the
existing generic evaluation, simultaneous witnesses and cyclic block
construction. They add relative multi-base coding and strict composition,
not a free-field embedding axiom or a proof of ShortWords.Honest.
WordProduct, ShortCodeDecode and PrimeCodeBatch are original executable
integrations/proofs using the checked integer determinant, modular matrix
arithmetic, finite stack-program combinators and compiler. Their fixed-TM
theorems concern exact short-code decoding and unit filtering of a supplied
prime-field candidate list. They do not assert that the upstream generator
or the main theorem's encoding has been composed. All modules enter Audit.

Literal encoding and rational canonicalization
---------------------------------------------
LiteralWords, LiteralInput, LiteralOutput, LiteralGenerator and PrimeOutput
are original integrations/proofs. They use the existing checked stack
programs, compositional compiler, and pinned mathlib identities for natural
binary digits and integer residues. The original TC10 encodeInput/encodeOutput
are unchanged. LiteralGenerator.main_of_generator is conditional on the
complete uniform data program and its semantic contract; no such complete
program is supplied here. PrimeOutput supplies the actual prime-field finishing
program for an explicitly supplied candidate list, including its final bytes.

FractionEuclid adapts the full BinaryFactorial.lean file from the pinned
OpenAI source (despite its name, that file supplies Euclid and quotient
routines). FractionReduction adapts the first StackLanguage namespace block
of RationalBinary.lean, through eval_fractionReduce. Namespace/import changes
use the existing TC10 machine. RationalLiteral adapts the three rational
canonicalization identities from RationalBinary.lean; its clean pair routine,
Procedure integration, signed-data normalization, literal encoder, entry bounds
and fixed-TM theorems are new. The upstream literal encoder is not reused:
it has a different digit order and zero convention. All adapted proofs are
rechecked, never accepted on provenance alone. Every module enters Audit.

Exact logarithmic honesty and computed finite-field roots
-------------------------------------------------------
IndexedSubstitution, GroupDictionary, GroupCyclic, TriangularDictionary,
TriangularPaths, ShortHonesty and SharpSemantic are original proofs. They
close the exact short dictionary and the unchanged sharp semantic target by
finite witness arguments; no universal free-field or embedding axiom is used.
All group identities are accompanied by strict formula-evaluation certificates.

PrimitiveRootSearch, FiniteRootConstruction and BinaryRootConstruction are
original executable integrations/proofs using the already checked matrix
powering, entrywise zero test, finite search, residue enumeration, field
construction and fixed-TM compiler. Finite cyclic-group/root existence uses
the pinned mathlib and only proves search success. The actual programs receive
no generator/root oracle. Exhaustive order tests have explicit unary budgets;
the binary stage computes these budgets from q and proves polynomial time in q.
The complete uniform hitting-list generator remains unimplemented.

Extension-coefficient pivot selection
------------------------------------
ExtensionMinor, ExtensionPivot, ExtensionPivotTime, PowerBasisPivot and
BinaryFieldPivot are original integrations and proofs. They reuse the existing
TC10 BlockDivision kernel argument, PivotExtension bordering identity, Bird
integer determinant, modular arithmetic, coefficient encoding and machine
compiler. No additional upstream source is imported. Unit reflection, exact
rank selection, polynomial intermediate encodings, coefficient-list conversion
and the binary field-construction composition are checked. Tests compare
literal algorithms against independent quadratic-field coordinate arithmetic.
The full generator, including extension-quotient/list composition, is still open.

Computed extension quotients and weighted naming selection
--------------------------------------------------------
NormalizedQuotient, MatrixSum, ExtensionInverse, ExtensionProjection,
ExtensionQuotient, ExtensionQuotientTime, PowerBasisQuotient and
BinaryFieldQuotient are original proofs and integrations. They use the checked
cofactor-kernel theorem, expanded-block regular representation, exact pivot
algorithm, prime-field inverse, power-basis conversion and machine compiler.
The implemented normalized quotient preserves the full kernel and has exactly
the complementary rows. The binary composition constructs its field from q.
No additional upstream source is imported.

ListArgmin, CollisionWeights, GreedySelector and GreedySelectorCorrectness are
original implementations/proofs using the existing binary integer arithmetic,
finite-stack compiler and WideGreedy semantic potential argument. The machine
computes the actual exponential weights and exact minimizing choices from the
supplied collision table. Finite-index transport connects this literal output
to the saved-log collision guarantee. The balanced naming table is now supplied by the subsequent integration.
The complete uniform hitting-list generator remains outstanding. All twelve
new modules enter the transitive axiom audit. Regression checks independently
check quadratic-field quotient products/full rank, signed entry bounds, empty
and noninitial-pivot cases, and naming selections across all small test tables.

Computed balanced names, literal copying and bounded field enlargement
-------------------------------------------------------------------
PrimePalette, GridCapacity, GridCoordinates, PrimeNamingTable,
PrimeNamingBalance, UnaryDivision, PrimeNames, PrimeNamesCorrectness and
PrimeNamesInterface are new local proofs/program compositions. They construct
the complete naming family from n,s and prove its balance, support separation,
original saved-log length bound and one fixed polynomial-time machine. The
auxiliary small prime removes the naming stage's previous extension-field
choice. Bertrand's postulate and finite-vector-space root counting are used
only to prove correctness of the explicitly searched/enumerated data.
SharpAssembly now invokes this computed naming interface with the same target.

BinaryListAccess and NamingCopy are new local compositions proving literal
name-driven matrix copying and final prime-field encoding. The core list is
still supplied; its universal construction and full runtime are not asserted.
SmallFieldStep is a new bounded composition of the checked field and root
constructors: failing capacity bounds the next quadratic field's cardinality
by (eW+2)^2. It has a binary-characteristic runtime bound and the existing
uniform degree bound. Initial small-prime cyclotomic splitting is supplied
separately by the subsequent Berlekamp integration; the full generator remains
outstanding.
All new modules are imported by TC10.Audit. No additional trusted axiom,
proof placeholder or native proof evaluator is used.


Computed Berlekamp splitting and initial cyclotomic fields
-------------------------------------------------------
BerlekampSplitting and Runtime/{FrobeniusMatrix,BerlekampKernel,
BerlekampScalar,BerlekampChoice,PolynomialRemainder,PolynomialMonic,
PolynomialGCD,BerlekampFactor,SmallCyclotomic} are local implementations
and formal proofs of classical algorithms and their integration. The factoring
method is Berlekamp's Frobenius-fixed algebra method, not claimed as a new
mathematical result. All algebraic lemmas, including the squarefree scalar-fixed
criterion and the nonzero-nonunit proper gcd, are proved in this environment.
The actual fixed basis comes from the existing checked prime-field quotient.
Polynomial remainder is computed using the existing canonical companion and
power-basis coordinates, followed by explicit modular monic normalization and
Euclidean iteration. The fixed-TM proofs use the local stack compiler and
proved bounds on all iterated state encodings. No external factoring engine,
field oracle or added upstream source is used.
The initial small odd-characteristic construction is now checked even when
the extension cardinality is too large to enumerate. The complete universal
core and MainStatement remain outstanding; no unconditional main proof is
asserted. New modules are included in the transitive audit and independently
implemented arithmetic regressions.


Executed design, cofactor, sampling and decoding pipeline
------------------------------------------------------
EnumeratedDesign, QuotientReindex, CofactorFormula, FiniteCyclicIndex and
Runtime/{MatrixListProduct,MatrixResize,MomentConstruction,MomentQuotient,
ComputedDesign,DesignOutput,CofactorEvaluation,BlockArithmetic,BlockForms,
CurveMatrices,CofactorTables,ExecutedCofactor,HomogeneousDecode,CofactorDecode,
PrimePipeline,ResiduePrefix,ResidueSamples,SampledPrimePipeline} are local
implementations and proof integrations, using the already audited compiler,
arithmetic and semantic theorems. No additional upstream source is imported.
The identities and algorithms are not asserted to be new mathematical results.

The exact computed quotient is linked to the rank theorem with an explicit
center enumeration, then multiplied and padded. The cofactor ring expression,
finite/cyclic index conversion, regular block ordering, companion and clock
are proved equal to the paper's realization. The composed prime-field machine
includes both guards, left normalization, the short dictionary and actual
serialization. Capped residue enumeration supplies distinct nonzero sample
scalars even when extension cardinality is too large to enumerate.

The complete arithmetic construction from original input parameters, final
universal simultaneous hitting contract, large-prime/rational branch integration
and MainStatement remain unproved. Pipeline runtime statements keep their
explicit seed/presentation/budget inputs; they are not substituted for the
unconditional main-input runtime statement. Every local module enters the
transitive axiom audit; independent regression computations remain tests only.

CachedExtensionQuotient is a local semantics-preserving optimization of the
existing computed quotient. It materializes the selected inverse once and
shares it throughout the output. compute_eq proves equality with the earlier
algorithm on all inputs, and compute_poly supplies its actual stack program.
MomentConstruction uses this implementation. No new correctness assumption,
upstream source or trusted evaluator is introduced by the optimization.

DenseDeterminant.detAlgorithm now calls the already local and proved tabulated
DeterminantAlgorithm.determinant. The old step expression remains as detBySteps;
detAlgorithm_eq and detAlgorithm_eq_steps prove both implementations identical.
This prevents repeated entry evaluation when running Lean functions directly.
The stack-machine construction and its polynomial proof still use the same
checked Bird semantics; no change to the trust boundary or main encoding.


Numeric odd-characteristic pipelines and executed sampling
--------------------------------------------------------
Runtime/{ExtensionOrderSearch,FieldDegree,CyclotomicField,CyclotomicArithmetic,
SmallPrimePipeline,SmallPrimeParameters,ExecutedSampling,RationalMatrix,
LargePrimeDesign,LargePrimePipeline,OddPrimePipeline} and the pipeline-sample
identity in ExecutedCofactor are local implementations and integrations.
They use the existing root-count, finite-field, rank, cofactor and descent
proofs, and the previously audited finite-stack/TM compiler. No additional
upstream source, oracle, evaluator axiom or mathematical axiom is imported.

The bounded extension-order search uses the elementary root-count argument
on a short candidate prefix. Degree selection retains the initial factor when
large enough and only enumerates a field under a proved polynomial failing-
branch cardinality bound. The large-prime quotient is computed over the prime
field before scalar lifting into the etale algebra. Rational normalization
uses adjugates, Euclidean fraction reduction and Cramer's rule. These algorithms
and identities are not claimed to be new mathematical results.

A single numeric-input odd-characteristic machine now includes the branch
selection and complete algebraic/encoding pipeline with the original q^4 and
W*q^7 bounds. At that stage the universal hitting/guard/short-decoding contract and
original-input assembly remained outstanding. The odd-prime part is now
closed by the integration described below; MainStatement is not claimed proved. New modules are included
in the transitive axiom audit and independent arithmetic regressions.

SmallPrimeHitting is the local specialization of those checked components to
the actually generated small-prime homogeneous list. Its universal hitting
and sharp core bounds do not assume arithmetic, design or sample witnesses.
That theorem explicitly precedes the two computed guards and short decoding;
their final odd-prime simultaneous-rank assembly is now proved below. No new
external result is used.


Complete odd-prime branch and rational finishing stages
-----------------------------------------------------
ExecutedEtaleSampling and LargePrimeHitting use the existing separable-root,
cofactor and block-descent results over commutative quotient algebras. The
regular block representation was generalized from fields to commutative rings
using Matrix.compRingEquiv and Algebra.leftMulMatrix. No field hypothesis is
silently imposed on a reducible cyclotomic quotient.

PrimeDecodedAssembly uses exact-list strengthenings of the prior guarded
normalization, unit filtering and short-code assembly. OddPrimeHitting and
OddPrimeGenerator integrate these with both numeric arithmetic branches,
original p,n,s,h parameters, balanced naming and exact finite-TM compilation.
The entire odd-prime original-input branch is now unconditional, including
the original sharp exponents; the all-characteristic MainStatement is not.

IntegerListProduct bounds all intermediate integer entries before invoking the
existing signed-remainder matrix loop. RationalShortDecode uses those exact
products and a shared-denominator power. RationalOutput, RationalCodeBatch,
RationalNaming and RationalNormalize implement rational finishing with actual
guards and exact canonical encoding. Their raw universal rational input still
needs an implementation and correctness proof. These are local integrations,
with no new external mathematical theorem, oracle, evaluator trust axiom or
claimed mathematical novelty. Every production module is transitively audited.


Final rational, sharp binary and all-characteristic closure (2026-10-16)
---------------------------------------------------------------------
The preceding entries describe earlier checkpoints. MainGenerator.main now
proves the exact unchanged MainStatement, including the complete original-input
finite-TM generator in every characteristic. No new external mathematical
result was imported for this final integration.

GeneratedFiniteHitting factors the verified finite-field execution/sampling
argument into a common interface. BinaryPipeline and BinaryExecutedHitting
supply it with actual BinaryRootConstruction outputs; BinaryGenerator retains
the sharp binary exponents through original-input parameters, short decoding
and balanced naming. PositiveGenerator combines the completed prime branches.

RationalDesign implements powers-of-two moments and the selected integral full
quotient, using EnumeratedDesign's explicit center enumeration. IntegerMatrix,
IntegerCofactor and IntegerCurve implement exact integer operations and the
literal companion/clock cofactor lift. IntegralCofactorFormula proves the
commuting-factor reordering; IntegerCurveSemantics proves the exact entry and
index agreement with IntegralCompanionHeight.raw. RationalPipeline computes
the fixed parameters and every raw sample. RationalExecutedHitting uses the
existing rational all-component sampling/descent theorem on precisely these
matrices. RationalAffineAssembly and RationalDecodedAssembly preserve actual
list coverage through both guards and the short decoder. RationalGenerator
adds balanced naming and exact canonical output with the sharp bounds.

MainGenerator.data performs the characteristic branch inside its actual
finite-stack program. LiteralGenerator.compile and the existing compiler
provide one finite TM and a polynomial bound on actual transitions and the
complete serialized output. The proof MainGenerator.main uses the hash-pinned
MainStatement directly, with no additional hypotheses. The original manuscript,
MainTheorem.lean and Encoding.lean remain byte-for-byte unchanged. Standard
Lean axioms propext, Classical.choice and Quot.sound are the only allowed
transitive axioms. These integrations are not a mathematical novelty claim
for the component constructions or a practical-runtime optimality claim.
