Math and TheoryMatrix-pencil rank distance as an explicit completion problem
Selected result in this collection
Problem and result
- Problem
- Dodig–Stošić conjecture on bounded rank perturbations of matrix pencils
- Posed in
- Dodig and Stošić, 'Is the bounded rank perturbations problem for matrix pencils just a completion problem?', Electron. J. Linear Algebra 41 (2025), 491–510, Conjecture 1
- Status
- Proved
- Result
- Over any infinite field, pencils A, B have δ(A,B) ≤ x exactly when K_{c,d}(A) is a constant full-rank compression of K_{c,d}(B) ⊕ (t − d)I_x; a cited linearization theorem then gives Conjecture 1 over algebraically closed fields.
Abstract
Let A and B be m × n matrix pencils over an infinite field and δ(A, B) the least normal rank of A′ − B′ over pencils A′, B′ strictly equivalent to A, B. For distinct c, d and every x ≥ 0, δ(A, B) ≤ x exactly when an explicit (2m+n) × (2n+m) dilation K_{c,d}(A) is obtained from K_{c,d}(B) ⊕ (t − d)I_x by one constant full-row-rank and one constant full-column-rank matrix. No regularity, rank or spectral condition is imposed, and the anchors may be eigenvalues. Over an algebraically closed field and at anchors outside the spectra, a known block minimal bases theorem turns this into Conjecture 1 of Dodig and Stošić: the bounded rank perturbation problem for matrix pencils is a completion problem.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Matrix theory
- Subject
- Matrix theory
- Result type
- Theorem resolving a published conjecture and reproducible proof package
- Formal proof
- Standalone Lean package
- Family
matrix-pencil-completion- Keywords
- matrix pencils, bounded rank perturbations, matrix pencil completion, strict equivalence, normal rank, Kronecker canonical form, block minimal bases, Dodig–Stošić conjecture
Statement and scope
Formal scope. The explicit equivalence over every infinite field, for arbitrary rectangular pencils, every border size and distinct anchors including eigenvalues, and the common-summand cancellation are formalized in two Lean projects. The identification with the barred pencils of the conjecture uses a published linearization theorem and is not formalized.
A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.
Manuscript
- PDF on this site
manuscript.pdf319 KB- PDF on GitHub
papers/mathematics/ matrix-pencil-completion/ manuscript.pdf - LaTeX source
papers/mathematics/ matrix-pencil-completion/ manuscript.tex
Formal proof
This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.
- Proof package
papers/mathematics/ matrix-pencil-completion/ - Lean project
papers/7 Lean filesmathematics/ matrix-pencil-completion/ lean_p1/ - Lakefile
papers/mathematics/ matrix-pencil-completion/ lean_p1/ lakefile.toml - Toolchain
leanprover/lean4:v4.35.0-rc3 - Lean project
papers/69 Lean filesmathematics/ matrix-pencil-completion/ lean_p1_converse/ - Lakefile
papers/mathematics/ matrix-pencil-completion/ lean_p1_converse/ lakefile.toml - Toolchain
leanprover/lean4:v4.35.0-rc3 - Library roots
- Library roots
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
lake exe cache get
bash verify.sh
lake build MatCP1
lake env lean ../lean_p1/AxiomAudit.lean- README
papers/mathematics/ matrix-pencil-completion/ README.md - Verification guide
papers/mathematics/ matrix-pencil-completion/ verification/ README.md - Verification record
papers/mathematics/ matrix-pencil-completion/ VERIFICATION.md - Authorship
papers/mathematics/ matrix-pencil-completion/ AUTHORSHIP.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Prior work. Dodig and Stošić, 2025.
Questions and answers
Is the Dodig–Stošić conjecture true?
This preprint proves it over every algebraically closed field: the bounded rank perturbation problem for matrix pencils is a completion problem. The final identification with the conjecture's barred pencils uses a published block minimal bases theorem of Dopico, Lawrence, Pérez and Van Dooren (2018). Dodig and Stošić had proved it when the rank bound is one, for full-row-rank pencils, and when the bound equals the rank distance.
What is the main theorem?
For distinct anchors c, d over any infinite field, δ(A, B) ≤ x exactly when the explicit (2m+n) × (2n+m) dilation K_{c,d}(A) is obtained from K_{c,d}(B) ⊕ (t − d)I_x by one constant full-row-rank matrix on the left and one constant full-column-rank matrix on the right. No regularity, rank or spectral condition is imposed, and the anchors may be eigenvalues.
Is the proof formally verified?
The explicit equivalence over every infinite field and the common-summand cancellation are formalized in two Lean 4 projects. The identification with barred pencils is cited and not formalized; three directly relevant articles were not read in full, and historical priority is not certified.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@misc{goyal2026matrixpencilcompletion,
author = {Goyal, Dev D.},
title = {Matrix-Pencil Rank Distance as an Explicit Completion Problem},
year = {2026},
month = oct,
note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/matrix-pencil-completion}
}