OAI/Computability/UniqueGames/Machines/MachineRegularInternalRow.lean

GitHub source file

145 declarations, 0 contain sorry, 0 declared as axioms

Physical construction of an internal regularization row

The input values belong on unary tapes. The cloud degree and the queried port are the only arithmetic parameters fixed in finite control. The stored cloud rotation supplies both the destination's local index and the return port. The final row contains the full fixed equality predicate.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.Alphabet line 31
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.equalityBits line 34

    Source documentation

    This literal is independent of the graph input.

    def equalityBits : List Bool :=
…
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.equalityBits_length_le line 37
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.emittedBits line 40
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.emittedBits_length line 43
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.emittedBits_eq_row line 48
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selected_rotation line 63

    Source documentation

    The address supplied to the physical lookup is the actual port-table row.

    theorem selected_rotation {n q : Nat} (table : ExpanderTables.Table n q)
    (i : Fin n) (p : Fin q) :
    (ExpanderTableWords.rotationWords table)[q * i.val + p.val]? =
      some (q * (ExpanderTables.lookup table (i, p)).1.val +
        (ExpanderTables.lookup table (i, p)).2.val) := by
…
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selected_rotation_div line 70
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selected_rotation_mod line 78
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.rotationLookupTrace line 87

    Source documentation

    A direct instantiation of the real affine getter on the actual rotor words.

    theorem rotationLookupTrace {n q : Nat} (table : ExpanderTables.Table n q)
    (i : Fin n) (p : Fin q) (source : K) (tape : Fin 5 → K)
    (distinct : Function.Injective tape) (outside : ∀ a, source ≠ tape a)
    (labels : MachineAffineLookup.Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.Alphabet

  11. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.FinishLabel line 110
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.finishFields line 118

    Source documentation

    Tail, selected global target, returned port, scratch, reverse field, equality field, row buffer, accumulated output.

    def finishFields (tape : Fin 8 → K) : Fin 3 → K := fun i =>
…
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.finishFields_zero line 122
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.finishFields_one line 124
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.finishFields_two line 126
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.finishInstruction line 130

    Source documentation

    The return port is copied from its physical unary tape before fixed-slope arithmetic adds the actual selected global target.

    def finishInstruction (q : Nat) (tape : Fin 8 → K) (labels : FinishLabel → Λ)
    (exit : Option Λ) : FinishLabel → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.FinishLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.Alphabet

  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.finishSteps line 149
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.finishSteps_le line 154
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.joinTrace line 161
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.finishTrace line 168

    Source documentation

    Actual final arithmetic, full relation emission, row append and cleanup. The only changed tape is the accumulated output; both physical target fields and all metadata are preserved. No execution hypothesis is supplied.

    theorem finishTrace (q : Nat) (tape : Fin 8 → K) (distinct : Function.Injective tape)
    (labels : FinishLabel → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.FinishLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.Alphabet

  21. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.RotorLabel line 283
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes line 288
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes_injective line 292
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes_outside line 300
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.rotorInstruction line 307
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.rotorFinalTapes line 318
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.rotorSteps line 328
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.rotorTrace line 335

    Source documentation

    The actual stored reverse row is read and physically divided by the fixed degree. Both output fields equal the coordinates of the actual table lookup.

    theorem rotorTrace {n q : Nat} (positive : 0 < q) (table : ExpanderTables.Table n q)
    (i : Fin n) (p : Fin q) (tape : Fin 8 → K) (distinct : Function.Injective tape)
    (labels : RotorLabel q → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (MachineFixedDivMod.State σ q))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.RotorLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.State

  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.rotorSteps_le line 414
  30. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape line 424
  31. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape.enumList line 429
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape.enumList_getElem?_ctorIdx_eq line 432
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape.enumList_nodup line 436
  34. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.(instance at line 438) line 438
  35. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectTape line 442
  36. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.RawSelectAlphabet line 443
  37. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectAlphabet line 445
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectAlphabet_eq line 447
  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectToBoolWord line 453
  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectToBoolTapes line 458
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.alphabet_tapes_apply line 461
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectToBoolTapes_eq line 468
  43. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectState line 476
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectStateEquiv line 478
  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectScratch line 484
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectQuery line 485
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectOutput line 486
  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.compareSlots line 488
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.subtractSlots line 492
  50. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectCopy line 496
  51. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectCopy.enumList line 500
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectCopy.enumList_getElem?_ctorIdx_eq line 503
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectCopy.enumList_nodup line 507
  54. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.(instance at line 509) line 509
  55. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectAdd line 513
  56. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectAdd.enumList line 517
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectAdd.enumList_getElem?_ctorIdx_eq line 519
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectAdd.enumList_nodup line 523
  59. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.(instance at line 525) line 525
  60. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage line 529
  61. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage.enumList line 533
  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage.enumList_getElem?_ctorIdx_eq line 535
  63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage.enumList_nodup line 539
  64. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.(instance at line 541) line 541
  65. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectControl line 545
  66. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectLabel line 554
  67. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.copySource line 556
  68. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.copyDestination line 562
  69. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.afterCopy line 568
  70. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.addSource line 575
  71. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.afterAdd line 579
  72. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.cleanupTape line 583
  73. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.afterCleanup line 586
  74. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectControl line 589
  75. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.rawSelectProgram line 613

    Source documentation

    All arithmetic is on extra tapes. The old-dart branch literally contains the shared selector program, with only static tape, label and state transport.

    def rawSelectProgram : SelectLabel → TM2.Stmt RawSelectAlphabet SelectLabel (SelectState σ) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.RawSelectAlphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectState

  76. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectProgram line 619
  77. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectProgram_control line 622
  78. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectCleanState line 634
  79. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectComparisonTrace line 639

    Source documentation

    One physical strict comparison decides the branch and preserves both input indices. In particular equality belongs to the dummy branch.

    theorem selectComparisonTrace (base : SelectTape → List Bool) (j k : Nat)
    (hj : base (.inr .localIndex) = encodeWord j)
    (hk : base (.inr .cloudSize) = encodeWord k)
    (hl : base (.inr .savedLeft) = []) (hr : base (.inr .savedRight) = [])
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step selectProgram))^[MachineUnaryLessAt.steps j k + 1]
      (some ⟨some (.inr (.compare .scan)), selectCleanState ambient register, base⟩) =
      some ⟨some (.inr (.copy (if j < k then .oldLocal else .dummyLocal) .seed)),
        selectCleanState ambient none, base⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectTape, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectCleanState

  80. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectCopyTrace line 662

    Source documentation

    Actual preserving unary copy used to construct both the selector query and the dummy-index operands.

    theorem selectCopyTrace (kind : SelectCopy) (base : SelectTape → List Bool)
    (a : Nat) (hword : base (copySource kind) = encodeWord a)
    (hscratch : base selectScratch = []) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step selectProgram))^[2 * (a + 1) + 1]
      (some ⟨some (.inr (.copy kind .seed)), selectCleanState ambient register, base⟩) =
      some ⟨some (afterCopy kind), selectCleanState ambient none,
        Function.update base (copyDestination kind)
          (encodeWord a ++ base (copyDestination kind))⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectCopy, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.copySource, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectScratch, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectCleanState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.afterCopy, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.copyDestination

  81. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectAddTrace line 683

    Source documentation

    The two runtime addends are read physically; no input-dependent offset is captured by a single finite instruction.

    theorem selectAddTrace (kind : SelectAdd) (base : SelectTape → List Bool)
    (a b : Nat) (hword : base (addSource kind) = encodeWord a)
    (houtput : base selectOutput = encodeWord b) (hscratch : base selectScratch = [])
    (ambient : σ) :
    (advance (TM2.step selectProgram))^[2 * (a + 1)]
      (some ⟨some (.inr (.add kind .scan)), selectCleanState ambient none, base⟩) =
      some ⟨some (afterAdd kind), selectCleanState ambient none,
        Function.update base selectOutput (encodeWord (a + b))⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectAdd, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.addSource, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectOutput, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectScratch, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectCleanState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.afterAdd

  82. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.CoreTape line 709
  83. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.CoreState line 710
  84. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.CoreLabel line 714
  85. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreEntry line 721
  86. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectCloudTrace line 725

    Source documentation

    The shared cloud-selector trace is preserved exactly by static tape, register and alphabet transport. These transports add no transition.

    theorem selectCloudTrace (t : GraphTables.Table) (v : Fin t.vertices)
    (i : Fin (PreprocessingCloudIndex.cloudSize t v))
    (extra : SelectExtraTape → List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step selectProgram))^[MachineCloudSelect.cloudSelectSteps t v i []]
      (some ⟨some (.inl (.inr .initialize)), selectCleanState ambient register,
        selectToBoolTapes (MachineEmbedding.tapes
          (MachineCloudSelect.memory (GraphTables.tableBits t) []
            (MachineCloudSelect.queryWord v.val i.val []) [] [] [] []) extra)⟩) =
      some ⟨some (.inr (.cleanup 0)), selectCleanState ambient none,
        selectToBoolTapes (MachineEmbedding.tapes
          (MachineCloudSelect.memory (GraphTables.tableBits t) []
            (MachineCloudSelect.queryWord v.val i.val []) [] [] []
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.cloudSelectSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectCleanState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectToBoolTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineEmbedding.tapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.memory, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.queryWord

  87. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectExtraMemory line 757
  88. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectMemory line 770
  89. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectMemory_query line 777
  90. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectMemory_output line 781
  91. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectMemory_scratch line 785
  92. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectMemory_extra line 789
  93. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_query line 794
  94. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_output line 806
  95. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_local line 818
  96. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_size line 830
  97. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_left line 842
  98. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_right line 854
  99. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectCleanupTrace line 866
  100. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.oldSelectSteps line 909
  101. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectOldTrace line 914
  102. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.dummySelectSteps line 958
  103. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.dummySelectSteps_eq line 962
  104. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectDummyTrace line 969

    Source documentation

    The dummy branch uses the actual truncating-subtraction scan on copied operands. The original local index, cloud size, prefix and dart count survive.

    theorem selectDummyTrace (graph : List Bool) (j v k o m : Nat) (hk : k ≤ j)
    (ambient : σ) :
    (advance (TM2.step selectProgram))^[dummySelectSteps j k o m]
      (some ⟨some (.inr (.copy .dummyLocal .seed)), selectCleanState ambient none,
        selectMemory graph j v k o m [] [] [] [] [] []⟩) =
      some ⟨none, selectCleanState ambient none,
        selectMemory graph j v k o m [] (encodeWord (m + o + (j - k))) [] [] [] []⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.dummySelectSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectCleanState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectMemory, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  105. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectionSteps line 1028
  106. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectionTrace line 1038

    Source documentation

    The entire actual selector program, with both runtime branches and the same clean final frame. Metadata values are premises about physical tapes.

    theorem selectionTrace (t : GraphTables.Table) (padding : Fin t.vertices → Nat)
    (v : Fin t.vertices) (i : Fin (PreprocessingCloudIndex.cloudSize t v + padding v))
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step selectProgram))^[selectionSteps t padding v i]
      (some ⟨some (.inr (.compare .scan)), selectCleanState ambient register,
        selectMemory (GraphTables.tableBits t) i.val v.val
          (PreprocessingCloudIndex.cloudSize t v)
          (PreprocessingPaddingOffsets.offset padding v.val) t.darts [] [] [] [] [] []⟩) =
      some ⟨none, selectCleanState ambient none,
        selectMemory (GraphTables.tableBits t) i.val v.val
          (PreprocessingCloudIndex.cloudSize t v)
          (PreprocessingPaddingOffsets.offset padding v.val) t.darts []
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectionSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectCleanState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectMemory

  107. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectionSteps_le line 1070
  108. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectorMachine line 1091
  109. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectionInTime line 1102
  110. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreRotorTapes line 1123

    Source documentation

    The fixed core rotor roles use the agreed reusable 27-tape frame.

    def coreRotorTapes : Fin 8 → CoreTape := ![3, 7, 10, 11, 12, 9, 13, 14]

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.CoreTape

  111. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreFinishTapes line 1126

    Source documentation

    Tail, selected destination, return port, scratch and emitted row fields.

    def coreFinishTapes : Fin 8 → CoreTape := ![1, 15, 14, 9, 24, 25, 26, 8]

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.CoreTape

  112. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreSelectTape line 1128
  113. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreSelectView line 1146
  114. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreSelectView_left line 1155
  115. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreSelectView_right line 1163
  116. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreCleanupTape line 1168
  117. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreRotorStateEquiv line 1170
  118. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreSelectStateEquiv line 1179
  119. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreAfterCleanup line 1186
  120. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreInstruction line 1191

    Source documentation

    The whole internal-row program has only fixed q and p in its code.

    def coreInstruction (q : Nat) (positive : 0 < q) (p : Fin q)
    (labels : CoreLabel q → Λ) (exit : Option Λ) :
    CoreLabel q → TM2.Stmt (fun _ : CoreTape => Bool) Λ (CoreState σ q)
  | .rotor stage => MachineStateEquiv.statement (coreRotorStateEquiv σ q)
      (rotorInstruction q positive p coreRotorTapes
        (fun l => labels (.rotor l)) (some (labels (.select (.inr (.compare .scan))))) stage)
  | .select stage => MachineCloudPadding.Placement.statement coreSelectTape
      (fun l => labels (.select l)) (some (labels (.finish .seedReturn)))
      (MachineStateEquiv.statement (coreSelectStateEquiv σ q) (selectProgram stage))
  | .finish stage => finishInstruction q coreFinishTapes
      (fun l => labels (.finish l)) (some (labels (.cleanup 0))) stage
  | .cleanup i => MachineDrain.drain (coreCleanupTape i) (labels (.cleanup i))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.CoreLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.CoreTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.CoreState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreRotorStateEquiv, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.rotorInstruction, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreRotorTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Placement.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreSelectTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreSelectStateEquiv, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.finishInstruction, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreFinishTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrain.drain, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreCleanupTape

  121. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreInitialState line 1205
  122. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreMachine line 1209
  123. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreMemory line 1220
  124. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreMemory_update_output line 1226
  125. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreRotorTapes_injective line 1234
  126. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreFinishTapes_injective line 1238
  127. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreCleaned line 1242
  128. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreCleanupSteps line 1247
  129. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreCleanupTrace line 1252
  130. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreCleaned_memory line 1329
  131. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreCleanupSteps_memory line 1337
  132. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreRotorFinalFrame line 1349
  133. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreRotorTrace line 1365
  134. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreSelectFrame line 1411
  135. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreSelectionTrace line 1420
  136. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreFinishTrace line 1455
  137. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreInputTapes line 1487
  138. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreSteps line 1497
  139. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreTrace line 1514

    Source documentation

    One full actual internal row of the serialized regularization, including the physical rotor lookup, both destination cases, full equality predicate, row append and complete reusable cleanup frame.

    theorem coreTrace (q : Nat) (positive : 0 < q) (p : Fin q)
    (labels : CoreLabel q → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : CoreTape => Bool) Λ (CoreState σ q))
    (code : ∀ l, program (labels l) = coreInstruction q positive p labels exit l)
    (t : GraphTables.Table) (padding : Fin t.vertices → Nat)
    (tables : ∀ v, ExpanderTables.Table (PreprocessingCloudIndex.cloudSize t v + padding v) q)
    (v : Fin t.vertices) (x : PreprocessingCloudIndex.PaddedCloud t padding v)
    (output : List Bool) (ambient : σ) :
    (advance (TM2.step program))^[coreSteps t padding tables v x p output.length]
      (some ⟨some (labels (coreEntry q)), coreInitialState q positive ambient,
        coreInputTapes t padding tables v x output⟩) =
      some ⟨exit, coreInitialState q positive ambient,
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.CoreLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.CoreTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.CoreState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreInstruction, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreInitialState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreInputTapes

  140. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.selectedIndex_le line 1563

    Source documentation

    A selected original dart is below the original dart count; a dummy target is the old-dart count plus its physical prefix and local remainder.

    theorem selectedIndex_le (t : GraphTables.Table) (padding : Fin t.vertices → Nat)
    (v : Fin t.vertices) (i : Fin (PreprocessingCloudIndex.cloudSize t v + padding v)) :
    PreprocessingInternalRows.selectedIndex t padding v i ≤
      t.darts + PreprocessingPaddingOffsets.offset padding v.val + i.val := by
…
  141. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.encodedDrop_length_le line 1574
  142. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.rotorSize_le_encodedLength line 1582

    Source documentation

    Every rotor entry occupies at least its delimiter on the physical tape.

    theorem rotorSize_le_encodedLength {n q : Nat} (positive : 0 < q)
    (table : ExpanderTables.Table n q) :
    n ≤ (encodeWords (ExpanderTableWords.rotationWords table)).length := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords

  143. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreTimeBound line 1592

    Source documentation

    For fixed cloud degree q this is affine in the lengths and unary values on the actual input tapes. All relation/cleanup constants are included.

    def coreTimeBound (q graphLength rotorLength x v i k o m outputLength : Nat) : Nat :=
…
  144. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreSteps_le line 1596
  145. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreMachineInTime line 1662

    Source documentation

    The concrete finite machine executes the actual internal row in the proved affine budget and returns the reusable clean frame.

    def coreMachineInTime (q : Nat) (positive : 0 < q) (t : GraphTables.Table)
    (padding : Fin t.vertices → Nat)
    (tables : ∀ v, ExpanderTables.Table (PreprocessingCloudIndex.cloudSize t v + padding v) q)
    (v : Fin t.vertices) (x : PreprocessingCloudIndex.PaddedCloud t padding v)
    (p : Fin q) (output : List Bool) :
    StateTransition.EvalsToInTime (coreMachine q positive p).step
      ⟨some (coreEntry q), coreInitialState q positive (), coreInputTapes t padding tables v x output⟩
      (some ⟨none, coreInitialState q positive (), coreInputTapes t padding tables v x
        (output ++ encodeWords (GraphTables.rowWords (PreprocessingInternalRows.row t padding tables v x p)))⟩)
      (coreTimeBound q (GraphTables.tableBits t).length
        (encodeWords (ExpanderTableWords.rotationWords (tables v))).length
        (PreprocessingRegularTables.vertexOrder t padding x.val).val v.val
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreMachine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreInitialState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreInputTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularInternalRow.coreTimeBound