OAI/Computability/MaxCut/Machines/MachineExpanderTableRows.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

Actual execution of all expander-table positions for one vertex

The inner loop calls the complete row machine once per fixed cloud/port position. The returned state and the successful machine execution are constructed together. Neither a row execution nor an inner-loop execution is a caller premise.

  1. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.singleStep_inline_MachineExpanderTableRows line 21
  2. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.sequence_inline_MachineExpanderTableRows line 27
  3. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.widen_inline_MachineExpanderTableRows line 34
  4. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.tableRowData line 40
  5. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.tableRowData_finalValue line 44
  6. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.tableRowData_frame0 line 48
  7. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.tableRowData_finalFrame line 55
  8. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.rowAfterState line 68
  9. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.rowAfterState_position line 74
  10. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.caller_rowAfterState line 79
  11. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.preparedRowInTime line 85

    Source documentation

    Preparation and one actual embedded row call, with the two extra tapes retained. The row value is computed from the actual old and small tables.

    def preparedRowInTime (positive : 0 < d) (G : Table v (degree d))
    (H : Table (cloudSize d) d) (vertex : Fin v) (state : State ρ d)
    (remaining : Nat) (output countSuffix result : List Bool) :
    StateTransition.EvalsToInTime (TM2.step (program positive H))
      ⟨some (.inr .prepareRow), state,
        boundaryTapes vertex.val remaining (encodeWords (rotationWords G)) output countSuffix result⟩
      (some ⟨some (.inr .afterRow), rowAfterState positive G H vertex state,
        boundaryTapes vertex.val remaining (encodeWords (rotationWords G))
          ((encodeWord (rowValue G H vertex state.2)).reverse ++ output) countSuffix result⟩)
      (1 + 80 * ((encodeWords (rotationWords G)).length + 1)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.rowAfterState, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  12. structure OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.VertexSuffixRun line 116

    Source documentation

    A successful suffix of the finite position loop, returning actual finite state together with the execution certificate and its preserved caller.

    structure VertexSuffixRun (positive : 0 < d) (G : Table v (degree d))
    (H : Table (cloudSize d) d) (vertex : Fin v) (state : State ρ d)
    (remaining : Nat) (output countSuffix result : List Bool) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State

  13. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.suffixRun_aux_inline_MachineExpanderTableRows line 130
  14. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.suffixInTime line 184
  15. structure OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.VertexRun line 192

    Source documentation

    The complete inner loop for one vertex, starting at position zero.

    structure VertexRun (positive : 0 < d) (G : Table v (degree d))
    (H : Table (cloudSize d) d) (vertex : Fin v) (state : State ρ d)
    (remaining : Nat) (output countSuffix result : List Bool) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State

  16. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.vertexInTime line 206
  17. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.oldTableWord line 233
  18. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices line 236
  19. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_zero line 240
  20. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_succ line 244
  21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_full line 250
  22. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.vertexBodyBudget line 255
  23. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.vertexLoopBudget line 258
  24. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.vertexLoopTapes line 261
  25. structure OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.VertexLoopRun line 265
  26. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.boundarySingleStep_inline_MachineExpanderTableLoop line 276
  27. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.vertexLoopInTime line 283

    Source documentation

    Execute every remaining vertex in the common finite table program.

    def vertexLoopInTime {v d : Nat} {ρ : Type} [Fintype ρ]
    (positive : 0 < d) (G : Table v (degree d)) (H : Table (cloudSize d) d)
    (current remaining : Nat) (state : State ρ d) (suffix : List Bool)
    (count : current + remaining = v) (position : state.2 = zeroPosition positive) :
    VertexLoopRun positive G H current remaining state suffix := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.zeroPosition, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.VertexLoopRun

  28. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.clearRegister_position line 341
  29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.clearRegister_register line 344
  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.clearRegister_idempotent line 347
  31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes_reverse_update line 350
  32. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.reverseOutputTrace line 368

    Source documentation

    Exact execution of the entire final reverse loop, including its empty test. No reversal-execution hypothesis is assumed.

    theorem reverseOutputTrace (positive : 0 < d) (H : Table (cloudSize d) d)
    (vertex remaining : Nat) (oldTable output countSuffix result : List Bool)
    (state : State ρ d) :
    (advance (TM2.step (program positive H)))^[output.length + 1]
      (some ⟨some (.inr .reverseOutput), state,
        boundaryTapes vertex remaining oldTable output countSuffix result⟩) =
      some ⟨some (.inr .done), clearRegister state,
        boundaryTapes vertex remaining oldTable [] countSuffix (output.reverse ++ result)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.clearRegister

  33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.reverseOutputHaltTrace line 401

    Source documentation

    The actual done statement halts one transition after reversal completes.

    theorem reverseOutputHaltTrace (positive : 0 < d) (H : Table (cloudSize d) d)
    (vertex remaining : Nat) (oldTable output countSuffix result : List Bool)
    (state : State ρ d) :
    (advance (TM2.step (program positive H)))^[output.length + 2]
      (some ⟨some (.inr .reverseOutput), state,
        boundaryTapes vertex remaining oldTable output countSuffix result⟩) =
      some ⟨none, clearRegister state,
        boundaryTapes vertex remaining oldTable [] countSuffix (output.reverse ++ result)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.clearRegister

  34. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.reverseOutputInTime line 416
  35. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.reverseOutputHaltInTime line 429
  36. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.completeBudget line 459
  37. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.timeCoefficient line 462
  38. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.timePolynomial line 465
  39. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.vertices_le_word_length line 468
  40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.completeBudget_le line 478

    Source documentation

    All actual loop, row, and final reversal costs are bounded quadratically.

    theorem completeBudget_le {v d : Nat} (positive : 0 < d)
    (G : Table v (degree d)) (H : Table (cloudSize d) d) :
    completeBudget G H ≤ (timePolynomial d).eval (oldTableWord G).length := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.completeBudget, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.timePolynomial, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.oldTableWord

  41. structure OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.TableRun line 513
  42. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.initializeInTime_inline_MachineExpanderTable line 525
  43. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.tableInTime line 544

    Source documentation

    Construct the entire table execution from its actual initialized inputs. No row trace, loop trace, or abstract computational witness is a hypothesis.

    def tableInTime {v d : Nat} {ρ : Type} [Fintype ρ]
    (positive : 0 < d) (G : Table v (degree d)) (H : Table (cloudSize d) d)
    (state : State ρ d) (suffix : List Bool) : TableRun positive G H state suffix := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderTable.TableRun

  44. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.cycleWords line 579

    Source documentation

    The six nonempty tape roles that may occur between expansion phases.

    def cycleWords (remaining : Nat) (word current vertex count result suffix : List Bool) :
    Tape → List Bool
  | .inl (.inl .table) => word
  | .inl (.inl .inputVertex) => vertex
  | .inl (.inr .vertexCount) => count
  | .inl (.inr .result) => result
  | .inr .remainingLevel => encodeWord remaining ++ suffix
  | .inr .currentSize => current
  | _ => []

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Tape, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  45. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.cycleTapes line 589
  46. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.toBool_cycleTapes line 593
  47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes_eq_cycleTapes line 598
  48. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.copyFrame line 608
  49. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.returnFrame line 613
  50. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.installedFrame line 618
  51. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.multipliedFrame line 622
  52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.copyFrame_eq_cycleTapes line 627
  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.returnFrame_eq_cycleTapes line 639
  54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.copyFrame_eq_update line 653
  55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.multipliedFrame_eq_update line 664
  56. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCost line 690
  57. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCoefficient line 696
  58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.wordLength_add_one_le line 701

    Source documentation

    The complete unary encoding, including every word delimiter, is counted.

    theorem wordLength_add_one_le {v q N : Nat} (G : Table v q) (hv : v ≤ N) :
    (encodeWords (rotationWords G)).length + 1 ≤ (q + 1)^2 * (N + 1)^2 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWords

  59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCost_le line 712
  60. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.vertexCount_monotone line 750
  61. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.level_le_vertexCount line 756
  62. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum line 768
  63. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_zero line 771
  64. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_succ line 774
  65. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_add line 778
  66. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget line 783
  67. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_zero line 786
  68. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_succ line 789
  69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_le line 795
  70. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_le line 823

    Source documentation

    All actual resize costs plus the counted-loop overhead.

    theorem familyBudget_le {d : Nat} (H : Table (cloudSize d) d)
    (growth : 1 < cloudSize d) (level : Nat) :
    familyBudget H level ≤
      (resizeCoefficient d + 4) * (vertexCount (degree d) level + 1)^5 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCoefficient

  71. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.paddedSize_le_succ_input line 837
  72. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.inputCoefficient line 847
  73. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_at_boundedLevel_le line 852

    Source documentation

    For the fixed base graph, the bounded padding level has a polynomial cost in the requested unary size, including size zero.

    theorem familyBudget_at_boundedLevel_le
    (H : Table (cloudSize PCP.Expanders.baseDegree) PCP.Expanders.baseDegree) (k : Nat) :
    familyBudget H (PCP.PreprocessingLevels.boundedLevel k) ≤ inputCoefficient * (k + 1)^5 := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.Expanders.baseDegree, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget, OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.boundedLevel, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamilyBounds.inputCoefficient