MachineTranslationTable.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Full forward permutation-table emission for a fixed binary-vector alphabet.

The input to this component is the zero-delimited unary index of one offset in F₂^s; this is an internal finite label, not a binary 3SAT variable name. The output is the serialization of every forward image of the translation. A finite-state transducer counts up to 2^s, emits the fixed literal table at the delimiter, and resets. The state bound and emission table depend only on the fixed dimension, and the polynomial-time certificate is obtained from the proved actual TM2 transducer and reversal programs.

This component supplies neither an occurrence-list loop nor a whole reduction.

def OAI.UniqueGamesTheorem.MachineTranslationTable.table line 34
Source documentation
Both the forward and inverse arrays have one entry for every alphabet label.
```
def table {s : Nat} (offset : Vector s) : Target.PermutationTable (2 ^ s) :=
…
```
theorem OAI.UniqueGamesTheorem.MachineTranslationTable.table_images line 37
theorem OAI.UniqueGamesTheorem.MachineTranslationTable.table_inverseImages line 42
theorem OAI.UniqueGamesTheorem.MachineTranslationTable.table_satisfied_iff line 48
def OAI.UniqueGamesTheorem.MachineTranslationTable.tableBits line 53
theorem OAI.UniqueGamesTheorem.MachineTranslationTable.decode_tableBits line 56
theorem OAI.UniqueGamesTheorem.MachineTranslationTable.tableWords_length line 60
abbrev OAI.UniqueGamesTheorem.MachineTranslationTable.State line 64
Source documentation
The last finite-control value is an overflow sentinel.
```
abbrev State (s : Nat) := Fin (2 ^ s + 1)
```
def OAI.UniqueGamesTheorem.MachineTranslationTable.initial line 66
def OAI.UniqueGamesTheorem.MachineTranslationTable.increment line 68
def OAI.UniqueGamesTheorem.MachineTranslationTable.transition line 71
def OAI.UniqueGamesTheorem.MachineTranslationTable.emission line 75
Source documentation
Every entry is a fixed finite output word, indexed by the fixed control state.
```
def emission {s : Nat} (state : State s) (symbol : Bool) : List Bool :=
…
```
Mentions: OAI.UniqueGamesTheorem.MachineTranslationTable.State
def OAI.UniqueGamesTheorem.MachineTranslationTable.output line 81
theorem OAI.UniqueGamesTheorem.MachineTranslationTable.output_word_from line 84
theorem OAI.UniqueGamesTheorem.MachineTranslationTable.output_encoded_append line 104
Source documentation
One serialized finite offset produces the complete forward table in order.
```
theorem output_encoded_append {s : Nat} (offset : Vector s) (rest : List Bool) :
    output s (encodeWord (Encoding.alphabetEquiv s offset).val ++ rest) =
      tableBits offset ++ output s rest := by
…
```
Mentions: OAI.UniqueGamesTheorem.MachineTranslationTable.output, OAI.UniqueGamesTheorem.MachineTranslationTable.tableBits
theorem OAI.UniqueGamesTheorem.MachineTranslationTable.output_encoded line 117
theorem OAI.UniqueGamesTheorem.MachineTranslationTable.output_encoded_list line 122
Source documentation
Complete tables are concatenated in the input occurrence order.
```
theorem output_encoded_list {s : Nat} (offsets : List (Vector s)) :
    output s (offsets.flatMap (fun offset =>
      encodeWord (Encoding.alphabetEquiv s offset).val)) = offsets.flatMap tableBits := by
…
```
Mentions: OAI.UniqueGamesTheorem.MachineTranslationTable.output, OAI.UniqueGamesTheorem.MachineTranslationTable.tableBits
def OAI.UniqueGamesTheorem.MachineTranslationTable.forwardComposition line 130
def OAI.UniqueGamesTheorem.MachineTranslationTable.computableInPolyTime line 138
Source documentation
A total actual polynomial-time machine, including on malformed input words. The record retains the literal composed machine, without a cast of its machine field when simplifying the two reversals in the semantic output.
```
noncomputable def computableInPolyTime (s : Nat) :
    TM2ComputableInPolyTime (id : List Bool → List Bool) id (output s) where
…
```
Mentions: OAI.UniqueGamesTheorem.MachineTranslationTable.output
theorem OAI.UniqueGamesTheorem.MachineTranslationTable.computation_finiteAlphabet line 146
Source documentation
All physical tapes of the actual composed machine have finite alphabets.
```
theorem computation_finiteAlphabet (s : Nat) :
    MachineFiniteAlphabet.FiniteAlphabet (computableInPolyTime s).tm := by
…
```
Mentions: OAI.UniqueGamesTheorem.MachineTranslationTable.computableInPolyTime
def OAI.UniqueGamesTheorem.MachineTranslationTable.offsetComputableInPolyTime line 157
Source documentation
The same machine, specialized to the actual offset and full-table encodings.
```
noncomputable def offsetComputableInPolyTime (s : Nat) :
    TM2ComputableInPolyTime
      (fun offset : Vector s => encodeWord (Encoding.alphabetEquiv s offset).val)
      tableBits (id : Vector s → Vector s) where
…
```
Mentions: OAI.UniqueGamesTheorem.MachineTranslationTable.tableBits