OAI/Computability/MaxCut/Machines/MachineCopy.lean

GitHub source file

81 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.

  1. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCopy.Alphabet line 12
  2. def OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkLoop line 15

    Source documentation

    Drain one tape into two reverse-order accumulators.

    def forkLoop (source left right : K) (fallback : β) (loopLabel : Λ) (exit : Option Λ) :
    TM2.Stmt (Alphabet (K := K) β) Λ (σ × Option β) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCopy.Alphabet

  3. def OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkTapes line 23
  4. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkTapes_source line 28
  5. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkTapes_left line 34
  6. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkTapes_right line 39
  7. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkTapes_self line 44
  8. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCopy.update_fork_source_inline_MachineCopy line 48
  9. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCopy.update_fork_left_inline_MachineCopy line 62
  10. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCopy.update_fork_right_inline_MachineCopy line 73
  11. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkStep_empty line 79
  12. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkStep_cons line 95
  13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkTrace line 114

    Source documentation

    Each symbol and the final empty test take one actual transition.

    theorem forkTrace (source left right : K)
    (sourceLeft : source ≠ left) (sourceRight : source ≠ right) (leftRight : left ≠ right)
    (fallback : β) (loopLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K) β) Λ (σ × Option β))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCopy.Alphabet

  14. def OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkInTime line 141
  15. def OAI.MaxCutGames.Foundations.Complexity.MachineCopy.drainedTapes line 161
  16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCopy.restoredTapes line 164
  17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCopy.copyTrace line 182
  18. def OAI.MaxCutGames.Foundations.Complexity.MachineCopy.copyInTime line 224

    Source documentation

    A timed witness whose stored step count is the exact two-loop trace length.

    def copyInTime (source destination scratch : K)
    (sourceDestination : source ≠ destination) (sourceScratch : source ≠ scratch)
    (destinationScratch : destination ≠ scratch)
    (fallback : β) (firstLabel secondLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K) β) Λ (σ × Option β))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCopy.Alphabet

  19. def OAI.MaxCutGames.Reduction.MachineSubstitution.pushWord line 270

    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. -/
  20. theorem OAI.MaxCutGames.Reduction.MachineSubstitution.stepAux_pushWord line 276

    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.MaxCutGames.Reduction.MachineSubstitution.pushWord

  21. theorem OAI.MaxCutGames.Reduction.MachineSubstitution.statementPushBound_pushWord line 290
  22. def OAI.MaxCutGames.Reduction.MachineSubstitution.loop line 302
  23. def OAI.MaxCutGames.Reduction.MachineSubstitution.program line 308
  24. def OAI.MaxCutGames.Reduction.MachineSubstitution.machine line 313
  25. def OAI.MaxCutGames.Reduction.MachineSubstitution.maxEmission line 325

    Source documentation

    The fixed maximum word length bounds pushes in each emitted statement.

    def maxEmission (emit : Bool → List Bool) : Nat :=
…
  26. theorem OAI.MaxCutGames.Reduction.MachineSubstitution.statementPushBound_le line 328
  27. theorem OAI.MaxCutGames.Reduction.MachineSubstitution.programPushBound_le line 338
  28. def OAI.MaxCutGames.Reduction.MachineSubstitution.tapeStacks line 348
  29. def OAI.MaxCutGames.Reduction.MachineSubstitution.running line 351
  30. def OAI.MaxCutGames.Reduction.MachineSubstitution.emitting line 355
  31. def OAI.MaxCutGames.Reduction.MachineSubstitution.halted line 359
  32. theorem OAI.MaxCutGames.Reduction.MachineSubstitution.update_input_inline_MachineSubstitution line 362
  33. theorem OAI.MaxCutGames.Reduction.MachineSubstitution.update_output_inline_MachineSubstitution line 367
  34. theorem OAI.MaxCutGames.Reduction.MachineSubstitution.step_empty line 372
  35. theorem OAI.MaxCutGames.Reduction.MachineSubstitution.step_cons line 379
  36. theorem OAI.MaxCutGames.Reduction.MachineSubstitution.step_emit line 389

    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.MaxCutGames.Reduction.MachineSubstitution.machine, OAI.MaxCutGames.Reduction.MachineSubstitution.emitting, OAI.MaxCutGames.Reduction.MachineSubstitution.running

  37. def OAI.MaxCutGames.Reduction.MachineSubstitution.next line 403
  38. theorem OAI.MaxCutGames.Reduction.MachineSubstitution.two_steps_cons line 407
  39. theorem OAI.MaxCutGames.Reduction.MachineSubstitution.substitution_steps line 417

    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.MaxCutGames.Reduction.MachineSubstitution.next, OAI.MaxCutGames.Reduction.MachineSubstitution.running, OAI.MaxCutGames.Reduction.MachineSubstitution.halted

  40. theorem OAI.MaxCutGames.Reduction.MachineSubstitution.initList_eq line 432
  41. theorem OAI.MaxCutGames.Reduction.MachineSubstitution.haltList_eq line 439
  42. theorem OAI.MaxCutGames.Reduction.MachineSubstitution.substitution_init_steps line 444
  43. def OAI.MaxCutGames.Reduction.MachineSubstitution.outputsInTime line 450
  44. theorem OAI.MaxCutGames.Reduction.MachineSubstitution.outputsInTime_steps line 457
  45. def OAI.MaxCutGames.Reduction.MachineSubstitution.computableInPolyTime line 461

    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
…
  46. def OAI.MaxCutGames.Reduction.MachineReverse.loop line 484
  47. def OAI.MaxCutGames.Reduction.MachineReverse.machine line 490
  48. def OAI.MaxCutGames.Reduction.MachineReverse.tapeStacks line 501
  49. def OAI.MaxCutGames.Reduction.MachineReverse.running line 504
  50. def OAI.MaxCutGames.Reduction.MachineReverse.halted line 507
  51. theorem OAI.MaxCutGames.Reduction.MachineReverse.update_input_inline_MachineReverse line 510
  52. theorem OAI.MaxCutGames.Reduction.MachineReverse.update_output_inline_MachineReverse line 515
  53. theorem OAI.MaxCutGames.Reduction.MachineReverse.step_empty line 521

    Source documentation

    Popping an empty input resets the internal state to none before halting.

    theorem step_empty (output : List Bool) (state : Option Bool) :
    machine.step (running [] output state) = some (halted output) := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineReverse.running, OAI.MaxCutGames.Reduction.MachineReverse.halted

  54. theorem OAI.MaxCutGames.Reduction.MachineReverse.step_cons line 529

    Source documentation

    One transition moves the head symbol from the input onto the output.

    theorem step_cons (head : Bool) (input output : List Bool) (state : Option Bool) :
    machine.step (running (head :: input) output state) =
      some (running input (head :: output) (some head)) := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineReverse.running

  55. def OAI.MaxCutGames.Reduction.MachineReverse.next line 537
  56. theorem OAI.MaxCutGames.Reduction.MachineReverse.reverse_steps line 541

    Source documentation

    An exact transition trace, with arbitrary initial accumulator and state.

    theorem reverse_steps (input output : List Bool) (state : Option Bool) :
    next^[input.length + 1] (some (running input output state)) =
      some (halted (input.reverse ++ output)) := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineReverse.next, OAI.MaxCutGames.Reduction.MachineReverse.running, OAI.MaxCutGames.Reduction.MachineReverse.halted

  57. theorem OAI.MaxCutGames.Reduction.MachineReverse.initList_eq line 555
  58. theorem OAI.MaxCutGames.Reduction.MachineReverse.haltList_eq line 562
  59. theorem OAI.MaxCutGames.Reduction.MachineReverse.reverse_init_steps line 567

    Source documentation

    The exact trace starts and ends at the standard encoded TM2 configurations.

    theorem reverse_init_steps (input : List Bool) :
    next^[input.length + 1] (some (initList machine input)) =
      some (haltList machine input.reverse) := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineReverse.next, OAI.MaxCutGames.Reduction.MachineReverse.machine

  60. def OAI.MaxCutGames.Reduction.MachineReverse.outputsInTime line 573
  61. theorem OAI.MaxCutGames.Reduction.MachineReverse.outputsInTime_steps line 579
  62. def OAI.MaxCutGames.Reduction.MachineReverse.computableInPolyTime line 583

    Source documentation

    Actual finite-machine polynomial-time computability, with identity encodings.

    noncomputable def computableInPolyTime :
    TM2ComputableInPolyTime (id : List Bool → List Bool) id List.reverse where
…
  63. def OAI.MaxCutGames.Foundations.Complexity.MachineControl.configuration line 609
  64. def OAI.MaxCutGames.Foundations.Complexity.MachineControl.statement line 615
  65. theorem OAI.MaxCutGames.Foundations.Complexity.MachineControl.stepAux_simulation line 630
  66. def OAI.MaxCutGames.Foundations.Complexity.MachineControl.program line 657
  67. theorem OAI.MaxCutGames.Foundations.Complexity.MachineControl.step_simulation line 662

    Source documentation

    The renamed program is conjugate to the original transition function, including the halted configuration.

    theorem step_simulation (labels : Λ ≃ Λ') (states : σ ≃ σ')
    (source : Λ → Stmt Γ Λ σ) (c : Cfg Γ Λ σ) :
    step (program labels states source) (configuration labels states c) =
      (step source c).map (configuration labels states) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineControl.program, OAI.MaxCutGames.Foundations.Complexity.MachineControl.configuration

  68. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineStackSwap.Alphabet line 689
  69. def OAI.MaxCutGames.Foundations.Complexity.MachineStackSwap.tapes line 692
  70. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStackSwap.tapes_first line 698
  71. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStackSwap.tapes_second line 700
  72. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStackSwap.tapes_third line 702
  73. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStackSwap.tapes_involutive line 705
  74. def OAI.MaxCutGames.Foundations.Complexity.MachineStackSwap.configuration line 710
  75. def OAI.MaxCutGames.Foundations.Complexity.MachineStackSwap.statement line 716
  76. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStackSwap.tapes_update_first line 733
  77. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStackSwap.tapes_update_second line 745
  78. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStackSwap.tapes_update_third line 757
  79. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStackSwap.stepAux_simulation line 769
  80. def OAI.MaxCutGames.Foundations.Complexity.MachineStackSwap.program line 817
  81. theorem OAI.MaxCutGames.Foundations.Complexity.MachineStackSwap.step_simulation line 820