{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R1824",
  "content_hash": null,
  "slug": "sabidussi-formalization-upstream-lean-v1",
  "type": "formalization",
  "title": "Pinned Lean proof in sabidussi-lean",
  "summary": "A public Lean 4.31.0 development proves the compatibility endpoint and records a clean upstream audit; controlled TheoremDB verification is still pending.",
  "relevance": "This is a complete public formal proof of the packet's compatibility target in a pinned Lean world, awaiting replay by TheoremDB's verifier.",
  "relevance_source": "recorded",
  "body": "The endpoint `Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary` takes an explicit Euler tour and a minimum-degree-four hypothesis, then produces an ordinary circuit decomposition compatible with that tour. Its graph model includes loops and parallel edges. The repository's production-source scan excludes `Challenge.lean`, which intentionally contains the statement placeholder used by Comparator. The production modules report no `sorry` or `admit`, and the upstream audit records only `propext`, `Classical.choice`, and `Quot.sound`. A separate Comparator workflow checks the solution wrapper against the reviewed statement. TheoremDB has pinned these materials but has not executed them inside its own controlled verifier.",
  "status": "pending_verification",
  "evidence_grade": "unverified_formalization",
  "scope": {
    "kind": "universal",
    "statement": "the circuit-decomposition consequence for the finite endpoint multigraph model represented by Sabidussi.LoopMultigraph"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "lean4_formalization_source",
    "command": "lake build && lake env lean Sabidussi/Audit.lean",
    "entrypoint": "Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary",
    "runtime": "Lean 4.31.0 with mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8",
    "citation": {
      "url": "https://github.com/gexahedron/sabidussi-lean/tree/da2f6ff7a7c7cc04e9ad34a53c3b6b8a18bd9ffa",
      "locator": "Sabidussi/OrdinaryCircuit.lean theorem Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary and VERIFICATION.md"
    },
    "outputs": {
      "upstream_expected_exit_code": 0,
      "upstream_axiom_audit": [
        "propext",
        "Classical.choice",
        "Quot.sound"
      ],
      "upstream_comparator": "reported passing",
      "theoremdb_controlled_verification": "pending"
    },
    "missing": [
      "source"
    ]
  },
  "formal_statement": "theorem Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary\n    {G : LoopMultigraph V E} (T : G.EulerTour)\n    (hmin : ∀ v : V, 4 ≤ G.degree v) :\n    ∃ S : G.OrdinaryCircuitDecomposition, S.Compatible T",
  "source": {
    "url": "https://github.com/gexahedron/sabidussi-lean/tree/da2f6ff7a7c7cc04e9ad34a53c3b6b8a18bd9ffa",
    "locator": "Sabidussi/OrdinaryCircuit.lean theorem Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary and VERIFICATION.md"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R1823",
      "title": "A compatible circuit decomposition is claimed for every eligible Euler tour",
      "object_type": "claim",
      "relation": "formalizes",
      "direction": "outgoing"
    },
    {
      "slug": "sabidussi-compatibility-conjecture",
      "title": "sabidussi compatibility conjecture",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}