Problem packetResearch packetR196
Rank and Smith normal form follow from the determinant formula
Link to a section
The record cites sources for its explanation.
Recorded status: established
Recorded scope: every positive matrix order n
Complete recorded scope and conditions
{
"kind": "universal",
"statement": "every positive matrix order n"
}Originating problem: Determinants of the disjoint-binary-support matrix
Authored record and scope
- Authored title
- Rank and Smith normal form follow from the determinant formula
- Record type
- claim
- Stored status
- established
- Evidence grade
- sourced
- Recorded scope data
- { "kind": "universal", "statement": "every positive matrix order n" }
2Authored explanation
At even order, the determinant is a unit, so \(A_n\) has full rank and Smith normal form equal to the identity. At odd order \(n=2m+1\), the kernel argument gives rank at most \(n-1\). The leading \(2m\times2m\) principal minor is \(A_{2m}\), whose determinant is a unit. Therefore the rank is exactly \(n-1\), and the Smith normal form is \(\operatorname{diag}(1,\ldots,1,0)\).
Continue this work
Replay material: source only
3Evidence
A verification source is cited. This record has no executable replay attached.
Verification source: arxiv.org ↗, Immediate corollary of the exact determinant and unimodular-minor argument
4How it connects
Uses
- claim
Recorded for
- problem
Cite this record
Cite the original sources separately.
Machine-readable record
Copy the structured record when continuing this work with an agent.
{
"schema": "theoremdb-agent-record-v1",
"ref": "R196",
"content_hash": null,
"slug": "dbm-claim-rank-smith-form",
"type": "claim",
"title": "Rank and Smith normal form follow from the determinant formula",
"summary": "Even orders are unimodular; odd orders have rank \\(n-1\\) and one zero Smith invariant.",
"relevance": "This records a result, observation, or conjecture used to assess the target problem.",
"relevance_source": "derived",
"body": "At even order, the determinant is a unit, so \\(A_n\\) has full rank and Smith normal form equal to the identity. At odd order \\(n=2m+1\\), the kernel argument gives rank at most \\(n-1\\). The leading \\(2m\\times2m\\) principal minor is \\(A_{2m}\\), whose determinant is a unit. Therefore the rank is exactly \\(n-1\\), and the Smith normal form is \\(\\operatorname{diag}(1,\\ldots,1,0)\\).",
"status": "established",
"evidence_grade": "sourced",
"scope": {
"kind": "universal",
"statement": "every positive matrix order n"
},
"reproduction": {
"schema": "theoremdb-reproduction-v1",
"readiness": "source_only",
"kind": "claim",
"citation": {
"url": "https://arxiv.org/abs/2210.12913",
"locator": "Immediate corollary of the exact determinant and unimodular-minor argument"
},
"missing": [
"source",
"command",
"runtime",
"expected_output"
]
},
"formal_statement": null,
"source": {
"url": "https://arxiv.org/abs/2210.12913",
"locator": "Immediate corollary of the exact determinant and unimodular-minor argument"
},
"models": [],
"continuation": null,
"relations": [
{
"slug": "R194",
"title": "Exact determinant of the disjoint-binary-support matrix",
"object_type": "claim",
"relation": "uses",
"direction": "outgoing"
},
{
"slug": "disjoint-binary-support-determinant",
"title": "disjoint binary support determinant",
"object_type": "problem",
"relation": "recorded_for",
"direction": "outgoing"
}
]
}6Provenance
View source, identifiers, and projection details
A statement this project treats as settled at the recorded evidence grade, with the work that backs it.