Main.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.RationalHitting.ExecutableGenerator.stack_implementation line 10
Source documentation
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 stack_implementation : StackImplementation := by
…
```
Mentions: OAI.RationalHitting.ExecutableGenerator.StackImplementation
theorem OAI.RationalHitting.ExecutableGenerator.implementation line 35
Source documentation
The finite-state compilation of the uniform stack implementation.
```
theorem implementation : Implementation := implementation_of_stack stack_implementation
…
```
Mentions: OAI.RationalHitting.ExecutableGenerator.Implementation, OAI.RationalHitting.ExecutableGenerator.implementation_of_stack, OAI.RationalHitting.ExecutableGenerator.stack_implementation
theorem OAI.RationalHitting.main line 44
Source documentation
A rational hitting list preserving every inverse domain, with invertible values, canonical rational binary output, and polynomial deterministic finite-state Turing time.
Distinct definitions of this name: ComparatorChallenges/RationalHitting.lean:108 (same statement text; different proof or body). Qualify references as OAI.RationalHitting.main@path.
```
theorem main : MainStatement :=
…
```
Mentions: OAI.RationalHitting.MainStatement