OAI/Computability/UniqueGames/Reduction/MachineTransfer.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Certified reversal and relabeling between finite alphabets

The actual TM2 machine transfers a list over a finite alphabet α to a second stack over β, reverses its order, and applies a fixed map f : α → β to each symbol. The trace has exactly input.length + 1 transitions. An explicit fallback symbol makes the push expression total, including the unused branch where the internal register is empty.

This primitive supports machine composition when intermediate stack alphabets differ. It does not yet implement the Unique Games reduction.

  1. abbrev OAI.UniqueGamesTheorem.Reduction.MachineTransfer.alphabet line 22
  2. def OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loop line 28
  3. def OAI.UniqueGamesTheorem.Reduction.MachineTransfer.machine line 35
  4. def OAI.UniqueGamesTheorem.Reduction.MachineTransfer.tapeStacks line 47
  5. def OAI.UniqueGamesTheorem.Reduction.MachineTransfer.running line 52
  6. def OAI.UniqueGamesTheorem.Reduction.MachineTransfer.halted line 56
  7. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.update_input line 60
  8. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.update_output line 66
  9. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.step_empty line 71
  10. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.step_cons line 79
  11. def OAI.UniqueGamesTheorem.Reduction.MachineTransfer.next line 88
  12. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.transfer_steps line 92

    Source documentation

    Exact actual-machine trace, for any accumulator and internal register.

    theorem transfer_steps (f : α → β) (fallback : β) (input : List α) (output : List β)
    (state : Option β) :
    (next f fallback)^[input.length + 1] (some (running f fallback input output state)) =
      some (halted f fallback (input.reverse.map f ++ output)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineTransfer.next, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.running, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.halted

  13. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.initList_eq line 109
  14. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.haltList_eq line 116
  15. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.transfer_init_steps line 123
  16. def OAI.UniqueGamesTheorem.Reduction.MachineTransfer.outputsInTime line 135
  17. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.outputsInTime_steps line 142
  18. def OAI.UniqueGamesTheorem.Reduction.MachineTransfer.computableInPolyTime line 146

    Source documentation

    A genuine finite-machine certificate with identity encodings and bound X+1.

    noncomputable def computableInPolyTime (f : α → β) (fallback : β) :
    TM2ComputableInPolyTime (id : List α → List α) (id : List β → List β)
      (fun input => input.reverse.map f) where
…
  19. def OAI.UniqueGamesTheorem.Reduction.MachineTransfer.exitAt line 166
  20. def OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt line 171
  21. def OAI.UniqueGamesTheorem.Reduction.MachineTransfer.tapesAt line 178
  22. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.tapesAt_src line 182
  23. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.tapesAt_dst line 187
  24. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.tapesAt_other line 192
  25. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.tapesAt_self line 197
  26. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.update_tapesAt_src line 201
  27. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.update_tapesAt_dst line 215
  28. def OAI.UniqueGamesTheorem.Reduction.MachineTransfer.nextAt line 226
  29. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.stepAt_empty line 231
  30. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.stepAt_cons line 245
  31. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.transferAt_steps line 263

    Source documentation

    Placement-aware exact transfer, preserving all ambient state and other tapes. The optional exit label is reached in the same final empty-pop transition.

    theorem transferAt_steps (src dst : K) (distinct : src ≠ dst)
    (f : Γ src → Γ dst) (fallback : Γ dst) (loopLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt Γ Λ (σ × Option (Γ dst)))
    (atLoop : program loopLabel = loopAt src dst f fallback loopLabel exit)
    (base : (k : K) → List (Γ k)) (input : List (Γ src)) (output : List (Γ dst))
    (ambient : σ) (register : Option (Γ dst)) :
    (nextAt dst program)^[input.length + 1]
      (some ⟨some loopLabel, (ambient, register), tapesAt src dst base input output⟩) =
      some ⟨exit, (ambient, none), tapesAt src dst base [] (input.reverse.map f ++ output)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.nextAt, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.tapesAt

  32. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransfer.transferAt_fromTapes line 288

    Source documentation

    The same trace starting with an arbitrary actual ambient tape family.

    theorem transferAt_fromTapes (src dst : K) (distinct : src ≠ dst)
    (f : Γ src → Γ dst) (fallback : Γ dst) (loopLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt Γ Λ (σ × Option (Γ dst)))
    (atLoop : program loopLabel = loopAt src dst f fallback loopLabel exit)
    (base : (k : K) → List (Γ k)) (ambient : σ) (register : Option (Γ dst)) :
    (nextAt dst program)^[(base src).length + 1]
      (some ⟨some loopLabel, (ambient, register), base⟩) =
      some ⟨exit, (ambient, none),
        tapesAt src dst base [] ((base src).reverse.map f ++ base dst)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.nextAt, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.tapesAt

  33. def OAI.UniqueGamesTheorem.Reduction.MachineTransfer.transferAtInTime line 303

    Source documentation

    A timed execution witness suitable for composing this bridge with other phases of the same actual transition system.

    def transferAtInTime (src dst : K) (distinct : src ≠ dst)
    (f : Γ src → Γ dst) (fallback : Γ dst) (loopLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt Γ Λ (σ × Option (Γ dst)))
    (atLoop : program loopLabel = loopAt src dst f fallback loopLabel exit)
    (base : (k : K) → List (Γ k)) (ambient : σ) (register : Option (Γ dst)) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some loopLabel, (ambient, register), base⟩
      (some ⟨exit, (ambient, none),
        tapesAt src dst base [] ((base src).reverse.map f ++ base dst)⟩)
      ((base src).length + 1) where
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.tapesAt