OAI/Computability/VertexCover/Fourier/SourceHonest.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.Hastad.SourceHonest.taggedAssignment line 45
2. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.taggedAssignment_left line 51
3. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.taggedAssignment_right line 55
4. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.taggedAssignment_right_restriction line 59
5. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.conditioned_equation_honest_satisfied line 77
6. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.mapped_conditioned_equation_honest_satisfied line 90
7. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.tapeAcceptance_conditioned_dictators line 109
8. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.numbered_assignment_restriction line 127
9. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.conditionedOccurrence_honest_satisfied line 149
10. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.conditionedOccurrenceList_honest_acceptance line 162
11. def OAI.UniqueGames.Foundations.Hastad.SourceHonest.honestGlobal line 196
12. def OAI.UniqueGames.Foundations.Hastad.SourceHonest.honestBits line 202
13. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.honestBits_code line 207
14. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.honestBits_dummy line 215
15. def OAI.UniqueGames.Foundations.Hastad.SourceHonest.honestValidJ line 221
16. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.validJ_nonempty_of_satisfying line 227
17. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.leftResponse_honest line 233
18. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.rightResponse_honest line 241
19. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.context_tapeAcceptance line 264
20. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.sourceEquation_honest_satisfied line 278
21. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.rawSourceList_honest_acceptance line 288
22. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_nonempty line 307
23. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance line 317
24. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_rat line 331
25. theorem OAI.UniqueGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_nonempty_rat line 341