OAI/Computability/MaxCut/PCP/FinalBooleanVerifier.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Direct application to the checked alphabet-reduction graph.

  1. abbrev OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.Label line 10
  2. def OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.bitIndex line 14
  3. def OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.labelsOfBits line 17
  4. def OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.bitsOfLabels line 20
  5. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.labelsOfBits_bitsOfLabels line 25
  6. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.bitsOfLabels_labelsOfBits line 30
  7. abbrev OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.verifier line 35
  8. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.query_tail line 45
  9. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.query_head line 51
  10. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.eventValue_eq line 58

    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.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.Label, OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.eventValue, OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.verifier, OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.labelsOfBits

  11. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.count_false_map_filter line 66
  12. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.count_false_finRange line 72
  13. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.rejection_count_eq line 87

    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.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.Label, OAI.MaxCutGames.Foundations.PCP.VerifierToCNF.rejectedEventCount, OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.verifier, OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.labelsOfBits

  14. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.verifier_completeness line 103
  15. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.verifier_reflects line 112
  16. def OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.cnf line 120
  17. abbrev OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.OutputAssignment line 123
  18. def OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.extractLabeling line 127
  19. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.cnf_completeness line 131
  20. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.cnf_count_bridge line 137
  21. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.failedCount_zero_of_satisfied line 145
  22. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.all_satisfied_of_rejectionCount_zero line 152
  23. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.cnf_reflects line 163
  24. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.cnf_satisfiable_iff line 173
  25. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.cnf_clause_count line 178
  26. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.twelve_query_auxiliary_factor line 182
  27. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.cnf_variable_count line 184
  28. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.cnf_nonempty line 189
  29. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.cnf_gap line 193
  30. abbrev OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.ReducedVertex line 209
  31. abbrev OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.ReducedDart line 212
  32. def OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF line 217
  33. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_completeness line 222
  34. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_clause_count line 228
  35. theorem OAI.MaxCutGames.Foundations.PCP.FinalBooleanVerifier.alphabetCNF_gap line 233