OAI/Computability/UniqueGames/Machines/MachineLazyTable.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

The actual whole-table lazy-graph machine, with fixed positive old degree. All unbounded counts and addresses reside on unary tapes.

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.Tape line 20
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.Tape.enumList line 25
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.Tape.enumList_getElem?_ctorIdx_eq line 29
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.Tape.enumList_nodup line 33
  5. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.(instance at line 35) line 35
  6. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.State line 39
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.clean line 41
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.clean_pair line 44
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.splitRoles line 47
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.splitView line 48
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.dummyRoles line 52
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.dummyView line 53
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.oldRoles line 57
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.splitRoles_left line 61
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.splitRoles_right line 64
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.dummyRoles_left line 67
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.dummyRoles_right line 70
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.oldRoles_injective line 73
  19. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.Label line 75
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.program line 85
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.frame line 122
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.initialTapes line 127
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.loopTapes line 129
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.finalTapes line 134
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.joinTrace line 136
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.dummyTrace line 142

    Source documentation

    Lift the actual dummy-block routine into the full program and account for the exact preserved frame. The tail and relation are cleared in the next phase.

    theorem dummyTrace (d : Nat) (positive : 0 < d) (base : Tape → List Bool) (v e : Nat)
    (ht : base .tail = encodeWord v) (he : base .reverse = encodeWord e)
    (hr : base .relation = []) (hb : base .rowBuffer = []) (hs : base .scratch = []) :
    (advance (TM2.step (program d positive)))^[MachineDummyRows.steps v e (base .output) d + 1]
      (some ⟨some (.dummy (MachineDummyRows.start d)), clean d positive, base⟩) =
      some ⟨some .clearDummyTail, clean d positive,
        Function.update (Function.update (Function.update base .reverse (encodeWord (e + d)))
          .relation MachineDummyRows.trueBits)
          .output (base .output ++ MachineDummyRows.rowsBits v e d)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.start, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.trueBits, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDummyRows.rowsBits

  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.oldTrace line 171
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.prefixSteps line 203
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.prefixTrace line 206
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.vertexBlock line 288
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.bodySteps line 292
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.frame_old_empty line 298
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.bodyTrace line 306

    Source documentation

    One entire vertex body: preserve-copy its tail, append the real dummy block, clear its temporary fields, transform all old rows, and increment both counters by actual pushes. The caller supplies no execution premise.

    theorem bodyTrace {n m : Nat} (d : Nat) (positive : 0 < d) (input : List Bool)
    (left v : Nat) (rows : Fin d → GraphTables.DartRow n m) (rest output : List Bool) :
    (advance (TM2.step (program d positive)))^[bodySteps d v rows output]
      (some ⟨some .copyVertexFirst, clean d positive,
        loopTapes d input n m left v (MachineLazyRows.recordsInput (List.ofFn rows) ++ rest) output⟩) =
      some ⟨some .guard, clean d positive,
        loopTapes d input n m left (v + 1) rest (output ++ vertexBlock d v rows)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.bodySteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.loopTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyRows.recordsInput, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.vertexBlock

  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.drainPhase line 418
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.finishSteps line 429
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.finishTrace line 431
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.remaining line 486
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.remaining_zero line 488
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.remaining_done line 489
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.remaining_cons line 491
  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.inputBlocks line 497
  42. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.outputBlocks line 500
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.vertexBlock_codec line 503
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.encodeWords_flatMap line 509
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.inputBlocks_codec line 515
  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.outputBlocks_codec line 522
  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.input_table_codec line 528
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.output_table_codec line 539
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.loopSteps line 551
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.loopTrace line 560

    Source documentation

    Induction over the actual unary fuel and the actual stored vertex order.

    theorem loopTrace {n d : Nat} (table : PortTables.Table n d) (positive : 0 < d)
    (input : List Bool) (count r : Nat) (hsum : r + count = n) (output : List Bool) :
    (advance (TM2.step (program d positive)))^[loopSteps table r count output]
      (some ⟨some .guard, clean d positive,
        loopTapes d input n (n * d) count r (inputBlocks table (remaining n r)) output⟩) =
      some ⟨none, clean d positive,
        finalTapes input (output ++ outputBlocks table (remaining n r))⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.loopSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.loopTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.inputBlocks, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.remaining, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.finalTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.outputBlocks

  51. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.totalSteps line 601
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.tableTrace line 607

    Source documentation

    The full table execution, including all headers, all dummy and moving rows, and complete work-tape cleanup, in the existing exact Boolean codec.

    theorem tableTrace {n d : Nat} (table : PortTables.Table n d) (positive : 0 < d) :
    (advance (TM2.step (program d positive)))^[totalSteps table]
      (some ⟨some (.split .copyFirst), clean d positive, initialTapes (PortTables.tableBits table)⟩) =
      some ⟨none, clean d positive,
        finalTapes (PortTables.tableBits table)
          (PortTables.tableBits (PreprocessingOverlayTables.lazy table))⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.totalSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.finalTapes

  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.dummyRows_length_le line 622
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.bodySteps_le line 635

    Source documentation

    A uniform bound for the actual vertex body, using the complete output size as a cap on its existing prefix. Degree is a fixed program parameter.

    theorem bodySteps_le {n d : Nat} (rows : Fin d → GraphTables.DartRow n (n * d))
    (v L : Nat) (output : List Bool) (hv : v ≤ n) (hn : n ≤ L) (hm : n * d ≤ L)
    (ho : output.length ≤ 20000 * (L + 1) ^ 2) :
    bodySteps d v rows output ≤ 1000000 * (d + 1) ^ 3 * (L + 1) ^ 2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.bodySteps

  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.output_length_le line 756
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.loopSteps_le line 773
  57. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.timePolynomial line 805
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.timePolynomial_eval line 808
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.totalSteps_le line 812
  60. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.machine line 843
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.machine_alphabet_finite line 854
  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.initial_configuration line 860
  63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.finalTapes_input line 869
  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.finalTapes_output line 870
  65. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.finalTapes_work_empty line 872
  66. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.machineInTime line 878

    Source documentation

    A full actual finite-machine execution with a fixed-degree polynomial budget, the exact lazy-table output, preserved original input, and clean work.

    def machineInTime {n d : Nat} (table : PortTables.Table n d) (positive : 0 < d) :
    StateTransition.EvalsToInTime (machine d positive).step
      (initList (machine d positive) (PortTables.tableBits table))
      (some ⟨none, clean d positive, finalTapes (PortTables.tableBits table)
        (PortTables.tableBits (PreprocessingOverlayTables.lazy table))⟩)
      ((timePolynomial d).eval (PortTables.tableBits table).length) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.finalTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLazyTable.timePolynomial