OAI/Computability/UniqueGames/Machines/MachinePaddedOverlay.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Physical composition of vertex padding, expander generation, and overlay

The level produced by vertex padding is the family machine's actual input stack. The two resulting archives are the overlay machine's actual archive stacks. Static tape placement and finite-state framing preserve the original input; no copying or recomputation is hidden in a phase boundary.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.BaseTable line 22
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.baseDegree line 23
  3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.overlayDegree line 24
  4. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.Tape line 25
  5. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.Alphabet line 26
  6. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.Label line 27
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.State line 28
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.overlayDegree_positive line 30
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.paddingTape line 33
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.paddingView line 35
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.paddingView_left line 39
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.paddingView_right line 41
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familyTape line 48

    Source documentation

    The family unary guard consumes the padding machine's existing level.

    def familyTape (k : MachineExpanderFamily.Tape) : Tape :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.Tape

  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familyView line 51
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familyView_left line 56
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familyView_right line 61
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.overlayTape line 70

    Source documentation

    Overlay reads exactly the two archives written by the previous phases.

    def overlayTape (k : MachineOverlayTable.Tape) : Tape :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.Tape

  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.overlayView line 75
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.overlayView_left line 82
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.overlayView_right line 89
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.paddingLabel line 109
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familyLabel line 110
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.overlayLabel line 111
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.main line 112
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familyEntry line 113
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.overlayEntry line 114
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familyStates line 116
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.overlayStates line 124
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familySource line 132
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.overlaySource line 137
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.program line 142
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.clean line 149
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.memory line 155

    Source documentation

    The archives, family count, and level residue are the only retained non-output stacks. Work stacks, including unused duplicate slots, are empty.

    def memory (input padded level rotor count output : List Bool) : Tape → List Bool
  | .inl k => MachineVertexPadding.memory input padded [] [] [] level [] [] k
  | .inr (.inl (.inl (.inl .table))) => rotor
  | .inr (.inl (.inr .currentSize)) => count
  | .inr (.inl _) => []
  | .inr (.inr k) => if k = MachineOverlayTable.output then output else []

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.padded, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.rotor, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.memory, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.output

  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.padded line 162
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.rotor line 165
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.initialTapes line 169
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.paddedTapes line 172
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familyTapes line 176
  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.finalTapes line 180
  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.placeExecution line 185
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.padding_initial_memory line 201
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.padding_final_memory line 213
  43. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.paddingInTime line 227

    Source documentation

    The actual padding execution stops at the family entry on the same physical level stack, and preserves both inactive finite states.

    noncomputable def paddingInTime (H : BaseTable) {n d : Nat} (hd : 0 < d) (t : PortTables.Table n d) :
    StateTransition.EvalsToInTime (TM2.step (program H d hd))
      ⟨some main, clean H d hd, initialTapes t⟩
      (some ⟨some familyEntry, clean H d hd, paddedTapes t⟩)
      ((MachineVertexPadding.timePolynomial d).eval (PortTables.tableBits t).length) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.main, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familyEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.paddedTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineVertexPadding.timePolynomial

  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.family_initial_memory line 240
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.family_final_memory line 263
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familyInTime line 294

    Source documentation

    The second phase executes the checked family program from the already materialized level. Its runtime is polynomial in the original vertex count.

    noncomputable def familyInTime (H : BaseTable) {n d : Nat} (hd : 0 < d)
    (t : PortTables.Table n d) :
    StateTransition.EvalsToInTime (TM2.step (program H d hd))
      ⟨some familyEntry, clean H d hd, paddedTapes t⟩
      (some ⟨some overlayEntry, clean H d hd, familyTapes H t⟩)
      (MachineExpanderFamilyBounds.inputCoefficient * (n + 1)^5) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familyEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.paddedTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.overlayEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familyTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.inputCoefficient

  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.rotationWords_resize line 352
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.rotor_familyAt line 358
  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.overlay_memory line 365
  50. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.overlayInTime line 388

    Source documentation

    Overlay executes on the two archives physically produced above; only its output stack changes in the retained outside frame.

    noncomputable def overlayInTime (H : BaseTable) {n d : Nat} (hd : 0 < d)
    (t : PortTables.Table n d) :
    StateTransition.EvalsToInTime (TM2.step (program H d hd))
      ⟨some overlayEntry, clean H d hd, familyTapes H t⟩
      (some ⟨none, clean H d hd, finalTapes H t⟩)
      ((MachineOverlayTable.timePolynomial d overlayDegree).eval
        ((PortTables.tableBits (padded t)).length + (rotor H n).length)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.overlayEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familyTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.finalTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayTable.timePolynomial, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.overlayDegree, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.padded, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.rotor

  51. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.sizePolynomial line 425

    Source documentation

    The actual padded vertex count is linear in the original encoded size.

    noncomputable def sizePolynomial : Polynomial Nat :=
…
  52. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.archivePolynomial line 430

    Source documentation

    Full unary lengths of both physical archives, including all graph predicate entries, all delimiters, and all expander reverse addresses.

    noncomputable def archivePolynomial (d : Nat) : Polynomial Nat :=
…
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.archive_length_le line 436
  54. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.familyPolynomial line 461
  55. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.timePolynomial line 464
  56. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.execution line 470

    Source documentation

    The complete three-phase program executes from the original serialized input alone, with a polynomial bound in that input's full unary length.

    noncomputable def execution (H : BaseTable) {n d : Nat} (hd : 0 < d)
    (t : PortTables.Table n d) :
    StateTransition.EvalsToInTime (TM2.step (program H d hd))
      ⟨some main, clean H d hd, initialTapes t⟩
      (some ⟨none, clean H d hd, finalTapes H t⟩)
      ((timePolynomial d).eval (PortTables.tableBits t).length) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.main, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.finalTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.timePolynomial

  57. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.machine line 496
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.alphabet_finite line 507
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.initial_configuration line 513
  60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.final_output line 530
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedOverlay.original_preserved line 536