OAI/Computability/UniqueGames/PCP/NameCompaction.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

An explicit name compaction for finite three-literal CNF formulas. Only the occurring names are scanned: the declared variable count is never enumerated. Both assignment transports preserve every clause evaluation and therefore every finite clause-score gap. The encoding bound is a size theorem; a machine running-time bound and the constant-gap PCP construction remain separate.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.clauseNames line 20
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.sourceNames line 23
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.activeNames line 26
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.literal_mem_active line 29
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.compactIndex line 38
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.decodeName line 42
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.compactLiteral line 45
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.compactClause line 49
  9. def OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.compactClauses line 55
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.compact line 58
  11. def OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.restrictAssignment line 62
  12. def OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.extendAssignment line 65
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.decode_compactIndex line 69
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.eval_compact_restrict line 73
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.eval_compact_extend line 79
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.map_attach_val line 89
  17. def OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.evaluationList line 93
  18. def OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.satisfiedCount line 96
  19. def OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.failedCount line 99
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.evaluationList_restrict line 102
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.evaluationList_extend line 108
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.satisfiedCount_restrict line 119
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.failedCount_restrict line 123
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.satisfiedCount_extend line 127
  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.failedCount_extend line 131
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.clauseNames_flat_length line 135
  27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.compact_clause_count line 144
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.length_eraseDups_le line 148
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.compact_active_bound line 162
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.compact_completeness line 167
  31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.compact_reflects line 176
  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.compact_satisfiable_iff line 187
  33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.compact_preserves_gap line 191
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.compact_encoding_bound line 198
  35. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.failureCount_evaluations line 216
  36. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.evaluations_allIndices line 226
  37. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.verifier_failureCount line 235

    Source documentation

    The semantic score is the checked verifier's actual failed-clause count.

    theorem verifier_failureCount (F : Formula) (A : Fin F.variables → Bool) :
    failureCount F A (allIndices F) = failedCount F A := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.failureCount, OAI.UniqueGamesTheorem.Foundations.PCP.allIndices, OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.failedCount

  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.NameCompaction.compact_verifier_soundness line 240