Matrix theory

Results in Matrix theory

• Selected result:

  Matrix-pencil rank distance as an explicit completion problem

  ProvedDodig–Stošić conjecture on bounded rank perturbations of matrix pencils

  Mathematics · Matrix theory · standalone Lean package

  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.

  Manuscript: Matrix-pencil rank distance as an explicit completion problem · Lean proof: Matrix-pencil rank distance as an explicit completion problem · Verification: Matrix-pencil rank distance as an explicit completion problem

• Selected result:

  Counterexamples to the Kronecker-square lower bound for nonnegative rank

  DisprovedVandaele–Gillis–Glineur–Tuyttens conjecture rank₊(M ⊗ M) ≥ rank₊(M) rank(M)

  Mathematics · Matrix theory · standalone Lean package

  For every k ≥ 0 an explicit rational nonnegative matrix C of order k + 11, rank k + 10 and nonnegative rank k + 11 has rank₊(C ⊗ C) ≤ (k + 10)² + 9, at least k + 1 below the conjectured bound rank₊(C) rank(C).

  Manuscript: Counterexamples to the Kronecker-square lower bound for nonnegative rank · Lean proof: Counterexamples to the Kronecker-square lower bound for nonnegative rank · Verification: Counterexamples to the Kronecker-square lower bound for nonnegative rank

• Selected result:

  Finite real counterexamples and spectral obstructions for q-permanent monotonicity

  Disproved for real symmetric positive-definite matricesReal-symmetric case of the Bapat–Lal q-permanent monotonicity conjecture on [−1,1]

  Mathematics · Matrix theory · standalone Lean package

  An explicit integer positive-definite matrix of order 896 has a q-permanent that strictly decreases between two explicit rationals in (0,1); counterexamples exist in every order N ≥ 896.

  Manuscript: Finite real counterexamples and spectral obstructions for q-permanent monotonicity · Lean proof: Finite real counterexamples and spectral obstructions for q-permanent monotonicity · Verification: Finite real counterexamples and spectral obstructions for q-permanent monotonicity

• Gyires's permanent inequality for structured matrices

  Partially resolvedGyires's permanent inequality for doubly stochastic matrices (Cheon–Wanless Conjecture 20)

  Mathematics · Matrix theory · shared Lean library

  Proves Gyires's permanent inequality for nonnegative circulants of orders 5, 6 and 7, permutation polynomials aI+bQ+cQ² and four-block matrices in all orders, one-exceptional-column/row matrices, and rank ≤ 2 through order 15.

  Manuscript: Gyires's permanent inequality for structured matrices · Lean proof: Gyires's permanent inequality for structured matrices · Verification: Gyires's permanent inequality for structured matrices

• Real positive-definite counterexamples to extended q-permanent monotonicity

  DisprovedDa Fonseca's q-permanent (μ-permanent) monotonicity conjecture

  Mathematics · Matrix theory · shared Lean library

  A real symmetric positive-definite 5×5 matrix has q-permanent 8,968,822,249 at q = 14 and 7,441,960,000 at q = 15; for each real q₀ > 1 a positive-definite matrix (size depending on q₀) has negative derivative at q₀.

  Manuscript: Real positive-definite counterexamples to extended q-permanent monotonicity · Lean proof: Real positive-definite counterexamples to extended q-permanent monotonicity · Verification: Real positive-definite counterexamples to extended q-permanent monotonicity

• An unbounded obstruction to projection AM–GM in Loewner order

  CounterexampleProjection AM–GM inequality in Loewner order for symmetrized products of projections

  Mathematics · Matrix theory · standalone Lean package

  Three rational rank-one orthogonal projections in ℝ³ have symmetrized product G ⋠ M³, M their mean (quadratic form −8/243), and for every real C some such triple with positive-definite mean has G ⋠ C·M³.

  Manuscript: An unbounded obstruction to projection AM–GM in Loewner order · Lean proof: An unbounded obstruction to projection AM–GM in Loewner order · Verification: An unbounded obstruction to projection AM–GM in Loewner order

• A polygon enclosure fails for sums of normal matrices

  CounterexampleKovačec's polygon enclosure conjecture for determinants of sums of normal matrices

  Mathematics · Matrix theory · standalone Lean package

  Normal 3×3 matrices with spectra (0, 1, i) and (−1−i, 1, −1+i) give det(A+B) = 2/3 + 2i/9, outside every bounded component closure of ℂ∖Γ, Γ the exterior boundary of the transposition graph, yet inside the permutation-value hull.

  Manuscript: A polygon enclosure fails for sums of normal matrices · Lean proof: A polygon enclosure fails for sums of normal matrices · Verification: A polygon enclosure fails for sums of normal matrices