OAI/Computability/UniqueGames/Machines/MachineLookupCore.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Finite control for destructive unary-indexed table lookup. The guard decreases the index even when the table is exhausted. Selection tests for an empty table before writing the destination. All tests inspect just one finite head register.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.Alphabet line 18
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.discard line 20
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.select line 28

    Source documentation

    Check that a field exists before seeding its destination delimiter.

    def select (source destination : K) (copyLabel rejected : Λ) :
    TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.Alphabet

  4. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.Label line 35
  5. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.Label.enumList line 39
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.Label.enumList_getElem?_ctorIdx_eq line 42
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.Label.enumList_nodup line 46
  8. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.(instance at line 48) line 48
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.program line 53

    Source documentation

    Six fixed labels and a single optional-bit register, independent of input.

    def program (index source destination : K) :
    Label → TM2.Stmt (Alphabet (K := K)) Label (σ × Option Bool)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.Alphabet

  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.tapes line 63

    Source documentation

    Three caller tapes with every other tape retained verbatim.

    def tapes (index source destination : K) (base : K → List Bool)
    (counter input output : List Bool) : K → List Bool :=
…
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.tapes_index line 68
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.tapes_source line 74
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.tapes_destination line 80
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.tapes_other line 85
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.update_index line 91
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.update_source line 105
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.update_destination line 116
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.fieldTapes_eq line 122
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLookup.machine line 131

    Source documentation

    A concrete finite machine using exactly three binary stacks. Its table and unary index may be supplied in a caller configuration; no list oracle is used.

    def machine : FinTM2 where
…