{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R138",
  "content_hash": null,
  "slug": "cdt6-claim-exact-leaf-complexity",
  "type": "claim",
  "title": "The minimum decision-tree leaf count is 1,693",
  "summary": "An exact recurrence over partial edge assignments gives a 1,693-leaf policy and a matching lower certificate.",
  "relevance": "For Leaf complexity of six-vertex graph connectivity, record cdt6-claim-exact-leaf-complexity (“The minimum decision-tree leaf count is 1,693”) records a bound, answer, status fact, or structural consequence. The record states: An exact recurrence over partial edge assignments gives a 1,693-leaf policy and a matching lower certificate.",
  "relevance_source": "recorded",
  "body": "Let \\(P\\) be the set of queried-present edges and \\(A\\) the set of queried-absent edges. Write \\(\\lambda(P,A)\\) for the fewest leaves needed to finish from this partial assignment. Monotonicity gives two terminal cases. If \\((V,P)\\) is connected, every completion is connected. If \\((V,K_6\\setminus A)\\) is disconnected, every completion is disconnected. A terminal state has value 1.\n\nAt every remaining state, the root of a continuation queries some unknown edge. Its two branches are independent subproblems, so\n\\[\n\\lambda(P,A)=\\min_{e\\notin P\\cup A}\n\\bigl(\\lambda(P,A\\cup\\{e\\})+\\lambda(P\\cup\\{e\\},A)\\bigr).\n\\]\nThis recurrence is an equality. Each query supplies an upper bound by joining optimal child trees. Every decision tree has some root query, so its leaf count is at least the corresponding child sum.\n\nA permutation of the six vertices preserves the recurrence. The exact computation replaces each state by the least packed pair \\((P,A)\\) among all 720 vertex relabelings. It evaluates every query choice, records an attaining edge, and obtains\n\\[\n\\lambda(\\varnothing,\\varnothing)=1693.\n\\]\nThe resulting certificate contains 23,352 canonical states. A separate pass checks each record. For every possible query, the two child values sum to at least the stored value. The recorded query attains equality. Following those recorded queries from the root reaches exactly 1,693 terminal leaves.\n\nFor a labeled state, choose a vertex permutation carrying it to its canonical representative, read the stored canonical edge, and query the inverse image of that edge. Repeating this after each answer reconstructs an optimal policy. At the root the certificate chooses edge \\(01\\); every edge is equivalent there by symmetry.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "bounded",
    "statement": "connectivity of every simple graph on six labeled vertices in the deterministic edge-query model",
    "bounds": {
      "vertices": {
        "min": 6,
        "max": 6
      },
      "possible_edges": {
        "min": 15,
        "max": 15
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.1145/3564246.3585199",
      "locator": "Exact isomorphism-reduced dynamic program and independently replayed certificate in cdt6-artifact-isomorphism-dp-certificate, executed 2026-07-24"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1145/3564246.3585199",
    "locator": "Exact isomorphism-reduced dynamic program and independently replayed certificate in cdt6-artifact-isomorphism-dp-certificate, executed 2026-07-24"
  },
  "relations": [
    {
      "slug": "R137",
      "title": "Minimal positive and maximal negative inputs require 1,327 leaves",
      "object_type": "claim",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R136",
      "title": "Isomorphism-reduced optimal-policy and lower-bound certificate",
      "object_type": "artifact",
      "relation": "verifies",
      "direction": "incoming"
    },
    {
      "slug": "R139",
      "title": "Classical graph-property results concern depth rather than this six-vertex leaf count",
      "object_type": "claim",
      "relation": "contextualizes",
      "direction": "incoming"
    },
    {
      "slug": "connectivity-decision-tree-six-leaves",
      "title": "connectivity decision tree six leaves",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}