OAI/Computability/MaxCut/Encoding/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.MaxCutGames.Foundations.PCP.NameCompaction.clauseNames line 19
  2. def OAI.MaxCutGames.Foundations.PCP.NameCompaction.sourceNames line 22
  3. def OAI.MaxCutGames.Foundations.PCP.NameCompaction.activeNames line 25
  4. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.literal_mem_active line 28
  5. def OAI.MaxCutGames.Foundations.PCP.NameCompaction.compactIndex line 37
  6. def OAI.MaxCutGames.Foundations.PCP.NameCompaction.decodeName line 41
  7. def OAI.MaxCutGames.Foundations.PCP.NameCompaction.compactLiteral line 44
  8. def OAI.MaxCutGames.Foundations.PCP.NameCompaction.compactClause line 48
  9. def OAI.MaxCutGames.Foundations.PCP.NameCompaction.compactClauses line 54
  10. def OAI.MaxCutGames.Foundations.PCP.NameCompaction.compact line 57
  11. def OAI.MaxCutGames.Foundations.PCP.NameCompaction.restrictAssignment line 61
  12. def OAI.MaxCutGames.Foundations.PCP.NameCompaction.extendAssignment line 64
  13. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.decode_compactIndex line 68
  14. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.eval_compact_restrict line 72
  15. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.eval_compact_extend line 78
  16. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.map_attach_val line 88
  17. def OAI.MaxCutGames.Foundations.PCP.NameCompaction.evaluationList line 92
  18. def OAI.MaxCutGames.Foundations.PCP.NameCompaction.satisfiedCount line 95
  19. def OAI.MaxCutGames.Foundations.PCP.NameCompaction.failedCount line 98
  20. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.evaluationList_restrict line 101
  21. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.evaluationList_extend line 107
  22. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.satisfiedCount_restrict line 118
  23. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.failedCount_restrict line 122
  24. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.satisfiedCount_extend line 126
  25. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.failedCount_extend line 130
  26. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.clauseNames_flat_length line 134
  27. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.compact_clause_count line 143
  28. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.length_eraseDups_le line 147
  29. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.compact_active_bound line 161
  30. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.compact_completeness line 166
  31. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.compact_reflects line 175
  32. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.compact_satisfiable_iff line 186
  33. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.compact_preserves_gap line 190
  34. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.compact_encoding_bound line 197
  35. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.failureCount_evaluations line 215
  36. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.evaluations_allIndices line 225
  37. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.verifier_failureCount line 234

    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.MaxCutGames.Foundations.PCP.failureCount, OAI.MaxCutGames.Foundations.PCP.allIndices, OAI.MaxCutGames.Foundations.PCP.NameCompaction.failedCount

  38. theorem OAI.MaxCutGames.Foundations.PCP.NameCompaction.compact_verifier_soundness line 239