MachineSubstitution.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

A certified machine for fixed symbol substitution

For a fixed table emit : Bool → List Bool, this actual finite TM2 machine produces (input.flatMap emit).reverse in exactly 2 * input.length + 1 transitions. It has one input-pop transition and one literal-emission transition per input symbol, followed by the final empty pop. Literal emission is a fixed finite statement; its maximum number of pushes depends only on emit.

This is a machine primitive, not a runtime theorem for the Unique Games reduction.

def OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.pushWord line 28

Source documentation

Push a fixed word in its listed order, then execute the continuation.

def pushWord (dst : K) : List (Γ dst) → TM2.Stmt Γ Λ σ → TM2.Stmt Γ Λ σ
  | [], continuation => continuation
  | symbol :: word, continuation =>
      .push dst (fun _ => symbol) (pushWord dst word continuation)

/-- Literal pushes preserve the state and every other tape. -/

theorem OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.stepAux_pushWord line 34

Source documentation

Literal pushes preserve the state and every other tape.

theorem stepAux_pushWord (dst : K) (word : List (Γ dst))
    (continuation : TM2.Stmt Γ Λ σ) (state : σ) (tapes : ∀ k, List (Γ k)) :
    TM2.stepAux (pushWord dst word continuation) state tapes =
      TM2.stepAux continuation state
        (Function.update tapes dst (word.reverse ++ tapes dst)) := by
…

Mentions: OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.pushWord

theorem OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.statementPushBound_pushWord line 48
def OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.loop line 60
def OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.program line 66
def OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.machine line 71
def OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.maxEmission line 83
Source documentation
The fixed maximum word length bounds pushes in each emitted statement.
```
def maxEmission (emit : Bool → List Bool) : Nat :=
…
```
theorem OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.statementPushBound_le line 86
theorem OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.programPushBound_le line 96
def OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.tapeStacks line 106
def OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.running line 109
def OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.emitting line 113
def OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.halted line 117
theorem OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.update_input line 120
theorem OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.update_output line 125
theorem OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.step_empty line 130
theorem OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.step_cons line 137
theorem OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.step_emit line 147
Source documentation
Emission does not depend on the register; the symbol is held in the control label.
```
theorem step_emit (emit : Bool → List Bool) (symbol : Bool)
    (input output : List Bool) (state : Option Bool) :
    (machine emit).step (emitting emit symbol input output state) =
      some (running emit input ((emit symbol).reverse ++ output) state) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.machine, OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.emitting, OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.running
def OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.next line 162
theorem OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.two_steps_cons line 166
theorem OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.substitution_steps line 176
Source documentation
Exact execution, including an arbitrary initial accumulator and register.
```
theorem substitution_steps (emit : Bool → List Bool)
    (input output : List Bool) (state : Option Bool) :
    (next emit)^[2 * input.length + 1] (some (running emit input output state)) =
      some (halted emit ((input.flatMap emit).reverse ++ output)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.next, OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.running, OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.halted
theorem OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.initList_eq line 191
theorem OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.haltList_eq line 198
theorem OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.substitution_init_steps line 203
def OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.outputsInTime line 209
theorem OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.outputsInTime_steps line 216

def OAI.UniqueGamesTheorem.Reduction.MachineSubstitution.computableInPolyTime line 220

Source documentation

A finite-machine polynomial-time certificate for reversed fixed substitution.

noncomputable def computableInPolyTime (emit : Bool → List Bool) :
    TM2ComputableInPolyTime (id : List Bool → List Bool) id
      (fun input => (input.flatMap emit).reverse) where
…