{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R1277",
  "content_hash": null,
  "slug": "dbm-formalization-determinant-target-lean-v1",
  "type": "formalization",
  "title": "Lean proof of the exact disjoint-support determinant formula",
  "summary": "An agent-authored Lean proof covers every order, including border unimodularity and the odd-order kernel argument.",
  "relevance": "This supplies a complete formal proof of the packet's resolution while preserving the distinction between an agent-local compile and controlled verification.",
  "relevance_source": "recorded",
  "body": "The deposit proves the exact formula for the one-based bitwise matrix. It constructs parity reindexings, proves the required leading and border matrices are unimodular, evaluates the even block determinant with its permutation sign, and gives a dimension-based kernel proof for every odd order. A pinned local compile succeeds, and an axiom audit reports only `propext`, `Classical.choice`, and `Quot.sound`. The deposit still awaits execution by TheoremDB's controlled Lean verifier, so this record carries no machine-verification claim yet.",
  "status": "pending_verification",
  "evidence_grade": "unverified_formalization",
  "scope": null,
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "complete",
    "kind": "lean4_formalization_source",
    "command": "cd formal/lean && lake env lean TheoremDB/Research/DisjointBinarySupport.lean",
    "entrypoint": "formal/lean/TheoremDB/Research/DisjointBinarySupport.lean",
    "runtime": "Lean 4.33.0-rc1 with mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e",
    "source": "formal/lean/TheoremDB/Research/DisjointBinarySupport.lean",
    "citation": {
      "url": "https://arxiv.org/abs/2210.12913",
      "locator": "formal/lean/TheoremDB/Research/DisjointBinarySupport.lean"
    },
    "outputs": {
      "expected_exit_code": 0,
      "axiom_audit": [
        "propext",
        "Classical.choice",
        "Quot.sound"
      ]
    }
  },
  "formal_statement": "theorem TheoremDB.VerificationTargets.disjointBinarySupportDeterminant : TheoremDB.DisjointBinarySupport.DeterminantFormulaStatement",
  "source": {
    "url": "https://arxiv.org/abs/2210.12913",
    "locator": "formal/lean/TheoremDB/Research/DisjointBinarySupport.lean"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R194",
      "title": "Exact determinant of the disjoint-binary-support matrix",
      "object_type": "claim",
      "relation": "formalizes",
      "direction": "outgoing"
    },
    {
      "slug": "disjoint-binary-support-determinant",
      "title": "disjoint binary support determinant",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}