OAI/Computability/UniqueGames/Machines/MachineLogCounter.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

An actual logarithmic-round counter. Unary input is stripped to a raw tally; each positive round emits one tally and halves the remaining input by pairing symbols. The zero input emits one round explicitly. All tapes except the canonical output are empty at termination.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.bitLength line 19
  2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.bitLength_zero line 21
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.bitLength_positive line 23
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.bitLength_half line 26
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.increments line 33
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.increments_true line 36
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.increments_half line 39
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.increments_false line 43
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.coreTime line 48
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.coreTime_zero line 53
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.coreTime_positive line 55
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.coreTime_bound line 59
  13. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.Alphabet line 69
  14. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.State line 70
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.initialState line 72
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.rawTapes line 74
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.update_input line 79
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.update_scratch line 84
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.update_output line 89
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.stripLoop line 94
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.guardLoop line 100
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.halfLoop line 109
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.program line 118
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.machine line 125
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.configuration line 136
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.next line 140
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.stripStep_true line 142
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.stripStep_false line 150
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.stripTrace line 158
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.halfStep_nil line 174
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.halfStep_false line 182
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.halfStep_true line 191
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.halfTrace line 201

    Source documentation

    A parity bit implements division by two using actual pop/push transitions.

    theorem halfTrace (n m : Nat) (output : List Bool) (parity started : Bool)
    (register : Option Bool) :
    next^[n + 1] (some (configuration (some 3) ((parity, started), register)
      (List.replicate n true) (List.replicate m true) output)) =
      some (configuration (some 4) ((false, started), none) []
        (List.replicate (m + (n + if parity then 1 else 0) / 2) true) output) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.next, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.configuration

  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.restoreTrace line 233
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.guardStep_zero line 250
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.guardStep_positive line 263
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.coreTrace line 276

    Source documentation

    The halving rounds are actual guard, scan, and restoration executions.

    theorem coreTrace (n : Nat) (output : List Bool) (started : Bool) :
    next^[coreTime n] (some (configuration (some 2) ((false, started), none)
      (List.replicate n true) [] output)) =
      some (configuration none initialState [] []
        (List.replicate (increments n started) true ++ output)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.next, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.coreTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.configuration, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.initialState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.increments

  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.initList_eq line 309
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.haltList_eq line 317
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.initialStep line 325
  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.totalTime line 334
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.totalTime_bound line 336
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.machineTrace line 341
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.outputsInTime line 356
  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.computableInPolyTime line 364

    Source documentation

    A genuine finite-machine certificate for unary log2(n)+1; its linear polynomial is measured in the actual encoded input length.

    noncomputable def computableInPolyTime :
    TM2ComputableInPolyTime encodeWord encodeWord (fun n => n.log2 + 1) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord