OAI/Computability/UniqueGames/Machines/FinalCNFTemplate.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Fixed literal templates for the twelve-query converter. All control data have constant size: twelve query references, nine auxiliary references, ten clauses, and three literal slots. Pattern bits remain symbolic throughout the proof.

These templates specify the actual serialized rows.

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.Reference line 17
  2. structure OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.LiteralTemplate line 22
  3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.ClauseTemplate line 27
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.queryLiteral line 29
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.auxiliaryLiteral line 32
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.tautologyTemplate line 35
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.chainTemplates line 39

    Source documentation

    The same prefix-chain clauses used by splitLong, in their output order.

    def chainTemplates (bits : Fin 12 → Bool) : Vector ClauseTemplate 10 :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.ClauseTemplate

  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.blockTemplates line 52
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.templates line 55
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.literalAt line 59

    Source documentation

    Fixed clause/slot indexing for the machine's finite emission plan.

    def literalAt (accepted : Bool) (bits : Fin 12 → Bool)
    (clause : Fin 10) (slot : Fin 3) : LiteralTemplate :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.LiteralTemplate

  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.templates_length line 63
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.templates_true line 66
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.templates_false line 69
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.literalTemplates line 72
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.literalTemplates_length line 75
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.literalWords line 80
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.clauseWords line 83
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.words line 86
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.words_length line 89
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.resolve line 98
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.resolve_query_value line 102
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.resolve_auxiliary_value line 106
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.instantiateLiteral line 114
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.instantiateClause line 117
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.splitLong_twelve line 122

    Source documentation

    A symbolic twelve-input chain expands to exactly these ten clauses.

    theorem splitLong_twelve {n : Nat} (ls : Fin 12 → Literal n) (ys : Fin 9 → Fin n) :
    VerifierToCNF.splitLong (List.ofFn ls) (List.ofFn ys) =
      [#v[ls 0, ls 1, ⟨ys 0, true⟩],
       #v[⟨ys 0, false⟩, ls 2, ⟨ys 1, true⟩],
       #v[⟨ys 1, false⟩, ls 3, ⟨ys 2, true⟩],
       #v[⟨ys 2, false⟩, ls 4, ⟨ys 3, true⟩],
       #v[⟨ys 3, false⟩, ls 5, ⟨ys 4, true⟩],
       #v[⟨ys 4, false⟩, ls 6, ⟨ys 5, true⟩],
       #v[⟨ys 5, false⟩, ls 7, ⟨ys 6, true⟩],
       #v[⟨ys 6, false⟩, ls 8, ⟨ys 7, true⟩],
       #v[⟨ys 7, false⟩, ls 9, ⟨ys 8, true⟩],
       #v[⟨ys 8, false⟩, ls 10, ls 11]] := by
…
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.instantiate_templates line 138

    Source documentation

    Instantiating the fixed plan reproduces the actual converter's entire block.

    theorem instantiate_templates :
    (templates (V.accepts e (VerifierToCNF.patternAt 12 p))
      (VerifierToCNF.patternAt 12 p)).map (instantiateClause V e p) =
        VerifierToCNF.block V (by decide) e p := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.templates, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.instantiateClause

  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.instantiate_templates_of_acceptance line 152
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.instantiateClause_words line 159
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.words_eq_block line 164

    Source documentation

    The finite plan's sixty natural fields are the converter's actual row words.

    theorem words_eq_block :
    words (V.accepts e (VerifierToCNF.patternAt 12 p)) (VerifierToCNF.patternAt 12 p)
      (fun r => (resolve V e p r).val) =
        (VerifierToCNF.block V (by decide) e p).flatMap Complexity.clauseWords := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.words, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.resolve, OAI.UniqueGamesTheorem.Foundations.Complexity.clauseWords

  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFTemplate.block_words_length line 172