OAI/Computability/MaxCut/Machines/MachineSubdivisionTableRead.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

Actual execution of the subdivision controller's full-table reader. The reader consumes exactly the fixed number of zero-delimited table entries, retains the unread input suffix, and reverses the saved table into forward order. No table entry is stored in finite control; only the number of delimiters is.

  1. def OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.tapes line 22
  2. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.tapes_input line 25
  3. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.tapes_reverse line 28
  4. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.update_input_inline_MachineSubdivisionTableRead line 31
  5. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.update_reverse_inline_MachineSubdivisionTableRead line 37
  6. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.step_true line 43
  7. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.step_false line 53
  8. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.readWordTrace line 65

    Source documentation

    One encoded entry consumes its final delimiter in the same transition that increments the finite completed-entry counter.

    theorem readWordTrace (q : Nat) (completed : Fin (q + 1)) (valid : completed.val < q)
    (base : Tape → List Bool) (value : Nat) (input reversed : List Bool)
    (ambient : Unit × Unit) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program q)))^[value + 1]
      (some ⟨some (.readTable completed), (ambient, register),
        tapes base (encodeWord value ++ input) reversed⟩) =
      some ⟨some (.readTable ⟨completed.val + 1, by omega⟩), (ambient, none),
        tapes base input ((encodeWord value).reverse ++ reversed)⟩ := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.tapes

  9. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.readWordsTrace line 87

    Source documentation

    Read a suffix of the q-entry table, stopping before any following data.

    theorem readWordsTrace (q : Nat) (words : List Nat) (completed : Fin (q + 1))
    (complete : completed.val + words.length = q) (base : Tape → List Bool)
    (suffix reversed : List Bool) (ambient : Unit × Unit) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program q)))^[(encodeWords words).length + 1]
      (some ⟨some (.readTable completed), (ambient, register),
        tapes base (encodeWords words ++ suffix) reversed⟩) =
      some ⟨some .reverseTable, (ambient, none),
        tapes base suffix ((encodeWords words).reverse ++ reversed)⟩ := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.tapes

  10. def OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.finalTapes line 117
  11. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.finalTapes_other line 120
  12. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.finalTapes_input line 125
  13. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.finalTapes_reverse line 128
  14. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.finalTapes_permutation line 131
  15. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.tableTrace line 136

    Source documentation

    Full exact table phase: read q delimited entries and reverse the physical saved stack, arriving at the actual row-emission label.

    theorem tableTrace (q : Nat) (words : List Nat) (length : words.length = q)
    (base : Tape → List Bool) (suffix : List Bool)
    (ambient : Unit × Unit) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program q)))^[2 * (encodeWords words).length + 2]
      (some ⟨some (.readTable 0), (ambient, register),
        tapes base (encodeWords words ++ suffix) []⟩) =
      some ⟨some (rowEntry q), (ambient, none), finalTapes base suffix (encodeWords words)⟩ := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.tapes, OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.finalTapes

  16. def OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.tableInTime line 165

    Source documentation

    Timed witness for the actual controller, with a fixed alphabet-dependent bound on its full forward table. Other row fields and unread input are preserved.

    def tableInTime {q : Nat} (table : Target.PermutationTable q)
    (base : Tape → List Bool) (suffix : List Bool)
    (ambient : Unit × Unit) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step (program q))
      ⟨some (.readTable 0), (ambient, register),
        tapes base (encodeWords (tableWords table) ++ suffix) []⟩
      (some ⟨some (rowEntry q), (ambient, none),
        finalTapes base suffix (encodeWords (tableWords table))⟩)
      (2 * (q * (q + 1)) + 2) where
…

    Mentions: OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.tapes, OAI.MaxCutGames.Explicit.MachineSubdivisionTableRead.finalTapes

  17. def OAI.MaxCutGames.Explicit.MachineSubdivisionBody.tableBits line 197
  18. structure OAI.MaxCutGames.Explicit.MachineSubdivisionBody.Ready line 200
  19. def OAI.MaxCutGames.Explicit.MachineSubdivisionBody.afterU line 209
  20. def OAI.MaxCutGames.Explicit.MachineSubdivisionBody.afterV line 213
  21. def OAI.MaxCutGames.Explicit.MachineSubdivisionBody.afterTable line 217
  22. def OAI.MaxCutGames.Explicit.MachineSubdivisionBody.rowPayload line 221
  23. def OAI.MaxCutGames.Explicit.MachineSubdivisionBody.afterRows line 226
  24. def OAI.MaxCutGames.Explicit.MachineSubdivisionBody.afterDrainU line 231
  25. def OAI.MaxCutGames.Explicit.MachineSubdivisionBody.afterDrainV line 235
  26. def OAI.MaxCutGames.Explicit.MachineSubdivisionBody.afterDrainTable line 239
  27. def OAI.MaxCutGames.Explicit.MachineSubdivisionBody.incrementTapes line 243
  28. def OAI.MaxCutGames.Explicit.MachineSubdivisionBody.bodyResult line 249
  29. def OAI.MaxCutGames.Explicit.MachineSubdivisionBody.bodyBudget line 253
  30. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionBody.rowField_ne_scratch_inline_MachineSubdivisionBody line 262
  31. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionBody.rowField_ne_accumulator_inline_MachineSubdivisionBody line 265
  32. def OAI.MaxCutGames.Explicit.MachineSubdivisionBody.incrementInTime line 268
  33. def OAI.MaxCutGames.Explicit.MachineSubdivisionBody.bodyInTime line 279

    Source documentation

    Complete actual .startU → .guard execution, without a phase-run premise.

    def bodyInTime {q : Nat} (base : Tape → List Bool) (u v : Nat)
    (table : Target.PermutationTable q) (suffix : List Bool)
    (ready : Ready base u v table suffix) :
    StateTransition.EvalsToInTime (TM2.step (program q))
      ⟨some .startU, initialState, base⟩
      (some ⟨some .guard, initialState, bodyResult base u v table suffix⟩)
      (bodyBudget base u v table suffix) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineSubdivisionBody.Ready, OAI.MaxCutGames.Explicit.MachineSubdivisionBody.bodyResult, OAI.MaxCutGames.Explicit.MachineSubdivisionBody.bodyBudget

  34. def OAI.MaxCutGames.Explicit.MachineSubdivisionLoopFrame.bodyBits line 355
  35. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionLoopFrame.bodyBits_nil line 358
  36. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionLoopFrame.bodyBits_cons line 360
  37. def OAI.MaxCutGames.Explicit.MachineSubdivisionLoopFrame.identityBits line 367
  38. def OAI.MaxCutGames.Explicit.MachineSubdivisionLoopFrame.rowBits line 370
  39. def OAI.MaxCutGames.Explicit.MachineSubdivisionLoopFrame.outputRows line 377
  40. def OAI.MaxCutGames.Explicit.MachineSubdivisionLoopFrame.frame line 381
  41. def OAI.MaxCutGames.Explicit.MachineSubdivisionLoopFrame.afterGuard line 392
  42. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionLoopFrame.frame_prepared line 396
  43. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionLoopFrame.guard_cons line 403
  44. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionLoopFrame.guard_nil line 424
  45. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionLoopFrame.ready line 441
  46. def OAI.MaxCutGames.Explicit.MachineSubdivisionBodySpec.resultTapes line 467
  47. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionBodySpec.bodyResult_eq line 478

    Source documentation

    Every tape at the body boundary, including all preserved headers and counters.

    theorem bodyResult_eq {q : Nat} (base : Tape → List Bool) (u v : Nat)
    (table : Target.PermutationTable q) (suffix : List Bool)
    (_ready : Ready base u v table suffix) :
    bodyResult base u v table suffix = resultTapes base u v table suffix := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineSubdivisionBodySpec.resultTapes

  48. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionBodySpec.result_input line 488
  49. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionBodySpec.result_locals line 495
  50. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionBodySpec.result_accumulator line 506
  51. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionBodySpec.encodeWord_succ line 514
  52. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionBodySpec.result_indices line 517
  53. def OAI.MaxCutGames.Explicit.MachineSubdivisionBodySpec.rowBits line 533

    Source documentation

    Four whole rows, with the final table already in left-to-right orientation.

    def rowBits {q : Nat} (u middle first last v : Nat) (table : Target.PermutationTable q) :
    List Bool :=
…
  54. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionBodySpec.rowPayload_eq line 541
  55. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionBodySpec.rowBits_eq_dynamic line 556

    Source documentation

    The natural-word description is literally the established finite-target constraint codec, rather than an alternative encoding.

    theorem rowBits_eq_dynamic {N q : Nat} (vertices : Fin 5 → Fin N)
    (table : Target.PermutationTable q) :
    rowBits (vertices 0).val (vertices 2).val (vertices 1).val (vertices 3).val
      (vertices 4).val table = MachineSubdivisionDynamicRows.rowBits vertices table := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineSubdivisionBodySpec.rowBits, OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.rowBits

  56. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionBodySpec.bodyBudget_le line 565

    Source documentation

    One conservative bound uniform over all occurrences in this output. Only the fixed alphabet and the runtime header sizes appear in the polynomial.

    theorem bodyBudget_le {q : Nat} (base : Tape → List Bool) (u v : Nat)
    (table : Target.PermutationTable q) (suffix : List Bool)
    (ready : Ready base u v table suffix) (n Q e : Nat)
    (hu : u < n) (hv : v < n) (he : e ≤ Q)
    (middle : base .middle = encodeWord (n + e))
    (first : base .first = encodeWord (n + Q + 2 * e))
    (last : base .last = encodeWord (n + Q + 2 * e + 1)) :
    bodyBudget base u v table suffix ≤ 100 * (n + 3 * Q + q * (q + 1) + 1) := by
…
  57. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionLoop.rowPayload_eq line 594
  58. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionLoop.bodyResult_eq_frame line 603
  59. def OAI.MaxCutGames.Explicit.MachineSubdivisionLoop.bodyBound line 626
  60. def OAI.MaxCutGames.Explicit.MachineSubdivisionLoop.bodyInTime line 628
  61. def OAI.MaxCutGames.Explicit.MachineSubdivisionLoop.loopInTime line 644

    Source documentation

    Every list occurrence is read once, emits exactly its four rows, and advances the three private numeric names. The loop includes its final zero-counter test.

    def loopInTime {n q : Nat} (Q e : Nat) (edges : List (Constraint n q))
    (emitted : List Bool) (fit : e + edges.length ≤ Q) :
    StateTransition.EvalsToInTime (machine q).step
      ⟨some .guard, initialState, frame Q e edges emitted⟩
      (some ⟨some .finishStart, initialState,
        frame Q (e + edges.length) ([] : List (Constraint n q))
          (emitted ++ outputRows Q e edges)⟩)
      (edges.length * (bodyBound n q Q + 1) + 1) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineSubdivisionLoop.bodyBound

  62. def OAI.MaxCutGames.Explicit.MachineSubdivisionFinish.timePolynomial line 699
  63. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionFinish.haltList_eq line 702
  64. def OAI.MaxCutGames.Explicit.MachineSubdivisionFinish.finishStartInTime line 711
  65. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionFinish.covers line 723
  66. def OAI.MaxCutGames.Explicit.MachineSubdivisionFinish.completePrefix line 730