OAI/Computability/UniqueGames/PCP/ExpanderRowControlLemmas.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Raw natural-word serialization of actual expander rotation tables

The list keeps the stored row order port + degree * vertex; no header is inserted. Lookup equalities and complete unary output lengths are data facts, not machine execution certificates. Kernel-checked with Lean 4.33.1.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.degree line 15
  2. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.cloudSize line 16
  3. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.rowFactor line 17
  4. structure OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.Control line 22

    Source documentation

    The encoded vertex of firstH already stores both square ports. The two graph-return registers and final-H register are overwritten by the corresponding callbacks. Every field is bounded independently of table size.

    structure Control (d : Nat) where
…
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.squarePorts line 30
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.start line 35

    Source documentation

    Consume the finite cloud coordinate and input port, and perform the first lookup in the fixed table. Initial register values need no inhabitance choice.

    def start {d : Nat} (H : Table (cloudSize d) d)
    (cloud : Fin (cloudSize d)) (port : Fin (degree d)) : Control d :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.cloudSize, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.degree, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.Control

  7. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.receiveFirst line 46
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.receiveSecond line 51

    Source documentation

    The second graph remainder completes the final lookup in the fixed table. The square return ports are ordered second, first, as in stepLookup.

    def receiveSecond {d : Nat} (H : Table (cloudSize d) d)
    (s : Control d) (returnedPort : Fin (degree d)) : Control d :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.cloudSize, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.Control, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.degree

  9. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.firstOffset line 58
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.secondOffset line 59
  11. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.outputPort line 61
  12. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.outputOffset line 66

    Source documentation

    The entire bounded contribution to the emitted row: output port plus q times output cloud, with q = d*d.

    def outputOffset {d : Nat} (s : Control d) : Fin (rowFactor d) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.Control, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.rowFactor

  13. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.firstAddress line 69
  14. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.secondAddress line 72
  15. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.outputAddress line 75
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.firstOffset_receiveFirst line 78
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.secondOffset_receiveFirst line 81
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.receiveFirst_port line 84
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.receiveSecond_port line 87
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.firstAddress_eq_rowIndex line 90
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.secondAddress_eq_rowIndex line 96
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.firstAddress_lt line 102
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.secondAddress_lt line 107
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.lookup_vertex_div line 114

    Source documentation

    Actual table returns split into the unary vertex quotient and finite port remainder. Both formulas are the definitions of the table's mixed-radix inverse.

    theorem lookup_vertex_div {v q : Nat} (G : Table v q) (x : Fin v × Fin q) :
    (lookup G x).1.val = (reverseIndex G (rowIndex v q x)).val / q := rfl
  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.lookup_port_mod line 117
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.lookup_port_eq_remainder line 120
  27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.rowIndex_lookup line 124
  28. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.outputPair line 128
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.outputAddress_eq_rowIndex line 132
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.outputAddress_lt line 138
  31. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.evaluateRow line 145

    Source documentation

    Pure row semantics: exactly two lookups in the input table. The two fixed H lookups occur inside start and receiveSecond. This is not a machine trace.

    def evaluateRow {v d : Nat} (G : Table v (degree d)) (H : Table (cloudSize d) d)
    (vertex : Fin v) (cloud : Fin (cloudSize d)) (port : Fin (degree d)) :
    Fin v × Control d :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.degree, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.cloudSize, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.Control

  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.evaluateRow_eq_lookup_step line 156

    Source documentation

    The finite callback sequence computes exactly the previously checked square/zigzag lookup, including both reversed square ports.

    theorem evaluateRow_eq_lookup_step {v d : Nat}
    (G : Table v (degree d)) (H : Table (cloudSize d) d)
    (vertex : Fin v) (cloud : Fin (cloudSize d)) (port : Fin (degree d)) :
    outputPair (evaluateRow G H vertex cloud port).1 (evaluateRow G H vertex cloud port).2 =
      lookup (step G H) (rowIndex v (cloudSize d) (vertex,cloud),port) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.degree, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.cloudSize, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.outputPair, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.evaluateRow

  33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.outputAddress_eq_step_row line 165
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.outputAddress_eq_step_reverseIndex line 175

    Source documentation

    The emitted natural number is the actual stored row, not just an extensionally equivalent endpoint pair.

    theorem outputAddress_eq_step_reverseIndex {v d : Nat}
    (G : Table v (degree d)) (H : Table (cloudSize d) d)
    (vertex : Fin v) (cloud : Fin (cloudSize d)) (port : Fin (degree d)) :
    outputAddress (evaluateRow G H vertex cloud port).1.val (evaluateRow G H vertex cloud port).2 =
      (reverseIndex (step G H) (rowIndex (v * cloudSize d) (degree d)
        (rowIndex v (cloudSize d) (vertex,cloud),port))).val := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.degree, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.cloudSize, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.outputAddress, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderRowControl.evaluateRow

  35. def OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.rotationWords line 204
  36. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.rotationWords_length line 206
  37. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.rotationWords_getElem line 210
  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.rotationWords_get line 216
  39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.rotationWords_getElem? line 223

    Source documentation

    The exact zero-based lookup hypothesis consumed by the machine lookup API.

    theorem rotationWords_getElem? (table : Table v d) (i : Fin (v * d)) :
    (rotationWords table)[i.val]? = some (reverseIndex table i).val := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.rotationWords

  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.rotationWords_getElem?_none line 229
  41. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.rotationWords_entry_lt line 233
  42. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.rotationWords_lookup line 239

    Source documentation

    The serialized reverse index decodes to the actual table lookup.

    theorem rotationWords_lookup (table : Table v d) (x : Fin v × Fin d) :
    (rotationWords table)[(rowIndex v d x).val]? =
      some (rowIndex v d (lookup table x)).val := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.rotationWords

  43. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.rotationWords_row_order line 246

    Source documentation

    Both the input and output use port-first mixed-radix row coordinates.

    theorem rotationWords_row_order (table : Table v d) (x : Fin v × Fin d) :
    (rotationWords table)[x.2.val + d * x.1.val]? =
      some ((lookup table x).2.val + d * (lookup table x).1.val) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.rotationWords

  44. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.decode_rotationWords line 251
  45. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.decoded_lookup line 256

    Source documentation

    Fully decode the serialized list, then select the actual reverse-dart row.

    theorem decoded_lookup (table : Table v d) (i : Fin (v * d)) :
    (decodeWords (encodeWords (rotationWords table))).bind (fun words => words[i.val]?) =
      some (reverseIndex table i).val := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.rotationWords

  46. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.decoded_coordinate_lookup line 262
  47. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.encode_rotationWords_length_eq line 269
  48. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.encode_rotationWords_length_le line 274

    Source documentation

    Complete raw-row serialization bound, with no discarded delimiter or prefix.

    theorem encode_rotationWords_length_le (table : Table v d) :
    (encodeWords (rotationWords table)).length ≤ (v * d) * (v * d + 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTableWords.rotationWords