OAI/Computability/UniqueGames/PCP/FinalBooleanVerifier.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.Label line 13
2. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.bitIndex line 17
3. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.labelsOfBits line 20
4. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.bitsOfLabels line 23
5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.labelsOfBits_bitsOfLabels line 28
6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.bitsOfLabels_labelsOfBits line 33
7. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.verifier line 38
8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.query_tail line 48
9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.query_head line 54
10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.eventValue_eq line 61

    Source documentation

    Acceptance is the actual graph predicate on the two recovered labels.

    theorem eventValue_eq (G : ConstraintGraph V E Label) (vertices : V ≃ Fin n)
        (edges : E ≃ Fin m) (assignment : Fin (n * 6) → Bool) (e : Fin m) :
        VerifierToCNF.eventValue (verifier G vertices edges) assignment e =
          G.edgeSatisfied (labelsOfBits vertices assignment) (edges.symm e) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.Label, OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.eventValue, OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.verifier, OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.labelsOfBits

11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.count_false_map_filter line 69
12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.count_false_finRange line 75
13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.rejection_count_eq line 90

    Source documentation

    The enumeration preserves the exact directed-dart rejection count.

    theorem rejection_count_eq [Fintype E] (G : ConstraintGraph V E Label)
        (vertices : V ≃ Fin n) (edges : E ≃ Fin m) (assignment : Fin (n * 6) → Bool) :
        VerifierToCNF.rejectedEventCount (verifier G vertices edges) assignment =
          G.rejectionCount (labelsOfBits vertices assignment) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.Label, OAI.UniqueGamesTheorem.Foundations.PCP.VerifierToCNF.rejectedEventCount, OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.verifier, OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.labelsOfBits

14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.verifier_completeness line 106
15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.verifier_reflects line 115
16. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.cnf line 123
17. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.OutputAssignment line 126
18. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.extractLabeling line 130
19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.cnf_completeness line 134
20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.cnf_count_bridge line 140
21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.failedCount_zero_of_satisfied line 148
22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.all_satisfied_of_rejectionCount_zero line 155
23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.cnf_reflects line 166
24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.cnf_satisfiable_iff line 176
25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.cnf_clause_count line 181
26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.twelve_query_auxiliary_factor line 185
27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.cnf_variable_count line 187
28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.cnf_nonempty line 192
29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.cnf_gap line 196
30. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.ReducedVertex line 210
31. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.ReducedDart line 213
32. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.alphabetCNF line 218
33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_completeness line 223
34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_clause_count line 229
35. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_gap line 234