OAI/Computability/UniqueGames/Machines/MachineInitialHeaders.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Actual caller-program traces for non-destructive unary-prefix emission and the two headers of the raw initial graph. Unread suffixes are never scanned.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineInitialHeaders.Alphabet line 23
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineInitialHeaders.prefixScan line 25
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineInitialHeaders.update_source line 36
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineInitialHeaders.update_scratch line 50
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineInitialHeaders.update_output line 61
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineInitialHeaders.prefixStep_true line 67
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineInitialHeaders.prefixStep_false line 78
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineInitialHeaders.replicate_append_cons line 88
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineInitialHeaders.prefixScanTrace line 94

    Source documentation

    The first loop takes one transition per unary bit and one for the delimiter.

    theorem prefixScanTrace (source scratch output : K)
    (hst : source ≠ scratch) (hso : source ≠ output) (hto : scratch ≠ output)
    (scale : ℕ) (again restore : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

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

  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineInitialHeaders.prefixTrace line 131
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineInitialHeaders.prefixInTime line 181
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineInitialHeaders.prefixScan_pushBound line 200
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineInitialHeaders.literalTrace line 208

    Source documentation

    One transition emits a fixed literal word and enters the caller continuation.

    theorem literalTrace (output : K) (word : List Bool) (label : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

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

  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineInitialHeaders.trace_trans line 221
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineInitialHeaders.headerTrace line 227

    Source documentation

    The complete raw initial-graph header phase, in an arbitrary caller program. Only the output tape changes; its old suffix is preserved verbatim.

    theorem headerTrace (nTape mTape scratch output : K)
    (_hnm : nTape ≠ mTape) (hnt : nTape ≠ scratch) (hno : nTape ≠ output)
    (hmt : mTape ≠ scratch) (hmo : mTape ≠ output) (hto : scratch ≠ output)
    (scanN restoreN scanM1 restoreM1 closeFirst scanM6 restoreM6 closeSecond : Λ)
    (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

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

  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineInitialHeaders.headerInTime line 307