OAI/Computability/MaxCut/Games/AddressOdometerSchedule.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MaxCutGames.Reduction.AddressOdometerSchedule.Tape line 16
  2. def OAI.MaxCutGames.Reduction.AddressOdometerSchedule.current line 20
  3. def OAI.MaxCutGames.Reduction.AddressOdometerSchedule.remaining line 23
  4. def OAI.MaxCutGames.Reduction.AddressOdometerSchedule.accumulator line 26
  5. def OAI.MaxCutGames.Reduction.AddressOdometerSchedule.currentAt line 29
  6. def OAI.MaxCutGames.Reduction.AddressOdometerSchedule.remainingAt line 32
  7. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.current_eq_iff line 35
  8. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.remaining_eq_iff line 38
  9. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.current_ne_remaining line 41
  10. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.remaining_ne_current line 44
  11. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.accumulator_ne_current line 47
  12. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.accumulator_ne_remaining line 50
  13. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.current_ne_accumulator line 53
  14. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.remaining_ne_accumulator line 55
  15. def OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setDigits line 60

    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.MaxCutGames.Reduction.AddressOdometerSchedule.Tape

  16. def OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setAcc line 68
  17. def OAI.MaxCutGames.Reduction.AddressOdometerSchedule.putDigit line 71
  18. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setDigits_current line 75
  19. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setDigits_remaining line 80
  20. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setDigits_other line 86
  21. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.digitCases_inline_AddressOdometerSchedule line 102
  22. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setDigits_zero line 114
  23. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setDigits_accumulator line 122
  24. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setAcc_self line 126
  25. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setAcc_setAcc line 128
  26. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setAcc_apply line 130
  27. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setDigits_setAcc line 133
  28. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.putDigit_current line 145
  29. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.putDigit_remaining line 150
  30. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.putDigit_other line 156
  31. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.putDigit_accumulator line 162
  32. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.putDigit_setAcc line 167
  33. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setDigits_putDigit line 179
  34. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setDigits_snoc line 198
  35. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setDigits_snoc_base line 231
  36. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setDigits_savedIndex line 237
  37. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.setAcc_other line 243
  38. def OAI.MaxCutGames.Reduction.AddressOdometerSchedule.allBits line 248
  39. def OAI.MaxCutGames.Reduction.AddressOdometerSchedule.blockPrefix line 251
  40. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.blockPrefix_eq_ofFn line 255
  41. def OAI.MaxCutGames.Reduction.AddressOdometerSchedule.blocks line 264
  42. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.blockPrefix_all line 267
  43. def OAI.MaxCutGames.Reduction.AddressOdometerSchedule.configuration line 274
  44. def OAI.MaxCutGames.Reduction.AddressOdometerSchedule.BodyTrace line 277
  45. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.val_snoc line 288
  46. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.zeros_snoc line 294
  47. def OAI.MaxCutGames.Reduction.AddressOdometerSchedule.initialConfiguration line 299
  48. def OAI.MaxCutGames.Reduction.AddressOdometerSchedule.finalConfiguration line 303
  49. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.exists_schedule line 309
  50. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.traversalInTime line 443

    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.MaxCutGames.Reduction.AddressOdometerSchedule.Tape, OAI.MaxCutGames.Reduction.AddressOdometerSchedule.currentAt, OAI.MaxCutGames.Reduction.AddressOdometerSchedule.remainingAt, OAI.MaxCutGames.Reduction.AddressOdometerSchedule.BodyTrace, OAI.MaxCutGames.Reduction.AddressOdometerSchedule.initialConfiguration

  51. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.initial_current line 464
  52. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.initial_remaining line 469
  53. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.final_current line 474
  54. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.final_remaining line 480
  55. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.final_accumulator line 486
  56. theorem OAI.MaxCutGames.Reduction.AddressOdometerSchedule.final_other line 494

    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.MaxCutGames.Reduction.AddressOdometerSchedule.Tape, OAI.MaxCutGames.Reduction.AddressOdometerSchedule.current, OAI.MaxCutGames.Reduction.AddressOdometerSchedule.remaining, OAI.MaxCutGames.Reduction.AddressOdometerSchedule.accumulator, OAI.MaxCutGames.Reduction.AddressOdometerSchedule.finalConfiguration