OAI/Computability/PerfectCompleteness/Machines/VerifierCircuit.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.capacity line 29
  2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.capacity_pos line 32
  3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.FreeBits line 36
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.machineInput line 39
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.actualRun line 42
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.accepting line 45
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.stackCapacity_le line 48
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.actualRun_stack_le line 55
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.actualRun_stepSafe line 61
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.accepting_stack_le line 71
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.actualRun_accepting_iff line 78
  12. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.Bit line 98
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.indexing line 101
  14. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.width line 105
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.bitEquiv line 108
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.bitWire line 111
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.stateEncoding line 114
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.stateEncoding_last line 119
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.stateEncoding_bitWire line 124
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.initialExpressions line 130
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.stepExpressions line 136
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.initialExpressions_eval line 142
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.stepExpressions_eval line 154
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.initialFrame line 169
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.timeFrame line 173
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.initialFrame_eval line 177
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.timeFrame_validity line 186
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.timeFrame_eval line 201
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.mismatchExpr line 219
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.acceptanceExpr line 224
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.mismatchExpr_eval line 228
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.acceptanceExpr_eval line 237
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.acceptanceExpr_stateEncoding line 271
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier line 288
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier_inputs line 292
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier_eval line 295
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier_accepts_iff line 302
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier_correct line 325
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.mismatchExpr_size_le line 331
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.acceptanceExpr_size_le line 336
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.stepExpressions_size_le line 346
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.initialExpressions_cost_le line 355
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier_gate_count line 371
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier_gates_le line 385
  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.widthPolynomial line 397
  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.widthPolynomial_eval line 402
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.gatePolynomial line 407
  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.formulaPolynomial line 413
  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier_gates_le_polynomial line 419
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.VerifierCircuit.circuitOfVerifier_formulaBits_length_le line 427