OAI/Computability/UniqueGames/Machines/MachineRegularOriginalRow.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Machine execution for an inherited regularization row

The machine reads the original reverse index from the physically stored input table. The unread working copy then starts at the 4096 original predicate fields; a fixed finite Boolean block copy retains exactly those fields. Unary arithmetic computes the new reverse index, and the checked row emitter appends the three physical fields. No input table or unbounded arithmetic function is stored in the machine's finite state or instructions.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.inheritedIndex line 27
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow line 32
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_eq line 37
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_tail line 45
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_reverse line 50
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_relation line 63
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_words line 76
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.prefixWords line 83
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.suffixWords line 86
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.prefixWords_length line 89
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.tableWords_at_row line 94
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.tableWords_drop_row line 106
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.selected_reverse line 112
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.remaining_relation line 119
  15. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.Tape line 128
  16. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.Buffer line 129
  17. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.State line 130
  18. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.Alphabet line 131
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.zeroBuffer line 133
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.lookupTape line 135
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.lookupTape_injective line 137
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.source_outside line 144
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.fields line 150
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.fields_zero line 152
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.fields_one line 153
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.fields_two line 154
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.fields_separate line 156
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.copyStateEquiv line 159
  29. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.Label line 165
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.relationCopyAt line 171
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.instruction line 176
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.machine line 188
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.looked line 201
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.copied line 205
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.affined line 210
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.looked_other line 215
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.looked_reverse line 220
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.looked_relation line 224
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.vectorBits_eq_encodedBlock line 234
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.relationBits_eq_encodedBlock line 246
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.relationCopy_step line 252

    Source documentation

    Reusable identity copy of exactly the physically read 4096 unary Boolean fields. The fixed register is reset; every other state component is retained.

    theorem relationCopy_step {K Λ σ : Type} [DecidableEq K]
    (src dst : K) (hne : src ≠ dst) (label : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State σ))
    (code : program label = relationCopyAt src dst exit)
    (relation : RelationTable) (suffix : List Bool) (base : K → List Bool)
    (input : base src = encodeWords (relationWords relation) ++ suffix)
    (ambient : σ) (buffer : Buffer) (register : Option Bool) :
    TM2.step program ⟨some label, ((ambient, buffer), register), base⟩ =
      some ⟨exit, ((ambient, zeroBuffer), register),
        Function.update (Function.update base src suffix) dst
          (encodeWords (relationWords relation) ++ base dst)⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.relationCopyAt, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.Buffer, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.zeroBuffer

  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.relationCopy_pushBound line 281
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.copied_other line 286
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.copied_reverse line 292
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.copied_relation line 297
  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.affined_other line 301
  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.affined_reverse line 306
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.affined_relation line 310
  49. structure OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.Input line 315

    Source documentation

    The input graph and dart index occur only as physically stored tape data.

    structure Input (t : Table) (e : Fin t.darts) (base : Tape → List Bool) : Prop where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.Tape

  50. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.emittedWords line 324
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.affined_fields line 327
  52. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.rowSteps line 337
  53. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.steps line 340
  54. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.finalTapes line 344
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.join_trace line 352
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.lookupTrace line 356
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.copyTrace line 370
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.affineTrace line 385
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.emitTrace line 406
  60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.traceAt line 433

    Source documentation

    All four phases are derived from their concrete instructions.

    theorem traceAt (q : Nat) (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt Alphabet Λ (State σ))
    (code : ∀ l, program (labels l) = instruction q labels exit l)
    (t : Table) (e : Fin t.darts) (base : Tape → List Bool) (input : Input t e base)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[steps q t e base]
      (some ⟨some (labels (.lookup .seed)), ((ambient, zeroBuffer), register), base⟩) =
      some ⟨exit, ((ambient, zeroBuffer), none), finalTapes q t e base⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.Input, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.zeroBuffer, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.finalTapes

  61. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.timeBound line 449
  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.steps_le line 452
  63. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.machineInTime line 470

    Source documentation

    Concrete finite-machine execution for the actual regularized input row.

    def machineInTime (H : BaseTable) (t : Table) (e : Fin t.darts)
    (base : Tape → List Bool) (input : Input t e base) (register : Option Bool) :
    StateTransition.EvalsToInTime (machine internalDegree).step
      ⟨some (.lookup .seed), (((), zeroBuffer), register), base⟩
      (some ⟨none, (((), zeroBuffer), none),
        Function.update (affined internalDegree t e base) (9 : Tape)
          (base (9 : Tape) ++ encodeWords (rowWords (inheritedRow H t e)))⟩)
      (timeBound internalDegree (tableBits t).length (base (9 : Tape)).length) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.Input, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.zeroBuffer, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.affined, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalRow.timeBound