{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R447",
  "content_hash": null,
  "slug": "levine-artifact-hint-attaining-partition-replay",
  "type": "artifact",
  "title": "Exact replay of one 81/224 hint-matrix partition",
  "summary": "A deterministic replay checks all 16 colorings of one four-class partition and obtains conditional matrix-game value \\(81/224\\).",
  "relevance": "For The value of Levine's two-player coin-index game, record levine-artifact-hint-attaining-partition-replay (“Exact replay of one 81/224 hint-matrix partition”) supplies evidence or a replay used to check the packet. The record states: A deterministic replay checks all 16 colorings of one four-class partition and obtains conditional matrix-game value \\(81/224\\).",
  "relevance_source": "recorded",
  "body": "The published \\(8\\times14\\) balanced matrix was transcribed row by row. An exploratory search found the following partition of its one-based column numbers:\n\\[\n\\{4,7,14\\},\\quad\\{2,3,10,11\\},\\quad\n\\{5,6,8,12\\},\\quad\\{1,9,13\\}.\n\\]\nThe replay checks that every column has four zeros and four ones and that the groups partition all fourteen columns. For each of the \\(2^4=16\\) independent color assignments to the groups, it constructs the induced fourteen-bit vector and takes the largest dot product with a matrix row. The sixteen maxima are\n\\[\n0,3,4,5,4,6,6,7,3,5,5,7,5,7,7,7.\n\\]\nTheir sum is \\(81\\), so the conditional matrix-game value is\n\\[\n\\frac{81}{14\\cdot16}=\\frac{81}{224}.\n\\]\nA second grouped-sum implementation returns the same maxima. This artifact checks attainment. The separate all-partitions artifact proves that every other column partition has value at most \\(81/224\\).",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "one four-class partition of the published 8 by 14 balanced hint matrix and all of its class-color assignments",
    "bounds": {
      "hint_matrix_rows": {
        "min": 8,
        "max": 8
      },
      "hint_matrix_columns": {
        "min": 14,
        "max": 14
      },
      "partition_classes": {
        "min": 4,
        "max": 4
      },
      "class_color_assignments": {
        "min": 16,
        "max": 16
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "python_exact_hint_partition_replay",
    "command": "python3 tools/levine_hint_partition_replay.py",
    "entrypoint": "tools/levine_hint_partition_replay.py",
    "runtime": "CPython 3.9.6, standard library only",
    "citation": {
      "url": "https://arxiv.org/abs/1407.4711",
      "locator": "Buhler et al., Sections 3.1 and 3.2, especially the matrix on journal page 17"
    },
    "dependencies": [
      {
        "name": "CPython standard library",
        "license": "Python-2.0"
      }
    ],
    "inputs": {
      "matrix_sha256": "9ee1416c5cfb391afdd14380ef11ec8cb1c4e857447245dc022f887476e2597c",
      "partition_sha256": "66fa12593a8fc25ed32df42e572991380e806f13a9d2fae6f4d658ad2949512b"
    },
    "outputs": {
      "stdout_sha256": "83dcdd1ab7bea03a91f5710a77cea8fa674f6bd232e956e6aa0594e72d188024",
      "stdout_bytes": 832,
      "row_scores_and_maxima_sha256": "f8d0a046eba184f0ec30166d70dd6ff48989dee1e84b58d729b5b55d63e587d4",
      "unreduced_value": "81/224",
      "reduced_value": "81/224",
      "direct_and_grouped_implementations_agree": true
    },
    "runtime_seconds": 0.03,
    "missing": [
      "source"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/1407.4711",
    "locator": "Buhler et al., Sections 3.1 and 3.2, especially the matrix on journal page 17"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R453",
      "title": "The published 81/224 matrix optimization has an independent exact replay",
      "object_type": "attempt",
      "relation": "produced",
      "direction": "incoming"
    },
    {
      "slug": "R448",
      "title": "Exact all-partitions certificate for the 81/224 hint-matrix value",
      "object_type": "artifact",
      "relation": "strengthens",
      "direction": "incoming"
    },
    {
      "slug": "levine-two-player-seven-twentieths",
      "title": "levine two player seven twentieths",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}