OAI/Computability/UniqueGames/PCP/ExpanderTableEnumeration.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Exact row enumeration and accumulator contents for an expander-table step

The outer loop enumerates original vertices, and the inner loop enumerates cloud/port positions in increasing mixed-radix order. The resulting list is the actual next table's stored rotation-word list. Prefix and reverse-encoding identities describe data accumulated by a row loop; they assert no runtime.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.globalIndex line 25

    Source documentation

    Input position in the actual next table, with port varying fastest.

    def globalIndex (vertex : Fin v) (position : Fin (rowFactor d)) :
    Fin ((v * cloudSize d) * degree d) :=
…
  2. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.globalIndex_val line 31
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.rowValue line 45

    Source documentation

    The number emitted by the checked pure row evaluator.

    def rowValue (G : Table v (degree d)) (H : Table (cloudSize d) d)
    (vertex : Fin v) (position : Fin (rowFactor d)) : Nat :=
…
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.rowValue_eq_reverseIndex line 51
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.vertexWords line 58
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.generatedWords line 61
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.vertexWords_length line 64
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.vertexWords_drop_succ line 68
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.vertexWords_drop_full line 75
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.vertexWords_drop_last line 80
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.ofFn_cast line 86
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.rotationWords_eq_ofFn line 91
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.rowCount_eq line 100

    Source documentation

    Associativity of the three stored mixed-radix coordinates.

    theorem rowCount_eq : v * rowFactor d = (v * cloudSize d) * degree d :=
…
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.generatedWords_eq_flat_ofFn line 103
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.generatedWords_eq_rotationWords line 122

    Source documentation

    Complete equality with the actual materialized next-table word order.

    theorem generatedWords_eq_rotationWords (G : Table v (degree d)) (H : Table (cloudSize d) d) :
    generatedWords G H = rotationWords (step G H) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.generatedWords

  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.generatedWords_length line 129
  17. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.priorVertices line 134
  18. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.prefixRows line 137
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.priorVertices_zero line 141
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.priorVertices_full line 144
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.priorVertices_succ line 149
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.prefixRows_zero line 156
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.prefixRows_succ line 160
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.prefixRows_complete line 168
  25. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.accumulate line 175

    Source documentation

    This is exactly the accumulator update performed after each emitted row.

    def accumulate (values : List Nat) (initial : List Bool) : List Bool :=
…
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.accumulate_eq line 178
  27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.accumulate_append line 186
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.accumulate_prefixRows_succ line 190
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.accumulate_generatedWords line 198
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.encode_generatedWords_length_le line 204
  31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableEnumeration.accumulate_generatedWords_length_le line 210