OAI/Computability/MaxCut/Games/CanonicalWordTemplate.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.MaxCutGames.Reduction.CanonicalWordTemplate.Token line 11

    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
  2. def OAI.MaxCutGames.Reduction.CanonicalWordTemplate.evalToken line 17
  3. def OAI.MaxCutGames.Reduction.CanonicalWordTemplate.evalTemplate line 22
  4. def OAI.MaxCutGames.Reduction.CanonicalWordTemplate.isVariable line 26
  5. def OAI.MaxCutGames.Reduction.CanonicalWordTemplate.variableTokens line 31
  6. def OAI.MaxCutGames.Reduction.CanonicalWordTemplate.blankTemplate line 33
  7. def OAI.MaxCutGames.Reduction.CanonicalWordTemplate.singleTemplate line 37
  8. def OAI.MaxCutGames.Reduction.CanonicalWordTemplate.fullTemplate line 42
  9. def OAI.MaxCutGames.Reduction.CanonicalWordTemplate.template line 49

    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.MaxCutGames.Reduction.CanonicalWordTemplate.Token

  10. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.blankTemplate_length line 56
  11. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.singleTemplate_length line 58
  12. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.fullTemplate_length line 61
  13. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.template_length line 64
  14. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.evalTemplate_length line 69
  15. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.eval_blankTemplate line 73
  16. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.eval_singleTemplate line 77
  17. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.eval_fullTemplate line 83
  18. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.eval_template line 90

    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.MaxCutGames.Reduction.CanonicalWordTemplate.evalTemplate, OAI.MaxCutGames.Reduction.CanonicalWordTemplate.template, OAI.MaxCutGames.Reduction.ActualCanonical.record

  19. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.variableTokens_blankTemplate line 97
  20. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.variableTokens_singleTemplate line 99
  21. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.variableTokens_fullTemplate line 103
  22. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.variableTokens_template line 109

    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.MaxCutGames.Reduction.CanonicalWordTemplate.variableTokens, OAI.MaxCutGames.Reduction.CanonicalWordTemplate.template

  23. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.variableTokens_template_length_le_one line 119
  24. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.name_mem_variableTokens_iff line 124
  25. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.occurrence_mem_variableTokens_iff line 132
  26. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.flatMap_encodeWord line 140

    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.MaxCutGames.Reduction.CanonicalWordTemplate.Token, OAI.MaxCutGames.Reduction.CanonicalWordTemplate.evalToken, OAI.MaxCutGames.Reduction.CanonicalWordTemplate.evalTemplate

  27. theorem OAI.MaxCutGames.Reduction.CanonicalWordTemplate.template_bits line 149
  28. inductive OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.Token line 164
  29. def OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.evalToken line 171
  30. def OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.evalTemplate line 175
  31. def OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.nameField line 178
  32. def OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.recordFields line 180
  33. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.recordFields_name line 183
  34. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.recordFields_occurrence line 187
  35. def OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.sourceFields line 190
  36. def OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.liftToken line 194
  37. def OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.liftRecord line 199
  38. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.liftRecord_length line 202
  39. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.eval_liftToken line 205
  40. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.eval_liftRecord line 211
  41. def OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.recordsList line 219
  42. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.recordsList_length line 223
  43. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.eval_recordsList line 233
  44. def OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.ambientShift line 251
  45. def OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.alphabetOffset line 255
  46. def OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.template line 259
  47. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.template_length line 263
  48. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.eval_data line 269

    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.MaxCutGames.Reduction.CanonicalBodyTemplate.evalTemplate, OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.sourceFields, OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.template, OAI.MaxCutGames.Reduction.ActualCanonical.data

  49. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.alphabetOffset_data line 283
  50. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.eval_canonical line 289
  51. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.alphabetOffset_canonical line 299
  52. def OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.coefficientTriples line 307

    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.MaxCutGames.Reduction.ActualEnumeration.Coefficients

  53. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.fromCoefficients_hBasis line 311
  54. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.standardTriple_fromCoefficients line 316
  55. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.eval_actualQuery line 327
  56. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.alphabetOffset_actualQuery line 335
  57. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.eval_fromCoefficients line 342

    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.MaxCutGames.Reduction.ActualSource.Source, OAI.MaxCutGames.Reduction.ActualGame.Question, OAI.MaxCutGames.Reduction.ActualEnumeration.Coefficients, OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.evalTemplate, OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.sourceFields, OAI.MaxCutGames.Reduction.ActualGame.names, OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.template, OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.coefficientTriples, OAI.MaxCutGames.Reduction.ActualGame.rhs, OAI.MaxCutGames.Reduction.ActualOrbit.body, OAI.MaxCutGames.Reduction.ActualGame.canonical, OAI.MaxCutGames.Reduction.ActualEnumeration.fromCoefficients

  58. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.alphabetOffset_fromCoefficients line 351
  59. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.actualEdge_permutation line 361

    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.MaxCutGames.Reduction.ActualSource.Source, OAI.MaxCutGames.Reduction.ActualSource.SplitGadget, OAI.MaxCutGames.Reduction.ActualGame.Outcome, OAI.MaxCutGames.Reduction.ActualGame.edge, OAI.MaxCutGames.Reduction.Encoding.translationTable, OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.alphabetOffset, OAI.MaxCutGames.Reduction.ActualGame.leftQuery, OAI.MaxCutGames.Reduction.ActualHomogeneous.hBasis, OAI.MaxCutGames.Reduction.ActualCanonical.standardTriple, OAI.MaxCutGames.Reduction.ActualGame.rhs, OAI.MaxCutGames.Reduction.ActualGame.rightQuery

  60. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.flatMap_encodeWord line 372
  61. theorem OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.actualQuery_bits line 381