OAI/Computability/MaxCut/Machines/MachineSubdivisionDynamicRows.lean

GitHub source file

88 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.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.rows line 28

    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.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.tokens line 35
  3. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.tokens_length line 41
  4. def OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.fields line 44
  5. def OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.rowBits line 50
  6. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.templateOutput_rows line 53
  7. def OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.field line 62

    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.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.scratch line 64
  9. def OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.output line 65
  10. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.field_ne_scratch line 67
  11. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.field_ne_output line 73
  12. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.scratch_ne_output line 79
  13. def OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.machine line 81
  14. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.machine_finiteAlphabet line 92
  15. def OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.phaseInTime line 99

    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.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.scratch, OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.machine, OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.tokens, OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.output, OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.field

  16. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.phase_budget line 116

    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.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.tokens, OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.field

  17. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.translation_inverse line 126

    Source documentation

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

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

    Mentions: OAI.MaxCutGames.Integration.BinaryLinear.Vector

  18. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionDynamicRows.translation_rows line 132

    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 : MaxCutGames.Integration.BinaryLinear.Vector s) :
    rows vertices (Encoding.translationTable a b) =
      MachineSubdivisionRows.rows vertices (Encoding.translationTable a b) := by
…

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

  19. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.Alphabet line 153
  20. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.guard line 157

    Source documentation

    A single finite statement: inspect the counter, decrement a positive counter, and jump to the body or exit. The zero delimiter is never consumed.

    def guard (counter : K) (bodyLabel exitLabel : Λ) :
    TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.Alphabet

  21. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.counterTapes line 166

    Source documentation

    An arbitrary caller frame with one tape holding the unary counter and its unread suffix. Only this tape depends on the counter value.

    def counterTapes (counter : K) (base : K → List Bool) (n : Nat)
    (suffix : List Bool) : K → List Bool :=
…
  22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.counterTapes_counter line 170
  23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.counterTapes_other line 175
  24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.guardPushBound line 181
  25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.stepAux_succ line 187

    Source documentation

    Positive counters lose exactly one true bit; the delimiter and suffix remain. Ambient state, unrelated tapes, and labels are accounted for explicitly.

    theorem stepAux_succ (counter : K) (bodyLabel exitLabel : Λ)
    (base : K → List Bool) (n : Nat) (suffix : List Bool)
    (ambient : σ) (register : Option Bool) :
    TM2.stepAux (guard counter bodyLabel exitLabel) (ambient, register)
      (counterTapes counter base (n + 1) suffix) =
      ⟨some bodyLabel, (ambient, none), counterTapes counter base n suffix⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.guard, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.counterTapes

  26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.stepAux_zero line 196

    Source documentation

    A zero counter is inspected without removing its delimiter.

    theorem stepAux_zero (counter : K) (bodyLabel exitLabel : Λ)
    (base : K → List Bool) (suffix : List Bool)
    (ambient : σ) (register : Option Bool) :
    TM2.stepAux (guard counter bodyLabel exitLabel) (ambient, register)
      (counterTapes counter base 0 suffix) =
      ⟨some exitLabel, (ambient, none), counterTapes counter base 0 suffix⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.guard, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.counterTapes

  27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.guardStep_succ line 204
  28. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.guardStep_zero line 216
  29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.guardTrace_succ line 229

    Source documentation

    The positive branch executes in exactly one transition of the ambient program.

    theorem guardTrace_succ (counter : K) (guardLabel bodyLabel exitLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.Alphabet

  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.guardTrace_zero line 242
  31. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.guardInTime_succ line 254
  32. def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryCounter.guardInTime_zero line 269
  33. inductive OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.Tape line 293
  34. abbrev OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.Tape.enumList line 300
  35. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.Tape.enumList_getElem?_ctorIdx_eq line 304
  36. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.Tape.enumList_nodup line 308
  37. instance OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.(instance at line 310) line 310
  38. abbrev OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.State line 314
  39. def OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.initialState line 316
  40. def OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.headerField line 318
  41. def OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.rowField line 323
  42. def OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.rowTokens line 331
  43. def OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.headerTokens line 334
  44. def OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.newHeaderField line 337
  45. structure OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.InitOp line 343

    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
…
  46. def OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.initOp line 349
  47. def OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.clearKeys line 360
  48. inductive OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.Label line 365
  49. def OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.headerNext line 381
  50. def OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.initNext line 384
  51. def OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.rowEntry line 388
  52. def OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.program line 393

    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.MaxCutGames.Explicit.MachineSubdivisionProgram.Label, OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.Tape, OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.State, OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.headerField, OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.headerNext, OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.initOp, OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.initNext

  53. def OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.machine line 437
  54. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.machine_finiteAlphabet line 448
  55. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.rowField_injective line 454
  56. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.clearKeys_covers line 458
  57. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.accumulator_not_mem_clearKeys line 462
  58. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionProgram.output_not_mem_clearKeys line 463
  59. def OAI.MaxCutGames.Explicit.MachineSubdivisionHeaders.inputTapes line 476
  60. def OAI.MaxCutGames.Explicit.MachineSubdivisionHeaders.afterVertices line 479
  61. def OAI.MaxCutGames.Explicit.MachineSubdivisionHeaders.afterAlphabet line 482
  62. def OAI.MaxCutGames.Explicit.MachineSubdivisionHeaders.resultTapes line 486
  63. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionHeaders.initList_eq line 491
  64. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionHeaders.first_result line 497
  65. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionHeaders.second_result line 505
  66. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionHeaders.third_result line 513
  67. def OAI.MaxCutGames.Explicit.MachineSubdivisionHeaders.headersInTime line 523

    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.MaxCutGames.Explicit.MachineSubdivisionHeaders.resultTapes

  68. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionHeaders.headers_budget line 557
  69. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionInit.source_ne_scratch line 574
  70. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionInit.source_ne_destination line 577
  71. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionInit.scratch_ne_destination line 580
  72. def OAI.MaxCutGames.Explicit.MachineSubdivisionInit.priorWord line 583
  73. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionInit.operationTrace line 588
  74. def OAI.MaxCutGames.Explicit.MachineSubdivisionInit.sourceValue line 635
  75. def OAI.MaxCutGames.Explicit.MachineSubdivisionInit.beforeValue line 646
  76. def OAI.MaxCutGames.Explicit.MachineSubdivisionInit.afterValue line 657
  77. def OAI.MaxCutGames.Explicit.MachineSubdivisionInit.frame line 660
  78. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionInit.frame_source line 667
  79. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionInit.frame_scratch line 672
  80. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionInit.frame_destination line 676
  81. def OAI.MaxCutGames.Explicit.MachineSubdivisionInit.atStage line 682
  82. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionInit.initNext_eq_atStage line 686
  83. def OAI.MaxCutGames.Explicit.MachineSubdivisionInit.stageCost line 690
  84. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionInit.sourceValue_le line 692
  85. def OAI.MaxCutGames.Explicit.MachineSubdivisionInit.prefixInTime line 695
  86. def OAI.MaxCutGames.Explicit.MachineSubdivisionInit.resultTapes line 737
  87. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionInit.final_frame line 751
  88. def OAI.MaxCutGames.Explicit.MachineSubdivisionInit.initializeInTime line 761

    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.MaxCutGames.Explicit.MachineSubdivisionHeaders.resultTapes, OAI.MaxCutGames.Explicit.MachineSubdivisionInit.resultTapes, OAI.MaxCutGames.Explicit.MachineSubdivisionInit.stageCost