{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R177",
  "content_hash": null,
  "slug": "cubic20ising-claim-matching-upper-bound",
  "type": "claim",
  "title": "Every connected cubic graph on 20 vertices has at most 254,658 ground states",
  "summary": "Local cut optimality injects spin pairs into graph matchings, and the sharp regular-graph partition-function bound controls their total number.",
  "relevance": "For Most antiferromagnetic ground states in a 3-connected cubic graph on twenty vertices, record cubic20ising-claim-matching-upper-bound (“Every connected cubic graph on 20 vertices has at most 254,658 ground states”) records a bound, answer, status fact, or structural consequence. The record states: Local cut optimality injects spin pairs into graph matchings, and the sharp regular-graph partition-function bound controls their total number.",
  "relevance_source": "recorded",
  "body": "For a cut with \\(k\\) crossing edges incident to a cubic vertex \\(v\\), flipping \\(v\\) changes the cut size by \\(3-2k\\). A maximum cut therefore has \\(k\\geq2\\) at every vertex. Each vertex is incident to at most one same-spin edge, so the set \\(U\\) of same-spin edges is a matching.\n\nGiven \\(U\\), label its edges with equality and all other graph edges with inequality. Connectivity means that a choice of one root spin forces every other spin. Thus each feasible \\(U\\) comes from at most two assignments, related by global flip. If \\(M_G(1)\\) denotes the total number of matchings, including the empty matching, then\n\\[\n\\operatorname{gs}(G)\\leq2M_G(1).\n\\]\n\nThe integrated form of Theorem 3 in Davies, Jenssen, Perkins, and Roberts gives\n\\[\nM_G(1)^{1/20}\\leq M_{K_{3,3}}(1)^{1/6}.\n\\]\nThe four matching sizes in \\(K_{3,3}\\) contribute \\(1,9,18,6\\), whose sum is 34. Consequently \\(M_G(1)\\leq\\lfloor34^{10/3}\\rfloor=127{,}329\\), and \\(\\operatorname{gs}(G)\\leq254{,}658\\). This applies before imposing 3-connectivity.",
  "status": "established",
  "evidence_grade": "mathematical_identity",
  "scope": {
    "kind": "bounded",
    "statement": "every connected cubic graph on exactly 20 vertices",
    "bounds": {
      "vertices": {
        "min": 20,
        "max": 20
      },
      "degree": {
        "min": 3,
        "max": 3
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://arxiv.org/abs/1508.04675",
      "locator": "Davies, Jenssen, Perkins, and Roberts, Theorem 3; the local-optimality reduction is proved in this record"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/1508.04675",
    "locator": "Davies, Jenssen, Perkins, and Roberts, Theorem 3; the local-optimality reduction is proved in this record"
  },
  "models": [],
  "relations": [
    {
      "slug": "R175",
      "title": "The certified interval is 36 through 254,658 ground states",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "cubic-graph-twenty-ising-degeneracy",
      "title": "cubic graph twenty ising degeneracy",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}