OAI/Computability/UniqueGames/Reduction/AddressMachineSpace.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.Extra line 15
  2. abbrev OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.Tape line 19
  3. abbrev OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.Control line 22
  4. abbrev OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.State line 23
  5. def OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.initialState line 25
  6. def OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.headerArithmeticSlots line 29
  7. def OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.headerTape line 34
  8. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.headerTape_eq_iff line 37
  9. def OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.fullHeaderSlots line 41
  10. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.fullHeaderSlots_source line 53
  11. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.fullHeaderSlots_work line 54
  12. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.fullHeaderSlots_arithmetic line 55
  13. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.arithmeticSlots_fullHeaderSlots line 58
  14. def OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.prefixSlots line 62
  15. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.prefixSlots_source line 65
  16. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.prefixSlots_work line 66
  17. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.prefixSlots_variables line 67
  18. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.prefixSlots_occurrences line 69
  19. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.prefixSlots_scratch line 71
  20. def OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.canonicalField line 74
  21. def OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.rhsField line 77
  22. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.canonicalField_occurrence line 79
  23. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.canonicalField_name line 82
  24. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.canonicalField_ne_rhsField line 93
  25. def OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.privateAddress line 97
  26. def OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.edgeSlot line 100
  27. def OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.edgeDecode line 111

    Source documentation

    A partial inverse proves separation without a default element of Fin k. It therefore applies unchanged at k = 0.

    private def edgeDecode : Tape k s d noiseCount →
    Option (MachineAddressEdge.Tape (4 * k) (1 + 9 * k))
  | .savedIndex j => some (.inl (.field (CanonicalBodyMachine.fieldIndex j 3)))
  | .field j slot => if slot = 3 then none
      else some (.inl (.field (CanonicalBodyMachine.fieldIndex j slot)))
  | .extra (.inl (.inl .baseValue)) => some (.inl .radix)
  | .extra (.inl (.inl .capacity)) => some (.inr 0)
  | .extra (.inl (.inl .reversed)) => some (.inr 1)
  | .extra (.inr (.inl tape)) => some (.inl tape)
  | _ => none

    Mentions: OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.Tape, OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.Tape, OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.fieldIndex

  28. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.edgeDecode_canonicalField line 122
  29. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.edgeDecode_edgeSlot line 127
  30. def OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.addressEdgeSlots line 137
  31. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.addressEdgeSlots_fieldIndex line 145
  32. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.addressSlots_name line 156
  33. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.addressSlots_occurrence line 163
  34. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.addressSlots_radix line 169
  35. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.addressSlots_capacity line 172
  36. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.addressSlots_output line 175
  37. def OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.current line 179
  38. def OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.remaining line 180
  39. def OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.finalOutput line 181
  40. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.current_rev line 183
  41. def OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.odometerSlots line 186
  42. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.odometerSlots_radix line 197
  43. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.odometerSlots_scratch line 199
  44. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.odometerSlots_current line 200
  45. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.odometerSlots_remaining line 202
  46. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.current_ne_remaining line 205
  47. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.current_ne_finalOutput line 207
  48. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.remaining_ne_finalOutput line 209
  49. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.edgeSlot_ne_of_decode_none line 212
  50. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.addressEdgeSlots_ne_rhsField line 220
  51. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.addressEdgeSlots_ne_source line 225
  52. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.addressEdgeSlots_ne_copyScratch line 230
  53. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.addressEdgeSlots_ne_headerTape line 237

    Source documentation

    Only the radix, capacity, and reversed accumulator intentionally overlap the address emitter's tapes with the arithmetic block.

    theorem addressEdgeSlots_ne_headerTape
    (tape : MachineAddressEdge.Tape (4 * k) (1 + 9 * k))
    (c : MachineAddressHeaders.Arithmetic.Control)
    (hb : c ≠ .baseValue) (hc : c ≠ .capacity) (hr : c ≠ .reversed) :
    addressEdgeSlots k s d noiseCount tape ≠ headerTape k s d noiseCount c := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.Tape, OAI.UniqueGamesTheorem.Reduction.MachineAddressHeaders.Arithmetic.Control, OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.addressEdgeSlots, OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.headerTape

  54. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.addressEdgeSlots_ne_remaining line 245
  55. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.addressEdgeSlots_ne_finalOutput line 250
  56. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.headerTape_ne_finalOutput line 255
  57. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.headerTape_ne_current line 259
  58. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.headerTape_ne_remaining line 263
  59. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.tupleOutput_headerTape line 267
  60. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.tupleOutput_source line 277
  61. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.tupleOutput_rhs line 282
  62. theorem OAI.UniqueGamesTheorem.Reduction.AddressMachineSpace.tupleOutput_occurrence line 290