Encoding.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Computable binary alphabet indexing and full translation permutation tables. The labels are actual Fin (2^s) entries in the target instance format.

def OAI.MaxCutGames.Reduction.Encoding.sideEquiv line 17
Source documentation
Number the left side first and the right side second.
```
def sideEquiv (n : Nat) : Bool × Fin n ≃ Fin (2*n) :=
…
```
theorem OAI.MaxCutGames.Reduction.Encoding.sideEquiv_false_val line 20
theorem OAI.MaxCutGames.Reduction.Encoding.sideEquiv_true_val line 24
def OAI.MaxCutGames.Reduction.Encoding.alphabetEquiv line 29
Source documentation
The integer label is the packed, least-significant-bit-first coordinate word.
```
def alphabetEquiv (s : Nat) : Integration.BinaryLinear.Vector s ≃ Fin (2^s) :=
…
```
Mentions: OAI.MaxCutGames.Integration.BinaryLinear.Vector
theorem OAI.MaxCutGames.Reduction.Encoding.alphabetEquiv_symm_apply_apply line 36
theorem OAI.MaxCutGames.Reduction.Encoding.alphabetEquiv_apply_symm_apply line 41
def OAI.MaxCutGames.Reduction.Encoding.translate line 45
theorem OAI.MaxCutGames.Reduction.Encoding.translate_involutive line 49
def OAI.MaxCutGames.Reduction.Encoding.translationTable line 63
Source documentation
Both forward and inverse tables are explicitly generated from every alphabet index. Characteristic two makes these two tables equal.
```
def translationTable {s : Nat} (a b : Integration.BinaryLinear.Vector s) :
    PermutationTable (2^s) where
…
```
Mentions: OAI.MaxCutGames.Integration.BinaryLinear.Vector
theorem OAI.MaxCutGames.Reduction.Encoding.translationTable_images line 70
theorem OAI.MaxCutGames.Reduction.Encoding.translationTable_inverseImages line 75
theorem OAI.MaxCutGames.Reduction.Encoding.translationTable_satisfied_iff line 81
def OAI.MaxCutGames.Reduction.Encoding.imageVertices line 92
Source documentation
Canonical vertex bodies are compared using their actual decidable equality. List.dedup fixes a deterministic order by retaining the last occurrence.
```
def imageVertices (queries : List Q) (body : Q → V) : List V :=
…
```
theorem OAI.MaxCutGames.Reduction.Encoding.mem_imageVertices line 95
theorem OAI.MaxCutGames.Reduction.Encoding.imageVertices_nodup line 99
theorem OAI.MaxCutGames.Reduction.Encoding.imageVertices_length_le line 102
abbrev OAI.MaxCutGames.Reduction.Encoding.ImageVertex line 107
def OAI.MaxCutGames.Reduction.Encoding.imageEquiv line 112
Source documentation
A computable numbering using idxOf; its inverse looks up that index. It involves no chosen Fintype.equivFin.
```
def imageEquiv (queries : List Q) (body : Q → V) :
    ImageVertex queries body ≃ Fin (imageVertices queries body).length :=
…
```
Mentions: OAI.MaxCutGames.Reduction.Encoding.ImageVertex, OAI.MaxCutGames.Reduction.Encoding.imageVertices
def OAI.MaxCutGames.Reduction.Encoding.imageVertex line 116
def OAI.MaxCutGames.Reduction.Encoding.imageIndex line 119
theorem OAI.MaxCutGames.Reduction.Encoding.imageIndex_eq_iff line 122
theorem OAI.MaxCutGames.Reduction.Encoding.imageVertices_range line 128