OAI/Computability/DirectedFeedback/RankGraph/SumBox.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectedFeedback.SumBox.Live line 12
  2. def OAI.DirectedFeedback.SumBox.base line 13
  3. def OAI.DirectedFeedback.SumBox.copies line 14
  4. theorem OAI.DirectedFeedback.SumBox.base_pos line 16
  5. theorem OAI.DirectedFeedback.SumBox.copies_pos line 17
  6. theorem OAI.DirectedFeedback.SumBox.c_le line 18
  7. def OAI.DirectedFeedback.SumBox.toBox line 23
  8. def OAI.DirectedFeedback.SumBox.validBox line 29
  9. theorem OAI.DirectedFeedback.SumBox.toBox_injective line 35
  10. theorem OAI.DirectedFeedback.SumBox.validBox_toBox line 64
  11. theorem OAI.DirectedFeedback.SumBox.validBox_surjective line 68
  12. def OAI.DirectedFeedback.SumBox.size line 76
  13. def OAI.DirectedFeedback.SumBox.tag line 77
  14. def OAI.DirectedFeedback.SumBox.digits line 78
  15. def OAI.DirectedFeedback.SumBox.copy line 79
  16. def OAI.DirectedFeedback.SumBox.embed line 80
  17. def OAI.DirectedFeedback.SumBox.valid line 82
  18. theorem OAI.DirectedFeedback.SumBox.embed_injective line 88
  19. theorem OAI.DirectedFeedback.SumBox.valid_iff line 92
  20. theorem OAI.DirectedFeedback.SumBox.valid_embed line 99
  21. theorem OAI.DirectedFeedback.SumBox.valid_surjective line 103
  22. theorem OAI.DirectedFeedback.SumBox.tag_embed line 111
  23. theorem OAI.DirectedFeedback.SumBox.digits_embed line 115
  24. theorem OAI.DirectedFeedback.SumBox.copy_embed line 119
  25. structure OAI.DirectedFeedback.BoundedExpr.LDef line 133
  26. theorem OAI.DirectedFeedback.BoundedExpr.LDef.congr line 141
  27. theorem OAI.DirectedFeedback.BoundedExpr.LDef.const line 146
  28. theorem OAI.DirectedFeedback.BoundedExpr.LDef.input line 156
  29. theorem OAI.DirectedFeedback.BoundedExpr.LDef.replicate line 167
  30. theorem OAI.DirectedFeedback.BoundedExpr.LDef.append line 176
  31. theorem OAI.DirectedFeedback.BoundedExpr.LDef.map line 185
  32. structure OAI.DFVSGames.BinaryFormula.Literal line 198
  33. def OAI.DFVSGames.BinaryFormula.Literal.eval line 203
  34. abbrev OAI.DFVSGames.BinaryFormula.Clause line 206
  35. def OAI.DFVSGames.BinaryFormula.Clause.eval line 208
  36. structure OAI.DFVSGames.BinaryFormula.Formula line 211
  37. def OAI.DFVSGames.BinaryFormula.Formula.Satisfiable line 214
  38. def OAI.DFVSGames.BinaryFormula.clauseNames line 217
  39. def OAI.DFVSGames.BinaryEncoding.bitsValue line 226
  40. theorem OAI.DFVSGames.BinaryEncoding.bitsValue_bits line 230
  41. def OAI.DFVSGames.BinaryEncoding.frame line 237
  42. def OAI.DFVSGames.BinaryEncoding.parseFrame line 241
  43. theorem OAI.DFVSGames.BinaryEncoding.parseFrame_encoded line 248
  44. theorem OAI.DFVSGames.BinaryEncoding.frame_length line 254
  45. def OAI.DFVSGames.BinaryEncoding.nameBits line 260
  46. def OAI.DFVSGames.BinaryEncoding.parseName line 262
  47. theorem OAI.DFVSGames.BinaryEncoding.parseName_encoded line 267
  48. theorem OAI.DFVSGames.BinaryEncoding.nameBits_length line 271
  49. theorem OAI.DFVSGames.BinaryEncoding.nameBits_length_le_of_lt_pow line 275
  50. def OAI.DFVSGames.BinaryEncoding.literalBits line 281
  51. def OAI.DFVSGames.BinaryEncoding.parseLiteral line 284
  52. theorem OAI.DFVSGames.BinaryEncoding.parseLiteral_encoded line 290
  53. theorem OAI.DFVSGames.BinaryEncoding.literalBits_length line 295
  54. def OAI.DFVSGames.BinaryEncoding.clauseBits line 299
  55. def OAI.DFVSGames.BinaryEncoding.parseClause line 302
  56. theorem OAI.DFVSGames.BinaryEncoding.clause_three_entries line 308
  57. theorem OAI.DFVSGames.BinaryEncoding.parseClause_encoded line 314
  58. def OAI.DFVSGames.BinaryEncoding.clauseNameSize line 318
  59. theorem OAI.DFVSGames.BinaryEncoding.clauseBits_length line 321
  60. def OAI.DFVSGames.BinaryEncoding.clausesBits line 326
  61. def OAI.DFVSGames.BinaryEncoding.formulaBits line 330
  62. def OAI.DFVSGames.BinaryEncoding.namesBitSize line 332
  63. theorem OAI.DFVSGames.BinaryEncoding.namesBitSize_nil line 335
  64. theorem OAI.DFVSGames.BinaryEncoding.namesBitSize_cons line 337
  65. theorem OAI.DFVSGames.BinaryEncoding.clausesBits_length line 341
  66. theorem OAI.DFVSGames.BinaryEncoding.formulaBits_length line 350
  67. theorem OAI.DFVSGames.BinaryEncoding.clauses_length_lt_bits line 355
  68. def OAI.DFVSGames.BinaryEncoding.ordinarySize line 360
  69. theorem OAI.DFVSGames.BinaryEncoding.ordinarySize_le_bits line 363
  70. theorem OAI.DFVSGames.BinaryEncoding.bits_le_three_ordinarySize line 369
  71. def OAI.DFVSGames.BinaryEncoding.parseClauses line 375
  72. theorem OAI.DFVSGames.BinaryEncoding.parseClauses_encoded line 384
  73. def OAI.DFVSGames.BinaryEncoding.decodeFormula line 399
  74. theorem OAI.DFVSGames.BinaryEncoding.decodeFormula_encoded line 403
  75. theorem OAI.DFVSGames.BinaryEncoding.formulaBits_injective line 412
  76. def OAI.DFVSMaxCut.alphaGW line 423
  77. def OAI.DFVSMaxCut.binary3SAT line 427
  78. structure OAI.DFVSMaxCut.Graph line 431
  79. def OAI.DFVSMaxCut.Graph.cutSize line 437
  80. def OAI.DFVSMaxCut.Graph.maxCut line 441
  81. structure OAI.DFVSMaxCut.ScaledGraph line 444
  82. def OAI.DFVSMaxCut.ScaledGraph.bits line 449
  83. structure OAI.DFVSMaxCut.GapReduction line 455
  84. def OAI.DFVSMaxCut.MainStatement line 470
  85. def OAI.DFVSGames.Repetition.dsRate line 478
  86. theorem OAI.DFVSGames.Repetition.dsRate_nonneg line 480
  87. theorem OAI.DFVSGames.Repetition.dsRate_lt_one line 485
  88. theorem OAI.DFVSGames.Repetition.exists_positive_power_lt line 489
  89. theorem OAI.DFVSGames.Repetition.exists_dsRate_pow_le line 500
  90. theorem OAI.DFVSGames.Repetition.dsRate_one_div_eight_hundred line 507
  91. theorem OAI.DFVSGames.Repetition.dsRate_one_div_fifteen line 511
  92. theorem OAI.DFVSGames.Repetition.exists_final_repetition_count line 515
  93. theorem OAI.DFVSGames.Repetition.exists_preliminary_repetition_count line 520
  94. theorem OAI.DFVSGames.Explicit.FinishBounds.exists_reciprocal_tolerance line 530
  95. theorem OAI.DFVSGames.Explicit.FinishBounds.subdivision_completeness line 549
  96. theorem OAI.DFVSGames.Explicit.FinishBounds.subdivision_soundness line 556
  97. theorem OAI.DFVSGames.Explicit.FinishBounds.final_completeness line 563
  98. structure OAI.DFVSGames.ParameterSelection.OuterParameters line 582
  99. theorem OAI.DFVSGames.ParameterSelection.exists_outerParameters line 598
  100. def OAI.DFVSGames.ParameterSelection.OuterParameters.pStar line 615
  101. theorem OAI.DFVSGames.ParameterSelection.OuterParameters.pStar_pos line 617
  102. theorem OAI.DFVSGames.ParameterSelection.OuterParameters.pStar_lt_one line 619
  103. theorem OAI.DFVSGames.ParameterSelection.OuterParameters.exists_parity_error line 622
  104. theorem OAI.DFVSGames.ParameterSelection.OuterParameters.matrix_error_budget line 639
  105. def OAI.DFVSGames.Foundations.Complexity.Runtime.statementPushBound line 657
  106. def OAI.DFVSGames.Foundations.Complexity.Runtime.maxLabelPushes line 667
  107. theorem OAI.DFVSGames.Foundations.Complexity.Runtime.maxLabelPushes_ge line 672
  108. def OAI.DFVSGames.Foundations.Complexity.Runtime.programPushBound line 684
  109. theorem OAI.DFVSGames.Foundations.Complexity.Runtime.statement_le_programPushBound line 687
  110. theorem OAI.DFVSGames.Foundations.Complexity.Runtime.stepAuxStackLength line 692
  111. theorem OAI.DFVSGames.Foundations.Complexity.Runtime.iterateSizeBound_inline_Runtime line 735
  112. theorem OAI.DFVSGames.Foundations.Complexity.Runtime.executionSizeBound line 747
  113. theorem OAI.DFVSGames.Foundations.Complexity.Runtime.stepStackLength line 770
  114. theorem OAI.DFVSGames.Foundations.Complexity.Runtime.initialStackLength line 783
  115. theorem OAI.DFVSGames.Foundations.Complexity.Runtime.haltedOutputLength line 790
  116. theorem OAI.DFVSGames.Foundations.Complexity.Runtime.outputLength_le line 794
  117. theorem OAI.DFVSGames.Foundations.Complexity.Runtime.encodedOutputLength line 806