Open Research Index

A Unified Framework for Formalizing Matrix Decomposition Proofs

Wanli Ma, Zichen Wang, Zaiwen Wen

arXivarxiv/2607.05874Jul 7, 2026math.NAscore 0

Existence proofs for many matrix decompositions share a recursive routine: a local transformation prepares the matrix, a slice is selected, a recursive solution is obtained, and the result is lifted and transported back. Formalizing this routine uniformly in dependent type theory is difficult because recursive subproblems may change index types, and reconstruction must preserve structural predicates across block embeddings and reindexings. We develop a Lean~4 framework that separates decomposition schemas, transformations, reduction strategies, measures, lifting, transport, and subtype…

SourceJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/arxiv/2607.05874
curl -X POST /api/v1/records/arxiv/2607.05874/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2607.05874/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'