OAI/Computability/BinPacking/CookLevin/Bounds.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.pairLengthPolynomial line 10
2. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.horizonPolynomial line 13
3. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.capacityPolynomial line 16
4. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.pairLengthPolynomial_eval line 19
5. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.horizonPolynomial_eval line 23
6. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.capacityPolynomial_eval line 27
7. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.paired_length_le line 32
8. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.one_le_pairLength line 38
9. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.pairLength_le_capacity line 43
10. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.one_le_capacity line 48
11. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.transition_prefix_le_capacity line 52
12. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.verifier_time_le_horizon line 67
13. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.horizon_monotone line 73
14. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.capacity_monotone line 77
15. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.execution_stack_length_le_capacity line 81
16. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.stackCapacity_le_polynomial line 101
17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.run_stack_length_le_capacity line 110
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.run_statement_budget_le_capacity line 119
19. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.configurationWidthPolynomial line 130
20. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.transitionGatesPolynomial line 134
21. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.tableauGatesPolynomial line 138
22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.configurationWidthPolynomial_eval line 143
23. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.transitionGatesPolynomial_eval line 149
24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.tableauGatesPolynomial_eval line 155
25. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.formulaBitsPolynomial line 163
26. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.formulaBitsPolynomial_eval line 166
27. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.formulaBits_length_le_polynomial line 172
28. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.circuitVariablesPolynomial line 183
29. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.circuitClausesPolynomial line 186
30. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.circuitBitsPolynomial line 189
31. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.circuitVariablesPolynomial_eval line 193
32. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.circuitClausesPolynomial_eval line 197
33. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.circuitBitsPolynomial_eval line 201
34. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.circuit_formulaBits_length_le line 207
35. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.circuit_formulaBits_length_le_polynomial line 217
36. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.toFormula_bits_length_le line 227
37. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Bounds.toFormula_bits_length_le_polynomial line 235