OAI/Computability/MinUncut/PCP/TableIteration.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.PCP.TableIteration.run line 12
2. def OAI.MinUncutGames.Foundations.PCP.TableIteration.runTables line 14
3. theorem OAI.MinUncutGames.Foundations.PCP.TableIteration.run_val line 17
4. def OAI.MinUncutGames.Foundations.PCP.TableIteration.iterationCount line 25
5. def OAI.MinUncutGames.Foundations.PCP.TableIteration.output line 27
6. def OAI.MinUncutGames.Foundations.PCP.TableIteration.outputTable line 29
7. theorem OAI.MinUncutGames.Foundations.PCP.TableIteration.output_val line 32
8. def OAI.MinUncutGames.Foundations.PCP.TableIteration.gapMap line 35
9. opaque OAI.MinUncutGames.Foundations.PCP.TableIteration.degreeData line 37
10. def OAI.MinUncutGames.Foundations.PCP.TableIteration.polynomialDegree line 40
11. theorem OAI.MinUncutGames.Foundations.PCP.TableIteration.sizeFactor_le_power line 42
12. theorem OAI.MinUncutGames.Foundations.PCP.TableIteration.run_completeness line 45
13. theorem OAI.MinUncutGames.Foundations.PCP.TableIteration.output_completeness line 49
14. theorem OAI.MinUncutGames.Foundations.PCP.TableIteration.gapMap_completeness line 53
15. theorem OAI.MinUncutGames.Foundations.PCP.TableIteration.output_darts_positive line 59
16. theorem OAI.MinUncutGames.Foundations.PCP.TableIteration.gapMap_nonempty line 63
17. theorem OAI.MinUncutGames.Foundations.PCP.TableIteration.run_size line 66
18. theorem OAI.MinUncutGames.Foundations.PCP.TableIteration.output_size line 70
19. theorem OAI.MinUncutGames.Foundations.PCP.TableIteration.initial_size_le line 75
20. theorem OAI.MinUncutGames.Foundations.PCP.TableIteration.output_size_le_input line 78
21. def OAI.MinUncutGames.Foundations.PCP.TableIteration.tableSizePolynomial line 86
22. theorem OAI.MinUncutGames.Foundations.PCP.TableIteration.tableSizePolynomial_eval line 89
23. def OAI.MinUncutGames.Foundations.PCP.TableIteration.tableBitsPolynomial line 94
24. theorem OAI.MinUncutGames.Foundations.PCP.TableIteration.output_bits_le line 97
25. def OAI.MinUncutGames.Foundations.PCP.TableIteration.formulaBitsPolynomial line 102
26. theorem OAI.MinUncutGames.Foundations.PCP.TableIteration.gapMap_bits_le line 105
27. def OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.wordEquiv line 120
28. def OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.walkEquiv line 126
29. def OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.addressEquiv line 129
30. def OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.labelEquiv line 135
31. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.wordEnd_map line 147
32. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.endpoint_map line 155
33. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.reach_iff line 159
34. def OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.ballEquiv line 170
35. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.wordToBall_map line 176
36. def OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.pullSelector line 182
37. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.decode_pullSelector line 190
38. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.decode_transport line 196
39. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.opinionAt_pullSelector line 206
40. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.advanceTail_map line 219
41. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.edgeAt_map line 227
42. def OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.pullAccepts line 242
43. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.pathAccepts_map line 245
44. def OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.dartEquiv line 271
45. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.edgeSatisfied_map line 274
46. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.rejectionCount_map line 287
47. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.satisfiable_iff line 308
48. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.pullReverse line 325
49. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.base_edgeSatisfied_map line 331
50. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.base_rejectionCount_map line 341
51. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.uniform_count_gap line 369
52. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.lazy_table_uniform_count_gap line 408
53. theorem OAI.MinUncutGames.Foundations.PCP.PoweringPortReindex.lazy_table_uniform_count_gap_at line 447
54. theorem OAI.MinUncutGames.Foundations.PCP.RoundTableGap.powered_count_gap line 480
55. theorem OAI.MinUncutGames.Foundations.PCP.RoundTableGap.build_count_gap line 511
56. theorem OAI.MinUncutGames.Foundations.PCP.RoundTableGap.step_gap line 526
57. theorem OAI.MinUncutGames.Foundations.PCP.TableGapReduction.run_gap line 548
58. theorem OAI.MinUncutGames.Foundations.PCP.TableGapReduction.output_gap line 553
59. theorem OAI.MinUncutGames.Foundations.PCP.TableGapReduction.output_satisfiable_iff line 561
60. theorem OAI.MinUncutGames.Foundations.PCP.TableGapReduction.gapMap_satisfiable_iff line 571
61. theorem OAI.MinUncutGames.Foundations.PCP.TableGapReduction.output_count_gap line 575
62. theorem OAI.MinUncutGames.Foundations.PCP.TableGapReduction.gapMap_clauseGap line 595
63. theorem OAI.MinUncutGames.Foundations.PCP.TableGapReduction.finalClauseGap_le_one line 601