FinalCNFPattern.lean`

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.

abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.Label line 26
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.labelEquiv line 29
Source documentation
Coordinate zero is the least significant bit.
```
abbrev labelEquiv : Label ≃ Fin 64 := AlphabetTable.Enumeration.labelEquiv
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.Label
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.labelEquiv_val line 31
def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.labelIndex line 36
def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.labelBits line 38
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.labelBits_labelIndex line 40
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.labelIndex_labelBits line 43
def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.leftHalf line 46
def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.rightHalf line 49
def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.relationAddress line 53
Source documentation
Graph rows store the right endpoint index fastest.
```
def relationAddress (bits : VerifierToCNF.Pattern 12) : Fin 4096 :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.relationAddress_val line 56
def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.patternRelationIndex line 62
Source documentation
The address is computed from the converter's actual enumerated pattern.
```
def patternRelationIndex (p : VerifierToCNF.PatternIndex 12) : Fin 4096 :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.patternRelationIndex_eq line 65
def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.tableGraph line 69
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.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.Label
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.tableGraph_tail line 73
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.tableGraph_reverse line 76
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.tableGraph_accepts line 79
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.tableVerifier line 85
Source documentation
The concrete Boolean verifier associated with an already indexed table.
```
abbrev tableVerifier (table : GraphTables.Table) : VerifierToCNF.FiniteVerifier 12 :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.relation_lookup_eq_verifier_accepts line 88
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.pattern_lookup_eq_verifier_accepts line 93
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.verifier_accepts_eq_lookup line 98
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.buffer_lookup_eq_verifier_accepts line 104
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.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.relationAddress, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.tableVerifier
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFPattern.pattern_buffer_lookup_eq_verifier_accepts line 111