OAI/Computability/UniqueGames/Machines/MachineFixedCopiesLemmas.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

A fixed number of copies of an arbitrary bit stream, by a real finite-alphabet machine. This is the uniform-rounding stream primitive: copying a header-free occurrence stream C times gives multiplicity C to every listed occurrence. The input is preserved during the copy phase, physically drained, and replaced by the forward-order result. No unbounded word is stored in finite control.

  1. def OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.copies line 24
  2. theorem OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.copies_zero line 27
  3. theorem OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.copies_succ line 29
  4. theorem OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.copies_length line 33
  5. def OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.tokens line 39
  6. theorem OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.tokens_length line 42
  7. theorem OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.templateOutput line 44
  8. theorem OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.copiedLength line 53
  9. abbrev OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.Tape line 57
  10. abbrev OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.Label line 58
  11. abbrev OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.State line 59
  12. def OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.initialState line 61
  13. def OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.program line 63
  14. def OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.machine line 69
  15. def OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.tapes line 80
  16. theorem OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.initList_eq line 83
  17. theorem OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.haltList_eq line 93
  18. theorem OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.copied_tapes line 101
  19. theorem OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.drained_tapes line 107
  20. theorem OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.transferred_tapes line 112
  21. def OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.outputInTime line 119

    Source documentation

    Copy, cleanup, and reversal all run on the actual finite transition program.

    def outputInTime (C : Nat) (word : List Bool) :
    TM2OutputsInTime (machine C) word (some (copies C word))
      ((4 * C + 1) * word.length + 3 * C + 3) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.machine, OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.copies

  22. def OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.computableInPolyTime line 165

    Source documentation

    Its linear polynomial is measured in the actual input bit length.

    noncomputable def computableInPolyTime (C : Nat) :
    TM2ComputableInPolyTime (id : List Bool → List Bool) id (copies C) where
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.copies

  23. theorem OAI.UniqueGamesTheorem.Explicit.MachineFixedCopies.computation_finiteAlphabet line 181
  24. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.identityTable line 196
  25. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.inverseTable line 202
  26. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.rows line 210

    Source documentation

    The saved fields are ordered u,p,q,r,v. All four edges are oriented left-to-right; hence the last permutation is inverted.

    def rows {n q : Nat} (vertices : Fin 5 → Fin n) (p : PermutationTable q) :
    List (Constraint n q) :=
…
  27. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.rows_length line 217
  28. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.tokens line 222

    Source documentation

    The program copies saved endpoint words and emits complete forward tables.

    def tokens (identity inverse : List Bool) : List (MachineFieldTemplate.Token 5) :=
…
  29. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.tokens_length line 228
  30. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.fields line 231
  31. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.rowBits line 234
  32. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.templateOutput_rows line 237
  33. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.field line 247

    Source documentation

    A finite stack layout: five preserved fields, scratch, and reversed output.

    def field (j : Fin 5) : Fin 7 := ⟨j.val, by omega⟩
  34. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.scratch line 249
  35. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.output line 250
  36. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.field_ne_scratch line 252
  37. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.field_ne_output line 258
  38. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.scratch_ne_output line 264
  39. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.machine line 266
  40. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.machine_finiteAlphabet line 277
  41. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.phaseInTime line 285

    Source documentation

    Exact physical row execution, preserving the five saved fields and restoring scratch. This is a phase theorem; it does not assume its own execution.

    def phaseInTime (identity inverse : List Bool) (base : Fin 7 → List Bool)
    (emptyScratch : base scratch = []) (state : MachineFieldTemplate.State Unit) :
    StateTransition.EvalsToInTime (machine identity inverse).step
      ⟨some (MachineFieldTemplate.startAt (tokens identity inverse).length 0), state, base⟩
      (some ⟨none, MachineFieldTemplate.reset state,
        MachineFieldTemplate.outputTapes base output
          (MachineFieldTemplate.templateOutput (tokens identity inverse)
            (fun j => base (field j)))⟩)
      (3 * MachineFieldTemplate.copiedLength (tokens identity inverse)
        (fun j => base (field j)) + 37) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.scratch, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.machine, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.tokens, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.output, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.field

  42. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.phase_budget line 300
  43. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.subdivisionVertexWords line 311

    Source documentation

    The semantic subdivision numbering: originals and middle vertices on the left, then two private right vertices for each occurrence.

    def subdivisionVertexWords (n Q u v e : Nat) : Fin 5 → Nat
  | 0 => u
  | 1 => n + Q + 2 * e
  | 2 => n + e
  | 3 => n + Q + 2 * e + 1
  | 4 => v
  44. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionRows.subdivisionVertexWords_bounded line 318