OAI/Computability/UniqueGames/PCP/RuntimeModel.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

The finite registers and physical tape roles of the alphabet-table machine. Input-sized numbers occur only on unary tapes. The comparison and emitter register layouts are related by explicit, executable product rearrangements.

  1. inductive OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.Tape line 19
  2. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.Tape.enumList line 25
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.Tape.enumList_getElem?_ctorIdx_eq line 29
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.Tape.enumList_nodup line 33
  5. instance OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.(instance at line 35) line 35
  6. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.Alphabet line 39
  7. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.Flags line 42

    Source documentation

    Self-loop flag, comparison mismatch flag, and second head register.

    abbrev Flags := Bool × Bool × Option Bool
  8. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.Ambient line 43
  9. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.State line 44
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.normal line 46
  11. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.initial line 49
  12. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.context line 51
  13. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.compareEquiv line 54
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.compareEquiv_normal line 61
  15. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.emitterEquiv line 66
  16. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.setupPorts line 72
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.setupPorts_injective line 75
  18. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.headPorts line 79
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.headPorts_injective line 82
  20. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.rowSources line 86
  21. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.headerSources line 87
  22. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.fieldPorts line 88
  23. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts line 90
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts_ne_output line 94
  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts_cover line 97
  26. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.compareStatement line 119
  27. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.emitterStatement line 124
  28. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.storeLoop line 130

    Source documentation

    Store the result chosen by the actual comparison's equal/different exit. This does not compare tape contents in a register transition.

    def storeLoop (value : Bool) (next : Λ) : TM2.Stmt Alphabet Λ (State q) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.Alphabet, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.State

  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.stepAux_storeLoop line 133
  30. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.nextRow line 138
  31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.stepAux_nextRow line 142
  32. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.RuntimeModel.transportInTime line 152

    Source documentation

    One-step simulations transport complete timed executions through the explicit finite register permutations.

    def transportInTime {K τ υ : Type} [DecidableEq K] {Γ : K → Type}
    (e : τ ≃ υ) (p : Λ → TM2.Stmt Γ Λ τ)
    {start finish : TM2.Cfg Γ Λ τ} {budget : Nat}
    (run : StateTransition.EvalsToInTime (TM2.step p) start (some finish) budget) :
    StateTransition.EvalsToInTime (TM2.step (MachineControl.program (Equiv.refl Λ) e p))
      (MachineControl.configuration id e start)
      (some (MachineControl.configuration id e finish)) budget := by
…