OAI/Computability/MaxCut/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.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.globalIndex line 23

    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.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.globalIndex_val line 29
  3. def OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.rowValue line 43

    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.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.rowValue_eq_reverseIndex line 49
  5. def OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords line 56
  6. def OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords line 59
  7. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords_length line 62
  8. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords_drop_succ line 66
  9. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords_drop_full line 73
  10. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords_drop_last line 78
  11. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.ofFn_cast_inline_ExpanderTableEnumeration line 84
  12. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.rotationWords_eq_ofFn line 89
  13. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.rowCount_eq line 98

    Source documentation

    Associativity of the three stored mixed-radix coordinates.

    theorem rowCount_eq : v * rowFactor d = (v * cloudSize d) * degree d :=
…
  14. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords_eq_flat_ofFn line 101
  15. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords_eq_rotationWords line 120

    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.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords

  16. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords_length line 127
  17. def OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.priorVertices line 132
  18. def OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.prefixRows line 135
  19. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.priorVertices_zero line 139
  20. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.priorVertices_full line 142
  21. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.priorVertices_succ line 147
  22. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.prefixRows_zero line 154
  23. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.prefixRows_succ line 158
  24. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.prefixRows_complete line 166
  25. def OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.accumulate line 173

    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.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_eq line 176
  27. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_append line 184
  28. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_prefixRows_succ line 188
  29. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_generatedWords line 196
  30. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.encode_generatedWords_length_le line 202
  31. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_generatedWords_length_le line 208