{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R307",
  "content_hash": null,
  "slug": "fib-claim-total-unimodular-review-pending",
  "type": "claim",
  "title": "Every Fibonacci-sum matrix is totally unimodular",
  "summary": "Every square minor of every \\(M_n\\) has determinant in \\(\\{-1,0,1\\}\\).",
  "relevance": "For fib problem determinant range; fib problem nonzero support, record fib-claim-total-unimodular-review-pending (“Every Fibonacci-sum matrix is totally unimodular”) records a bound, answer, status fact, or structural consequence. The record states: Every square minor of every \\(M_n\\) has determinant in \\(\\{-1,0,1\\}\\).",
  "relevance_source": "recorded",
  "body": "Proof. Let \\(Q_n\\) be the bipartite support graph of \\(M_n\\), with row vertices \\(r_i\\) and column vertices \\(c_j\\) joined when \\(i+j\\) is Fibonacci.\n\nFirst, \\(Q_n\\) is chordal bipartite. On a cycle, choose a vertex with largest numerical label \\(m\\) and suppose it is \\(r_m\\). If \\(q_k\\le m<q_{k+1}\\), its two cycle neighbors must have labels \\(a=q_{k+1}-m\\) and \\(b=q_{k+2}-m\\). The vertex \\(c_b\\) has only two neighbors with labels at most \\(m\\): \\(r_m\\) and \\(r_z\\), where \\(z=m-q_k\\). Since \\(a+z=q_{k-1}\\), the edge \\(r_zc_a\\) is a chord of every cycle longer than four.\n\nSecond, every edge of \\(Q_n\\) lies in at most two four-cycles. For a four-cycle on rows \\(x<X\\) and columns \\(y<Y\\), its corner sums \\(A=x+y\\), \\(B=x+Y\\), \\(C=X+y\\), and \\(D=X+Y\\) are Fibonacci and satisfy \\(A+D=B+C\\). If \\(B\\le C\\), Fibonacci growth forces \\(B=C=q_t\\), \\(A=q_{t-2}\\), and \\(D=q_{t+1}\\). Thus both row and column increments equal \\(q_{t-1}\\). For an edge whose endpoint labels sum to \\(q_s\\), there is at most one square in which it is the low corner. A high-corner square requires both labels to exceed \\(q_{s-2}\\). A middle-corner square requires one label to exceed \\(q_{s-1}\\). These requirements cannot occur together because \\(q_s=q_{s-1}+q_{s-2}\\), and the two middle orientations cannot both occur.\n\nThird, \\(Q_n\\) is outerplanar by induction. When the new label \\(m\\) has one available Fibonacci sum, \\(r_m\\) and \\(c_m\\) add pendant edges. When \\(2m=q_{k+2}\\), the two new vertices complete one square along an old diagonal edge. When \\(2m>q_{k+2}\\), they complete two squares along vertex-disjoint old edges, using two old pendant vertices. Each attachment edge must border the outer face. An internal attachment edge would border two bounded faces. Chordal bipartiteness makes both faces squares, and the new square would place that edge in three four-cycles, contradicting the preceding paragraph.\n\nNow take a square submatrix \\(B\\) of \\(M_n\\) with even row and column sums. Its support is an induced subgraph \\(H\\) of \\(Q_n\\), so \\(H\\) is outerplanar and chordal bipartite, and every vertex of \\(H\\) has even degree. Each nontrivial component has no bridges. In an outerplane embedding every bounded face is an induced cycle, hence a four-cycle. Checkerboard-color the faces with the outer face white. Every edge borders exactly one black face, so \\(|E(H)|\\) is four times the number of black faces. The sum of the entries of \\(B\\) is therefore divisible by four.\n\nCamion's criterion says that 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. It applies to \\(M_n\\). Hence every square minor of \\(M_n\\) lies in \\(\\{-1,0,1\\}\\), including \\(\\det M_n\\). The complete indexed argument and its verification boundary are preserved in research/fibonacci/total_unimodularity_proof.md.",
  "status": "supported",
  "evidence_grade": "mathematical_argument",
  "scope": {
    "kind": "universal",
    "statement": "every square minor of every matrix M_n, for 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": "Self-contained proof in research/fibonacci/total_unimodularity_proof.md"
    },
    "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": "Self-contained proof in research/fibonacci/total_unimodularity_proof.md"
  },
  "models": [],
  "relations": [
    {
      "slug": "R919",
      "title": "Every Fibonacci-sum matrix is totally unimodular",
      "object_type": "claim",
      "relation": "supersedes",
      "direction": "incoming",
      "metadata": {
        "reason": "The exact determinant-range consequence has been verified in Lean; the stronger prose claim keeps its independent-review boundary."
      }
    },
    {
      "slug": "R309",
      "title": "Every nonsingular Fibonacci-sum matrix is unimodular",
      "object_type": "claim",
      "relation": "strengthens",
      "direction": "outgoing"
    },
    {
      "slug": "R293",
      "title": "Lucas sequences may share total unimodularity",
      "object_type": "claim",
      "relation": "generalizes",
      "direction": "incoming"
    },
    {
      "slug": "R281",
      "title": "Prove total unimodularity",
      "object_type": "attempt",
      "relation": "addresses",
      "direction": "incoming"
    },
    {
      "slug": "R284",
      "title": "A complete AI-generated proof was reported",
      "object_type": "claim",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "fib-problem-determinant-range",
      "title": "Fibonacci-sum indicator determinant conjecture",
      "object_type": "problem",
      "relation": "claims_resolution_of",
      "direction": "outgoing"
    },
    {
      "slug": "R306",
      "title": "The matrices may be totally unimodular",
      "object_type": "claim",
      "relation": "supersedes",
      "direction": "outgoing",
      "metadata": {
        "reason": "This revision records the independent-review boundary explicitly."
      }
    }
  ]
}