OAI/Computability/UniqueGames/PCP/PreprocessingInternalRows.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.localStep line 15

   Source documentation

   The one actual cloud-table lookup used by this internal row.

   def localStep (v : Fin t.vertices) (x : PaddedCloud t padding v) (p : Fin q) :
       Fin (cloudSize t v + padding v) × Fin q :=
   …

2. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.destination line 20

   Source documentation

   Decode the returned cloud index into its actual global padded dart.

   def destination (v : Fin t.vertices) (x : PaddedCloud t padding v) (p : Fin q) :
       PaddedCloud t padding v :=
   …

3. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.rowIndex line 24
4. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.row line 30

   Source documentation

   This is a row read from the actual serialized output table.

   def row (v : Fin t.vertices) (x : PaddedCloud t padding v) (p : Fin q) :
       GraphTables.DartRow (vertexCount t padding) (vertexCount t padding * (q + 1)) :=
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.DartRow

5. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.equalityRelation line 35

   Source documentation

   The fixed, complete 64-label equality predicate.

   def equalityRelation : GraphTables.RelationTable :=
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.RelationTable

6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.equalityRelation_apply line 38
7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.cloud_rotation line 43

   Source documentation

   The reindexed local cloud graph is exactly the stored local lookup.

   theorem cloud_rotation (v : Fin t.vertices) (x : PaddedCloud t padding v) (p : Fin q) :
       (cloudGraphs t padding tables v).rot (x, p) =
         (destination t padding tables v x p, (localStep t padding tables v x p).2) := by
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.destination, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.localStep

8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.source_rotation line 53

   Source documentation

   The actual global replacement rotation uses that same lookup and select.

   theorem source_rotation (v : Fin t.vertices) (x : PaddedCloud t padding v) (p : Fin q) :
       (sourcePortGraph t padding tables).rot (x.val, .inl p) =
         ((destination t padding tables v x p).val,
           .inl (localStep t padding tables v x p).2) := by
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.destination, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.localStep

9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.rotation_internal line 66

   Source documentation

   Full output rotation, retaining the actual return port.

   theorem rotation_internal (v : Fin t.vertices) (x : PaddedCloud t padding v) (p : Fin q) :
       PortTables.rotation (ofCloudTables t padding tables)
           (vertexOrder t padding x.val, portOrder q (.inl p)) =
         (vertexOrder t padding (destination t padding tables v x p).val,
           portOrder q (.inl (localStep t padding tables v x p).2)) := by
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.rotation, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.destination, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.localStep

10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.reverseIndex_internal line 74

    Source documentation

    The stored global reverse index is the row-major encoding of the destination.

    theorem reverseIndex_internal (v : Fin t.vertices) (x : PaddedCloud t padding v) (p : Fin q) :
        ((ofCloudTables t padding tables).reverseIndex[rowIndex t padding v x p]).val =
          (q + 1) * (vertexOrder t padding (destination t padding tables v x p).val).val +
            (localStep t padding tables v x p).2.val := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.rowIndex, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.destination, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.localStep

11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.relation_ext line 84
12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.relations_internal line 94

    Source documentation

    Equality is the entire stored relation vector, not only one tested entry.

    theorem relations_internal (v : Fin t.vertices) (x : PaddedCloud t padding v) (p : Fin q) :
        (ofCloudTables t padding tables).relations[rowIndex t padding v x p] = equalityRelation := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.rowIndex, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.equalityRelation

13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.row_tail line 101
14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.row_reverse line 106
15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.row_relation line 113
16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.localStep_original line 118
17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.localStep_dummy line 123
18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.row_tail_original line 127
19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.row_tail_dummy line 133
20. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.selectedIndex line 140

    Source documentation

    The global target number computed from an arbitrary returned cloud index.

    def selectedIndex (v : Fin t.vertices) (i : Fin (cloudSize t v + padding v)) : Nat :=
    …

21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.selectedIndex_eq line 146

    Source documentation

    Rank/select destination decoding agrees with the prefix-offset formula.

    theorem selectedIndex_eq (v : Fin t.vertices) (i : Fin (cloudSize t v + padding v)) :
        (vertexOrder t padding (paddedCloudSelect t padding v i).val).val =
          selectedIndex t padding v i := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.selectedIndex

22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.selectedIndex_old line 171

    Source documentation

    Old target indices select the original dart from its actual cloud list.

    theorem selectedIndex_old (v : Fin t.vertices) (i : Fin (cloudSize t v + padding v))
        (hi : i.val < cloudSize t v) :
        selectedIndex t padding v i = (cloudSelect t v ⟨i.val, hi⟩).val.val := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.selectedIndex

23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.selectedIndex_dummy line 177

    Source documentation

    Dummy target indices use the checked prefix offset and local index.

    theorem selectedIndex_dummy (v : Fin t.vertices) (i : Fin (cloudSize t v + padding v))
        (hi : cloudSize t v ≤ i.val) :
        selectedIndex t padding v i =
          t.darts + PreprocessingPaddingOffsets.offset padding v.val + (i.val - cloudSize t v) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.selectedIndex, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingPaddingOffsets.offset

24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.row_reverse_selectedIndex line 184

    Source documentation

    Closed arithmetic reverse field for the row machine.

    theorem row_reverse_selectedIndex (v : Fin t.vertices) (x : PaddedCloud t padding v) (p : Fin q) :
        (row t padding tables v x p).reverseIndex.val =
          (q + 1) * selectedIndex t padding v (localStep t padding tables v x p).1 +
            (localStep t padding tables v x p).2.val := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.row, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.selectedIndex, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.localStep

25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.rowWords_eq line 193

    Source documentation

    All 4098 words of the actual internal row, in the existing codec.

    theorem rowWords_eq (v : Fin t.vertices) (x : PaddedCloud t padding v) (p : Fin q) :
        GraphTables.rowWords (row t padding tables v x p) =
          [(vertexOrder t padding x.val).val,
            (q + 1) * selectedIndex t padding v (localStep t padding tables v x p).1 +
              (localStep t padding tables v x p).2.val] ++
            GraphTables.relationWords equalityRelation := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.rowWords, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.row, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.selectedIndex, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.localStep, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.relationWords, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingInternalRows.equalityRelation