OAI/Computability/MaxCut/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.MaxCutGames.Foundations.Complexity.MachineLazyTable.Tape line 14
  2. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.Tape.enumList line 19
  3. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.Tape.enumList_getElem?_ctorIdx_eq line 23
  4. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.Tape.enumList_nodup line 27
  5. instance OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.(instance at line 29) line 29
  6. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.State line 33
  7. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.clean line 35
  8. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.clean_pair line 38
  9. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.splitRoles line 41
  10. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.splitView line 42
  11. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.dummyRoles line 46
  12. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.dummyView line 47
  13. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.oldRoles line 51
  14. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.splitRoles_left line 55
  15. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.splitRoles_right line 58
  16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.dummyRoles_left line 61
  17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.dummyRoles_right line 64
  18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.oldRoles_injective line 67
  19. inductive OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.Label line 69
  20. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.program line 79
  21. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.frame line 116
  22. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.initialTapes line 121
  23. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.loopTapes line 123
  24. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.finalTapes line 128
  25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.joinTrace_inline_MachineLazyTable line 130
  26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.dummyTrace line 136

    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.MaxCutGames.Foundations.Complexity.MachineLazyTable.Tape, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.steps, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.start, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.clean, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.trueBits, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowsBits

  27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.oldTrace line 165
  28. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.prefixSteps line 197
  29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.prefixTrace line 200
  30. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.vertexBlock line 282
  31. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.bodySteps line 286
  32. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.frame_old_empty line 292
  33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.bodyTrace line 300

    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.MaxCutGames.Foundations.Complexity.MachineLazyTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.bodySteps, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.clean, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.loopTapes, OAI.MaxCutGames.Foundations.Complexity.MachineLazyRows.recordsInput, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.vertexBlock

  34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.drainPhase line 412
  35. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.finishSteps line 423
  36. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.finishTrace line 425
  37. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.remaining line 480
  38. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.remaining_zero line 482
  39. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.remaining_done line 483
  40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.remaining_cons line 485
  41. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.inputBlocks line 491
  42. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.outputBlocks line 494
  43. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.vertexBlock_codec line 497
  44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.encodeWords_flatMap_inline_MachineLazyTable line 503
  45. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.inputBlocks_codec line 509
  46. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.outputBlocks_codec line 516
  47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.input_table_codec line 522
  48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.output_table_codec line 533
  49. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.loopSteps line 545
  50. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.loopTrace line 554

    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.MaxCutGames.Foundations.Complexity.MachineLazyTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.loopSteps, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.clean, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.loopTapes, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.inputBlocks, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.remaining, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.finalTapes, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.outputBlocks

  51. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.totalSteps line 595
  52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.tableTrace line 601

    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.MaxCutGames.Foundations.Complexity.MachineLazyTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.totalSteps, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.clean, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.initialTapes, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.finalTapes

  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.dummyRows_length_le_inline_MachineLazyTable line 616
  54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.bodySteps_le line 629

    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.MaxCutGames.Foundations.Complexity.MachineLazyTable.bodySteps

  55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.output_length_le line 750
  56. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.loopSteps_le line 767
  57. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.timePolynomial line 799
  58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.timePolynomial_eval line 802
  59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.totalSteps_le line 806
  60. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.machine line 837
  61. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.machine_alphabet_finite line 848
  62. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.initial_configuration line 854
  63. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.finalTapes_input line 863
  64. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.finalTapes_output line 864
  65. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.finalTapes_work_empty line 866
  66. def OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.machineInTime line 872

    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.MaxCutGames.Foundations.Complexity.MachineLazyTable.machine, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.clean, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.finalTapes, OAI.MaxCutGames.Foundations.Complexity.MachineLazyTable.timePolynomial