OAI/Computability/MaxCut/Games/AddressTupleLoaded.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. abbrev OAI.MaxCutGames.Integration.AddressTupleLoaded.Arena line 10
  2. def OAI.MaxCutGames.Integration.AddressTupleLoaded.fieldAssignment line 16

    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.MaxCutGames.Integration.AddressTupleLoaded.Arena

  3. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.stageTapes_eq line 23
  4. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.fieldAssignment_frame line 49
  5. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_frame line 55
  6. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_field line 63
  7. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_source line 70
  8. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_extra line 76
  9. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_header line 83
  10. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_radix line 91
  11. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_capacity line 99
  12. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_current line 107
  13. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_remaining line 114
  14. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_finalOutput line 121
  15. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_loaderWork line 128
  16. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_privateAddress line 143
  17. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_clean line 153

    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.MaxCutGames.Integration.AddressTupleLoaded.Arena

  18. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_rhs line 172
  19. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_name line 182
  20. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_occurrence line 191
  21. def OAI.MaxCutGames.Integration.AddressTupleLoaded.canonicalValues line 197
  22. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_canonicalField line 204

    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.MaxCutGames.Integration.AddressTupleLoaded.Arena, OAI.MaxCutGames.Integration.AddressTupleLoaded.canonicalValues

  23. theorem OAI.MaxCutGames.Integration.AddressTupleLoaded.loaded_savedFields line 225

    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.MaxCutGames.Integration.AddressTupleLoaded.Arena, OAI.MaxCutGames.Integration.AddressTupleLoaded.canonicalValues

  24. def OAI.MaxCutGames.Integration.AddressTupleCleanup.loadedFields line 248

    Source documentation

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

    def loadedFields : List (AddressMachineSpace.Tape k s d noiseCount) :=
…
  25. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.loadedFields_length line 253
  26. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.mem_loadedFields line 256
  27. abbrev OAI.MaxCutGames.Integration.AddressTupleCleanup.Label line 270
  28. abbrev OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared line 272
  29. abbrev OAI.MaxCutGames.Integration.AddressTupleCleanup.steps line 278

    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) :=
…
  30. abbrev OAI.MaxCutGames.Integration.AddressTupleCleanup.budget line 281
  31. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared_field line 284
  32. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared_outside line 291

    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.MaxCutGames.Integration.AddressTupleCleanup.cleared

  33. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared_source line 300
  34. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared_savedIndex line 306
  35. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared_extra line 313
  36. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared_index line 320
  37. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared_work line 326
  38. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared_scratch line 332
  39. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared_copyScratch line 338
  40. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared_headerTape line 344
  41. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared_current line 352
  42. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared_remaining line 359
  43. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared_finalOutput line 366
  44. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.steps_le line 373
  45. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.steps_le_uniform line 378
  46. abbrev OAI.MaxCutGames.Integration.AddressTupleCleanup.entry line 386
  47. def OAI.MaxCutGames.Integration.AddressTupleCleanup.instruction line 390

    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.MaxCutGames.Integration.AddressTupleCleanup.Label

  48. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.trace line 395
  49. theorem OAI.MaxCutGames.Integration.AddressTupleCleanup.trace_clean line 408
  50. def OAI.MaxCutGames.Integration.AddressTupleCleanup.execution line 420
  51. abbrev OAI.MaxCutGames.Integration.AddressTupleFrame.Arena line 452
  52. theorem OAI.MaxCutGames.Integration.AddressTupleFrame.cleared_outputTapes line 455

    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.MaxCutGames.Integration.AddressTupleFrame.Arena, OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared

  53. theorem OAI.MaxCutGames.Integration.AddressTupleFrame.cleared_appended line 476

    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.MaxCutGames.Integration.AddressTupleFrame.Arena, OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared

  54. theorem OAI.MaxCutGames.Integration.AddressTupleFrame.cleared_fieldAssignment line 488

    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.MaxCutGames.Integration.AddressTupleFrame.Arena, OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared, OAI.MaxCutGames.Integration.AddressTupleLoaded.fieldAssignment

  55. theorem OAI.MaxCutGames.Integration.AddressTupleFrame.cleared_loaded line 496
  56. theorem OAI.MaxCutGames.Integration.AddressTupleFrame.cleared_appended_loaded line 506

    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.MaxCutGames.Integration.AddressTupleFrame.Arena, OAI.MaxCutGames.Integration.AddressTupleCleanup.cleared

  57. abbrev OAI.MaxCutGames.Integration.AddressTupleFrame.finalTapes line 518

    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.MaxCutGames.Integration.AddressTupleFrame.Arena

  58. theorem OAI.MaxCutGames.Integration.AddressTupleFrame.finalTapes_other line 532
  59. theorem OAI.MaxCutGames.Integration.AddressTupleFrame.finalTapes_source line 539
  60. theorem OAI.MaxCutGames.Integration.AddressTupleFrame.finalTapes_current line 544
  61. theorem OAI.MaxCutGames.Integration.AddressTupleFrame.finalTapes_remaining line 551
  62. theorem OAI.MaxCutGames.Integration.AddressTupleFrame.finalTapes_header line 559

    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.MaxCutGames.Integration.AddressTupleFrame.finalTapes

  63. theorem OAI.MaxCutGames.Integration.AddressTupleFrame.finalTapes_radix line 568
  64. theorem OAI.MaxCutGames.Integration.AddressTupleFrame.finalTapes_capacity line 576
  65. theorem OAI.MaxCutGames.Integration.AddressTupleFrame.finalTapes_output line 584
  66. theorem OAI.MaxCutGames.Integration.AddressTupleFrame.finalTapes_clean line 592