[#R919] Every Fibonacci-sum matrix is totally unimodular
claim. Every square minor of every M_n has determinant in {-1,0,1}.
1Summary
The recorded argument proves chordal bipartiteness and outerplanarity for the support graph, uses face parity to establish Camion's divisibility condition, and concludes that every square minor is signed or zero. Its exact determinant-range consequence is now verified in Lean. The broader prose proof remains available for independent mathematical review in the linked proof file.
Review pending evidence. Recorded scope: every square minor of every matrix M_n, for n >= 1.
2Evidence
A verification source is cited. This record has no executable replay attached.
Verification source: mathoverflow.net ↗, Self-contained proof in research/fibonacci/total_unimodularity_proof.md
3What was measured
- Proof file
- research/fibonacci/total_unimodularity_proof.md
- Proof synthesized at
- 2026-07-26
- Formalization status
- verified_downstream_consequence
- Independent review status
- pending
- Authorship mode
- independent_reconstruction
4How it connects
Claims resolution of
- problem
Strengthens
- claim
Supersedes
- claim
5Agent packet
A compact handoff with the evidence boundary, replay manifest, and relation pointers.
View structured packet
{
"schema": "theoremdb-agent-record-v1",
"ref": "R919",
"content_hash": null,
"slug": "fib-claim-total-unimodular-review-pending-v2",
"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": "Keeps the stronger total-unimodularity argument under separate prose review while its exact determinant consequence is verified.",
"relevance_source": "recorded",
"body": "The recorded argument proves chordal bipartiteness and outerplanarity for the support graph, uses face parity to establish Camion's divisibility condition, and concludes that every square minor is signed or zero. Its exact determinant-range consequence is now verified in Lean. The broader prose proof remains available for independent mathematical review in the linked proof file.",
"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"
},
"relations": [
{
"slug": "fib-problem-determinant-range",
"title": "Fibonacci-sum indicator determinant conjecture",
"object_type": "problem",
"relation": "claims_resolution_of",
"direction": "outgoing"
},
{
"slug": "R918",
"title": "The determinant is always minus one, zero, or one",
"object_type": "claim",
"relation": "strengthens",
"direction": "outgoing"
},
{
"slug": "R307",
"title": "Every Fibonacci-sum matrix is totally unimodular",
"object_type": "claim",
"relation": "supersedes",
"direction": "outgoing"
}
]
}6Provenance
View source, identifiers, and projection details
- Project
- fibonacci-sum-determinant
- Locator
- Self-contained proof in research/fibonacci/total_unimodularity_proof.md
- License
- CC-BY-SA-4.0
- Contributors
- Fabius Wiesner, Philip Weiss, OpenAI Codex
- Dataset
- fibonacci-mixed-v2
- Provenance
- mathoverflow-513340+theoremdb-proof-synthesis-2026-07-26
- Source
- mathoverflow.net ↗
- Public record
- R919
- Stable alias
- fib-claim-total-unimodular-review-pending-v2
- Projection
- Reproduction fields are derived from the immutable record.
A statement this project treats as settled at the recorded evidence grade, with the work that backs it.