OAI/Computability/UniqueGames/Reduction/AddressTupleCleanupLemmas.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

The exact frame after a tuple body and its field cleanup

Loading replaces the initially empty equation-field tapes. Appending writes only the shared reversed-output header, which is outside those fields. The actual field drains therefore restore the original arena with precisely the same appended bytes. Saved occurrence indices and the odometer survive.

  1. def OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.loadedFields line 15

    Source documentation

    The executable field order is slot-major within each tuple position.

    def loadedFields : List (AddressMachineSpace.Tape k s d noiseCount) :=
…
  2. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.loadedFields_length line 20
  3. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.mem_loadedFields line 23
  4. abbrev OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.Label line 37
  5. abbrev OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared line 39
  6. abbrev OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.steps line 45

    Source documentation

    Proof-side cost on the shared arena. Its arithmetic-header tape dimensions use the fixed polynomial coefficient representation in PolynomialMachine. The executable drain list, entry, and instructions do not evaluate this cost.

    noncomputable abbrev steps (base : AddressMachineSpace.Tape k s d noiseCount → List Bool) :=
…
  7. abbrev OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.budget line 48
  8. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared_field line 51
  9. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared_outside line 58

    Source documentation

    Every tape outside the physical loaded fields is preserved verbatim.

    theorem cleared_outside (base : AddressMachineSpace.Tape k s d noiseCount → List Bool)
    (tape : AddressMachineSpace.Tape k s d noiseCount)
    (outside : ∀ position : Fin k, ∀ slot : Fin 4, tape ≠ .field position slot) :
    cleared k s d noiseCount base tape = base tape := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared

  10. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared_source line 67
  11. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared_savedIndex line 73
  12. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared_extra line 80
  13. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared_index line 87
  14. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared_work line 93
  15. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared_scratch line 99
  16. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared_copyScratch line 105
  17. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared_headerTape line 111
  18. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared_current line 119
  19. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared_remaining line 126
  20. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared_finalOutput line 133
  21. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.steps_le line 140
  22. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.steps_le_uniform line 145
  23. abbrev OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.entry line 153
  24. def OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.instruction line 157

    Source documentation

    Fixed concrete drain instructions on the actual shared address state.

    def instruction (labels : Label k s d noiseCount → Λ) (exit : Option Λ) :
    Label k s d noiseCount → TM2.Stmt
      (fun _ : AddressMachineSpace.Tape k s d noiseCount => Bool) Λ (AddressMachineSpace.State k) :=
…

    Mentions: OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.Label

  25. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.trace line 162
  26. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.trace_clean line 175
  27. def OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.execution line 187
  28. abbrev OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.Arena line 212
  29. def OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.fieldAssignment line 218

    Source documentation

    The explicit field assignment performed by all k real lookup stages. Unrelated tapes, including the loader's empty index/work tapes, are unchanged.

    def fieldAssignment (F : SourceEncoding.Input) (tuple : Fin k → Fin F.equations.length)
    (baseArena : Arena k s d noiseCount → List Bool) : Arena k s d noiseCount → List Bool
  | .field j slot => encodeWord
      ((SourceEncoding.equationWords F.equations[(tuple j).val])[slot.val]'(by simp)) ++
        baseArena (.field j slot)
  | tape => baseArena tape

    Mentions: OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.Arena

  30. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.stageTapes_eq line 225
  31. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.fieldAssignment_frame line 251
  32. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_frame line 257
  33. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_field line 265
  34. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_source line 272
  35. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_extra line 278
  36. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_header line 285
  37. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_radix line 293
  38. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_capacity line 301
  39. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_current line 309
  40. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_remaining line 316
  41. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_finalOutput line 323
  42. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_loaderWork line 330
  43. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_privateAddress line 345
  44. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_clean line 355

    Source documentation

    Cleanliness of the actual edge machine is preserved by the actual loader. All of these local work tapes occupy the private disjoint arena block.

    theorem loaded_clean (F : SourceEncoding.Input) (tuple : Fin k → Fin F.equations.length)
    (baseArena : Arena k s d noiseCount → List Bool)
    (clean : MachineAddressEdge.Clean (AddressMachineSpace.addressEdgeSlots k s d noiseCount)
      baseArena) :
    MachineAddressEdge.Clean (AddressMachineSpace.addressEdgeSlots k s d noiseCount)
      (MachineSourceTuple.stageTapes F tuple baseArena k) := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.Arena

  45. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_rhs line 374
  46. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_name line 384
  47. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_occurrence line 393
  48. def OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.canonicalValues line 399
  49. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_canonicalField line 406

    Source documentation

    The three names and the distinct saved occurrence field are exact unary values; the RHS remains on its separate field tape.

    theorem loaded_canonicalField (F : SourceEncoding.Input) (tuple : Fin k → Fin F.equations.length)
    (baseArena : Arena k s d noiseCount → List Bool)
    (hsaved : ∀ j, baseArena (.savedIndex j) = encodeWord (tuple j).val)
    (hempty : ∀ j slot, baseArena (.field j slot) = []) (j : Fin k) (slot : Fin 4) :
    MachineSourceTuple.stageTapes F tuple baseArena k
      (AddressMachineSpace.canonicalField k s d noiseCount j slot) =
        encodeWord (canonicalValues F tuple j slot) := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.Arena, OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.canonicalValues

  50. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.loaded_savedFields line 427

    Source documentation

    Literal input function used by the generic field-template machine.

    theorem loaded_savedFields (F : SourceEncoding.Input) (tuple : Fin k → Fin F.equations.length)
    (baseArena : Arena k s d noiseCount → List Bool)
    (hsaved : ∀ j, baseArena (.savedIndex j) = encodeWord (tuple j).val)
    (hempty : ∀ j slot, baseArena (.field j slot) = []) :
    (fun i => MachineSourceTuple.stageTapes F tuple baseArena k
      (MachineAddressEdge.addressSlots (AddressMachineSpace.addressEdgeSlots k s d noiseCount)
        (.field i))) = CanonicalBodyMachine.savedFields (canonicalValues F tuple) := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.Arena, OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.canonicalValues

  51. abbrev OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.Arena line 462
  52. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.cleared_outputTapes line 465

    Source documentation

    Clearing the physical fields commutes with an append to any other tape.

    theorem cleared_outputTapes (base : Arena k s d noiseCount → List Bool)
    (output : Arena k s d noiseCount) (bits : List Bool)
    (outside : ∀ j : Fin k, ∀ slot : Fin 4, output ≠ .field j slot) :
    AddressTupleCleanup.cleared k s d noiseCount
        (MachineFieldTemplate.outputTapes base output bits) =
      MachineFieldTemplate.outputTapes
        (AddressTupleCleanup.cleared k s d noiseCount base) output bits := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.Arena, OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared

  53. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.cleared_appended line 486

    Source documentation

    The actual edge-output slot is a header tape, not a loaded equation field.

    theorem cleared_appended (base : Arena k s d noiseCount → List Bool) (bits : List Bool) :
    AddressTupleCleanup.cleared k s d noiseCount
        (MachineAddressEdge.appended (AddressMachineSpace.addressEdgeSlots k s d noiseCount)
          base bits) =
      MachineAddressEdge.appended (AddressMachineSpace.addressEdgeSlots k s d noiseCount)
        (AddressTupleCleanup.cleared k s d noiseCount base) bits := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.Arena, OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared

  54. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.cleared_fieldAssignment line 497

    Source documentation

    Cleanup erases exactly the fields assigned by the tuple loader.

    theorem cleared_fieldAssignment (F : SourceEncoding.Input)
    (tuple : Fin k → Fin F.equations.length) (base : Arena k s d noiseCount → List Bool)
    (hfields : ∀ j slot, base (.field j slot) = []) :
    AddressTupleCleanup.cleared k s d noiseCount
      (AddressTupleLoaded.fieldAssignment F tuple base) = base := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.Arena, OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared, OAI.UniqueGamesTheorem.Integration.AddressTupleLoaded.fieldAssignment

  55. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.cleared_loaded line 505
  56. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.cleared_appended_loaded line 515

    Source documentation

    Exact endpoint of load, edge-byte append, and actual loaded-field cleanup.

    theorem cleared_appended_loaded (F : SourceEncoding.Input)
    (tuple : Fin k → Fin F.equations.length) (base : Arena k s d noiseCount → List Bool)
    (hindex : base .index = []) (hwork : base .work = [])
    (hfields : ∀ j slot, base (.field j slot) = []) (bits : List Bool) :
    AddressTupleCleanup.cleared k s d noiseCount
        (MachineAddressEdge.appended (AddressMachineSpace.addressEdgeSlots k s d noiseCount)
          (MachineSourceTuple.stageTapes F tuple base k) bits) =
      MachineAddressEdge.appended (AddressMachineSpace.addressEdgeSlots k s d noiseCount)
        base bits := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.Arena, OAI.UniqueGamesTheorem.Integration.AddressTupleCleanup.cleared

  57. abbrev OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.finalTapes line 527

    Source documentation

    Literal final arena; this abbreviation contains no execution assumption.

    noncomputable abbrev finalTapes (F : SourceEncoding.Input) (tuple : Fin k → Fin F.equations.length)
    (base : Arena k s d noiseCount → List Bool) (bits : List Bool) :
    Arena k s d noiseCount → List Bool :=
…

    Mentions: OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.Arena

  58. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.finalTapes_other line 543
  59. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.finalTapes_source line 550
  60. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.finalTapes_current line 554
  61. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.finalTapes_remaining line 561
  62. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.finalTapes_header line 569

    Source documentation

    All arithmetic headers except the reversed-output tape remain literal.

    theorem finalTapes_header (header : MachineAddressHeaders.Arithmetic.Control)
    (hne : header ≠ .reversed) :
    finalTapes F tuple base bits (AddressMachineSpace.headerTape k s d noiseCount header) =
      base (AddressMachineSpace.headerTape k s d noiseCount header) := by
…

    Mentions: OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.finalTapes

  63. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.finalTapes_radix line 578
  64. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.finalTapes_capacity line 586
  65. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.finalTapes_output line 594
  66. theorem OAI.UniqueGamesTheorem.Integration.AddressTupleFrame.finalTapes_clean line 602