OAI/Computability/MaxCut/PCP/ExpanderRowControl.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.MaxCutGames.Foundations.PCP.ExpanderRowControl.degree line 10
  2. abbrev OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.cloudSize line 11
  3. abbrev OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.rowFactor line 12
  4. structure OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.Control line 17

    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.MaxCutGames.Foundations.PCP.ExpanderRowControl.squarePorts line 25
  6. def OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.start line 30

    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.MaxCutGames.Foundations.PCP.ExpanderRowControl.cloudSize, OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.degree, OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.Control

  7. def OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.receiveFirst line 41
  8. def OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.receiveSecond line 46

    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.MaxCutGames.Foundations.PCP.ExpanderRowControl.cloudSize, OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.Control, OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.degree

  9. def OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.firstOffset line 53
  10. def OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.secondOffset line 54
  11. def OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.outputPort line 56
  12. def OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.outputOffset line 61

    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.MaxCutGames.Foundations.PCP.ExpanderRowControl.Control, OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.rowFactor

  13. def OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.firstAddress line 64
  14. def OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.secondAddress line 67
  15. def OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.outputAddress line 70
  16. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.firstOffset_receiveFirst line 73
  17. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.secondOffset_receiveFirst line 76
  18. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.receiveFirst_port line 79
  19. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.receiveSecond_port line 82
  20. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.firstAddress_eq_rowIndex line 85
  21. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.secondAddress_eq_rowIndex line 91
  22. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.firstAddress_lt line 97
  23. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.secondAddress_lt line 102
  24. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.lookup_vertex_div line 109

    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.MaxCutGames.Foundations.PCP.ExpanderRowControl.lookup_port_mod line 112
  26. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.lookup_port_eq_remainder line 115
  27. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.rowIndex_lookup line 119
  28. def OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.outputPair line 123
  29. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.outputAddress_eq_rowIndex line 127
  30. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.outputAddress_lt line 133
  31. def OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.evaluateRow line 140

    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.MaxCutGames.Foundations.PCP.ExpanderRowControl.degree, OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.cloudSize, OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.Control

  32. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.evaluateRow_eq_lookup_step line 151

    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.MaxCutGames.Foundations.PCP.ExpanderRowControl.degree, OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.cloudSize, OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.outputPair, OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.evaluateRow

  33. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.outputAddress_eq_step_row line 160
  34. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.outputAddress_eq_step_reverseIndex line 170

    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.MaxCutGames.Foundations.PCP.ExpanderRowControl.degree, OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.cloudSize, OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.outputAddress, OAI.MaxCutGames.Foundations.PCP.ExpanderRowControl.evaluateRow

  35. def OAI.MaxCutGames.Foundations.PCP.ExpanderTableWords.rotationWords line 195
  36. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableWords.rotationWords_length line 197
  37. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableWords.rotationWords_getElem line 201
  38. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableWords.rotationWords_get line 207
  39. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableWords.rotationWords_getElem? line 214

    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.MaxCutGames.Foundations.PCP.ExpanderTableWords.rotationWords

  40. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableWords.rotationWords_getElem?_none line 220
  41. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableWords.rotationWords_entry_lt line 224
  42. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableWords.rotationWords_lookup line 230

    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.MaxCutGames.Foundations.PCP.ExpanderTableWords.rotationWords

  43. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableWords.rotationWords_row_order line 237

    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.MaxCutGames.Foundations.PCP.ExpanderTableWords.rotationWords

  44. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableWords.decode_rotationWords line 242
  45. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableWords.decoded_lookup line 247

    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.MaxCutGames.Foundations.PCP.ExpanderTableWords.rotationWords

  46. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableWords.decoded_coordinate_lookup line 253
  47. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableWords.encode_rotationWords_length_eq line 260
  48. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTableWords.encode_rotationWords_length_le line 265

    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.MaxCutGames.Foundations.PCP.ExpanderTableWords.rotationWords