OAI/Computability/UniqueGames/Reduction/AddressOdometerSchedule.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.Tape line 17
  2. def OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.current line 21
  3. def OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.remaining line 24
  4. def OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.accumulator line 27
  5. def OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.currentAt line 30
  6. def OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.remainingAt line 33
  7. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.current_eq_iff line 36
  8. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.remaining_eq_iff line 39
  9. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.current_ne_remaining line 42
  10. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.remaining_ne_current line 45
  11. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.accumulator_ne_current line 48
  12. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.accumulator_ne_remaining line 51
  13. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.current_ne_accumulator line 54
  14. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.remaining_ne_accumulator line 56
  15. def OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setDigits line 61

    Source documentation

    Odometer coordinate zero is the low coordinate; physical saved positions are reversed to match the actual occurrence-tuple enumeration.

    def setDigits (m : ℕ) {q : ℕ} (digits : Fin q → ℕ)
    (base : Tape k s d noiseCount → List Bool) : Tape k s d noiseCount → List Bool
  | .savedIndex i => if h : i.rev.val < q then encodeWord (digits ⟨i.rev.val, h⟩)
      else base (.savedIndex i)
  | .extra (.inr (.inr (.inl i))) => if h : i.val < q then encodeWord (m - 1 - digits ⟨i.val, h⟩)
      else base (.extra (.inr (.inr (.inl i))))
  | tape => base tape

    Mentions: OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.Tape

  16. def OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setAcc line 69
  17. def OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.putDigit line 72
  18. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setDigits_current line 76
  19. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setDigits_remaining line 81
  20. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setDigits_other line 87
  21. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.digitCases line 103
  22. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setDigits_zero line 115
  23. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setDigits_accumulator line 123
  24. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setAcc_self line 127
  25. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setAcc_setAcc line 129
  26. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setAcc_apply line 131
  27. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setDigits_setAcc line 134
  28. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.putDigit_current line 146
  29. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.putDigit_remaining line 151
  30. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.putDigit_other line 157
  31. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.putDigit_accumulator line 163
  32. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.putDigit_setAcc line 168
  33. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setDigits_putDigit line 180
  34. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setDigits_snoc line 199
  35. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setDigits_snoc_base line 232
  36. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setDigits_savedIndex line 238
  37. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.setAcc_other line 244
  38. def OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.allBits line 249
  39. def OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.blockPrefix line 252
  40. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.blockPrefix_eq_ofFn line 256
  41. def OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.blocks line 265
  42. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.blockPrefix_all line 268
  43. def OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.configuration line 275
  44. def OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.BodyTrace line 278
  45. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.val_snoc line 289
  46. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.zeros_snoc line 295
  47. def OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.initialConfiguration line 300
  48. def OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.finalConfiguration line 304
  49. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.exists_schedule line 310
  50. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.traversalInTime line 444

    Source documentation

    The time bound is derived from the concrete schedule, not from the number of tuples alone. Dimension zero consists of its single actual body trace.

    theorem traversalInTime
    (program : Λ → TM2.Stmt (fun _ : Tape k s d noiseCount => Bool) Λ (σ × Option Bool))
    (bodyLabel : Λ) (next resetLabel : ℕ → Λ) (canonical : σ)
    (positive : 0 < m) (B : ℕ) (base : Tape k s d noiseCount → List Bool)
    (bits : (Fin k → Fin m) → List Bool)
    (atCheck : ∀ i, i < k → program (next i) =
      increment (currentAt k s d noiseCount i) (remainingAt k s d noiseCount i) bodyLabel (resetLabel i))
    (atReset : ∀ i, i < k → program (resetLabel i) =
      reset (currentAt k s d noiseCount i) (remainingAt k s d noiseCount i) (resetLabel i) (next (i + 1)))
    (bodies : BodyTrace program bodyLabel (next 0) canonical base bits B) :
    Nonempty (StateTransition.EvalsToInTime (TM2.step program)
      (initialConfiguration (m := m) k bodyLabel canonical base)
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.Tape, OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.currentAt, OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.remainingAt, OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.BodyTrace, OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.initialConfiguration

  51. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.initial_current line 465
  52. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.initial_remaining line 470
  53. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.final_current line 475
  54. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.final_remaining line 481
  55. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.final_accumulator line 487
  56. theorem OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.final_other line 495

    Source documentation

    Traversal frames every tape outside the digits and reversed output.

    theorem final_other (base : Tape k s d noiseCount → List Bool)
    (exitLabel : Λ) (canonical : σ) (bits : (Fin k → Fin m) → List Bool)
    (tape : Tape k s d noiseCount)
    (hc : ∀ i, tape ≠ current k s d noiseCount i)
    (hr : ∀ i, tape ≠ remaining k s d noiseCount i)
    (ha : tape ≠ accumulator k s d noiseCount) :
    (finalConfiguration exitLabel canonical base bits).stk tape = base tape := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.Tape, OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.current, OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.remaining, OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.accumulator, OAI.UniqueGamesTheorem.Reduction.AddressOdometerSchedule.finalConfiguration