OAI/Computability/PerfectCompleteness/Machines/CircuitBatchLemmas.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Batch.cost line 17
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Batch.gates line 19
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Batch.roots line 23
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Batch.cost_nil line 27
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Batch.cost_cons line 29
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Batch.gates_length line 32
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Batch.roots_length line 38
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Batch.gates_ordered line 42
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Batch.roots_bounds line 51
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Batch.eval_roots line 68
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Batch.rootAt line 79
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Batch.rootAt_lt line 82
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Batch.eval_rootAt line 89
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Batch.cost_le line 98
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Batch.cost_ofFn line 108
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Batch.cost_ofFn_le line 112
  17. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Fragment line 122
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.empty line 130
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.evalWires line 132
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.evalWires_input line 135
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.evalWires_consistent line 140
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.append line 144
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.evalWires_append line 148
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.evalWires_append_old line 154
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.toCircuit line 161
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.toCircuit_eval line 164
  27. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame line 170
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.eval line 178
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.initial line 181
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.initial_eval line 185
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.step line 189
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.step_gate_count line 200
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.step_gate_count_sum line 206
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.step_gate_count_le line 211
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.step_eval line 217
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.step_eval_fun line 238
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.network line 244
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.«repeat» line 247
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.repeat_eval line 252
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.repeat_gate_count line 261
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.repeat_gate_count_sum line 271
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.repeat_gate_count_le line 276
  43. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.toCircuit line 282
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.toCircuit_eval line 285
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitBatch.Frame.repeat_toCircuit_eval line 288
  46. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ConfigIndex.SymbolBit line 308
  47. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ConfigIndex.Indexing line 310
  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ConfigIndex.Indexing.width line 320
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ConfigIndex.cellReorder line 323
  50. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ConfigIndex.Indexing.configIndexEquiv line 329
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ConfigIndex.Indexing.configIndex_label line 340
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ConfigIndex.Indexing.configIndex_state line 345
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ConfigIndex.Indexing.configIndex_cell line 351
  54. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ConfigIndex.ofMachine line 361