OAI/Computability/UniqueGames/Machines/MachineDrainManyLemmas.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

Actual cleanup of a finite list of work tapes

Each list position supplies one fixed drain label. The finite-sequence theorem composes the checked physical drains; neither the list nor a runtime tape index is stored in the register. Repeated tape names are allowed. The cleanup bound uses the lengths before cleanup, since draining can only shorten a tape.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.Alphabet line 26
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.Tapes line 27
  3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.LocalLabel line 28
  4. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.Label line 29
  5. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.Data line 30
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.entry line 32
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.localInstruction line 35
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.instruction line 39
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.result line 44
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.cost line 47
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.finalTapes line 49
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.finalRegister line 53
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.finalRegister_none line 58
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.steps line 61
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.sequence_result line 66
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.sequence_steps line 76
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.finalTapes_apply line 84

    Source documentation

    Selected tapes are empty; every other tape word is preserved.

    theorem finalTapes_apply (chosen : List K) (base : Tapes K) (k : K) :
    finalTapes chosen base k = if k ∈ chosen then [] else base k := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.Tapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.finalTapes

  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.finalTapes_mem line 95
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.finalTapes_not_mem line 98
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.lengthSum line 101
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.lengthSum_mono line 105
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.steps_le line 115

    Source documentation

    This upper bound remains valid when the cleanup list repeats tapes.

    theorem steps_le (chosen : List K) (base : Tapes K) :
    steps chosen base ≤ lengthSum chosen base + chosen.length := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.Tapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.lengthSum

  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.steps_le_uniform line 131
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.trace line 147

    Source documentation

    Exact execution of all concrete drains in the supplied ambient program.

    theorem trace (chosen : List K) (labels : Label chosen → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

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

  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.execution line 168
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.workTapes line 181

    Source documentation

    An executable complete cleanup list from an explicit finite enumeration.

    def workTapes {N : Nat} (enumeration : Fin N ≃ K) (output : K) : List K :=
…
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.mem_workTapes line 184
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.workTapes_length_le line 191
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.haltTapes line 197

    Source documentation

    The tape component of the actual halted configuration: only output remains.

    def haltTapes (output : K) (word : List Bool) : Tapes K :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.Tapes

  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.finalTapes_workTapes line 200
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.cleanupTrace line 212

    Source documentation

    With a clean register, complete work-tape cleanup reaches the standard halted shape, preserving the output word and the ambient state exactly.

    theorem cleanupTrace {N : Nat} (enumeration : Fin N ≃ K) (output : K)
    (labels : Label (workTapes enumeration output) → Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.workTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrainMany.Alphabet

  32. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.Profile line 235
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.equalityProfile line 237
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.equalityProfile_encodeWord line 240
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.statement_roundtrip line 255
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.copyStateEquiv line 260
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.normalState line 267
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.copyStatement line 269
  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.copyInCompareState line 274
  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.nonDestructiveCompareInTime line 321
  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.setEntry line 378
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.setEntry_apply line 381
  43. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.setExpected line 387
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.foldProfile line 391
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.foldProfile_apply line 394
  46. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.Tape line 410
  47. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.Label line 411
  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.labelAt line 413
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.storePair line 416
  50. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.profileProgram line 423

    Source documentation

    The fixed list of pairs determines all control labels and original fields. The program compares only copied work-stack heads, then stores one finite bit.

    def profileProgram {q : Nat} (cells : List (Fin q × Fin q)) (label : Label cells) :
    TM2.Stmt (fun _ : Tape q => Bool) (Label cells) (MachineCompare.State (Profile q)) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCompare.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.Profile

  51. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.pairTime line 443
  52. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.prefixProfile line 447
  53. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.prefixTime line 451
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.prefixProfile_succ line 455
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.prefixTime_succ line 463
  56. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.stageInTime line 471

    Source documentation

    One fully constructed copy/copy/compare/store stage, restoring every stack.

    def stageInTime {q : Nat} (cells : List (Fin q × Fin q)) (r : Nat) (hr : r < cells.length)
    (base : Tape q → List Bool) (hwork : ∀ w : Fin 3, base (.inr w) = []) (profile : Profile q) :
    StateTransition.EvalsToInTime (TM2.step (profileProgram cells))
      ⟨some (labelAt cells r 0), normalState profile, base⟩
      (some ⟨some (labelAt cells (r + 1) 0),
        normalState (setExpected (fun i => base (.inl i)) profile cells[r]), base⟩)
      (pairTime (fun i => base (.inl i)) cells[r]) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.Profile, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.profileProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.labelAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.normalState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.setExpected, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.pairTime

  57. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.prefixInTime line 517

    Source documentation

    Compose the actual stages up to any fixed position in the pair list.

    def prefixInTime {q : Nat} (cells : List (Fin q × Fin q))
    (base : Tape q → List Bool) (hwork : ∀ w : Fin 3, base (.inr w) = []) (initial : Profile q)
    (r : Nat) (hr : r ≤ cells.length) :
    StateTransition.EvalsToInTime (TM2.step (profileProgram cells))
      ⟨some (labelAt cells 0 0), normalState initial, base⟩
      (some ⟨some (labelAt cells r 0),
        normalState (prefixProfile (fun i => base (.inl i)) initial cells r), base⟩)
      (prefixTime (fun i => base (.inl i)) cells r) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.Profile, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.profileProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.labelAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.normalState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.prefixProfile, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.prefixTime

  58. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.allPairs line 537
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.mem_allPairs line 540
  60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.length_allPairs line 543
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.foldProfile_allPairs line 546
  62. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.profileMachine line 552

    Source documentation

    A concrete finite machine for the full field equality matrix.

    def profileMachine (q : Nat) : FinTM2 where
…
  63. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.profileInTime line 564

    Source documentation

    Compute every matrix entry while preserving all original field stacks.

    def profileInTime (q : Nat) (base : Tape q → List Bool)
    (hwork : ∀ w : Fin 3, base (.inr w) = []) (initial : Profile q) :
    StateTransition.EvalsToInTime (profileMachine q).step
      ⟨some (labelAt (allPairs q) 0 0), normalState initial, base⟩
      (some ⟨none, normalState (equalityProfile (fun i => base (.inl i))), base⟩)
      (((allPairs q).map (pairTime (fun i => base (.inl i)))).sum + 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.Profile, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.profileMachine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.labelAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.allPairs, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.normalState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.equalityProfile, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.pairTime

  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.pairTime_le line 590
  65. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.totalTime_le line 599
  66. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.profileInTime_bounded line 611

    Source documentation

    A linear bound in the maximum original field length, for fixed q. The actual machine and execution witness are retained.

    def profileInTime_bounded (q : Nat) (base : Tape q → List Bool)
    (hwork : ∀ w : Fin 3, base (.inr w) = []) (initial : Profile q)
    (L : Nat) (hL : ∀ i, (base (.inl i)).length ≤ L) :
    StateTransition.EvalsToInTime (profileMachine q).step
      ⟨some (labelAt (allPairs q) 0 0), normalState initial, base⟩
      (some ⟨none, normalState (equalityProfile (fun i => base (.inl i))), base⟩)
      (q * q * (5 * L + 6) + 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.Profile, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.profileMachine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.labelAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.allPairs, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.normalState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFieldProfile.equalityProfile