OAI/Computability/MaxCut/Machines/MachinePaddedOverlay.lean

GitHub source file

73 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.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.BaseTable line 22
  2. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.baseDegree line 23
  3. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.overlayDegree line 24
  4. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.Tape line 25
  5. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.Alphabet line 26
  6. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.Label line 27
  7. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.State line 28
  8. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.overlayDegree_positive line 30
  9. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.paddingTape line 33
  10. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.paddingView line 35
  11. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.paddingView_left line 39
  12. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.paddingView_right line 41
  13. def OAI.MaxCutGames.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.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Tape, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.Tape

  14. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.familyView line 51
  15. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.familyView_left line 56
  16. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.familyView_right line 61
  17. def OAI.MaxCutGames.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.MaxCutGames.Foundations.Complexity.MachineOverlayTable.Tape, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.Tape

  18. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.overlayView line 75
  19. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.overlayView_left line 82
  20. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.overlayView_right line 89
  21. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.paddingLabel line 107
  22. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.familyLabel line 108
  23. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.overlayLabel line 109
  24. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.main line 110
  25. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.familyEntry line 111
  26. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.overlayEntry line 112
  27. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.familyStates line 114
  28. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.overlayStates line 122
  29. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.familySource line 130
  30. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.overlaySource line 135
  31. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.program line 140
  32. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.clean line 147
  33. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.memory line 153

    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.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.padded, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.rotor, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.memory, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.output

  34. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.padded line 160
  35. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.rotor line 163
  36. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.initialTapes line 167
  37. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.paddedTapes line 170
  38. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.familyTapes line 174
  39. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.finalTapes line 178
  40. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.placeExecution_inline_MachinePaddedOverlay line 183
  41. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.padding_initial_memory line 199
  42. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.padding_final_memory line 211
  43. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.paddingInTime line 225

    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.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.program, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.main, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.clean, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.initialTapes, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.familyEntry, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.paddedTapes, OAI.MaxCutGames.Foundations.Complexity.MachineVertexPadding.timePolynomial

  44. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.family_initial_memory line 238
  45. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.family_final_memory line 261
  46. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.familyInTime line 292

    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.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.program, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.familyEntry, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.clean, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.paddedTapes, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.overlayEntry, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.familyTapes, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.inputCoefficient

  47. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.rotationWords_resize line 350
  48. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.rotor_familyAt line 356
  49. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.overlay_memory line 362
  50. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.overlayInTime line 386

    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.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.program, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.overlayEntry, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.clean, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.familyTapes, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.finalTapes, OAI.MaxCutGames.Foundations.Complexity.MachineOverlayTable.timePolynomial, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.overlayDegree, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.padded, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.rotor

  51. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.sizePolynomial line 423

    Source documentation

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

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

    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.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.archive_length_le line 434
  54. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.familyPolynomial line 459
  55. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.timePolynomial line 462
  56. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.execution line 468

    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.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.program, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.main, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.clean, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.initialTapes, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.finalTapes, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.timePolynomial

  57. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.machine line 494
  58. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.alphabet_finite line 505
  59. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.initial_configuration line 511
  60. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.final_output line 528
  61. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.original_preserved line 534
  62. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.rawProgram line 545
  63. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.sourceMachine_eq line 553
  64. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.cleanupTapes line 559

    Source documentation

    A fixed finite list of every non-output stack. This includes both retained archives, the original input, and the physically consumed level.

    noncomputable def cleanupTapes : List Tape :=
…
  65. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.cleanup_complete line 562
  66. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.initial_configuration line 566
  67. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.terminalRun line 577

    Source documentation

    The raw terminal witness is the actual three-phase execution. No phase trace, output-size bound, or complexity assertion is an input hypothesis.

    noncomputable def terminalRun (H : BaseTable) (d : Nat) (hd : 0 < d)
    (a : PortTables.Input d) :
    MachineCanonicalOutput.TerminalRun (rawProgram H d hd) (PortTables.inputBits a)
      (PortTables.inputBits (PreprocessingStageMaps.paddedOverlay H d a))
      ((MachinePaddedOverlay.timePolynomial d).eval (PortTables.inputBits a).length) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.TerminalRun, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.rawProgram, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlay.timePolynomial

  68. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.computableInPolyTime line 591

    Source documentation

    A concrete machine reaches the canonical haltList encoding of the existing executable preprocessing map in polynomial time.

    noncomputable def computableInPolyTime (H : BaseTable) (d : Nat) (hd : 0 < d) :
    TM2ComputableInPolyTime (PortTables.inputBits (ports := d))
…
  69. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.finite_alphabet line 601

    Source documentation

    Finiteness belongs to the exact machine stored in the certificate above.

    theorem finite_alphabet (H : BaseTable) (d : Nat) (hd : 0 < d) :
    ∀ k, Finite ((computableInPolyTime H d hd).tm.Γ k) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.computableInPolyTime

  70. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyCodec.rowsBits_ofFn line 614
  71. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyCodec.encodeWords_flatMap_inline_MachineLazyCodec line 631
  72. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyCodec.rowBits_stay line 637
  73. theorem OAI.MaxCutGames.Foundations.Complexity.MachineLazyCodec.rowsBits_stay line 644