{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R1819",
  "content_hash": null,
  "slug": "cdc-claim-proof-2026",
  "type": "claim",
  "title": "Every finite bridgeless graph has a cycle double cover",
  "summary": "The 2026 proof turns a nowhere-zero flow over the three-dimensional vector space over the two-element field into a family of cycles covering every edge twice.",
  "relevance": "This is the published resolution of the canonical conjecture, supported by two independent human expositions.",
  "relevance_source": "recorded",
  "body": "The standard reduction lets us work with a loopless cubic multigraph. Give it a nowhere-zero flow f with values in Gamma = F_2^3, whose existence follows from the Jaeger-Kilpatrick eight-flow theorem and Tutte's group-flow theorem. At a cubic vertex, write the three nonzero incident values as x, y, z, so x + y + z = 0. Choose local offsets g_(v,e) so that, after any common translation t_v, the two-element sets {t_v + g_(v,e), t_v + g_(v,e) + f(e)} have a parity property: each element of Gamma occurs on zero or two incident edges.\n\nThe local pairs must agree at the two ends of every edge. For e = uv, this is equivalent to finding vertex translations t_v in Gamma and bits epsilon_e in F_2 satisfying t_u + t_v + epsilon_e f(e) = g_(u,e) + g_(v,e). Regard the left side as a linear map L. A dual obstruction is a family of linear functionals eta_e in Gamma* with eta_e(f(e)) = 0 and the sum of eta_e over edges incident to v equal to 0 at each vertex. The local cubic calculation shows that the sum of eta_e(g_(v,e)) over incident edges is the parity of the nonzero incident eta_e. Summing over vertices counts each nonzero edge functional twice, so every obstruction annihilates the right side. Linear duality therefore gives the required t_v and epsilon_e.\n\nDefine the common edge pair P_e using either endpoint. For each s in Gamma, take the edges whose pair contains s. Every vertex has degree zero or two in this edge set, so it is a disjoint union of cycles. Each edge belongs to exactly two of these eight edge sets because P_e has two elements. Taking all cycle components with multiplicity gives a cycle double cover. The cubic reduction carries the cover back to the original bridgeless graph.",
  "status": "established",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "universal",
    "statement": "all finite bridgeless loopless undirected multigraphs, including disconnected graphs and graphs with parallel edges"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_proof.pdf",
      "locator": "Theorem 1.1 and Section 2, pages 1-3, cross-checked against the expositions by Geelen and Oum"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_proof.pdf",
    "locator": "Theorem 1.1 and Section 2, pages 1-3, cross-checked against the expositions by Geelen and Oum"
  },
  "models": [
    {
      "provider": "OpenAI",
      "model": "GPT-5.6 Sol Ultra",
      "role": "proof generation"
    },
    {
      "provider": "OpenAI",
      "model": "GPT-5.6 Sol",
      "role": "writeup"
    }
  ],
  "continuation": null,
  "relations": [
    {
      "slug": "R1820",
      "title": "Pinned Lean proof in cdc-lean",
      "object_type": "formalization",
      "relation": "formalizes",
      "direction": "incoming"
    },
    {
      "slug": "cycle-double-cover-conjecture",
      "title": "cycle double cover conjecture",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}