Rational hitting lists: main

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/Main.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

theorem Complexity.RationalHitting.ExecutableGenerator.stack_implementation : StackImplementation

One fixed finite stack program computes the exact canonical list on literal unary inputs, with a fixed polynomial bound on all actual stack steps.

theorem Complexity.RationalHitting.ExecutableGenerator.implementation : Implementation

The finite-state compilation of the uniform stack implementation.

theorem Complexity.RationalHitting.main : MainStatement

A rational hitting list preserving every inverse domain, with invertible values, canonical rational binary output, and polynomial deterministic finite-state Turing time.