OAI/Computability/MaxCut/Machines/RuntimeModel.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

Fixed natural polynomials are represented by literal Horner coefficients. The coefficient representation is independent of the machine input. The actual machine wrapper is built from the shared physical unary Horner subroutine.

  1. inductive OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.BodyWork line 11
  2. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.BodyExtra line 19
  3. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.Arena line 20
  4. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.QueryState line 21
  5. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.ArithmeticState line 22
  6. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.State line 23
  7. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.QueryMetadata line 24
  8. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.ArithmeticMetadata line 26
  9. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.workTape line 31
  10. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.variableHeader line 32
  11. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.clauseHeader line 33
  12. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.canonicalSignature line 35
  13. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.canonicalState line 38
  14. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.queryStateEquiv line 42
  15. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.arithmeticStateEquiv line 48
  16. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.rankControls line 54
  17. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.clauseRankSlots line 64
  18. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.variableRankSlots line 67
  19. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.baseSlots line 72

    Source documentation

    Both address-base phases use the same clean arithmetic work tapes. The right side adds the retained left block; the left side adds a seeded zero.

    def baseSlots (right : Bool) : MachineHorner.Layout 2 ↪ Arena u Extra where
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.Arena

  20. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.querySources line 94
  21. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.queryLayout line 99
  22. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.perSlotCleanup line 112

    Source documentation

    Retained global headers are excluded from cleanup.

    def perSlotCleanup : List (Arena u Extra) := [workTape .rank, workTape .leftBase]

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.Arena, OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.workTape

  23. def OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.finalBaseCleanup line 113
  24. theorem OAI.MaxCutGames.Foundations.Hastad.SourceRuntimeModel.initializer_arena line 115
  25. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial line 126
  26. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial_eval line 130
  27. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial_eval_reverse line 136
  28. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficients line 143

    Source documentation

    An actual finite coefficient list for every fixed natural polynomial. No evaluation of an input is included in this static representation choice.

    noncomputable def coefficients (p : Polynomial Nat) :
    {cs : List Nat // coefficientPolynomial cs = p} := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial

  29. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.highCoefficients line 163
  30. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.width line 166
  31. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.digit line 168
  32. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.digitBound line 171
  33. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.le_sum_of_mem line 173
  34. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.digit_le_bound line 183
  35. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.highCoefficients_foldl line 189
  36. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.range_map_digit line 196
  37. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.prependFields line 210
  38. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.prependFieldsTapes line 216
  39. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.stepAux_prependFields line 222
  40. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.prependFieldsTapes_apply line 232
  41. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.popN line 246
  42. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.stepAux_popN line 251
  43. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.clearFields line 262
  44. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.clearFieldsTapes line 267
  45. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.stepAux_clearFields line 272
  46. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.clearFieldsTapes_apply line 282
  47. abbrev OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.Layout line 300
  48. abbrev OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.Label line 301
  49. abbrev OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.State line 302
  50. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.fieldWord line 304
  51. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.fieldIndices line 308
  52. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.fieldIndices_nodup line 311
  53. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.inl_not_mem_fields line 314
  54. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.inr_mem_fields line 317
  55. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.initialTapes line 320
  56. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes line 323
  57. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes_inl line 326
  58. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes_inr line 331
  59. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.slots line 336
  60. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes_clean line 338
  61. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.innerLabels line 342
  62. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.program line 345
  63. abbrev OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.machine line 355
  64. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.afterHornerTapes line 366
  65. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.afterInputTapes line 369
  66. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.finalTapes line 372
  67. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.clearFields_final line 375
  68. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.initList_eq line 386
  69. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.haltList_eq line 392
  70. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.initializationTrace line 398
  71. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.cleanupTrace line 408
  72. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.prefixValuePolynomial line 425
  73. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.prefixCostPolynomial line 429
  74. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.prefixValuePolynomial_eval line 435
  75. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.prefixCostPolynomial_eval line 441
  76. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.timePolynomial line 451
  77. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.timePolynomial_eval line 455
  78. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.hornerValue_eq_eval line 462
  79. theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.hornerStageTrace line 468
  80. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.outputsInTime line 484

    Source documentation

    Exact execution includes literal initialization, the physical Horner subroutine, input consumption, and cleanup of every coefficient tape.

    def outputsInTime (p : Polynomial Nat) (n : Nat) :
    Turing.TM2OutputsInTime (machine p) (encodeWord n) (some (encodeWord (p.eval n)))
      ((timePolynomial p).eval n) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.machine, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.timePolynomial

  81. def OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialMachine.computableInPolyTime line 505

    Source documentation

    A genuine finite Boolean-stack machine for evaluating any fixed natural polynomial on zero-delimited unary input, with a polynomial transition bound.

    def computableInPolyTime (p : Polynomial Nat) :
    Turing.TM2ComputableInPolyTime encodeWord encodeWord p.eval where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWord