OAI/Computability/PerfectCompleteness/Machines/ProducerInvariant.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.Snapshot line 13
2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.snapshot_ext line 19
3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.snapshot line 27
4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.next line 32
5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.rootValues line 33
6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.recordBits line 34
7. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.Snapshot.currentBits line 37
8. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.Snapshot.rootBits line 38
9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.lowerStage line 40
10. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.stage line 45
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.gateRecords_append line 48
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.recordsBits_append line 56
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.step_roots line 60
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.lowerStage_snapshot line 68
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.stage_snapshot line 88
16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.stages line 99
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.stages_snapshot line 105
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.compile_frameForest line 114
19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.recordBits_step line 125
20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.step_repeat line 133
21. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.circuitOutput line 140
22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.circuitOutput_snapshot line 144
23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.finalFrame line 150
24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.finalFrame_circuit line 155
25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.verifier_stages line 158
26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.verifier_output line 177
27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.snapshot_root_mem_lt line 183
28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.snapshot_rootBits_length_le line 188
29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.snapshot_records_length_le line 194
30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.snapshot_lengths_le line 204
31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.stage_tokenBits_length_le line 220
32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.stage_countBits_length_le line 231
33. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.budgetPolynomial line 239
34. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.tapePolynomial line 243
35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.budgetPolynomial_eval line 246
36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.tapePolynomial_eval line 254
37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.freeFrame_lengths_le line 258
38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.timeFrame_gate_count line 274
39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.timeFrame_gates_le line 282
40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.timeFrame_current_le line 292
41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.transition_cost_le_budget line 300
42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.timeFrame_lengths_le line 312
43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.initial_tokens_length_le line 328
44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.transition_tokens_length_le line 341
45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.acceptance_tokens_length_le line 360
46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.finalFrame_lengths_le line 377
47. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.stageEnvelopePolynomial line 393
48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.stageEnvelopePolynomial_eval line 397
49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.timeFrame_stageEnvelope line 403
50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.verifier_circuitBits_length_le line 420
51. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.stepExpressions line 443
52. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.transitionTokens line 451
53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.transitionTokens_eq line 456
54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.compile_transitionTokens line 475
55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerInvariant.stepExpressions_verifier line 510