{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R81",
  "content_hash": null,
  "slug": "bsm12-claim-certified-five-to-seven",
  "type": "claim",
  "title": "The certified interval for M6 is 5 through 7",
  "summary": "A first-reply counting argument proves five queries are necessary, and a deterministic greedy decision tree identifies all 924 secrets in at most seven.",
  "relevance": "For Optimal balanced-subset Mastermind on twelve points, record bsm12-claim-certified-five-to-seven (“The certified interval for M6 is 5 through 7”) records a bound, answer, status fact, or structural consequence. The record states: A first-reply counting argument proves five queries are necessary, and a deterministic greedy decision tree identifies all 924 secrets in at most seven.",
  "relevance_source": "recorded",
  "body": "Let \\(M_6\\) be the minimum worst-case depth. Fix any first query \\(Q\\). A reply \\(j\\) leaves\n\\[\n\\binom{6}{j}\\binom{6}{6-j}=\\binom{6}{j}^{2}\n\\]\npossible secrets. The seven class sizes are\n\\[\n1,36,225,400,225,36,1.\n\\]\nAfter the reply 3, a strategy with total depth four would have three queries left. Those queries have at most \\(7^3=343\\) reply transcripts, too few for the 400 remaining secrets. Hence \\(M_6\\geq5\\).\n\nFor the upper endpoint, order the 924 queries lexicographically as increasing six-tuples. At each nonsingleton knowledge state, score every query by\n\\[\n\\left(\\max_j |C_j|,\\ \\sum_j |C_j|^2,\\ -|\\{j:C_j\\ne\\varnothing\\}|\\right),\n\\]\nwhere \\(C_j\\) is the reply-\\(j\\) child. Choose the lexicographically first query with minimum score. The executable replay builds the whole tree. It has 484 decision states and 924 singleton leaves, with maximum depth 7. Therefore\n\\[\n\\boxed{5\\leq M_6\\leq7}.\n\\]\nThe computation leaves \\(M_6=5\\), \\(6\\), and \\(7\\) possible.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "bounded",
    "statement": "adaptive identification of every six-element secret among the six-element subsets of a twelve-element ground set, using only six-element intersection queries",
    "bounds": {
      "ground_set_size": {
        "min": 12,
        "max": 12
      },
      "secret_size": {
        "min": 6,
        "max": 6
      },
      "allowed_queries": {
        "min": 924,
        "max": 924
      },
      "secrets": {
        "min": 924,
        "max": 924
      },
      "certified_query_lower_bound": {
        "min": 5,
        "max": 5
      },
      "certified_query_upper_bound": {
        "min": 7,
        "max": 7
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.4153/CJM-1966-007-2",
      "locator": "The lower bound is the self-contained first-reply argument in this record; the upper bound is reproduced by bsm12-artifact-greedy-depth-seven"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.4153/CJM-1966-007-2",
    "locator": "The lower bound is the self-contained first-reply argument in this record; the upper bound is reproduced by bsm12-artifact-greedy-depth-seven"
  },
  "relations": [
    {
      "slug": "R78",
      "title": "Exhaustive replay of the depth-7 greedy tree",
      "object_type": "artifact",
      "relation": "verifies",
      "direction": "incoming"
    },
    {
      "slug": "R80",
      "title": "The closest literature treats broader query models",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "R79",
      "title": "Close the remaining two-query gap by certified minimax search",
      "object_type": "attempt",
      "relation": "targets",
      "direction": "incoming"
    },
    {
      "slug": "balanced-subset-mastermind-twelve",
      "title": "balanced subset mastermind twelve",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}