Third-party source materials and attribution
============================================

This archive includes adaptations of computational and algebraic infrastructure
from OpenAI math, revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb:
https://github.com/openai/math/tree/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Computability/RationalHitting

The upstream materials are licensed under Apache License 2.0. The unmodified
license is included at reference/openai/LICENSE. Original reference sources,
with their notices, are preserved under reference/openai/lean/ and identified
by reference/openai/provenance.json. These reference copies are not imported
by TC10. Adaptations have local namespaces/imports and, where indicated,
generalized statements or new integrations. File headers and
TC10/Runtime/PROVENANCE.txt describe that reuse and the successive integrations.
All imported local proofs are rebuilt and audited; provenance is not a proof.

Lean and mathlib dependencies are fetched separately at the revisions recorded
in lean-toolchain and lake-manifest.json. They retain their own licenses.
This notice records third-party terms; it does not assign a new license to the
manuscript or to original contributions in this project.
