OAI/Computability/UniqueGames/PCP/PoweringTablesLemmas.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Executable tables of the actual powering graph

The input rotor and every base predicate are stored finite vectors. The output has one row for each start vertex, bounded port word, and orientation, with the two orientations adjacent. Every complete predicate table is generated from the bounded first-address lookup test. Degree and walk length fix the output alphabet; neither the alphabet nor an address list depends on the input vertex count.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.labelCount line 24

    Source documentation

    Program-constant output alphabet size for degree d and walk length n+1.

    def labelCount (d n : Nat) : Nat := 64 ^ addressCount d (n + 1)
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.dartCount line 27

    Source documentation

    Number of directed recorded-walk occurrences, including orientation.

    def dartCount (vertices d n : Nat) : Nat := 2 * vertices * d ^ (n + 1)
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.mathematicalGraph line 29
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.rowAccepts line 36

    Source documentation

    The finite first-address predicate evaluator used for each stored row.

    def rowAccepts {vertices d : Nat} (input : PortTables.Table vertices d) (n : Nat)
    (e : PoweringTest.Dart (Fin vertices) (Fin d) n)
    (a b : Fin (labelCount d n)) : Bool :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.Dart, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.labelCount

  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.rowAccepts_eq line 45
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.table line 55
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.table_vertices line 60
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.table_darts line 63
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.semantics_table line 67

    Source documentation

    Complete decoded semantics, with executable vertex, dart and label orders.

    theorem semantics_table {vertices d : Nat} (input : PortTables.Table vertices d) (n : Nat) :
    GenericGraphTables.semantics (table input n) =
      GenericGraphTables.enumeratedGraph (mathematicalGraph input n) (Equiv.refl _)
        (dartEquiv vertices d n) (paddedLabelEquiv d (n + 1) 64) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.semantics, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.table, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.enumeratedGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.mathematicalGraph

  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.table_accepts line 74

    Source documentation

    Each actual output relation entry is the bounded stored-opinion evaluator.

    theorem table_accepts {vertices d : Nat} (input : PortTables.Table vertices d) (n : Nat)
    (i : Fin (dartCount vertices d n)) (a b : Fin (labelCount d n)) :
    GenericGraphTables.acceptsAt (table input n).rows i a b =
      rowAccepts input n (decodeDart vertices d n i) a b := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.dartCount, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.labelCount, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.acceptsAt, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.rowAccepts

  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.table_reverse line 83

    Source documentation

    The reverse row flips just the orientation in the recorded-walk encoding.

    theorem table_reverse {vertices d : Nat} (input : PortTables.Table vertices d) (n : Nat)
    (direction : Bool) (w : Walk (Fin vertices) (Fin d) (n + 1)) :
    GenericGraphTables.reverseAt (table input n).rows (encodeDart vertices d n (direction, w)) =
      encodeDart vertices d n (!direction, w) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.reverseAt, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.table

  12. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.outputBits line 96

    Source documentation

    Serialized output in the shared generic graph codec.

    def outputBits {vertices d : Nat} (input : PortTables.Table vertices d) (n : Nat) : List Bool :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table

  13. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.transform line 100

    Source documentation

    The actual function on variable-size regular input tables.

    def transform (d n : Nat) (input : PortTables.Input d) : GenericGraphTables.Table (labelCount d n) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Input, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.labelCount

  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.firstMatch_of_first line 132

    Source documentation

    The row machine scans the same increasing address-index order.

    theorem firstMatch_of_first {S : Nat} (mask : Fin S → Bool) (i : Fin S)
    (hi : mask i = true) (hfirst : ∀ j : Fin S, j.val < i.val → mask j = false) :
    firstMatch mask = some i := by
…
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.firstMatch_firstIndex line 142
  16. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.endpointMask line 152

    Source documentation

    An actual endpoint comparison; it has no reachability oracle input.

    def endpointMask (G : PortGraph (Fin vertices) (Fin d)) (t : Nat)
    (center target : Fin vertices) (i : AddressIndex d t) : Bool :=
…
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.firstMatch_endpointMask line 156
  18. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.slotCount line 166
  19. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.RowBuffer line 168
  20. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.fixedLabelAt line 171

    Source documentation

    This lookup is fixed by the reduction parameters, not the input graph.

    def fixedLabelAt (d n : Nat) (a : Fin (PoweringTables.labelCount d n))
    (i : Fin (slotCount d n)) : GraphTables.Label :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.labelCount, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.slotCount, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Label

  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.fixedLabelAt_addressIndex line 175
  22. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.walkData line 185

    Source documentation

    For each actual path edge, store its complete base relation, then the start-to-tail mask, then the end-to-head mask. Every bit is computed.

    def walkData (input : PortTables.Table vertices d) (n : Nat)
    (w : Walk (Fin vertices) (Fin d) (n + 1))
    (k : Fin (n + 1)) : Field (slotCount d n) → Bool
  | .inl (a, b) => PortTables.accepts input (edgeAt (PortTables.portGraph input) n w k) a b
  | .inr (.inl i) => endpointMask (PortTables.portGraph input) (n + 1) w.1
      (edgeAt (PortTables.portGraph input) n w k).1 i
  | .inr (.inr i) => endpointMask (PortTables.portGraph input) (n + 1)
      (endpoint (PortTables.portGraph input) w)
      ((PortTables.portGraph input).rot (edgeAt (PortTables.portGraph input) n w k)).1 i

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.slotCount, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.portGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.endpointMask

  23. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.walkBits line 195
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.basePredicate_walkBits line 199
  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.leftMatches_walkBits line 206
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.rightMatches_walkBits line 213
  27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.firstMatch_walkBits_left line 221
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.firstMatch_walkBits_right line 231
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.edgeAccept_walkBits line 242
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.rowAccept_walkBits line 255
  31. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.transposeField line 267

    Source documentation

    Reverse orientation exchanges the two mask fields and label arguments.

    def transposeField {S : Nat} : Field S → Field S
  | .inl (a, b) => .inl (b, a)
  | .inr (.inl i) => .inr (.inr i)
  | .inr (.inr i) => .inr (.inl i)
  32. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.transposeBits line 272
  33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.basePredicate_transposeBits line 275
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.leftMatches_transposeBits line 280
  35. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.rightMatches_transposeBits line 286
  36. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.edgeAccept_transposeBits line 292
  37. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.rowAccept_transposeBits line 301
  38. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.rowBits line 309

    Source documentation

    The fully specified data block for either directed occurrence.

    def rowBits (input : PortTables.Table vertices d) (n : Nat)
    (e : PoweringTest.Dart (Fin vertices) (Fin d) n) : RowBuffer d n :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.Dart, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.RowBuffer

  39. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.rowData line 313
  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.rowBits_packData line 318
  41. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.rowBits_field line 325
  42. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.rowAccept_rowBits line 333

    Source documentation

    No match-mask or base-relation premise remains in the evaluator bridge.

    theorem rowAccept_rowBits (input : PortTables.Table vertices d) (n : Nat)
    (e : PoweringTest.Dart (Fin vertices) (Fin d) n)
    (a b : Fin (PoweringTables.labelCount d n)) :
    rowAccept (fixedLabelAt d n) (rowBits input n e) a b =
      PoweringTables.rowAccepts input n e a b := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTest.Dart, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.labelCount, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.fixedLabelAt, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.rowBits, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.rowAccepts

  43. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.rowBlock_at_rowBits line 343
  44. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.dataWords line 351
  45. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.dataTape line 355
  46. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.dataTape_eq line 359
  47. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.dataWords_length line 364
  48. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.dataTape_length_le line 370
  49. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.emittedRelation line 376
  50. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.emittedRelation_eq line 381
  51. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.rowBlock_unary line 389
  52. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.emittedRelation_table line 402

    Source documentation

    The emitted bits are the relation of the actual numbered output row.

    theorem emittedRelation_table (input : PortTables.Table vertices d) (n : Nat)
    (i : Fin (PoweringTables.dartCount vertices d n)) :
    emittedRelation input n (decodeDart vertices d n i) =
      (PoweringTables.table input n).rows[i].relation := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.dartCount, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.emittedRelation, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.table

  53. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.rowBlock_unary_table line 429
  54. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.tableRowMachineInTime line 439

    Source documentation

    With the actual computed data on its input tape, the existing finite row machine emits precisely the serialized relation of the actual output table. The unread input suffix and prior output tape are preserved as specified.

    def tableRowMachineInTime (input : PortTables.Table vertices d) (n : Nat)
    (i : Fin (PoweringTables.dartCount vertices d n)) (suffix : List Bool)
    (register : RowBuffer d n) (tapes : Bool → List Bool)
    (hinput : tapes false = dataTape input n (decodeDart vertices d n i) ++ suffix) :
    StateTransition.EvalsToInTime (PoweringMachineRow.machine (t := n + 1) (fixedLabelAt d n)).step
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.dartCount, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.RowBuffer, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.dataTape, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowData.fixedLabelAt

  55. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.tailPorts line 472

    Source documentation

    The actual ports before a selected time, with no vertex-dependent choice.

    def tailPorts : (n : Nat) → (Fin (n + 1) → D) → Fin (n + 1) → List D
  | 0, _, _ => []
  | n + 1, p, k => Fin.cases [] (fun j => p 0 :: tailPorts n (fun i => p i.succ) j) k
  56. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.tailPorts_length line 476
  57. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.walkEnd_tailPorts line 486
  58. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.headPorts line 497
  59. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.walkEnd_headPorts line 500
  60. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.addressPorts line 508
  61. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.walkEnd_addressPorts line 511
  62. inductive OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.Instruction line 517

    Source documentation

    Static commands; all changing vertex identifiers remain inputs to evaluation.

    inductive Instruction (d : Nat) where
…
  63. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.Instruction.radius line 522

    Source documentation

    The number of shared trajectory tapes needed by a single instruction.

    def Instruction.radius {d : Nat} : Instruction d → Nat
  | .relation ports _ _ _ => ports.length
  | .equal left right => max left.length right.length

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.Instruction

  64. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.addressPorts_length_le line 526
  65. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.evaluate line 531
  66. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.fieldPlan line 539
  67. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.evaluate_fieldPlan line 545
  68. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.directedFieldPlan line 565
  69. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.fieldPlan_radius line 569
  70. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.directedFieldPlan_radius line 584
  71. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.evaluate_directedFieldPlan line 589
  72. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.rowPlan line 597

    Source documentation

    The exact fixed sequence of data-producing commands, in serialized order.

    def rowPlan {d : Nat} (n : Nat) (ports : Fin (n + 1) → Fin d) (direction : Bool) :
    List (Instruction d) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.Instruction

  73. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.evaluate_rowPlan line 603
  74. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringFieldPlan.dataTape_eq_plan line 614
  75. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowHeaderSemantics.blockSize line 633
  76. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowHeaderSemantics.reverseOffset line 635
  77. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowHeaderSemantics.reverseValue line 638
  78. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowHeaderSemantics.tailVertex line 642
  79. def OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowHeaderSemantics.headerWords line 646
  80. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowHeaderSemantics.table_tail line 651

    Source documentation

    The stored tail is the recorded start or endpoint according to direction.

    theorem table_tail (input : PortTables.Table vertices d) (n : Nat) (vertex : Fin vertices)
    (ports : Fin (n + 1) → Fin d) (direction : Bool) :
    (PoweringTables.table input n).rows[encodeDart vertices d n (direction, vertex, ports)].tail =
      tailVertex input n vertex ports direction := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowHeaderSemantics.tailVertex

  81. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowHeaderSemantics.table_reverseValue line 664

    Source documentation

    The reverse address retains the word and changes only its direction bit.

    theorem table_reverseValue (input : PortTables.Table vertices d) (n : Nat)
    (vertex : Fin vertices) (ports : Fin (n + 1) → Fin d) (direction : Bool) :
    (PoweringTables.table input n).rows[encodeDart vertices d n
      (direction, vertex, ports)].reverseIndex.val = reverseValue d n vertex ports direction := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowHeaderSemantics.reverseValue

  82. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowHeaderSemantics.headerWords_eq line 674
  83. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowHeaderSemantics.header_relation_bits line 686

    Source documentation

    Prepending these two fields to the existing relation yields the exact serialized row, preserving the rest of the output tape.

    theorem header_relation_bits (input : PortTables.Table vertices d) (n : Nat)
    (vertex : Fin vertices) (ports : Fin (n + 1) → Fin d) (direction : Bool)
    (suffix : List Bool) :
    encodeWords (headerWords input n vertex ports direction) ++
      (encodeWords (GenericGraphTables.relationWords
        (PoweringTables.table input n).rows[encodeDart vertices d n
          (direction, vertex, ports)].relation) ++ suffix) =
      encodeWords (GenericGraphTables.rowWords
        (PoweringTables.table input n).rows[encodeDart vertices d n
          (direction, vertex, ports)]) ++ suffix := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringRowHeaderSemantics.headerWords, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.relationWords, OAI.UniqueGamesTheorem.Foundations.PCP.PoweringTables.table, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.rowWords