{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R920",
  "content_hash": null,
  "slug": "fib-claim-determinant-range-formally-proved-v2",
  "type": "claim",
  "title": "The determinant is always minus one, zero, or one",
  "summary": "For every integer n >= 1, the determinant of the Fibonacci-sum indicator matrix M_n belongs to {-1,0,1}.",
  "relevance": "For fib problem determinant range; fib problem nonzero support, record fib-claim-determinant-range-formally-proved-v2 (“The determinant is always minus one, zero, or one”) records a bound, answer, status fact, or structural consequence. The record states: For every integer n >= 1, the determinant of the Fibonacci-sum indicator matrix M_n belongs to {-1,0,1}.",
  "relevance_source": "recorded",
  "body": "Proof. Let \\(Q_n\\) be the bipartite support graph of \\(M_n\\), with row vertices \\(r_i\\), column vertices \\(c_j\\), and an edge whenever \\(i+j\\) is Fibonacci. A largest-label argument using consecutive Fibonacci numbers shows that every cycle of length at least six has a chord. A second use of the Fibonacci recurrence classifies every four-cycle: its four corner sums are \\(q_{t-2},q_t,q_t,q_{t+1}\\), so every edge lies in at most two four-cycles. These facts support an induction that embeds \\(Q_n\\) outerplanarly.\n\nNow take any square submatrix \\(B\\) of \\(M_n\\) whose row and column sums are even. Its support graph is an Eulerian induced subgraph of \\(Q_n\\). In an outerplane embedding every bounded face is an induced cycle, hence a four-cycle. Color the faces black and white with the outer face white. Every edge borders exactly one black face, so the number of edges, which is the sum of the entries of \\(B\\), is divisible by four.\n\nCamion's criterion now applies: a \\(0,\\!\\pm\\!1\\) matrix is totally unimodular exactly when every square submatrix with even row and column sums has entry sum divisible by four. Therefore every square minor of \\(M_n\\) belongs to \\(\\{-1,0,1\\}\\). In particular, \\(\\det(M_n)\\in\\{-1,0,1\\}\\) for every \\(n\\ge1\\).",
  "status": "established",
  "evidence_grade": "mathematical_argument",
  "scope": {
    "kind": "universal",
    "statement": "every matrix size n >= 1"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://mathoverflow.net/questions/513340/is-the-determinant-of-this-fibonacci-sum-indicator-matrix-always-1-0-or/513372",
      "locator": "research/fibonacci/total_unimodularity_proof.md and formal/lean/TheoremDB/Fibonacci/DeterminantRange.lean"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://mathoverflow.net/questions/513340/is-the-determinant-of-this-fibonacci-sum-indicator-matrix-always-1-0-or/513372",
    "locator": "research/fibonacci/total_unimodularity_proof.md and formal/lean/TheoremDB/Fibonacci/DeterminantRange.lean"
  },
  "models": [],
  "relations": [
    {
      "slug": "fib-problem-determinant-range",
      "title": "Fibonacci-sum indicator determinant conjecture",
      "object_type": "problem",
      "relation": "resolves",
      "direction": "outgoing",
      "metadata": {
        "verification_record": "fib-formalization-determinant-range-lean-v1-lean-5e5b725441ec-verified-e4e988240074"
      }
    },
    {
      "slug": "R918",
      "title": "The determinant is always minus one, zero, or one",
      "object_type": "claim",
      "relation": "supersedes",
      "direction": "outgoing",
      "metadata": {
        "reason": "Pairs the verified determinant-range result with its complete human-readable proof."
      }
    }
  ]
}