OAI/Computability/UniqueGames/Machines/MachineSubdivisionDynamicRowsLemmas.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

Four-edge subdivision row emission with a physical permutation-table field.

The program depends only on the fixed identity table. Five saved endpoint words and the entire final forward permutation table are physical tape contents. In particular an input-dependent permutation is not inserted into a program label or literal instruction. The last row is oriented v → r; for binary-vector translations its table equals the inverse table of the original u → v edge.

  1. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.rows line 30

    Source documentation

    The last table is the actual table for the left-to-right v → r row.

    def rows {n q : Nat} (vertices : Fin 5 → Fin n) (p : PermutationTable q) :
    List (Constraint n q) :=
…
  2. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.tokens line 37
  3. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.tokens_length line 43
  4. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.fields line 46
  5. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.rowBits line 52
  6. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.templateOutput_rows line 55
  7. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.field line 64

    Source documentation

    Six preserved fields, scratch, and a reversed-output accumulator.

    def field (j : Fin 6) : Fin 8 := ⟨j.val, by omega⟩
  8. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.scratch line 66
  9. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.output line 67
  10. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.field_ne_scratch line 69
  11. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.field_ne_output line 75
  12. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.scratch_ne_output line 81
  13. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.machine line 83
  14. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.machine_finiteAlphabet line 94
  15. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.phaseInTime line 101

    Source documentation

    Literal execution of the fixed program; all six input fields are preserved.

    def phaseInTime (identity : List Bool) (base : Fin 8 → List Bool)
    (emptyScratch : base scratch = []) (state : MachineFieldTemplate.State Unit) :
    StateTransition.EvalsToInTime (machine identity).step
      ⟨some (MachineFieldTemplate.startAt (tokens identity).length 0), state, base⟩
      (some ⟨none, MachineFieldTemplate.reset state,
        MachineFieldTemplate.outputTapes base output
          (MachineFieldTemplate.templateOutput (tokens identity)
            (fun j => base (field j)))⟩)
      (3 * MachineFieldTemplate.copiedLength (tokens identity)
        (fun j => base (field j)) + 37) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.scratch, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.machine, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.tokens, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.output, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.field

  16. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.phase_budget line 118

    Source documentation

    The variable permutation table is read once; vertex words are read according to their explicit occurrences in the four rows.

    theorem phase_budget (identity : List Bool) (base : Fin 8 → List Bool) :
    3 * MachineFieldTemplate.copiedLength (tokens identity)
        (fun j => base (field j)) + 37 =
      3 * ((base (field 0)).length + 2 * (base (field 1)).length +
        2 * (base (field 2)).length + 2 * (base (field 3)).length +
        (base (field 4)).length + (base (field 5)).length) + 37 := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.tokens, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.field

  17. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.translation_inverse line 128

    Source documentation

    The inverse table of a binary translation is literally the same table.

    theorem translation_inverse {s : Nat}
    (a b : UniqueGamesTheorem.Integration.BinaryLinear.Vector s) :
    inverseTable (Encoding.translationTable a b) = Encoding.translationTable a b := rfl

    Mentions: OAI.UniqueGamesTheorem.Integration.BinaryLinear.Vector

  18. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.translation_rows line 134

    Source documentation

    Therefore the dynamic emitter serializes the same left-to-right rows as the general subdivision emitter, including the reversed final edge.

    theorem translation_rows {n s : Nat} (vertices : Fin 5 → Fin n)
    (a b : UniqueGamesTheorem.Integration.BinaryLinear.Vector s) :
    rows vertices (Encoding.translationTable a b) =
      MachineSubdivisionRows.rows vertices (Encoding.translationTable a b) := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.BinaryLinear.Vector, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionDynamicRows.rows, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.rows

  19. inductive OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.Tape line 149
  20. abbrev OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.Tape.enumList line 156
  21. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.Tape.enumList_getElem?_ctorIdx_eq line 160
  22. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.Tape.enumList_nodup line 164
  23. instance OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.(instance at line 166) line 166
  24. abbrev OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.State line 170
  25. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.initialState line 172
  26. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.headerField line 174
  27. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.rowField line 179
  28. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.rowTokens line 187
  29. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.headerTokens line 190
  30. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.newHeaderField line 193
  31. structure OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.InitOp line 199

    Source documentation

    Nine fixed affine passes initialize headers, the loop counter, and all three private vertex indices. none means accumulate into the existing unary word.

    structure InitOp where
…
  32. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.initOp line 205
  33. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.clearKeys line 216
  34. inductive OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.Label line 221
  35. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.headerNext line 237
  36. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.initNext line 240
  37. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.rowEntry line 244
  38. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.program line 249

    Source documentation

    A fixed finite program: the table reader counts only q delimiters in finite control, while all unbounded integers are physical unary tape contents.

    def program (q : Nat) : Label q → TM2.Stmt (fun _ : Tape => Bool) (Label q) State
  | .headerStart i => SourceMachine.fieldStart (headerField i) (.headerRead i)
  | .headerRead i => SourceMachine.fieldLoop .input (headerField i)
      (.headerRead i) (some (headerNext i))
  | .initialize i 0 =>
      match (initOp i).seed with
      | some offset => MachineUnaryAffineAt.seed (initOp i).destination offset (.initialize i 1)
      | none => .goto (fun _ => .initialize i 1)
  | .initialize i 1 => MachineUnaryAffineAt.scan (initOp i).source .affineScratch
      (initOp i).destination (initOp i).coefficient (.initialize i 1) (.initialize i 2)
  | .initialize i 2 => MachineTransfer.loopAt .affineScratch (initOp i).source
      id false (.initialize i 2) (some (initNext i))
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.Label, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.Tape, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.State, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.headerField, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.headerNext, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.initOp, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.initNext

  39. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.machine line 293
  40. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.machine_finiteAlphabet line 304
  41. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.rowField_injective line 310
  42. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.clearKeys_covers line 314
  43. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.accumulator_not_mem_clearKeys line 318
  44. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionProgram.output_not_mem_clearKeys line 319
  45. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionFinish.timePolynomial line 332
  46. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionFinish.haltList_eq line 335
  47. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionFinish.finishStartInTime line 343
  48. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionFinish.covers line 355
  49. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionFinish.completePrefix line 362
  50. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionHeaders.inputTapes line 404
  51. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionHeaders.afterVertices line 407
  52. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionHeaders.afterAlphabet line 410
  53. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionHeaders.resultTapes line 414
  54. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionHeaders.initList_eq line 419
  55. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionHeaders.first_result line 425
  56. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionHeaders.second_result line 433
  57. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionHeaders.third_result line 441
  58. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionHeaders.headersInTime line 451

    Source documentation

    The input headers are consumed literally; all unread constraint bits retain their original order and no tape contains an implicit runtime number.

    def headersInTime (q n Q : Nat) (body : List Bool) :
    StateTransition.EvalsToInTime (machine q).step
      (initList (machine q) (encodeWords [n, q, Q] ++ body))
      (some ⟨some (.initialize 0 0), initialState, resultTapes n q Q body⟩)
      (n + q + Q + 6) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionHeaders.resultTapes

  59. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionHeaders.headers_budget line 485
  60. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.source_ne_scratch line 502
  61. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.source_ne_destination line 505
  62. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.scratch_ne_destination line 508
  63. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.priorWord line 511
  64. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.operationTrace line 516
  65. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.sourceValue line 563
  66. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.beforeValue line 574
  67. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.afterValue line 585
  68. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.frame line 588
  69. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.frame_source line 595
  70. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.frame_scratch line 600
  71. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.frame_destination line 604
  72. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.atStage line 610
  73. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.initNext_eq_atStage line 614
  74. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.stageCost line 618
  75. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.sourceValue_le line 620
  76. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.prefixInTime line 623
  77. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.resultTapes line 665
  78. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.final_frame line 679
  79. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.initializeInTime line 689

    Source documentation

    The actual initialized loop counters and fresh numeric vertex IDs are proved outputs of unary arithmetic, including the runtime vertex header.

    def initializeInTime (q n Q : Nat) (body : List Bool) :
    StateTransition.EvalsToInTime (machine q).step
      ⟨some (.initialize 0 0), initialState, MachineSubdivisionHeaders.resultTapes n q Q body⟩
      (some ⟨some (.emitHeader (MachineFieldTemplate.startAt (headerTokens q).length 0)),
        initialState, resultTapes n q Q body⟩)
      (9 * stageCost n Q) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionHeaders.resultTapes, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.resultTapes, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.stageCost

  80. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionEmission.headerBits line 709
  81. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionEmission.resultTapes line 711
  82. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionEmission.header_template line 715
  83. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionEmission.header_copiedLength line 723
  84. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionEmission.header_result line 731
  85. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionEmission.headerInTime line 737
  86. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionEmission.prepareInTime line 756

    Source documentation

    From raw input headers to the running occurrence loop, including all finite arithmetic phases and literal output-header emission.

    def prepareInTime (q n Q : Nat) (body : List Bool) :
    StateTransition.EvalsToInTime (machine q).step
      (initList (machine q) (encodeWords [n, q, Q] ++ body))
      (some ⟨some .guard, initialState, resultTapes n q Q body⟩)
      (n + q + Q + 6 + 9 * MachineSubdivisionInit.stageCost n Q +
        (3 * (n + 7 * Q + 2) + 10)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionEmission.resultTapes, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionInit.stageCost