{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R1820",
  "content_hash": null,
  "slug": "cdc-formalization-upstream-lean-v1",
  "type": "formalization",
  "title": "Pinned Lean proof in cdc-lean",
  "summary": "A public Lean 4.31.0 development proves the cycle-double-cover endpoint without project-specific axioms; controlled TheoremDB verification is still pending.",
  "relevance": "This is a complete public formal proof of the canonical target in a pinned Lean world, awaiting replay by TheoremDB's verifier.",
  "relevance_source": "recorded",
  "body": "The endpoint `CDCLean.cycleDoubleCover_of_bridgeless` takes a finite edge-labelled loopless multigraph and a proof of its cut-based bridgeless predicate, and returns a nonempty cycle double cover. Parallel edges, disconnected graphs, and edgeless graphs are covered. The pinned repository records a successful full build, a source scan with no `sorry`, `admit`, `native_decide`, custom `axiom`, `opaque`, or `unsafe`, and an axiom report containing only `propext`, `Classical.choice`, and `Quot.sound`. Those are upstream results. TheoremDB has pinned the source and dependency world but has not yet executed this repository inside its controlled verifier, so the formalization remains unverified here.",
  "status": "pending_verification",
  "evidence_grade": "unverified_formalization",
  "scope": {
    "kind": "universal",
    "statement": "the exact finite loopless multigraph theorem represented by CDCLean.FiniteGraph"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "lean4_formalization_source",
    "command": "lake build CDCLean && lake env lean CDCLean/Audit.lean",
    "entrypoint": "CDCLean.cycleDoubleCover_of_bridgeless",
    "runtime": "Lean 4.31.0 with mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8",
    "citation": {
      "url": "https://github.com/openai/cdc-lean/tree/577e9d9ea326d520f80672ee69b830bf1d513df5",
      "locator": "CDCLean/Main.lean theorem CDCLean.cycleDoubleCover_of_bridgeless and VERIFICATION.md"
    },
    "outputs": {
      "upstream_expected_exit_code": 0,
      "upstream_axiom_audit": [
        "propext",
        "Classical.choice",
        "Quot.sound"
      ],
      "theoremdb_controlled_verification": "pending"
    },
    "missing": [
      "source"
    ]
  },
  "formal_statement": "theorem CDCLean.cycleDoubleCover_of_bridgeless\n    {V E : Type u} [Fintype V] [Fintype E] [DecidableEq V] [DecidableEq E]\n    (G : FiniteGraph V E) (hb : G.Bridgeless) :\n    Nonempty G.CycleDoubleCover",
  "source": {
    "url": "https://github.com/openai/cdc-lean/tree/577e9d9ea326d520f80672ee69b830bf1d513df5",
    "locator": "CDCLean/Main.lean theorem CDCLean.cycleDoubleCover_of_bridgeless and VERIFICATION.md"
  },
  "relations": [
    {
      "slug": "R1819",
      "title": "Every finite bridgeless graph has a cycle double cover",
      "object_type": "claim",
      "relation": "formalizes",
      "direction": "outgoing"
    },
    {
      "slug": "cycle-double-cover-conjecture",
      "title": "cycle double cover conjecture",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}