RapidMachineDecisionInput.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Turing's Section 8 designated-symbol undecidability, specialized to the three finite presentations used by the rapid-forcing constructions. These are purely machine-theoretic conditional inputs.

def OAI.ForcedComputation.RapidMachineHaltingUndecidable line 14
Source documentation
Finite transition tables with a distinguished terminal state.
```
def RapidMachineHaltingUndecidable : Prop :=
…
```
def OAI.ForcedComputation.AlternatingMachineHaltingUndecidable line 20
Source documentation
Flattened finite tables with a finite list of terminal states.
```
def AlternatingMachineHaltingUndecidable : Prop :=
…
```
def OAI.ForcedComputation.LatticeMachineHaltingUndecidable line 25
Source documentation
Ragged finite tables, stopping at the first absent instruction.
```
def LatticeMachineHaltingUndecidable : Prop :=
…
```