[edemaine]

Context: I proved a lot of complexity/algorithm theorems in https://github.com/edemaine/lean-trominoes and am now trying to "rationalize" against more common infrastructure. Complexitylib seems like one target, and one thing I could use is Mathlib's TM2. In any case this seems like a useful tool for others, and even on your roadmap, so thought I'd make it my first contribution. As it is my first, I may have made some mistakes; happy to revise as you request. (Or feel free to edit yourself.) I haven't actually tried using these theorems yet...

---

Mathlib’s TM2 machines compute using several stacks, making them convenient for implementing algorithms. Complexitylib’s FP class consists of functions on binary strings computable in polynomial time. Complexitylib already connects Mathlib’s single-tape TM0 machines to FP; this PR extends that connection to TM2.

Mathlib already compiles TM2 machines into TM0 machines, but its correctness theorem does not bound the simulation’s runtime. This PR establishes a quadratic bound: an input of length n and a TM2 computation taking t steps require at most C * (n + t + 1)² compiled steps, where C depends only on the machine. It also proves that the compiled machine produces the expected tape contents, including empty outputs.

Combined with Complexitylib’s existing TM0-to-FP bridge, the new input/output adapters support:

• Binary inputs and outputs, directly.
• Other finite sets of symbols, through explicit binary encodings. Input and output symbol sets may differ.
• Restricted input domains, checked by a finite-state validator. The source runtime bound is required only on accepted inputs.

Malformed symbol encodings and inputs rejected by the validator return empty output. Output-length bounds follow from the source runtime. Every working stack must have a finite symbol set.

The bridge reuses existing simulation tools from the rational hitting-list development. The original compiler files and their attribution remain unchanged.

This completes the OAI-TM2-BRIDGE milestone in the roadmap. That section describes the intended application to OpenAI’s formalization of choiceless polynomial time. Connecting its concrete algorithm and structure encodings to Complexitylib, and completing the planned separation theorem, remain separate work under OAI-CPT-STRUCTURES and OAI-CPT-SEPARATION. The integration notes distinguish the completed bridge from those remaining tasks.

Validation passed: the full library build, five validation suites, nine API checks, linters, 29 maintenance-script tests, axiom audit, and blueprint consistency checks. Examples cover different input/output symbol sets, empty symbol sets, malformed encodings, and restricted input domains.