OAI/Computability/UniqueGames/Reduction/CanonicalBodyTemplateLemmas.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Lower a complete canonical-body template to the actual field-template machine. There are four saved fields per query position, numbered by field + 4 * position. The template constants depend only on finite coefficient and RHS data; names and occurrence identifiers remain saved tape contents.

  1. inductive OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.Token line 22
  2. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.evalToken line 27
  3. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.evalTemplate line 31
  4. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.nameField line 34
  5. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.recordFields line 36
  6. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.recordFields_name line 39
  7. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.recordFields_occurrence line 43
  8. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.sourceFields line 46
  9. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.liftToken line 50
  10. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.liftRecord line 55
  11. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.liftRecord_length line 58
  12. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.eval_liftToken line 61
  13. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.eval_liftRecord line 67
  14. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.recordsList line 75
  15. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.recordsList_length line 79
  16. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.eval_recordsList line 89
  17. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.ambientShift line 107
  18. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.alphabetOffset line 111
  19. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.template line 115
  20. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.template_length line 119
  21. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.eval_data line 125

    Source documentation

    Exact body serialization of general canonical data.

    theorem eval_data {n m k s d : Nat} (occ : Fin k → Fin m)
    (names : Fin m → Fin 3 → Fin n) (rhs : Fin m → F2)
    (z : Ambient s d) (a : Fin k → Fin 3 → Ambient s d) :
    evalTemplate (sourceFields occ names) (template z a (fun j => rhs (occ j))) =
      bodyWords ((ActualCanonical.data occ names rhs z a).1.2,
        (ActualCanonical.data occ names rhs z a).2) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.evalTemplate, OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.sourceFields, OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.template, OAI.UniqueGamesTheorem.Reduction.ActualCanonical.data

  22. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.alphabetOffset_data line 139
  23. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.eval_canonical line 145
  24. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.alphabetOffset_canonical line 155
  25. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.coefficientTriples line 163

    Source documentation

    The finite coefficient table's three coefficients for each local record.

    def coefficientTriples {k s d : Nat} (c : ActualEnumeration.Coefficients k (Ambient s d))
    (j : Fin k) : Fin 3 → Ambient s d :=
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.Coefficients

  26. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.fromCoefficients_hBasis line 167
  27. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.standardTriple_fromCoefficients line 172
  28. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.eval_actualQuery line 183
  29. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.alphabetOffset_actualQuery line 191
  30. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.eval_fromCoefficients line 198

    Source documentation

    Direct specialization to an actual enumerated coefficient table.

    theorem eval_fromCoefficients (S : ActualSource.Source) {k s d : Nat}
    (occ : ActualGame.Question S k) (c : ActualEnumeration.Coefficients k (Ambient s d)) :
    evalTemplate (sourceFields occ (ActualGame.names S))
        (template c.1 (coefficientTriples c) (fun j => ActualGame.rhs S (occ j))) =
      bodyWords (ActualOrbit.body (ActualGame.canonical S k s d)
        (occ, ActualEnumeration.fromCoefficients k (Ambient s d) c)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualSource.Source, OAI.UniqueGamesTheorem.Reduction.ActualGame.Question, OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.Coefficients, OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.evalTemplate, OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.sourceFields, OAI.UniqueGamesTheorem.Reduction.ActualGame.names, OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.template, OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.coefficientTriples, OAI.UniqueGamesTheorem.Reduction.ActualGame.rhs, OAI.UniqueGamesTheorem.Reduction.ActualOrbit.body, OAI.UniqueGamesTheorem.Reduction.ActualGame.canonical, OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.fromCoefficients

  31. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.alphabetOffset_fromCoefficients line 207
  32. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.actualEdge_permutation line 217

    Source documentation

    Both permutation offsets of an actual edge are the same finite expressions used by the corresponding canonical-body templates.

    theorem actualEdge_permutation (S : ActualSource.Source) (k : Nat) {s d : Nat}
    (g : ActualSource.SplitGadget s d) (omega : ActualGame.Outcome S k g) :
    (ActualGame.edge S k g omega).permutation =
      Encoding.translationTable
        (alphabetOffset ((ActualGame.leftQuery S k g omega).2 (ActualHomogeneous.hBasis k))
          (ActualCanonical.standardTriple (ActualGame.leftQuery S k g omega).2)
          (fun j => ActualGame.rhs S ((ActualGame.leftQuery S k g omega).1 j)))
        (alphabetOffset ((ActualGame.rightQuery S k g omega).2 (ActualHomogeneous.hBasis k))
          (ActualCanonical.standardTriple (ActualGame.rightQuery S k g omega).2)
          (fun j => ActualGame.rhs S ((ActualGame.rightQuery S k g omega).1 j))) := rfl

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualSource.Source, OAI.UniqueGamesTheorem.Reduction.ActualSource.SplitGadget, OAI.UniqueGamesTheorem.Reduction.ActualGame.Outcome, OAI.UniqueGamesTheorem.Reduction.ActualGame.edge, OAI.UniqueGamesTheorem.Reduction.Encoding.translationTable, OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.alphabetOffset, OAI.UniqueGamesTheorem.Reduction.ActualGame.leftQuery, OAI.UniqueGamesTheorem.Reduction.ActualHomogeneous.hBasis, OAI.UniqueGamesTheorem.Reduction.ActualCanonical.standardTriple, OAI.UniqueGamesTheorem.Reduction.ActualGame.rhs, OAI.UniqueGamesTheorem.Reduction.ActualGame.rightQuery

  33. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.flatMap_encodeWord line 228
  34. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.actualQuery_bits line 237
  35. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.fieldEquiv line 263
  36. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.fieldIndex line 266
  37. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.fieldIndex_val line 269
  38. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.savedFields line 272
  39. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.savedFields_fieldIndex line 275
  40. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.lowerToken line 280
  41. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.lowerTemplate line 284
  42. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.lowerTemplate_length line 287
  43. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.tokenOutput_lowerToken line 290
  44. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.templateOutput_lowerTemplate line 297
  45. def OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.template line 306

    Source documentation

    This fixed token list is directly accepted by the actual template machine.

    def template {k s d : Nat} (z : Ambient s d) (a : Fin k → Fin 3 → Ambient s d)
    (b : Fin k → F2) : List (MachineFieldTemplate.Token (4*k)) :=
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.Token

  46. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.template_length line 310
  47. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.templateOutput_data line 315
  48. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.templateOutput_actualQuery line 324
  49. theorem OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.templateOutput_fromCoefficients line 334

    Source documentation

    Exact output using the finite coefficient table directly as program data.

    theorem templateOutput_fromCoefficients (S : ActualSource.Source) {k s d : Nat}
    (occ : ActualGame.Question S k) (c : ActualEnumeration.Coefficients k (Ambient s d)) :
    MachineFieldTemplate.templateOutput
        (template c.1 (CanonicalBodyTemplate.coefficientTriples c)
          (fun j => ActualGame.rhs S (occ j)))
        (savedFields (CanonicalBodyTemplate.sourceFields occ (ActualGame.names S))) =
      encodeWords (bodyWords (ActualOrbit.body (ActualGame.canonical S k s d)
        (occ, ActualEnumeration.fromCoefficients k (Ambient s d) c))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualSource.Source, OAI.UniqueGamesTheorem.Reduction.ActualGame.Question, OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.Coefficients, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.templateOutput, OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.template, OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.coefficientTriples, OAI.UniqueGamesTheorem.Reduction.ActualGame.rhs, OAI.UniqueGamesTheorem.Reduction.CanonicalBodyMachine.savedFields, OAI.UniqueGamesTheorem.Reduction.CanonicalBodyTemplate.sourceFields, OAI.UniqueGamesTheorem.Reduction.ActualGame.names, OAI.UniqueGamesTheorem.Reduction.ActualOrbit.body, OAI.UniqueGamesTheorem.Reduction.ActualGame.canonical, OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.fromCoefficients

  50. def OAI.UniqueGamesTheorem.Reduction.OccurrenceTupleOrder.readCoordinates line 365

    Source documentation

    Read the physical saved digit positions in reverse coordinate order.

    def readCoordinates {m k : Nat} (digits : Fin k → Fin m) : Fin k → Fin m :=
…
  51. theorem OAI.UniqueGamesTheorem.Reduction.OccurrenceTupleOrder.readCoordinates_apply line 368
  52. theorem OAI.UniqueGamesTheorem.Reduction.OccurrenceTupleOrder.readCoordinates_involutive line 371
  53. def OAI.UniqueGamesTheorem.Reduction.OccurrenceTupleOrder.coordinateEquiv line 376
  54. theorem OAI.UniqueGamesTheorem.Reduction.OccurrenceTupleOrder.readCoordinates_snoc line 382
  55. theorem OAI.UniqueGamesTheorem.Reduction.OccurrenceTupleOrder.tupleOrder_readCoordinates line 388

    Source documentation

    Exact equality of occurrence lists after reading saved digits in reverse coordinate order. This includes dimension zero and radix zero.

    theorem tupleOrder_readCoordinates (m k : Nat) :
    (MachineTupleOdometer.tupleOrder m k).map readCoordinates =
      ActualEnumeration.functions (List.finRange m) k := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.OccurrenceTupleOrder.readCoordinates, OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.functions

  56. theorem OAI.UniqueGamesTheorem.Reduction.OccurrenceTupleOrder.functions_readCoordinates line 413
  57. theorem OAI.UniqueGamesTheorem.Reduction.OccurrenceTupleOrder.functions_flatMap line 422

    Source documentation

    An arbitrary exact emitted list, including serialized edge bytes, inherits the order identity. There is no permutation or counting-only replacement.

    theorem functions_flatMap (m k : Nat) (emit : (Fin k → Fin m) → List α) :
    (ActualEnumeration.functions (List.finRange m) k).flatMap emit =
      (MachineTupleOdometer.tupleOrder m k).flatMap
        (fun digits => emit (readCoordinates digits)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.functions, OAI.UniqueGamesTheorem.Reduction.OccurrenceTupleOrder.readCoordinates

  58. theorem OAI.UniqueGamesTheorem.Reduction.OccurrenceTupleOrder.actualSchedule_order line 439

    Source documentation

    Apply the coordinate readout to an existing actual odometer schedule. Its visit-order theorem already follows from the real nested-cycle constructors.

    theorem actualSchedule_order
    (tree : MachineTupleOdometer.NestedCycle m current remaining bodyLabel
      checkLabel resetLabel program k exitLabel start finish) :
    tree.order.map readCoordinates = ActualEnumeration.functions (List.finRange m) k := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.OccurrenceTupleOrder.readCoordinates, OAI.UniqueGamesTheorem.Reduction.ActualEnumeration.functions

  59. theorem OAI.UniqueGamesTheorem.Reduction.OccurrenceTupleOrder.actualSchedule_flatMap line 445
  60. structure OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input line 472
  61. abbrev OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Table line 477
  62. def OAI.UniqueGamesTheorem.Reduction.SourceEncoding.equationWords line 479
  63. def OAI.UniqueGamesTheorem.Reduction.SourceEncoding.inputWords line 482
  64. def OAI.UniqueGamesTheorem.Reduction.SourceEncoding.inputBits line 485
  65. def OAI.UniqueGamesTheorem.Reduction.SourceEncoding.parseEquation line 487
  66. theorem OAI.UniqueGamesTheorem.Reduction.SourceEncoding.parseEquation_encoded line 503
  67. def OAI.UniqueGamesTheorem.Reduction.SourceEncoding.parseEquations line 510
  68. theorem OAI.UniqueGamesTheorem.Reduction.SourceEncoding.parseEquations_encoded line 519

    Source documentation

    Parsing preserves the entire ordered list, including all equal entries.

    @[simp] theorem parseEquations_encoded {n : Nat}
    (equations : List (CloneGap.Equation (Fin n))) (rest : List Nat) :
    parseEquations n equations.length (equations.flatMap equationWords ++ rest) =
      some (equations, rest) := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.CloneGap.Equation, OAI.UniqueGamesTheorem.Reduction.SourceEncoding.parseEquations, OAI.UniqueGamesTheorem.Reduction.SourceEncoding.equationWords

  69. def OAI.UniqueGamesTheorem.Reduction.SourceEncoding.decodeInputWords line 528
  70. theorem OAI.UniqueGamesTheorem.Reduction.SourceEncoding.decodeInputWords_encoded line 538
  71. def OAI.UniqueGamesTheorem.Reduction.SourceEncoding.decodeInputBits line 547
  72. theorem OAI.UniqueGamesTheorem.Reduction.SourceEncoding.decodeInputBits_encoded line 550
  73. theorem OAI.UniqueGamesTheorem.Reduction.SourceEncoding.inputWords_injective line 554
  74. theorem OAI.UniqueGamesTheorem.Reduction.SourceEncoding.inputBits_injective line 559
  75. theorem OAI.UniqueGamesTheorem.Reduction.SourceEncoding.equationWords_length line 564
  76. theorem OAI.UniqueGamesTheorem.Reduction.SourceEncoding.equationsWords_length line 567
  77. theorem OAI.UniqueGamesTheorem.Reduction.SourceEncoding.inputWords_length line 576
  78. theorem OAI.UniqueGamesTheorem.Reduction.SourceEncoding.equationBits_length_le line 581
  79. theorem OAI.UniqueGamesTheorem.Reduction.SourceEncoding.equationsBits_length_le line 588
  80. theorem OAI.UniqueGamesTheorem.Reduction.SourceEncoding.inputBits_length line 599
  81. theorem OAI.UniqueGamesTheorem.Reduction.SourceEncoding.inputBits_length_le line 606
  82. theorem OAI.UniqueGamesTheorem.Reduction.SourceEncoding.inputBits_length_ge_variables line 612
  83. theorem OAI.UniqueGamesTheorem.Reduction.SourceEncoding.inputBits_length_ge_equations line 615