OAI/Computability/MaxCut/Games/FinalCNFPattern.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Concrete relation addresses for the final Boolean verifier

Six-bit labels use the already checked executable little-endian enumeration. A twelve-bit CNF pattern is split into its two endpoint labels, then addressed in the graph table's row-major order. This fixed address map uses the actual VerifierToCNF.patternAt enumeration, so no assumed correspondence between two enumeration orders is needed. The graph interpretation is an explicit relabeling of the validated table semantics.

  1. abbrev OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.Label line 22
  2. abbrev OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.labelEquiv line 25

    Source documentation

    Coordinate zero is the least significant bit.

    abbrev labelEquiv : Label ≃ Fin 64 := AlphabetTable.Enumeration.labelEquiv

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.Label

  3. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.labelEquiv_val line 27
  4. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.labelIndex line 32
  5. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.labelBits line 34
  6. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.labelBits_labelIndex line 36
  7. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.labelIndex_labelBits line 39
  8. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.leftHalf line 42
  9. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.rightHalf line 45
  10. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.relationAddress line 49

    Source documentation

    Graph rows store the right endpoint index fastest.

    def relationAddress (bits : VerifierToCNF.Pattern 12) : Fin 4096 :=
…
  11. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.relationAddress_val line 52
  12. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.patternRelationIndex line 58

    Source documentation

    The address is computed from the converter's actual enumerated pattern.

    def patternRelationIndex (p : VerifierToCNF.PatternIndex 12) : Fin 4096 :=
…
  13. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.patternRelationIndex_eq line 61
  14. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.tableGraph line 65

    Source documentation

    Interpret the numeric table over its explicitly decoded Boolean labels.

    def tableGraph (table : GraphTables.Table) :
    ConstraintGraph (Fin table.vertices) (Fin table.darts) Label :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.Label

  15. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.tableGraph_tail line 69
  16. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.tableGraph_reverse line 72
  17. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.tableGraph_accepts line 75
  18. abbrev OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.tableVerifier line 81

    Source documentation

    The concrete Boolean verifier associated with an already indexed table.

    abbrev tableVerifier (table : GraphTables.Table) : VerifierToCNF.FiniteVerifier 12 :=
…
  19. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.relation_lookup_eq_verifier_accepts line 84
  20. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.pattern_lookup_eq_verifier_accepts line 89
  21. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.verifier_accepts_eq_lookup line 94
  22. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.buffer_lookup_eq_verifier_accepts line 100

    Source documentation

    A reader's pointwise buffer correctness gives the actual verifier bit.

    theorem buffer_lookup_eq_verifier_accepts (table : GraphTables.Table)
    (e : Fin table.darts) (buffer : Fin 4096 → Bool)
    (read_correct : ∀ i, buffer i = table.rows[e].relation[i])
    (bits : VerifierToCNF.Pattern 12) :
    buffer (relationAddress bits) = (tableVerifier table).accepts e bits :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.relationAddress, OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.tableVerifier

  23. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFPattern.pattern_buffer_lookup_eq_verifier_accepts line 107