{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R448",
  "content_hash": null,
  "slug": "levine-artifact-hint-partition-exhaustive",
  "type": "artifact",
  "title": "Exact all-partitions certificate for the 81/224 hint-matrix value",
  "summary": "An exact C++ replay enumerates all 190,899,322 partitions of fourteen columns, finds maximum \\(81/224\\), and recovers all 3,920 reported attaining partitions.",
  "relevance": "For The value of Levine's two-player coin-index game, record levine-artifact-hint-partition-exhaustive (“Exact all-partitions certificate for the 81/224 hint-matrix value”) supplies evidence or a replay used to check the packet. The record states: An exact C++ replay enumerates all 190,899,322 partitions of fourteen columns, finds maximum \\(81/224\\), and recovers all 3,920 reported attaining partitions.",
  "relevance_source": "recorded",
  "body": "The program encodes the published balanced \\(8\\times14\\) matrix as fourteen-bit row masks and checks that each row has seven 1s and each column has four. It enumerates unlabeled set partitions exactly once through restricted-growth strings. For a partition \\(P\\) with \\(C\\) classes, it enumerates all \\(2^C\\) binary class colorings \\(v\\), takes the largest of the eight exact row intersections, and computes\n\\[\nV(M;P)=\\frac{1}{14\\cdot2^C}\\sum_v\\max_r r\\mathbin{\\cdot}v.\n\\]\nComparing these fractions across \\(1\\le C\\le14\\) gives the matrix-game maximum. The run evaluates 20,732,504,062 partition-coloring pairs.\n\nThe class counts sum to the Bell number\n\\[\nB_{14}=190{,}899{,}322.\n\\]\nThe global maximum is \\(81/224\\). It occurs for 2,016 four-class partitions, 560 five-class partitions, and 1,344 six-class partitions, totaling 3,920. No other class count attains the maximum. Both the endpoint and the total match the published report. The program also checks the four-class witness from the separate Python replay and obtains numerator 81.\n\nThis certificate covers the finite optimization for the displayed hint matrix. The implication \\(p^*\\le V(M)\\) still uses the matrix-hint reduction proved by Buhler and coauthors. The computation does not close the remaining gap between \\(7/20\\) and \\(81/224\\).",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all unlabeled set partitions of the 14 columns of the published balanced 8 by 14 hint matrix",
    "bounds": {
      "hint_matrix_rows": {
        "min": 8,
        "max": 8
      },
      "hint_matrix_columns": {
        "min": 14,
        "max": 14
      },
      "partition_classes": {
        "min": 1,
        "max": 14
      },
      "partitions": {
        "min": 190899322,
        "max": 190899322
      },
      "partition_colorings": {
        "min": 20732504062,
        "max": 20732504062
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "cpp_exact_set_partition_enumerator",
    "command": "clang++ -O3 -std=c++17 tools/levine_hint_partition_exhaustive.cpp -o /tmp/levine_hint_partition_exhaustive && /tmp/levine_hint_partition_exhaustive",
    "entrypoint": "tools/levine_hint_partition_exhaustive.cpp",
    "runtime": "Apple clang 21.0.0 and the C++17 standard library",
    "citation": {
      "url": "https://arxiv.org/abs/1407.4711",
      "locator": "Buhler et al., Sections 3.1, 3.2, and 3.4, especially the 8 by 14 matrix on journal page 17"
    },
    "dependencies": [
      {
        "name": "Apple clang and libc++",
        "license": "Apache-2.0 WITH LLVM-exception"
      }
    ],
    "inputs": {
      "matrix_sha256": "9ee1416c5cfb391afdd14380ef11ec8cb1c4e857447245dc022f887476e2597c",
      "independent_four_class_partition_sha256": "66fa12593a8fc25ed32df42e572991380e806f13a9d2fae6f4d658ad2949512b"
    },
    "outputs": {
      "stdout_sha256": "e45fe1396302490acd6f095219e5e5c79abc9c5a746f5c73210a22de4b533746",
      "stdout_bytes": 1995,
      "partitions_checked": 190899322,
      "partition_colorings_checked": 20732504062,
      "partition_class_count": {
        "min": 1,
        "max": 14
      },
      "global_maximum": "81/224",
      "global_attaining_partitions": 3920,
      "attaining_class_counts": "4, 5, and 6",
      "known_partition_and_score_verified": true,
      "first_maximizer_class_count": 4,
      "first_maximizer_groups_one_based": [
        "1,2,3,4,5",
        "6,7,10,12",
        "8,9,11,13",
        "14"
      ]
    },
    "runtime_seconds": 121.83,
    "missing": [
      "source"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/1407.4711",
    "locator": "Buhler et al., Sections 3.1, 3.2, and 3.4, especially the 8 by 14 matrix on journal page 17"
  },
  "models": [],
  "relations": [
    {
      "slug": "R453",
      "title": "The published 81/224 matrix optimization has an independent exact replay",
      "object_type": "attempt",
      "relation": "produced",
      "direction": "incoming"
    },
    {
      "slug": "R455",
      "title": "The checked interval is 7/20 through 81/224, and equality at 7/20 remains open",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R447",
      "title": "Exact replay of one 81/224 hint-matrix partition",
      "object_type": "artifact",
      "relation": "strengthens",
      "direction": "outgoing"
    },
    {
      "slug": "levine-two-player-seven-twentieths",
      "title": "levine two player seven twentieths",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}