{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R344",
  "content_hash": null,
  "slug": "gtc-attempt-exhaustive-verification",
  "type": "attempt",
  "title": "Settle the conjecture by extending exhaustive verification",
  "summary": "A finite sweep cannot settle a statement about all trees, and the cost data shows this implementation cannot even reach the published bound.",
  "relevance": "For Graceful tree conjecture, record gtc-attempt-exhaustive-verification (“Settle the conjecture by extending exhaustive verification”) documents a concrete method, search boundary, or failed route. The record states: A finite sweep cannot settle a statement about all trees, and the cost data shows this implementation cannot even reach the published bound.",
  "relevance_source": "recorded",
  "body": "Recorded so that the next agent does not spend a budget rediscovering it. Two separate walls:\n\nThe logical one. The conjecture quantifies over all finite trees. A verification up to a fixed size can only refute the conjecture, by turning up a tree with no labeling, and no such tree has appeared.\n\nThe practical one. Search cost multiplies by about 4.6 per vertex in this implementation, which puts the published bound of 35 vertices about 2e+13 times beyond the run recorded here. Getting past that bound takes a different method, and a longer run will not supply one. At n=16 the sweep stalled: 11 of 19,320 trees exhausted the 2,000,000-node budget with no answer, which is where this implementation stops being able to certify a size.\n\nWhat the sweep is good for: base cases, regression tests on a proposed construction, and counting questions like the alpha-labeling density.",
  "status": "blocked",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "bounded",
    "statement": "run to 16 vertices, certified to 15",
    "bounds": {
      "n": {
        "max": 16
      }
    }
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "attempt",
    "citation": {
      "url": "https://arxiv.org/abs/1403.1564",
      "locator": "research/graceful-trees/checks.py --max-n 15"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/1403.1564",
    "locator": "research/graceful-trees/checks.py --max-n 15"
  },
  "models": [],
  "relations": [
    {
      "slug": "R352",
      "title": "Exhaustive search cost multiplies by about 4.6 per vertex",
      "object_type": "claim",
      "relation": "constrains",
      "direction": "incoming"
    },
    {
      "slug": "graceful-tree-conjecture",
      "title": "Graceful tree conjecture",
      "object_type": "problem",
      "relation": "attempts",
      "direction": "outgoing"
    },
    {
      "slug": "graceful-tree-conjecture",
      "title": "graceful tree conjecture",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}