OAI/Computability/UniqueGames/Machines/MachineUniformRun.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Whole-instance uniform copying: exact physical header arithmetic, repeated body emission, actual cleanup, and a polynomial bound in the input codec length.

  1. def OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.outputBits line 18
  2. def OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.afterScale line 21
  3. def OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.afterEmit line 25
  4. def OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.scaleInTime line 29
  5. theorem OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.repeated_template line 51
  6. theorem OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.template_output line 62
  7. theorem OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.template_copiedLength line 74
  8. def OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.emitInTime line 82
  9. def OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.prefixPolynomial line 99
  10. theorem OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.input_length line 102
  11. def OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.prefixInTime line 106
  12. def OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.timePolynomial line 123
  13. theorem OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.haltList_eq line 126
  14. def OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.finishStartInTime line 134
  15. def OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.outputInTime line 146

    Source documentation

    The complete actual run, including the physical cleanup and output reversal.

    noncomputable def outputInTime (C n q Q : Nat) (body : List Bool) :
    TM2OutputsInTime (machine C) (encodeWords [n, q, Q] ++ body)
      (some (outputBits C n q Q body))
      ((timePolynomial C).eval (encodeWords [n, q, Q] ++ body).length) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.outputBits, OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.timePolynomial

  16. def OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.computation line 181

    Source documentation

    A fixed actual program works for every game and every alphabet size.

    noncomputable def computation {q : Nat} (C : Nat) (hC : 0 < C) :
    TM2ComputableInPolyTime gameBits gameBits (UniformTarget.construct (q := q) C hC) where
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.UniformTarget.construct

  17. theorem OAI.UniqueGamesTheorem.Explicit.MachineUniformRun.finiteAlphabet line 204