OAI/Computability/UniqueGames/Reduction/EncodingLemmas.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

Computable binary alphabet indexing and full translation permutation tables. The labels are actual Fin (2^s) entries in the target instance format.

  1. def OAI.UniqueGamesTheorem.Reduction.Encoding.sideEquiv line 29

    Source documentation

    Number the left side first and the right side second.

    def sideEquiv (n : Nat) : Bool × Fin n ≃ Fin (2*n) :=
…
  2. theorem OAI.UniqueGamesTheorem.Reduction.Encoding.sideEquiv_false_val line 32
  3. theorem OAI.UniqueGamesTheorem.Reduction.Encoding.sideEquiv_true_val line 36
  4. def OAI.UniqueGamesTheorem.Reduction.Encoding.alphabetEquiv line 41

    Source documentation

    The integer label is the packed, least-significant-bit-first coordinate word.

    def alphabetEquiv (s : Nat) : Integration.BinaryLinear.Vector s ≃ Fin (2^s) :=
…

    Mentions: OAI.UniqueGamesTheorem.Integration.BinaryLinear.Vector

  5. theorem OAI.UniqueGamesTheorem.Reduction.Encoding.alphabetEquiv_symm_apply_apply line 48
  6. theorem OAI.UniqueGamesTheorem.Reduction.Encoding.alphabetEquiv_apply_symm_apply line 53
  7. def OAI.UniqueGamesTheorem.Reduction.Encoding.translate line 57
  8. theorem OAI.UniqueGamesTheorem.Reduction.Encoding.translate_involutive line 61
  9. def OAI.UniqueGamesTheorem.Reduction.Encoding.translationTable line 75

    Source documentation

    Both forward and inverse tables are explicitly generated from every alphabet index. Characteristic two makes these two tables equal.

    def translationTable {s : Nat} (a b : Integration.BinaryLinear.Vector s) :
    PermutationTable (2^s) where
…

    Mentions: OAI.UniqueGamesTheorem.Integration.BinaryLinear.Vector

  10. theorem OAI.UniqueGamesTheorem.Reduction.Encoding.translationTable_images line 82
  11. theorem OAI.UniqueGamesTheorem.Reduction.Encoding.translationTable_inverseImages line 87
  12. theorem OAI.UniqueGamesTheorem.Reduction.Encoding.translationTable_satisfied_iff line 93
  13. def OAI.UniqueGamesTheorem.Reduction.Encoding.imageVertices line 106

    Source documentation

    Canonical vertex bodies are compared using their actual decidable equality. List.dedup fixes a deterministic order by retaining the last occurrence.

    def imageVertices (queries : List Q) (body : Q → V) : List V :=
…
  14. theorem OAI.UniqueGamesTheorem.Reduction.Encoding.mem_imageVertices line 109
  15. theorem OAI.UniqueGamesTheorem.Reduction.Encoding.imageVertices_nodup line 113
  16. theorem OAI.UniqueGamesTheorem.Reduction.Encoding.imageVertices_length_le line 116
  17. abbrev OAI.UniqueGamesTheorem.Reduction.Encoding.ImageVertex line 121
  18. def OAI.UniqueGamesTheorem.Reduction.Encoding.imageEquiv line 126

    Source documentation

    A computable numbering using idxOf; its inverse looks up that index. It involves no chosen Fintype.equivFin.

    def imageEquiv (queries : List Q) (body : Q → V) :
    ImageVertex queries body ≃ Fin (imageVertices queries body).length :=
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.Encoding.ImageVertex, OAI.UniqueGamesTheorem.Reduction.Encoding.imageVertices

  19. def OAI.UniqueGamesTheorem.Reduction.Encoding.imageVertex line 130
  20. def OAI.UniqueGamesTheorem.Reduction.Encoding.imageIndex line 133
  21. theorem OAI.UniqueGamesTheorem.Reduction.Encoding.imageIndex_eq_iff line 136
  22. theorem OAI.UniqueGamesTheorem.Reduction.Encoding.imageVertices_range line 142
  23. abbrev OAI.UniqueGamesTheorem.Reduction.ActualOrbit.Ambient line 167
  24. def OAI.UniqueGamesTheorem.Reduction.ActualOrbit.body line 169
  25. def OAI.UniqueGamesTheorem.Reduction.ActualOrbit.offset line 172
  26. def OAI.UniqueGamesTheorem.Reduction.ActualOrbit.Vertex line 175

    Source documentation

    Only realized bodies are vertices; no extra formal records are added.

    def Vertex (can : Q → Ambient s d × T) := {o : Vector d × T // ∃ q, body can q = o}

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualOrbit.Ambient, OAI.UniqueGamesTheorem.Reduction.ActualOrbit.body

  27. def OAI.UniqueGamesTheorem.Reduction.ActualOrbit.vertex line 177
  28. theorem OAI.UniqueGamesTheorem.Reduction.ActualOrbit.vertex_surjective line 180
  29. instance OAI.UniqueGamesTheorem.Reduction.ActualOrbit.vertexFintype line 185
  30. instance OAI.UniqueGamesTheorem.Reduction.ActualOrbit.vertexNonempty line 190
  31. theorem OAI.UniqueGamesTheorem.Reduction.ActualOrbit.vertex_eq_iff line 193
  32. abbrev OAI.UniqueGamesTheorem.Reduction.ActualOrbit.TwoSidedVertex line 201

    Source documentation

    false is the left copy and true is the right copy.

    abbrev TwoSidedVertex (can : Q → Ambient s d × T) := Bool × Vertex can

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualOrbit.Ambient, OAI.UniqueGamesTheorem.Reduction.ActualOrbit.Vertex

  33. def OAI.UniqueGamesTheorem.Reduction.ActualOrbit.vertexEquiv line 203
  34. def OAI.UniqueGamesTheorem.Reduction.ActualOrbit.explicitVertexEquiv line 209

    Source documentation

    Executable vertex numbering from an exhaustive list, preserving the same realizable-body subtype used in the semantic statements.

    def explicitVertexEquiv [DecidableEq (Vector d × T)]
    (can : Q → Ambient s d × T) (queries : List Q) (full : ∀ q, q ∈ queries) :
    Vertex can ≃ Fin (Encoding.imageVertices queries (body can)).length :=
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualOrbit.Ambient, OAI.UniqueGamesTheorem.Reduction.ActualOrbit.Vertex, OAI.UniqueGamesTheorem.Reduction.Encoding.imageVertices, OAI.UniqueGamesTheorem.Reduction.ActualOrbit.body

  35. def OAI.UniqueGamesTheorem.Reduction.ActualOrbit.unfold line 221
  36. theorem OAI.UniqueGamesTheorem.Reduction.ActualOrbit.add_self_vector line 224
  37. theorem OAI.UniqueGamesTheorem.Reduction.ActualOrbit.add_cancel_vector line 228
  38. theorem OAI.UniqueGamesTheorem.Reduction.ActualOrbit.constraint_iff_unfolded line 232

    Source documentation

    The precise orientation used by the generated edge.

    theorem constraint_iff_unfolded (can : Q → Ambient s d × T)
    (labelL labelR : Vertex can → Vector s) (q r : Q) :
    (labelL (vertex can q) + offset can q) + offset can r = labelR (vertex can r) ↔
      unfold can labelL q = unfold can labelR r := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualOrbit.Ambient, OAI.UniqueGamesTheorem.Reduction.ActualOrbit.Vertex, OAI.UniqueGamesTheorem.Reduction.ActualOrbit.vertex, OAI.UniqueGamesTheorem.Reduction.ActualOrbit.offset, OAI.UniqueGamesTheorem.Reduction.ActualOrbit.unfold

  39. theorem OAI.UniqueGamesTheorem.Reduction.ActualOrbit.unfold_eq_of_canonical_eq line 245

    Source documentation

    A common full canonical record has one common unfolded value on each side.

    theorem unfold_eq_of_canonical_eq (can : Q → Ambient s d × T)
    (label : Vertex can → Vector s) (q r : Q) (h : can q = can r) :
    unfold can label q = unfold can label r := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualOrbit.Ambient, OAI.UniqueGamesTheorem.Reduction.ActualOrbit.Vertex, OAI.UniqueGamesTheorem.Reduction.ActualOrbit.unfold

  40. abbrev OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.Ambient line 269
  41. abbrev OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.Record line 270
  42. abbrev OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.Body line 271
  43. def OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.vectorWord line 273
  44. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.vectorWord_lt line 276
  45. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.vectorWord_injective line 279
  46. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.vectorWord_eq_iff line 285
  47. def OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.recordWords line 290

    Source documentation

    Words: tag, name, occurrence, followed by three split coefficient pairs. Padding is zero. A single record uses only the first coefficient pair.

    def recordWords {n m s d : Nat} : Record n m s d → List Nat
  | .blank => [0, 0, 0, 0, 0, 0, 0, 0, 0]
  | .single name coefficient =>
      [1, name.val, 0, vectorWord coefficient.1, vectorWord coefficient.2, 0, 0, 0, 0]
  | .full occurrence coefficients =>
      [2, 0, occurrence.val,
        vectorWord (coefficients 0).1, vectorWord (coefficients 0).2,
        vectorWord (coefficients 1).1, vectorWord (coefficients 1).2,
        vectorWord (coefficients 2).1, vectorWord (coefficients 2).2]

    Mentions: OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.Record, OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.vectorWord

  48. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.recordWords_length line 300
  49. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.recordWords_injective line 304
  50. def OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.recordsWords line 339
  51. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.recordsWords_nil line 342
  52. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.recordsWords_cons line 345
  53. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.recordsWords_length line 349
  54. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.recordsWords_take_head line 355
  55. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.recordsWords_injective line 362
  56. def OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.bodyWords line 390
  57. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.bodyWords_length line 393
  58. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.bodyWords_injective line 397
  59. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.bodyWords_eq_iff line 405
  60. def OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.wordBound line 408
  61. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.recordWords_bounded line 410
  62. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.bodyWords_bounded line 435
  63. def OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.bodyBits line 446
  64. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.bodyBits_injective line 449
  65. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.bodyBits_eq_iff line 454
  66. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.bodyBits_length_le line 457
  67. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.imageVertices_bodyWords line 463

    Source documentation

    Serializing before deduplication preserves the exact retained vertex order.

    theorem imageVertices_bodyWords {Q : Type*} {n m k s d : Nat}
    [DecidableEq (Body n m k s d)] (queries : List Q) (body : Q → Body n m k s d) :
    Encoding.imageVertices queries (fun q => bodyWords (body q)) =
      (Encoding.imageVertices queries body).map bodyWords := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.Body, OAI.UniqueGamesTheorem.Reduction.Encoding.imageVertices, OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.bodyWords

  68. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.imageVertices_bodyBits line 471
  69. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.idxOf_map_injective line 479
  70. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.imageIndex_map_val line 493

    Source documentation

    Injective serialization leaves the actual numeric vertex index unchanged, not just the vertex set or its cardinality.

    theorem imageIndex_map_val {Q A B : Type*} [DecidableEq A] [DecidableEq B]
    (queries : List Q) (body : Q → A) (f : A → B) (hf : Function.Injective f)
    (q : Q) (hq : q ∈ queries) :
    (Encoding.imageIndex queries (fun q => f (body q)) q hq).val =
      (Encoding.imageIndex queries body q hq).val := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.Encoding.imageIndex

  71. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.imageIndex_bodyWords_val line 507
  72. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalEncoding.imageIndex_bodyBits_val line 514
  73. def OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.radix line 538

    Source documentation

    Most-significant-word first, with leading zero words retained in the fixed-length domain. Mathlib's ofDigits uses the opposite list order.

    def radix (B : Nat) (words : List Nat) : Nat := Nat.ofDigits B words.reverse
  74. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.radix_eq_foldl line 540
  75. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.radix_nil line 546
  76. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.radix_append_word line 549

    Source documentation

    This is precisely the arithmetic operation of MachineRadixStep.

    theorem radix_append_word (B : Nat) (words : List Nat) (digit : Nat) :
    radix B (words ++ [digit]) = B * radix B words + digit := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.radix

  77. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.radix_lt_pow_length line 553
  78. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.radix_injective_of_length_eq line 561

    Source documentation

    Fixed width makes leading zero words unambiguous.

    theorem radix_injective_of_length_eq {B : Nat} (hB : 1 < B)
    {xs ys : List Nat} (sameLength : xs.length = ys.length)
    (xsBounded : ∀ w ∈ xs, w < B) (ysBounded : ∀ w ∈ ys, w < B)
    (sameAddress : radix B xs = radix B ys) : xs = ys := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.radix

  79. def OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.base line 573

    Source documentation

    One larger than the proved bound on every canonical word.

    def base (n m s d : Nat) : Nat := wordBound n m s d + 1
  80. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.base_eq line 575
  81. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.one_lt_base line 579
  82. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.bodyWords_lt_base line 586
  83. def OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.capacity line 590
  84. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.capacity_pos line 592
  85. def OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.bodyAddress line 595
  86. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.bodyAddress_val line 601
  87. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.bodyAddress_injective line 604
  88. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.bodyAddress_eq_iff line 612
  89. def OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.capacityPolynomial line 616

    Source documentation

    For fixed k,s,d, the entire direct-address space is a polynomial in n+m.

    noncomputable def capacityPolynomial (k s d : Nat) : Polynomial Nat :=
…
  90. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.capacityPolynomial_eval line 619
  91. inductive OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.Token line 634

    Source documentation

    A literal word or a reference to one of the four saved input fields.

    inductive Token
  | literal (value : Nat)
  | name (index : Fin 3)
  | occurrence
  deriving DecidableEq, Repr
  92. def OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.evalToken line 640
  93. def OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.evalTemplate line 645
  94. def OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.isVariable line 649
  95. def OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.variableTokens line 654
  96. def OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.blankTemplate line 656
  97. def OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.singleTemplate line 660
  98. def OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.fullTemplate line 665
  99. def OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.template line 672

    Source documentation

    Coefficient equality alone selects the record tag and the input field.

    def template {s d : Nat} (a : Fin 3 → Ambient s d) : List Token :=
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.Token

  100. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.blankTemplate_length line 679
  101. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.singleTemplate_length line 681
  102. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.fullTemplate_length line 684
  103. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.template_length line 687
  104. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.evalTemplate_length line 692
  105. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.eval_blankTemplate line 696
  106. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.eval_singleTemplate line 700
  107. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.eval_fullTemplate line 706
  108. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.eval_template line 713

    Source documentation

    The template evaluates to the exact existing canonical-record encoding.

    theorem eval_template {n m s d : Nat} (names : Fin m → Fin 3 → Fin n)
    (occurrence : Fin m) (a : Fin 3 → Ambient s d) :
    evalTemplate (fun j => (names occurrence j).val) occurrence.val (template a) =
      recordWords (ActualCanonical.record names occurrence a) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.evalTemplate, OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.template, OAI.UniqueGamesTheorem.Reduction.ActualCanonical.record

  109. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.variableTokens_blankTemplate line 720
  110. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.variableTokens_singleTemplate line 722
  111. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.variableTokens_fullTemplate line 726
  112. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.variableTokens_template line 732

    Source documentation

    Exact input-field profile: blank has none; single reads one selected name; full reads the occurrence identifier. Coefficient values are program constants.

    theorem variableTokens_template {s d : Nat} (a : Fin 3 → Ambient s d) :
    variableTokens (template a) =
      if a 0 = a 1 then
        if a 0 = a 2 then [] else [.name 2]
      else if a 0 = a 2 then [.name 1]
      else if a 1 = a 2 then [.name 0]
      else [.occurrence] := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.variableTokens, OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.template

  113. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.variableTokens_template_length_le_one line 742
  114. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.name_mem_variableTokens_iff line 747
  115. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.occurrence_mem_variableTokens_iff line 755
  116. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.flatMap_encodeWord line 763

    Source documentation

    Emitting each token's existing unary-delimited word gives exactly the existing list-of-words serialization, with no alternative encoding.

    theorem flatMap_encodeWord (names : Fin 3 → Nat) (occurrence : Nat) (tokens : List Token) :
    tokens.flatMap (fun token => encodeWord (evalToken names occurrence token)) =
      encodeWords (evalTemplate names occurrence tokens) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.Token, OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.evalToken, OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.evalTemplate

  117. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalWordTemplate.template_bits line 772